From http://www.seas.gwu.edu/~rhyspj/spring09cs145/lab8/lab82.htmlThe 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))))$? I wonder if the $x$ in $(y\,\, x)$ and the $x$ in $(x\,\, y)$ are the sameor 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))))$?Do the two occurrences of $y$ mean the same variable?
recursive lambda expressions
terminology;lambda calculus
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.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.