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?


1 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.

  • $\begingroup$ "...the most strictest sense..." - double superlative $\endgroup$
    – d'alar'cop
    Jul 16, 2014 at 22:27
  • $\begingroup$ @d'alar'cop: oops, that slipped in. Thanks. $\endgroup$
    – Roy
    Jul 16, 2014 at 22:49
  • $\begingroup$ Is "(lambda (x) ((y x) (lambda (x) (x y))))" equivalent to "(lambda (x) (y (lambda (x) (x y))))"? Can it be further simplied? thanks. $\endgroup$
    – Tim
    Jul 16, 2014 at 23:37
  • 1
    $\begingroup$ Let me translate those terms to more conventional (and I think clearer) notation first: $(\lambda x.(yx) (\lambda x.xy))$ and $(\lambda x. y (\lambda x.xy))$. Both of these terms are in normal form (they cannot be reduced any further), and they are different. You can also see this clearly in how they behave. The first term accepts an argument $M$ and substitutes it for the first $x$ (which is in scope): $(\lambda x.(yx) (\lambda x.xy))M \rhd_\beta (yM)(\lambda x.xy)$. The second term throws it away (since there are no $x$'s in scope): $(\lambda x.y (\lambda x.xy))M \rhd_\beta y(\lambda x.xy)$. $\endgroup$
    – Roy
    Jul 16, 2014 at 23:48

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.