Complexity of Strongly Normalising λ-Terms via Non-idempotent Intersection Types
We present a typing system for the λ-calculus, with non-idempotent intersection types. As it is the case in (some) systems with idempotent intersections, a λ-term is typable if and only if it is strongly normalising. Non-idempotency brings some further information into typing trees, such as a bound on the longest β-reduction sequence reducing a term to its normal form.
We actually present these results in Klop’s extension of λ-calculus, where the bound that is read in the typing tree of a term is refined into an exact measure of the longest reduction sequence.
This complexity result is, for longest reduction sequences, the counterpart of de Carvalho’s result for linear head-reduction sequences.
- [BM03]Baillot, P., Mogbil, V.: Soft lambda-calculus: a language for polynomial time computation. CoRR, cs.LO/0312015 (2003)Google Scholar
- [CS07]Coquand, T., Spiwack, A.: A proof of strong normalisation using domain theory. Logic. Methods Comput. Science 3(4) (2007)Google Scholar
- [dC09]de Carvalho, D.: Execution time of lambda-terms via denotational semantics and intersection types. CoRR, abs/0905.4251 (2009)Google Scholar
- [How80]Howard, W.A.: The formulae-as-types notion of construction. In: Seldin, J.P., Hindley, J.R. (eds.) To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pp. 479–490. Academic Press, London (1980), Reprint of a manuscript written 1969Google Scholar
- [Klo80]Klop, J.-W.: Combinatory Reduction Systems, volume 127 of Mathematical Centre Tracts. CWI, PhD Thesis (1980)Google Scholar
- [KW99]Kfoury, A.J., Wells, J.B.: Principality and decidable type inference for finite-rank intersection types. In: Proc. of the 26th Annual ACM Symp. on Principles of Programming Languages (POPL 1999), pp. 161–174. ACM Press, New York (1999)Google Scholar
- [Len05]Lengrand, S.: Induction principles as the foundation of the theory of normalisation: Concepts and techniques. Technical report, PPS laboratory, Université Paris 7 (March 2005), http://hal.ccsd.cnrs.fr/ccsd-00004358
- [Len06]Lengrand, S.: Normalisation & Equivalence in Proof Theory & Type Theory. PhD thesis, Univ. Paris 7 & Univ. of St Andrews (2006)Google Scholar
- [NM04]Neergaard, P.M., Mairson, H.G.: Types, potency, and idempotency: why nonlinearity and amnesia make a type system work. In: Okasaki, C., Fisher, K. (eds.) Proc. of the ACM International Conference on Functional Programming, pp. 138–149. ACM Press, New York (September 2004)Google Scholar