Eigenschaften unendlicher Listen

... [ Seminar "Einführung in die funktionale Programmiersprache Haskell" ] ... [ Inhaltsverzeichnis ] ... [ Zurück ] ... [ Weiter ] ...

Eigenschaften unendlicher Listen

Leider reicht das Prinzip der Induktion nicht immer aus, um jede Eigenschaft von unendlichen Listen zu beweisen. Diese Tatsache soll im folgenden Beispiel anhand der Funktion iterate näher betrachtet werden.

iterate  :: (α -> α) -> α -> [α]
iterate f x = x : iterate f (f x)

Die Funktion iterate liefert als Rückgabewert eine unendliche Liste. Die Funktionsdefinition soll durch folgende Gleichung ersetzt werden:

iterate f x = x : map f (iterate f x)

Im Folgenden soll nun bewiesen werden, dass die neue Definition von iterate das gleiche Ergebnis liefert. Es muss also überprüft werde, ob die beiden unenendlichen Listen gleich sind. Allerdings kann diese Behauptung hier nicht mit Hilfe der der Induktion bewiesen werden, da kein geeignetes Argument zur Anwendung des Induktionsbeweises zur Verfügung steht.
Wie könnten sonst solche Resultate überprüft werden?
Eine Möglichkeit wäre die Prüfung der Gleichheit aller Elemente an den entsprechenden Positionen der Listen. Um es anders auszudrücken, die Gleicheit zweier unendlicher Listen xs und ys könnte dadurch bewiesen werden, dass die Elemente der Listen an den gleichen Indizes identisch sind. Das heisst, es gilt:

xs !! n = ys !! n

für alle natürlichen Zahlen n

Leider ist diese Annahme falsch. Dies wird bei der Betrachtung der beiden Listen xs = ⊥ und ys = [⊥] deutlich. Diese beiden Listen sind unterschiedlich, liefern beim Indizieren mit natürlichen Zahlen jedoch das gleiche Ergebnis und zwar das undefinierte Element ⊥.

Eine zweite Möglichkeit liefert uns die im vorherigen Kapitel definierte Funktion approx. Für diese Funktion gilt:

lim n→∞ approx n xs = xs für alle Listen xs.

Hieraus folgt, dass im Falle

approx  n xs = approx n ys
für alle n 

auch xs = ys gilt.

Es kann also die Eigenschaft xs ⊆ ys dadurch bewiesen werden, dass gezeigt wird, dass

approx n xs ⊆ approx n ys für alle n gilt.

Unter Anwendung dieser Idee auf die Definition von iterate kann folgende Gleichung definiert werden:

iterate f (f x) = map f (iterate f x)

Unter Nutzung der Approximationsfunktion approx kann nun mit Hilfe der vollständigen Induktion die obige Gleichung bewiesen werden.

Beweis:

approx n (iterate f (f x)) = approx n (map f (iterate f x))

soll durch Induktion über n bewiesen werden.

Fall (0) : 
Es gilt: approx 0 xs = ⊥ für alle Listen xs 

Fall (n + 1):
linke Seite:
  approx (n +1) (iterate f (f x))
= {Definition von iterate}
  approx (n + 1) (f x : iterate f (f (f x)))
= {Definition von approx}
  f x : approx n (iterate f (f (f x)))
= {Induktionshypothese}
  f x : approx n (map f (iterate f (f x)))

rechte Seite: 
  approx (n + 1) (map f (iterate f x))
= {Definition von iterate}
  approx (n + 1) (map f (x : iterate f (f x)))
= {Definition von map}
  approx (n + 1) (f x : map f ( iterate f (f x)))
= {Definition von approx}
  f x : approx n (map f (iterate f (f x)))

=> beide Seiten liefern das gleiche Ergebnis, womit der Beweis erbracht ist!

... [ Seminar "Einführung in die funktionale Programmiersprache Haskell" ] ... [ Inhaltsverzeichnis ] ... [ Zurück ] ... [ Weiter ] ...