Fixpunkt-Kombinatoren

• Definition: Θ = (λxy.(y(xxy)))(λxy.(y(xxy))) mathend000#

• Satz: Θf→_βf (Θf ) mathend000#, d. h. Θf mathend000# ist Fixpunkt von f mathend000#
• d.h. Θ mathend000# ist Fixpunkt-Kombinator, (T wegen Turing)

• Folgerung: im Lambda-Kalkül kann man beliebige Wiederholung (Schachtelung) von Rechnungen beschreiben

Anwendung:

f = \ g x -> if x==0 then 1 else x * g(x-1)

Beispiel: f (λz.z)7 = 7⋅(λz.z)6 = 7⋅6 mathend000#, f (λz.z)0 = 1 mathend000#;

Θf7→_β^*7⋅(f (Θf )6)→_β^*7⋅(6⋅(f (Θf )5))→_β^*... mathend000#