0
$\begingroup$

Several times, I saw $\lambda$-terms such as $\lambda x. \lambda x.x$, where $x$ is bound by the inner lambda, which I agree.

why not just write it as $\lambda y. \lambda x.x$, so it is clear and you don't need to comment such as "where $x$ is bound by the inner lambda".

  1. what is the point of writing $\lambda x. \lambda x.x$, why not just write it as $\lambda y. \lambda x.x$? Usually, we don't write long lambda terms, so we have enough names to name bound variables distinctly.

  2. why not just state that "all bound variables should be given distinct names" to avoid such vague terms and explanations?

  3. is there a particular reason for having $\lambda x. \lambda x.x$?

I believe it is because of the syntax of lambda terms. I also believe banning such terms is reasonable.

$\endgroup$
3
$\begingroup$

You have basically discovered the Barendregt convention.

Yes, it's silly to write terms such as $\lambda x. \lambda x. x$ when $\lambda y. \lambda x. x$ is $\alpha$-equivalent and clearer.

We could forbid the former form the syntax of the lambda calculus. This however would force us to check $x$ does not occur bound in $M$ every time we craft (introduce) the term $\lambda x. M$.

The Barandregt convention goes further. It stipulates that, when building (introducing) a term $\lambda x. M$ we are always allowed to do that. However, when destructuring (eliminating) a term $\lambda x. M$ we can assume that $x$ was $\alpha$-converted so no to cope with other bound names in $M$, nor with other names that we could have around elsewhere at the moment: e.g., if we are writing a proof involving terms $N$ and $O$, the convention stipulates that $x$ does not occur in $N,O$ as well.

The convention is just a convenient shortcut, made for lazy humans which do not want to spend their time and energy to fix trivialities. Basically, we pretend that $\lambda x.\lambda x. M$ is allowed when it's convenient to do so (introduction), yet we pretend that the same is no longer allowed when convenient to do so (elimination). It feels a bit like cheating, but one could (in theory) always fix the proof to be perfectly sound.

$\endgroup$
3
  • $\begingroup$ I have an idea to introduce $\lambda$-terms and define substitution on them in an implementation. So I realized such vague terms ruins your strategy, therefore wanted to know if it is ok to ban such term. Now I am sure that I can just ban such terms to avoid troubles. Thank you for your answer :) $\endgroup$
    – alim
    Feb 19 '17 at 14:04
  • $\begingroup$ @alim Yes, in an implementation you can always keep those variables distinct, if you want. Watch out when you perform substitution. $\endgroup$
    – chi
    Feb 19 '17 at 14:07
  • $\begingroup$ Yes, I will be careful on substitution. I think that I found a way to correctly substitute, which is the reason for asking this question. thank you, you helped me a lot. :) $\endgroup$
    – alim
    Feb 19 '17 at 14:18

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.