Чтобы доказать, что SKK и II бета-эквивалент, лямбда-исчисление

Question

Я новичок в лямбда-исчислении и пытаюсь доказать следующее.

SKK и II являются бета-эквивалентом.

где

S = лямбда xyz.xz(yz) K = лямбда xy.x I = лямбда xx

Я пытался уменьшить SKK, открыв его, но ничего не получилось, он стал грязным. Не думайте, что SKK можно уменьшить без расширения S, K.

Answer 1

  SKK
= (λxyz.xz(yz))KK
→ λz.Kz(Kz)        (in two steps actually, for the two parameters)

  Kz
= (λxy.x)z
→ λy.z

  λz.Kz(Kz)
→ λz.(λy.z)(λy.z)  (again, several steps)
→ λz.z
= I

(Вы должны быть в состоянии доказать, что II → I)

Answer 2

Другой подход с меньшим количеством шагов, сначала уменьшите SK до λyz.z;

SKK
= (λxyz.xz(yz))KK
→ λyz.Kz(yz) K
→ λyz.(λxy.x)z(yz) K
→ λyz.(λy.z)(yz) K
→ λyz.z K
→ λz.z
= I