Search code examples
lambda-calculus

When will the x be equivalent to the y in substitution in beta-reduction?

I am learning type theory from the book Type Theory and Formal Proof. This is the definition of substitution.

definition

See the (1b), I can't find an example that the x is equivalent to the y. X and y both are variables, so I think that if y is declared as a variable, the x cannot be equivalent to the y.

Solution

  • Case 1a could also be rewritten as

    y[x:=N] ≡ N, if x ≡ y

    x, y, z, ... are just meta variables that stand for concrete variables u, v, w, ... in the language of lambda calculus. In principle, we could insert the same actual variable for the placeholders x and y when applying the definition template to some concrete lambda term, and that's the case when x ≡ y.

    1a covers the case where the variable in which the substitution happens is the same as the one which gets substituted, and 1b covers the case where the variable in which the substitution happens is not the one that gets substituted.
    In case 1a, the entire variable gets replaced; in case 1b, nothing happens.

    Example:

    (a) (λu.u)(λw.w) >> u[u:=(λw.w)] ≡ (λw.w)   (covered by case 1a)
(b) (λu.v)(λw.w) >> v[u:=(λw.w)] ≡ v        (covered by case 1b)

    Both substitutions have the form y[x:=N], and in both examples, N ≡ (λw.w).
    In (a), y ≡ u and x ≡ u, so x ≡ y: This is case 1a.
    In (b), y ≡ v and x ≡ u, so x \≡ y: This is case 1b.