External and Internal Syntax of the λ-calculus

Abstract. It is well known that defining the substitution operation on λ-terms appropriately and establish basic properties like the substitution lemma is a subtle task if we wish to do it formally. The main obstacle here comes from the fact that unsolicited capture of free variables may occur during the substitution if one defines the operation naively. We argue that although there are several approaches to cope with this problem, they are all unsatisfactory since each of them defines the λ-terms in terms of a single fixed syntax. We propose a new way of defining λ-terms which uses an external syntax to be used mainly by humans and an internal syntax which is used to implement λ-terms on computers. In this setting, we will show that we can define λ-terms and the sub-stitution operation naturally and can establish basic properties of terms easily.