An implicit characterization of PSPACE

DOI10.1145/2159531.2159540MaRDI QIDQ2946666zbMATH OpenOpenAlexFDO

Authors Marco Gaboardi, Jean-Yves Marion, Simona Ronchi Della Rocca

Publication date 17 September 2015

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1006.0030

zbMATH Keywords

implicit computational complexitylinear logicpolynomial spaceoperational semanticstype assignment

Mathematics Subject Classification ID

Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Semantics in the theory of computing (68Q55)

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.

Recommendations

• A logical account of pspace
• A type system for PSPACE derived from light linear logic
• scientific article; zbMATH DE number 2006637
• Characterizing PSPACE with pointers
• Soft linear logic and polynomial complexity classes

Cited in

(11)

• scientific article; zbMATH DE number 5722524 (Why is no real title available?)
• Polynomial time in untyped elementary linear logic
• scientific article; zbMATH DE number 2006637 (Why is no real title available?)
• Computational Complexity Via Finite Types
• Characterizing PSPACE with pointers
• Implicit computation complexity in higher-order programming languages
• Reasonable space for the -calculus, logarithmically
• A type system for PSPACE derived from light linear logic
• IP = SPACE
• Reasonable space for the \(\lambda \)-calculus, logarithmically
• Unary resolution: characterizing \textsc{Ptime}

This page was built for publication: An implicit characterization of PSPACE

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2946666)