Confluence results for the pure strong categorical logic CCL. \(\lambda\)- calculi as subsystems of CCL. (English) Zbl 0707.03012

Author’s summary: “The Strong Categorical Combinatory Logic (CCL, CCL\(\beta\eta\) SP), developed by Curien (1986) is, when typed and augmented with a rule defining a terminal object, a presentation of Cartesian Closed Categories. Furthermore, it is equationally equivalent to the Lambda-calculus with explicit couples and Surjective Pairing. Here we study the confluence properties of (CCL, CCL\(\beta\eta\) SP) and of several of its subsystems, and the relationship between untyped Lambda- calculi and (CCL, CCL\(\beta\eta\) SP) as rewriting systems. We prove that there exists a subset \({\mathcal D}\) of CCL, and a subsystem SL\(\beta\) of CCL\(\beta\eta\) SP confluent on \({\mathcal D}\), a very simple isomorphism between \(\Lambda\), the classical Lambda-calculus, and a subset \({\mathcal S}{\mathcal D}_{\lambda}\) of \({\mathcal D}\), which is extended between \(\beta\)- derivations of \(\Lambda\) and a class of derivations of SL\(\beta\). Substitution, which is a one-step operation belonging to the metalanguage of \(\Lambda\), is now described by rewritings with SL\(\beta\) and calculations between several substitutions launched at the same time may be performed by SL\(\beta\). This point is a real increase in the calculation capacities of Lambda-calculus (same results for \({\mathcal D}).\)
The same result holds for the Lambda-calculus with couples and projection rules (without Surjective Pairing).
The locally confluent subsystem CCL\(\beta\) SP (that is \(SL\beta +(SP))\) is not confluent. This result is obtained by firstly designing a new counter-example (different from J. W. Klop’s one) for confluence of the Lambda-calculus with couples and Surjective Pairing and then translating it into CCL. However, CCL\(\beta\) SP is shown to be confluent on the set derived from \({\mathcal S}{\mathcal D}_{\lambda}.\)
These results cannot be obtained with classical methods of confluence and we designed a new method called Interpretation Method based on this trick: a given relation R is confluent on a set X if and only if a relation \({\mathcal E}(R)\) induced by R on a set of regularized terms \({\mathcal E}(X)\) is confluent.”
Reviewer: C.Berline


03B40 Combinatory logic and lambda calculus
68Q42 Grammars and rewriting systems
18D15 Closed categories (closed monoidal and Cartesian closed categories, etc.)
03G30 Categorical logic, topoi
Full Text: DOI


[1] Barendregt, H.P., The lambda-calculus, (1984), North-Holland Amsterdam · Zbl 0549.03012
[2] Barendregt, H.P., Pairing without conventional restraints, Z. math. logik grundlag. math., 20, 289-306, (1974) · Zbl 0299.02030
[3] de Brujin, N., Lambda-calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church – rosser theorem, Indag. math., 34, 381-392, (1972) · Zbl 0253.68007
[4] de Brujin, N., Lambda-calculus notation with namefree formulas involving symbols that represent reference transforming mappings, Indag. math., 40, 348-356, (1978) · Zbl 0393.03009
[5] Church, A., The calculi of lambda-conversion, Annals of mathematics studies, Vol. 6, (1941), Princeton Univ. Press · JFM 67.0041.01
[6] Curien, P.L., Categorical combinators, sequential algorithms and functional programming, Research notes in theoretical computer science, (1986), Pitman London · Zbl 0643.68004
[7] Curry, H.B., Combinatory logic, (1958), North-Holland Amsterdam · Zbl 0158.24703
[8] Curry, H.B.; Hindley, J.R.; Seldin, J.P., Combinatory logic, (1972), North-Holland Amsterdam · Zbl 0269.02005
[9] Hardin, T., Résultats de confluence pour LES règles fortes de la logique combinatoire catégorique et liens avec LES lambda-calculs, Thèse de doctorat, 7, (1987), Université de Paris
[10] Hardin, T.; Laville, A., Proof of termination of the rewriting system SUBST on CCL, Theoret. comput. sci., 46, 305-312, (1986) · Zbl 0618.68031
[11] Hindley, R.; Seldin, J., Introduction to combinators and λ-calculus, London mathematical society student texts, Vol. 1, (1986), Cambridge University Press · Zbl 0614.03014
[12] Klop, J.W., Combinatory reduction systems, Dissertation, (1982), Mathematisch Centrum Amsterdam · Zbl 0466.03006
[13] Klop, J.W.; de Vrijer, R., Unique normal forms for λ-calculus with surjective pairing tech. report., 87-03, (1987), Centre of Mathematics and Computer Science Amsterdam
[14] Knuth, D.; Bendix, P., Simple word problems in universal algebras, (), 263-297 · Zbl 0188.04902
[15] Lambek, J.; Scott, P.J., Introduction to higher order categorical logic, (1987), Cambridge Univ. Press · Zbl 0596.03002
[16] Levy, J.J., Réductions correctes and optimales dans le lambda-calcul, Thèse d’etat, 7, (1978), Université de Paris
[17] Mauny, M., Compilation des langages fonctionnels dans LES combinateurs categoriques, Thèse de troisième cycle, 7, (1985), Université de Paris
[18] Turner, D., A new implementation technique for applicative languages, Software practice experience, 9, 31-49, (1979) · Zbl 0386.68009
[19] R. de Vrijer, Surjective pairing and strong normalisation: two themes in λ-calculus, Dissertation, University of Amsterdam.
[20] H. Yokouchi, Relationship between λ-calculus and rewriting systems for categorical combinators, Preprint, IBM Research Center, Tokyo. · Zbl 0672.03006
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.