1

Currently I am trying to use substitution in Lamdba Calculus but I haven't cleared up free and bound variables quite like I thought I had. For example, I have the following expression:

λx.xy where y is a free variable and x is a bound variable.

I'm unsure whether x is only bound because of λx. E.g if the expression was λx.yx, would the y be bound and the x be free? or would the x still be bound because of λx?

Here is the actual question I am trying to tackle:

(y(λz.xz)) [x := λy.zy]

I believe that y is a free variable and within the λ-expression, z is bound and x is free. Is this correct?

Chris
  • 151

1 Answers1

3

$$(y~(\lambda ~z~.~x~z))[~x := \lambda~ y~.~z~y~]$$

That expression has a lot of variable name conflicts:

$$(y_1~(\lambda ~z_1~.~x_1~z_1))[~x_1 := \lambda~ y_2~.~z_2~y_2~]$$

which transforms to:

$$(y_1~(\lambda ~z_1~.~(\lambda~ y_2~.~z_2~y_2)~z_1))$$

Here

  • $y_1$ is a free variable
  • $y_2$ is a bound variable
  • $z_1$ is a bound variable
  • $z_2$ is a free variable

The initial expression isn't actually a valid lambda expression because of the [], so whether $x_1$ is a free or bound variable is ambiguous, since it isn't actually part of the expression. If the [] is meant to represent a beta transform, then $x_1$ was a bound variable in the expression:

$$(\lambda x_1~.~y_1~(\lambda ~z_1~.~x_1~z_1))(\lambda~ y_2~.~z_2~y_2)$$

DanielV
  • 23,556
  • 1
    [] is the standard notation for substitution, which is just a syntactic transformation. In this case there would only be one name conflict, for $z$. To carry out the substitution we need to use $\alpha$-conversion to give $z$ a different name in the right-hand side term, then replace every instance of $x$ in the term on the left. – sudee Oct 07 '16 at 21:35
  • @sudee $y$ also has a name conflict. – DanielV Oct 07 '16 at 22:15
  • They do have the same name but because the inner $y$ is bound by the $\lambda$-abstraction there is no ambiguity. – sudee Oct 08 '16 at 06:08
  • Why is $_2$ bound in $(_1 ( _1 . ( _2 . _2 _2) _1))$ if there's no $ _2$ anywhere? I'm using this other math.se answer as a guide to figure out what's bound and what's free. – joseville Nov 11 '21 at 18:40
  • 1
    @joseville I don't know how I messed that up, just a typo. Sorry for that. z_1 is bound and z_2 is free. – DanielV Nov 12 '21 at 01:03