1
$\begingroup$

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?

$\endgroup$

1 Answer 1

3
$\begingroup$

$$(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)$$

$\endgroup$
5
  • 1
    $\begingroup$ [] 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. $\endgroup$
    – sudee
    Oct 7, 2016 at 21:35
  • $\begingroup$ @sudee $y$ also has a name conflict. $\endgroup$
    – DanielV
    Oct 7, 2016 at 22:15
  • $\begingroup$ They do have the same name but because the inner $y$ is bound by the $\lambda$-abstraction there is no ambiguity. $\endgroup$
    – sudee
    Oct 8, 2016 at 6:08
  • $\begingroup$ 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 ](math.stackexchange.com/a/1559114/833760) as a guide to figure out what's bound and what's free. $\endgroup$
    – joseville
    Nov 11, 2021 at 18:40
  • 1
    $\begingroup$ @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. $\endgroup$
    – DanielV
    Nov 12, 2021 at 1:03

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.