Journal of the Association for Computing Machinery, Vol. 43, No. 2, March 1996, pp. 362–397.

Confluence Properties of Weak and Strong Calculi of Explicit Substitutions

PIERRE-LOUIS CURIEN

THÉRÈSE HARDIN

AND

JEAN-JACQUES LÉVY

Abstract. Categorical combinators [Curien 1986/1993; Hardin 1989; Yokouchi 1989] and more recently λσ-calculus [Abadi 1991; Hardin and Lévy 1989], have been introduced to provide an explicit treatment of substitutions in the λ-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:

1. We present a confluent weak calculus of substitutions, where no variable clashes can be feared;

2. We sove a conjecture raised in Abadi [1991]: λσ-calculus is not confluent (it is confluent on ground terms only).

This unfortunate result is “repaired” by presenting a confluent version of the λσ-calculus, named the λEnv-calculus in Hardin and Lévy [1989], called here the confluent λσ-calculus.

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

Copyright 1996 by ACM, Inc. Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or direct commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Publications Dept, ACM Inc., fax +1 (212) 869-0481, or permissions@acm.org.