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?

  • $\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, 2016 at 12:33

1 Answer 1


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.