An Implicit Characterization of PSPACE
Identifieur interne : 000D09 ( Hal/Corpus ); précédent : 000D08; suivant : 000D10An Implicit Characterization of PSPACE
Auteurs : Marco Gaboardi ; Jean-Yves Marion ; Simona Ronchi Della RoccaSource :
- ACM Transactions on Computational Logic [ 1529-3785 ] ; 2012.
English descriptors
- mix :
Abstract
We present a type system for an extension of lambda calculus with a conditional construction, named STAB, that characterizes the PSPACE class. This system is obtained by extending STA, a type assignment for lambda-calculus inspired by Lafont's Soft Linear Logic and characterizing the PTIME class. We extend STA by means of a ground type and terms for booleans and conditional. The key issue in the design of the type system is to manage the contexts in the rule for conditional in an additive way. Thanks to this rule, we are able to program polynomial time Alternating Turing Machines. From the well-known result APTIME = PSPACE, it follows that STAB is complete for PSPACE. Conversely, inspired by the simulation of Alternating Turing machines by means of Deterministic Turing machine, we introduce a call-by-name evaluation machine with two memory devices in order to evaluate programs in polynomial space. As far as we know, this is the first characterization of PSPACE that is based on lambda calculus and light logics.
Url:
DOI: 10.1145/2159531.2159540
Links to Exploration step
Hal:hal-00591868Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">An Implicit Characterization of PSPACE</title><author><name sortKey="Gaboardi, Marco" sort="Gaboardi, Marco" uniqKey="Gaboardi M" first="Marco" last="Gaboardi">Marco Gaboardi</name><affiliation><hal:affiliation type="researchteam" xml:id="struct-175461" status="VALID"><idno type="RNSR">201020947E</idno><orgName>Foundations of Component-based Ubiquitous Systems</orgName><orgName type="acronym">FOCUS</orgName><desc><address><addrLine>Dipartimento di Informatica - Scienza e Ingegneria (DISI)Universita' di BolognaMura Anteo Zamboni, 740126 BolognaITALY</addrLine><country key="IT"></country></address><ref type="url">http://www.inria.fr/equipes/focus</ref></desc><listRelation><relation active="#struct-34586" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-419351" type="direct"></relation><relation active="#struct-30978" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-34586" type="direct"><org type="laboratory" xml:id="struct-34586" status="VALID"><idno type="RNSR">198318250R</idno><orgName>Inria Sophia Antipolis - Méditerranée </orgName><orgName type="acronym">CRISAM</orgName><desc><address><addrLine>2004 route des Lucioles BP 93 06902 Sophia Antipolis</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/centre/sophia/</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-419351" type="direct"><org type="laboratory" xml:id="struct-419351" status="VALID"><orgName>Dipartimento di Informatica - Scienza e Ingegneria [Bologna]</orgName><orgName type="acronym">DISI</orgName><desc><address><addrLine>http://www.informatica.unibo.it/it</addrLine><country key="IT"></country></address><ref type="url">http://www.informatica.unibo.it/it</ref></desc><listRelation><relation active="#struct-30978" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-30978" type="indirect"><org type="institution" xml:id="struct-30978" status="VALID"><orgName>Università di Bologna [Bologna]</orgName><orgName type="acronym">UNIBO</orgName><desc><address><addrLine>Via Zamboni, 33 - 40126 Bologna</addrLine><country key="IT"></country></address><ref type="url">http://www.eng.unibo.it/PortaleEn/default.htm</ref></desc></org></tutelle></tutelles></hal:affiliation></affiliation></author><author><name sortKey="Marion, Jean Yves" sort="Marion, Jean Yves" uniqKey="Marion J" first="Jean-Yves" last="Marion">Jean-Yves Marion</name><affiliation><hal:affiliation type="researchteam" xml:id="struct-29797" status="VALID"><idno type="RNSR">200918992J</idno><orgName>Theoretical adverse computations, and safety</orgName><orgName type="acronym">CARTE</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/carte</ref></desc><listRelation><relation active="#struct-129671" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-423084" type="direct"></relation><relation active="#struct-206040" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-129671" type="direct"><org type="laboratory" xml:id="struct-129671" status="VALID"><idno type="RNSR">198618246Y</idno><orgName>INRIA Nancy - Grand Est</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/nancy</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-423084" type="direct"><org type="department" xml:id="struct-423084" status="VALID"><orgName>Department of Formal Methods </orgName><orgName type="acronym">LORIA - FM</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.loria.fr/la-recherche-en/departements/formal-methods</ref></desc><listRelation><relation active="#struct-206040" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation></org></tutelle><tutelle active="#struct-206040" type="indirect"><org type="laboratory" xml:id="struct-206040" status="VALID"><idno type="IdRef">067077927</idno><idno type="RNSR">198912571S</idno><idno type="IdUnivLorraine">[UL]RSI--</idno><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><date type="start">2012-01-01</date><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-413289" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-413289" type="indirect"><org type="institution" xml:id="struct-413289" status="VALID"><idno type="IdRef">157040569</idno><idno type="IdUnivLorraine">[UL]100--</idno><orgName>Université de Lorraine</orgName><orgName type="acronym">UL</orgName><date type="start">2012-01-01</date><desc><address><addrLine>34 cours Léopold - CS 25233 - 54052 Nancy cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-lorraine.fr/</ref></desc></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="IdRef">02636817X</idno><idno type="ISNI">0000000122597504</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation></affiliation></author><author><name sortKey="Ronchi Della Rocca, Simona" sort="Ronchi Della Rocca, Simona" uniqKey="Ronchi Della Rocca S" first="Simona" last="Ronchi Della Rocca">Simona Ronchi Della Rocca</name><affiliation><hal:affiliation type="laboratory" xml:id="struct-83587" status="VALID"><orgName>Dipartimento di Informatica [Torino]</orgName><desc><address><addrLine>Università di Torino</addrLine><country key="IT"></country></address><ref type="url">http://www.di.unito.it/</ref></desc><listRelation><relation active="#struct-47709" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-47709" type="direct"><org type="institution" xml:id="struct-47709" status="VALID"><orgName>Università degli studi di Torino</orgName><orgName type="acronym">UNITO</orgName><desc><address><addrLine>Via Verdi, 8 10124 Torino Italie</addrLine><country key="IT"></country></address><ref type="url">http://www.unito.it/</ref></desc></org></tutelle></tutelles></hal:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:hal-00591868</idno><idno type="halId">hal-00591868</idno><idno type="halUri">https://hal.archives-ouvertes.fr/hal-00591868</idno><idno type="url">https://hal.archives-ouvertes.fr/hal-00591868</idno><idno type="doi">10.1145/2159531.2159540</idno><date when="2012">2012</date><idno type="wicri:Area/Hal/Corpus">000D09</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">An Implicit Characterization of PSPACE</title><author><name sortKey="Gaboardi, Marco" sort="Gaboardi, Marco" uniqKey="Gaboardi M" first="Marco" last="Gaboardi">Marco Gaboardi</name><affiliation><hal:affiliation type="researchteam" xml:id="struct-175461" status="VALID"><idno type="RNSR">201020947E</idno><orgName>Foundations of Component-based Ubiquitous Systems</orgName><orgName type="acronym">FOCUS</orgName><desc><address><addrLine>Dipartimento di Informatica - Scienza e Ingegneria (DISI)Universita' di BolognaMura Anteo Zamboni, 740126 BolognaITALY</addrLine><country key="IT"></country></address><ref type="url">http://www.inria.fr/equipes/focus</ref></desc><listRelation><relation active="#struct-34586" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-419351" type="direct"></relation><relation active="#struct-30978" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-34586" type="direct"><org type="laboratory" xml:id="struct-34586" status="VALID"><idno type="RNSR">198318250R</idno><orgName>Inria Sophia Antipolis - Méditerranée </orgName><orgName type="acronym">CRISAM</orgName><desc><address><addrLine>2004 route des Lucioles BP 93 06902 Sophia Antipolis</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/centre/sophia/</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-419351" type="direct"><org type="laboratory" xml:id="struct-419351" status="VALID"><orgName>Dipartimento di Informatica - Scienza e Ingegneria [Bologna]</orgName><orgName type="acronym">DISI</orgName><desc><address><addrLine>http://www.informatica.unibo.it/it</addrLine><country key="IT"></country></address><ref type="url">http://www.informatica.unibo.it/it</ref></desc><listRelation><relation active="#struct-30978" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-30978" type="indirect"><org type="institution" xml:id="struct-30978" status="VALID"><orgName>Università di Bologna [Bologna]</orgName><orgName type="acronym">UNIBO</orgName><desc><address><addrLine>Via Zamboni, 33 - 40126 Bologna</addrLine><country key="IT"></country></address><ref type="url">http://www.eng.unibo.it/PortaleEn/default.htm</ref></desc></org></tutelle></tutelles></hal:affiliation></affiliation></author><author><name sortKey="Marion, Jean Yves" sort="Marion, Jean Yves" uniqKey="Marion J" first="Jean-Yves" last="Marion">Jean-Yves Marion</name><affiliation><hal:affiliation type="researchteam" xml:id="struct-29797" status="VALID"><idno type="RNSR">200918992J</idno><orgName>Theoretical adverse computations, and safety</orgName><orgName type="acronym">CARTE</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/carte</ref></desc><listRelation><relation active="#struct-129671" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-423084" type="direct"></relation><relation active="#struct-206040" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-129671" type="direct"><org type="laboratory" xml:id="struct-129671" status="VALID"><idno type="RNSR">198618246Y</idno><orgName>INRIA Nancy - Grand Est</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/nancy</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-423084" type="direct"><org type="department" xml:id="struct-423084" status="VALID"><orgName>Department of Formal Methods </orgName><orgName type="acronym">LORIA - FM</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.loria.fr/la-recherche-en/departements/formal-methods</ref></desc><listRelation><relation active="#struct-206040" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation></org></tutelle><tutelle active="#struct-206040" type="indirect"><org type="laboratory" xml:id="struct-206040" status="VALID"><idno type="IdRef">067077927</idno><idno type="RNSR">198912571S</idno><idno type="IdUnivLorraine">[UL]RSI--</idno><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><date type="start">2012-01-01</date><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-413289" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-413289" type="indirect"><org type="institution" xml:id="struct-413289" status="VALID"><idno type="IdRef">157040569</idno><idno type="IdUnivLorraine">[UL]100--</idno><orgName>Université de Lorraine</orgName><orgName type="acronym">UL</orgName><date type="start">2012-01-01</date><desc><address><addrLine>34 cours Léopold - CS 25233 - 54052 Nancy cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-lorraine.fr/</ref></desc></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="IdRef">02636817X</idno><idno type="ISNI">0000000122597504</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation></affiliation></author><author><name sortKey="Ronchi Della Rocca, Simona" sort="Ronchi Della Rocca, Simona" uniqKey="Ronchi Della Rocca S" first="Simona" last="Ronchi Della Rocca">Simona Ronchi Della Rocca</name><affiliation><hal:affiliation type="laboratory" xml:id="struct-83587" status="VALID"><orgName>Dipartimento di Informatica [Torino]</orgName><desc><address><addrLine>Università di Torino</addrLine><country key="IT"></country></address><ref type="url">http://www.di.unito.it/</ref></desc><listRelation><relation active="#struct-47709" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-47709" type="direct"><org type="institution" xml:id="struct-47709" status="VALID"><orgName>Università degli studi di Torino</orgName><orgName type="acronym">UNITO</orgName><desc><address><addrLine>Via Verdi, 8 10124 Torino Italie</addrLine><country key="IT"></country></address><ref type="url">http://www.unito.it/</ref></desc></org></tutelle></tutelles></hal:affiliation></affiliation></author></analytic><idno type="DOI">10.1145/2159531.2159540</idno><series><title level="j">ACM Transactions on Computational Logic</title><idno type="ISSN">1529-3785</idno><imprint><date type="datePub">2012</date></imprint></series></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="mix" xml:lang="en"><term>implicit computational complexity</term><term>linear logic</term><term>operational semantics</term><term>polynomial space</term><term>type assignment</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">We present a type system for an extension of lambda calculus with a conditional construction, named STAB, that characterizes the PSPACE class. This system is obtained by extending STA, a type assignment for lambda-calculus inspired by Lafont's Soft Linear Logic and characterizing the PTIME class. We extend STA by means of a ground type and terms for booleans and conditional. The key issue in the design of the type system is to manage the contexts in the rule for conditional in an additive way. Thanks to this rule, we are able to program polynomial time Alternating Turing Machines. From the well-known result APTIME = PSPACE, it follows that STAB is complete for PSPACE. Conversely, inspired by the simulation of Alternating Turing machines by means of Deterministic Turing machine, we introduce a call-by-name evaluation machine with two memory devices in order to evaluate programs in polynomial space. As far as we know, this is the first characterization of PSPACE that is based on lambda calculus and light logics.</div></front></TEI><hal api="V3"><titleStmt><title xml:lang="en">An Implicit Characterization of PSPACE</title><author role="aut"><persName><forename type="first">Marco</forename><surname>Gaboardi</surname></persName><email>gaboardi@di.unito.it</email><idno type="halauthor">956204</idno><affiliation ref="#struct-175461"></affiliation><affiliation ref="#struct-50194"></affiliation></author><author role="aut"><persName><forename type="first">Jean-Yves</forename><surname>Marion</surname></persName><email>Jean-Yves.Marion@loria.fr</email><idno type="halauthor">81159</idno><affiliation ref="#struct-29797"></affiliation></author><author role="aut"><persName><forename type="first">Simona</forename><surname>Ronchi Della Rocca</surname></persName><email>ronchi@di.unito.it</email><idno type="halauthor">370234</idno><affiliation ref="#struct-83587"></affiliation></author><editor role="depositor"><persName><forename>Jean-Yves</forename><surname>Marion</surname></persName><email>JEAN-YVES.MARION@LORIA.FR</email></editor></titleStmt><editionStmt><edition n="v1" type="current"><date type="whenSubmitted">2011-05-10 13:52:19</date><date type="whenModified">2015-09-22 01:12:56</date><date type="whenReleased">2011-05-10 14:18:59</date><date type="whenProduced">2012</date><date type="whenEndEmbargoed">2011-05-10</date><ref type="file" target="https://hal.archives-ouvertes.fr/hal-00591868/document"><date notBefore="2011-05-10"></date></ref><ref type="file" subtype="author" n="1" target="https://hal.archives-ouvertes.fr/hal-00591868/file/main.pdf"><date notBefore="2011-05-10"></date></ref></edition><respStmt><resp>contributor</resp><name key="113627"><persName><forename>Jean-Yves</forename><surname>Marion</surname></persName><email>JEAN-YVES.MARION@LORIA.FR</email></name></respStmt></editionStmt><publicationStmt><distributor>CCSD</distributor><idno type="halId">hal-00591868</idno><idno type="halUri">https://hal.archives-ouvertes.fr/hal-00591868</idno><idno type="halBibtex">gaboardi:hal-00591868</idno><idno type="halRefHtml">ACM Transactions on Computational Logic, Association for Computing Machinery, 2012, 13 (2), pp.Article 18. <10.1145/2159531.2159540></idno><idno type="halRef">ACM Transactions on Computational Logic, Association for Computing Machinery, 2012, 13 (2), pp.Article 18. <10.1145/2159531.2159540></idno></publicationStmt><seriesStmt><idno type="stamp" n="CNRS">CNRS - Centre national de la recherche scientifique</idno><idno type="stamp" n="INRIA">INRIA - Institut National de Recherche en Informatique et en Automatique</idno><idno type="stamp" n="LORIA2">Publications du LORIA</idno><idno type="stamp" n="INRIA-NANCY-GRAND-EST">INRIA Nancy - Grand Est</idno><idno type="stamp" n="LORIA">LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications</idno><idno type="stamp" n="LORIA-FM" p="LORIA">Méthodes formelles</idno><idno type="stamp" n="INRIA-LORRAINE">INRIA Nancy - Grand Est</idno><idno type="stamp" n="INRIA-SOPHIA">INRIA Sophia Antipolis - Méditerranée</idno><idno type="stamp" n="INRIASO">INRIA-SOPHIA</idno><idno type="stamp" n="UNIV-LORRAINE">Université de Lorraine</idno><idno type="stamp" n="INRIA_TEST">INRIA - Institut National de Recherche en Informatique et en Automatique</idno></seriesStmt><notesStmt><note type="audience" n="2">International</note><note type="popular" n="0">No</note><note type="peer" n="1">Yes</note></notesStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">An Implicit Characterization of PSPACE</title><author role="aut"><persName><forename type="first">Marco</forename><surname>Gaboardi</surname></persName><email>gaboardi@di.unito.it</email><idno type="halAuthorId">956204</idno><affiliation ref="#struct-175461"></affiliation><affiliation ref="#struct-50194"></affiliation></author><author role="aut"><persName><forename type="first">Jean-Yves</forename><surname>Marion</surname></persName><email>Jean-Yves.Marion@loria.fr</email><idno type="halAuthorId">81159</idno><affiliation ref="#struct-29797"></affiliation></author><author role="aut"><persName><forename type="first">Simona</forename><surname>Ronchi Della Rocca</surname></persName><email>ronchi@di.unito.it</email><idno type="halAuthorId">370234</idno><affiliation ref="#struct-83587"></affiliation></author></analytic><monogr><idno type="halJournalId" status="VALID">9525</idno><idno type="issn">1529-3785</idno><title level="j">ACM Transactions on Computational Logic</title><imprint><publisher>Association for Computing Machinery</publisher><biblScope unit="volume">13</biblScope><biblScope unit="issue">2</biblScope><biblScope unit="pp">Article 18</biblScope><date type="datePub">2012</date></imprint></monogr><idno type="doi">10.1145/2159531.2159540</idno></biblStruct></sourceDesc><profileDesc><langUsage><language ident="en">English</language></langUsage><textClass><keywords scheme="author"><term xml:lang="en">implicit computational complexity</term><term xml:lang="en">polynomial space</term><term xml:lang="en">linear logic</term><term xml:lang="en">type assignment</term><term xml:lang="en">operational semantics</term></keywords><classCode scheme="halDomain" n="info.info-lo">Computer Science [cs]/Logic in Computer Science [cs.LO]</classCode><classCode scheme="halTypology" n="ART">Journal articles</classCode></textClass><abstract xml:lang="en">We present a type system for an extension of lambda calculus with a conditional construction, named STAB, that characterizes the PSPACE class. This system is obtained by extending STA, a type assignment for lambda-calculus inspired by Lafont's Soft Linear Logic and characterizing the PTIME class. We extend STA by means of a ground type and terms for booleans and conditional. The key issue in the design of the type system is to manage the contexts in the rule for conditional in an additive way. Thanks to this rule, we are able to program polynomial time Alternating Turing Machines. From the well-known result APTIME = PSPACE, it follows that STAB is complete for PSPACE. Conversely, inspired by the simulation of Alternating Turing machines by means of Deterministic Turing machine, we introduce a call-by-name evaluation machine with two memory devices in order to evaluate programs in polynomial space. As far as we know, this is the first characterization of PSPACE that is based on lambda calculus and light logics.</abstract></profileDesc></hal></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Hal/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000D09 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Hal/Corpus/biblio.hfd -nk 000D09 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Hal
|étape= Corpus
|type= RBID
|clé= Hal:hal-00591868
|texte= An Implicit Characterization of PSPACE
}}
| This area was generated with Dilib version V0.6.33. |  |