1
$\begingroup$

Given I have the expression $\lambda x (y(\lambda y(xy)))$, I know that $x$ is a bound variable because of the initial $\lambda x$, but I'm not sure how I could express the $y$ since it is free before the scope of $\lambda y$ and bound within this scope.

In order to represent this free variable, should I try some kind of substitution?

For example, $$\lambda x (y\quad(\;[z/y]\; \lambda y (xy)\;)\quad)$$

$$\lambda x (y\quad(\; \lambda z (xz)\;)\quad)$$

is the right way to do it?

$\endgroup$
  • 1
    $\begingroup$ The sets of free variables and bound variables don't need to be disjoint. $\endgroup$ – Derek Elkins Aug 22 '17 at 1:55
  • $\begingroup$ Ok, but will $y$ be free or not? By the definition I read, $FREE \text{_} VARIABLES( \lambda x.r) = FREE \text{_} VARIABLES(r) - \{x\}$, so I think this tells me $y$ won't be considered free, but in a certain point it is, so I'm confused $\endgroup$ – Daniel Aug 22 '17 at 2:13
  • 2
    $\begingroup$ $y$ is a free variable (and a bound variable), that it's also a bound variable in some other subterm is irrelevant. That said, you will often need to distinguish between different occurrences of a variable. In this case, one occurrence of $y$ is free and the other bound. An occurrence of a variable can't be both bound and free for the same expression. $y$ isn't a free variable in the subterm $\lambda y(xy)$, but the free variables for $y(\lambda y(xy))$ is the union of the free variables of the subterm $y$ and the free variables of the subterm $\lambda y(xy)$, and thus includes $y$. $\endgroup$ – Derek Elkins Aug 22 '17 at 2:19

Your Answer

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

Browse other questions tagged or ask your own question.