Skip to main content
SpringerLink
Log in

Light affine lambda calculus and polynomial time strong normalization

  • Published:
Archive for Mathematical Logic Aims and scope Submit manuscript

Abstract

Light Linear Logic (LLL) and Intuitionistic Light Affine Logic (ILAL) are logics that capture polynomial time computation. It is known that every polynomial time function can be represented by a proof of these logics via the proofs-as-programs correspondence. Furthermore, there is a reduction strategy which normalizes a given proof in polynomial time. Given the latter polynomial time “weak” normalization theorem, it is natural to ask whether a “strong” form of polynomial time normalization theorem holds or not. In this paper, we introduce an untyped term calculus, called Light Affine Lambda Calculus (λLA), which corresponds to ILAL. λLA is a bi-modal λ-calculus with certain constraints, endowed with very simple reduction rules. The main property of LALC is the polynomial time strong normalization: any reduction strategy normalizes a given λLA term in a polynomial number of reduction steps, and indeed in polynomial time. Since proofs of ILAL are structurally representable by terms of λLA, we conclude that the same holds for ILAL.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Asperti, A.: Light affine logic. In: Proceedings of LICS’98, 300–308 (1998)

  2. Asperti A. and Roversi L. (2002). Intuitionistic light affine logic (proof-nets, normalization complexity, expressive power, programming notation). ACM Trans. Comput. Logic 3(1): 137–175

    Article  MathSciNet  Google Scholar 

  3. Baillot, P.: Stratified coherence spaces: a denotational semantics for light linear logic. Theor. Comput. Sci. 318(1–2), 29–55 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  4. Baillot, P., Terui, K.: Light types for polynomial time computation in lambda-calculus. In:Proceedings of LICS’04, 266–275 (2004)

  5. Barendregt, H.P.:Lambda calculi with types. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.), Handbook of Logic in Computer Science, vol. 2, pp. 117–309. Oxford University Press (1992)

  6. Bellantoni S. and Cook S. (1992). New recursion-theoretic characterization of the polytime functions. Comput. Complex. 2: 97–110

    Article  MATH  MathSciNet  Google Scholar 

  7. Bellantoni S., Niggl K.-H. and Schwichtenberg H. (2000). Ramification, modality and linearity in higher type recursion. Ann. Pure Appl. Logic 104: 17–30

    Article  MATH  MathSciNet  Google Scholar 

  8. Danos V. and Joinet J.-B. (2003). Linear logic & elementary time. Inf. Comput. 183(1): 123–137

    Article  MATH  MathSciNet  Google Scholar 

  9. Girard J.-Y. (1998). Light linear logic. Inf. Comput. 14(3): 175–204

    Article  MathSciNet  Google Scholar 

  10. Girard J.-Y., Scedrov A. and Scott P.J. (1992). Bounded linear logic: a modular approach to polynomial time computability. Theor. Comput. Sci. 97: 1–66

    Article  MATH  MathSciNet  Google Scholar 

  11. Hofmann M. (2000). Safe recursion with higher types and BCK algebra. Ann. Pure App. Logic 104: 113–166

    Article  MATH  Google Scholar 

  12. Kanovich M., Okada M. and Scedrov A. (2003). Phase semantics for light linear logic. Theor. Comput. Sci. 294(3): 525–549

    Article  MATH  MathSciNet  Google Scholar 

  13. Leivant D. (1994). A foundational delineation of poly-time. Inf. Comput. 110(2): 390–420

    Article  MathSciNet  Google Scholar 

  14. Leivant, D., Marion, J.-Y.: Ramified recurrence and computational complexity I: Word recurrence and poly-time. In: Clote, P., Remmel, J. (eds.), Feasible Mathematics II, pp. 320–343. Birkhauser (1994)

  15. Mairson, H., Terui, K.: On the computational complexity of cut-elimination in linear logic. In: Proceedings of ICTCS 2003, pp. 23–36. LNCS, vol.2841 (2003)

  16. Murawski, A.S., Ong, C.-H.L.: Discreet games, light affine logic and ptime computation. In:Proceedings of CSL 2000, pp. 427–441, Springer, Heidelberg LNCS, vol.1862 (2000)

  17. Murawski A.S. and Ong C.-H.L. (2004). On an interpretation of safe recursion in light affine logic. Theor. Comput. Sci. 318: 197–223

    Article  MATH  MathSciNet  Google Scholar 

  18. Neergaard, P., Mairson, H.: LAL is square: representation and expressiveness in light affine logic. In: presented at the Fourth International Workshop on Implicit Computational Complexity (2002)

  19. Roversi, L.A.: P-time completeness proof for light logics. In: Proceedings of CSL’99, pp. 469–483 Springer, LNCS , vol.1683 (1999)

  20. Roversi L. (2000). Light affine logic as a programming language: a first contribution. Int. J. Found. Comput. Sci. 11(1): 113–152

    Article  MathSciNet  Google Scholar 

  21. Terui, K.:Light affine lambda calculus and polytime strong normalization. In: Proceedings of LICS2001, pp. 209–220 (2001)

  22. Terui, K.: Light Logic and Polynomial Time Computation. PhD thesis, Keio University, March 2002. Available at http://research.nii.ac.jp/∼terui

  23. Terui K. (2004). Light affine set theory: a naive set theory of polynomial time. Studia Logica 77: 9–40

    Article  MATH  MathSciNet  Google Scholar 

  24. Wells J.B. (1999). Typability and type checking in system F are equivalent and undecidable. Ann. Pure Appl. Logic 98: 111–156

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. National Institute of Informatics, 2-1-2 Hitotsubashi, Chiyoda-ku, 101-8430, Tokyo, Japan

    Kazushige Terui

Authors
  1. Kazushige Terui
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Kazushige Terui.

Additional information

This is a full version of the paper [21] presented at LICS 2001.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Terui, K. Light affine lambda calculus and polynomial time strong normalization. Arch. Math. Logic 46, 253–280 (2007). https://doi.org/10.1007/s00153-007-0042-6

Download citation

  • Received:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00153-007-0042-6

Keywords

Search

Navigation