recursive lambda expressions

Question

From http://www.seas.gwu.edu/~rhyspj/spring09cs145/lab8/lab82.html

The lambda operator does not bind every occurrence of its variable because "shadowing" can occur. A variable is bound by its nearest enclosing lambda.

In $(\lambda (x) ((y\,\, x) (\lambda (x) (x\,\, y))))$, the $x$ in $(y\,\, x)$ is bound by the outermost lambda, whereas the $x$ in $(x\,\, y)$ is bound by the inner lambda. In this example, both occurrences of $y$ are free.

How shall I understand the lambda expression $(\lambda (x) ((y\,\, x) (\lambda (x) (x\,\, y))))$?

1. I wonder if the $x$ in $(y\,\, x)$ and the $x$ in $(x\,\, y)$ are the same or different variables?

   If I rename one of them, will the renamed version be the same as $(\lambda (x) ((y\,\, x) (\lambda (x) (x\,\, y))))$? E.g.

   • Is $(\lambda (x) ((y\,\, x) (\lambda (z) (z\,\, y))))$ the same as $(\lambda (x) ((y\,\, x) (\lambda (x) (x\,\, y))))$?
   • Is $(\lambda (z) ((y\,\, z) (\lambda (x) (x\,\, y))))$ the same as $(\lambda (x) ((y\,\, x) (\lambda (x) (x\,\, y))))$?

2. Do the two occurrences of $y$ mean the same variable?

Answer 1

1. Informally speaking the two x's are indeed different variables (technically speaking, they are the same variables but bound by different abstractors).

   As for your two inquiries regarding equivalences: in the strictest sense possible, they are not syntactically equivalent ($M \not\equiv N$). However, they are what is called equivalent modulo alpha ($M \equiv_\alpha N$). This basically means that one can be transformed into the other through $\alpha$-conversion (which leaves the behaviour of the term unchanged). The result is that the names of bound variables become arbitrary - as they should be.

   Note that most equivalences in lambda calculus are stated modulo $\alpha$, and most lambda logicians seem to regard the formulation and application of the rule as a tedious formality. Once they have specified the $\alpha$-rule (if they even care to do so in the first place), they tend to adopt the following convention: 'from now on, when we say $M$ and $N$ are equivalent ($M \equiv N$), we just mean that they are equivalent modulo alpha ($M \equiv_\alpha N$), unless stated otherwise'. So in most contexts, you can simply say they are 'the same', but I think you should be aware of the details behind it.

2. Yes. If $y$ were to be substituted for some $z$ in that term, then all occurrences of $y$ will be replaced by $z$.

This is perhaps a useful free resource that covers some of the basics a little more rigorously: http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/geuvers.pdf.