Konfluenz ohne Termination

• Anwendung: CR(→_β) für Lambda-Kalkül,

  Beispiel: (λy.yy)(I(λz.zz)) für I = λx.x

• Satz: Falls →₁⊆→₂⊆→₁^* und DP(→₂), dann CR(→₁).
• Beweis (TeReSe Ex. 1.3.1)

  DP(→₂)⇒DP(→₂^*) = CR(→₂), →₁^*=→₂^*, CR(→₁).

• Anwendung: s→₂t durch vollständige Reduktion
  einer Menge von markierten Redexes in s

  Markierungen werden verbraucht oder kopiert,
  neue entstehende Redexe nicht markiert

  deswegen ist →₂ wohldefiniert (es gilt SN(→₂))

• Bemerkung/Wiederholung: WCR(→) $\not\Rightarrow$CR(→)