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