A logical account of pspace

ABSTRACT

We propose a characterization of PSPACE by means of atype assignment for an extension of lambda calculus with a conditional construction. The type assignment STA_B is an extension of STA, a type assignment for lambda-calculus inspired by Lafont's Soft Linear Logic.

We extend STA by means of a ground type and terms for booleans. The key point is that the elimination rule for booleans is managed in an additive way. Thus, we are able to program polynomial time Alternating Turing Machines. Conversely, we introduce a call-by-name evaluation machine in order tocompute programs in polynomial space. As far as we know, this is the first characterization of PSPACE which is based on lambda calculusand light logics.

REFERENCES

• 1: S. Abiteboul , V. Vianu, Fixpoint extensions of first-order logic and datalog-like languages, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.71-79, June 1989, Pacific Grove, California, United States
• 2: Andrea Asperti , Luca Roversi, Intuitionistic Light Affine Logic, ACM Transactions on Computational Logic (TOCL), v.3 n.1, p.137-175, January 2002 [doi>10.1145/504077.504081]
• 3: Patrick Baillot , Kazushige Terui, Light Types for Polynomial Time Computation in Lambda-Calculus, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, p.266-275, July 13-17, 2004 [doi>10.1109/LICS.2004.22]
• 4: Henk Barendregt. The Lambda Calculus: Its Syntax and Semantics. Elsevier/North-Holland, Amsterdam, London, New York, revised edition, 1984.
• 5: Ashok K. Chandra , Dexter C. Kozen , Larry J. Stockmeyer, Alternation, Journal of the ACM (JACM), v.28 n.1, p.114-133, Jan. 1981 [doi>10.1145/322234.322243]
• 6: Paolo Coppola, Ugo Dal Lago, and Simona Ronchi Della Rocca. Elementary affine logic and the call by value lambda calculus. In Proceedings of the Typed Lambda Calculi and Applications, 7th International Conference -- TLCA '05, Nara, Japan, April 21-23, 2005, volume 3461 of Lecture Notes in Computer Science, pages 131--145. Springer, 2005.
• 7: Marco Gaboardi and Simona Ronchi Della Rocca. A soft type assignment system for λ-calculus. In Proceedings of the Computer Science Logic, 21st International Workshop -- CSL'07, Lausanne, Switzerland, September 11-15, 2007, volume 4646 of Lecture Notes in Computer Science, pages 253--267. Springer, 2007.
• 8: Jean-Yves Girard, Light linear logic, Information and Computation, v.143 n.2, p.175-204, June 15, 1998 [doi>10.1006/inco.1998.2700]
• 9: Andreas Goerdt, Characterizing complexity classes by higher type primitive recursive definitions, Theoretical Computer Science, v.100 n.1, p.45-66, June 22, 1992 [doi>10.1016/0304-3975(92)90363-K]
• 10: Erich Grädel, Phokion G. Kolaitis, Leonid Libkin, Maarten Marx, Joel Spencer, Moshe Y. Vardi, Yde Venema, and Scott Weinstein. Finite Model Theory and its applications. Springer, 2007.
• 11: Neil D. Jones, The expressive power of higher-order types or, life without CONS, Journal of Functional Programming, v.11 n.1, p.55-94, January 2001 [doi>10.1017/S0956796800003889]
• 12: Jean-Louis Krivine, A call-by-name lambda-calculus machine, Higher-Order and Symbolic Computation, v.20 n.3, p.199-207, September 2007 [doi>10.1007/s10990-007-9018-9]
• 13: Yves Lafont, Soft linear logic and polynomial time, Theoretical Computer Science, v.318 n.1-2, p.163-180, June 2004 [doi>10.1016/j.tcs.2003.10.018]
• 14: Daniel Leivant , Jean-Yves Marion, Lambda calculus characterizations of poly-time, Proceedings of the International Conference on Typed Lambda Calculi and Applications, p.274-288, March 16-18, 1993
• 15: Daniel Leivant , Jean-Yves Marion, Ramified Recurrence and Computational Complexity II: Substitution and Poly-Space, Selected Papers from the 8th International Workshop on Computer Science Logic, p.486-500, September 25-30, 1994
• 16: Daniel Leivant , Jean-Yves Marion, Predicative Functional Recurrence and Poly-space, Proceedings of the 7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.369-380, April 14-18, 1997
• 17: François Maurel. Nondeterministic light logics and NP-time. In Martin Hofmann, editor, Proceedings of the Typed Lambda Calculi and Applications, 6th International Conference -- TLCA 2003, Valencia, Spain, June 10-12, 2003, volume 2701 of Lecture Notes in Computer Science, pages 241--255. Springer, 2003.
• 18: Virgile Mogbil and Vincent Rahli. Uniform circuits, & boolean proof nets. In Sergei N. Artemov and Anil Nerode, editors, Proceedings of the Symposium on Logical Foundations of Computer Science -- LFCS'07, volume 4514 of Lecture Notes in Computer Science, pages 401--421. Springer, June 2007.
• 19: Isabel Oitavem, Implicit Characterizations of Pspace, Proceedings of the International Seminar on Proof Theory in Computer Science, p.170-190, October 07-12, 2001
• 20: Simona Ronchi Della Rocca and Luca Roversi. Lambda calculus and intuitionistic linear logic. Studia Logica, 59(3), 1997.
• 21: Walter J. Savitch. Relationship between nondeterministic and deterministic tape classes. Journal of Computer and System Sciences, 4:177--192, 1970.
• 22: Ulrich Schopp, Stratified Bounded Affine Logic for Logarithmic Space, Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science, p.411-420, July 10-14, 2007 [doi>10.1109/LICS.2007.45]
• 23: Kazushige Terui. Linear logical characterization of polyspace functions (extended abstract), 2000. URL http://citeseer.ist.psu.edu/294754.html. Unpublished.
• 24: Kazushige Terui, Proof Nets and Boolean Circuits, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, p.182-191, July 13-17, 2004 [doi>10.1109/LICS.2004.34]
• 25: Moshe Y. Vardi, The complexity of relational query languages (Extended Abstract), Proceedings of the fourteenth annual ACM symposium on Theory of computing, p.137-146, May 05-07, 1982, San Francisco, California, United States [doi>10.1145/800070.802186]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Proof theory; Lambda calculus and related systems

General Terms:
Design, Languages, Theory

Keywords:
implicit computational complexity, linear logic, polynomial space, type assignment