Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

Have a problem proving K MN=M

  1. By the K combinator definition

    $ (\lambda x y.x) M N $

  2. Parenthesized

    $ ((\lambda x. (\lambda y.x)) M) N $

  3. By the principal axiom of lambda calculus

    $ (\lambda y.M) N $

  4. Second application of the principal axiom

    $ M[y:= N] $ ?

This would give correct result if M is y-free. Apparently there is an error at one of the steps.

share|cite|improve this question
up vote 3 down vote accepted

When you reduce $(\lambda x.\lambda y.x)M$, the result is $(\lambda y.x)[x:= M]$. This substitution is only defined if$y$ is not free in $M$. Otherwise the $\lambda y$ will need to be $\alpha$-renamed before you can proceed.

Some texts define the substitution function to do this $\alpha$-renaming implicitly, others consider the result of the substitution to be undefined if the variable capture condition is not met.

share|cite|improve this answer
Does it mean the proof has to do case analysis: if y is free in M we follow this path; otherwise, rename y to something else and proceed in similar venue. Is there a proof without branching? – Tegiri Nenashi Jun 15 '12 at 19:29
@TegiriNenashi: The most convenient way to proceed would be, because you're free to $\alpha$-convert at any time, to start by saying: "Choosen an $\alpha$-renaming of $\lambda xy.x$ such the each variable becomes something that is neither free in $M$ nor in $N$; in the following, assume that the letters $x$ and $y$ stand for whichever such "safe" variable names we choose." – Henning Makholm Jun 15 '12 at 20:07
...(continued) Often the lambda calculus is defined such the real name of variables in the calculus is always something ugly such as $X''''''''$, and the meaning of the "$x$"s that appear on the page in actual proofs is always a meta-variable that ranges over the ugly "real" variable names. (Another somewhat popular convention is that calculus-level variable names are in typewriter-style like x, and things in mathematics fonts like $x$ are always metavariables that range over variable names). – Henning Makholm Jun 15 '12 at 20:09

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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