Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions. (English) Zbl 0944.68033

Summary: This paper studies confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions, where extensionality is interpreted by \(\eta\)-expansion. For that, we propose a scheme for explicit substitutions which describes those abstract properties that are sufficient to guarantee confluence. Our method makes it possible to treat at the same time many well-known calculi such as \(\lambda_{\sigma},\lambda_{\sigma \Uparrow},\lambda_{\varphi},\lambda_{s},\lambda_{v},\lambda_{f},\lambda_{d}\) and \(\lambda_{d}n\).


68N18 Functional programming and lambda calculus
Full Text: DOI


[1] Abadi, M.; Cardelli, L.; Curien, P.L.; Lévy, J.-J., Explicit substitutions, J. funct. programming, 4, 1, 375-416, (1991) · Zbl 0941.68542
[2] Y. Akama, On Mints’ reductions for ccc-Calculus, in: Proc. Int. Conf. on Typed Lambda Calculi and Applications (TLCA), Lecture Notes in Computer Science, vol. 664, Springer, Berlin, 1993. · Zbl 0786.03006
[3] Benaissa, Z.-E.-A.; Briaud, D.; Lescanne, P.; Rouyer-Degli, J., \(λυ\), a calculus of explicit substitutions which preserves strong normalisation, J. funct. programming, 6, 5, 699-722, (1996) · Zbl 0873.68108
[4] Bloo, R.; Rose, K., Combinatory reduction systems with explicit substitution that preserve strong normalisation, ()
[5] Briaud, D., An explicit eta rewrite rule, () · Zbl 1063.68552
[6] P.-L. Curien, Combinateurs Catégoriques, algorithmes séquentiels et programmation applicative, Thèse d’etat, Université Paris VII, 1983.
[7] P.-L. Curien, Categorical combinators, sequential algorithms and functional programming, Progress in Theoretical Computer Science, 1st ed., Birkhaüser, Basel, 1986. · Zbl 0643.68004
[8] P.-L. Curien, R. Di Cosmo, A confluent reduction system for the \(λ\)-calculus with surjective pairing and terminal object, in: Leach, Monien, Artalejo (Eds.), Internat. Conf. on Automata, Languages and Programming (ICALP), Lecture Notes in Computer Science, vol. 510, Springer, Berlin, 1991, pp. 291-302. · Zbl 0769.68056
[9] P.-L. Curien, T. Hardin, J.-J. Lévy, Confluence Properties of Weak and Strong Calculi of Explicit substitutions, Technical Report 1617, INRIA-Rocquencourt, 1992.
[10] P.-L. Curien, T. Hardin, A. Rı́os, Strong normalisation of Substitutions, MFCS’92, Lecture Notes in Computer Science, vol. 629, Springer, Berlin, 1992, pp. 209-218.
[11] de Bruijn, N., Lambda-calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem, Indag. mat., 5, 35, 381-392, (1972) · Zbl 0253.68007
[12] de Bruijn, N., Lambda-calculus notation with namefree formulas involving symbols that represent reference transforming mappings, Indag. mat., 40, 356-384, (1978) · Zbl 0393.03009
[13] Di Cosmo, R.; Kesner, D., A confluent reduction for the extensional typed \(λ\)-calculus with pairs, sums, recursion and terminal object, () · Zbl 1422.03022
[14] R. Di Cosmo, D. Kesner, Combining first order algebraic rewriting systems, recursion and extensional typed lambda calculi, Internat Conf. on Automata, Languages and Programming (ICALP), Lecture Notes in Computer Science, vol. 820, Springer, Berlin, 1994. · Zbl 0874.68158
[15] Di Cosmo, R.; Kesner, D., Rewriting with extensional polymorphic \(λ\)-calculus (extended abstract), ()
[16] D. Dougherty, Some lambda calculi with categorical sums and products, Proc. 5th Int. Conf. on Rewriting Techniques and Applications (RTA), Lecture Notes in Computer Science, vol. 690, Springer, Berlin, 1993.
[17] G. Dowek, T. Hardin, C. Kirchner, Higher-Order Unification via explicit substitutions, Proc. Symp. on Logic in Computer Science (LICS), 1995. · Zbl 1005.03016
[18] T. Ehrhard, Une sémantique catégorique des types dépendants. Application au calcul des constructions, Thèse de doctorat, Université de Paris VII, 1988.
[19] Ferreira, M.C.F.; Kesner, D.; Puel, L., \(λ\)-calculi with explicit substitutions and composition which preserve \(β\)-strong normalization (extended abstract), (), 284-298 · Zbl 1355.68039
[20] T. Hardin, 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, Université de Paris VII, 1987.
[21] T. Hardin, \(η\)-reduction for explicit substitutions, Algebraic and Logic Programming’92, Lecture Notes in Computer Science, vol. 632, Springer, Berlin, 1992.
[22] Hardin, T., Eta-conversion for the languages of explicit substitutions, Applicable alg. eng. commun. comput., 5, 317-341, (1994) · Zbl 0810.03010
[23] T. Hardin, A. Laville, Proof of termination of the rewriting system subst on c.c.l., Theoret. Comput. Sci., 1986. · Zbl 0618.68031
[24] T. Hardin, J.-J. Lévy, A confluent calculus of substitutions, France-Japan Artificial Intelligence and Computer Science Symp., 1989.
[25] T. Hardin, L. Maranget, B. Pagano, Functional back-ends and compilers within the lambda-sigma calculus, 1995, Draft. · Zbl 1345.68056
[26] G. Huet, Résolution d’équations dans les langages d’ordre \(1,2,…,ω\), Thèse de Doctorat d’état, Université Paris VII, 1976.
[27] Jay, C.B.; Ghani, N., The virtues of eta-expansion, J. funct. programming, 5, 2, 135-154, (1995) · Zbl 0833.68072
[28] F. Kamareddine, A. Rı́os, A \(λ\)-calculus à la de Bruijn with explicit substitutions, Proc. Int. Symp. on Programming Language Implementation and Logic Programming, Lecture Notes in Computer Science, vol. 982, Springer, Berlin, 1995.
[29] Kesner, D., Confluence properties of extensional and non-extensional \(λ\)-calculi with explicit substitutions, (), 184-199 · Zbl 0944.68033
[30] D. Kesner, Confluence of extensional and non-extensional \(λ\)-calculi with explicit substitutions, Technical Report 1103, LRI, Université Paris-Sud, 1997. · Zbl 0944.68033
[31] D. Kesner, Reasoning about redundant patterns, J. Funct. Logic Programming, 1997, to appear. · Zbl 0924.68047
[32] J.W. Klop, Combinatory Reduction Systems, Mathematical Centre Tracts, vol. 127, CWI, Amsterdam, 1980, Ph.D. Thesis. · Zbl 0466.03006
[33] Klop, J.W.; van Oostrom, V.; van Raamsdonk, F., Combinatory reduction systems: introduction and survey, Theoret. comput. sci., 121, 279-308, (1993) · Zbl 0796.03024
[34] P. Lescanne, From \(λσ\) to \(λv\), a journey through calculi of explicit substitutions, in: Ann. ACM Symp. on Principles of Programming Languages (POPL), ACM, 1994, pp. 60-69.
[35] P. Lescanne, Personal Communication, 1996.
[36] P. Lescanne, J. Rouyer-Degli, The calculus of explicit substitutions \(λν\), Technical Report, INRIA, Lorraine, 1994. · Zbl 0873.68108
[37] M. Mauny, Compilation des langages fonctionnels dans les combinateurs catégoriques. Applications au langage ML, Thèse 3em̀e cycle, Université Paris VII, 1985.
[38] P.-A. Mellies, Four typed-lambda calculi with explicit substitutions may not terminate: the first examples, 1994, Draft.
[39] Mellies, P.-A., Typed \(λ\)-calculi with explicit substitutions may not terminate, () · Zbl 1063.03522
[40] Mints, G., Closed categories and the theory of proofs, Zapiski nauchnykh seminarov leningradskogo otdeleniya matematicheskogo instituta im. V.A. steklova AN SSSR, 68, 83-114, (1977)
[41] G. Mints, Teorija categorii i teoria dokazatelstv.I, Aktualnye problemy logiki i metodologii nauky, 1979, pp. 252-278.
[42] Muñoz, C., A left-linear variant of \(λσ\), () · Zbl 0884.03012
[43] B. Pagano, Des calculs de substitution explicite et de leur application à la compilation des langages fonctionnels, Thèse de doctorat, Université Pierre et Marie Curie, 1998.
[44] G. Pottinger, The Church Rosser theorem for the typed lambda-calculus with Surjective pairing, Notre Dame J. Formal Logic 22 (3) (1981) pp. 264-268. · Zbl 0476.03026
[45] D. Prawitz, Ideas and results in proof theory, Proc. 2nd Scandinavian Logic Symp., 1971, pp. 235-307. · Zbl 0226.02031
[46] A. Rı́os, Contribution à l’étude des \(λ\)-calculus avec substitutions explicites, Thèse de doctorat, Université de Paris VII, 1993.
[47] V. van Oostrom, F. van Raamsdonk, Weak orthogonality implies confluence: the higher-order case, Proc. 3rd Internat. Symp. on Logical Foundations of Computer Science, 1994, pp. 379-392. · Zbl 0964.68523
[48] Zantema, H., Termination on term rewriting: interpretation and type elimination, J. symbolic comput., 1, 17, 23-50, (1994) · Zbl 0810.68087
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.