Fixpunkt-Kombinatoren

• Definition: Y : = λf.((λx.f (xx))(λx.f (xx)))
• Satz: Yf ist Fixpunkt von f
• d.h. Y ist Fixpunkt-Kombinator
• Beweis: vergleiche (Yf ) und f (Yf )
• Folgerung: rec wird eigentlich nicht benötigt

wir benutzen eine Variante des Y:

Y' = λf.(λx.f (λy.xxy))(λx.f (λy.xxy))),

weil sonst die Aufrufe (xx) nicht halten würden.

Ü: weitere Fixpunktkombinatoren, Θ = (λxy.(y(xxy)))(λxy.(y(xxy)))