• Als Spam markieren
• Beitrag melden

• 
  Diese Gruppe Alles

• Archiv
• RSS-Feeds

• Kontakt
• Hilfe
• Impressum
• Datenschutz

mergesort mit Zusicherungen

Im Zuge einer anderen Diskussion gab's verschiedene Meinungen darüber,
wie nützlich denn Zusicherungen sind. Insbesondere, ob eine
Schleifeninvariante (im rekursiven Fall: der Induktionsschritt) für den
Programmierer überhaupt handhabbar sind.

In diesem Zusammenhang wurde ich gebeten, als einfaches Beispiel einfach
mal einen Mergesort mit entsprechenden Zusicherungen hinzuschreiben.

Genauer gesagt, muss nur gerade so viel an Zusicherungen hingeschrieben
werden, dass ein lediglich konstruktive Logik verwendendes Beweissystem
in der Lage ist, aus den Zusicherungen die Nachbedingungen der
Sortierfunktion zu beweisen.

Damit die Sache nicht zu lang wird, schreibe ich nur die Zusicherungen
für "Ergebnis ist sortiert" hin. In einem echten Mergesort müsste man
auch nachweisen, dass das Ergebnis die gleichen Elemente wie der Input
enthält (und im Fall von Dubletten sogar in der gleichen Anzahl), aber
das spar ich mir hier - man bräuchte einiges an Hilfsfunktionen für die
Zusicherungen.

Den Algorithmus habe ich aus
http://www.physik.fu-berlin.de/~aloose/static/informatik/vordiplom/sortieren.txt
geklaut, es ist in Haskell (ist die syntaktisch einfachste Sprache).
Syntaktisch ergänzt habe ich die Sprache um Vorbedingungen und
Nachbedingungen:
<Funktionsname> [<Parameterliste>] :: require <boolescher Ausdruck>
<Funktionsname> [<Parameterliste>] :: ensure <boolescher Ausdruck>
In Nachbedingungen (bei "ensure") steht der Name "result" für das
Funktionsergebnis.

Erstmal eine Hilfsfunktion:

sorted :: Ord a => [a] -> Bool
sorted [] = True
sorted [x] = True
sorted (x1:x2:xs) = (x1 <= x2) && sorted (x2:xs)

merge :: Ord a => [a] -> [a] -> [a]
merge a b :: require (sorted a) && (sorted b)
merge a b :: ensure sorted result
-- Diese beiden Zusicherungen reichen dem Inferenzsystem bereits!
merge [] [] = []
-- Nachbedingung folgt trivial aus "sorted [] = True".
merge [] ys = ys
merge xs [] = xs
-- Nachbedingung folgt trivial aus der Vorbedingung.
merge (x:xs) (y:ys)
| x <= y    = x : merge xs (y:ys)
| otherwise = y : merge (x:xs) ys
-- Für die merge-Aufrufe muss die Vorbedingung nachgewiesen werden.
-- Für die Parameter (y:ys) und (x:xs)
-- folgt sie trivial aus der Vorbedingung.
-- Für die Parameter xs und ys muss das System
--   sorted x:xs -> sorted xs
-- als Hilfsannahme beweisen. Sie folgt allerdings recht einfach
-- aus "sorted [x] = True" und
-- "sorted [x1:x2:xs] = ... && sorted [x2:xs]".
-- Das Inferenzsystem muss an dieser Stelle allerdings "schlau genug"
-- sein, "sorted (x:xs)" in "sorted (x1:x2:xs)" zu transformieren,
-- so dass der dritte Fall von "sorted" anwendbar wird. Im dümmsten Fall
-- wird es alle Transformationen stumpf durchprobieren (das gibt einen
-- Algorithmus mit O(2^N)), allerdings denke ich, dass heutzutage die
-- meisten Inferenzsysteme schlau genug sind, den Suchraum drastisch
-- einzuschränken. Meine Hoffnung (Erwartung, eigentlich) ist, dass wir
-- bei etwas landen, das die gleiche Charakteristik wie H-M hat:
-- theoretischer worst case ist O(2^N), in der Praxis eher O(N log N).
--
-- Man beachte, dass wie durch das bloße Hinschreiben von Vor- und
-- Nachbedingung der Induktionsschritt als Axiom ins System eingeführt
-- wird.
-- Das Inferenzsystem muss sich daher nicht mit vollständiger Induktion
-- abplagen, die verbleibenden Aussagen lassen sich mit
-- Prädikatenlogik der ersten Stufe behandeln. Und die wiederum ist
-- vollständig *und* entscheidbar (im Gegensatz zur Prädikatenlogik
-- der zweiten Stufe, die Aussagen enthält, für die man die vollständige
-- Induktion oder den Satz vom ausgeschlossenen Dritten über unendlich
-- große Mengen benötigt, wenn man sie beweisen will).
-- (Einschränkung: entscheidbar ist nur der Beweis zutreffender
-- Zusicherungen. Der Beweis, dass eine Zusicherung falsch ist, ist
-- unentscheidbar, außer man schränkt sich auf Funktionen mit lediglich
-- einem Parameter ein - und schon die Gleichheit hat zwei Parameter.
-- Ich glaube nicht, dass das in der Praxis ein großes Problem ist, aber
-- es ist natürlich auf jeden Fall eine ärgerliche Einschränkung.)

halb:: [a] -> Int
halb xs = div (length xs) 2

mergesort :: Ord a => [a] -> [a]
mergesort a :: ensure sorted merge a
mergesort [] = []
mergesort [x] = [x]
-- In den obigen beiden Klauseln ist die Nachbedingung trivial erfüllt.
mergesort xs
merge
(mergesort (take (halb xs) xs))
(mergesort (drop (halb xs) xs))
-- Hier muss nachgewiesen werden, dass die Vorbedingungen der
-- "merge"-Aufrufe erfüllt sind (trivial, aus der Nachbedingung
-- von "mergesort") und dass die Nachbedingung von "mergesort"
-- erfüllt ist (wiederum trivial aus der Nachbedingung von "merge").


Der eigentliche Knackpunkt ist die Klausel
merge (x:xs) (y:ys)
| x <= y    = x : merge xs (y:ys)
| otherwise = y : merge (x:xs) ys
die auch - nicht ganz zufällig, wie ich meine - der Kernpunkt des
Verfahrens ist, an dem die eigentliche Arbeit getan wird.
Ich halte es deshalb auch für vertretbar, dem Entwickler des Algorithmus
zuzumuten, an dieser Stelle notfalls ein paar extra Hinweise für den
Inferenzalgorithmus hinzuschreiben (in diesem Fall also, dass x:xs
äquivalent zu x1:x2:xs ist und dass er diese Fälle der
"sorted"-Funktion
anwenden soll). Damit hilft man nicht nur dem Inferenzalgorithmus auf
die Sprünge, sondern auch dem Programmierer, der das Ganze ein paar
Jahre später wartet und sich fragt, warum das Ganze eigentlich funktioniert.

Das ist natürlich aufwändiger als ein einfaches Abschreiben des
Algorithmus aus dem Internet - aber ich denke auch, dass man beim
Abschreiben nicht wirklich die Details versteht. (Ich hab den
Algorithmus auch erst *vollständig* verstanden, als ich die Inferenz für
den Fall "merge (x:xs) (y:ys)" nachvollziehen musste... *jetzt* bin ich
zuversichtlich, dass ich auch Variationen des Algorithmus auf
Korrektheit prüfen kann, und zwar ohne Beispielfälle im Kopf
durchzuspielen. Der Vorteil des Inferenzsystems ist, dass mir dann der
Computer bestätigen kann, dass der Algorithmus korrekt ist, ohne dass
ich alle Details verstehe.)

Zum Glück ist algorithmische Arbeit eher selten. In den allermeisten
Fällen ruft man einfach eine bestehende Sortierfunktion auf, iteriert
über eine Ergebnismenge aus der Datenbank, usw. - die Vor- und
Nachbedingungen derartiger Operationen liegen alle auf Trivialniveau.
Aber wenn Chris Okasaki etwas über funktionale Datenstrukturen schreibt,
wäre es wirklich nicht schlecht, wenn in den Algorithmen die
Schlüsselzusicherungen auch mit drinstünden.
Vielleicht sollte man sein Buch nochmal mit


Grüße,
Jo

Antworten