0
$\begingroup$

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.

1 Answers 1

3

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.

  • 0
    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?2012-06-15
  • 0
    @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."2012-06-15
  • 0
    ...(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).2012-06-15