Analysing the implicit complexity of programs
Identifieur interne :
000764 ( PascalFrancis/Corpus );
précédent :
000763;
suivant :
000765
Analysing the implicit complexity of programs
Auteurs : J. Y. MarionSource :
-
Information and computation : (Print) [ 0890-5401 ] ; 2003.
RBID : Pascal:03-0426819
Descripteurs français
English descriptors
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.
Notice en format standard (ISO 2709)
Pour connaître la documentation sur le format Inist Standard.
pA |
A01 | 01 | 1 | | @0 0890-5401 |
---|
A02 | 01 | | | @0 INFCEC |
---|
A03 | | 1 | | @0 Inf. comput. : (Print) |
---|
A05 | | | | @2 183 |
---|
A06 | | | | @2 1 |
---|
A08 | 01 | 1 | ENG | @1 Analysing the implicit complexity of programs |
---|
A09 | 01 | 1 | ENG | @1 Special issue: ICC '99 |
---|
A11 | 01 | 1 | | @1 MARION (J. Y.) |
---|
A12 | 01 | 1 | | @1 DAWAR (Anuj) @9 ed. |
---|
A12 | 02 | 1 | | @1 LEIVANT (Daniel) @9 ed. |
---|
A14 | 01 | | | @1 Loria Calligramme Project B.P. 239 @2 54506 Vandoeuvre-lès-Nancy @3 FRA @Z 1 aut. |
---|
A20 | | | | @1 2-18 |
---|
A21 | | | | @1 2003 |
---|
A23 | 01 | | | @0 ENG |
---|
A43 | 01 | | | @1 INIST @2 8341 @5 354000118344710010 |
---|
A44 | | | | @0 0000 @1 © 2003 INIST-CNRS. All rights reserved. |
---|
A45 | | | | @0 18 ref. |
---|
A47 | 01 | 1 | | @0 03-0426819 |
---|
A60 | | | | @1 P @2 C |
---|
A61 | | | | @0 A |
---|
A64 | 01 | 1 | | @0 Information and computation : (Print) |
---|
A66 | 01 | | | @0 USA |
---|
C01 | 01 | | ENG | @0 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. |
---|
C02 | 01 | X | | @0 001D02A05 |
---|
C02 | 02 | X | | @0 001D01A03 |
---|
C02 | 03 | X | | @0 001A02A01F |
---|
C03 | 01 | X | FRE | @0 Informatique théorique @5 01 |
---|
C03 | 01 | X | ENG | @0 Computer theory @5 01 |
---|
C03 | 01 | X | SPA | @0 Informática teórica @5 01 |
---|
C03 | 02 | X | FRE | @0 Complexité calcul @5 02 |
---|
C03 | 02 | X | ENG | @0 Computational complexity @5 02 |
---|
C03 | 02 | X | SPA | @0 Complejidad computación @5 02 |
---|
C03 | 03 | X | FRE | @0 Théorie implicite @5 03 |
---|
C03 | 03 | X | ENG | @0 Implicit theory @5 03 |
---|
C03 | 03 | X | SPA | @0 Teoría implícita @5 03 |
---|
C03 | 04 | X | FRE | @0 Analyse programme @5 04 |
---|
C03 | 04 | X | ENG | @0 Program analysis @5 04 |
---|
C03 | 04 | X | SPA | @0 Análisis programa @5 04 |
---|
C03 | 05 | X | FRE | @0 Complexité programme @5 05 |
---|
C03 | 05 | X | ENG | @0 Program complexity @5 05 |
---|
C03 | 05 | X | SPA | @0 Complejidad programa @5 05 |
---|
C03 | 06 | X | FRE | @0 Temps polynomial @5 06 |
---|
C03 | 06 | X | ENG | @0 Polynomial time @5 06 |
---|
C03 | 06 | X | SPA | @0 Tiempo polinomial @5 06 |
---|
C03 | 07 | X | FRE | @0 Programmation fonctionnelle @5 07 |
---|
C03 | 07 | X | ENG | @0 Functional programming @5 07 |
---|
C03 | 07 | X | SPA | @0 Programación funcional @5 07 |
---|
C03 | 08 | X | FRE | @0 Ordre 1 @5 08 |
---|
C03 | 08 | X | ENG | @0 First order @5 08 |
---|
C03 | 08 | X | SPA | @0 Orden 1 @5 08 |
---|
C03 | 09 | 3 | FRE | @0 Système réécriture @5 09 |
---|
C03 | 09 | 3 | ENG | @0 Rewriting systems @5 09 |
---|
C03 | 10 | X | FRE | @0 Relation ordre chemin ensemble multiple @4 CD @5 96 |
---|
C03 | 10 | X | ENG | @0 Multiset path ordering @4 CD @5 96 |
---|
N21 | | | | @1 293 |
---|
|
pR |
A30 | 01 | 1 | ENG | @1 ICC '99 Workshop on Implicit Computational Complexity @3 Trento ITA @4 1999-07 |
---|
|
Format Inist (serveur)
NO : | PASCAL 03-0426819 INIST |
ET : | Analysing the implicit complexity of programs |
AU : | MARION (J. Y.); DAWAR (Anuj); LEIVANT (Daniel) |
AF : | Loria Calligramme Project B.P. 239/54506 Vandoeuvre-lès-Nancy/France (1 aut.) |
DT : | Publication en série; Congrès; Niveau analytique |
SO : | Information and computation : (Print); ISSN 0890-5401; Coden INFCEC; Etats-Unis; Da. 2003; Vol. 183; No. 1; Pp. 2-18; Bibl. 18 ref. |
LA : | Anglais |
EA : | 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. |
CC : | 001D02A05; 001D01A03; 001A02A01F |
FD : | Informatique théorique; Complexité calcul; Théorie implicite; Analyse programme; Complexité programme; Temps polynomial; Programmation fonctionnelle; Ordre 1; Système réécriture; Relation ordre chemin ensemble multiple |
ED : | Computer theory; Computational complexity; Implicit theory; Program analysis; Program complexity; Polynomial time; Functional programming; First order; Rewriting systems; Multiset path ordering |
SD : | Informática teórica; Complejidad computación; Teoría implícita; Análisis programa; Complejidad programa; Tiempo polinomial; Programación funcional; Orden 1 |
LO : | INIST-8341.354000118344710010 |
ID : | 03-0426819 |
Links to Exploration step
Pascal:03-0426819
Le 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><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>
</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>
</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><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>
</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>
<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>
<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>
<server><NO>PASCAL 03-0426819 INIST</NO>
<ET>Analysing the implicit complexity of programs</ET>
<AU>MARION (J. Y.); DAWAR (Anuj); LEIVANT (Daniel)</AU>
<AF>Loria Calligramme Project B.P. 239/54506 Vandoeuvre-lès-Nancy/France (1 aut.)</AF>
<DT>Publication en série; Congrès; Niveau analytique</DT>
<SO>Information and computation : (Print); ISSN 0890-5401; Coden INFCEC; Etats-Unis; Da. 2003; Vol. 183; No. 1; Pp. 2-18; Bibl. 18 ref.</SO>
<LA>Anglais</LA>
<EA>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.</EA>
<CC>001D02A05; 001D01A03; 001A02A01F</CC>
<FD>Informatique théorique; Complexité calcul; Théorie implicite; Analyse programme; Complexité programme; Temps polynomial; Programmation fonctionnelle; Ordre 1; Système réécriture; Relation ordre chemin ensemble multiple</FD>
<ED>Computer theory; Computational complexity; Implicit theory; Program analysis; Program complexity; Polynomial time; Functional programming; First order; Rewriting systems; Multiset path ordering</ED>
<SD>Informática teórica; Complejidad computación; Teoría implícita; Análisis programa; Complejidad programa; Tiempo polinomial; Programación funcional; Orden 1</SD>
<LO>INIST-8341.354000118344710010</LO>
<ID>03-0426819</ID>
</server>
</inist>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/PascalFrancis/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000764 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000764 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= PascalFrancis
|étape= Corpus
|type= RBID
|clé= Pascal:03-0426819
|texte= Analysing the implicit complexity of programs
}}
| This area was generated with Dilib version V0.6.33. Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022 | ![](Common/icons/LogoDilib.gif) |