Fold-Funktion


[Seminar "Einführung in Haskell"] - [Inhalt] - [zurück] - [weiter]

Ü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.

 
       foldn (+ 6) 5 4

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:
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.


[Seminar "Einführung in Haskell"] - [Inhalt] - [zurück] - [weiter] - [nach oben]