A confluent reduction for the extensional typed \(\lambda\)-calculus with pairs, sums, recursion and terminal object. (English) Zbl 1422.03022

Lingas, Andrzej (ed.) et al., Automata, languages and programming. 20th international colloquium, ICALP 93, Lund, Sweden, July 5–9, 1993. Proceedings. Berlin: Springer-Verlag. Lect. Notes Comput. Sci. 700, 645-656 (1993).
Summary: We add extensional equalities for the functional and product types to the typed \(\lambda\)-calculus with not only products and terminal object, but also sums and bounded recursion (a version of recursion that does not allow recursive calls of infinite length). We provide a confluent and strongly normalizing (thus decidable) rewriting system for the calculus, that stays confluent when allowing unbounded recursion. For that, we turn the extensional equalities into expansion rules, and not into contractions as is done traditionally. We first prove the calculus to be weakly confluent, which is a more complex and interesting task than for the usual \(\lambda\)-calculus. Then we provide an effective mechanism to simulate expansions without expansion rules, so that the strong normalization of the calculus can be derived from that of the underlying, traditional, non extensional system. These results give us the confluence of the full calculus, but we also show how to deduce confluence without the weak confluence property, using only our technique of simulating expansions.
For the entire collection see [Zbl 0814.00020].


03B40 Combinatory logic and lambda calculus
Full Text: DOI


[1] Y. Akama. On mints’ reductions for ccc-calculus. \(TLCA\). LNCS 664, Springer Verlag, 1993. · Zbl 0786.03006
[2] H. Barendregt. \(The Lambda Calculus; Its syntax and Semantics\). North Holland, 1984. · Zbl 0551.03007
[3] P.L. Curien and R. Di Cosmo. A confluent reduction system for the λ-calculus with surjective pairing and terminal object. \(ICALP 91\), LNCS 510, pages 291-302. · Zbl 0769.68056
[4] H.B. Curry and R. Feys. \(Combinatory Logic\), volume 1. North Holland, 1958. · Zbl 0081.24104
[5] D. Cubric. On free ccc. Distributed on the types mailing list, 1992.
[6] R. Di Cosmo and D. Kesner. Simulating expansions without expansions. Technical report, INRIA, 1993. · Zbl 0831.03004
[7] D. Dougherty. Some reduction properties of a lambda calculus with coproducts and recursive types. Technical report, Wesleyan University, 1990. E-mail: ddougherty@eagle.wesleyan.edu.
[8] J.Y. Girard. \(Interprétation fonctionelle et élimination des coupures dans l'arithmétique d'ordre supérieure\). Thèse de doctorat d’état, Université de Paris VII, 1972.
[9] J.Y. Girard, Y. Lafont, and P. Taylor. \(Proofs and Types\). Cambridge University Press, 1990. · Zbl 0671.68002
[10] G. Huet. Résolution d’équations dans les langages d’ordre 1,2,..., \(Ω\). Thèse de doctorat d’état, Université de Paris VII, 1976.
[11] C. Barry Jay. Long \(Βη\) normal forms and confluence (revised). Technical Report ECS-LFCS-91-183, LFCS, 1992. University of Edimburgh.
[12] C. Barry Jay and N. Ghani. The virtues of eta-expansion. Technical Report ECS-LFCS-92-243, LFCS, 1992. University of Edimburgh. · Zbl 0833.68072
[13] J.W. Klop. Combinatory reduction systems. \(Mathematical Center Tracts\), 27, 1980. · Zbl 0466.03006
[14] J.J. Lévy. An algebraic interpretation of the \(λΒκ\)-calculus and a labelled \(λ\)-calculus. \(TCS\), 2:97-114, 1976. · Zbl 0335.02016
[15] J. Lambek and P.J. Scott. \(An introduction to higher order categorical logic\). CUP, 1986. · Zbl 0596.03002
[16] G. Mints. Closed categories and the theory of proofs. \(Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im. V.A. Steklova AN SSSR\), 68:83-114, 1977.
[17] G. Mints. Teorija categorii i teoria dokazatelstv.I. \(Aktualnye problemy logiki i metodologii nauky\), pages 252-278, 1979.
[18] G. Pottinger. The Church Rosser Theorem for the Typed lambda-calculus with Surjective Pairing. \(Notre Dame Journal of Formal Logic\), 22(3):264-268, 1981. · Zbl 0476.03026
[19] D. Prawitz. Ideas and results in proof theory. \(Proc. 2nd Scand. Logic Symp.\), pages 235-307, 1971. · Zbl 0226.02031
[20] A. Poigné and J. Voss. On the implementation of abstract data types by programming language constructs. \(JCSS\), 34(2-3):340-376, April/June 1987. · Zbl 0619.68025
[21] A.S. Troelstra. Strong normalization for typed terms with surjective pairing. · Zbl 0624.03043
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.