patternModerate
Free and Bound in Lambda Calculus
Viewed 0 times
boundcalculusfreeandlambda
Problem
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?
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?
Solution
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.
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.
Context
StackExchange Computer Science Q#10212, answer score: 11
Revisions (0)
No revisions yet.