2
$\begingroup$

I am very confused as to which variables are captured by which λ in the example below:

(λa.λb.(λa.a)aba)(ab)

I am new to lambda calculus and the repetition of variables makes this example hard for me to understand and reduce. Any help would be appreciated!

$\endgroup$
2
$\begingroup$

If you make the construction tree of the expression, a variable $x$ of a leaf refers to that $\lambda x$ which is closest to $x$ in the path from $x$ to the root.

Another way to see it is with the use of scoping rules. The scope of each $\lambda$ is the body of the $\lambda$.

So, the scope of the inner-most $\lambda a$ is only $a$. This means that any occurrence of $a$ outside that parenthesis refers to a different variable than the $a$ inside the parenthesis (point 1).

The scope of the $\lambda b$ is $(λa.a)aba$, so similarly any $b$ outside this expression refers to a different variable (that just happens to have the same name).

The scope of the outermost $\lambda a$ is $\lambda b.(\lambda a.a)aba$. Here things are a bit more complex, because there's another $\lambda a$ inside. But according to point (1) the $a$ in $\lambda a.a$ is different than the $a$'s in the rest of the body. So, only the $a$'s in $aba$ refer to the outermost $\lambda a$.

Note that there are no lambda's to bind the $a$ and $b$ in subexpression $(ab)$ (on the right of the expression). Therefore, the $a$ and $b$ in $(ab)$ occur free.

$\endgroup$

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.