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.
Similar content being viewed by others
References
Asperti, A.: Light affine logic. In: Proceedings of LICS’98, 300–308 (1998)
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
Baillot, P.: Stratified coherence spaces: a denotational semantics for light linear logic. Theor. Comput. Sci. 318(1–2), 29–55 (2004)
Baillot, P., Terui, K.: Light types for polynomial time computation in lambda-calculus. In:Proceedings of LICS’04, 266–275 (2004)
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)
Bellantoni S. and Cook S. (1992). New recursion-theoretic characterization of the polytime functions. Comput. Complex. 2: 97–110
Bellantoni S., Niggl K.-H. and Schwichtenberg H. (2000). Ramification, modality and linearity in higher type recursion. Ann. Pure Appl. Logic 104: 17–30
Danos V. and Joinet J.-B. (2003). Linear logic & elementary time. Inf. Comput. 183(1): 123–137
Girard J.-Y. (1998). Light linear logic. Inf. Comput. 14(3): 175–204
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
Hofmann M. (2000). Safe recursion with higher types and BCK algebra. Ann. Pure App. Logic 104: 113–166
Kanovich M., Okada M. and Scedrov A. (2003). Phase semantics for light linear logic. Theor. Comput. Sci. 294(3): 525–549
Leivant D. (1994). A foundational delineation of poly-time. Inf. Comput. 110(2): 390–420
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)
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)
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)
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
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)
Roversi, L.A.: P-time completeness proof for light logics. In: Proceedings of CSL’99, pp. 469–483 Springer, LNCS , vol.1683 (1999)
Roversi L. (2000). Light affine logic as a programming language: a first contribution. Int. J. Found. Comput. Sci. 11(1): 113–152
Terui, K.:Light affine lambda calculus and polytime strong normalization. In: Proceedings of LICS2001, pp. 209–220 (2001)
Terui, K.: Light Logic and Polynomial Time Computation. PhD thesis, Keio University, March 2002. Available at http://research.nii.ac.jp/∼terui
Terui K. (2004). Light affine set theory: a naive set theory of polynomial time. Studia Logica 77: 9–40
Wells J.B. (1999). Typability and type checking in system F are equivalent and undecidable. Ann. Pure Appl. Logic 98: 111–156
Author information
Authors and Affiliations
Corresponding author
Additional information
This is a full version of the paper [21] presented at LICS 2001.
Rights 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
Received:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00153-007-0042-6