7
$\begingroup$

Here's something from Slonneger's "Syntax and Semantics of Programming Languages":

A variable may occur both bound and free in the same lambda expression: for example, in λx.yλy.yx the first occurrence of y is free and the other two are bound.

I assume the free variable is the y right after the λx. and the bound y's are the λy.y which I can sort of intuitively grasp. So ((λx.yλy.yx)a)b) would reduce to (yλy.ya)b) then to bba ? Can someone explain how this came to be? In the end it's the expression b twice. Can someone perhaps provide more examples of bound and free variables?

$\endgroup$

migrated from cstheory.stackexchange.com Mar 2 '13 at 21:12

This question came from our site for theoretical computer scientists and researchers in related fields.

  • $\begingroup$ I think Slonneger didn't use a good example there, because $\lambda x.y$ may be easily misread as $\lambda xy$, which is usually short for $\lambda x.\lambda y$. I would give a different example: in $(\lambda x.\lambda y. xyx)x$, the last occurrence of $x$ is free, and the others are bound. $\endgroup$ – Jay Mar 31 '16 at 12:33
11
$\begingroup$

I've added brackets to disambiguate $$\lambda x.(\color{red}y (\color{green}{\lambda y}.(\color{blue}yx)))$$ the red $y$ is free and the blue one is bound by the green abstraction. I don't think it makes sense to say that the green $y$ is bound, but it together with the lambda is a binder.

We can beta reduce the term once

$$\begin{array}? && \lambda x.(y (\lambda y.(yx)))ab \\ &\to_\beta& (y (\lambda y.(ya)))b \end{array}$$

but no further, as there are no remaining redexes left.

$\endgroup$

Your Answer

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