Movatterモバイル変換

1. Whenlaying out the early principles of \(\lambda\)-calculus, Churchrestricted \(\beta\)-reduction to only those cases where variable capturedoes not occur. As an illustration of the kinds of difficulties thatcan arise if one is too casual about free and bound variables, one canformulate a sequent calculus for first-order logic where cutelimination fails if one views first-order formulas as concreteobjects rather than as an equivalence class of \(\alpha\)-convertibleformulas.

2. Other definitions ofsubstitution are available. One can, for example, modify clause (5)by requiring that all free occurrences of \(y\) in \(M\) arerewritten so that they do not become bound after substitution. Inthis way the variable capture that we are trying to avoid is built into the definition of substitution and thereby does not need to be laiddown as a separate convention.

There is a small price to pay for such an approach, though: thedefinition of substitution is somewhat more complicated than thestraightforward definition given here. There is even somenondeterminism in such an approach to substitution: if we need torewrite free occurrences of \(y\) in \(M\) beforesubstituting \(M\) for free occurrences of \(x\) in\(\lambda y[A]\), how should we do it? Which of theinfinitely many variables should we choose? One can get around thisdifficulty by using a predefined enumeration of the set of variables,or by other syntactic measures such as the so-called de Bruijnrepresentation of terms (which this entry does not treat). Ourstraightforward approach suffices for this entry’s introductorypurposes.

3. The theorem saysgiven \(M\) one can find at least one \(F\)that \(Fx = M\), but in fact there are infinitelymany. For example, if \(Fx = M\),then \(\bK F \bK\) also works. Church’s initial understanding of\(\lambda x[M]\) was existential—a solutionof \(Fx = M\) for \(F\)—though nowadays oneunderstands \(\lambda x[M]\) as a unique object, namely, thefunction that, given \(x\), produces \(M\).

4. This is not to say that nosense whasotever can be made of adding 5 and the identity function.The intention of this example is to motivate the differentiation of adomain of discourse into kinds or types.

Indeed, if one wanted, one possible strategy for interpreting sucha combination would be to ‘promote’ the number 5 byreading it as the constant function \(\lambda x\)[5]; we then needto understand addition of unary functions. One can can naturallyunderstand \((\lambda x[5]) + (\lambda x[x]\)) as\((\lambda x[5 + x])\).

5. If an untyped\(\lambda\)-term \(M\) can be assigned one type, then it can beassigned infinitely many types: for any type variable \(a\) occursin the type \(\sigma\) assigned to \(M\), one can substitute any type\(\tau\), and the result is still a type for \(M\). For example, thecombinator \(\bI\) can be assigned the type \(a \rightarrow a.\)Thus, it can be assigned the types:

It is thus not correct to talk aboutthe type of a typableterm.

Nonetheless, a result known as theprincipal type theoremassures us that the situation with \(\bI\) just illustrated istypical: if a term \(M\) can be assigned a type at all, then thereis a type \(\tau\) such that all types that can be assigned to \(M\)are instances of \(\tau\). Such a type is called aprincipaltype of \(M\). Even though it is improper to talkaboutthe principal type of a typable term—if \(a\)and \(b\) are distinct type variables, then \(a \rightarrow a\) and \(b \rightarrow b\) are distinct principaltypes of \(\bI\)—there is still a precise sense in which thereis one and only one principal type of a typable term: \(a \rightarrow a\) and \(b \rightarrow b\) are simply (uniform)substitution instances of each other.

There is an algorithm for computing principal types; see (Hindley,1997, chapter 3).

6.Definition: For a natural number \(n\), define\(\bc_n\), the \(n\)thChurch numeral, as\(\lambda f[\lambda x[f^n x]]\). \((\text{‘}f^n x\text{’}\) is theapplication of the \(n\)-fold iteration of \(f\) to \(x.)\)

Thus \(\bc_0\), the Church numeral for the natural number 0, is\(\lambda x[x], \bc_1\) is \(\lambda f[\lambda x[fx]], \bc_2\) is\(\lambda f[\lambda x[f(fx)]]\), and so forth.