Eigenschaften der Reduktion

→ auf Λ ist

• konfluent

  ∀A, B, C∈Λ : A→_β^*B∧A→_β^*C⇒∃D∈Λ : B→_β^*D∧C→_β^*D

• (Folgerung: jeder Term hat höchstens eine Normalform)
• aber nicht terminierend (es gibt Terme mit unendlichen Ableitungen)

  W = λx.xx, Ω = WW.

• es gibt Terme mit Normalform und unendlichen Ableitungen, KIΩ mit K = λxy.x, I = λx.x