From λσ to λν: a journey through calculi of explicit substitutions

ABSTRACT

This paper gives a systematic description of several calculi of explicit substitutions. These systems are orthogonal and have easy proofs of termination of their substitution calculus. The last system, called &lgr;v, entails a very simple environment machine for strong normalization of &lgr;-terms.

REFERENCES

• ACCL91: M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. L~vy. Explicit substitutions. J. of Functional Programming, 1(4):375-416, 1991.
• Asp92: A. Asperti. A categorical understanding of environment machines. J. of Functional Programming, 2(1):23-59, January 1992.
• Bar84: H.P. Barendregt. The Lambda-Calculus, its syntax and semantics. Studies in Logic and the Foundation of Mathematics. Elsevier Science Publishers B. V. (North-Holland), Amsterdam, 1984. Second edition.
• CHL92: P.-L. Curien, Th. Hardin, and J.-J. L6vy. Confluence properties of weak and strong calculi of explicit substitutions. RR 1617, INRIA, Rocquencourt, February 1992.
• Cré90: P. Cr6gut. An abstract machine for the normalization of A-calculus. In Proc. Conf. on Lisp and Functional Progamming, 1990.
• Cur93: Pierre-Louis Curien, Categorical combinators, sequential algorithms, and functional programming (2nd ed.), Birkhauser Boston Inc., Cambridge, MA, 1994
• Har92: Thérèse Hardin, Eta-conversion for the Languages of Explicit Substitutions, Proceedings of the Third International Conference on Algebraic and Logic Programming, p.306-321, September 02-04, 1992
• Her88: M. Hermann. Vademecum of divergent term rewriting systems. Research report 88-R-082, Centre de Recherche en Informatique de Nancy, 1988.
• HL89: Th. Hardin and J.-J. L6vy. A confluent calculus of substitutions. In France-Japan Artificial Intelligence and Computer Science Symposium, Izu~ 1989.
• HL91: G. Huet and J.-J. L6vy. Computations in orthogonal rewriting systems, i. In J.-L. Lassez and G. Plotkin, editors, Computational Logic, chapter 11. The MIT Press, 1991.
• Les90: Pierre Lescanne, Implementations of Completion by Transition Rules + Control: ORME, Proceedings of the Second International Conference on Algebraic and Logic Programming, p.262-269, October 01-03, 1990
• Les92: Pierre Lescanne, Termination of Rewrite Systems by Elementary Interpretations, Proceedings of the Third International Conference on Algebraic and Logic Programming, p.21-36, September 02-04, 1992
• Río93: A. Rios. Contributions a lYtude des )~-calculs avec des substitutions explicites. Thbse de Doctorat d'Universit6, U. Paris VII, 1993.
• Rit92: E. PAtter. Categorical Abstract Machines for Higher-Order Typed Lambda Calculi. PhD thesis, Cambridge U., Trinity College, September 1992.
• Zan93: Hans Zantema, Termination of Term Rewriting by Interpretation, Proceedings of the Third International Workshop on Conditional Term Rewriting Systems, p.155-167, July 08-10, 1992

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Theory