Abstract Conditions for the Confluence of Explicit Substitution Calculi

The aim of this paper is to give abstract properties of some calculi with explicit substitution which will be sufficient to prove their confluence. We define a property that we call “implementing a good notion of substitution.” We show that calculi with explicit substitution having this property are confluent and their substitution reductions are also confluent. We test our theory with the well-known calculi of explicit substitution λs, λυ and λse. The latter is λs with open terms. The property of implementing a good substitution is natural and characterizes a large number of calculi. Two conditions of this property are usually checked as an initial step in the proof for confluence. The third condition is new and is the key for our proofs of confluence.