Actual Arithmetic and Feasibility
Identifieur interne : 009912 ( Main/Merge ); précédent : 009911; suivant : 009913Actual Arithmetic and Feasibility
Auteurs : Jean-Yves Marion [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: This paper presents a methodology for reasoning about the computational complexity of functional programs. We introduce a first order arithmetic AT 0 which is a syntactic restriction of Peano arithmetic. We establish that the set of functions which are provably total in AT 0, is exactly the set of polynomial time functions. The cut-elimination process is polynomial time computable. Compared to others feasible arithmetics, AT 0 is conceptually simpler. The main feature of AT 0 concerns the treatment of the quantification. The range of quantifiers is restricted to the set of actual terms which is the set of constructor terms with variables. The inductive formulas are restricted to conjunctions of atomic formulas.
Url:
DOI: 10.1007/3-540-44802-0_9
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 001917
- to stream Istex, to step Curation: 001898
- to stream Istex, to step Checkpoint: 001F32
Links to Exploration step
ISTEX:6C062EB64BE7E4873CD468376BD8BBFF2CBD6BB4Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><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></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:6C062EB64BE7E4873CD468376BD8BBFF2CBD6BB4</idno><date when="2001" year="2001">2001</date><idno type="doi">10.1007/3-540-44802-0_9</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-6CC68BMF-F/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">001917</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001917</idno><idno type="wicri:Area/Istex/Curation">001898</idno><idno type="wicri:Area/Istex/Checkpoint">001F32</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001F32</idno><idno type="wicri:doubleKey">0302-9743:2001:Marion J:actual:arithmetic:and</idno><idno type="wicri:Area/Main/Merge">009912</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" 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><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>Loria, B.P. 239, 54506, Vandœuvre-lés-Nancy Cedex</wicri:regionArea><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><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: This paper presents a methodology for reasoning about the computational complexity of functional programs. We introduce a first order arithmetic AT 0 which is a syntactic restriction of Peano arithmetic. We establish that the set of functions which are provably total in AT 0, is exactly the set of polynomial time functions. The cut-elimination process is polynomial time computable. Compared to others feasible arithmetics, AT 0 is conceptually simpler. The main feature of AT 0 concerns the treatment of the quantification. The range of quantifiers is restricted to the set of actual terms which is the set of constructor terms with variables. The inductive formulas are restricted to conjunctions of atomic formulas.</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 009912 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 009912 | 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é= ISTEX:6C062EB64BE7E4873CD468376BD8BBFF2CBD6BB4
|texte= Actual Arithmetic and Feasibility
}}
| This area was generated with Dilib version V0.6.33. |  |