On lexicographic termination ordering with space bound certifications
Identifieur interne : 009436 ( Main/Merge ); précédent : 009435; suivant : 009437On lexicographic termination ordering with space bound certifications
Auteurs : Guillaume Bonfante ; Jean-Yves Marion ; Jean-Yves MoyenSource :
English descriptors
Abstract
We propose a method to analyse the program space complexity, based on termination orderings. This method can be implemented to certify the runspace of programs. We demonstrate that the class of functions computed by first order functional programs over free algebras which terminate by Lexicographic Path Ordering and admit a polynomial quasi-interpretation, is exactly the class of functions computable in polynomial space.
Links toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: 002F16
- to stream Crin, to step Curation: 002F16
- to stream Crin, to step Checkpoint: 001531
Links to Exploration step
CRIN:bonfante01aLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="465">On lexicographic termination ordering with space bound certifications</title></titleStmt><publicationStmt><idno type="RBID">CRIN:bonfante01a</idno><date when="2001" year="2001">2001</date><idno type="wicri:Area/Crin/Corpus">002F16</idno><idno type="wicri:Area/Crin/Curation">002F16</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">002F16</idno><idno type="wicri:Area/Crin/Checkpoint">001531</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">001531</idno><idno type="wicri:Area/Main/Merge">009436</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">On lexicographic termination ordering with space bound certifications</title><author><name sortKey="Bonfante, Guillaume" sort="Bonfante, Guillaume" uniqKey="Bonfante G" first="Guillaume" last="Bonfante">Guillaume Bonfante</name></author><author><name sortKey="Marion, Jean Yves" sort="Marion, Jean Yves" uniqKey="Marion J" first="Jean-Yves" last="Marion">Jean-Yves Marion</name></author><author><name sortKey="Moyen, Jean Yves" sort="Moyen, Jean Yves" uniqKey="Moyen J" first="Jean-Yves" last="Moyen">Jean-Yves Moyen</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>lexicographic path ordering</term><term>polynomial space certification</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en" wicri:score="1436">We propose a method to analyse the program space complexity, based on termination orderings. This method can be implemented to certify the runspace of programs. We demonstrate that the class of functions computed by first order functional programs over free algebras which terminate by Lexicographic Path Ordering and admit a polynomial quasi-interpretation, is exactly the class of functions computable in polynomial space.</div></front></TEI></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Merge
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 009436 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 009436 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Merge
|type= RBID
|clé= CRIN:bonfante01a
|texte= On lexicographic termination ordering with space bound certifications
}}
| This area was generated with Dilib version V0.6.33. |  |