Article ID Journal Published Year Pages File Type
9655960 Electronic Notes in Theoretical Computer Science 2005 16 Pages PDF
Abstract
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.
Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics
Authors
,