Analysing the implicit complexity of programs
Identifieur interne : 000723 ( PascalFrancis/Checkpoint ); précédent : 000722; suivant : 000724Analysing the implicit complexity of programs
Auteurs : J. Y. Marion [France]Source :
- Information and computation : (Print) [ 0890-5401 ] ; 2003.
Descripteurs français
- Pascal (Inist)
English descriptors
- KwdEn :
Abstract
We study termination proofs in order to (i) determine computational complexity of programs and (ii) generate efficient programs from the complexity analysis. For this, we construct a termination ordering, called light multiset path ordering (LMPO), which is a restriction of the multiset path ordering. We establish that the class of first order functional programs on lists which is terminating by LMPO characterises exactly the functions computable in polynomial time.
Affiliations:
Links toward previous steps (curation, corpus...)
Links to Exploration step
Pascal:03-0426819Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Analysing the implicit complexity of programs</title><author><name sortKey="Marion, J Y" sort="Marion, J Y" uniqKey="Marion J" first="J. Y." last="Marion">J. Y. Marion</name><affiliation wicri:level="3"><inist:fA14 i1="01"><s1>Loria Calligramme Project B.P. 239</s1><s2>54506 Vandoeuvre-lès-Nancy</s2><s3>FRA</s3><sZ>1 aut.</sZ></inist:fA14><country>France</country><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Vandœuvre-lès-Nancy</settlement></placeName></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">INIST</idno><idno type="inist">03-0426819</idno><date when="2003">2003</date><idno type="stanalyst">PASCAL 03-0426819 INIST</idno><idno type="RBID">Pascal:03-0426819</idno><idno type="wicri:Area/PascalFrancis/Corpus">000764</idno><idno type="wicri:Area/PascalFrancis/Curation">000279</idno><idno type="wicri:Area/PascalFrancis/Checkpoint">000723</idno><idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000723</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Analysing the implicit complexity of programs</title><author><name sortKey="Marion, J Y" sort="Marion, J Y" uniqKey="Marion J" first="J. Y." last="Marion">J. Y. Marion</name><affiliation wicri:level="3"><inist:fA14 i1="01"><s1>Loria Calligramme Project B.P. 239</s1><s2>54506 Vandoeuvre-lès-Nancy</s2><s3>FRA</s3><sZ>1 aut.</sZ></inist:fA14><country>France</country><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Vandœuvre-lès-Nancy</settlement></placeName></affiliation></author></analytic><series><title level="j" type="main">Information and computation : (Print)</title><title level="j" type="abbreviated">Inf. comput. : (Print)</title><idno type="ISSN">0890-5401</idno><imprint><date when="2003">2003</date></imprint></series></biblStruct></sourceDesc><seriesStmt><title level="j" type="main">Information and computation : (Print)</title><title level="j" type="abbreviated">Inf. comput. : (Print)</title><idno type="ISSN">0890-5401</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Computational complexity</term><term>Computer theory</term><term>First order</term><term>Functional programming</term><term>Implicit theory</term><term>Multiset path ordering</term><term>Polynomial time</term><term>Program analysis</term><term>Program complexity</term><term>Rewriting systems</term></keywords><keywords scheme="Pascal" xml:lang="fr"><term>Informatique théorique</term><term>Complexité calcul</term><term>Théorie implicite</term><term>Analyse programme</term><term>Complexité programme</term><term>Temps polynomial</term><term>Programmation fonctionnelle</term><term>Ordre 1</term><term>Système réécriture</term><term>Relation ordre chemin ensemble multiple</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">We study termination proofs in order to (i) determine computational complexity of programs and (ii) generate efficient programs from the complexity analysis. For this, we construct a termination ordering, called light multiset path ordering (LMPO), which is a restriction of the multiset path ordering. We establish that the class of first order functional programs on lists which is terminating by LMPO characterises exactly the functions computable in polynomial time.</div></front></TEI><inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0890-5401</s0></fA01><fA02 i1="01"><s0>INFCEC</s0></fA02><fA03 i2="1"><s0>Inf. comput. : (Print)</s0></fA03><fA05><s2>183</s2></fA05><fA06><s2>1</s2></fA06><fA08 i1="01" i2="1" l="ENG"><s1>Analysing the implicit complexity of programs</s1></fA08><fA09 i1="01" i2="1" l="ENG"><s1>Special issue: ICC '99</s1></fA09><fA11 i1="01" i2="1"><s1>MARION (J. Y.)</s1></fA11><fA12 i1="01" i2="1"><s1>DAWAR (Anuj)</s1><s9>ed.</s9></fA12><fA12 i1="02" i2="1"><s1>LEIVANT (Daniel)</s1><s9>ed.</s9></fA12><fA14 i1="01"><s1>Loria Calligramme Project B.P. 239</s1><s2>54506 Vandoeuvre-lès-Nancy</s2><s3>FRA</s3><sZ>1 aut.</sZ></fA14><fA20><s1>2-18</s1></fA20><fA21><s1>2003</s1></fA21><fA23 i1="01"><s0>ENG</s0></fA23><fA43 i1="01"><s1>INIST</s1><s2>8341</s2><s5>354000118344710010</s5></fA43><fA44><s0>0000</s0><s1>© 2003 INIST-CNRS. All rights reserved.</s1></fA44><fA45><s0>18 ref.</s0></fA45><fA47 i1="01" i2="1"><s0>03-0426819</s0></fA47><fA60><s1>P</s1><s2>C</s2></fA60><fA61><s0>A</s0></fA61><fA64 i1="01" i2="1"><s0>Information and computation : (Print)</s0></fA64><fA66 i1="01"><s0>USA</s0></fA66><fC01 i1="01" l="ENG"><s0>We study termination proofs in order to (i) determine computational complexity of programs and (ii) generate efficient programs from the complexity analysis. For this, we construct a termination ordering, called light multiset path ordering (LMPO), which is a restriction of the multiset path ordering. We establish that the class of first order functional programs on lists which is terminating by LMPO characterises exactly the functions computable in polynomial time.</s0></fC01><fC02 i1="01" i2="X"><s0>001D02A05</s0></fC02><fC02 i1="02" i2="X"><s0>001D01A03</s0></fC02><fC02 i1="03" i2="X"><s0>001A02A01F</s0></fC02><fC03 i1="01" i2="X" l="FRE"><s0>Informatique théorique</s0><s5>01</s5></fC03><fC03 i1="01" i2="X" l="ENG"><s0>Computer theory</s0><s5>01</s5></fC03><fC03 i1="01" i2="X" l="SPA"><s0>Informática teórica</s0><s5>01</s5></fC03><fC03 i1="02" i2="X" l="FRE"><s0>Complexité calcul</s0><s5>02</s5></fC03><fC03 i1="02" i2="X" l="ENG"><s0>Computational complexity</s0><s5>02</s5></fC03><fC03 i1="02" i2="X" l="SPA"><s0>Complejidad computación</s0><s5>02</s5></fC03><fC03 i1="03" i2="X" l="FRE"><s0>Théorie implicite</s0><s5>03</s5></fC03><fC03 i1="03" i2="X" l="ENG"><s0>Implicit theory</s0><s5>03</s5></fC03><fC03 i1="03" i2="X" l="SPA"><s0>Teoría implícita</s0><s5>03</s5></fC03><fC03 i1="04" i2="X" l="FRE"><s0>Analyse programme</s0><s5>04</s5></fC03><fC03 i1="04" i2="X" l="ENG"><s0>Program analysis</s0><s5>04</s5></fC03><fC03 i1="04" i2="X" l="SPA"><s0>Análisis programa</s0><s5>04</s5></fC03><fC03 i1="05" i2="X" l="FRE"><s0>Complexité programme</s0><s5>05</s5></fC03><fC03 i1="05" i2="X" l="ENG"><s0>Program complexity</s0><s5>05</s5></fC03><fC03 i1="05" i2="X" l="SPA"><s0>Complejidad programa</s0><s5>05</s5></fC03><fC03 i1="06" i2="X" l="FRE"><s0>Temps polynomial</s0><s5>06</s5></fC03><fC03 i1="06" i2="X" l="ENG"><s0>Polynomial time</s0><s5>06</s5></fC03><fC03 i1="06" i2="X" l="SPA"><s0>Tiempo polinomial</s0><s5>06</s5></fC03><fC03 i1="07" i2="X" l="FRE"><s0>Programmation fonctionnelle</s0><s5>07</s5></fC03><fC03 i1="07" i2="X" l="ENG"><s0>Functional programming</s0><s5>07</s5></fC03><fC03 i1="07" i2="X" l="SPA"><s0>Programación funcional</s0><s5>07</s5></fC03><fC03 i1="08" i2="X" l="FRE"><s0>Ordre 1</s0><s5>08</s5></fC03><fC03 i1="08" i2="X" l="ENG"><s0>First order</s0><s5>08</s5></fC03><fC03 i1="08" i2="X" l="SPA"><s0>Orden 1</s0><s5>08</s5></fC03><fC03 i1="09" i2="3" l="FRE"><s0>Système réécriture</s0><s5>09</s5></fC03><fC03 i1="09" i2="3" l="ENG"><s0>Rewriting systems</s0><s5>09</s5></fC03><fC03 i1="10" i2="X" l="FRE"><s0>Relation ordre chemin ensemble multiple</s0><s4>CD</s4><s5>96</s5></fC03><fC03 i1="10" i2="X" l="ENG"><s0>Multiset path ordering</s0><s4>CD</s4><s5>96</s5></fC03><fN21><s1>293</s1></fN21></pA><pR><fA30 i1="01" i2="1" l="ENG"><s1>ICC '99 Workshop on Implicit Computational Complexity</s1><s3>Trento ITA</s3><s4>1999-07</s4></fA30></pR></standard></inist><affiliations><list><country><li>France</li></country><region><li>Grand Est</li><li>Lorraine (région)</li></region><settlement><li>Vandœuvre-lès-Nancy</li></settlement></list><tree><country name="France"><region name="Grand Est"><name sortKey="Marion, J Y" sort="Marion, J Y" uniqKey="Marion J" first="J. Y." last="Marion">J. Y. Marion</name></region></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/PascalFrancis/Checkpoint
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000723 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Checkpoint/biblio.hfd -nk 000723 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= PascalFrancis
|étape= Checkpoint
|type= RBID
|clé= Pascal:03-0426819
|texte= Analysing the implicit complexity of programs
}}
| This area was generated with Dilib version V0.6.33. |  |