AbstractCategorical combinators [Curien 1986/1993; Hardin 1989; Yokouchi 1989] and more recently lambda-sigma-calculus [Abadi 1991; Hardin and Lévy 1989], have been introduced to provide an explicit treatment of substitutions in the lambda-calculus. we reintroduce here the ingredients of these calculi in a self-contained and stepwise way, with a special emphasis on confluence properties. The main new results of the paper with respect to Curien [1986/1993], Harding [1989], Abadi [1991], and Hardin and Lévy [1989] are the following:
This unfortunate result is ``repaired'' by presenting a confluent version of the lambda-sigma-calculus, named the lambdaEnv-calculus in Hardin and Lévy [1989], called here the confluent lambda-sigma-calculus.
- We present a confluent weak calculus of substitutions, where no variable clashes can be feared;
- We sove a conjecture raised in Abadi [1991]: lambda-sigma-calculus is not confluent (it is confluent on ground terms only).
The abstract is also available as a LaTeX file, a DVI file, or a PostScript file.
Categories and Subject Descriptors: F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages -- operational semantics; F.3.3 [Logics and Meanings of Programs]: Studies of Program Constructs -- functional constructs; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic -- lambda calenders and related systems
General Terms: Languages, Theory
Additional Key Words and Phrases: Confluency, explicit substitutions
Selected papers that cite this one
- P.-L. Curien, T. Hardin, and A. Ríos. Strong normalizations of substitutions. Journal of Logic and Computation, 6(6):799-817, December 1996.
- César Muñoz. Confluence and preservation of strong normalisation in an explicit substitutions calculus. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, pages 440-447, New Brunswick, New Jersey, 27-30 July 1996. IEEE Computer Society Press.
Selected references
- M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit substitutions. Journal of Functional Programming, 1(4):375-416, October 1991.
- Gérard Berry and Jean-Jacques Lévy. Minimal and optimal computations of recursive programs. Journal of the ACM, 26(1):148-175, January 1979.
- Gérard Boudol. Lambda-calculi for (strict) parallel functions. Information and Computation, 108(1):51-127, January 1994.
- P.-L. Curien. An abstract framework for environment machines. Theoretical Computer Science, 82(2):389-402, 31 May 1991. Note.
- Pierre-Louis Curien and Thérèse Hardin. Theoretical pearl: Yet yet a counterexample for lambda + SP. Journal of Functional Programming, 4(1):113-115, January 1994.
- Nachum Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17(3):279-301, March 1982.
- John Field. On laziness and optimality in lambda interpreters: Tools for specification and analysis. In Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, pages 1-15, San Francisco, California, January 1990.
- Thérèse Hardin. Confluence results for the pure strong categorical logic CCL. lambda-Calculi as subsystems of CCL. Theoretical Computer Science, 65(3):291-342, 17 July 1989. Fundamental study.
- Thérèse Hardin and Alain Laville. Proof of termination of the rewriting system SUBST on CCL. Theoretical Computer Science, 46(2-3):305-312, 1986. Note.
- Gérard Huet. Confluent reductions: Abstract properties and application to term rewriting systems. Journal of the ACM, 27(4):797-821, October 1980.
- John Lamping. An algorithm for optimal lambda calculus reduction. In Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, pages 16-30, San Francisco, California, January 1990.
- Luc Maranget. Optimal derivations in weak lambda-calculi and in orthogonal terms rewriting systems. In Conference Record of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, pages 255-269, Orlando, Florida, January 1991.
- C.-H. Luke Ong. Fully abstract models of the lazy lambda calculus. In 29th Annual Symposium on Foundations of Computer Science, pages 368-376, White Plains, New York, 24-26 October 1988. IEEE.
- Hirofumi Yokouchi. Church-Rosser theorem for a rewriting system on categorical combinators. Theoretical Computer Science, 65(3):271-290, 17 July 1989. Fundamental study.