2
$\begingroup$

In lambda calculus, starting from $KII$ we can get by a single $\beta$-reduction to either

$\lambda y.II$

or $KI$

Now, according to Church-Rosser, these should be reducing into a common normal form. But the first reduces to $I$ and the second to $\lambda y.\lambda z.z$.

Am I doing wrong $\beta$-reductions or the theorem holds only on some condition? I do not see a common reduct here.

|cite|improve this question
$\endgroup$
  • 1
    $\begingroup$ (1) You are missing parens in the first term: $(\lambda y. I)I$. (2) How did you get the second term? Remember, $KII$ is syntactic sugar for $(KI)I$. It seems that you did a reduction step as if it was $K(II)$. $\endgroup$ – Anton Trunov Nov 29 '16 at 13:20
  • $\begingroup$ @AntonTrunov and it was indeed K(II) in the book, a momentary lapse of attention. $\endgroup$ – Gergely Dec 13 '16 at 9:19
3
$\begingroup$

Remember that $1)$ application is left associative and $2)$ application has higher precedence than abstraction. This is:

$1)$ $ A B C = (A B) C \neq A (B C)$
$2)$ $ \lambda x. A B = \lambda x. (A B) \neq (\lambda x. A) B$

So

$KII = (KI)I = ((\lambda x y. x) I) I = (\lambda y. I) I = I$

|cite|improve this answer
$\endgroup$
  • $\begingroup$ sorry my remark was wrong $\endgroup$ – Gergely Nov 30 '17 at 8:38

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.