Fold-Funktion
Übersicht
Fold
fold ist eine der mächtigsten Funktionen in Haskell, teilweise aber auch schwer zu verstehen.
Vereinfachend gesagt erhält fold eine Funktion, die dann zwischen den Elementen angewandt
(gefaltet) wird.
Viele der bisher vorgestellten rekursiven Definitionen haben einen sehr ähnlichen Aufbau, dargestellt an der
folgenden Definition für eine allgemeine rekursive Funktion f:
f :: Nat -> A
f Zero = c
f (Succ n) = h(f n)
|
Hier steht A für einen bestimmten Typen und c ist eine Konstante aus A. h ist dabei
eine Typdeklaration h :: A -> A. Zu beachten ist, dass f ein Element aus Nat hernimmt und
Zero durch c ersetzt, ebenso wie Succ durch h.
Folgendes Beispiel verdeutlicht dies:
Succ(Succ(Succ Zero)) wird zu h(h(h c))
|
Die zwei Gleichungen für f können nun in den Termen einer einzigen Funktion foldn
untergebracht werden, der sogenannten fold-Funktion für Nat.
Die Definition für foldn:
foldn :: (α -> α) -> α -> Nat -> α
foldn h c Zero = c
foldn h c (Succ n) = h(foldn h c n)
|
Zur Veranschaulichung wird an dieser Stelle ein Beispiel gegeben, das mit dem
hier
enthaltenen Code weiter getestet werden kann. Das + ist dabei nur eine frei gewählte Möglichkeit und kann
durch andere Funktionen, wie z.B. * ersetzt werden.
Als einzelne Rechenschritte ergeben sich daraus veranschaulicht:
4. 6 +
3. 6 +
2. 6 +
1. 6 +
0. 5
= 29
|
Im einzelnen ergibt sich:
m + n = foldn Succ m n
m * n = foldn (+m) Zero n
m ^ n = foldn (*m) (Succ Zero) n
|
Daraus folgt, dass auch für die Identitäts-Funktion id auf Nat id = foldn Succ Zero gilt.
Eine passende fold-Funktion kann zu jedem rekursiven Datentypen definiert werden. In anderen Ausarbeitungen (z.B. Kapitel "Listen") werden
weitere folgen.
In den obigen Beispielen gibt jede Instanz von foldn auch ein Element aus Nat zurück. In den folgenden zwei bekannten Beispielen gibt
foldn nun ein Element der Form (Nat, Nat) zurück:
fact :: Nat -> Nat
fact = snd · foldn f(Zero, Succ Zero)
where f(m, n) = (Succ m, Succ m * n)
fib :: Nat -> Nat
fib = fst · foldn g(Zero, Succ Zero)
where g(m, n) = (n, m + n)
|
Die Funktion fact berechnet die Fakultät und fib die Fibonacci-Funktion. Jedes der beiden Programme berechnet erst ein
allgemeineres Ergebnis als Element (Nat, Nat) und extrahiert dann das erwartete Ergebnis.
foldn f(Zero, Succ Zero) n = (n, fact n)
foldn g(Zero, Succ Zero) n = (fib n, fib(Succ n))
|
Diese Gleichungen können per Induktion geprüft werden. Das Programm für fib ist effizienter
als eine direkte rekursive Definition. Das rekursive Programm würde eine exponentielle Anzahl an (+)-Operationen
benötigen, während das obige nur eine lineare Anzahl benötigt. Aber Effizienz soll nicht
Gegenstand dieser Ausarbeitung sein, sondern wird später im Kapitel 7 behandelt. Dort wird auch auf die
Programmiertechniken eingegangen werden, die zu diesen obigen neuen Programmen führen.
Es gibt zwei Vorteile, rekursive Definitionen als
foldn zu schreiben:
- Erstens wird die Definition kürzer, da nur noch eine Gleichung geschrieben werden muss statt vorher zwei
und
- zweitens ist es möglich, generelle Eigenschaften von foldn zu prüfen und sie für den
Beweis von spezifischen Fällen zu nutzen.
Mit anderen Worten ist es so einfacher, da nur ein Beweis geführt werden muss statt zwei oder mehr.
[nach oben]
Fusion
Die Fusion wird auch als Verschmelzung bezeichnet und gehört zum Bereich der fold-Funktion. Um die Fusion
besser darstellen zu können, soll der folgende Fusionssatz für Nat durch Induktion bewiesen werden.
Es lässt sich festellen, dass...
f · foldn g a = foldn h b
|
... unter bestimmten Umständen für die enthaltenen Variablen gilt. Dieser Satz wird als
Fusionssatz bezeichnet, da die Berechnung von f mit der Berechnung von foldn g a verschmilzt.
Fusionssätze können zu einem bemerkenswerten Effizienzanstieg führen. Statt erst das eine Element
eines Datentypen zu bearbeiten und dann nochmals das Ergebnis, ist es durch Fusion teilweise möglich,
die beiden Bearbeitungsschritte in einem zu kombinieren.
Statt über die Annahmen zu diskutieren, die eine Fusion ermöglichen, wird anhand des obigen Beispiels durch vollständigen
Induktions-Beweis verdeutlicht, worum es geht. Die Annahmen werden also im Folgenden mit abgeleitet.
Beweis: Es wird f(foldn g a n) = foldn h b n durch vollständige Induktion auf n geprüft.
Fall 1 (
): Für die linke Seite ergibt sich:
f(foldn g a )
= {case exhaustion in der Definition von foldn}
f
|
Für die rechte Seite ergibt sich nun:
foldn h b
= {case exhaustion in der Definition von foldn}
|
Diese beiden Ergebnisse müssen gleich sein und hiermit ergibt sich die erste Bedingung, nämlich das f eine strikte Funktion ist.
Fall 2 (Zero): Für die linke Seite ergibt sich:
f(foldn g a Zero)
= {1. Gleichung für foldn}
f a
|
Für die rechte Seite ergibt sich nun:
foldn h b Zero
= {1. Gleichung für foldn}
b
|
Diese beiden Ergebnisse müssen ebenfalls gleich sein und hiermit ergibt sich die zweite Bedingung, nämlich das f a = b.
Fall 3 (Succ n): Für die linke Seite ergibt sich:
f(foldn g a (Succ n))
= {2. Gleichung für foldn}
f (g(foldn g a n))
|
Für die rechte Seite ergibt sich nun:
foldn h b (Succ n)
= {2. Gleichung für foldn}
h(foldn h b(Succ n))
= {Induktionshypothese}
h(f(foldn g a n))
|
Da diese beiden Ergebnisse ebenfalls gleich sein müssen, ergibt sich hiermit f · g = h · f.
Zusammenfassend kann gesagt werden, dass eine Gleichung für unendliche Zahlen gilt, wenn sie für
partielle Zahlen gilt. Es wurde ebenso das Fusionstheorem für foldn gezeigt, also wenn
f strikt, f a = b und f · g = h · f ist, dann gilt:
f · foldn g a = foldn h b
|
[nach oben]
Beispiele
Hier soll anhand des oben genannten Theorems der Fusion bewiesen werden, dass Zero links-assoziativ bzgl. (+) ist. Oder symbolisch, dass
Zero + n = n für alle Zahlen n gilt. Da n = foldn Succ Zero n ist, besteht nun die Notwendigkeit zu prüfen, dass:
(Zero +) · foldn Succ Zero = foldn Succ Zero
|
Wird das Theorem der Fusion berücksichtigt gilt die obige Gleichung, wenn ebenso gilt:
Zero + =
Zero + Zero = Zero
Zero + Succ n = Succ(Zero + n)
|
Alle drei Gleichungen sind unmittelbar von der (+)-Definition abhängig.
Als zweites Beispiel wird gezeigt, dass Succ Zero links-assoziativ bzgl. (*) ist.
Um die Fusion wieder zu berücksichtigen, müssen drei Fälle untersucht werden:
Succ Zero * =
Succ Zero * Zero = Zero
Succ Zero * Succ n = Succ(Succ Zero * n)
|
Die ersten beiden sind dabei unmittelbar abhängig von der (*)-Definition. Die dritte Gleichung muss weiter untersucht werden und es ergibt sich:
Succ Zero * Succ n
= {Definition (*)}
(Succ Zero * n) + Succ Zero
= {Definition (+)}
Succ((Succ Zero * n) + Zero)
= {Definition (+)}
Succ(Succ Zero * n)
|
Keines der beiden Ergebnisse wurde explizit durch Induktion überprüft. Die einzige Benutzung der Induktion
lag im Beweis des Verschmelzungstheorems.