zbMATH — the first resource for mathematics

Comparing and implementing calculi of explicit substitutions with eta-reduction. (English) Zbl 1067.03042
Summary: The past decade has seen an explosion of work on calculi of explicit substitutions. Numerous works have illustrated the usefulness of these calculi for practical notions like the implementation of typed functional programming languages and higher-order proof assistants. It has also been shown that eta-reduction is useful for adapting substitution calculi for practical problems like higher-order unification. This paper concentrates on rewrite rules for eta-reduction in three different styles of explicit substitution calculi: \(\lambda\sigma\), \(\lambda s_e\) and the suspension calculus. Both \(\lambda\sigma\) and \(\lambda s_e\), when extended with eta-reduction rules, have proved useful for solving higher-order unification. We enlarge the suspension calculus with an adequate eta-reduction rule which we show to preserve termination and confluence of the associated substitution calculus and to correspond to the eta rules of the other two calculi. We prove that \(\lambda\sigma\) and \(\lambda s_e\) as well as \(\lambda \sigma\) and the suspension calculus are non-comparable while \(\lambda s_e\) is more adequate than the suspension calculus in simulating one-step beta-reduction.
After defining the eta-reduction rule in the suspension calculus, and after comparing these three calculi of explicit substitutions (all with an eta rule), we then concentrate on the implementation of the rewrite rules of eta-reduction in these calculi. We note that it is usual practice when implementing the eta rule for substitution calculi, to mix isolated applications of eta-reduction with the application of other rules of the corresponding substitution calculi. The main disadvantage of this practice is that the eta rewrite rules so obtained are unclean because they have an operational semantics different from that of the eta-reduction of the \(\lambda\)-calculus. For the three calculi in question enlarged with adequate eta rules we show how to implement these eta rules. For the \(\lambda s_e\) we build a clean implementation of the eta rule and we prove that it is not possible to follow the same approach for the \(\lambda\sigma\) and \(\lambda_{\text{SUSP}}\).

03B70 Logic in computer science
03B40 Combinatory logic and lambda calculus
68N18 Functional programming and lambda calculus
68Q42 Grammars and rewriting systems
ALF; Automath
Full Text: DOI
[1] Abadi, M.; Cardelli, L.; Curien, P.-L.; Lévy, J.-J., Explicit substitutions, Journal of functional programming, 1, 4, 375-416, (1991) · Zbl 0941.68542
[2] Ayala-Rincón, M.; Kamareddine, F., On applying the \(\lambda s_e\)-style of unification for simply-typed higher order unification in the pure lambda calculus, (), 41-54 · Zbl 1073.03007
[3] Ayala-Rincón, M.; Kamareddine, F., Unification via the \(\lambda s_e\)-style of explicit substitution, The logic journal of the interest group in pure and applied logics, 9, 4, 489-523, (2001) · Zbl 0987.03012
[4] Ayala-Rincón, M.; Muñoz, C., Explicit substitutions and all that, Revista colombiana de computación, 1, 1, 47-71, (2000)
[5] Baader, F.; Nipkow, T., Term rewriting and all that, (1998), Cambridge University Press
[6] Barendregt, H., The lambda calculus: its syntax and semantics, (1984), North-Holland · Zbl 0551.03007
[7] Benaissa, Z.-el-A.; Briaud, D.; Lescanne, P.; Rouyer-Degli, J., \(\lambda \upsilon\), a calculus of explicit substitutions which preserves strong normalization, Journal of functional programming, 6, 5, 699-722, (1996) · Zbl 0873.68108
[8] Benaissa, Z.-el-A.; Lescanne, P.; Rose, K.H., Modeling sharing and recursion for weak reduction strategies using explicit substitution, (), 393-407
[9] R. Bloo, Preservation of termination for explicit substitution, Ph.D. Thesis, Department of Mathematics and Computing Science, Eindhoven University of Technology, 1997 · Zbl 0883.03008
[10] Bloo, R.; Rose, K., Combinatory reduction systems with explicit substitution that preserve strong normalisation, (), 169-183
[11] Borovanský, P., Implementation of higher-order unification based on calculus of explicit substitutions, (), 363-368
[12] Briaud, D., An explicit eta rewrite rule, (), 94-108 · Zbl 1063.68552
[13] Curien, P.-L.; Hardin, T.; Lévy, J.-J., Confluence properties of weak and strong calculi of explicit substitutions, Journal of the ACM, 43, 2, 362-397, (1996), Also as Rapport de Recherche INRIA 1617, 1992 · Zbl 0885.03014
[14] de Bruijn, N.G., Lambda-calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church – rosser theorem, Indagationes mathematicae, 34, 5, 381-392, (1972) · Zbl 0253.68007
[15] Dowek, G.; Hardin, T.; Kirchner, C., Higher-order unification via explicit substitutions, Information and computation, 157, 1-2, 183-235, (2000) · Zbl 1005.03016
[16] Ferreira, M.C.F.; Kesner, D.; Puel, L., Lambda-calculi with explicit substitutions and composition which preserve beta-strong normalisation, (), 284-298 · Zbl 1355.68039
[17] B. Guillaume, Un calcul des substitutions avec etiquettes, Ph.D. Thesis, Université de Savoie, Chambéry, 1999
[18] Guillaume, B., The \(\lambda s_e\)-calculus does not preserve strong normalization, Journal of functional programming, 10, 4, 321-325, (2000) · Zbl 0971.68021
[19] Hardin, T., Eta-conversion for the languages of explicit substitutions, (), 306-321 · Zbl 0925.03089
[20] Hardin, T.; Maranget, L.; Pagano, B., Functional runtime systems within the lambda – sigma calculus, Journal of functional programming, 8, 2, 131-176, (1998) · Zbl 0918.03018
[21] Kamareddine, F.; Nederpelt, R.P., On stepwise explicit substitution, International journal of foundations of computer science, 4, 3, 197-240, (1993) · Zbl 0806.03013
[22] Kamareddine, F.; Nederpelt, R.P., A useful \(\lambda\)-notation, Theoretical computer science, 155, 85-109, (1996) · Zbl 0873.03018
[23] Kamareddine, F.; Ríos, A., A \(\lambda\)-calculus à la de Bruijn with explicit substitutions, (), 45-62
[24] Kamareddine, F.; Ríos, A., Extending a \(\lambda\)-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms, Journal of functional programming, 7, 395-420, (1997) · Zbl 0882.03011
[25] Kamareddine, F.; Ríos, A., Bridging de Bruijn indices and variable names in explicit substitutions calculi, The logic journal of the interest group of pure and applied logic, 6, 6, 843-874, (1998) · Zbl 0914.03019
[26] Kamareddine, F.; Ríos, A., Relating the \(\lambda \sigma\)- and \(\lambda s\)-styles of explicit substitutions, Journal of logic and computation, 10, 3, 349-380, (2000) · Zbl 0953.03013
[27] Kamareddine, F.; Ríos, A., Explicit substitutions à la de Bruijn: the local and global way, Electronic notes in theoretical computer science, 85, 7, (2003) · Zbl 1264.03044
[28] Kamareddine, F.; Ríos, A.; Wells, J.B., Calculi of generalised \(\beta\)-reduction and explicit substitution: type free and simply typed versions, The journal of functional and logic programming, 1998, 5, 1-44, (1998)
[29] Kesner, D., Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions, Theoretical computer science, 238, 1-2, 183-220, (2000) · Zbl 0944.68033
[30] Lescanne, P.; Rouyer-Degli, J., Explicit substitutions with de bruijn’s levels, (), 294-308
[31] Liang, C.; Nadathur, G., Tradeoffs in the intensional representation of lambda terms, (), 192-206 · Zbl 1045.68530
[32] L. Magnusson, The implementation of ALF—a proof editor based on Martin Löf’s type theory with explicit substitutions, Ph.D. Thesis, Chalmers, 1995
[33] C. Muñoz, Un calcul de substitutions pour la représentation de preuves partielles en théorie de types, Ph.D. Thesis, Université Paris 7, 1997, English version in Rapport de recherche INRIA RR-3309, 1997
[34] Nadathur, G., A fine-grained notation for lambda terms and its use in intensional operations, The journal of functional and logic programming, 1999, 2, 1-62, (1999) · Zbl 0924.68055
[35] Nadathur, G., The suspension notation for lambda terms and its use in metalanguage implementations, () · Zbl 1261.68043
[36] Nadathur, G.; Miller, D., An overview of \(\lambda\)prolog, (), 810-827
[37] Nadathur, G.; Wilson, D.S., A notation for lambda terms a generalization of environments, Theoretical computer science, 198, 49-98, (1998) · Zbl 0901.03015
[38] Nederpelt, R.P.; Geuvers, J.H.; de Vrijer, R.C., Selected papers on automath, (1994), North-Holland · Zbl 0822.03009
[39] A. Ríos, Contribution à l’étude des \(\lambda\)-calculs avec substitutions explicites, Ph.D. Thesis, Université de Paris 7, 1993
[40] Vestergaard, R.; Wells, J.B., Cut rules and explicit substitutions, Mathematical structures in computer science, 11, 1, 131-168, (2001) · Zbl 0972.68102
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.