1
$\begingroup$

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?
$\endgroup$
4
$\begingroup$
  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.

$\endgroup$
  • $\begingroup$ "...the most strictest sense..." - double superlative $\endgroup$ – d'alar'cop Jul 16 '14 at 22:27
  • $\begingroup$ @d'alar'cop: oops, that slipped in. Thanks. $\endgroup$ – Roy O. Jul 16 '14 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 '14 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 O. Jul 16 '14 at 23:48

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.