MHB Free variables and binding occurrence of each variable.

[JamesBwoii]

Hi, I'm trying to identify the free variable and binding occurrence but I'm not sure if they're right in lambda calculus.

1. $x$
2. $\lambda x.x$
3. $(\lambda a.z)a$
4. $\lambda a.za$
5. $(\lambda n.n)z$
6. $\lambda z.(\lambda y.(\lambda x.x)y)z$
7. $(\lambda t.((\lambda t.(\lambda t.t)t)t))t$

Then for free variables for them I have got:

1. $x$
2. No free variable
3. ${z,a}$
4. $z$
5. $z$
6. No free variable
7. $t$

For the binding occurrence would it just be the link between the $\lambda x$ and the free variable $x$ in $\lambda x.x$?

 

[Evgeny.Makarov]

Mmm, lambda calculus... (in Homer Simpson's voice).

You are right about free variables. The term "binding occurrence" is not standard. You are probably right, but you may want to consult the definition and maybe post it here. I would say, "...and the free variable $x$ in the body of $\lambda x.x$".