The geometry of linear higher-order recursion

ABSTRACT

Imposing linearity and ramification constraints allows to weaken higher-order (primitive) recursion in such a way that the class of representable functions equals the class of polynomial-time computable functions, as the works by Leivant, Hofmann, and others show. This article shows that fine-tuning these two constraints leads to different expressive strengths, some of them lying well beyond polynomial time. This is done by introducing a new semantics, called algebraic context semantics. The framework stems from Gonthier's original work (itself a model of Girard's geometry of interaction) and turns out to be a versatile and powerful tool for the quantitative analysis of normalization in the lambda calculus with constants and higher-order recursion.

REFERENCES

• 1: Klaus Aehlig , Jan Johannsen , Helmut Schwichtenberg , Sebastiaan Terwijn, Linear Ramified Higher Type Recursion and Parallel Complexity, Proceedings of the International Seminar on Proof Theory in Computer Science, p.1-21, October 07-12, 2001
• 2: Patrick Baillot , Marco Pedicini, Elementary Complexity and Geometry of Interaction, Fundamenta Informaticae, v.45 n.1-2, p.1-31, January 2001
• 3: Stephen Bellantoni , Stephen Cook, A new recursion-theoretic characterization of the polytime functions, Computational Complexity, v.2 n.2, p.97-110, 1992 [doi>10.1007/BF01201998]
• 4: Bellantoni, S., Niggl, K. H., and Schwichtenberg, H. 2000. Higher type recursion, ramification and polynomial time. Ann. Pure App. Logic 104, 17--30.
• 5: Bonfante, G., Marion, J.-Y., and Moyen, J.-Y. 2004. On complexity analysis by quasi-interpretations. Theor. Comput. Sci. To appear.
• 6: Ugo Dal Lago, Context Semantics, Linear Logic and Computational Complexity, Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science, p.169-178, August 12-15, 2006 [doi>10.1109/LICS.2006.21]
• 7: Dal Lago, U. and Martini, S. 2006. An invariant cost model for the lambda calculus. In Proceedings of the. 2nd Conference on Computability in Europe. Lecture Notes in Computer Science, vol. 3988. 105--114.
• 8: Dal Lago, U., Martini, S., and Roversi, L. 2003. Higher order linear ramified recurrence. In Types for Proofs and Programs, Post-Workshop Proceedings. Lecture Notes in Computer Science, vol. 3085. 178--193.
• 9: V. Danos , H. Herbelin , L. Regnier, Game semantics and abstract machines, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p.394, July 27-30, 1996
• 10: Vincent Danos , Laurent Reginer, Reversible, irreversible and optimal &lgr;-machines, Theoretical Computer Science, v.227 n.1-2, p.79-97, Oct. 1, 1999 [doi>10.1016/S0304-3975(99)00049-3]
• 11: Dan R. Ghica, Slot games: a quantitative model of computation, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.85-97, January 12-14, 2005, Long Beach, California, USA
• 12: Jean-Yves Girard, Geometry of interaction 2: deadlock-free algorithms, Proceedings of the International Conference on Computer Logic, p.76-93, December 01, 1988
• 13: Girard, J.-Y. 1989. Geometry of interaction 1: Interpretation of system F. In Proceedings of the Logic Colloquium 88, 221--260.
• 14: 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]
• 15: Georges Gonthier , Martín Abadi , Jean-Jacques Lévy, The geometry of optimal lambda reduction, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.15-26, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143172]
• 16: Martin Hofmann, Linear Types and Non Size-Increasing Polynomial Time Computation, Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, p.464, July 02-05, 1999
• 17: Hofmann, M. 2000. Safe recursion with higher types and BCK-algebra. Ann. Pure Appl. Logic 104, 113--166.
• 18: Joachimski, F. and Matthes, R. 2003. Short proofs of normalization for the simply-typed lambda-calculus, permutative conversions and Gödel's T. Archive Math. Logic 42, 1, 59--87.
• 19: 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]
• 20: Daniel Leivant, Stratified functional programs and computational complexity, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.325-333, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158659]
• 21: Daniel Leivant, Applicative Control and Computational Complexity, Proceedings of the 13th International Workshop and 8th Annual Conference of the EACSL on Computer Science Logic, p.82-95, September 20-25, 1999
• 22: Leivant, D. 1999b. Ramified recurrence and computational complexity III: Higher type recurrence and elementary complexity. Ann. Pure Appl. Logic 96, 209--229.
• 23: Leivant, D. 2002. Intrinsic reasoning about functional programs I: First order theories. Ann. Pure Appl. Logic 114, 1-3, 117--153.
• 24: Daniel Leivant, Intrinsic reasoning about functional programs II: unipolar induction and primitive-recursion, Theoretical Computer Science, v.318 n.1-2, p.181-196, June 2004 [doi>10.1016/j.tcs.2003.11.002]
• 25: 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
• 26: Harry G. Mairson, From Hilbert Spaces to Dilbert Spaces: Context Semantics Made Simple, Proceedings of the 22nd Conference Kanpur on Foundations of Software Technology and Theoretical Computer Science, p.2-17, December 12-14, 2002
• 27: Ostrin, G. and Wainer, S. 2002. Proof theoretic complexity. In Proof and System Reliability, H. Schwichtenberg and R. Steinbrüggen, Eds. NATO Science Series, vol. 62. Kluwer, 369--398.
• 28: David Sands, Operational Theories of Improvement in Functional Languages (Extended Abstract), Proceedings of the 1991 Glasgow Workshop on Functional Programming, p.298-311, August 12-14, 1991
• 29: Simmons, H. 2005. Tiering as a recursion technique. Bull. Symbol. Logic 11, 3, 321--350.

INDEX TERMS

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

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.3 Complexity Measures and Classes
          Subjects: Machine-independent complexity**

General Terms:
Languages, Performance, Theory

Keywords:
Geometry of interaction, higher-order recursion, implicit computational complexity, lambda calculus, type systems