1unitedpower: Frage zum Wiki-Artikel „Links richtig gestalten“

Beitrag lesen

problematische Seite

„Um Rekursion zu verstehen, muss man zunächst Rekursion verstehen.” —Cheatah

„Um Rekursion zu verstehen, muss man zunächst Fixpunkte verstehen.” — Ich

„Y?” — Gunnar

„Y-Combinator” — Church

Und jetzt mal anschaulich am Standardbeispiel:

fac (x) = if (x === 0)
   then 1
   else x * fac (x - 1)

Intuitiv haben wir ein gutes Verständnis für solche rekursiven Definitionen. In der konstruktiven Mathematik wäre das aber unzulässig, weil der zu definierende Term (fac) auf der rechten Seite wieder auftraucht.

Wir suchen stattdessen nach eine Lösung für das Gleichungssystem:

fac (x) == if (x === 0)
   then 1
   else x * fac (x - 1)

Und jetzt kommt der etwas verwirrende Part: Wir suchen nicht nach Lösungen für x, sondern nach Lösungen für die freie Variable fac. Mit etwas Mühe macht das auch Sinn, denn wir wollen am Ende schließlich eine Funktion von den natürlichen Zahlen in die natürlichen Zahlen haben.

Zufälligerweise ist die Lösung für dieses Gleichungssystem aber auch der Fixpunkt der folgenden Funktion f:

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

Mit \x -> ... führe ich eine anonyme Funktion ein - also einen Closure. f ist demnach eine Funktion höherer Ordnung: Sie bekommt als Parameter eine Funktion und gibt auch eine Funktion zurück. Der Fixpunkt von f ist also ebenfalls eine Funktion - und nicht irgendeine, sondern genau unsere gesuchte Fakultätsfunktion. Noch eine kleine Umbenennung um Missverständnisse zu vermeiden…

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

… und wir können endlich fac als Fixpunkt von f definieren:

fac = fix(f)

Die ganze Herleitung findet man zum Beispiel in Semantics Engineering with PLT Redex