Actual arithmetic and feasibility
Identifieur interne : 001733 ( Crin/Checkpoint ); précédent : 001732; suivant : 001734Actual arithmetic and feasibility
Auteurs : Jean-Yves MarionSource :
English descriptors
- KwdEn :
Abstract
This paper presents a methodology for reasoning about the computational complexity of functional programs. We introduce a first order arithmetic \StrictTa which is a syntactic restriction of Peano arithmetic. We establish that the set of functions which are provably total in \StrictTa, is exactly the set of polynomial time functions.The cut-elimination process is polynomial time computable. Compared to others feasible arithmetics, \StrictTa is conceptually simpler. The main feature of \StrictTa concerns the treatment of the quantification. The range of quantifiers is restricted to the set of {\em actual terms} which is the set of constructor terms with variables. The inductive formulas are restricted to conjunctions of atomic formulas.
Links toward previous steps (curation, corpus...)
Links to Exploration step
CRIN:marion01aLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="174">Actual arithmetic and feasibility</title></titleStmt><publicationStmt><idno type="RBID">CRIN:marion01a</idno><date when="2001" year="2001">2001</date><idno type="wicri:Area/Crin/Corpus">002F10</idno><idno type="wicri:Area/Crin/Curation">002F10</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">002F10</idno><idno type="wicri:Area/Crin/Checkpoint">001733</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">001733</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Actual arithmetic and feasibility</title><author><name sortKey="Marion, Jean Yves" sort="Marion, Jean Yves" uniqKey="Marion J" first="Jean-Yves" last="Marion">Jean-Yves Marion</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>arithmetic</term><term>curry-howard</term><term>feasabilitity</term><term>proof-theory</term><term>ptime</term><term>quantification</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en" wicri:score="2690">This paper presents a methodology for reasoning about the computational complexity of functional programs. We introduce a first order arithmetic \StrictTa which is a syntactic restriction of Peano arithmetic. We establish that the set of functions which are provably total in \StrictTa, is exactly the set of polynomial time functions.The cut-elimination process is polynomial time computable. Compared to others feasible arithmetics, \StrictTa is conceptually simpler. The main feature of \StrictTa concerns the treatment of the quantification. The range of quantifiers is restricted to the set of {\em actual terms} which is the set of constructor terms with variables. The inductive formulas are restricted to conjunctions of atomic formulas.</div></front></TEI><BibTex type="inproceedings"><ref>marion01a</ref><crinnumber>A01-R-183</crinnumber><category>3</category><equipe>CALLIGRAMME</equipe><author><e>Marion, Jean-Yves</e></author><title>Actual arithmetic and feasibility</title><booktitle>{International Workshop on Computer Science Logic - CSL'2001, Paris, France}</booktitle><year>2001</year><editor>L. Fribourg</editor><volume>2142</volume><series>Lecture notes in Computer Science</series><pages>115--129</pages><month>Sep</month><publisher>Springer</publisher><keywords><e>proof-theory</e><e>feasabilitity</e><e>ptime</e><e>arithmetic</e><e>quantification</e><e>curry-howard</e></keywords><abstract>This paper presents a methodology for reasoning about the computational complexity of functional programs. We introduce a first order arithmetic \StrictTa which is a syntactic restriction of Peano arithmetic. We establish that the set of functions which are provably total in \StrictTa, is exactly the set of polynomial time functions.The cut-elimination process is polynomial time computable. Compared to others feasible arithmetics, \StrictTa is conceptually simpler. The main feature of \StrictTa concerns the treatment of the quantification. The range of quantifiers is restricted to the set of {\em actual terms} which is the set of constructor terms with variables. The inductive formulas are restricted to conjunctions of atomic formulas.</abstract></BibTex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Crin/Checkpoint
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001733 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Crin/Checkpoint/biblio.hfd -nk 001733 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Crin
|étape= Checkpoint
|type= RBID
|clé= CRIN:marion01a
|texte= Actual arithmetic and feasibility
}}
| This area was generated with Dilib version V0.6.33. |  |