Verifikation von ML-Programmen mit dem

Beweisprüfer Lego

Diplomarbeit im Fach Informatik

Martin Hofmann-Fischer

geboren am 9. November 1965 in Erlangen

Lehrstuhl für Informatik VII Rechnerarchitektur und -Verkehrstheorie

Institut für Mathematische Maschinen und Datenverarbeitung Friedrich-Alexander-Universität Erlangen-Nürnberg

Betreuer: Dr. Terry Stroup und Norbert Götz

Beginn: 8. Februar 1991 Abgabe: 7. August 1991

Ich versichere, daß ich diese Arbeit ohne fremde Hilfe und ohne Benutzung anderer als der angegebenen Quellen angefertigt habe und daß die Arbeit in gleicher oder ähnlicher Form noch keiner anderen Prüfungsbehörde vorgelegen hat und von dieser als Teil einer Prüfungsleistung angenommen wurde. Alle Ausführungen, die wörtlich oder sinngemäß übernommen wurden, sind als solche gekennzeichnet.

Erlangen, den 7. August 1991

Vorwort

Neuere Forschungsarbeiten haben gezeigt, daß sich intuitionistische Typentheorie zur modularen Spezifikation und Verifikation funktionaler Programme einsetzen läßt. Aufgrund der Analogie zwischen logischen Sätzen und Typen wird eine Spezifikation in diesem Ansatz als Typ aufgefaßt; Vertreter dieses Typs sind dann verifizierte Programme; die modulare Zerlegung von Spezifikationen entspricht dabei dem modus ponens. In den letzten Jahren sind Implementationen intuitionistischer Typenkalküle entstanden (LEGO), die sich zur maschinenunterstützten Verifikation von Programmen eignen.

In der vorliegenden Arbeit wird diese Vorgehensweise am Beispiel der funktionalen Programmiersprache ML (Meta-Language) praktisch durchgeführt. Es werden die Konstrukte von ML typentheoretisch interpretiert und darauf aufbauend eine Umgebung geschaffen, die eine interaktive Verifikation von ML-Programmen am Rechner erlaubt. An einem größeren Beispiel wurde die Methode praktisch erprobt.

Danksagung

Hiermit bedanke ich mich bei meinen Betreuern Dr. Terry Stroup und Norbert Götz für die Hinführung zu dieser interessanten Aufgabe und für die aufmunternde Unterstützung vor allem in der Anfangsphase der Arbeit. Des weiteren möchte ich mich bedanken bei allen Mitgliedern des Dienstagsclubs und bei Thorsten Altenkirch für zahlreiche fachliche Diskussionen und kritische Kommentare zu Vorabversionen von Teilen dieser Arbeit. Mein besonderer Dank gilt meinen beiden Eltern, für ihre sorgfältige Korrekturlesearbeit. ii

Inhalt

1 Einleitung 1

2 Grundlagen 7 2.1 Funktionale Programmiersprachen . . . . . . . . . . . . . . . . . . . . 7 2.2 Datentypen als T –Algebren . . . . . . . . . . . . . . . . . . . . . . . 9

2.2.1 Definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2.2.2 Parametrische T –Algebren . . . . . . . . . . . . . . . . . . . . 12 2.2.3 Iteration . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.2.4 Primitive Rekursion . . . . . . . . . . . . . . . . . . . . . . . 14 2.2.5 Induktion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 2.2.6 Das datatype–Konstrukt von ML . . . . . . . . . . . . . . . . 20

2.2.6.1 Pattern–matching und primitive Rekursion . . . . . . 20 2.2.6.2 Polymorphe ML-Datentypen . . . . . . . . . . . . . . 21

2.3 Modularisierung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 2.3.1 Das Modulkonzept von ML . . . . . . . . . . . . . . . . . . . 23 2.3.2 Typentheoretische Verifikation . . . . . . . . . . . . . . . . . . 23 2.3.3 Sharing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25

3 Lego–Interpretationen 29

3.1 T –Algebren in Lego . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

3.1.1 Darstellung von Kategorien . . . . . . . . . . . . . . . . . . . 29 3.1.1.1 Kategorienaxiome . . . . . . . . . . . . . . . . . . . 30 3.1.1.2 Kommutative Quadrate . . . . . . . . . . . . . . . . 30 3.1.1.3 Terminales und initiales Objekt . . . . . . . . . . . . 31 3.1.1.4 Produkt und Coprodukt . . . . . . . . . . . . . . . . 32 3.1.1.5 Exponentenobjekte . . . . . . . . . . . . . . . . . . . 34

3.1.2 Darstellung von Funktoren . . . . . . . . . . . . . . . . . . . . 34 3.1.3 T –Algebren nach Church und Wraith . . . . . . . . . . . . . . 35

3.1.3.1 Einführung . . . . . . . . . . . . . . . . . . . . . . . 36 3.1.3.2 Church–Datentypen . . . . . . . . . . . . . . . . . . 36 3.1.3.3 Initialität . . . . . . . . . . . . . . . . . . . . . . . . 38

3.1.4 Primitive Rekursion . . . . . . . . . . . . . . . . . . . . . . . 40 3.1.5 Induktion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40

3.1.5.1 Initiale T -Algebren durch kleine Σ-Typen . . . . . . 42

3.2 Wahrheitswerte, Gleichheit und Fallunterscheidung . . . . . . . . . . 43 3.2.1 Wahrheitswerte . . . . . . . . . . . . . . . . . . . . . . . . . . 43 3.2.2 Gleichheit . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 3.2.3 Lemmata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47

3.3 Natürliche Zahlen und allgemeine Rekursion . . . . . . . . . . . . . . 48

3.3.1 Allgemeine Rekursion . . . . . . . . . . . . . . . . . . . . . . . 49 3.3.1.1 Verallgemeinerung auf mehrfache Zugriffe . . . . . . 51 3.3.1.2 Induktionsprinzipien . . . . . . . . . . . . . . . . . . 52 3.3.1.3 Wertung . . . . . . . . . . . . . . . . . . . . . . . . . 54 3.3.1.4 Verallgemeinerung auf Ordinale . . . . . . . . . . . . 54 3.3.1.5 Lego und Partialität . . . . . . . . . . . . . . . . . . 54

3.4 Zusammenfassung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55

4 Ein Beispiel 57 4.1 Ausgangsspezifikation . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 4.2 Implementierung von change attrib . . . . . . . . . . . . . . . . . . 60

4.2.1 Implementierung des Funktors ChangeAttrib . . . . . . . . . 61 4.2.1.1 Lego-Darstellung von ChangeAttrib: . . . . . . . . . 61 4.2.1.2 Verifikation von ChangeAttrib . . . . . . . . . . . . 62

4.3 Implementierung von Symtab' als Termalgebra . . . . . . . . . . . . . 63 4.3.1 Lego-Darstellung von Symtab' . . . . . . . . . . . . . . . . . . 64 4.3.2 Verifikation von Symtab' . . . . . . . . . . . . . . . . . . . . . 65

4.3.2.1 Implementierung des datatypes . . . . . . . . . . . . 66

4.4 Wiederholungsfreie Listen . . . . . . . . . . . . . . . . . . . . . . . . 67

4.4.1 Zerlegung in Symtab'' und SeqPairs . . . . . . . . . . . . . . 67

4.4.1.1 Lego-Darstellung . . . . . . . . . . . . . . . . . . . . 68 4.4.2 Zerlegung in Symtab''' und SeqDup . . . . . . . . . . . . . . 69 4.4.3 Implementierung des Funktors Symtab''' . . . . . . . . . . . 72

4.4.3.1 Implementierung von symtab . . . . . . . . . . . . . 73 4.4.3.2 Verifikation der Funktionen present und add …. 76 4.4.3.3 Verifikation von lookup . . . . . . . . . . . . . . . . 77 4.4.3.4 Implementierung von SeqDup . . . . . . . . . . . . . 78

5 Schlußbetrachtung 79 5.1 Zusammenfassung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 5.2 Einordnung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 5.3 Ausblick und Anregungen zu weiterführender Arbeit . . . . . . . . . . 80

5.3.1 Abstrakte Datentypen . . . . . . . . . . . . . . . . . . . . . . 80 5.3.2 Imperative Strukturen . . . . . . . . . . . . . . . . . . . . . . 80 5.3.3 Partialität . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80 5.3.4 Komplexität . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81 5.3.5 Parallele Konstrukte und Nebenläufigkeit . . . . . . . . . . . . 81 5.3.6 PER-Semantik funktionaler Programmiersprachen . . . . . . . 81

5.4 Wertung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82

Kapitel 1

Einleitung

Ausgehend von der Beobachtung, daß große Programmsysteme grundsätzlich fehlerbehaftet sind und daß die (nicht erschöpfende) Suche nach diesen Fehlern oftmals mehr Zeit als die eigentliche Programmentwicklung beansprucht, entsteht der Wunsch nach einer formalen, glaubhaften und zumindest teilweise maschinenunterstützten und –überprüften Verifikation von Programmen, insbesondere in sicherheitskritischen und schwer zu durchschauenden Bereichen. Unter Verifikation versteht man in diesem Zusammenhang einen mathematischen Beweis, daß das Programm korrekt ist.

Mit Verifikation untrennbar verbunden ist daher stets die genaue und formale Spezifikation der Anforderungen, die an ein Programm gestellt werden. (Ein mathematischer Beweis, daß ein vorgelegtes Programm ”ein Betriebssystem ist“, ist schwer vorstellbar.) Dies setzt ein formales System zur Formulierung logischer Sätze (Spezifikationen) und zur Notation und Herleitung formaler Beweise dieser Sätze voraus. Aufgrund der konstruktiven Natur von Programmen bietet sich für diese Beweise intuitionistische Logik an. Außerdem muß die verwendete Programmiersprache eine adäquate und zugängliche Beschreibung durch logische Sätze gestatten. Schließlich ist für erfolgreiche Spezifikation und Verifikation die Möglichkeit zu logisch konsistenter Zerlegung (Modularisierung) sowohl der Programme als auch der Verifikationsbeweise in handhabbare und sinnzusammenhängende Teile erforderlich. Ein System, welches maschinenunterstützte Spezifikation, Verifikation und Implementation ermöglichen soll, muß diesen Anforderungen gerecht werden.

Die programmiersprachlichen Teile dieser Forderungen werden in besonders guter Weise durch typisierte modulare funktionale Programmiersprachen, wie ML [HMM87] oder Hope [BMS80] realisiert. Dieser Arbeit liegt nun die — u.a. in [Luo91, Str89, Hue88, NPS90] geteilte — Auffassung zugrunde, daß diese Sprachen am besten durch intuitionistische typentheoretische Systeme zu beschreiben sind. Sie sollen im folgenden kurz beschrieben werden.

Typentheoretische Spezifikation und Verifikation baut auf der auf Heyting [Hey56] zurückgehenden Sichtweise intuitionistischer Beweise als Konstruktionen auf. Am augenfälligsten wird diese Idee an Heytings Interpretation der (intuitionistischen) Implikation: Ein Beweis des Satzes P → Q soll ein konstruktives Verfahren sein, welches (hypothetische) Beweise des Satzes P in solche von Q überführt und nicht eine Argumentation, die aus der Wahrheit von P und dem gleichzeitigen Nichtzutreffen von Q auf einen Widerspruch schließt. Ähnlich verhält es sich bei der intuitionistischen Interpretation der Allquantifizierung (ein Beweis von ∀x ∈ A.B(x) ist ein Verfahren, das aus beliebig vorgegebenen Elementen x von A Beweise für B(x) bestimmt) oder bei der Konjunktion (ein Beweis von P ∧ Q ist ein Paar (p, q), wobei p ein Beweis für P und q ein solcher für Q ist). Ordnet man nun jedem Satz P die Menge (den Typ) Proof (P) seiner Beweise zu, so ist

Proof (P → Q) = Proof (Q)^{Proof (P)}

Proof (P ∧ Q) = Proof (P) × Proof (Q)

Proof (∀x ∈ X.B(x)) = ∏_{x∈A} Proof (B(x)) .

Der Typ der Beweise einer Implikation ist also der Exponententyp (Funktionstyp) der Beweistypen der beiden Implikanden; der Typ der Beweise von Konjunktion und Allquantifizierung ist ein cartesisches Produkt bzw. ein indiziertes Produkt. In ähnlicher Weise lassen sich auch die anderen prädikatenlogischen Konnektive und auch Konstrukte aus höherer Logik (Leibniz–Gleichheit) interpretieren. Diese semantische und formale^{1} Analogie von Sätzen und (gewissen) Typen ist als propositions as types–Paradigma oder Curry–Howard–Isomorphismus [Coq85a] bekannt. Man kann diese Analogie noch weiter treiben und einen logischen Satz mit dem Typ seiner Beweise identifizieren; dies entspricht auch der (intuitionistischen) Auffassung, daß die Extension eines logischen Satzes nicht sein Wahrheitsgehalt, sondern seine potentielle Beweisbarkeit ist. In diesem Sinne sind Sätze spezielle Typen; das Beweisen von Sätzen wird zum Aufsuchen von Objekten eines gewissen Typs. Der Ausdruck a:A steht dann sowohl für ”a ist ein Objekt (Programm) vom Typ A“, als auch für ”a ist ein Beweis von A“. Damit entspricht das Überprüfen von Beweisen der aus funktionalen Programmiersprachen bekannten Typüberprüfung und läßt sich mit ähnlichen Algorithmen bewerkstelligen.

Dies liefert eine gemeinsame und unifizierte Darstellung von Implementation und Verifikation, bzw. von Typinformation und (logischer) Spezifikation: Eine Spezifikation kann man als sogenannten Σ–Typ (indizierte disjunkte Vereinigung) Σt:τ.σ(t) auffassen, wobei τ den Typ des spezifizierten Programms (man denke an τ = input type → output type)^{2} und σ ein als logischer Satz aufgefaßter Typ ist, der das Programm spezifiziert. Ein Objekt des Σ–Typs Σt:τ.σ(t) ist dann ein Paar (t, s), wobei t ein Objekt des Typs τ, also etwa eine Funktion mit dem gewünschten Ein–/Ausgabetyp und s als Objekt (Beweis) von σ(t) eine formale Verifikation von t darstellt.

Implementation und Verifikation werden in der Typentheorie deshalb unter der Aufgabe des Auffindens von Objekten eines gewissen Typs subsumiert. Ein Beispiel soll dies verdeutlichen: Wir betrachten den Typ list der Listen. Sei sorting (f)ein Satz (Typ), der die Eigenschaft, daß f : list → list eine Sortierfunktion ist, zum Ausdruck bringt. Eine Spezifikation eines Sortieralgorithmus ist dann durch Σf:list → list.sorting (f) gegeben. Ein Objekt dieses Typs besteht aus einer Funktion f des Typs list → list und einem Beweis, daß f eine Sortierfunktion ist. Solch ein Objekt bezeichnen wir als verifizierte Implementierung der Spezifikation.

1Die Analogie ist auch formaler Natur: Der Ausdruck λp:P.λq:Q.p kann sowohl als Beweis der Tautologie P → Q → P, als auch als Projektion auf das erste Argument gedeutet werden.

2Selbstverständlich lassen sich unter Verwendung cartesischer Produkte auch Signaturen mit mehr als einer Funktion als Typ darstellen.

Parametrisierte Spezifikationen und (den ML–Funktoren vergleichbare) Modulkonstrukte lassen sich in diesem Ansatz als Typen der Form S_{1} → S_{2} darstellen, wobei S_{1} = Σt:τ_{1}.σ_{1}(t) und S_{2} = Σt:τ_{2}.σ_{2}(t) Spezifikationen sind. Objekte eines solchen Typs sind Funktionen, die aus einer Implementierung des Typs τ_{1} eine solche vom Typ τ_{2} bestimmen und gleichzeitig aus einem Korrektheitsbeweis für τ_{1} einen solchen für τ_{2} bestimmen. Dies ermöglicht es, die Aufgabe der verifizierten Implementierung von S_{2} (also das Auffinden eines Objekts dieses Typs) zu zerlegen in die Aufgabe, ein Objekt von S_{1} → S_{2} zu bestimmen — dies kann man als partielle (verifizierte) Implementierung von S_{2} deuten — und die Aufgabe, einen Vertreter von S_{1} zu ermitteln; das entspricht der verifizierten Implementierung der vorher als bereits realisiert angenommenen Spezifikation S_{1}. Durch einfache Applikation erhält man dann eine verifizierte Implementierung der Spezifikation S_{2}.^{3} Genaueres zu dieser Vorgehensweise findet sich im Abschnitt 2.3.

Ein weiterer wichtiger Gesichtspunkt typentheoretischer Programmierung ist die als Imprädikativität bezeichnete Möglichkeit, über alle Typen eines gewissen Universums zu quantifizieren, ohne dieses dabei zu verlassen. Dies ermöglicht Ausdrücke, wie ∀P.P → P, was logisch gesehen die Tautologie P → P für alle Sätze P und auf der Typebene den Typ der polymorphen Identität, welche — mit beliebigen Typen instantiiert — die entsprechende (monomorphe) Identitätsfunktion liefert. Man beachte, daß die polymorphe Identität auch auf ihren eigenen Typ angewandt werden kann.

Imprädikativität ermöglicht einerseits die typentheoretische Modellierung sogenannter polymorpher Funktionen (ML) und gestattet andererseits eine interne Definition der Konnektive ∨, ∧, ∃ (vgl. Abschnitt 3.1.1 und 3.1.5), der intensionalen Gleichheit (durch x = y ⇔_{def} ∀P.P (x) → P (y)^{4}) und schließlich von kategoriellen Datentypen, wie natürliche Zahlen, Listen, Bäume, Paare, streams ([Hag87, Wra89]), so daß diese Konstrukte einem imprädikativen System nicht als axiomatische Basiskonstrukte hinzugefügt werden brauchen. Es darf jedoch nicht verschwiegen werden, daß die zu diesen Datentypen gehörigen Induktionsprinzipien zwar konsistent, jedoch nicht aus der Codierung ableitbar sind. Sie werden daher als Axiome hinzugefügt.

Möchte man typentheoretische Systeme zur maschinenunterstützten Verifikation und/oder Entwicklung von Programmen einsetzen, so sind gewisse Entscheidbarkeitseigenschaften des Systems wünschenswert: Nur wenn die Typisierungsrelation ”:“ entscheidbar ist, lassen sich Beweise maschinell überprüfen; entscheidbare strukturelle Äquivalenz von Termen ist nützlich für gleichungsorientiertes Beweisen. Diese Eigenschaften und verschiedene beweistheoretische Resultate (z.B. Konsistenz) folgen aus der als starke Normalisierung bezeichneten Eigenschaft eines Systems, daß die β–Reduktion von Termen eine noethersche Relation ist, jede Folge von Reduktionen also irgendwann abbricht (bei einem Term in Normalform).

3Man beachte die formale Analogie zum modus ponens

4Diese Definition der Gleichheit wird als Leibniz–Gleichheit bezeichnet. ”Dinge, die durch nichts zu unterscheiden sind, sollen gleich sein.“

Es erscheint also wünschenswert, daß ein Typensystem zur Beschreibung funktionaler Sprachen sowohl Σ–Typen zur oben beschriebenen Darstellung von Spezifikationen zur Verfügung stellt, Imprädikativität erlaubt und die beschriebenen Entscheidbarkeitseigenschaften hat. Leider widersprechen sich diese Forderungen zum Teil; je nach intendierter Anwendung sind an der einen oder anderen Eigenschaft Abstriche zu machen. Es existieren daher verschiedene intuitionistische Typensysteme, deren wichtigste im folgenden kurz skizziert werden.

1971 stellte Martin–Löf ein imprädikatives System mit einem einzigen Typuniversum und Σ–Typen vor [ML71]. Girard zeigte von diesem Kalkül die Inkonsistenz, d.h. daß jeder Typ (also auch die logischen Sätze) einen Vertreter (einen Beweis) hat [Gir71, Coq90]. Es ist seitdem als Girards Paradoxon bekannt, daß die zur Spezifikation verwandten Σ–Typen nicht demselben Universum, wie die imprädikativen Typen angehören können. Martin–Löf präsentierte daraufhin in [ML84] ein prädikatives System, dessen Konsistenz ”auf einfache Weise“ gezeigt werden kann, welches aber nicht die imprädikativen Codierungen und auch nicht die Darstellung von Polymorphismus erlaubt. Dieser Typenkalkül stellt dafür induktive Datentypen durch strukturelle Regeln bereit; auch mit Induktion geführte Beweise erlauben die Extraktion von Programmen [NPS90]. Allerdings hat dieses System keine starke Normalisierung und keine entscheidbare Typisierungsrelation. Der Theorembeweiser NuPRL [CH90] baut auf diesem System auf.

Girards ”système F“, bzw. der polymorphe λ–Kalkül (PLC) ist ein imprädikatives System, das allerdings keine Σ–Typen und auch keine typenwertigen Funktionen (dependent types) bereitstellt. Es wurde von Girard [Gir71] eingeführt, um die Schnittfreiheit der Arithmetik zweiter Ordnung zu zeigen (diese folgt aus der starken Normalisierung des PLC) und unabhängig von Reynolds [Rey74] entdeckt, der damit parametrisch polymorphe Funktionen untersuchte. Dieses System ist theoretisch sehr gut untersucht ([BMM90, See87, Mes88, BFŠS90, Wra89] nur als Beispiele) und bildet die Grundlage des weiter unten beschriebenen Calculus of Constructions. Wegen des Fehlens strukturierter Typen und einer internen Logik ist der PLC als Umgebung für Programmverifikation jedoch weniger geeignet.

Der von Coquand und Huet entwickelte imprädikative Calculus of Constructions (CC) erweitert den PLC um dependent types. Dadurch wird es möglich, Prädikate und insbesondere die Leibniz–Gleichheit darzustellen. In der dadurch gegebenen internen Logik kann das System in einem gewissen Rahmen ”über sich selbst“ sprechen: Läßt sich im CC ein Vertreter des Typs, der die Gleichheit zweier CC– Terme zum Ausdruck bringt, angeben, so sind diese Terme auch syntaktisch gleich. Konstrukte funktionaler Programmiersprachen (induktive Datentypen) lassen sich im CC durch imprädikative Codierung darstellen. Mit Hilfe der internen Logik können Aussagen über diese Typen formuliert und bewiesen werden. Es existieren mehrere Implementationen des CC, in ihnen wurden zahlreiche mathematische Theoreme formuliert und bewiesen; auch auf dem Gebiet der Programmentwicklung und –verifikation bestehen Erfahrungen [PM86]. Im CC existieren jedoch keine Σ–Typen, diese wurden von Luo [Luo90] hinzugefügt. Das dadurch entstehende System ECC zusammen mit der Implementation Lego durch Pollack [LPT89, Pol88] bildet die Grundlage dieser Arbeit. Lego unterstützt das Auffinden von Vertretern vorgegebener Typen des ECC durch komplexe Buchführung, welche das Erstellen solcher Vertreter in einem top–down–Verfahren ermöglicht. Die automatische Typüberprüfung erlaubt das Überprüfen von Beweisen und auch der Kompatibilität von Moduln.

Für eine genaue und detailliertere Beschreibung dieser und verwandter Typensysteme verweisen wir auf [Bar90], für eine Einführung in Lego auf [LPT89].

Überblick über die Arbeit Die vorliegende Arbeit verwendet das Lego–System, um modulare ML–Programme maschinell unterstützt zu verifizieren. Dabei werden sowohl die theoretischen Grundlagen dieses Vorhabens beleuchtet, als auch die Vorgehensweise an einem größeren Beispiel praktisch durchgeführt. Grundidee der Arbeit ist es, die Konstrukte von ML als Terme des ECC, bzw. von Lego darzustellen, um dann die oben beschriebene typentheoretische Verifikationsmethodik anzuwenden.

Im zweiten Kapitel wird eine kategorielle Sichtweise nichtmodularer funktionaler Programmiersprachen vorgestellt, und gleichzeitig der Teil von ML, auf den sich die Arbeit bezieht, eingegrenzt. Außerdem wird die in der Einleitung angedeutete typentheoretische Interpretation modularer Verifikation vertieft.

Im dritten Kapitel wird die Interpretation von ML in Lego — aufbauend auf den im zweiten Kapitel vermittelten kategoriellen Anschauungen — beschrieben, es werden Probleme von Gleichheit und Entscheidbarkeit behandelt, und es wird gezeigt, wie gewisse Fälle beweisbar terminierender allgemeiner Rekursion auch in einem stark normalisierenden Kalkül dargestellt werden können.

Das vierte Kapitel ist einem größeren Beispiel — der Symboltabelle aus [San89]

— gewidmet, es dient einerseits dazu, die praktische Verwendbarkeit des beschriebenen Ansatzes zu begründen und andererseits der Verdeutlichung der vorher theoretisch gegebenen Konstruktionen.

Im fünften Kapitel werden schließlich einige Erweiterungsmöglichkeiten und offene Probleme vorgestellt.

6 KAPITEL 1. EINLEITUNG

Grundlagen

In diesem Kapitel werden programmiersprachliche, typentheoretische und kategorielle Grundlagen der Arbeit präsentiert, soweit sie nicht in einschlägigen Lehrbüchern zu finden sind. Vorausgesetzte Kenntnisse finden sich etwa in [Mac71, HS79, MA86] (Kategorien und Datentypen) [Coq85a, Coq90, CH88, Hue88, Luo90] (Typentheorie und Calculus of Constructions); die Quellen [Hue88, Šče90] bieten eine gute Einführung in diverse Typensysteme, eine Beschreibung des Lego-Systems und zahlreiche gut verständliche Anwendungsbeispiele sind in [LPT89, Tay89] gegeben. Die Definition der Programmiersprache Standard–ML ist in [HMT89] gegeben, eine gut lesbare Einführung ist [HMM87].

Im ersten Abschnitt behandeln wir die für die formale Verifikation wichtigen Aspekte (nichtmodularer) funktionaler Programmiersprachen, im zweiten Abschnitt wird die Darstellung induktiver Datentypen und damit verbundener Funktionen als sogenannte T –Algebren erklärt, der dritte Abschnitt schließlich behandelt logische und typentheoretische Aspekte des modularen Teils von ML, dabei wird gleichzeitig auch die Lego–Interpretation des Modulkonzeptes beschrieben.

2.1 Funktionale Programmiersprachen

Wie alle höheren Programmiersprachen bestehen auch funktionale Programmiersprachen aus Daten–, Kontroll– und (seit neuerem auch) Modulstrukturen. Im Gegensatz zu herkömmlichen Programmiersprachen sind jedoch die einzigen Kontrollstrukturen einer funktionalen Sprache die Applikation (einer Funktion auf ihr Argument) und die Abstraktion (von Ausdrücken mit freien Variablen zu Funktionstermen). Wie kann dies — insbesondere bei strenger Typisierung — ausreichen?

Zunächst stellt jede funktionale Programmiersprache eine große Zahl von Basisfunktionen, wie etwa add, times, cons, nil, etc. zur Verfügung, aus denen durch Komposition, Applikation und Abstraktion neue entstehen. Dies allein ist freilich immer noch zu wenig; ihre volle Universalität erhalten funktionale Programmiersprachen erst durch das Vorhandensein sogenannter Kombinatoren, die es ermöglichen, aus schon bekannten (implementierten) Funktionen neue zusammenzusetzen. Hierzu gehören der Iterator, der aus einer natürlichen Zahl und einer (Endo–)Funktion ihre entsprechend Iterierte bildet, der primitive Rekursor, oder auch so allgemeine Kon-

Datentyp  Basisfunktionen Kombinatoren
Nat. Zahlen  0, ν  Iteration
Listen  nil,cons  Listeniteration
Cart. Produkt  Proj. (fst,snd) Paarung ”⟨., .⟩“
(Disj.) Vereinigung  Inj. (inl,inr)  Falluntersch. (case)
Funktionenraum (A ⇒ B)  Applikat.  Abstraktion
Unendl. Listen (lazy streams) hd,tail          mkstream

  Wahrheitswerte  true,false       if then else

Ind. Datentyp (ML datatype) Konstr. (con_{i})  pattern–matching
Bäume  leaf,node  Baumiteration
…  …  …

Abbildung 2.1: Datentypen funktionaler Programmiersprachen

strukte, wie das aus ML bekannte pattern–matching. Die Kombinatoren bilden also Funktionen und/oder Werte auf Funktionen und/oder Werte ab. Fassen wir Funktionen als Werte oder Objekte ”erster Klasse“ auf, so könnten wir auch die Kombinatoren zu den Basisfunktionen zählen; wir wollen die Unterscheidung jedoch an dieser Stelle beibehalten. Woher kommen nun die Basisfunktionen und Kombinatoren, nach welchen Kriterien werden sie ausgewählt? Goguen [GTWW77] und andere Autoren [MA86] haben festgestellt, daß diese sehr eng mit den verwendeten Datenstrukturen zusammenhängen, ja daß jedem Datentyp ihm eigentümliche Basisfunktionen und Kombinatoren zugeordnet sind. Das ist nicht weiter verwunderlich, denn eine Datenstruktur macht nur dann Sinn, wenn es Möglichkeiten gibt, Vertreter aus ihr zu konstruieren, d.h. wenn sie als Wertebereich einer Funktion auftritt, und auf ihre Werte zugegriffen werden kann, d.h. wenn sie Definitionsbereich gewisser Funktionen ist. Umgekehrt stehen auch Funktionen allein schon durch ihre Typisierung in Beziehung zu gewissen Datenstrukturen. Vollständig polymorphe, an keine Datenstruktur gebundene Funktionen sind — zumindest beim Polymorphismus von ML — auf wenige Beispiele beschränkt.

2.2. DATENTYPEN ALS T –ALGEBREN 9

Geht man nun — gemäß Ockhams^{1} Rasiermesser — davon aus, daß nur die unbedingt erforderlichen Funktionen ”einzubauen sind“, und die weiteren, der Bequemlichkeit dienenden, in einer Bibliothek und als funktionale Programme bereitgestellt werden sollen, so wird man zu einer Datenstruktur nur soviele Basisfunktionen und Kombinatoren fordern, wie nötig sind, um alle Vertreter des Typs zu kreieren, bzw. wie erforderlich sind, um alle relevante Information aus der Struktur herauszuholen. Andererseits wird man mit den Konstruktionsfunktionen keine Vertreter des Datentyps erzeugen, die nicht mit Funktionen auf dem Datentyp verwendet werden können. Die gemäß diesen Minimalforderungen zu einigen aus der funktionalen Programmierung bekannten Datenstrukturen gehörigen Funktionen sind in Tabelle 2.1 zusammengefaßt. Wir stellen an dieser Zusammenstellung zunächst fest, daß bei einigen dieser Datentypen (N, list, datatype,…) die Basisfunktionen (0, ν, nil, cons, con_{i},…) in den Typ hineinlaufen — wir bezeichnen sie dann als Konstruktoren —, während die Kombinatoren (Iterator, fold, if then else, pattern–matching,…) dazu dienen, mit Vertretern des Typs zu arbeiten. Diese Datentypen bilden in der der Sprache zugrundeliegenden Kategorie [BW90] eine initiale T –Algebra. Dies deshalb, weil hier zwischen den Konstruktoren keine Gleichungen bestehen, und der Kombinator gerade den von der Initialität geforderten eindeutig bestimmten Morphismus realisiert. Andere Datentypen (Produkt, streams, Funktionenräume,…) werden durch Kombinatoren aufgebaut (Paarung, make–stream, currying,…) und durch Basisfunktionen verwendet (Projektionen, (hd, tail), Applikation). Die Basisfunktionen nennen wir dann Destruktoren. Diese Datentypen bilden terminale T –Coalgebren und codieren meist (potentiell) unendliche Datenstrukturen. Die Programmiersprache ML weist hier eine gewisse Asymmetrie auf, indem sie kein den datatypes vergleichbares allgemeines Konzept zur Erzeugung von Coalgebren bereitstellt. Ein solches wurde z.B. in [Hag87] vorgeschlagen.

1Wilhelm von Ockham (engl.: Occam), Naturphilosoph, 1300–1349

Auf den so gebildeten Datentypen können nun durch Hinzufügen von Funktionen und Relationen, wie der Gleichheit, und anschließende Abstraktion neue Typen gewonnen werden, z.B. stacks und sets aus Listen oder aus Bäumen. Diese gehören jedoch nicht zum Basisinventar von ML und werden deshalb in dieser Arbeit auch nicht als solches untersucht. Implementationen solcher Datentypen durch ML–Code lassen sich mit den in der Arbeit beschriebenen Verfahren aber auch in Lego durchführen.

Einschränkungen Dem Leser wird nicht entgangen sein, daß mit den beschriebenen Konstruktionen nur totale Funktionen definiert werden können und somit nicht die volle Turing–Mächtigkeit erreicht werden kann. Die Klasse der darstellbaren Funktionen ist dennoch sehr groß [Hue88] und auch in Hinblick auf einfachere Parallelisierbarkeit schlagen verschiedene Autoren [BTM90, Rey90] vor, auf Partialität und damit die volle Mächtigkeit zu verzichten. Heutige funktionale Programmiersprachen beinhalten allerdings stets auch die allgemeine Rekursion als Funktionskonstruktor; ihre theoretische Begründung basiert auf ganz anderen Betrachtungen (domains), die in dieser Arbeit nicht angestellt werden. Gewisse Fälle beweisbar terminierender allgemeiner Rekursionen lassen sich jedoch mit der in Abschnitt 3.3 gegebenen Methode auch in den beschriebenen Ansatz eingliedern.

Außer den beschriebenen Konstrukten enthalten funktionale Programmiersprachen auch imperative Strukturen, wie Zeiger, Wertzuweisungen oder Ausnahmebehandlungen (exceptions), ohne die praktische Programmierung zum jetzigen Zeitpunkt nicht möglich erscheint. Sie werden in dieser Arbeit allerdings aus Zeit– und Platzgründen nicht untersucht.

2.2 Datentypen als T –Algebren

Im letzten Abschnitt haben wir gesehen, daß für ein Verständnis von Datentypen die Untersuchung ihrer Beziehungen zu anderen Objekten wichtig ist, ja daß sie dadurch eigentlich schon vollständig beschrieben sind. Der Zweig der Mathematik, der sich mit den Beziehungen von Objekten untereinander beschäftigt, ist die Kategorientheorie (‘Category theory always asks … What are the morphisms?’ [Mac71]) Wir geben daher in diesem Abschnitt eine kategorielle Sichtweise von Datentypen, die sich, wie wir im nächsten Abschnitt sehen werden, fast unmittelbar auf Lego übertragen läßt. In diesem Kapitel werden einige kategorientheoretische Grundkenntnisse vorausgesetzt. Der Leser findet in den eingangs genannten Standardwerken eine Einführung.

2.2.1 Definition

Sei für den Rest dieses Abschnitts eine beliebige cartesisch abgeschlossene Kategorie K vorgegeben. Ein Objekt N von K heißt Objekt der natürlichen Zahlen (kurz NNO), wenn es einen Pfeil 1 →^{0} N (der die Null auszeichnet) und einen Pfeil N →^{ν} N (den Nachfolger) gibt, derart daß es zu jedem anderen Objekt X mit ausgezeichnetem Element 1 →^{e} X und einer einstelligen Operation X →^{f} X einen eindeutigen^{2} Pfeil N →^{u} X gibt, derart daß u^{∘}ν = f^{∘}u und u^{∘}0 = e ist. So ist beispielsweise in der Kategorie Set aller Mengen mit Funktionen als Pfeilen die Menge N der natürlichen Zahlen ein NNO; der eindeutige Pfeil N →^{u} X ist gegeben durch n ↦ f^{n}(e).

Unter einem Listenobjekt über einem fest vorgegebenen Objekt der Einträge E verstehen wir ein Objekt list(E) zusammen mit einem Pfeil nil : 1 → list(E)^{3} und einem Pfeil cons : E ×list(E) → list(E) (mit der aus LISP bekannten Bedeutung), derart daß zu jedem anderen Objekt X mit ausgezeichnetem Element 1 →^{n} X und einer Operation E × X →^{c} X einen eindeutigen Pfeil list(E) →^{u} X gibt, so daß e = u^{∘}nil und c^{∘}(id_{E} × u) = u^{∘}cons ist.

In der Kategorie der Mengen wiederum ist list(E) gegeben durch die ”wirklichen Listen“, d.h. durch das freie Monoid E^{∗}. Der eindeutige Morphismus N →^{u} X ist die sogenannte Listeniteration:

(e_{1}, e_{2}, ..., e_{ℓ}) ↦ c(e_{1}, c(e_{2}, ..., c(e_{ℓ}, n))...)

Auf analoge Weise lassen sich binäre oder beschriftete Bäume, Termalgebren und ähnliche frei erzeugte Datenstrukturen kategoriell modellieren. Um von solchen speziellen Beispielen zu abstrahieren, und um allgemeine Resultate zeigen zu können, haben Lehmann und Smyth den Begriff der T –Algebra eingeführt [LS81]:

Definition 2.2.1.1 Sei T : K → K covarianter Endofunktor auf K. Eine T –Algebra besteht aus einem Objekt A und einem Morphismus T (A) → A. Eine T –Algebra (A, T (A) →^{φ} A) heißt initial, wenn zu jeder anderen T –Algebra (X, ψ) auf eindeutige Weise ein Pfeil u : A → X existiert, so daß

2Eigentlich müßte es hier heißen ”auf eindeutige Weise“; gemeint ist, daß je zwei Pfeile, die der geforderten Bedingung genügen, gleich sind. Da es im Deutschen kein kurzes Wort zur Bezeichnung dieses Sachverhaltes gibt, wollen wir par abus de langage den Begriff ”eindeutiger Pfeil“ mitunter verwenden.

3Die Notationen A →^{f} B und f:A → B zur Bezeichnung von Pfeilen einer Kategorie sind synonym

[figure: T (X); X; ψ; T (A); A; φ; T (u); u]

kommutiert. Den Morphismus φ einer initialen T –Algebra nennt man Strukturmorphismus, der Funktor T wird als Signaturfunktor der T –Algebra bezeichnet.^{4}

Da zwei initiale T –Algebren (zum selben Signaturfunktor) stets isomorph sind, spricht man auch von der initialen T –Algebra.

Das oben eingeführte NNO ist initiale T –Algebra zu T (X) := 1 + X mit Strukturmorphismus [0, ν]; der zum Listenobjekt gehörige Signaturfunktor ist T (X) := 1 + E × X, der entsprechende Strukturmorphismus ist [nil, cons]. Ein weiteres wichtiges Beispiel wird durch den (konstanten) Funktor T (X) = 1 + 1 gegeben: Die zu ihm gehörige initiale T –Algebra hat zwei ausgezeichnete Elemente und kann zur Repräsentation der Menge bool der Wahrheitswerte verwendet werden.

Existenz: Initiale T –Algebren brauchen nicht notwendigerweise zu existieren, es gilt jedoch folgender Satz [MA86]

Theorem 2.2.1.2 Ist K ω–covollständige Kategorie, hat also Colimites unendlicher Ketten und ist T : K → K polynomialer Funktor, also aus konstanten Funktoren, dem Identitätsfunktor, sowie Produkt und Coprodukt aufgebaut, so existiert die initiale T –Algebra.

Im folgenden wollen wir die Existenz initialer T –Algebren stillschweigend voraussetzen und auch das Attribut ”initial“ — falls aus dem Kontext ersichtlich — weglassen.

Notation: Die initiale T –Algebra zu einem Funktor T bezeichnen wir mit μX.T (X). Die Variable X wird dadurch gebunden. Das NNO N schreibt sich in dieser Notation beispielsweise N = μX.1 + X.

Manche Autoren bezeichnen initiale T –Algebren auch als (kleinste) Fixpunkte eines Endofunktors; dies erklärt sich aus folgendem Satz [Lam70]:

Satz 2.2.1.3 Der Strukturmorphismus einer initialen T –Algebra A ist Isomorphismus, d.h. es ist T (A) ≅ A.

4Die Bezeichnung T -Algebra ist insofern mißverständlich, als sie etwa in [BW85] in anderer Bedeutung gebraucht. Deshalb bezeichnen manche Autoren die hier beschriebenen Objekte auch als R– oder Ψ-Algebren [MA86]. In Übereinstimmung mit [RP88, BFŠS90, Alt90] wurde hier dennoch erstere Bezeichnung gewählt.

Beweis: Sei T vorgegeben und A := μX.T (X) initiale T –Algebra mit Struktur-

morphismus φ : T (A) → X Wegen T (T (A)) →^{T (φ)} T (A) ist auch T (A) (a priori nicht initiale) T –Algebra. Sei u der deshalb existierende eindeutige Morphismus A → T (A). Weil nun

[figure: T (A); A; φ; T (A); A; φ; T (s); s]

sowohl mit s := φ^{∘}u, als auch mit s := id_{A} kommutiert, muß φ^{∘}u = id_{A} sein. Nach Definition ist aber T (φ^{∘}u) = T (φ)^{∘}T (u) = u^{∘}φ und somit u^{∘}φ = T (id_{A}) = id_{T (A)}□

Der Strukturmorphismus einer T –Algebra ist also stets invertierbar. Bei den natürlichen Zahlen ist dieses Inverse der Vorgänger, bei den Listen das Paar (car,cdr).

Bemerkung 2.2.1.4 Die Tatsache, daß bei dieser Darstellung der Wertebereich etwa des Vorgängers nicht N selbst, sondern 1 + N ist, läßt sich als Ausnahmebehandlung (exception) deuten. Ist der Vorgänger definiert, so liegt das Resultat in N, wird er dagegen auf Null angewandt, so resultiert dies in einem Ergebnis in 1 —eine ”Fehlermeldung“ tritt auf.

Bemerkung 2.2.1.5 Als kategorielles Konzept gestatten auch die T –Algebren eine Dualisierung durch ”Umdrehen aller Pfeile“. Die entstehenden Konstrukte sind die bereits im letzten Abschnitt erwähnten terminalen T –Coalgebren [Hag87]. Sie lassen sich zur Modellierung (potentiell) unendlicher, sogenannter lazy Datenstrukturen verwenden. Ist z.B. T (X) = A×X, so ist die terminale T –Coalgebra gegeben durch ein (mit νX.T (X) bezeichnetes) Objekt S und einen Morphismus S →^{ψ} A × X, derart, daß zu jeder anderen T –Coalgebra X →^{f} A × X genau ein Pfeil X →^{m} S existiert, so daß

[figure: X; A × X; f; S; A × S; ψ; m; A × m]

kommutiert. Das Objekt S kann man als lazy–stream, also als unendliche Liste deuten. Durch den Morphismus m (make stream) wird ein Prozeß (X, f), der eine unendliche Folge von Elementen aus A liefert (X ist ”Zustandsraum“ und f die Übergangsfunktion), als unendliche Liste aufgefaßt. Die beiden Komponenten des Morphismus ψ liefern dann das jeweils nächste Element, bzw. den Rest der Liste.

Ein anderes wichtiges Beispiel ist durch die terminale T –Coalgebra zu T (X) = 1 + X, also zum Signaturfunktor des NNO, gegeben. In Set ist diese die Menge N ∪ {∞}, der Strukturmorphismus ist der Vorgänger, wobei pred(∞) = ∞ ist. Wie sich das NNO zur Modellierung von Iteration und primitiver Rekursion eignet, repräsentiert dieses Objekt die while–Schleife, bzw. die unbeschränkte Minimalisierung.

2.2.2 Parametrische T –Algebren

Hängt wie im Falle der Listen der Signaturfunktor außer von X noch von einem weiteren Objekt P ab, so spricht man von einer parametrisierten T –Algebra. Die Zuordnung des Parameters zur initialen T –Algebra, also im Falle der Listen die Zuordnung von E zu list(E), läßt sich auf folgende Weise zu einem Funktor erweitern [Hag87]:

Sei T : K × K → K ein (in beiden Argumenten) covarianter Bifunktor und P beliebiges K–Objekt. Mit D(P) := μX.T (P, X) bezeichnen wir die zum Parameter P gehörige T –Algebra; mit φ_{P} : T (P, D(P)) → D(P) den entsprechenden Strukturmorphismus.

Sei jetzt ein Pfeil P →^{f} Q (P, Q beliebig) vorgegeben. Wir konstruieren einen

Pfeil D(P) → D(Q): Wegen T (P, D(Q)) →^{T (f,id)} T (Q, D(Q)) ist auch D(Q) (im allgemeinen nicht initiale) T (P,?)–Algebra. Es existiert also ein (eindeutiger) Pfeil von D(P) — der initialen T (P,?)–Algebra nach D(Q). Diesen bezeichnen wir mit D(f). Man überzeugt sich durch Nachrechnen davon, daß die Zuordnung f ↦ D(f) funktoriell ist.

Im Falle der Listen ist diese Zuordnung gerade die aus LISP bekannte mapcar– Funktion, die eine Funktion auf die einzelnen Elemente einer Liste anwendet.

2.2.3 Iteration

Der kraft Initialität gegebene eindeutige Pfeil läßt sich nun verwenden, um Funktionen auf einer T –Algebra zu definieren. Als Beispiel wollen wir die Funktion λ : list(E) → N, die die Länge einer Liste bestimmt, definieren. (Es ist hier K=Set). Mit

1 + N × E ⟶^{[0,ν∘π_{1}]} N

ist auch N initiale 1+? × E–Algebra. Die deshalb eindeutig gegebene Funktion list(E) → N ist gerade die gesuchte Längenfunktion, da mit der ”wirklichen“ Längenfunktion das Diagramm

[figure: 1 + N × E; N; [0, ν^{∘}π_{1}]; 1 + list(E) × E; list(E); [nil, cons]; 1 + λ × id_{E}; λ]

kommutiert.

Betrachten wir diese Situation algorithmisch, so sehen wir, daß hier eine Funktion durch Iteration definiert wurde:

λ(nil) = 0
λ(cons(e, l)) = ν(λ(l))

Diese Gleichungen sind ja gerade die Kommutationsbedingungen obigen Diagramms. Allgemein ist es so, daß eine Funktion f : list(E) → R, die durch das Iterationsschema

f(nil) = n
f(cons(e, l)) = h(e, f(l))

gegeben ist, kategoriell modelliert wird durch den eindeutigen Pfeil f, der das Diagramm

[figure: 1 + R × E; R; [n, h]; 1 + list(E) × E; list(E); [nil, cons]; 1 + f × id_{E}; f]

kommutieren läßt.

2.2.4 Primitive Rekursion

Neben der Iteration läßt sich auch das Konstruktionsschema der primitiven Rekursion, bei der ja neben dem ”alten“ Funktionswert f(e, l) auch noch das Argument l zur Definition des neuen Funktionswertes zur Verfügung steht, kategoriell formulieren. Wir bleiben beim Beispiel der Listen und wollen zunächst mengentheoretisch definieren, was hier unter primitiver Rekursion zu verstehen sei.

Definition 2.2.4.1 (Primitive Rekursion für Listen, mengentheoretisch) Ein primitives Rekursionsschema zur Definition einer Funktion f : list(E) → R besteht aus einer Konstanten n aus R und einer Funktion h : E × list(E) × R → R. Dieses definiert eindeutig die Funktion f als Lösung der Rekursionsgleichungen

f(nil) = n
f(cons(e, l)) = h(e, l, f(l))

Kategoriell läßt sich dies so ausdrücken:

Definition 2.2.4.2 (Primitive Rekursion für Listen, kategoriell) Ein (kategorielles) primitives Rekursionsschema zur Definition eines Pfeiles list(E) → R ist ein Morphismus ψ : 1 + E × list(E) × R → R.^{5} Man sagt, ψ bestimmt f : list(E) → R durch primitive Rekursion, wenn

5ψ entspricht [n, h]

[figure: 1 + E × list(E) × R; R; ψ; 1 + E × list(E); list(E); [nil, cons]; 1 + ⟨id_{E×list(E)}, f⟩; f]

kommutiert.

Wie man sich durch ”Diagrammjagd“ (diagram–chasing) überzeugen kann, hat dies die intendierte Bedeutung. Wir wollen diese Situation nun auf beliebige T –Algebren verallgemeinern.

Definition 2.2.4.3 (Primitive Rekursion für T –Algebren) Sei T (A) →^{φ} A initiale T –Algebra und R beliebiges Objekt (Objekt des Resultats). Unter einem primitiven Rekursionsschema des Typs A → R verstehen wir einen Pfeil ψ : T (A × R) → R. Wir sagen, f : A → R erfüllt das Rekursionsschema, wenn

[figure: T (A × R); R; ψ; T (A); A; φ; T (⟨id_{A}, f⟩); f]

kommutiert.

Durch eine Verallgemeinerung des auf Dedekind zurückgehenden Paarungstricks zeigen wir, daß jedes Rekursionsschema eine eindeutige Lösung hat: Wegen

⟨φ^{∘}T (π_{1}), ψ⟩ : T (A × R) → A × R

ist A × R (nicht unbedingt initiale) T –Algebra. Es existiert also genau ein Pfeil f̃, so daß

[figure: T (A × R); A × R; ⟨φ^{∘}T (π_{1}), ψ⟩; T (A); A; φ; T (f̃); f̃]

kommutiert. Der Pfeil f := π_{2} ∘ f̃ erfüllt dann das Rekursionsschema ψ. Davon und von der Eindeutigkeit kann man sich wiederum durch Nachrechnen überzeugen. Zu bemerken ist, daß hier auch der Beweis der Kommutativität von der Initialität Gebrauch macht.

Beispiel: Zur Verdeutlichung betrachten wir nun auch das Objekt der natürlichen Zahlen. Es ist T (X) = 1 + X, ein primitives Rekursionsschema vom Typ R also ein Pfeil 1 + N × R → R, bzw. zwei Pfeile 1 →^{g} R und N × R →^{h} R.^{6} Diese bestimmen genau ein f : N → R mit

f^{∘}0 = g
f^{∘}ν = h^{∘}⟨id_{N}, f⟩

bzw. mengentheoretisch

f(0) = g
f(n + 1) = h(n, f(n))

Hier erkennen wir die gewohnte Form der primitiven Rekursion wieder.

Primitive Rekursion mit Parametern Bei der allgemeinsten Form der primitiven Rekursion sind neben n noch zusätzliche Parameter vorhanden:

f(0, x⃗) = g(x⃗)
f(n + 1, x⃗) = h(n, f(n, x⃗), x⃗)

Diese Situation läßt sich jedoch auf die bereits behandelte reduzieren, indem man als Ergebnisraum einen Funktionenraum wählt:

f̃(0) = λx⃗.g(x⃗)
f̃(n + 1) = λx⃗.h(n, f(n, x⃗), x⃗)

Kategoriell läßt sich diese Konstruktion mit Hilfe von Exponentenobjekten durchführen.

2.2.5 Induktion

Um Aussagen über natürliche Zahlen, Listen, Bäume und ähnliche Datenstrukturen zu beweisen, wird häufig das Prinzip der strukturellen Induktion verwandt. Wollen wir dieses Prinzip auf beliebige T –Algebren anwenden, so ist zunächst eine ausreichend allgemeine Formulierung des Induktionsprinzips zu bestimmen und dann zu untersuchen, ob dieses verallgemeinerte Induktionsprinzip schon aus der Initialität folgt, oder ob es als weiteres Axiom hinzuzunehmen ist.

Bemerkung 2.2.5.1 Strukturelle Induktion läßt sich auch für nichtrekursive Datenstrukturen, wie etwa bool formulieren, in diesem Fall besagt sie, daß eine Aussage, die für true und false gilt, für alle Objekte des Typs bool erfüllt ist.

Ein Induktionsprinzip für eine Datenstruktur macht eine Aussage über Eigenschaften derselben. Also wird am Anfang eine geeignete (kategorielle) Formalisierung des Begriffs der Eigenschaft stehen müssen. Dafür gibt es (durchaus auch aus philosophischer Sicht) grundsätzlich zwei Möglichkeiten:

6Hier ist also ψ = [g, h]

• Eine Eigenschaft über A soll ein Morphismus von A in ein spezielles Objekt Ω, das Objekt der Wahrheitswerte, sein. (In Set ist Ω = {true, false}.)

• Eine Eigenschaft über einem Objekt A soll ein Unterobjekt von A, also ein Objekt U mit Monomorphismus U ↪^{ι} A sein. Mit U meinen wir das Objekt derjenigen Individuen aus A, denen die Eigenschaft zukommt.

Was haben diese beiden Definitionen miteinander zu tun? Ist eine Eigenschaft über A durch einen Pfeil P:A → Ω gegeben, so erhalten wir das die Eigenschaft beschreibende Unterobjekt als Differenzkern (equalizer) von P und dem ”konstant wahren Pfeil“.

[figure: U_{P}; A; ι; Ω; P; true]

Daß es hingegen zu jedem Unterobjekt von A einen Pfeil von A nach Ω (mit geeigneten Zusatzbedingungen) gibt, ist gerade die charakteristische Eigenschaft eines elementaren Topos. (Set ist ein Topos.)

Ist eine Eigenschaft als Pfeil P:A → Ω gegeben, so können wir die Aussage ”das Element x:1 → A hat P“ formulieren als P^{∘}x = true. Ist eine Eigenschaft dagegen als Unterobjekt U ↪^{ι} A gegeben, so sagen wir x:1 → A habe U, wenn es einen Pfeil x̃:1 → U mit ι^{∘} x̃ = x gibt. Dasselbe gilt für verallgemeinerte Elemente x:R → A.

[figure: R; x̃; U; A; ι; Ω; P; x; true]

Ein Prädikat, das immer erfüllt ist, nennen wir universell. P:A → Ω ist universell, falls P über true:1 → Ω faktorisiert und U ↪^{ι} A ist universell, falls ι Isomorphismus ist.

Verschiedene Versuche und Irrwege haben nun gezeigt, daß für die Generalisierung des Induktionsprinzips die Definition von Eigenschaften als Unterobjekte günstiger ist. Überlegen wir uns also zunächst, wie in dieser Darstellung das Induktionsprinzip für natürliche Zahlen aussieht. Sei ein Unterobjekt U ↪^{ι} N vorgegeben. Die Induktionsvoraussetzungen lauten dann:

• 0 hat U, d.h. es existiert ˜0:1 → U mit 0 = ι^{∘} ˜0

• U ist unter Nachfolger abgeschlossen, anders gesagt, das verallgemeinerte Element ν^{∘}ι:U → N hat U, d.h. es existiert ν̃:U → U mit ι^{∘} ν̃ = ν^{∘}ι.

Zusammenfassend können wir sagen, daß U die Induktionsvoraussetzungen erfüllt, wenn es Pfeile ˜0:1 → U und ν̃:U → U gibt, so daß folgendes Diagramm kommutiert.

[figure: 0; 1; ˜0; ι; N; N; ν; U; U; ν̃; ι]

Das Induktionsprinzip sagt dann aus, daß solch eine Eigenschaft U universell ist, also für alle Elemente von N erfüllt ist. Kategoriell bedeutet dies, daß ι — die Inklusion — Isomorphismus ist. Dies aber können wir in der Tat beweisen, denn wegen der Initialität von N existiert ein Pfeil u:N → U mit den entsprechenden Natürlichkeitsbedingungen. Dies liefert einen Endomorphismus ι^{∘}u:N → N, der wiederum wegen der Initialität von N gleich der Identität sein muß. u^{∘}ι ist auch die Identität, allein schon, weil ι Monomorphismus (injektiv) ist.

In der gewählten Formulierung können wir das Induktionsprinzip für N also aus der Initialität zeigen. Stellen wir nun mit Hilfe des Coproduktes N als initiale T –Algebra dar,

[figure: 1 + N; N; [0, ν]; 1 + U; U; [˜0, ν̃]; 1 + ι; ι]

so liegt folgende Verallgemeinerung des Induktionsprinzips für beliebige T –Algebren nahe:

Definition 2.2.5.2 (Induktive Prädikate) Eine durch ein Unterobjekt U ↪^{ι} A gegebene Eigenschaft über einer initialen T –Algebra T (A) →^{φ} A heißt induktiv, wenn es einen Morphismus ψ:T (U) → U gibt, welcher mit der Inklusion verträglich ist.

[figure: T (A); A; φ; T (U); U; ψ; T (ι); ι]

Wir können nun das Argument für die natürlichen Zahlen kopieren und folgenden Satz beweisen:

Satz 2.2.5.3 (Induktionsprinzip für T –Algebren) Ein induktives Prädikat über einer initialen T –Algebra ist universell.

Beweis: Sei T (A) →^{φ} A die T –Algebra und U ↪^{ι} A ein — vermöge ψ : T (U) → U — induktives Unterobjekt von A. Aufgrund der Initialität von A gibt es genau einen Pfeil u : A → U mit u^{∘}ψ = φ^{∘}T (u). Da nun

[figure: T (A); A; φ; T (A); A; φ; T (u)^{∘}T (ι); u^{∘}ι]

kommutiert, muß ι^{∘}u = id_{A} sein. Folglich ist ι^{∘}u^{∘}ι = ι und wegen der Linkskürzbarkeit von ι auch u^{∘}ι = id_{U}. Die Inklusion ι ist also Isomorphismus mit Inversem u. □

Anhand von Beispielen zu Listen (T (X) = 1 + E × X), Bäumen (T (X) = 1+E ×X ×X)^{7}, kann man sich davon überzeugen, daß obige Definition das Prinzip der strukturellen Induktion modelliert; für T (X) = 1 + X + (N → X) erhalten wir als initiale T –Algebra ein Anfangssegment der abzählbaren Ordinale, notiert durch Fundamentalfolgen; hier modelliert unser Induktionsprinzip sogar die transfinite Induktion.

Wir wissen jetzt, daß die Forderung der Initialität das Prinzip der strukturellen Induktion mit einschließt. Mit gewissen Einschränkungen gilt auch das Umgekehrte:

Satz 2.2.5.4 Sei T (A) →^{φ} A schwach initiale T –Algebra — der Morphismus u aus 2.2.1.1 also nicht auf eindeutige Weise gegeben — und sei jedes induktive Unterobjekt von A universell, die Inklusion also Isomorphismus. Falls die zugrundeliegende Kategorie Differenzkerne hat, so ist unter diesen Voraussetzungen A initiale T –Algebra.

Beweis: Wir nehmen an, A sei nicht initial, es gäbe also eine (nicht initiale) T –Algebra T (X) →^{ψ} X und zwei Pfeile u_{1}, u_{2} : A → X mit den entsprechenden Kommutationsbedingungen.

Sei E →^{ι} A Differenzkern dieser beiden Pfeile ( ι ist dann automatisch ein Monomorphismus).

[figure: T (X); X; ψ; T (A); A; φ; T (u_{1}); u_{2}; T (u_{2}); u_{1}; T (E); E; T (ι); ι]

7Das Objekt E soll hier jeweils den Typ der Einträge bzw. Blattbeschriftungen repräsentieren.

Nun ist

u_{1}^{∘}φ^{∘}T (ι) = ψ^{∘}T (u_{1}^{∘}ι) = ψ^{∘}T (u_{2}^{∘}ι) = u_{2}^{∘}φ^{∘}T (ι)

Wegen der Universalität von E gibt es also einen (sogar eindeutigen) Pfeil von T (E) nach E, der das Diagramm kommutieren läßt. Mithin ist E induktives Unterobjekt von X; die Inklusion ι ist also nach Voraussetzung Isomorphismus. Damit ist aber

u_{1} = u_{1}^{∘}ι^{∘}ι^{−1} = u_{2}^{∘}ι^{∘}ι^{−1} = u_{2}

□

Bemerkung 2.2.5.5 Wir können die Betrachtungen zum Induktionsprinzip ”dualisieren“ und erhalten so Aussagen über Quotientenobjekte terminaler T –Coalgebren (Ein Quotientenobjekt eines Objekts A ist ein Objekt Q mit einem Epimorphismus σ:A → → Q). Ob dies ein nützliches Beweisprinzip für Coalgebren darstellt, bleibt zu untersuchen.

Wir haben jetzt einen kategoriellen Formalismus zur Beschreibung von Datenstrukturen und Morphismen auf ihnen im Sinne von Abschnitt 2.1 bereitgestellt. Im nächsten Abschnitt wollen wir sehen, wie sich die Datentypen von ML in diesem Formalismus präsentieren.

2.2.6 Das datatype–Konstrukt von ML

Zur Definition rekursiver Datenstrukturen stellt ML den Konstruktor datatype mit der Syntax

datatype name = con_{1}of argtype|… |con_{n}of argtype;

zur Verfügung. In den durch argtype angedeuteten Argumenttypen der Konstruktoren darf der definierte Datentyp rekursiv auftreten.

Beispiel 2.2.6.1 Typische datatype–Deklarationen sind etwa

datatype booltree = leaf of bool | node of booltree*booltree*bool

oder

datatype nat = zero | succ of nat

Die Konstruktion von Objekten eines solchen Typs erfolgt ausschließlich unter Verwendung der in der Deklaration angegebenen Konstruktoren; Funktionen auf solchen Datentypen werden definiert durch Fallunterscheidung und (primitive) Rekursion. Die Semantik des datatype–Konstruktes stellt sicher, daß eine durch Fallunterscheidung gegebene Funktion wohldefiniert ist.

Fassen wir mit Barr und Wells [BW90] eine funktionale Programmiersprache als Kategorie auf, deren Objekte die Datenstrukturen (Typen) und deren Pfeile die in der Programmiersprache definierbaren Funktionsterme sind, so sind die ML– datatypes initiale T –Algebren zu einem geeigneten, durch die Deklaration eindeutig gegebenen, Funktor.^{8} Einen Ausdruck für diesen Funktor erhalten wir nach folgender Vorschrift:

8Das trifft nicht auf alle datatypes zu, wir wollen allerdings nur die als initiale T –Algebra darstellbaren betrachten. Vgl. dazu auch die Bemerkung am Ende dieses Abschnitts

|  ⇝ +
*  ⇝ ×

Rekursives Auftreten des Datentyps

⇝ X

In obigem Beispiel etwa ergibt sich der Signaturfunktor zu

                 Tbooltree(X) = bool + X × X × bool

2.2.6.1 Pattern–matching und primitive Rekursion

Zur Definition von Funktionen auf datatypes stellt ML das schon in Abschnitt 2.1 erwähnte pattern–matching zur Verfügung. Auf nat=datatype zero|succ of nat etwa lassen sich Funktionen definieren durch

f=fun
   zero => ...
   |succ n => ...

Um dieses kategoriell und typentheoretisch verstehen zu können, müssen wir mehrere Fälle unterscheiden: Befinden sich, wie im Beispiel, auf der linken Seite der Pfeile nur die Konstruktoren und zwar jeder und kommt in den Klauseln rechts der Pfeile die zu definierende Funktion rekursiv nur angewandt auf die Argumente der rechts stehenden Konstruktoren vor, so liegt eine primitive Rekursion vor, die mit den beschriebenen Mitteln kategoriell und, wie wir später sehen, auch typentheoretisch modelliert werden kann.

Befinden sich auf der linken Pfeilseite geschachtelte Ausdrücke in den Konstruktoren, wie etwa bei

f=fun zero => zero
      |succ (succ n) => n+2
      |succ n => zero

und gilt die Einschränkung für die rechte Seite nach wie vor, so liegt eigentlich eine geschachtelte primitive Rekursion vor. Dies wird deutlich, wenn wir f umschreiben zu

f=fun zero => zero
      |succ n => aux n
aux=fun
      zero => zero
      |succ n => n+2

Auch dieser Fall von pattern-matching läßt sich also auf den behandelten Fall zurückführen. Man beachte, daß man bei der informellen Verifikation eines solchen Schemas im allgemeinen gerade dies tut.

Schließlich kann es sein, daß die rekursive Verwendung von f in den Klauseln sich nicht auf die Applikation auf Argumente der Konstruktoren beschränkt. Dann liegt eine allgemeine (evtl. nichtterminierende) Rekursion vor, die mit gänzlich anderen Methoden zu untersuchen ist. Eine mögliche Vorgehensweise wird im Abschnitt 3.3 beschrieben.

2.2.6.2 Polymorphe ML-Datentypen

Die polymorphen ML–Datentypen wie zum Beispiel

datatype `p list1 = nil1 | cons1 of `p*list1

entsprechen den im letzten Abschnitt eingeführten parametrisierten T –Algebren. In diesem Beispiel ist T (P, X) = 1+P ×X. Leider stellt ML die Wirkung eines solchen polymorphen Datentyps auf Pfeile nicht als primitives Konstrukt zur Verfügung; der Benutzer kann diese aber jeweils selbst implementieren.

Hat der Signaturfunktor einer T –Algebra eine gewisse Form^{9}, so läßt sich umgekehrt die T –Algebra auch in ML modellieren. Der aufgrund der Initialität gegebene eindeutige Morphismus läßt sich in diesem Fall auch als ML–Funktion darstellen. Am (schon wiederholt benutzten) Beispiel der natürlichen Zahlen (also T (X) = 1 + X) sei dies erläutert:

datatype nat=zero | succ of nat;
signature NATALG=
sig
  type O;
  val z:X;
  val s:X->X;
end;
functor UNI(X:NATALG)=
  struct
    f=fun zero => X.z
          |succ n => X.s (f n);
end;

Bemerkung 2.2.6.2 Es können sich in ML auch zwei Datentypdeklarationen wechselseitig rekursiv aufrufen. Man denke an die trees und forests aus [BB85]. Diese lassen sich mit Hilfe von Produktkategorien bzw. cartesischen Produkten modellieren. Wie Thorsten Altenkirch in [Alt90] bemerkt, erlaubt ML schließlich auch kontravariante Signaturfunktoren, wie in

datatype junk = foo of junk->unit

(hier ist T (X) = X → 1); die Semantik solcher Ausdrücke muß über domain– Gleichungen erklärt werden.

Beides spielt in den Anwendungen eine untergeordnete Rolle und soll in dieser Arbeit nicht weiter untersucht werden.

9Er muß aus Konstanten, der Identität, +, ×, → und Funktoren, die aus parametrischen T – Algebren entstanden sind, zusammengesetzt sein.

2.3 Modularisierung

In diesem Abschnitt wird das Modulkonzept von ML typentheoretisch beschrieben — diese Darstellung folgt [MH88] — und, wie in der Einleitung angedeutet, auf die Verifikation ausgedehnt. Außerdem wird das modelltheoretisch erklärte sharing [ST86] typentheoretisch gefaßt. Da die Lego–Darstellung dieser Konzepte keine weiteren Überlegungen erfordert, beschreiben wir sie gleich in diesem Abschnitt.

Größere Programmsysteme lassen sich im allgemeinen nicht in einem Stück implementieren, geschweige denn verifizieren. Insbesondere wenn mehrere Menschen an einer Programmentwicklung beteiligt sind, ist es unumgänglich, die Implementierungsaufgabe in überschaubare Teile, sogenannte Moduln zu zerlegen, die separat implementiert und verifiziert werden können. Dies setzt freilich klar definierte Schnittstellen zwischen den Moduln voraus, die ein Zusammensetzen auch ohne genaue Kenntnis aller Implementierungsdetails ermöglichen. Außerdem sollten die Moduln nicht beliebige Stücke des Programmsystems darstellen, sondern ein oder mehrere sinngemäß zusammengehörige Teile der Gesamtaufgabe realisieren. Eine solche Unterteilung nur aufgrund der Problemstellung und ohne genaue Kenntnis der Lösung vorzunehmen, wird durch die Strategie der schrittweisen Verfeinerung ermöglicht (Für eine Beschreibung dieser Vorgehensweise cf. [MT]). Die Programmiersprache Standard–ML stellt mit ihrem Struktur– und Funktorkonzept eine Einrichtung zur Verfügung, die in logisch konsistenter Weise sowohl die schrittweise Verfeinerung unterstützt, als auch klar definierte Schnittstellen zwischen den einzelnen Moduln bereitstellt.

2.3.1 Das Modulkonzept von ML

Unter einer Struktur versteht man in ML eine gepackte Umgebung, also eine Zusammenfassung von (benutzerdefinierten) Typen, Konstanten und Funktionen. Diese Strukturen haben, wie alle ML–Objekte, einen Typ, der als Signatur bezeichnet wird. Aus der Signatur einer Struktur gehen alle Typen der in ihr enthaltenen Objekte hervor. Ein Funktor^{10} ist nun eine Abbildung zwischen Strukturen, man kann ihn (je nach Informationsgehalt der Argumentstruktur) wahlweise als — in einer anderen Struktur — parametrisierte Struktur, oder als echte Funktion von Strukturen auffassen. Der Typ eines Funktors ist SIG_{1} → SIG_{2}, wobei SIG_{1} der Typ (die Signatur) der Argumentstruktur und SIG_{2} der Typ der Resultatstruktur ist.^{11} Funktoren mehrerer Argumente erhält man formal durch Packen der Quellstrukturen zu einer einzigen und ausdrücklich nicht durch currying, da Funktoren selbst weder Quelle noch Ziel eines Funktors sein können. Diese Entscheidung wurde getroffen, um die Typisierung schon zur Übersetzungszeit überprüfbar zu machen, was bei beliebigen Funktoren höherer Ordnung nicht möglich ist (für neuere Ansätze in dieser Richtung cf. jedoch [Mog89, M^{+}90]).

10Die hier erklärten ML–Funktoren sind nicht mit den im letzten Abschnitt beschriebenen Endofunktoren von Kategorien zu verwechseln. Außer dem Namen bestehen wenig Gemeinsamkeiten

11Hängt auch die Zielsignatur von der Argumentstruktur ab — das kann bei gewissen sharing– Bedingungen der Fall sein —, so ist der Typ des Funktors entsprechend Πs_{1}:SIG_{1}.SIG_{2}(s)

Eine gegebene Spezifikation implementiert man zunächst als Funktor, dessen Argumentstrukturen zwar spezifiziert, aber noch nicht implementiert werden. Bei deren Implementierung geht man nach demselben Muster vor, bis schließlich die Teilaufgaben so überschaubar geworden sind, daß sie in einem Schritt implementiert werden können. Dadurch wird dem Prinzip der schrittweisen Verfeinerung Rechnung getragen. Im Gegensatz zu anderen Modularisierungskonzepten bleibt hier die Struktur der Programmentwicklung auch im fertigen Programm sichtbar — der top–down–Entwurf findet nicht nur auf dem Papier statt. Für eine genauere Beschreibung des Modulkonzepts von ML vgl. [Mac84].

2.3.2 Typentheoretische Verifikation

Was für die Implementierung gilt, gilt umsomehr noch für die Verifikation: Ein ”Ein– Schritt“–Korrektheitsbeweis eines größeren Programms ist praktisch unmöglich. Die Verifikation wird sich daher an der Modulstruktur des Programms orientieren. Ein formaler Ansatz für solche modulare Verifikation ist die von Sannella und Tarlecki entwickelte Sprache Extended–ML [ST86]. Hier wird jede Signatur um Axiome angereichert, die die Teile einer Struktur dieser Signatur beschreiben. Eine Implementierung einer Signatur besteht damit nicht mehr nur aus ML–Objekten, die die in der Signatur angegebenen ML–Typen realisieren, sondern auch aus Beweisen, daß diese die entsprechenden Axiome erfüllen. Bei Funktoren verhält es sich ganz analog; die Teile der Zielsignatur sind unter Verwendung von (hypothetischen) Elementen der Quellstruktur zu implementieren, die Korrektheitsbeweise werden unter Verwendung der (hypothetischen) Korrektheitsbeweise der Quellstruktur geführt. Damit wird eine (partielle) Verifikation schon während der Programmentwicklung möglich, der endgültige Korrektheitsbeweis des Gesamtsystems ergibt sich automatisch beim Zusammensetzen der beteiligten Moduln. Bei Extended ML werden nun — zumindest in der aktuellen Entwicklungsstufe — die Korrektheitsbeweise noch informell mit Bleistift und Papier geführt. Mit Hilfe des Beweisprüfers Lego ist es jedoch möglich, auch die Beweise formal und maschinenüberprüft zu führen. Da in Lego zwischen Typen und Aussagen (Axiomen), sowie Objekten und Beweisen kein wirklicher Unterschied besteht, verwischt sich in Lego auch der Unterschied zwischen Implementierung und Korrektheitsbeweis: Eine Lego–Spezifikation besteht aus einem strukturierten Typ, der sowohl die Typinformation, als auch die spezifizierenden Axiome enthält; ein Lego–Term, der diesen Typ realisiert, enthält automatisch Implementierung und Korrektheitsbeweise. Der type–checker überprüft nicht nur die Typen der implementierenden Objekte, sondern auch den Korrektheitsbeweis.

Funktoren sind in Lego ganz analog Abbildungen zwischen Strukturen, in denen nicht nur die Objekte, sondern auch die Beweise der Zielstruktur in denen der Argumentstruktur parametrisiert sind. Da Lego, wie in der Einleitung verdeutlicht, Objekte und Beweise identifiziert, ist es hier jedoch erforderlich, sicherzustellen, daß die Implementierung der Zielstruktur nicht von der Form des Korrektheitsbeweises der Argumentstruktur abhängt. Der Korrektheitsbeweis der Zielstruktur darf hingegen sowohl auf Implementierung, als auch auf den Korrektheitsbeweis der Quellstruktur zugreifen. Eine genauere Diskussion dieses Sachverhaltes und insbesondere dessen Zusammenhangs mit der sog. Grothendieck–Konstruktion findet sich in [BM90].

An dieser Stelle ist es vielleicht sinnvoll, darauf hinzuweisen, daß bei Extended ML die Programmiersprache nicht als Menge der Beweise (bzw. Objekte) der Spezifikationen, sondern als Teilmenge letzterer aufgefaßt wird. (”Programme sind ausführbare Spezifikationen“) Dies führt dazu, daß auch im Rumpf eines Extended– ML–Funktors Axiome, also logische Formeln stehen, die die noch nicht implementierten Teile des Funktors beschreiben.

In unserem Ansatz wollen wir dies jedoch nicht zulassen und Spezifikation und Implementation auch in den Fällen, wo erstere letztere eindeutig bestimmt (Horn–Klauseln, bestimmte ∀∃–Sätze, Harrop–Formeln), voneinander getrennt halten. Man hat also jeweils die noch nicht implementierten Teile eines Funktors der Argumentstruktur hinzuzufügen, bzw. sollte einen Funktor gleich in einem Schritt implementieren, was ja eigentlich auch durch die Zerlegung intendiert wird. Der Autor ist der Ansicht, daß dieser Umstand aufgrund des besseren typentheoretischen Verständnisses in Kauf genommen werden sollte.

Die oben ungenau postulierten ”strukturierten Typen“ werden in der Typentheorie als Σ–Typen, wegen ihrer Analogie zur kategoriellen Summe (Coprodukt), bezeichnet. Solch ein Σ–Typ hat die Form Σt:T.B(t), wobei T ein gewisses Typuniversum und B eine (durch einen Term in einer freien Typvariablen beschriebene) Abbildung von diesem Typuniversum in ein anderes bezeichnet. Ein Objekt des Σ–Typs besteht aus einem Paar (τ, b) mit τ:T und b:B(τ) (man denke an Implementierung und Korrektheitsbeweis). Je nach Art der Zugriffsmöglichkeiten unterscheidet man zwei Arten von Σ–Typen: Starke Σ–Typen stellen beide Projektionen π_{1}:Σt:T.B(t) → T und π_{2}:Πx:Σt:T.B(t).B(π_{1}(x)) zur Verfügung; während die sog. schwachen Σ–Typen oder intuitionistischen Existenzquantoren nur den Zugriff auf die erste, die Typkomponente, gestatten. Es ist als ”Girards–Paradoxon“ [Gir71] bekannt, daß starke Σ–Typen nicht imprädikativ sein können, in Lego also nicht mehr zu Prop gehören können. Starke Σ–Typen wurden von Luo in den calculus of constructions und in Lego eingeführt; in seiner Dissertation [Luo90] findet sich auch eine detaillierte Einführung in die typentheoretischen Grundlagen dieser Typen. Auf den genauen Zusammenhang starker Σ–Typen mit ML–Funktoren gehen Harper und Mitchell in [MH88] ein. Hier sei nur gesagt, daß in Lego ML–Signaturen als starke Σ–Typen und ML–Funktoren als Objekte des Typs Πs:S_{1}.S_{2}(s) für geeignete Σ–Typen S_{1} und (von s:S_{1} abhängiges) S_{2}.^{12} repräsentiert werden.

Auch unabhängig von Verifikationszwecken lassen sich Σ–Typen zur typentheoretischen Modellierung abstrakter Datentypen einsetzen (vgl. Abschnitt 2.1). Während Mitchell und Plotkin meinen, hierfür seien schwache Σ–Typen ausreichend (die in diesem Falle also nur den Zugriff auf den abstrakten Datentyp selbst, nicht aber auf seine Implementierung gestatten) [MP88], argumentiert MacQueen in seinem Papier [Mac84] dafür, daß nur starke und somit prädikative Σ–Typen abstrakte Datentypen adäquat modellieren. Eine genaue Untersuchung dieses Disputs mit Hilfe von Lego wäre sehr interessant und aufschlußreich, wurde jedoch in dieser Arbeit aus Zeit– und Platzgründen nicht durchgeführt.

12Die ”Grothendieck–Bedingung“ der Unabhängigkeit des Implementationsteils der Struktur Σ_{2} vom Beweisteil von S_{1} ließe sich explizit in Lego formulieren und zum Typ des Funktors hinzunehmen. (Dieser würde dann zu Πs_{1}:S_{1}.Σs_{2}:S_{2}(s_{1}).Gr(s_{1}, s_{2}), wobei Gr die Unabhängigkeit zum Ausdruck bringt.)

2.3.3 Sharing

Hat ein Funktor mehrere Argumentsignaturen, so ist es oft unvermeidlich, an deren Kompatibilität zusätzliche Forderungen zu stellen. So setzt die Anwendung eines Funktors, der aus zwei Ordnungsstrukturen deren Durchschnitt berechnet, voraus, daß die Grundmengen der beiden Argumentstrukturen übereinstimmen. Diese Zusatzbedingung wird als sharing bezeichnet. Bei der genauen Diskussion dieses Phänomens und dessen Lego–Modellierung wollen wir uns, um die Notation nicht zu überfrachten, an diesem auf Sannella zurückgehenden Beispiel orientieren; der allgemeine Fall sollte dadurch deutlich werden. In ML stellt sich die eben skizzierte Situation folgendermaßen dar:

signature PO =
  sig
     type elem
     val le:elem->elem->bool
  end

functor Cut(structure X : PO
            structure Y : PO
            sharing type X.elem = Y.elem) :  PO =
   struct
        type elem = X.elem
        fun le a b = (X.le a b) andalso (Y.le a b)
   end

Durch den Ausdruck sharing type X.elem = Y.elem wird zum Ausdruck gebracht, daß Cut nur auf solche Strukturen X und Y angewandt werden darf, deren Elementtyp übereinstimmt. Von dieser Forderung wird im Funktorrumpf auch wirklich Gebrauch gemacht; ohne die sharing–Bedingung wäre der Ausdruck Y.le a b nicht wohltypisiert, da a und b ja vom Typ X.elem sind. Für die typentheoretische Modellierung bietet sich zunächst die Einführung einer (mit ”=“ bezeichneten) Gleichheit von Typen an; mit dieser läßt sich das Argument von cut als Struktur des Typs ΣX:PO. ΣY:PO.X.elem = Y.elem spezifizieren. Im Funktorrumpf ist dann neben den Strukturen X und Y auch der Beweis für die Übereinstimmung ihrer Typkomponenten zugänglich. Daß dieser aber auch im Sinne von ML verwendet werden kann, setzt eine Typisierungsregel der Form

\frac{S = T, s:S}{s:T}

voraus. Eine solche war in Martin–Löfs System von ’84 in der Tat vorhanden [ML84], doch ist in diesem die Typisierungsrelation ”:“ nicht mehr entscheidbar und das System nicht mehr stark normalisierend. Der Grund dafür ist einfach der, daß dann im Kontext [H:D=(D->D)] der untypisierte λ–Kalkül dargestellt werden kann. Ein in [AL^{+}90] vorgeschlagener Ausweg besteht darin, in den Fällen, wo die Typisierung nicht automatisch überprüft werden kann, einen expliziten Beweis beizufügen. Der Standard–ML type–checker begegnet diesem Problem durch Beschränkung der sharing–constraints auf Pfade, d.h. auf Ausdrücke der Form

sharing S.A.B.C = T.X.Y.Z

Bedingungen wie D = D → D lassen sich dann nicht formulieren.

Lego stellt zur Formulierung der Gleichheit von Typen die Leibniz–Gleichheit Q zur Verfügung^{13}, welche aber keine Konvertierungsregel obiger Form hat. Man kann zwar für S,T:Prop aus (Q S T) aufgrund der Definition von Q eine Konvertierungsfunktion f:S->T herleiten, doch hat man keine Garantie, daß diese die Identität oder zumindest ein Isomorphismus ist. Diese Forderung ließe sich jedoch zur Argumentstruktur explizit hinzunehmen; sie würde dann zu

ΣX:PO . ΣY:PO . Σf:X.elem → Y.elem . X.elem = Y.elem ∧ iso(f, X, Y)

Bei dieser Vorgehensweise wäre jedoch für jede Anwendung das Prädikat ”iso“ neu und adäquat zu formulieren, was die Verifikation nicht unerheblich kompliziert.

Eine ganz andere Methode, das sharing zu modellieren, besteht in der expliziten Parametrisierung der Signaturen durch die Anteile, auf die später in einer sharing– Bedingung zugegriffen wird. In [Luo90, LB88] wird diese Vorgehensweise als ”sharing by parametrization“, bezeichnet. In unserem Beispiel wird dann PO die Grundmenge als freie Variable enthalten; die beiden Argumentsignaturen werden durch ein und dieselbe Grundmenge instantiiert:

PO(e) = e → e → bool
Cut : Πe.PO(e) → PO(e) → PO(e)

Daß PO hier kein Σ–Typ mehr ist, liegt daran, daß — aufgrund der Einfachheit des Beispiels — PO nur Typen enthält, auf die später durch sharing zugegriffen wird.

Auf diese Weise werden einerseits die Probleme mit der Typisierung bei sharing aus der Welt geschafft und andererseits die durch das sharing ins Spiel gebrachten verdeckten Abhängigkeiten von Typen expliziert. Auch die syntaktische Asymmetrie im Funktorrumpf von Cut (es wird X.elem und nicht Y.elem verwendet) tritt so nicht mehr auf. Der Preis, den man für diese Vorteile zu bezahlen hat, besteht darin, daß schon bei der Konzeption einer Struktur auf deren eventuelle spätere Verwendung in einem sharing–Konstrukt Rücksicht genommen werden muß. Bei der top–down– Programmentwicklung ist dies unerheblich, da hier ja die Verwendung einer Struktur vor deren Entwicklung steht; anders ist es bei Strukturen, die in einer Bibliothek für spätere noch nicht feststehende Verwendung zusammengefaßt sind. Hier sollten so viele Typen, wie (sinnvoll) möglich (etwa bei Listen der Typ der Einträge, bei Prozessen der Typ der Aktionen), durch Parametrisierung von außen zugänglich gemacht werden. Zum Abschluß geben wir — auch als Einführung in die Notation — die Lego–Darstellung des eben beschriebenen Beispiels an:

13Q[T|Type][s,t:T] == {P:T->Prop}(P s) -> P t

28 KAPITEL 2. GRUNDLAGEN

PO[elem:Prop] == le:elem -> elem -> bool;
Cut[elem:Prop][po1,po2:PO elem] ==
   [e1,e2:elem]andalso (po1 e1 e2)(po2 e1 e2):PO elem;

Im Beispiel aus Kapitel 4 finden sich weitere und auch kompliziertere Anwendungen dieser Methode.

Lego–Interpretationen

Die im letzten Kapitel beschriebenen Strukturen werden nun im Typensystem Lego modelliert. Dabei wurde die Grundentscheidung getroffen, die nichtmodularen Typen von ML, das sind Basistypen, datatypes, Funktions– und Produkttypen als Typen des imprädikativen Universums Prop darzustellen.^{1} Diese Entscheidung läßt sich begründen mit der ”tatsächlichen“ Imprädikativität induktiver Typen (die zugehörigen Kombinatoren lassen sich auf beliebige Typen, auch auf den Datentyp selbst anwenden). Ein formaleres Argument findet sich in [MH88], wo die ML– Basistypen im (imprädikativen) Universum U_{1} angesiedelt werden. Zu jedem Konstrukt werden Sätze formuliert und bewiesen, die es so genau eingrenzen, daß bei der Verwendung in den meisten Fällen eine Expansion in die Bestandteile oder gar in die Normalform vermieden werden kann.

Im ersten Abschnitt wird die Darstellung der T –Algebren und außerdem die Lego–Modellierung der Konzepte ”Induktion“ und ”primitive Rekursion“ beschrieben. Der zweite Abschnitt beschäftigt sich mit der Modellierung von Wahrheitswerten, Fallunterscheidungen sowie Gleichheit und im dritten Abschnitt werden die natürlichen Zahlen und eine (eingeschränkte) Form der allgemeinen Rekursion präsentiert.

3.1 T –Algebren in Lego

3.1.1 Darstellung von Kategorien

Die Objekte des Universums Propbilden mit den Funktionstermen als Morphismen, der üblichen Komposition von λ–Termen und der Leibniz–Gleichheit eine cartesisch abgeschlossene Kategorie PROP, über die — unter gewissen Annahmen — in Lego selbst gesprochen werden kann. In diesem Abschnitt wird nun die kategorielle Struktur von Prop beschrieben^{2}; dies bildet die Grundlage für die Darstellung der in Abschnitt 2.2 beschriebenen kategoriellen Datentypen als kleine Typen.

1Mit diesen Objekten sind Typen gemeint, die selbst den Typ Prop haben. Luo [Luo90] und Coquand [Coq90] bezeichnen diese als ”kleine Typen“.

2Diese Aussagen beziehen sich natürlich nicht nur auf die Kategorie der syntaktischen Terme selbst, sondern auf jedes andere Modell (etwa PER–Modell) von Prop, welches den im folgenden eingeführten Axiomen genügt. Siehe dazu auch Abschnitt 3.1.3.3.

30 KAPITEL 3. LEGO–INTERPRETATIONEN

3.1.1.1 Kategorienaxiome

Beginnen wir mit der Komposition: Durch

o[A,B,C|Prop][f:B->C][g:A->B] ==
[a:A]f(g a)

läßt sich diese als geschlossener Term formulieren. Das gleiche gilt für die Identitäten:

I[A|Prop] == [a:A]a

Ohne weitere Annahmen können wir nun beweisen, daß diese Definitionen den Kategorienaxiomen genügen^{3}:

[A,B,C,D:Prop][f:C->D][g:B->C][h:A->B]
[cat comp = (Q refl (o f(o g h))) :

Q(o f (o g h)) (o (o f g) h)]  Assoziativität von o
[cat I1= (Q refl h):  Q (o h (I|A)) h];  Rechtsneutralität von I
[cat I2= (Q refl h):  Q (o (I|B) h) h];  Linksneutralität von I

Discharge A;  Abstraktion vom Kontext

3.1.1.2 Kommutative Quadrate

Für kompliziertere Beweise nützlich ist folgende Definition kommutativer Quadrate:

commutes[A,B,C,D|Prop][a:A->B][b:A->C][c:B->D][d:C->D] ==
{x:A}Q (c (a x))(d (b x))

Der Satz (commutes |A|B|C|D a b c d) bringt zum Ausdruck, daß

                           [figure: C; D; d; A; B; a; b; c]

kommutiert. Kommutative Quadrate können zu weiteren zusammengesetzt werden; dies bringen wir durch folgendes Lemma zum Ausdruck:

commcomp:{A,B,C,D,E,F|Prop}
{a|A->B}{b|A->C}{c|B->D}{d|C->D}{e|C->E}{f|D->F}{g|E->F}
(commutes a b c d)->(commutes d e f g)->commutes a (o e b) (o f c) g == ...^{4}

Es bezieht sich auf die Situation

3Diese Beweise funktionieren nur unter Verwendung der η–Regel für Π–Typen. In der XCC n– Version von Lego sind diese implementiert.

4Hier und im folgenden wird durch ”== ...“ angedeutet, daß der Lego–Beweis der Aussage, bzw. der Lego–Term hier aus Übersichtlichkeitsgründen weggelassen wurde, sich aber im — separat erscheinenden — Anhang unter demselben Namen findet.

3.1. T –ALGEBREN IN LEGO 31

                                 [figure: E; F; g; C; D; d; e; f; C; D; A; B; a; b; c]

3.1.1.3 Terminales und initiales Objekt Durch den Typ der polymorphen Identität ist in PROP ein schwach terminales Objekt gegeben:

Unit == {A|Prop}A->A

Zu beliebig vorgegebenem Objekt A existiert ein Pfeil nach Unit:

xob[A|Prop]:A->Unit == [a:A]star, wobei
star:Unit == [A|Prop][a:A]a

Wir können von xob die Natürlichkeit beweisen:

unitnat:{A,B|Prop}{f:A->B}Q (xob|A) (o (xob|A f)) == ...

also, daß folgendes Diagramm kommutiert:

                                 [figure: B; Unit; xob|B; xob|A; A; f]

aber nicht die Eindeutigkeit (starke Terminalität), diese nehmen wir als Axiom an:^{5}

[uniteta:{A:Prop}{f:A->Unit}Q (xob|A) f]

bzw. dazu äquivalent in ”Elementform“:

unitind:{u:Unit}Q star u == ...

Ebenso haben wir ein a priori schwach initiales Objekt zur Verfügung, dessen Universalität wir ebenfalls als Axiom fordern:

Zero == {A|Prop}A
box[A|Prop]:Zero->A == [z:Zero]z|A
[zeroeta:{A:Prop}{f:Zero->A}Q (box|A) f];

Fassen wir Prop wieder als Typ der Sätze auf, so sind unser initiales und terminales Objekt nichts anderes, als die second–order–Codierungen des falschen und des wahren Satzes. Diese Analogie liegt auch der nun folgenden Darstellung von Produkt und Coprodukt zugrunde:

5Zur Begründung dieser und folgender Axiome siehe Abschnitt 3.1.3.3

32 KAPITEL 3. LEGO–INTERPRETATIONEN 3.1.1.4 Produkt und Coprodukt Durch die intuitionistische Konjunktion (A ∧ B := ∀C.(A → B → C) → C) ist in PROP ein ”schwaches“ Produkt gegeben durch

[A,B,C|Prop]
PROD [A,B:Prop] == {C|Prop}(A->B->C)->C

mit den Projektionen

pi1 [p:PROD A B] == p([a:A][ :B]a)
pi2 [p:PROD A B] == p([ :A][b:B]b)

und dem Kombinator

paar[f:C->A][g:C->B][c:C] == [X|Prop][h:A->B->X]h (f c)(g c):PROD A B

Manchmal ist es nützlich, den Kombinator auch in Elementform zur Verfügung zu haben:

pair[A,B|Prop][a:A][b:B]:PROD A B == [C|Prop][f:A->B->C]f a b

Die sogenannten β–Regeln für dieses Produkt können wir beweisen:

[C|Prop][f:C->A][g:C->B]
prod beta1 :  Q (o (pi1|A|B) (paar f g)) f == ...
prod beta2 :  Q (o (pi2|A|B) (paar f g)) g == ...
Discharge A;

In üblicher Notation lautet die erste β–Regel

π_{1}^{∘}⟨f, g⟩ = f für f:C → A, g:C → B

Die η–Regel müssen wir wiederum als Axiom postulieren:

[prod eta:{A,B,C:Prop}{h:C->PROD A B}
   Q h (paar (o (pi1|A|B) h) (o (pi2|A|B) h))]

In üblicher Notation:

h = ⟨π_{1}^{∘}h, π_{2}^{∘}h⟩ für h:C → A × B

Die Universalität des Produkts können wir nun aber herleiten [LS85]:

prod univ:{A,B,C|Prop}{f:C->A}{g:C->B}{u:C->PROD A B}
   (Q (o (pi1|A|B) u) f) -> (Q (o (pi2|A|B) u) g) -> (Q u (paar f g)) == ...

In ähnlicher Weise liefert die intuitionistische Disjunktion (A ∨ B := ∀C.(A → C) → (B → C) → C) ein (zunächst) schwaches Coprodukt, welches wir durch Postulierung der η–Regel zu einem wirklichen machen:

SUM [A,B:Prop] == {C|Prop}(A->C)->(B->C)->C
[A,B|Prop]

i1 [a:A] == [X|Prop][f:A->X][g:B->X](f a):SUM A B  Injektionen

i2 [b:B] == [X|Prop][f:A->X][g:B->X](g b):SUM A B

case == [s:SUM A B](s f g)  Kombinator

Die β-Regeln ([f, g]^{∘}ι_{1} = f; [f, g]^{∘}ι_{2} = g) lassen sich durch Normalisierung beweisen:

[C|Prop][f:A->C][g:B->C]
sum beta1 ==(Q refl f) :  Q (o (case f g)(i1|A|B)) f
sum beta2 = (Q refl g) :  Q (o (case f g)(i2|A|B)) g];

Discharge A;  Abstraktion vom Kontext

Die η–Regel ([h^{∘}ι_{1}, h^{∘}ι_{2}] = h) postulieren wir:

[sum eta:{A,B,C:Prop}{h:(SUM A B)->C}
Q (case (o h (i1|A|B))(o h (i2|A|B))) h]

Aus dieser läßt sich die Universalität beweisen:

sum univ:{A,B,C|Prop}{f:A->C}{g:B->C}{u:(SUM A B)->C}
(Q (o u (i1|A|B)) f) -> (Q (o u (i2|A|B)) g) -> (Q u (case f g)) == ...

und — was für die spätere Verwendung des Coprodukts als Teil von Signaturfunktoren wichtiger ist — folgendes ”Induktionsprinzip“:

sumind:{A,B:Prop}{P:(SUM A B)->Prop}
({a:A}P(i1 a)) -> ({b:B}P(i2 b)) -> {x:SUM A B}P x == ...

Intuitiv bringt dieses zum Ausdruck, daß das Coprodukt nur die durch die Injektionen gelieferten Elemente enthält. Eine Eigenschaft, die auf dem Bild der beiden Injektionen erfüllt ist, gilt auf dem gesamten Coprodukt.

Funktorialität von PROD und SUM Es ist bekannt, daß sich die Objektabbildungen ‘Produkt’ und ‘Coprodukt’ durch

f × g := ⟨f^{∘}π_{1}, g^{∘}π_{2}⟩ bzw.
f + g := [ι_{1}^{∘}f, ι_{2}^{∘}g]

zu covarianten Bifunktoren erweitern lassen; diese Erweiterung können wir auch in Lego vornehmen und auch die Funktorialität von + und × — da diese nur von den β–Regeln und der Natürlichkeit abhängen auch ohne Verwendung der η–Regeln — beweisen.

3.1.1.5 Exponentenobjekte

Die Pfeil–Typen A->B bilden in PROP Exponentenobjekte, die Kombinatoren ”curry“ und ”uncurry“ lassen sich definieren:

curry[A,B,C|Prop][f:(PROD A B)->C] == [a:A][b:B]f(pair a b)
uncurry[A,B,C|Prop][f:A->B->C] == [axb:PROD A B]f (pi1 axb)(pi2 axb)

Es läßt sich in Lego beweisen, daß curry Isomorphismus mit Inversem uncurry ist und auch die Natürlichkeit dieser beiden Transformationen.

Wir haben somit die Basis geschaffen für die Darstellung der ML–Typen und Funktionen als kategorielle Datentypen im Universum PROP. Die folgenden Konstruktionen von Endofunktoren und T –Algebren beziehen sich immer auf die hier beschriebene Kategorie.

3.1.2 Darstellung von Funktoren

Das Ziel ist es nun, zu den in Abschnitt 2.2 beschriebenen kategoriellen Datentypen (T –Algebren) geschlossene Lego–Terme zu finden, die diese in der Kategorie PROP repräsentieren. Wir werden sogar einen geschlossenen Term bestimmen, der zu jedem beliebig vorgegebenen Signaturfunktor die initiale T –Algebra bestimmt (samt den zugehörigen Kombinatoren). Dies setzt voraus, daß wir den Begriff des Funktors als Lego–Typ darstellen und uns fragen, welche Funktoren dann in diesem Sinne eine Darstellung als Lego–Terme besitzen. Der Begriff der Darstellbarkeit eines Funktors erscheint erstmals bei Reynolds in seinem Nachweis der Nichtexistenz mengentheoretischer Modelle für den polymorphen λ–Kalkül [RP88]. Auf Lego übertragen ist ein covarianter Endofunktor eines kategoriellen Modells darstellbar, wenn es ge-

schlossene Lego–Terme T:Prop -> Prop und Tm:{X,Y|Prop}(X->Y) -> (T X) ->

(T Y)^{6} gibt, die auf der Modellebene seine Objekt– bzw. Pfeilabbildung beschreiben. Wir können im Sinne der Programmverifikation zusätzlich einen geschlossenen Lego–Term postulieren, der die Funktorialität von Tm bzgl. T beweist. Der Typ ”covarianter Funktor“ wird damit zu einem Tripel:

FuncP ==

<T: Prop -> Prop>  Objektabbildung

   <Tm: {X,Y|Prop}(X->Y) -> (T X)->(T Y)>  Pfeilabbildung
      ({X:Prop}Q (I|(T X)) (Tm (I|X)))  Erhaltung der Identitäten

⋀  ”und“

      ({X,Y,Z:Prop}{f:X->Y}{g:Y->Z}

         Q (Tm (o g f)) (o (Tm g) (Tm f)))  Erhaltung der Komposition

Covariante Funktoren in Lego sind damit Objekte des Typs FuncP. Für contravariante Funktoren kann in analoger Weise ein Typ FuncM definiert werden. Es erhebt sich nun die natürliche Frage nach einer semantischen Charakterisierung der in dieser strengen Weise in Lego darstellbaren Funktoren. Die auf den ersten Blick vielleicht erstaunliche Antwort lautet, daß für die Darstellbarkeit eines Funktors schon die Darstellbarkeit seiner Objektabbildung als Term des Typs Prop->Prop ausreicht. Der Beweis dieser Tatsache findet sich in [Alt90]. Thorsten Altenkirch gibt sogar Lego–Terme

6Einen solchen Term, der die Wirkung eines Funktors auf Pfeile internalisiert, bezeichnen Wraith [Wra89] und Kock [Koc70] auch als sog. strength (Stärke) des Funktors. Dies deshalb, weil ein Funktor dessen Wirkung auf Pfeile einer cartesisch abgeschlossenen Kategorie durch eine natürliche Transformation der entsprechenden Exponentenobjekte beschrieben werden kann, als starker Funktor (strong functor) bezeichnet wird.

ArrowP:FuncM->FuncP->FuncP  wobei ArrowP(F, G)(X) = F (X) → G(X)

ArrowM:FuncP->FuncM->FuncM  wie oben, aber Varianzen umgekehrt
PiP:(Prop->FuncP)->FuncP  wobei PiP(λX.F (X))(Y) = ΠX.F (X)(Y)
PiM:(Prop->FuncM)->FuncM  wie oben, aber Varianzen umgekehrt

welche es erlauben, aus der Lego–Darstellung der Objektabbildung (die sich auf der untersten Ebene ja aus Pfeilen und Produkten konstanter Funktoren, bzw. der Identität zusammensetzen) die Lego–Darstellung des Funktors als Tripel abzuleiten. Auf diese Weise wird der Beweis internalisiert und konstruktiv gemacht.

Für unsere Zwecke benötigen wir jedoch nicht diese allgemeinen Operatoren, sondern nur solche für das Produkt und Coprodukt, welche sich aus den oben genannten Kombinatoren zusammensetzen lassen:

PLUS:FuncP->FuncP->FuncP == ...  wobei PLUS(F, G)(X) = F (X) + G(X)
TIMES:FuncP->FuncP->FuncP == ...  wobei TIMES(F, G)(X) = F (X) × G(X)

Außerdem Kombinatoren für konstante Funktoren und die Identität:

KP:Prop->FuncP  wobei KP(A)(X) = A
ID:FuncP  wobei ID(X) = X

Mit Hilfe dieser Kombinatoren, lassen sich alle polynomialen Funktoren — also die Signaturfunktoren der meisten praktisch vorkommenden Datentypen — zusammensetzen; der Beweis für deren Funktorialität braucht dann nicht jeweils neu geführt zu werden, sondern ergibt sich einfach als Projektion des entsprechenden Terms auf die Beweiskomponente. Als Beispiel wollen wir den Signaturfunktor für beschriftete binäre Bäume in dieser Weise darstellen: Es ist T_{ltree}(X) = 1 + E × X × X, falls die Wurzel unbeschriftet ist. In Lego schreiben wir also

LTREESIG == PLUS (KP Unit) (TIMES E (TIMES ID ID))

und erhalten mit LTREESIG.1 die Wirkung des Funktors auf Objekte, mit LTREESIG.2.1 seine Wirkung auf Pfeile und über LTREESIG.2.2 den Beweis für die Funktorialität.

3.1.3 T –Algebren nach Church und Wraith

Notation: Die nun folgenden Konstruktionen beziehen sich auf das PLC– Fragment des ECC, wir schreiben daher der Übersichtlichkeit halber des öfteren ∀α anstelle von {A|Prop}, λa:A statt [a:A] und ΛA anstatt [A|Prop].

3.1.3.1 Einführung

Zur Darstellung von T –Algebren in Lego wollen wir die von verschiedenen Autoren vorgeschlagene Verallgemeinerung der Church–Datentypen einsetzen. Dieser liegt die wohl auf [GTWW77] zurückgehende Auffassung von Datentypen als (eingefrorenen) Kontrollstrukturen zugrunde. Am Beipiel der booleans sei dies verdeutlicht. Das zu den Wahrheitswerten gehörige Konstrukt ist die Fallunterscheidung des (polymorphen) Typs

bool → ∀α.α → α → α

welche einen Wahrheitswert und zwei Werte eines beliebigen Typs A auf ein Element von A abbildet. Dies kann man auch als Abbildung von bool in den polymorphen Typ ∀α.α → α → α deuten (vgl. die Abbildung eines Rings in die Homomorphismengruppe eines seiner Moduln). Diese Abbildung ist injektiv — zwei Wahrheitswerte, die sich in ihrer Wirkung als ”Fallunterscheider“ nicht unterscheiden, sind gleich. Fordert man von einer polymorphen Funktions des Typs ∀α.α → α → α andererseits, daß sie uniform für alle Typen arbeite, so kann sie nur eine der beiden Projektionen sein. In diesem Falle ist die oben beschriebene Abbildung also sogar ein Isomorphismus.

Dies ist der semantische Hintergrund für die nun folgende Darstellung von T – Algebren in Lego (bzw. im PLC)

3.1.3.2 Church–Datentypen

Church definiert zu jeder natürlichen Zahl n einen geschlossenen λ–Term, das sogenannte Numeral

ñ := λfλx. \underbrace{f(f(f ⋯ (f}_{n Stück} x))) ⋯)

welches zu einer Funktion deren n–fach Iterierte bestimmt. Man kann nun zu jeder berechenbaren Funktion einen geschlossenen λ–Term angeben, der angewandt auf ein Numeral die Numeraldarstellung des Funktionswertes liefert [Bar84].

Diese Darstellung der natürlichen Zahlen als Iteratoren hebt ihren ordinalen, operierenden Charakter hervor, was ja auch ihrer programmiersprachlichen Verwendung entspricht.

Analog lassen sich Listen als λ–Terme der Form

λc.λn.c e_{1}(c e_{2} ⋯ (c e_{ℓ} n) ⋯)

definieren. Auch das betont deren Rolle als Iterationsschemata.

Wir wollen nun mögliche Typisierungen dieser Terme im polymorphen λ–Kalkül betrachten. Im Falle der Numeralia kann x beliebigen Typ α haben, f muß dann aber vom Typ α → α sein (außer bei ˜1, wo nur der domain von f fixiert ist). Das Resultat der Anwendung eines Numerals auf einen Funktionsterm des Typs α → α und einen Term des Typs α ist wiederum vom Typ α, so daß den Church–Numeralia der polymorphe Typ

polynat := ∀α.(α → α) → α → α

zugesprochen werden kann. Eine ähnliche Überlegung für die Church–Listen führt — falls die Einträge e_{i} den gemeinsamen Typ β haben — auf

polylist := ∀α.α → (β → α → α) → α

den Typ der polymorphen Listen.

Da nun andererseits — wie man durch ein Church–Rosser Argument zeigen kann — die Normalformen von PLC–Termen des Typs polynat gerade die Church– Numeralia und die Normalformen von Termen des Typs polylist^{7} gerade die Church–Listen sind, erscheint die Verwendung dieser Typen als Darstellung der natürlichen Zahlen, bzw. der Listen im PLC gerechtfertigt.

Diese Beobachtung läßt sich auf beliebige finitäre mehrsortige Signaturen verallgemeinern; Böhm und Berarducci geben zu jeder solchen Signatur einen PLC– Typausdruck an, dessen geschlossenen Terme — zusammen mit auch als geschlossene Terme darstellbaren Konstruktoren — eine initiale Algebra zu dieser Signatur bilden [BB85].

Da der polymorphe λ–Kalkül im Gegensatz zum untypisierten stark normalisierend ist, können natürlich nicht alle berechenbaren Funktionen als geschlossene Terme des Typs polynat → polynat dargestellt werden. Jedoch zeigt Girard [Gir71], daß jede Funktion, deren Totalität in der Arithmetik zweiter Ordnung beweisbar ist, als PLC–Term des Typs polynat → polynat repräsentiert werden kann. Diese Funktionenklasse schließt die primitiv rekursiven Funktionen, aber auch die Ackermann–Funktion mit ein; nicht–akademische Beispiele von Funktionen, die nicht zu dieser Klasse gehören, sind bislang nicht bekannt. Dieses Resultat überträgt sich via Codierung natürlich auch auf die nach Böhm und Berarducci gegebenen Ausdrücke für freie Algebren.

Um nun diese Resultate auf beliebige T –Algebren zu erweitern, verwenden wir die in Abschnitt 3.1.1 beschriebenen Darstellungen von Produkt und Coprodukt. Mit Hilfe der Isomorphismen

(A + B → C) ≅ (A → C) × (B → C)^{8}
(A × B) → C ≅ A → B → C
A × B ≅ B × A
(A + B) × C ≅ (A × C) + (B × C)
1 × A ≅ A × 1 ≅ A

welche aus den βη–Regeln für Produkt und Coprodukt folgen, können wir dann den Ausdruck für polynat umformen zu

∀α.((1 + α) → α) → α

7Für die Listen trifft dies nur zu, wenn der Typ der Einträge eine freie Typvariable im Sinne von [BB85] ist.

8Der besseren Lesbarkeit wegen haben wir hier statt SUM und PROD die übliche Infixnotation gewählt.

Hier erkennen wir den Signaturfunktor der natürlichen Zahlen wieder: Mit T (X) = 1 + X ist

polynat ≅ ∀α.(T (α) → α) → α

Dieser Ausdruck läßt sich ganz natürlich auf solche T –Algebren verallgemeinern, deren Signaturfunktor im PLC (bzw. in Lego) im Sinne des letzten Abschnittes darstellbar ist. In der Tat zeigt folgende auf Reynolds [RP88] zurückgehende Überlegung, daß in jedem kategoriellen Modell des PLC der Ausdruck

A := ∀α.(T (α) → α) → α

als schwach initiale T –Algebra interpretiert wird: Ein Vertreter a dieses Typs ist eine polymorphe Funktion, die zu einem beliebigen Typ X und einer Funktion T (X) → X, also zu einer (nicht notwendigerweise initialen) T –Algebra ein Element ihres Trägers bestimmt, welches wir als Resultat der Applikation des kraft schwacher Initialität gegebenen Morphismus auf a interpretieren. Diese Überlegung liefert uns den PLC–Ausdruck für diesen Morphismus:

uni := Λα.λf:(T α) → α.λa : A.a α f: ∀α.((T α) → α) → (A → α)

Aufgrund der Imprädikativität des PLC können wir, wie folgt, auch einen Term vom Typ (T A) → A konstruieren, der als Strukturmorphismus interpretiert wird.

φ := λx : T (A). \underbrace{Λα.λf:T (α) → α.}_{Wir geben uns α,f vor...} \underbrace{f((T (uni α f))x)}_{und konstruie- ren einen Term des Typs α}

(Man kann an dieser Stelle versuchen, den Term φ von Hand oder mit Hilfe von Lego zu erstellen, um seine Struktur besser zu durchschauen, siehe unten.) Mit dieser Wahl von ‘uni’ und φ kommutiert nun das relevante Diagramm syntaktisch, d.h. es ist für alle Typen α und Terme f:T (α) → α

λx:T (A).uni(φx) =_{β} λx:T (A).f(T (uni)x)

Damit ist gezeigt, daß jedes kategorielle Modell des PLC ein schwach initiales Objekt zu jedem im PLC darstellbaren Funktor besitzt. Daraus ergibt sich auch die Unmöglichkeit eines mengentheoretischen Modells des PLC, da es in Set aus Kardinalitätsgründen keine schwach initiale T –Algebra zum Signaturfunktor T (X) := (X → polybool) → polybool — welcher darstellbar ist — geben kann.

3.1.3.3 Initialität

Es existieren nun aber parametrische (PER–) Modelle des PLC, in denen der Ausdruck ∀α.((1 + α) → α) → α sogar als initiale T –Algebra interpretiert wird, was die axiomatische Hinzunahme der Eindeutigkeit von ‘uni’ als Axiom rechtfertigt [BFŠS90, Hyl82, Šče90]. In diesen Modellen gelten auch die — im Abschnitt 3.1.1 — postulierten η–Regeln für das schwache Produkt und Coprodukt, sodaß auch diese gerechtfertigt sind.

Bemerkung 3.1.3.1 G. Wraith [Wra89] macht darauf aufmerksam, daß auch schwach terminale T –Coalgebren (z.B. streams, vgl. 2.2) eine Darstellung im PLC haben. In der Tat wird der Ausdruck

∃α.(α → T (α)) × α

als schwach terminale T –Coalgebra mit geschlossenen Termen als Strukturmorphismus und Kombinator interpretiert. Man kann auch hier die starke Terminalität fordern, ob dies jedoch in den parametrischen Modellen zulässig ist, scheint noch offen zu sein.

Kehren wir nun zu Lego zurück: Im Kontext

[T:FuncP];  Ein beliebiger covarianter (Signatur–)Funktor

können wir den Ausdruck für die T –Algebra definieren

datatype == {C|Prop}((T.1 C)->C)->C

außerdem den Kombinator ‘uni’:

uni:{X|Prop}((T.1 X)->X)->datatype->X ==
   [X|Prop][f:(T.1 X)->X][dt:datatype]dt|X f

und den Strukturmorphismus:

phi:(T.1 datatype)->datatype ==
   [H:T.1 datatype][C|Prop][f:(T.1 C)->C]f (T.2.1 (uni C f) H)

Die Entstehung des Terms für den Strukturmorphismus wird deutlicher, wenn wir ihn interaktiv mit Lego konstruieren:

Goal (T.1 datatype)->datatype;

Intros Tdt;  Wir geben das Argument des Typs T.1 datatype vor
Intros C f;  ...und die Argumente des zu konstruierenden datatype
?3:  C  Es bleibt ein Vertreter von C zu konstruieren

Refine f;                                                            C ist Ziel von f

?4:  T.1 C  Dieses Ziel ließe sich mit (T.1 datatype)->T.1 C lösen
Refine T.2.1 (uni C f)  Der mit T geliftete Kombinator hat diesen Typ

Refine Tdt; *** QED ***

Durch Discharge T abstrahieren wir nun vom Kontext [T:FuncP]. Wir können jetzt die starke Initialität von datatype — mit Hilfe der Leibniz–Gleichheit — formulieren:

Ini == {T:FuncP}{X:Prop}[A=datatype T][TX=T.1 X]
{f:TX->X}{u:A->X}[ph=phi T][Tu=T.2.1 u]

(commutes ph Tu u f)->Q u (uni T X f)  Dies ist die eigentliche Aussage

und dem Kontext als Postulat hinzufügen:

[ini:Ini]

Dadurch wird die Modellklasse auf die parametrischen Modelle eingeschränkt. Gerade die sind es jedoch, die uns für die Modellierung einer Programmiersprache interessieren.

3.1.4 Primitive Rekursion

Wir können nun, wie in Abschnitt 2.2 beschrieben, auch primitive Rekursion definieren. Im Kontext

[T:FuncP][R|Prop]  Signaturfunktor und Resultattyp

setzen wir dazu

recscheme == [A=datatype T][TAxR=T.1 (PROD A R)]TAxR->R

und definieren primitive Rekursion durch

primrec[psi:recscheme] ==
o (pi2|?|?)
  (uni T (PROD (datatype T) R)
         (paar (o (phi T) (T.2.1 (pi1|?|?)))  psi))

Der Kombinator primrec liefert also zu vorgegebenem primitiven Rekursionsschema die eindeutig bestimmte Lösung. Das können wir in Lego (aus der Initialität) beweisen:

primreclaws: {psi:recscheme}[ph=phi T]
commutes ph (T.2.1 (paar (I|A) primrec)) (primrec psi) psi == ...

3.1.5 Induktion

In diesem Abschnitt soll gezeigt werden, wie der beschriebene kategorielle Zusammenhang von Induktion und Initialität auch in Lego dazu verwendet werden kann, aus einem allgemeinen Initialitätsaxiom ein der allgemeinen kategoriellen Induktion vergleichbares Prinzip und auch die speziellen Induktionsaxiome für die natürlichen Zahlen, die booleans etc. herzuleiten.

Das Problem dabei ist, daß die kategorielle Konstruktion ausgiebig von Unterobjekten und Differenzkernen — beides Objekte, die als solche in Lego nicht existieren — Gebrauch macht. Um die Situation zu konkretisieren, wollen wir uns einen Typ und ein Prädikat über diesem vorgeben:

[A|Prop]
[P:A->Prop]

Gesucht wäre ein Objekt sub P : Prop, welches diejenigen Individuen von A, auf die die Eigenschaft P zutrifft, zusammenfaßt. Zu diesem Zweck bietet sich zunächst der intuitionistische Existenzquantor an

ex == {B:Prop}({a:A}B)->B

dessen Beweise (also Individuen) in Normalform ja gerade aus Paaren (a, p) mit a:A und p : Pa bestehen. Es lassen sich zusätzlich Terme

ex intro:{a:A}(P a) -> ex == ...

und

witness:ex -> A == ...

definieren, derart daß witness die erste Komponente eines Existenzbeweises zu extrahieren gestattet:

ex eta:{a:A}{p:P a} Q a (witness (ex intro a p) == ...

Leider ist jedoch die zweite Projektion, d.i. die Extraktion des zugehörigen Beweises nicht definierbar, obwohl auf der Meta–Ebene bekannt ist, daß alle Beweise der Existenzaussage durch ex intro, also durch das Paar Zeuge–Beweis, entstanden sind. Wir können somit nicht beweisen, daß

{h:ex} P (witness h)

gilt. Gerade dies ist aber für die Konstruktion aus dem letzten Abschnitt erforderlich. Nun ist es so, daß für allgemeine Existenzquantoren, d.h. solche in denen auch über Prop selbst oder noch höhere Typen quantifiziert wird, die Annahme einer derartigen Projektion auf die Beweiskomponente sogar inkonsistent wäre (Girards Paradoxon). Wird jedoch, wie in unserem Fall, nur über kleine Typen, also solche, die selbst den Typ Prop haben, quantifiziert, so kann die zweite Projektion nicht nur als Axiom, sondern unter Erhaltung der starken Normalisierung sogar als (implementierte) Schlußregel hinzugenommen werden [Luo90]. Man spricht dann nicht mehr von intuitionistischen Existenzquantoren, sondern von kleinen Σ–Typen. Diese sind in der verwendeten Lego–Version realisiert. Wir können daher definieren:

sub == <a:A>P a
sub intro:{a:A}(P a) -> sub == [a:A][p:P a]((a,p):sub)

iota:sub->A == [u:sub]u.1  Projektion auf die erste Komponente

und sowohl die auch für den Existenzquantor gültige η–Regel, als auch die Korrektheit des Σ–Typs beweisen:

Piota:{u:sub} P (iota u) == u.2  Projektion auf die zweite Komponente

sub eta:{a:A}{p:P a} Q a (iota (sub intro a p)) ==

[a:A][ :P a] Q refl a  durch Normalisierung

Nun entspricht dieser Untermengenkonstruktor noch immer nicht dem kategoriellen Konstrukt, da die ”Inklusion“ iota im allgemeinen nicht injektiv ist: Falls für ein Individuum a:A die Tatsache, daß P auf a zutrifft, zwei verschiedene Beweise p1,p2:P a gestattet, so ist

(iota (sub intro a p1)) = (iota (sub intro a p2)) = a

obwohl natürlich (sub intro a p1) von (sub intro a p2) verschieden ist. Wir werden daher nicht, wie in der kategoriellen Version, zeigen können, daß sub zu A isomorph ist (Falls sub überhaupt die Induktionsvoraussetzungen erfüllt), sondern nur — was aber eigentlich ja genau das Gewünschte ist —, daß {a:A}P a gilt, die Eigenschaft P also universell ist. Konkret bedeutet das, daß wir aus der Lego– Formulierung der Initialität^{9} aus dem letzten Abschnitt folgende Formulierung der Induktion herleiten können:

indcat:{T:FuncP}[A=datatype T]{P:A->Prop}[U=sub P][TU=T.1 U]
[TA=T.1 A][i=iota|A|P][Ti=T.2.1 i]
[ph=phi T]{f:TU->U}

   (commutes f Ti i ph) -> {a:A}P a == ...  die eigentliche Aussage

Bedenken wir, daß auch der Morphismus f:TU->U nur eingeführt wurde, um die Stabilität von U unter dem Strukturmorphismus phi kategoriell zu fassen, so können wir — da wir in Lego ja auch über Elemente sprechen können — dies weiter vereinfachen zu

indlog:{T:FuncP}[A=datatype T]{P:A->Prop}[U=sub P][i=iota|A|P]
[ph=phi T][Ti=T.2.1 i][TU=T.1 U]
   ({tu:TU}P (ph (Ti tu))) -> {a:A}P a

Der Lego–Herleitung von indcat folgt weitgehend dem beschriebenen kategoriellen Beweis und verwendet wie dieser das Lemma

eta:Q (uni T A ph) (I|A) == ...

Der Beweis von indlog ergibt sich in einfacher Weise aus den Konversionsregeln für die kleinen Σ–Typen. Aus indlog lassen sich dann unter Verwendung von sumind und unitind (vgl. 3.1.1) die gewohnten Induktionsprinzipien für bool =

datatype (PLUS ONE ONE) und nat = datatype (PLUS ONE ID) herleiten (vgl.

die Abschnitte 3.2, 3.3).

3.1.5.1 Initiale T -Algebren durch kleine Σ-Typen

An dieser Stelle ist es vielleicht sinnvoll, darauf hinzuweisen, daß wir mit Hilfe der kleinen Σ–Typen sogar T –Algebren definieren können, für die sich ein Induktionsprinzip im leeren Kontext beweisen läßt, wir folglich ohne das Initialitätsaxiom auskommen. Am Beispiel der natürlichen Zahlen sei dies gezeigt. Wir definieren zunächst wie gehabt:

pre nat == {A|Prop}A->(A->A)->A^{10}
pre zero:pre nat == [A|Prop][z:A][s:A->A]z
pre succ[n:pre nat] == [A|Prop][z:A][s:A->A]s(n z s)

11 Und können nun ein Prädikat definieren, welches zum Ausdruck bringt, daß ein bestimmtes Objekt des Typs pre nat von zero durch succ erreichbar ist:

9Von den beliebig aber fest vorgegebenen Objekten A und P haben wir durch Discharge A abstrahiert.

11Daß hier die Church–Darstellung und nicht die datatype–Darstellung gewählt wurde, ist unerheblich.

3.2. WAHRHEITSWERTE, GLEICHHEIT UND FALLUNTERSCHEIDUNG 43

reachable[n:pre nat] == P:pre nat->Prop

   (P pre zero)->  Falls P für zero gilt
   (n:pre nat(P n)->P (pre succ n))  und unter succ abgeschlossen ist,

->P n  dann soll es auf n zutreffen.

Mit der beschriebenen (Pseudo–)Untermengenkonstruktion können wir nun den Typ nat als das Unterobjekt der erreichbaren pre nat’s definieren:

nat ==<n:pre nat>reachable n

Auf nat lassen sich die Funktionen zero und succ definieren, wobei natürlich die zweite Komponente der Funktion succ aus dem Erreichbarkeitsbeweis des Arguments einen solchen für das Resultat produzieren muß. Leider gibt jetzt jedoch die Leibniz–Gleichheit nicht mehr die erwartete Beobachtungsäquivalenz auf nat wieder [ST87], da sich ja zwei Objekte des Typs nat, obwohl in der ersten Komponente gleich, im Beweis für ihre Erreichbarkeit unterscheiden können. Deshalb definieren wir

eq[m,n:nat] == Q m.1 n.1

Das gleiche gilt auch für andere Prädikate; sinnvoll sind nur solche, die die Form des Beweises nicht berücksichtigen. Solche wollen wir als kohärent bezeichnen:

coherent[P:nat->Prop] == {m,n:nat}(eq m n) -> (P m) -> P n

Für solche kohärente Eigenschaften können wir nun in der Tat folgendes Induktionsprinzip beweisen, ohne auf irgendwelche Axiome zurückzugreifen:

Goal {P:nat->Prop}(coherent P)->(P zero)->
    ({n:nat}(P n)->P (succ n))->{n:nat}P n;
...

Da die Kohärenzbeweise für jedes Prädikat und jede Funktion neu zu führen sind (das könnte zwar teilweise automatisiert werden), wollen wir diese Darstellung für unser Vorhaben aber nicht einsetzen.

3.2 Wahrheitswerte, Gleichheit und Fallunterscheidung

3.2.1 Wahrheitswerte

In diesem Abschnitt sollen die Lego-Darstellung des Datentyps bool der Wahrheitswerte und einige seiner Eigenschaften und Verwendungsmöglichkeiten beschrieben werden. In ML ist bool erklärt als

datatype bool = true | false

Dies führt auf den Lego–Ausdruck

BOOLSIG == PLUS ONE ONE
bool == datatype BOOLSIG

bool hat daher zwei ausgezeichnete Vertreter

true == phi BOOLSIG (i1 star)^{12}
false == phi BOOLSIG (i2 star)

— die beiden Komponenten des zu BOOLSIG gehörigen Strukturmorphismus. Den zu bool gehörigen Iterator (uni BOOLSIG) bezeichnen wir (nach einer kleinen Umordnung der Argumente) mit if:

if[A|Prop][b:bool][a1,a2:A] ==
          uni BOOLSIG (case ([ :Unit]a1)([ :Unit]a2)

Steht if zur Verfügung, so lassen sich in bekannter Weise auch die anderen Boole’schen Funktionen darstellen:

orelse[b1,b2:bool] == if b1 true b2
andalso[b1,b2:bool] == if b1 b2 false
implies[b1,b2:bool == if b1 b2 true
negate[b:bool] == if b false true

Aus dem Initialitätsaxiom für T –Algebren können wir folgendes Induktionsprinzip für bool herleiten:

boolind:{P:bool->Prop}(P true)->(P false)->b:boolP b == ...

welches zum Ausdruck bringt, daß true und false die einzigen (beobachtbaren) Vertreter des Typs bool sind.

Dies impliziert erstaunlicherweise noch nicht die Konsistenz, also not (Q true false); jedoch hätte true = false zur Folge, daß je zwei Vertreter eines beliebigen (kleinen) Typs (Leibniz–)gleich sind. In der Tat existiert ein Modell des CC — das sogenannte proof–irrelevance–Modell [Coq90] — in dem das der Fall ist. Um dieses auszuschließen, fordern wir einen Typ mit zwei unterscheidbaren Objekten:

[zen:Prop]
[yin,yang:zen]
[yinisnotyang:not (Q yin yang)]^{13}

und können damit die Konsistenz beweisen:

consistency:  not (Q true false) == ...  yinisnotyang ...

Man hätte natürlich auch direkt die Konsistenz fordern können, doch wird auf diese Weise die Lage des Problems deutlicher.

Die hauptsächliche Bedeutung des Typs bool liegt in seiner Verwendung als Wertebereich von Relationen bzw. Eigenschaften. In Lego steht dafür ja bekanntlich auch der Typ Prop selbst zur Verfügung und in der Tat läßt sich bool über die Funktionen

12siehe Abschnitt 3.1.1.

13Die Wahl dieser Bezeichnungen hat keine weltanschaulichen Gründe.

isthecase[b:bool] == Q true b
isnotthecase[b:bool] == Q false b

jederzeit nach Prop überführen. Das Umgekehrte ist freilich nur eingeschränkt möglich, da sich für bool folgende Entscheidbarkeitseigenschaft zeigen läßt:

bycases:{b:bool}or (isthecase b)(isnotthecase b)

== Ausdruck mit boolind^{14}

die ja — das ist das zentrale Dogma des Intuitionismus — für Prop gerade nicht allgemein gilt. Haben wir es dagegen mit einem speziellen Satz X:Prop zu tun, von dem or X (not X)^{15} gezeigt werden kann, so können wir einen geschlossenen Term x:bool angeben und unter Verwendung des Lemmas sumind, welches sich ja ebenso auf or bezieht, beweisen, daß

iff X (isthecase x)

gilt. Der Typ bool reflektiert somit gerade die Unterklasse von Prop, die das Prinzip des tertium non datur erfüllt.

Man kann diese Situation auch auf folgende Weise rekursionstheoretisch deuten: Zu jedem rekursiv aufzählbaren Prädikat P über den natürlichen Zahlen existiert ein geschlossener Term P des Typs nat->Prop^{16}, so daß P ñ bewiesen werden kann, genau dann, wenn P (n) gilt. (ñ bezeichnet hier und im folgenden das zu n gehörige Numeral succ^{n}zero.) Zum Beweis dieser Tatsache verwendet man das Kleene’sche T–Prädikat, das als primitiv rekursive Funktion eine Lego–Darstellung hat.

Da aber jedes durch einen geschlossenen Term des Typs nat->bool repräsentierbare Prädikat entscheidbar ist (aufgrund der starken Normalisierungseigenschaft), kann nicht jedes Prädikat P, welches als Term P des Typs nat->Prop darstellbar ist, auch eine Darstellung als Term des Typs nat->bool haben. Läßt sich allerdings der Satz

{n:nat}or (P n) (not (P n))

beweisen, so ist P entscheidbar, (da sowohl P, als auch P̄ rekursiv aufzählbar sind) und es existiert ein Term p des Typs nat->bool mit

{n:nat}iff (P n) (isthecase (p n))

NB: Dies bedeutet keineswegs, daß jedes entscheidbare Prädikat als geschlossener Term des Typs nat->bool repräsentierbar wäre, da nicht von jedem solchen die Entscheidbarkeit, also der Satz

{n:nat} or (P n) (not (P n))

14Die Bezeichnung ”bycases“ erklärt sich aus der Verwendung dieses Satzes bei Beweisen, wie später noch deutlich wird.

15or ist die in 3.1.1 erwähnte intuitionistische Disjunktion.

16Der Typ nat wird im nächsten Abschnitt noch genau beschrieben

bewiesen werden kann. Gleichwohl ist die Klasse der definierbaren Prädikate sehr groß und schließt alle praktisch vorkommenden Fälle mit ein [Gir71]. Indem wir diese Sichtweise auf beliebige Typen A verallgemeinern, wollen wir ein Prädikat P:A->Prop entscheidbar nennen, wenn

{a:A}or (P a)(not (P a))

gilt. Auch in diesem Fall läßt sich ein geschlossener Term des Typs A->bool finden, der P reflektiert.

3.2.2 Gleichheit

Die Programmiersprache ML stellt zu gewissen vor– und benutzerdefinierten Datentypen eine Gleichheitsfunktion mit Wertebereich bool zur Verfügung, Datentypen, die eine solche Gleichheit gestatten, werden als equality–types bezeichnet [HMT89]. Innerhalb von Signaturen lassen sich solche Typen auch explizit durch

eqtype t

spezifizieren. Erscheint dieses Konstrukt in der Argumentsignatur eines ML– Funktors, so kann in dessen Rumpf die Gleichheitsfunktion verwendet werden. In Lego läßt sich eine entscheidbare Gleichheit mit Hilfe des Prädikates

eqtype[X:Prop][eq:X->X->bool] ==
        {x,y:X}iff (isthecase (eq x y)) (Q x y);

spezifizieren; dadurch wird die logische Gleichwertigkeit von eq und der Leibniz– Gleichheit zum Ausdruck gebracht. Das ML–eqtype Konstrukt wird dann durch den Σ–Typ

<t:Prop><eq:t->t->bool> eqtype t eq

modelliert.

Leider gestatten nun nicht alle induktiven Typen (datatypes) eine entscheidbare Gleichheit, stünde nämlich eine solche für den von Reynolds untersuchten Typ

datatype R = C of (R->bool)->bool

d.i. die T –Algebra zum (covarianten) Signaturfunktor T (X) = (X → bool) → bool zur Verfügung, so wäre das System aufgrund der in [CPM89] beschriebenen Antinomie inkonsistent. Entscheidbare Gleichheiten müssen daher für jeden in Frage kommenden Typ neu (etwa durch Rekursion) definiert werden. Beispiele für solche eqtypes sind etwa bool selber mit

eqbool[b1,b2:bool] == andalso (implies b1 b2)(implies b2 b1)

ebenso aber nat und list; letzterer nur, falls der Typ der Einträge eine entscheidbare Gleichheit hat.

3.2.3 Lemmata

Zum Abschluß dieses Abschnitts sollen noch einige den Typ bool betreffende Lemmata, welche in den Beispielen Verwendung finden, beschrieben werden:

Um Funktionen zu verifizieren, die das if Konstrukt enthalten, ist folgender Spezialfall von boolind nützlich:

[A:Prop][a1,a2:A][b:bool][P:A->Prop]
ifind:

   ((isthecase b)->P a1)->  Falls b die Aussage (P a1) impliziert
   ((isnotthecase b)->P a2)->  und aus b̄ (P a2) folgt.

P (if b a1 a2) == ...;  so soll P für den if–Ausdruck gelten

Und außerdem Sätze iftrue und iffalse, die bei bekanntem Entscheidungsglied den if–Ausdruck zu vereinfachen gestatten:

iftrue:(isthecase b) -> Q a1 (if b a1 a2) == ...
iffalse:(isnotthecase b) -> Q a2 (if b a1 a2) == ...

Für die logischen Konnektive lassen sich die üblichen Gesetze beweisen und außerdem auch die Tatsache, daß isthecase einen Heyting–Algebra–Morphismus zwischen bool und Prop bildet:

orrule[b1,b2:bool]:iff (isthecase (orelse b1 b2))
                       (or (isthecase b1)(isthecase b2) == ...

und analoge Sätze für andalso, implies etc.

Während die eine Richtung des als Kontraposition bezeichneten aussagenlogischen Prinzips

(A → B) ↔ (¬B → ¬A)

auch intuitionistisch für beliebige Sätze gezeigt werden kann:

contrapos1:{A,B|Prop}(A->B)->(not B)->not A == ...

gilt die andere Richtung nur, wenn der eine Implikand entscheidbar ist:

contrapos2:{a|bool}{B|Prop}((isnotthecase a)->not B)->B->isthecase a == ...

Für entscheidbare Gleichheiten lassen sich dieselben Gesetze, die für die Leibniz– Gleichheit gelten, beweisen:

eq refl:{X|Prop}{eq:X->X->bool}{x:X}(eqtype X eq)->
   isthecase (eq x x) == ...;
eq sym:{X|Prop}{eq:X->X->bool}{x,y:X}(eqtype X eq)->
   Q (isthecase (eq x y)) (isthecase (eq y x)) == ...;
eq trans:  ...
eq resp:  ...
...

An dieser Stelle wird deutlich, wie Spezifikationen — in diesem Fall eqtype X eq — Teil einer Prämisse sein können und somit unabhängig von der Implementation (Realisierung) derselben Aussagen gezeigt werden können. Vgl. 2.3.

3.3 Natürliche Zahlen und allgemeine Rekursion

Wie schon beschrieben, lassen sich auch die natürlichen Zahlen als datatype bzw. T –Algebra modellieren. In ML sind die natürlichen Zahlen als Basistyp nicht vorhanden, da — wohl aus historischen Gründen — den ganzen Zahlen (int) der Vorzug gegeben wurde. Möchte man nur programmieren, ist dies auch völlig ausreichend; wegen des Fehlens eines Induktionsprinzips und der primitiven Rekursion sind die ganzen Zahlen für Verifikationszwecke jedoch unbefriedigend. Wir wollen deshalb in den Beispielen den Typ int wann immer möglich durch den Datentyp

datatype nat = zero | succ of nat

ersetzen. Der damit verbundene Geschwindigkeitsverlust (Addition und Multiplikation haben bei nat exponentielle Komplexität!) ist für die Verifikation unerheblich.

In Lego stellen sich die natürlichen Zahlen als

nat == datatype NATSIG, wobei
NATSIG == PLUS ONE ID

dar. Die Konstruktoren Null und Nachfolger ergeben sich zu

zero:nat == phi NATSIG (i1 star)
succ[n:nat]:nat == phi NATSIG (i2 n)

Wie schon für bool können wir auch für nat das Induktionsprinzip aus dem allgemeinen Initialitätsaxiom beweisen:

natind:{P:nat->Prop}(P zero)->
                    ({n:nat}(P n)->P (succ n))->
                    {n:nat}P n == ...

Unter Zuhilfenahme des Konsistenzaxioms yinisnotyang erhalten wir aus der Initialität auch die anderen beiden Peano–Axiome

{n:nat}not Q zero (succ n)
{m,n:nat}(Q (succ n)(succ m)) -> Q m n

Aus dem primitiven Rekursor für beliebige T –Algebren läßt sich ein solcher für nat gewinnen:

natrec[R|Prop][g:R][h:nat->R->R]:nat->R ==
...  primrec NATSIG ...

Ebenso ergeben sich aus der Kommutationsbedingung für den allgemeinen Rekursor die Gesetze für natrec:

glaw:{R|Prop}{g:R}{h:nat->R->R}Q g (natrec g h zero) == ...
hlaw:{R|Prop}{g:R}{h:nat->R->R}
     {n:nat}Q (h n (natrec g h n))(natrec g h (succ n)) == ...

Mit Hilfe der primitiven Rekursion können wir nun Addition, Multiplikation und viele weitere zahlentheoretische Funktionen in Lego modellieren und ihre Gesetze beweisen. Wichtig ist hier, daß der Resultattyp R durchaus auch ein Funktionstyp sein kann, wodurch einerseits — wie im Kapitel über T –Algebren beschrieben — auch Parameter berücksichtigt werden können und andererseits auch solche Funktionen, wie z.B. die Ackermann–Funktion, die durch primitive Rekursion ohne Funktionstypen nicht darstellbar sind, erzeugt werden können [Hue88]. Als Beispiel für eine solche ”higher–order–Rekursion“ sei hier die Darstellung der Ordnungsrelation ≤ auf den natürlichen Zahlen als Funktion vom Typ nat->nat->bool angegeben:

le:nat->nat->bool ==
natrec

([ :nat]true)  0 ≤ n gilt unabh. von n

   ([n:nat][n is le than:nat->bool]  n ≤? sei schon bekannt.

natrec  (n + 1) ≤? durch Rekursion

         false  n + 1 ≰ 0

         [n1:nat][ :bool]n is le than n1

(n + 1) ≤ (n_{1} + 1) ⇔ n ≤ n_{1}

   )];

Wir können nun durch Induktion zeigen, daß die so definierte (entscheidbare) ≤– Relation mit der second–order–Definition von ≤ übereinstimmt:

stable[P:nat->Prop] == {n:nat}(P n)->P(succ n);
LE[m,n:nat] == {P:nat->Prop}(stable P)->(P m)->P n;
Goal {m,n:nat}iff (isthecase (le m n)) (LE m n);
...

In ähnlicher Weise können wir auf nat auch eine Gleichheitsfunktion des Typs nat->nat->bool definieren und so zeigen, daß nat ein eqtype (vgl. 3.2) ist.

3.3.1 Allgemeine Rekursion

Bislang haben wir zur Definition von Funktionen auf Datentypen nur die primitive Rekursion entlang des Termaufbaus verwendet. Viele Algorithmen haben jedoch nicht diese Struktur, sondern verwenden beliebige rekursive Zugriffe auf andere Funktionswerte. Man denke beispielsweise an Algorithmen, wie merge–sort, die auf dem Prinzip des divide and conquer beruhen. Wollen wir auch solche Algorithmen mit Lego verifizieren, so müssen wir überlegen, wie allgemeine Rekursionsschemata in Lego dargestellt werden können. Betrachten wir als Einstieg nachstehende rekursive Definition einer Funktion von N nach N:

f(0) := 1
f(n) := 2 · f(⌊\frac{n}{2}⌋)

Das dieser Funktion zugrundeliegende Rekursionsschema entspricht der folgenden

Definition 3.3.1.1 Ein (einfaches) Rekursionsschema vom Typ A → B ist gegeben durch • eine Abbruchbedingung end:A->bool

• eine Konstante base:B

• eine Funktion reduce:A->A

   • eine Funktion scheme:A->B->B

Eine Lösung eines solchen Rekursionsschemas (falls sie existiert) ist eine Funktion f:A->B, derart, daß

{a:A}Q (f a) (if (end a)
                   base
                   (scheme a (f (reduce a)))
             )

gilt.

Allein schon weil Lego nur totale Funktionen kennt, kann es allerdings keinen geschlossenen Lego–Term geben, der zu jedem solchen Rekursionsschema eine Lösung berechnet. Anders ist die Situation jedoch, wenn ein Beweis dafür bekannt ist, daß ein vorgegebenes allgemeines Rekursionsschema eine eindeutige überall definierte Lösung hat. Ein solcher Beweis kann zum Beispiel aus einem Komplexitätsmaß w:A->nat bestehen, dessen Verschwinden die Abbruchbedingung impliziert und durch die Schrittfunktion reduce echt reduziert wird:

base condition == {a:A}(Q zero (w a))->isthecase (end a)
red condition == {a:A}or (isthecase (end a))
                         (LT (reduce a) a)

(LT soll ”echt kleiner“ bedeuten und kann beispielsweise durch

LT[m,n:nat]==LE (succ m) n

dargestellt werden.

Es gibt nun einen geschlossenen Lego–Term recurse, der aus einem allgemeinen Rekursionsschema und einem Komplexitätsmaß eine Funktion berechnet, von der — unter Zuhilfenahme obiger Prämissen — in Lego selbst gezeigt werden kann, daß sie das Rekursionsschema löst. Wir nehmen dazu das Schema und die Prämissen als Kontext an:

[A,B|Prop][end:A->bool][base:B] [reduce:A->A][w:A->nat]
[scheme:A->B->B] [bc:base condition][rc:red condition]

und definieren eine Hilfsfunktion über primitive Rekursion:

rec up to n ==
natrec
   ([ :A]base)
   ([n:nat][up to n:A->B][a:A]
        if (end a)
              base
              (scheme a (up to n (reduce a))))

Durch Induktion über n läßt sich von dieser Funktion zeigen, daß sie für alle a, deren Komplexität n nicht überschreitet, die Rekursionsgleichungen erfüllt. Mit

recurse[a:A] == rec up to n (w a) a;  Diagonalisierung

Discharge A;  Abstraktion vom Kontext

erhalten wir somit eine Lösung des Rekursionsschemas.

3.3.1.1 Verallgemeinerung auf mehrfache Zugriffe

Bei obigem Rekursionsschema ging jeweils nur ein früherer f–Wert in die Berechnung des neuen ein. Rekursionsschemata wie das der Ackermann–Funktion oder des merge–sort–Verfahrens greifen jedoch auf zwei oder mehrere frühere Funktionswerte zurück. Dieser Tatsache kann man durch folgende Verallgemeinerung Rechnung tragen:

Definition 3.3.1.2 Ein verallgemeinertes Rekursionsschema vom Typ A → B ist gegeben durch

• eine Abbruchbedingung end:A->bool

• eine Konstante base:B

   • eine Funktion scheme:A->(A->B)->B

Eine Lösung eines solchen Rekursionsschemas (falls sie existiert) ist eine Funktion f:A->B, derart, daß

{a:A}Q (f a) (if (end a)
                   base
                   (scheme a f)
             )

(Man beachte, daß das zweite Argument von scheme hier die Funktion f selbst ist.^{17}

Damit ein Rekursionsschema dieser Bauart überhaupt eine effektiv berechenbare Funktion beschreibt, müssen wir sicherstellen, daß die Funktion f innerhalb von scheme nur an endlich vielen Stellen ausgewertet wird. Diese Forderung ist für eine in Lego oder ML definierbare Funktion scheme automatisch erfüllt.

Wollen wir wiederum eine Lösung eines solchen Schemas durch einen geschlossenen Lego–Term berechnen, so müssen wir wie im oben betrachteten Spezialfall beweisen, daß die Folge der rekursiven Rückgriffe für jedes a nach endlich vielen Schritten terminiert. Auch hier kann solch ein Beweis durch die Angabe eines Komplexitätsmaßes w:A->nat geliefert werden derart, daß die Bedingungen

17Eine noch weitergehende Verallgemeinerung wäre es, den Anfangswert noch in a zu parametrisieren; man hätte dann base:A->B mit entsprechenden Rekursionsgleichungen.

base condition == {a:A}(Q (w a) zero)->(isthecase (end a))  und

cont condition ==
  {a:A}or (isthecase (end a))

({f1,f2:A->B}  Auf zwei Funktionen ...

               ({a':A}(LT (w a') (w a))->

Q (f1 a') (f2 a')) ->... die unterhalb von a übereinstimmen ...

               Q (scheme a f1)(scheme a f2)  reagiert scheme a gleich.

erfüllt sind.^{18} Ganz analog zum vorherigen Spezialfall läßt sich dann auch hier eine Hilfsfunktion durch primitive Rekursion definieren, aus der man wiederum durch Instantiierung mit (w a) eine Funktion erhält, die nachweisbar den Rekursionsgleichungen genügt.

Beispiel 3.3.1.3 Für die Implementierung der eingangs als Motivation genannten merge–sort–Funktion setzen wir:

merge-sort-end[l:list] == null l;
merge-sort-base == nil;
merge-sort-scheme[l:list][ms:list->list] ==
    put together (ms (fst half l)) (ms (snd half l));

Als Komplexitätsmaß wählen wir die Länge, oder auch den aufgerundeten Zweierlogarithmus der Länge. Die Funktionen null, nil, put together, fst half, snd half seien mit der durch die Bezeichnung suggerierten Bedeutung vorhanden. Wir haben nun die entsprechende Anfangs– und Stetigkeitsbedingung zu zeigen, also, daß verschwindende Länge das Zutreffen von null impliziert und daß (merge-sort-scheme l) auf Funktionen, die sich auf kürzeren Listen als l identisch verhalten, gleich reagiert. Dazu ist nachzuweisen, daß fst half und snd half verkürzen. Mit

merge-sort == recurse merge-sort-end merge-sort-base merge-sort-scheme length

erhalten wir die gewünschte Funktion.

3.3.1.2 Induktionsprinzipien

Für die Verifikation durch Rekursion gegebener Funktionen verwendet man üblicherweise Induktion über das Komplexitätsmaß. Da dieses Maß bereits Teil einer jeden in Lego dargestellten rekursiven Funktion ist, läßt sich dieser Induktionsbeweis auch unabhängig von der zu beweisenden Eigenschaft führen:

rec ind1: {P:B->Prop}(P base) ->
            ({f:A->B}({a:A}P (f a))->{a:A}P(scheme a f)) ->
                   {a:A}P (recurse a) == ...

18Man könnte sich fragen, warum man hier überhaupt noch die Abbruchbedingung explizit fordert, wo doch aus dem nichttrivialen Fall der zweiten Bedingung hervorgeht, daß scheme a f für wa = 0 von f unabhängig ist. Man müßte dann aber zusätzlich fordern, daß B nicht leer ist.

Dieses Lemma sagt aus, daß eine sog. Sicherheitseigenschaft, die im Basisfall gilt und durch das Schema nicht verändert wird, für die Resultate der durch Rekursion definierten Funktion gilt. Ein Beispiel wäre etwa die Eigenschaft einer Liste, sortiert zu sein. Nicht formulieren lassen sich in diesem Schema allerdings Eigenschaften, die auch von der Eingabe abhängen, wie etwa die Eigenschaft einer Sortierfunktion, eine Permutation der Eingabeliste durchzuführen. Dies liegt einfach daran, daß P nur über die Resultate spricht. Abhilfe schafft daher folgendes der Scott–Induktion [Cou90a] vergleichbare Prinzip:

recind:{P:A->(A->B)->Prop}  Eine Eigenschaft

{maxeval:A->nat}  und eine Auswertungsschranke

({a1,a2:A}(LT (w a1) (w a2))->

     LT (maxeval a1) (maxeval a2))                              maxeval ist monoton

->({a:A}{f1,f2:A->B}

     ({a':A}(LE (w a')(maxeval a))                               P a berücksichtigt f
         ->Q (f1 a')(f2 a'))  nur unterhalb
          ->(P a f1)->P a f2)  von (maxeval a)
->({a:A}(Q (maxeval a)zero)->P a ([ :A]base))  Induktionsanfang

->({f:A->B}{a:A}({a':A}(LT (w a')(w a))->P a' f)

     -> P a ([a:A]if (end a) base (scheme a f)))  Induktionsschritt

->{a:A}P a recurse == ...;Unter vorstehenden Bedingungen hat recurse die Eigenschaft P a

Hier wird zum Ausdruck gebracht, daß recurse seiner Spezifikation genügt, wenn ihr die Konstante base für solche Eingaben, die die Abbruchbedingung erfüllen, genügt, und wenn scheme angewandt auf Funktionen, die die Spezifikation partiell (bis zu einer bestimmten Komplexität) befriedigen, die Spezifikation erfüllt.

Beispiel 3.3.1.4 Im Verlauf der Verifikation der oben beschriebenen merge--sort– Funktion könnte etwa

Goal {l:list} P l merge-sort;  wobei

P[l:list][f:list->list] ==
    {e:entry}iff (member^{20}e l) (member e (f l))

zu zeigen sein. Durch Refine P reduziert sich diese Aufgabe auf folgende Unterziele: Zunächst ist zu zeigen, daß P stetig ist, es also eine — von l abhängige — obere Schranke gibt, bis zu der P den Werteverlauf von f berücksichtigt. Hier wertet P die Funktion nur an der Stelle l selbst aus; wir wählen also maxeval == length und erhalten durch elementare Schritte die Monotonie und die Stetigkeit. Als nächstes haben wir den Induktionsanfang, also

{l:list}(Q (length l) zero) -> P l nil

19Diese Terme beziehen sich auf einen Kontext, in dem ein Rekursionsschema vorgegeben ist.

Durch Discharge wird dann die Parametrisierung hergestellt.

20Der Typ entry und die Funktion member seien geeignet definiert.

zu zeigen. Es bleibt der Induktionsschritt; hier läuft dieser darauf hinaus, zu beweisen, daß put together, fst half und snd half weder Elemente hinzufügen, noch löschen.

3.3.1.3 Wertung

Durch dieses Rekursionsschema wird die Klasse der darstellbaren Funktionen zwar nicht vergrößert, aber das Schema erlaubt es, bei der Lego–Verifikation gegebener Programme näher am Programmtext zu bleiben, als das ohnedies der Fall wäre. Außerdem ermöglicht dieses Schema die Lego–Darstellung (ohne sinnentstellende Simulation) des euklidischen Algorithmus, von merge–sort und anderen Algorithmen, bei denen die Problemgröße in jedem Schritt nicht nur um eins (wie bei der primitiven Rekursion) reduziert wird. Da die Anwendung dieses allgemeinen Rekursors in Lego schon durch die Typisierung nur in den Fällen zulässig ist, in denen das Schema eine eindeutige, totale Lösung hat, treten hier die üblichen Probleme der allgemeinen Rekursion mit der Auswertereihenfolge [BTM90] u.ä. nicht auf. Nachdem andererseits ein Terminationsbeweis Teil jeder Verifikation ist, stellt dies — zumindest für Verifikationszwecke — keine Einschränkung dar.

3.3.1.4 Verallgemeinerung auf Ordinale

Nun ist es leider nicht so, daß sich die Termination jedes Rekursionsschemas durch Induktion über nat beweisen ließe. Das Ackermann–Schema beispielsweise erfordert nachweislich Induktion entlang ω^{2}. Dies legt die Verallgemeinerung der oben beschriebenen Vorgehensweise auf größere Ordinale als ω nahe. Voraussetzung dafür ist, daß das in Frage kommende Ordinal einerseits in Lego darstellbar ist und andererseits einen in Lego definierbaren Rekursor besitzt (Dem Operator natrec für nat vergleichbar.). Für die Ordinale ω^{2} (Paare von natürlichen Zahlen) und ω^{ω} (Listen von solchen) ist das beispielsweise der Fall; ob die abzählbaren Ordinale nach Coquand [Coq85b] einen darstellbaren Rekursor besitzen, bleibt noch zu untersuchen. Es ist bekannt [Ros84, Tai61], daß sich die Termination jedes (überhaupt terminierenden) Rekursionsschemas durch Induktion entlang einem genügend langen Ordinal zeigen läßt; die Frage der Lego–Darstellbarkeit rekursiver Funktionen reduziert sich somit auf die Frage der Darstellbarkeit von Ordinalzahlen.

3.3.1.5 Lego und Partialität

In [Str89] wird darauf aufmerksam gemacht, daß in gewissen Fällen auch partielle, nicht total erweiterbare Funktionen sinnvoll sein können. Als Beispiel wären hier Interpreter und andere Simulationsprogramme zu nennen, die das gesamte mögliche Verhalten einer universellen Maschine beinhalten^{21}. Solche Funktionen lassen sich mit dem beschriebenen Verfahren nicht vollständig verifizieren. Man wird daher die einzelnen Komponenten separat bearbeiten und die endgültige (evtl. nichtterminierende) Rekursion nur informell verifizieren. Dies ist zweifellos unschön und läuft der Idee von durchgehender formaler maschinenunterstützter Verifikation zuwider. Der Autor meint allerdings, daß diese Fälle so punktuell auftreten, daß eine Anreicherung von Lego um Scott–Domains und Partialität — mit allen daraus sich ergebenden Problemen — nicht gerechtfertigt erscheint.

21Das Problem liegt hier darin, daß diese Funktionen auf die Eingabe eines (codierten) Programms hin mit dem durch letzteres beschriebenen (evtl. fehlerhaften) Verhalten reagieren und nicht, wie ein Compiler, nur ein übersetztes Programm erzeugen.

Ein anderes Argument gegen die Beschränkung auf totale Funktionen ist der Wunsch, auch potentiell unendliches Verhalten, wie das von Prozessen oder lazy streams modellieren zu können. Dazu ist zu sagen, daß sich solche Strukturen in Lego unter Beibehaltung der starken Normalisierung als sogenannte codatatypes (vgl. Bemerkung 2.2.1.5) darstellen lassen [Hag87, Wra89, Alt90]. Dieser Ansatz erscheint sehr vielversprechend; inwieweit er den Anforderungen gerecht wird, bleibt freilich noch zu untersuchen.

3.4 Zusammenfassung

Wir haben jetzt die wichtigsten Konstrukte der Programmiersprache ML in Lego interpretiert und Beweisprinzipien bereitgestellt. Datentypen haben wir als initiale T –Algebren dargestellt und die beiden Beweisprinzipien Konsistenz (yinisnotyang) und Initialität formuliert. Aus diesen haben wir Induktionsprinzipien abgeleitet, die im Falle der booleans und der natürlichen Zahlen die bekannten Induktionsaxiome liefern. Zur Definition von Funktionen haben wir einen primitiven Rekursor bereitgestellt, der die Darstellung von in ML durch pattern-matching gegebenen Funktionen erlaubt.

Bei der Gleichheit haben wir zwischen entscheidbarer und unentscheidbarer unterschieden; die eine läßt sich in if–Konstrukten verwenden, die andere nur zur Spezifikation. Wir haben gesehen, daß Fallunterscheidung als Beweisprinzip nur für entscheidbare Prädikate möglich ist und haben für diese ein entsprechendes Prinzip (bycases) gezeigt.

Als weitere Möglichkeit zur Definition von Funktionen wurde ein allgemeines Rekursionsprinzip definiert, welches Fixpunkte stetiger Funktionale zu berechnen gestattet, falls ein geeigneter Totalitätsbeweis vorliegt. Als zugehöriges Beweisprinzip wurde eine totale Version der Scott-Induktion [Cou90a] formuliert und bewiesen.

Die Modulkonstrukte von ML haben wir wie in [MH88] durch Σ–Typen modelliert und dabei den Signaturbegriff von ML in einer Extended–ML vergleichbaren Weise durch die Hinzufügung von Axiomen erweitert. Dadurch werden die Vorteile des ML–Modulsystems (Kompositionalität, (relative) Unabhängigkeit der verschiedenen Moduln) auch für die Verifikation nutzbar. Dem sharing–Problem sind wir wir durch explizite Parametrisierung der Signaturen begegnet.

Wir haben deutlich gemacht, daß unser Ansatz nicht die volle Turing–Mächtigkeit beinhaltet und versucht, diese Einschränkung zu begründen. Außerdem haben wir auf die Modellierung imperativer Strukturen und abstrakter Datentypen verzichtet. In der Schlußbetrachtung (Kapitel 5.3) werden allerdings mögliche Abhilfen diskutiert.

56 KAPITEL 3. LEGO–INTERPRETATIONEN

Im folgenden Kapitel wollen wir nun anhand eines größeren Beispiels die gebotenen Konstruktionen praktisch einsetzen und verdeutlichen.

Ein größeres Beispiel

In diesem Kapitel soll anhand eines größeren Beispiels die praktische Durchführung der Verifikation eines modularen ML-Programms mit Hilfe von Lego verdeutlicht und gezeigt werden, daß eine solche nicht nur theoretisch, sondern auch effektiv möglich ist. Gewählt wurde die aus der Literatur bekannte [Har86] und von Sannella und Tarlecki zur Demonstration ihres Extended–ML–Ansatzes verwendete modulare Implementation einer Symboltabelle [San89]. Die folgende Lego–Verifikation orientiert sich sehr genau an der Implementation von Sannella und Tarlecki; dadurch soll einerseits deutlich werden, daß nicht nur spezielle, eigens zu diesem Zweck konstruierte Programme mit Lego verifiziert werden können und andererseits eine Vergleichbarkeit mit anderen Verifikationsansätzen ermöglicht werden. Nur an den Stellen, wo dies unumgänglich erschien, wurden behutsam einige Änderungen vorgenommen. Die originalen Extended–ML–Signaturen wurden der leichteren Lesbarkeit halber in den Text mit aufgenommen.

4.1 Ausgangsspezifikation

Eine Symboltabelle ist Teil eines jeden Compilers; sie dient dazu, während der syntaktischen Analyse gewonnene Informationen (sog. Attribute) über Bezeichner (Symbole) aufzunehmen und später bereitzustellen. Dazu sollten zumindest Funktionen für den Test auf Präsenz eines Bezeichners in der Symboltabelle, zum Ermitteln des Attributes eines vorhandenen Bezeichners und zum Hinzufügen neuer Bezeichner samt ihren Attributen vorhanden sein; sinnvoll ist auch die Möglichkeit, Attribute vorhandener Bezeichner zu ändern, schließlich brauchen wir eine nullstellige Funktion (Konstante) zur Erzeugung einer neuen (leeren) Symboltabelle. Die Extended–ML–Signatur einer solchen Tabelle stellt sich somit folgendermaßen dar:

signature SYMTAB =
     sig
         structure Ident :  IDENT
         structure Attrib :  ATTRIB
         type symtab
         val empty :  symtab
         val add :  Ident.ident -> Attrib.attrib -> symtab -> symtab
         val change attrib :  Ident.ident -> Attrib.attrib -> symtab -> symtab

         val present :  Ident.ident -> symtab -> bool
         axiom present i empty = false
         axiom present i (add i' a' s) = (i=i') orelse (present i s)
         axiom present i (change attrib i' a' s) = (present i s)
         val lookup :  Ident.ident -> symtab -> Attrib.attrib
         axiom lookup i empty = Attrib.null attrib
         axiom lookup i (add i a s) = a
         axiom i<>i' => (lookup i (change attrib i a s)) = a
         axiom (present i s) => (lookup i (change attrib i a s)) = a
         axiom i<>i => (lokp i (change attrib i' a' s)) = (lookup i s)
     end

Die Strukturen IDENT und ATTRIB sind dabei durch

signature IDENT =
     sig
         eqtype ident
     end
signature ATTRIB =
     sig
         eqtype attrib
         val null attrib:attrib
     end

gegeben.

Im Gegensatz zum ursprünglichen Sannella-Beispiel haben wir hier alle Funktionen in ihrer ”curryfizierten“ Form geschrieben, dies erhöht die Lesbarkeit der entsprechenden Lego-Darstellungen. Außerdem wurde nicht nur ident, sondern auch attrib als eqtype spezifiziert; auf diese Änderung wird in Abschnitt 4.4.3.4 näher eingegangen. Schließlich ist zu sagen, daß die freien Variablen in den Axiomen stets als universell über die ganze Formel quantifiziert zu verstehen sind.

Strukturen der Signatur SYMTAB erhalten wir durch einen (hypothetischen) Funktor, der in Ident und Attrib parametrisiert ist:

functor Symtab
    (structure X : IDENT,
     structure Y : ATTRIB)
         :  sig include SYMTAB
                sharing Ident = X and Attrib = Y
         end
    = ?

Lego-Darstellung von IDENT und ATTRIB: In Lego stellen sich nun die Signaturen IDENT und ATTRIB folgendermaßen dar:

IDENT == <ident:Prop>
         <eqid:ident->ident->bool>
         (eqtype ident eqid);

ATTRIB == <attrib :  Prop>
          <eqattr :  attrib->attrib->bool>
          <null attrib :  attrib #
          (eqtype attrib eqattr);

Eine Struktur der Signatur IDENT besteht danach aus einem (kleinen) Typ ident:Prop, einer Gleichheitsfunktion auf diesem und einem Beweis, daß diese tatsächlich eine solche ist (vgl. 3.2). Bei ATTRIB verhält es sich analog, nur daß noch eine Konstante null attrib:attrib hinzutritt, die keiner weiteren Spezifikation zu genügen hat. Zu beachten ist, daß man auf diese Komponenten nicht über ihre Namen, sondern ausschließlich über die Projektionsfunktionen ?.1 und ?.2 zugreifen kann. Ist also etwa Attrib:ATTRIB, so erhält man den zugehörigen Grundtyp durch Attrib.1, die Gleichheit durch Attrib.2.1, die Konstante durch Attrib.2.2.1 und den Beweis für die Gleichheitseigenschaft über Attrib.2.2.2. Im Rahmen einer Beweissitzung führt man natürlich geeignete Abkürzungen für diese Ausdrücke ein, die dann allerdings, wie alle Abkürzungen in Lego, global sind. Dies ist zweifelsohne ein Nachteil von Lego; falls die Programmverifikation mit Lego Verbreitung findet, wird man darüber nachdenken müssen, wie hier Abhilfe geschaffen werden kann.

Lego-Darstellung der Signatur SYMTAB: Da auf die Komponenten Ident und Attrib der Signatur SYMTAB durch sharing zugegriffen wird, werden wir wie in Abschnitt 2.3 beschrieben diese explizit als Parameter vorgeben:

SYMTAB[Ident:IDENT][Attrib:ATTRIB] ==

Abkürzungen

    [ident=Ident.1][eqid:ident->ident->bool=Ident.2.1]
    [EQID:eqtype ident eqid=Ident.2.2]
    [attrib=Attrib.1][null attrib:attrib=Attrib.2.2.1]

Komponenten

    <symtab:Prop>
    <empty:symtab>
    <add:ident->attrib->symtab->symtab>
    <change attrib:ident->attrib->symtab->symtab>
    <present:ident->symtab->bool>
      ({i:ident}isnotthecase (present i empty)) #
      ({a':attrib}{s:symtab}{i,i':ident}
                Q (present i (add i' a' s))
                   (orelse (eqid i i')(present i s))) #
      ({i,i':ident}{a':attrib}{s:symtab}
                Q (present i (change attrib i' a' s))
                   (present i s)) #
    <lookup:ident->symtab->attrib>
      ({i:ident}Q (lookup i empty) null attrib) #
      ({i:ident}{a:attrib}{s:symtab}
                Q (lookup i (add i a s)) a) #
      ({i,i':ident}{a':attrib}{s:symtab}

                (isnotthecase (eqid i i')) ->
                   (Q (lookup i (add i' a' s)) (lookup i s))) #
      ({i:ident}{a:attrib}{s:symtab}
                (isthecase (present i s))->
                   (Q (lookup i (change attrib i a s)) a)) #
      ({i,i':ident}{a':attrib}{s:symtab}
                (isnotthecase (eqid i i')) ->
                   (Q (lookup i (change attrib i' a' s)) (lookup i s)))

Hier ist zu beachten, daß nur in den Fällen, in denen die Gleichheit wirklich als Funktion mit Wertebereich bool verwendet wird, die entscheidbare Gleichheit eingesetzt wurde, während in den Fällen, in denen die Gleichheit eher der Spezifikation einer bestimmten Funktion dient, die (leichter handhabbare) Leibniz–Gleichheit Verwendung fand. Extended–ML selbst macht ja keinen Unterschied zwischen diesen Gleichheitsbegriffen. In einigen Fällen wurde außerdem das etwas unschöne … = true und … = false durch das suggestivere isthecase bzw. isnotthecase ersetzt. Weiterhin ist zu beachten, daß die in Extended-ML implizit vorhandenen Quantifizierungen in Lego explizit anzugeben sind.

4.2 Implementierung von change attrib durch add:

Die Funktion change attrib stellt in gewisser Weise zusätzlichen Luxus dar; sie kann jederzeit durch einen entsprechenden Aufruf von add ersetzt werden. Genau dies soll im folgenden Zerlegungsschritt geschehen: Wir gehen davon aus, daß der Funktor Symtab bis auf die Funktion change attrib bereits vorliegt und fügen letztere unter Verwendung von add hinzu. Dabei ist natürlich zu zeigen, daß die entsprechenden Axiome erfüllt sind: Wir geben uns dazu zwei (hypothetische) Funktoren vor:

[Symtab':{Ident:IDENT}{Attrib:ATTRIB}SYMTAB' Ident Attrib];
[Change Attrib:{Ident:IDENT}{Attrib:ATTRIB}
      (SYMTAB' Ident Attrib) -> SYMTAB Ident Attrib];

Die Signatur SYMTAB' hat dabei dieselbe Gestalt, wie SYMTAB, nur die Funktion change attrib und die sie betreffenden Axiome fehlen. Der universelle Typ {Ident:IDENT}{Attrib:ATTRIB} ... der beiden Funktoren bringt zum Ausdruck, daß nicht nur deren Resultat (wie das bei einem Funktionstyp der Fall wäre), sondern auch dessen Typ von der Eingabestruktur abhängen.

Unter der Annahme dieser beiden Funktoren läßt sich dann der gesuchte Funktor Symtab durch Komposition realisieren:

Symtab:{Ident:IDENT}{Attrib:ATTRIB}SYMTAB Ident Attrib
==
[Ident:IDENT][Attrib:ATTRIB]
Change Attrib Ident Attrib (Symtab' Ident Attrib)

Die durch Lego automatisch vorgenommene Typprüfung stellt sicher, daß dieser zusammengesetzte Ausdruck den angegebenen Typ hat, d.h. daß die Zerlegung korrekt ist. Auch hier wird die durch das sharing gegebene implizite Abhängigkeit des Resultattyps von der Eingabe durch den universellen Typ von Symtab deutlich gemacht.

4.2.1 Implementierung des Funktors ChangeAttrib

Es geht nun darum, die eben hypothetisch angenommenen Funktoren (evtl. durch weitere Verfeinerung und Zerlegung) zu implementieren. Der Funktor ChangeAttrib soll dabei in der oben angedeuteten Weise realisiert werden. In Extended-ML stellt sich dies folgendermaßen dar:

functor ChangeAttrib
    (X : SYMTAB') :
        sig include SYMTAB
            sharing Ident = X.Ident and Attrib = X.Attrib
        end
    =   struct
            open X
            fun change attrib i a s = if (present i s) then (add i a s) else s
        end

Der im Artikel von Sannella vorhandene Zwischenschritt, in dem der Rumpf von ChangeAttrib noch Axiome enthält, wurde übersprungen, da die dort vorhandenen Axiome wörtlich die Implementierung beschreiben. Wollten wir diesen Schritt dennoch in Lego behandeln, so müßten wir den Funktor gemäß dem in Abschnitt 2.3 Gesagten weiter verfeinern.

4.2.1.1 Lego-Darstellung von ChangeAttrib:

Für die Lego-Darstellung obigen implementierten Funktors geben wir uns zunächst dessen Argumente als Kontext vor:

[Ident:IDENT][Attrib:ATTRIB][St':SYMTAB' Ident Attrib]

Den im ML-Original vorhandenen open-Ausdruck können wir als Bündel lokaler Konstantendefinitionen deuten; in gewisser Weise wird dies durch folgende, allerdings globale Abkürzungsdefinitionen in Lego modelliert:

ident == Ident.1
eqid:ident->ident->bool == Ident.2.1
EQID:eqtype ident eqid == Ident.2.2
attrib == Attrib.1
null attrib:attrib == Attrib.2.2.1
symtab == St'.1
empty:symtab == St'.2.1
add:ident->attrib->symtab->symtab == St'.2.2.1
present:ident->symtab->bool == St'.2.2.2.1

presempty:{i:ident}isnotthecase (present i empty) == St'.2.2.2.2.1
presadd:{a':attrib}{s:symtab}{i,i':ident}
    Q  (present i (add i' a' s))
       (orelse (eqid i i')(present i s)) == St'.2.2.2.2.2.1
lookup:ident->symtab->attrib == St'.2.2.2.2.2.2.1
lkupempty:{i:ident}Q (lookup i empty) null attrib == St'.2.2.2.2.2.2.2.1
lkupadd1:{i:ident}{a:attrib}{s:symtab}
    Q (lookup i (add i a s)) a == St'.2.2.2.2.2.2.2.2.1
lkupadd2:{i,i':ident}{a':attrib}{s:symtab}
    (isnotthecase (eqid i i')) ->
       (Q (lookup i (add i' a' s)) (lookup i s)) == St'.2.2.2.2.2.2.2.2.2

Da wir bei der Verifikation diese verwenden, geben wir auch den Beweisen der Axiome der Argumentstruktur eigene Namen. Die explizite Typisierung der Beweise und Funktionen ist nicht zwingend, erleichtert jedoch die Lesbarkeit, da nur so die vorher definierten Abkürzungen verwendet werden (lookup hätte sonst den

Typ Ident.1 -> Attrib.1 -> St'.1).

Nun können wir die Implementation von change attrib in Lego vornehmen:

change attrib[i:ident][a:attrib][s:symtab] ==
    if (present i s) (add i a s) s

Bei dieser Darstellung wurde die in Kap. 3.2 beschriebene if-Funktion verwendet. Dies ist nur möglich, weil present eine entscheidbares Prädikat (mit Wertebereich bool) ist. Bei der Verifikation werden wir natürlich die über if bereits gezeigten Sätze verwenden. Versuchen wir also, die change attrib betreffenden Axiome zu beweisen:

4.2.1.2 Verifikation von ChangeAttrib

Goal {i:ident}{a:attrib}{s:symtab}
            (isthecase (present i s))->
              Q (lookup i (change attrib i a s)) a;
...
Save chlkup1;^{1}

In diesem Beweis, der auch in Lego sozusagen straightforward ist, wird zunächst isthecase (present i s) als Hypothese eingeführt und dann mit Hilfe des Lemmas iftrue, welches zum Ausdruck bringt, daß ein if-Ausdruck bei wahrem Entscheidungsglied gleich seinem then-Teil ist, die Behauptung unter Verwendung von lkupadd1 gezeigt. Als nächstes haben wir zu zeigen, daß die Präsenz eines Bezeichners in der Tabelle durch Änderungen an seinen Attributen nicht verändert wird:

Goal {i,i':ident}{a':attrib}{s:symtab}
                 Q  (present i (change attrib i' a' s))
                    (present i s);
...
Save chpres;

1Die Lego-Beweise finden sich im separat erscheinenden Anhang

In diesem schon etwas komplizierteren Beweis verwenden wir das in Abschnitt 3.2 beschriebene Lemma ifind, welches auch in den Fällen, in denen der Wahrheitswert des Entscheidungsgliedes eines if-Ausdrucks a priori unbekannt ist, über letzteren eine Aussage zu machen gestattet. Des weiteren macht der Beweis in der Weise von der Entscheidbarkeit der Gleichheit auf ident Gebrauch, daß nach dem Wahrheitsgehalt von (eqid i i') zwei Fälle unterschieden werden. Ein solches — in der klassischen Logik stets mögliches — Vorgehen setzt in Lego gerade die Entscheidbarkeit der Aussage, nach der unterschieden wird, voraus.

Schließlich ist zu zeigen, daß change attrib die Attribute anderer als des angegebenen Bezeichners unverändert läßt:

Goal {i,i':ident}{a':attrib}{s:symtab}
            (isnotthecase (eqid i i'))->
              Q (lookup i (change attrib i' a' s)) (lookup i s);
...
Save chlkup2;

Dieser ebenfalls über ifind geführte Beweis unterscheidet nach der Präsenz von i' in s zwei Fälle; aufgrund der Entscheidbarkeit von present ist auch dies möglich.

Es sind nun alle erforderlichen Axiome gezeigt; die Beweise, die Funktion change attrib und die aus dem Argument übernommenen Funktionen und Typen können zum Funktor ChangeAttrib gepackt werden:

ChangeAttrib == (
symtab,
empty,add,change attrib,present,
presempty,presadd,chpres,
lookup,
lkupempty,lkupadd1,lkupadd2,chlkup1,chlkup2):SYMTAB Ident Attrib

Der Lego-typechecker überprüft hier wiederum die Typen der Funktionen und auch die Korrektheit der Beweise. Durch

Discharge Ident;

schließlich abstrahieren wir vom geschaffenen Kontext; ChangeAttrib ist jetzt in Ident, Attrib und St' parametrisiert.

4.3 Implementierung von Symtab' als Termalgebra

In den nun folgenden Schritten braucht die Funktion change attrib nicht mehr berücksichtigt zu werden; gelingt es, den Funktor Symtab', der diese nicht enthält, zu implementieren, so liefert dies durch Zusammensetzen mit dem eben implementierten und verifizierten Funktor Change Attrib eine Lösung der ursprünglich gestellten Aufgabe.

64 KAPITEL 4. EIN BEISPIEL

Für die Realisierung der verbliebenen, vereinfachten Symboltabelle werden im Papier von Sannella und Tarlecki zwei Möglichkeiten näher untersucht; deren eine basiert auf der unmittelbaren Darstellung der Symboltabelle als datatype mit den Konstruktoren empty und add; die weiteren Funktionen ergeben sich dann durch primitive Rekursion; also durch pattern matching:

functor Symtab'
    (structure X : IDENT
    structure Y : ATTRIB) :
         sig    include SYMTAB'
                sharing Ident = X and Attrib = Y
         end
    = struct
         structure Ident :  IDENT = X
         structure Attrib :  ATTRIB = Y
         datatype symtab =
                empty
                | addc of Ident.ident * Attrib.attrib * symtab
         val add = curry (curry addc)
         fun present i empty = false
                | present i (add i', a', s)) = (i=i') orelse (present i s)
         fun lookup i empty = Attrib.null attrib
                | lookup i (add i' a' s)) = if i=i' then a else (lookup i s)
    end

4.3.1 Lego-Darstellung von Symtab'

Für die Lego-Darstellung ist es (aus Effizienzgründen)^{2} günstiger, die datatype-Deklaration aus dem Funktor herauszulösen und sie – in eine entsprechende Struktur gepackt – als zusätzliches Argument zu übergeben:

DATSYM[Ident:IDENT][Attrib:ATTRIB] ==
[ident=Ident.1][attrib=Attrib.1]
<symtab:Prop>
<empty:symtab>
<add:ident->attrib->symtab->symtab>
({P:symtab->Prop}
    (P empty)->
    ({i:ident}{a:attrib}{s:symtab}
      (P s)->P (add i a s))->

    {s:symtab}P s) #  symind
<symrec:{R|Prop}R->(ident->attrib->symtab->R->R)->symtab->R>  symrec
({R|Prop}{g:R}{h:ident->attrib->symtab->R->R}  emptyrec

    Q g (symrec g h empty)) #

({R|Prop}{g:R}{h:ident->attrib->symtab->R->R}  addrec

    {i:ident}{a:attrib}{s:symtab}
      Q (h i a s (symrec g h s)) (symrec g h (add i a s)));

2Die aktuelle Lego-Version scheint alle Definitionen — also auch das komplizierte datatype-Konstrukt — intern bis zur Normalform zu expandieren. Daher ist dessen unmittelbare Verwendung – zumindest zum jetzigen Zeitpunkt – kaum möglich. Selbstverständlich kann jedoch — was auch geschieht — nachträglich die Struktur DATSYM durch einen datatype implementiert werden.

Diese (parametrisierte Struktur) enthält mit struktureller Induktion und primitiver Rekursion eine axiomatische Beschreibung des gewünschten Datentyps, die bis auf Isomorphie nur eine Implementierung zuläßt. Diese wollen wir jedoch noch etwas aufschieben, und uns zunächst der Realisierung von Symtab' zuwenden. Wir geben uns dazu wiederum die Argumente (den Datentyp eingeschlossen) als Kontext vor und ”öffnen“ die entsprechenden Strukturen:

[Ident:IDENT][Attrib:ATTRIB]
[ident=Ident.1][eqid:ident->ident->bool=Ident.2.1]
[attrib=Attrib.1][null attrib:attrib=Attrib.2.2.1]
[DatSym:DATSYM Ident Attrib]
[DatSym:DATSYM Ident Attrib]
[symtab=DatSym.1]
...

Die Funktionen present und lookup können wir nun durch primitive Rekursion, die ja das pattern-matching widerspiegelt, implementieren:

present:ident->symtab->bool == permute
  (symrec
     ([ :ident]false) (**case empty ***)
     ([i':ident][ :attrib][ :symtab][present in s:ident->bool][i:ident]
         orelse (eqid i i') (present in s i));

Die Anwendung von permute ist hier erforderlich, da die Variable, nach der rekurriert wird, grundsätzlich die erste ist. Der Vorteil dieser Vorgehensweise ist es, daß symrec ohne gebundene Variablen auskommt. Die Funktion lookup erhalten wir analog:

lookup:ident->symtab->attrib ==
permute
  (symrec
     ([ :ident]null attrib)
     ([i':ident][a:attrib][ :symtab][lookup in s:ident->attrib][i:ident]
         if (eqid i i') a (lookup in s i));

4.3.2 Verifikation von Symtab'

Die Beweise für die Axiome ergeben sich fast unmittelbar aus den Gesetzen emptyrec und addrec, die die primitive Rekursion beschreiben. Zu bemerken ist nur, daß diese Gesetze, die ja die Gleichheit gewisser Funktionen beschreiben (Wertebereiche von lookup etc. sind Exponentenobjekte), jeweils mit bestimmten Werten zu instantiieren sind. Dazu ist das ”Makro“ unext – ein geschlossener Lego-Term des Typs

{A,B|Prop}{f,g:A->B}(Q f g)->{a:A}Q (f a) (g a)

nützlich. Mit seiner Hilfe läßt sich das (im Beweis von presempty auftretende) Unterziel

?1 :  isnotthecase (present i empty)

durch

Refine unext ??  (emptyrec ??);

lösen. Die durch das Fragezeichen markierten Metavariablen werden dabei durch Unifikation automatisch so besetzt, daß sich das Unterziel als Spezialfall von emptyrec, einer Komponente der Struktur DATSYM, welche den Rekursionsanfang einer primitiven Rekursion über dem Datentyp symtab beschreibt, ergibt. Freilich kann der Unifizierungsalgorithmus von Lego nicht alle auftretenden Fälle bearbeiten. Hier muß man von Fall zu Fall probieren und evtl. einige Parameter von Hand instantiieren.

Die Implementationen samt den Beweisen der zugehörigen Axiome lassen sich nun, wie schon bei ChangeAttrib, zu einer Struktur der Signatur SYMTAB' packen

Symtab' pre ==
(symtab,empty,add,present,
presempty,presadd,
lookup,lkupempty,lkupadd1,lkupadd2):SYMTAB' Ident Attrib

Durch Abstraktion (Discharge Ident) erhalten wir daraus einen Funktor des Typs

Symtab' pre:{Ident:IDENT}{Attrib:ATTRIB}{DatSym:DATSYM Ident Attrib}
  SYMTAB' Ident Attrib

Es bleibt die Implementierung der Struktur DATSYM durch ein datatype-Konstrukt:

4.3.2.1 Implementierung des datatypes

Wir geben uns erneut die Argumente vor

[Ident:IDENT][Attrib:ATTRIB];

und führen die Abkürzungen ein. Der Signaturfunktor des Datentypes ist

SYSIG == PLUS ONE (TIMES (KP (PROD id at)) ID)

Wir setzen also

symtab == datatype SYSIG;
empty:symtab == phi SYSIG (i1 star);
add[i:id][a:at][s:sy]:sy ==
   phi SYSIG (i2 (pair (pair i a) s));

Den Rekursor symrec erhalten wir durch Instantiierung des allgemeinen Rekursors primrec und einige Umbenennungen. Auch die beiden Gesetze emptyrec und addrec können wir aus dem allgemein gezeigten Lemma primreclaws herleiten. Um das Induktionsprinzip aus indlog herzuleiten, müssen wir sumind und unitind, also die Induktionsprinzipien für die Bestandteile des Signaturfunktors verwenden und außerdem mit Hilfe von prod eta Variablen von Produkttypen expandieren, d.h. a : A × B durch (π_{1}(a), π_{2}(a)) ersetzen.

Die erhaltenen Terme können wir dann zu einem Funktor DatSym des Typs

{Ident:IDENT}{Attrib:ATTRIB}DATSYM Ident Attrib

zusammensetzen und erhalten den gesuchten Funktor Symtab' durch Komposition:

Symtab'[Ident:IDENT][Attrib:ATTRIB] ==
Symtab' pre Ident Attrib (DatSym Ident Attrib):SYMTAB' Ident Attrib

4.4 Implementierung von Symtab' durch wiederholungsfreie Listen

Bei der eben beschriebenen Lösung werden obsolete Einträge weiter in der Symboltabelle geführt, die Funktion lookup greift aber jeweils auf den letzten Eintrag zu, so daß diese nicht in Erscheinung treten. Dies ist — wie bewiesen — zwar korrekt, aber bei sich häufig ändernden Einträgen sehr ineffizient. Eine Möglichkeit, hier Abhilfe zu schaffen, ist es, die Liste der Einträge nur beim erstmaligen Auftreten eines Bezeichners zu verlängern und sonst den alten Eintrag zu entfernen. Da diese Aufgabe weitere noch nicht in Erscheinung getretene Aspekte der Programmverifikation mit Lego verdeutlicht, wollen wir auch diese hier behandeln:

4.4.1 Zerlegung in Symtab'' und SeqPairs

Zunächst wird, wie schon bei ChangeAttrib eine horizontale Zerlegung der Aufgaben vorgenommen: Es wird ein Funktor SeqPairs eingeführt, der eine Listenstruktur über Paaren von Bezeichnern und Attributen erzeugt:

functor SeqPairs
    (structure X : IDENT
    structure Y : ATTRIB
         ) : sig include SEQPAIRS
                 sharing Ident = X and Attrib = Y
             end
    =?

und ein Funktor Symtab'', der aus einer solchen Struktur eine Symboltabelle erzeugt:

functor Symtab''
    (S : SEQPAIRS
         ) : sig include SYMTAB'
                 sharing Ident = X and Attrib = Y
             end = ?

Aus diesen läßt sich durch Komposition der gesuchte Funktor Symtab' zusammensetzen:

functor Symtab'
    (structure X : IDENT
    structure Y :ATTRIB
         ) : sig include SYMTAB'
                 sharing Ident = X and Attrib = Y
             end
    = Symtab''(SeqPairs(structure X = X, structure Y = Y))

Die Signatur SEQPAIRS ist dabei gegeben durch

signature SEQPAIRS =
    sig
        structure Ident:IDENT
        structure Attrib:ATTRIB
        datatype sequence =
          nil
          |cons of (Ident.ident * Attrib.attrib)*sequence
        val null:  sequence -> bool
        axiom null nil = true
        axiom null(cons((i,a),s) = false
        val hd:  sequence->Ident.ident*Attrib.attrib
        axiom hd(cons((i,a),s)) = (i,a)
        val tl:  sequence -> sequence
        axiom tl(cons((i,a),s)=s
    end

4.4.1.1 Lego-Darstellung

Um dies in Lego zu übertragen, haben wir wieder die Signaturen den sharing-Einschränkungen gemäß zu parametrisieren; die durch ”?“ implementierten Funktoren nehmen wir wieder vorläufig als Kontext an, was uns die Verifikation des Zerlegungsschrittes noch vor deren Realisierung ermöglicht:

[SeqPairs:{Ident:IDENT}{Attrib:ATTRIB}SEQPAIRS Ident Attrib];
[Symtab'':{Ident:IDENT}{Attrib:ATTRIB}
     (SEQPAIRS Ident Attrib)->(SYMTAB' Ident Attrib)];
[Symtab':{Ident:IDENT}{Attrib:ATTRIB}SYMTAB' Ident Attrib=
     [Ident:IDENT][Attrib:ATTRIB]Symtab'' Ident Attrib
                                         (SeqPairs Ident Attrib)];

Die Signatur SEQPAIRS ergibt sich dabei zu:

SEQPAIRS[Ident:IDENT][Attrib:ATTRIB] ==
[ident=Ident.1][attrib=Attrib.1]
<sequence:Prop>
<nil:sequence>
<cons:(PROD ident attrib)->sequence->sequence>
<seqrec:{R|Prop}R->((PROD ident attrib)->sequence->R->R)->sequence->R>

({P:sequence->Prop}(P nil)->  seqind

                   ({e:PROD ident attrib}{s:sequence}
                         (P s)->P (cons e s))->
                   {s:sequence}P s) #

({R|Prop}{g:R}{h:(PROD ident attrib)->sequence->R->R}  nilrec

      Q g (seqrec g h nil)) #

({R|Prop}{g:R}{h:(PROD ident attrib)->sequence->R->R}  consrec

{e:PROD ident attrib}{s:sequence}
      Q (h e s (seqrec g h s))(seqrec g h (cons e s))) #
<null:sequence->bool>

(isthecase (null nil)) #  null1
({e:PROD ident attrib}{s:sequence}isnotthecase (null (cons e s))) #  null2

4.4. WIEDERHOLUNGSFREIE LISTEN 69

<hd:sequence->PROD ident attrib>  hdax

({e:PROD ident attrib}{s:sequence}Q (hd (cons e s)) e) #

<tl:sequence->sequence>  tlax

({e:PROD ident attrib}{s:sequence}Q (tl (cons e s)) s)

4.4.2 Zerlegung in Symtab''' und SeqDup

Die Implementierung des Funktors Symtab'' vollzieht sich durch eine weitere Zerlegung:

functor SeqDup
(S:SEQPAIRS
):  sig include SEQDUP
        sharing Seq=S
    end
= ?
functor Symtab'''
(S:SEQDUP
):  sig include SYMTAB'
        sharing Ident=S.Seq.Ident and Attrib=S.Seq.Attrib
    end
= ?

Der Funktor SeqDup fügt dabei zur durch S übergebenen Listenstruktur die Möglichkeit des wiederholungsfreien Anfügens und des Löschens von Einträgen hinzu. Außerdem wird die Struktur um einige Hilfsfunktionen angereichert:

signature SEQDUP =
sig
structure Seq :  SEQPAIRS
open Seq; open Ident; open Attrib
val add :  ident * attrib -> sequence -> sequence
val ismatch :  ident -> sequence -> bool
val remove :  ident -> sequence ->sequence
axiom (ismatch i s) => (add ( i,a) s) = (cons (i,a) (remove i s))
axiom not (ismatch i s) => (add ( i,a) s) = (cons (i,a) s)
axiom (ismatch i nil) = false
axiom (ismatch i (cons (i',a) s)) = (i=i') orelse (ismatch i s)
axiom not (ismatch i (remove i s))
local
val member :  (ident*attrib) -> sequence -> bool
axiom (member e nil) = false
axiom (member e (cons e' s)) = (e=e') orelse (member e s)
in
axiom i<>i' => (member (i',a') (remove i s)) = (member (i',a') s)
end
end

Der Funktor Symtab'' ergibt sich dann durch Komposition:

functor Symtab''
    (S:SEQPAIRS
        ) : sig include SYMTAB'
                sharing Ident=S.Seq.Ident and Attrib=S.Seq.Attrib
            end
    = Symtab'''(SeqDup(S))

Bei der Lego-Darstellung der Signatur SEQDUP stoßen wir dabei auf das Problem der korrekten Modellierung des local-Konstrukts im zweiten die Funktion remove betreffenden Axiom. Überlegen wir uns dazu zunächst, was damit intuitiv gemeint ist: Die local deklarierte Funktion member dient nur der Spezifikation des Verhaltens von remove und braucht von Strukturen, die SEQDUP implementieren, nicht bereitgestellt zu werden. Will man andererseits – etwa bei der Verifikation – einer Implementierung des Funktors Symtab''', in dessen Argument ja eine Struktur der Signatur SEQDUP vorkommt – das zweite remove-Axiom verwenden, so möchte man zumindest von der hypothetischen Existenz einer Funktion member ausgehen. Diese Betrachtungen legen es nahe, das local-Konstrukt typentheoretisch durch den intuitionistischen Existenzquantor zu modellieren. Wir wollen uns dessen Definition und Verwendung kurz vergegenwärtigen:

Intuitionistischer Existenzquantor Durch

Ex[T|Type][P:T->Prop] == A:Prop(t:T(P t)->A)->A

läßt sich in Lego ein Ausdruck definieren, der die intuitionistische, existentielle Quantifizierung wiedergibt. Ist T ein Typ und P:T->Prop ein Prädikat über diesem, so erlaubt es ein Beweis von Ex P, eine beliebige Aussage A aus t:T(P t)->A herzuleiten:

[T:Type][P:T->Prop][H:Ex P]
Goal A;
?0:  A
Refine H:Ex P;
?1:  t:T(P t)->A
Intros t Pt;
t:T
Pt:P t
?3:  A

Wir befinden uns also in einem Kontext, in dem ein Individuum mit der Eigenschaft P nämlich t ”existiert“. Umgekehrt erhalten wir Beweise von Ex P im Kontext

[t:T][Pt:P t] durch ExIntro t Pt, wobei
ExIntro[T|Type][P|T->Prop][t:T[Pt:P t] ==
    [A:Prop][H:t:T(P t)->A]H t Pt

Durch ein Normalisierungsargument kann man zeigen, daß jedem Beweis einer Existenzaussage ein Zeuge und ein Beweis, daß dieser die verlangte Eigenschaft hat, zugrundeliegt. Gleichwohl gestatten Beweise der Existenzaussagen keine nachträgliche Extraktion dieser beiden Komponenten; geschlossene Terme 4.4. WIEDERHOLUNGSFREIE LISTEN 71

witness:(Ex P)->T
proof:H:Ex PP (witness H)

existieren also nicht. Dies macht den intuitionistischen Existenzquantor geeignet zur Modellierung ”versteckter“ Funktionen und Typen, wie member (vgl. dazu auch [MP88]). Die Lego-Darstellung der Signatur SEQDUP ergibt sich daher zu:

[SEQDUP[Ident:IDENT][Attrib:ATTRIB][Seq:SEQPAIRS Ident Attrib]=
[ident=Ident.1][eqid:ident->ident->bool=Ident.2.1][attrib=Attrib.1]
[sequence=Seq.1][nil=Seq.2.1][cons=Seq.2.2.1]
<add:(PROD ident attrib)->sequence->sequence>
<ismatch:ident->sequence->bool>
<remove:ident->sequence->sequence>
(*axioms for add *)
({i:ident}{a:attrib}{s:sequence} (isthecase (ismatch i s)) ->
     Q (add (pair i a) s)
       (cons (pair i a) (remove i s))) #
({i:ident}{a:attrib}{s:sequence}(isnotthecase (ismatch i s)) ->
     Q (add (pair i a) s)
       (cons (pair i a) s)) #
(* axioms for ismatch *)
({i:ident}isnotthecase (ismatch i nil)) #
({i:ident}{i':ident}{a':attrib}{s:sequence}
     Q (ismatch i (cons (pair i' a') s))
       (orelse (eqid i i') (ismatch i s))) #
(* axioms for remove *)
({i:ident}{s:sequence}isnotthecase (ismatch i (remove i s))) #
(* local *)
(Ex [member:(PROD ident attrib)->sequence->bool]
Ex [eqe:(PROD ident attrib)->(PROD ident attrib)->bool]
Ex [eqt:eqtype (PROD ident attrib) eqe]
     (* axioms for member *)
Ex [memnil:{e:PROD ident attrib}isnotthecase (member e nil)]
Ex [memcons:{e,e':PROD ident attrib}{s:sequence}
     Q (member e (cons e' s)) (orelse (eqe e e')(member e s))]
(* in *)
{i,i':ident}{a':attrib}{s:sequence}(isnotthecase (eqid i i'))->
     Q (member (pair i' a') (remove i s))
       (member (pair i' a') s)
)];

Wir beachten, daß aufgrund der sharing-Bedingung im Funktor Symtab''' die Signatur SEQDUP in einer Struktur des Typs SEQPAIRS parametrisiert ist.

Wir können jetzt die vorgenommene Zerlegung auf ihre Korrektheit überprüfen, indem wir die Funktoren SeqDup und Symtab''' annehmen:

[SeqDup:{Ident:IDENT}{Attrib:ATTRIB}{S:SEQPAIRS Ident Attrib}
      SEQDUP Ident Attrib S];

[Symtab''':{Ident:IDENT}{Attrib:ATTRIB}
      {Sp:SEQPAIRS Ident Attrib}
      {S:SEQDUP Ident Attrib Sp}
      SYMTAB' Ident Attrib];

und aus diesen den gesuchten Funktor Symtab'' zusammensetzen:

[Symtab'':{Ident:IDENT}{Attrib:ATTRIB}
      (SEQPAIRS Ident Attrib)->(SYMTAB' Ident Attrib)
=
[Ident:IDENT][Attrib:ATTRIB][S:SEQPAIRS Ident Attrib]
Symtab''' Ident Attrib S (SeqDup Ident Attrib S)];

Wir beachten dabei, wie die durch sharing gebundenen Teile ”weitergereicht“ werden.

Es bleibt nun die Realisierung der beiden hypothetisch angenommenen Funktoren. Beginnen wir mit dem zweiten der beiden:

4.4.3 Implementierung des Funktors Symtab'''

In Extended-ML ergibt sich dieser Funktor zu

functor Symtab'''
    (S : SEQDUP
        ) :  sig include SYMTAB'
                sharing Ident = S.Seq.Ident and Attrib = S.Seq.Attrib
            end
    = struct
        structure Ident :  IDENT = S.Seq.Ident
        structure Attrib :  ATTRIB = S.Seq.Attrib
        type symtab = S.Seq.Sequence
        val empty = S.Seq.nil
        fun add i a s = S.add (i,a) s
        val present = S.ismatch
        fun lookup i s = if (S.Seq.null s) then Attrib.null attrib
                        else let val (i',a') = S.Seq.hd s in
                                if i=i' then a'
                                else (lookup i (S.Seq.tl s)) end
    end

Zu beachten ist, daß hier lookup durch allgemeine Rekursion implementiert wurde. Es ist klar, daß man die Funktion ebensogut durch primitive Rekursion (patternmatching) erhalten hätte, doch wollen wir, da man an diesem Beispiel gut die Verifikation allgemein rekursiver Funktionen studieren kann, dabei bleiben. Für die Lego-Darstellung geben wir uns wiederum die Argumente vor und führen geeignete Abkürzungen ein:

[Ident:IDENT][Attrib:ATTRIB]  Argumente
[ident=Ident.1] [eqid:ident->ident->bool=Ident.2.1]  Abkürzungen

[attrib=Attrib.1] [null attrib=Attrib.2.2.1]

[Sp:SEQPAIRS Ident Attrib]  Argumente
[Ssequence=Sp.1][Snil:Ssequence=Sp.2.1] [Scons:...]  [Sseqind:...]  Abkürzungen

[Sseqrec:  ...][Snilrec:  ...]  [Sconsrec:  ...]
[Snull:  ...][Snull1:  ...]  [Snull2:]
[Shd:  ...]  [Shdax:  ...]
[Stl:  ...  ][Stlax:  ...]

[S:SEQDUP Ident Attrib Sp]  Argumente
[Sadd:  ...][Sadd1:  ...]  [Sadd2:  ...]  Abkürzungen

[Sismatch:  ...][Sismatch1:  ...]  [Sismatch2:  ...]
[Sremove:  ...][Sremove1:  ...]
[Sremove2:  ...]

Durch die Präfigierung verschiedener Objekte und Beweise mit ”S“ wird de-

ren Zugehörigkeit zur Struktur Sp:SEQPAIRS Ident Attrib, bzw: S:SEQDUP Ident

Attrib Sp zum Ausdruck gebracht. Aus diesen Eingabedaten ist eine verifizierte Implementierung von SYMTAB' zu erstellen. Beginnen wir mit dem Typ symtab.

4.4.3.1 Implementierung von symtab

Setzen wir hier, wie im Original, symtab == Ssequence, so können Vertreter s von symtab durchaus einige Einträge doppelt enthalten und da die Axiome über alle Vertreter von symtab quantifiziert sind, wird man diese Fälle dann bei den Beweisen berücksichtigen müssen. Es ist aber unter diesen Voraussetzungen nicht möglich, das im Verlaufe der Verifikation von lookup auftretende Unterziel

{s:symtab}{i,i':ident}
(isnotthecase (eqid i i')) -> Q (lookup i s) (lookup i (Sremove i' s))

also, daß die Entfernung eines Bezeichners aus einer Symboltabelle die anderen Einträge unverändert läßt, zu zeigen. Dies deshalb, weil die Funktion Sremove ihrer Spezifikation gemäß die Reihenfolge der Listeneinträge beliebig verändern kann (Sremove ist nur über member spezifiziert.), so daß obsolete Einträge — so vorhanden — nach vorne geraten könnten.

Beispiel Sei

s := (⟨i, new⟩, ⟨i, old⟩, ⟨i′, foo⟩)

und

                    Sremove i′ s = (⟨i, old⟩, ⟨i, new⟩)

das ist mit der Spezifikation von Sremove durchaus vereinbar, so ist

           (lookup i s) = new ≠ old = (lookup i (Sremove i′ s))

Dieser Fall kann natürlich nicht eintreten, wenn s — wie das ja auch beabsichtigt ist — nur durch empty und add erzeugt wurde, da dann ja veraltete Einträge jeweils entfernt wurden. Dies ist auch der Schlüssel zur Vermeidung des Problems bei der Lego–Verifikation: Wir definieren durch

gen by add[s:Ssequence] ==
{P:Ssequence->Prop}(P Snil)->
    ({s:Ssequence}{e:PROD ident attrib}(P s)->P(Sadd e s))->
    P s

ein Prädikat auf Ssequence, welches zum Ausdruck bringt, daß s nur durch empty und Sadd erzeugt wurde und können dann symtab ähnlich wie die Numerale aus Abschnitt 3.1.5 als ”Teilmenge“ von Ssequence definieren, auf die dieses Prädikat zutrifft:

symtab == <s:Ssequence>gen by add s

Wir können nun natürlich — allein schon aus Typisierungsgründen — auch nicht mehr add == Sadd setzen, sondern müssen definieren:

add[i:ident][a:attrib][s:symtab] ==
(Sadd (pair i a) s.1,
[P:Ssequence->Prop][Pnil:P Snil]
[Pstab:{s:Ssequence}{e:PROD ident attrib}(P s)->P(Sadd e s)]
Pstab s.1 (pair i a) (s.2 P Pnil Pstab) ):symtab

Ebenso setzen wir

empty ==
(Snil,
[P:Ssequence->Prop][Pnil:P Snil]
[ :{s:Ssequence}{e:PROD ident attrib}(P s)->P(Sadd e s)]
Pnil):symtab

Auf diese Weise ist das Problem eliminiert: Wir können — siehe Abschnitt 4.4.3.3 — in der Tat beweisen, daß s:symtab zu jedem Bezeichner höchstens einen Eintrag enthält und somit oben beschriebenes Problem nicht mehr auftritt.^{3} Ein auf der Hand liegender Nachteil ist jedoch, daß Symboltabellen — wegen der Beweiskomponente — nun nicht mehr mit der Leibniz-Gleichheit verglichen werden können. Dies erscheint allerdings ohnehin nicht adäquat, da die Übereinstimmung von Symboltabellen ja nur bis auf beobachtbare Unterschiede (observational equivalence), das sind Resultate der Funktionen auf symtab, interessieren. Da im vorliegenden Beispiel Gleichheit von Symboltabellen nicht erforderlich ist, wurde die Implementierung einer solchen Gleichheitsfunktion nicht vorgenommen.

3Der Verfasser ist der Ansicht, daß das beschriebene Problem keine ”typentheoretische Spitzfindigkeit“ ist, sondern in der Praxis tatsächlich zu äußerst schwer zu entdeckenden bugs führen könnte. Man stelle sich etwa vor, daß in einer späteren Erweiterung in Unkenntnis der beschriebenen Einschränkungen eine Funktion fastadd hinzugefügt wird, die Einträge ohne Rücksicht auf etwa vorhandene obsolete Einträge vorn anfügt. Es könnte dann — allerdings nur in seltenen und kaum reproduzierbaren Fällen (das ist gerade das Problem) — zu falschen Resultaten der Funktion lookup kommen. Bei der beschriebenen Lösung ist diese Komplikation jedoch ausgeschlossen, da solch eine Funktion fastadd gar nicht mit Ziel symtab typisiert werden könnte.

Implementierung der Funktion lookup Im Originalbeispiel ist die Funktion lookup durch allgemeine Rekursion gegeben. Für die Lego-Darstellung wollen wir daher die in 3.3 beschriebene Methode einsetzen. In dieser steht die Variable, nach der rekurriert wird, immer an erster Stelle, daher — und auch wegen der Konstruktion von symtab, die wir bei den Beweisen nicht ”mitschleppen“ wollen — definieren wir durch Rekursion zunächst eine Funktion

lookup tw:Ssequence->ident->attrib, aus der wir lookup dann gemäß
lookup:ident->symtab->attrib ==
[i:ident][s:symtab]lookup tw s.1 i

gewinnen. Nun also zur rekursiven Definition von lookup tw: Dazu ist zunächst ein Terminierungsbeweis für obiges Rekursionsschema erforderlich. In diesem Fall zeigt man die Terminierung durch Induktion über die Länge des (als Liste aufgefaßten) Arguments s. Wir definieren also durch primitive Rekursion eine Längenfunktion

Slength:Ssequence->nat == Sseqrec
    zero
    ([ :PROD ident attrib][ :Ssequence][n:nat]succ n)

Diese werden wir als Komplexitätsmaß für die Rekursion verwenden. Als nächstes brauchen wir die Abbruchkonstante. Bei Vorliegen der Abbruchbedingung Snull soll unabhängig von i der Wert null attrib zurückgegeben werden:

lkup base=[ :ident]null attrib

Diese ist selbst eine Funktion, da der Wertebereich von lookup ja ident->attrib ist. Das eigentliche Rekursionsschema ist gegeben durch

lkup scheme[s:Ssequence][lk:Ssequence->ident->attrib] ==
[i:ident] let (Shd s) ([e:PROD ident attrib][i'=pi1 e][a'=pi2 e]
            if (eqid i i') a'
                           (lk (Stl s) i))

wobei let durch

let[A,B|Prop] == [a:A][f:A->B]f a

definiert ist. Wir haben nun zu zeigen, daß die Abbruchbedingung mit dem Komplexitätsmaß verträglich ist:

Goal base condition Snull Slength;

Refine Sseqind ...  Mit Induktion

...
Save lkup bc;

und, daß die Anwendung des Schemas das Komplexitätsmaß echt reduziert wird:

Goal cont condition Snull lkup scheme Slength;

...  ebenso durch Induktion

Save lkup cc;

Aus diesen Daten können wir jetzt lookup tw durch Rekursion definieren:

lookup tw:Ssequence->ident->attrib ==
   recurse Snull lkup base lkup scheme Slength

Wir beachten, daß die Beweise lkup bc und lkup cc hier nicht eingehen; sie werden erst bei Verwendung der Rekursionsgleichungen und der Fixpunktinduktion erforderlich.

Es sind jetzt alle Funktionen implementiert, wir könen daran gehen, die zugehörigen Beweise zu liefern.

4.4.3.2 Verifikation der Funktionen present und add

Es ist zu zeigen:

Goal {i:ident}isnotthecase (present i empty);  und

Goal {a':attrib}{s:symtab}{i,i':ident}
                 Q (present i (add i' a' s))
                   (orelse (eqid i i')(present i s));

Ersteres folgt unmittelbar aus Sismatch1, während wir für den Beweis der zweiten Aussage — wie im Orginal von Sannella — folgendes Lemma verwenden.

Goal {i,i':ident}{s:Ssequence}
(isnotthecase (eqid i i'))->
     Q (Sismatch i (Sremove i' s)) (Sismatch i s);

welches zum Ausdruck bringt, daß Sremove keine Bezeichner hinzufügt und auch nicht mehr, als angegeben, entfernt. Nehmen wir zunächst an, dies sei schon gezeigt. Dann folgt die Aussage über present und add durch Fallunterscheidung nach Sismatch i' s sowie eqid i i' und einfache Gleichungsumformungen.

Der Beweis des Lemmas gestaltet sich nun etwas komplizierter, da wir die Funktion Sremove nur im Kontext von member kennen. Wir haben daher zunächst einen Zusammenhang zwischen Sismatch und member herzustellen. Etwa

(isthecase (Sismatch i s))->
Ex ([a:attrib]isthecase (member (pair i a) s));

In dieser Form können wir die Aussage aber gar nicht formulieren, da member ja nur lokal im Axiom Sremove2 vorkommt. Wir haben den Zusammenhang daher in einer beliebigen Funktion member, die den Axiomen genügt, parametrisiert zu formulieren:

Goal {i:ident}{s:Ssequence}
{member:(PROD ident attrib)->Ssequence->bool}
{eqe:(PROD ident attrib)->(PROD ident attrib)->bool}
{eqt:eqtype (PROD ident attrib) eqe}
{memnil:{e:PROD ident attrib}isnotthecase (member e Snil)}
{memcons:{e,e':PROD ident attrib}{s:Ssequence}
Q (member e (Scons e' s)) (orelse (eqe e e')(member e s))}
(isthecase (Sismatch i s)) ->
Ex ([a:attrib]isthecase (member (pair i a) s))

Diesen Satz können wir nun durch Induktion über s und einige Fallunterscheidungen beweisen.

Save ismtomem;

Auf den ersten Blick verwunderlich ist vielleicht die Tatsache, daß es uns hier auch in einer intuitionistischen Umgebung gelingt, aus dem bloßen Vorhandensein eines Eintrags, das zugehörige Attribut in Form der Existenzaussage tatsächlich namhaft zu machen. Dies liegt daran, daß im Verlauf der Induktion ja alle Einträge von s zugänglich werden. Wir brauchen nun noch die andere Richtung der Aussage:

Goal {i:ident}{s:Ssequence}

...  Parametrisierung durch member

Ex ([a:attrib]isthecase (member (pair i a) s)) ->
   (isthecase (Sismatch i s))

Diese beweist man ebenso durch Induktion über s.

Save memtoism;

Schließlich brauchen wir auch noch Kontrapositionen dieser beiden Aussagen, in denen die Existenzquantoren in Allquantoren umgewandelt werden; diese erhalten wir aber durch einfache logische Umformungen.

Mit Hilfe dieser Beziehungen ist es jetzt ein leichtes, das Lemma zu zeigen und somit die empty, present und add betreffenden Axiome.

4.4.3.3 Verifikation von lookup

Diese Beweise sind die kompliziertesten des gesamten Beispiels. Ihre Schwierigkeit rührt vor allem von dem eingangs beschriebenen Problem mit Sremove und von der rekursiven Formulierung der Funktion lookup her.

Zunächst müssen wir beweisen, daß in einer Symboltabelle, also einer durch empty und add erzeugten Sequenz zu jedem Bezeichner höchstens ein Eintrag steht. In Lego formulieren wir das so:

Goal ...
{s:symtab}{i:ident}{a,a':attrib}
   (isthecase (member (pair i a) s.1))->
   (isthecase (member (pair i a') s.1))->Q a a');
...
Save uniqueids;

Die Ellipse (dots) steht für die wiederum erforderliche Quantifizierung wegen der Unzugänglichkeit von member. Der etwas umständliche Beweis verwendet Induktion über s und einige Fallunterscheidungen.

Als nächstes zeigen wir, daß lookup tatsächlich den Wert null attrib liefert, falls keine Übereinstimmung auftritt:

Goal {i:ident}{s:Ssequence}
(isnotthecase (Sismatch i s))->Q null attrib (lookup tw s i);

Diesen Beweis führen wir mit recind, dem in Abschnitt 3.3 besprochenen Beweisprinzip für rekursiv definierte Funktionen. Der Induktionsanfang ergibt sich aus der Definition von lookup, den Induktionsschritt zeigen wir durch Fallunterscheidung. Nun haben wir zu zeigen, daß das Auftreten eines Eintrags in der Liste das Resultat des entsprechenden lookup-Aufrufs festlegt:

Goal ...  Parametrisierung durch member

{i:ident}{a:attrib}{s:symtab}
   (isthecase (member (pair i a) s.1))->
   (Q a (lookup i s));

Dieser Beweis ergibt sich relativ leicht aus dem oben gezeigten Lemma uniqueids. Schließlich haben wir noch einen weiteren Zusammenhang zwischen lookup und member herzustellen: Wir wollen zeigen, daß lookup außer null attrib nur Resultate produziert, die wirklich in der Tabelle vorhanden sind:

Goal ...  Parametrisierung durch member

{i:ident}{s:Ssequence}(isthecase (Sismatch i s))->
isthecase (member (pair i (lookup tw s i)) s);

Auch für dieses Lemma brauchen wir die ”Scott-Induktion“ recind. Die Beweise der Axiome über lookup können nun durch Induktion und Fallunterscheidung in einfacher Weise geführt werden. Durch Zusammensetzen und folgende Abstraktion erhalten wir den Funktor Symtab'''.

4.4.3.4 Implementierung von SeqDup

Es bleibt nun noch die Realisierung der Funktoren SeqDup und SeqPairs, welche die entsprechenden Listenstrukturen bereitstellen. Bei der Implementierung von SeqDup müssen wir dann, wie in Abschnitt 4.4.2 angedeutet, die Funktion member implementieren (nur so kann der Beweis für ihre Existenz geführt werden). Zu diesem Zweck benötigen wir auch eine entscheidbare Gleichheit auf Attrib. In einer persönlichen Mitteilung hat Don Sannella darauf aufmerksam gemacht, daß dies im allgemeinen nicht adäquat sei, da man zur Spezifikation (nur dieser dient member) evtl. auch nicht–implementierbare Funktionen heranziehen möchte.Wie es allerdings möglich ist, das dieser Überlegung zugrundeliegende Konzept der Persistenz [Far90] typentheoretisch zu modellieren, ist noch unbekannt.

Da bei den Implementierungen weiter keine neuen Konzepte und Ideen Verwendung finden, wollen wir sie hier nicht beschreiben. Es wurden allerdings alle Schritte mit Lego durchgeführt.

Wir haben jetzt die Symboltabelle vollständig verifiziert und implementiert. Falls wir den Funktor Symtab mit geeigneten eqtypes Ident und Attrib instantiieren (Wir können für beides nat wählen), so sind prinzipiell auch Berechnungen durch Normalisierung möglich.

Schlußbetrachtung

5.1 Zusammenfassung

Wir haben nun vorgeführt, wie die wichtigsten Konstrukte der Programmiersprache ML einschließlich der Funktoren im Extended Calculus of Constructions bzw. in Lego interpretiert werden können. Diese Interpretation wurde dazu verwendet, modulare ML-Programme mit Hilfe der internen Logik des ECC zu verifizieren, bzw. verifiziert zu implementieren. Es wurde versucht, zu verdeutlichen, wie sich auch die Verifikation großer Programme gemäß deren Modulstruktur vollzieht. Die semantische Begründung der Modellierung des nichtmodularen Teils gründete sich dabei auf die Initiale-Algebra-Interpretation induktiver Datentypen [LS81, GTWW77], die des Modulkonzepts auf die denotationelle Semantikgebung aus [MH88]. Das dort gegebene ”Verflachungsargument“: ‘… it is possible to treat … functor declarations by simple macro expansion’ überträgt sich auch auf die Verifikation: Liegt eine vollständige modulare verifizierte Implementierung vor, so läßt sich aus dieser sowohl die nichtmodulare Implementation, als auch die nichtmodulare Verifikation durch Projektion extrahieren. An einem komplexeren Beispiel wurde die Vorgehensweise konkretisiert und ihre praktische Durchführbarkeit gezeigt.

5.2 Einordnung

Die Anreicherung von Signaturen um Axiome geht auf Extended ML [ST86] zurück; in diesem Ansatz findet Verifikation bislang allerdings nur informell statt. Die typentheoretischen Repräsentationen induktiver Datentypen sind inzwischen zu einer Art Allgemeingut geworden. Für Zwecke der formalen Programmentwicklung wurden sie bereits von Paulin-Mohring [PM89] und Martin-Löf^{1} [NPS90] verwendet; bei beiden steht aber nicht die verifizierte Implementierung gegebener Spezifikationen, sondern die Extraktion verifizierter Programme aus intuitionistischen Beweisen gewisser Π_{2}^{0}-Sätze im Vordergrund. Eine verwandte Arbeit ist [Luo91],in der Zusammenhänge zwischen typentheoretischer und algebraischer Spezifikation [Wir90] beschrieben werden und auch von Erfahrungen mit Lego berichtet wird.

1Martin-Löf verwendet nicht die imprädikativen Repräsentationen, sondern erhält induktive Datentypen durch strukturelle Regeln

5.3 Ausblick und Anregungen zu weiterführender Arbeit

5.3.1 Abstrakte Datentypen

Das abstype–Konstrukt von ML zur Definition abstrakter Datentypen, wie stack, set oder bag wurde in dieser Arbeit nicht untersucht. In [MH88] wird vorgeschlagen, diese durch Funktoren zu ersetzen. Dies ist im wesentlich auch der in [Mac84] beschrittene Weg. In [MP88] dagegen werden dafür intuitionistische Existenzquantoren ähnlich wie bei der Modellierung des local-Konstrukts in Abschnitt 4.4.2. Beide Möglichkeiten wären auf ihre Vor– und Nachteile mit Hilfe von Lego zu untersuchen.

5.3.2 Imperative Strukturen

wie Zeiger, Wertzuweisungen, continuations oder Ausnahmebehandlungen (exceptions) haben wir ebenfalls nicht berücksichtigt. Manche Autoren argumentieren dafür, daß diese in zukünftigen stark parallelisierbaren Sprachen auch keinen Platz mehr hätten. (In [Cou90b] findet sich ein entsprechendes Zitat.) Der Verfasser ist allerdings der Ansicht, daß zumindest exceptions nach wie vor ihre Berechtigung haben. Ohne imperative Abbruchmöglichkeit böte beispielsweise die parallele Suche in einem Baum keinen wesentlichen Vorteil gegenüber der sequentiellen.

Zur typentheoretischen Modellierung imperativer Strukturen bietet sich Moggis computational monads Ansatz an [Mog90]. Zur Darstellung von Ausnahmebehandlungen etwa würde man dann ein Tripel (T, μ, η) mit T (X) = X + E (E ist die Menge der Ausnahmen) fixieren; Funktionen zwischen Typen A und B sind dann nicht mehr Vertreter von A → B, sondern von A → T (B). Deren Komposition ist wie in der Kleisli-Kategorie [LS85] erklärt.

Da es, wie wir in Abschnitt 3.1.2 gesehen haben, möglich ist, Funktoren und strength im ECC auszudrücken, sollte es auch möglich sein, die beschriebene Vorgehensweise auf diese Art auszubauen. Ob dies allerdings die in ML und anderen funktionalen Programmierprachen vorhandenen Ausnahmebehandlungen adäquat modelliert, bleibt zu untersuchen.

5.3.3 Partialität

Wie in der Arbeit mehrfach erwähnt, erlaubt die Entscheidung für die Modellierung aller vorkommenden Funktionen als ”ausführbare“ CC-Terme keine Darstellung echt partieller Funktionen und somit auch nicht aller totalen rekursiven Funktionen. Verschiedene Autoren [BTM90, Rey90] schlagen vor, aus dieser Not eine Tugend zu machen und eine echte Programmiersprache ohne allgemeine Rekursion und ohne Partialität zu entwickeln, die aufgrund der dann gegebenen starken Normalisierung leichter parallelisiert werden könnte (Die Auswertereihenfolge spielt keine Rolle.). In 5.3. AUSBLICK UND ANREGUNGEN ZU WEITERFÜHRENDER ARBEIT 81

dieser Arbeit wurde dazu insofern ein Anfang gemacht, als gezeigt wurde, wie sich auch allgemein rekursiv gegebene Algorithmen, denen aber eine im CC darstellbare Funktion zugrundeliegt, ohne sinnentstellende Abänderungen in solch einer Sprache formulieren lassen.

5.3.4 Komplexität

Verschiedentlich wird als Nachteil der imprädikativen Repräsentationen induktiver Datentypen deren Ineffizienz angesehen (Die Berechnung des Vorgängers eines Numerals n erfordert n β-Reduktionen.). Deren Sinn liegt jedoch keineswegs in der Abwicklung wirklicher Berechnungen (obwohl dies prinzipiell natürlich möglich ist), sondern in der Modellierung von Programmen einer anderen, effizienteren Programmiersprache. Möchte man diese nicht nur verifizieren, sondern auch über deren Komplexität Aussagen machen, so stellt die Zahl der β-Reduktionen für die Berechnung im typentheoretischen Modell zwar ein mögliches, aber im allgemeinen nicht adäquates Maß dar. Eine Möglichkeit, hier Abhilfe zu schaffen, besteht darin, frei definierte Komplexitätsmaße jedem Modul, bzw. jeder Funktion — ähnlich, wie die Korrektheitsbeweise — mitzugeben. Per Komposition vererbt sich dann das Komplexitätsmaß auch auf zusammengesetzte Funktionen und Moduln. Spezifikationen wären dann nicht mehr Typen der Form Σt:τ.σ(t), sondern Σt:τ.σ(t) × Σk:κ.ρ(k, t), wobei κ den Typ des Komplexitätsmaßes bezeichnet und ρ(k, t) zum Ausdruck bringt, daß die Implementierung t die Komplexität k besitzt. Vgl. dazu auch [Gur91].

5.3.5 Parallele Konstrukte und Nebenläufigkeit

In der letzten Zeit sind Erweiterungen funktionaler Sprachen um Prozeßkonstrukte und Parallelität untersucht worden [GMP89, Hol83, Nes91]. Wie typentheoretische Verifikation auch solcher Programme aussehen könnte, ist im Augenblick noch unbekannt. Grundsätzlich möglich erscheint es, prozeßhaftes Verhalten durch Codatentypen (Abschnitte 2.1 und 2.2) zu modellieren; ebenfalls vielversprechend ist die — allerdings noch in den Anfängen steckende — Erweiterung von propositions as types auf Prozesse und Lineare Logik [Abr91]. Eine Abhandlung über Zusammenhänge von Typentheorie und Nebenläufigkeit findet sich in [CP88].

5.3.6 PER-Semantik funktionaler Programmiersprachen

Eine Klasse von Modellen des Calculus of Constructions wird durch die Kategorie P ER(D) der partiellen Äquivalenzrelationen auf einer kombinatorischen Algebra, etwa D = ω gegeben. Für eine genaue Definition dieser Kategorie cf. [Luo90, Str89]. Luo beweist ein Reflektionsresultat, welches zum Ausdruck bringt, daß die Leibniz-Gleichheit auf der Ebene der PER-Modelle die ”wirkliche“ Gleichheit widerspiegelt [Luo90].

Dem nichtmodularen Teil einer funktionalen Pogrammiersprache kann man nun eine operationelle Semantik geben als Funktor von ihrer syntaktischen Kategorie (Typen als Objekte, Funktionsterme als Morphismen [BW90]) in die Kategorie P ER(ω): Typen ordnet man dabei die Menge der internen Repräsentationen (via Codierung sind das natürliche Zahlen) ihrer Vertreter zu (dies läßt sich als partielle Äquivalenzrelation auffassen, deren domain gerade diese Menge ist und die auf diesem als die Gleichheit auf dem Typen erklärt ist.). Funktionsterme werden abgebildet auf die sie auf dem Niveau der internen Repräsentationen realisierenden partiell rekursiven Funktionen. Dies sind per definitionem PER-Morphismen. Man könnte nun untersuchen, inwieweit diese Semantikgebung mit der in der Arbeit vorgestellten Interpretation verträglich ist, d.h. ob die PER-Interpretationen von ML-Termen mit den PER-Interpretationen der entsprechenden CC-Termen identisch oder zumindest isomorph sind. Dies dürfte der Fall sein, sollte jedoch — auch in Hinblick auf die parametrische PER-Interpretation nach [BFŠS90] — genauer untersucht werden.

5.4 Wertung

Ob sich maschinenunterstützte Programmverifikation tatsächlich praktisch einsetzen läßt, wird nur die Zukunft klären können. Immerhin hat das Beispiel gezeigt, daß auch bei genauer informeller Verifikation Fehler auftreten können, die bei maschineller Überprüfung zutage treten. Der Autor vertritt jedoch den Standpunkt, daß der hauptsächliche Wert von Arbeiten wie der vorliegenden in der Gewinnung neuer Einsichten in die Theorie der Programmierung und in der möglichen Entwicklung neuer Programmiersprachen liegt.

Literatur

[Abr91] Samson Abramsky. Proofs as processes. Vortrag auf dem International Symposium on Theoretical Computer Science in honor of Boris Trakhtenbrot, Tel-Aviv, Juni 1991.

[AL^{+}90] Thorsten Altenkirch, Zhaohui Luo, et al. Equality for categories. e–mail, Apr.–Sep. 1990. unpublished.

[Alt90] Thorsten Altenkirch. Impredicative representations of categorical datatypes, thesis proposal. University of Edinburgh, 10 1990. unpublished.

[Bar84] Hendrik Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, second edition, 1984.

[Bar90] Hendrik Barendregt. Functional programming and lambda calculus. In Formal Models and Semantics, chapter 7, pages 321–363. Elsevier Science, 1990. Handbook of Theoretical Computer Science, Volume B.

[BB85] Corrado Boehm and Alessandro Berarducci. Automatic Synthesis of typed λ-programs on Term Algebras. Technical Report 39, Theoretical Computer Science, North Holland, 1985.

[BFŠS90] E. S. Bainbridge, P. J. Freyd, A. Ščedrov, and P. J. Scott. Functorial polymorphism. Theoretical Comp. Sci., 1990.

[BM90] Rod Burstall and James McKinna. Deliverables: An approach to program semantics in constructions. In Proceedings of the First Workshop on Logical Frameworks, 1990.

[BMM90] K. Bruce, A. Meyer, and J. Mitchell. The semantics of the second-order lambda calculus. In G. Huet, editor, Logical Foundations of Functional Programming. Addison-Wesley, 1990.

[BMS80] Rod Burstall, D. MacQueen, and D. Sannella. Hope: an experimental applicative language. In Proc. 1980 LISP Conference, Stanford, California, 1980.

[BTM90] Val Breazu-Tannen and A. Meyer. Computable values can be classical. In G. Huet, editor, Logical Foundations of Functional Programming. Addison– Wesley, 1990.

[BW85] Michael Barr and Charles Wells. Toposes, Triples and Theories. Springer, 1985.

[BW90] Michael Barr and Charles Wells. Category Theory for Computing Science. International Series in Computer Science. Prentice Hall, 1990.

[CH88] Thierry Coquand and Gérard Huet. The calculus of constructions. Information and Computation, 76:95–120, 1988.

[CH90] R. L. Constable and D. J. Howe. Nuprl as a general logic. In Piergiorgio Odifreddi, editor, Logic and Computer Science, pages 123–196. Academic Press Ltd., 1990.

[Coq85a] Thierry Coquand. Sur l’analogie entre les propositions et les types. In Guy Cousineau, Pierre Louis Curien, and Bernard Robinet, editors, Combinators and Funcional Programming Languages, pages 71–84. LNCS 242, Springer, 1985.

[Coq85b] Thierry Coquand. Une théorie des constructions. PhD thesis, Université Paris VII, 1 1985. Thèse de 3ème cycle.

[Coq90] Thierry Coquand. Metamathematical investigations of a calculus of constructions. In Piergiorgio Odifreddi, editor, Logic and Computer Science, pages 91–118. Academic Press Ltd., 1990.

[Cou90a] Bruno Courcelle. Recursive applicative program schemes. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B. Elsevier, 1990.

[Cou90b] Guy Cousineau. Introduction to Part I (CAML: The Theory, the Machine and the Language). In G. Huet, editor, Logical Foundations of Functional Programming. Addison-Wesley, 1990.

[CP88] Rance Cleaveland and Prakash Panangaden. Type theory and concurrency. International Journal of Parallel Processing, 17(2):153–206, 1988.

[CPM89] T. Coquand and C. Paulin-Mohring. Inductively defined types. In LNCS 389. Springer, 1989.

[Far90] Jordi Farrès-Casals. Proving correctness w.r.t. specifications with hidden parts. In Algebraic and Logic Programming, pages 25–39. Springer, 1990. LNCS 463.

[Gir71] Jean-Yves Girard. Une extension de l’interpretation de Gödel à l’analyse, et son application à l’élimination des coupures dans l’analyse et la théorie des types. In J. E. Fenstad, editor, 2nd Scandinavian Logic symposium, pages 63–92. North Holland, 1971.

[GMP89] Alessandro Giacalone, Prateek Mishra, and Sanjiva Prasad. FACILE: A Symmetric Integration of Concurrent and Functional Programming. In Theory and Practice of Software Development (TAPSOFT), pages 184–209. Springer, 1989. LNCS 352.

[GTWW77] J. Goguen, J. Thatcher, E. Wagner, and J. Wright. Initial algebra semantics and continuous algebras. JACM, 24, 1977.

[Gur91] Douglas J. Gurr. Semantic Frameworks for Complexity. PhD thesis, University of Edinburgh, 1991.

[Hag87] Tatsuya Hagino. A Categorical Programming Language. PhD thesis, University of Edinburgh, 1987.

[Har86] Robert Harper. Introduction to Standard ML. Report ECS-LFCS-86-14, University of Edinburgh, 1986.

[Hey56] Arend Heyting. Intuitionism: An Introduction. Amsterdam, 1956.

[HMM87] Robert Harper, David MacQueen, and Robin Milner. Standard ML. LFCS Education. University of Edinburgh, May 1987. A five day course Functional Programming in ML; Part I: The Standard ML Core Language (Milner); Part II: Standard ML Input/Output (Harper); Part III: Modules for Standard ML (MacQueen).

[HMT89] Robert Harper, Robin Milner, and Mads Tofte. The definition of Standard ML (version 3). Report ECS-LFCS-89-81, University of Edinburgh, May 1989.

[Hol83] Sören Holmström. PFL: A functional language for parallel programming, and its implementation. Programming Methodology Group, Report 7, University of Goteborg and Chalmers University of Technology, September 1983.

[HS79] Horst Herrlich and George Strecker. Category Theory. Heldermann, Berlin, second edition, 1979.

[Hue88] Gérard Huet. A uniform approach to type theory. Rapports de Recherche 795, INRIA, Fevrier 1988.

[Hyl82] J. Martin E. Hyland. The effective topos. In A.S̃. Troelstra and D. van Dalen, editors, The L. E. J. Brower Centenary Symposium, pages 165–216. North-Holland, 1982.

[Koc70] A. Kock. Strong functors and monoidal monads. Various Publications Series 11, Aarhus Universitet, 1970.

[Lam70] Joachim Lambek. Subequalizers. Canad. Math. Bull., 13:337–349, 1970.

[LB88] Butler Lampson and Rod Burstall. Pebble, a kernel language for modules and abstract data types. Information and Computation, 76:278–346, 1988.

[LPT89] Zhaohui Luo, Randy Pollack, and Paul Taylor. How to Use LEGO (A Preliminary User’s Manual). Technical Report 27, Laboratory for Foundations of Computer Science, Oct. 1989.

[LS81] Daniel J. Lehmann and Michael B. Smyth. Algebraic specification of data types: A synthetic approach. Mathematical Systems Theory, 14:97–139, 1981.

[LS85] Joachim Lambek and Philip Scott. Introduction to Higher-Order Categorical Logic. Cambridge University Press, 1985.

[Luo90] Zhaohui Luo. An Extended Calculus of Constructions. PhD thesis, University of Edinburgh, July 1990.

[Luo91] Zhaohui Luo. Program specification and data refinement in type theory. Technical report, LFCS, 1991.

[M^{+}90] Eugenio Moggi et al. Higher order modules and the phase distinction. Technical report, LFCS Edinburgh, 1990.

[MA86] Ernest G. Manes and Michael A. Arbib. Algebraic Approaches to Program Semantics. Springer, 1986.

[Mac71] Saunders Mac Lane. Categories for the Working Mathematician. Springer, 1971.

[Mac84] David MacQueen. Modules for Standard ML. In LISP and Functional Programming, pages 198–207. ACM, 1984.

[Mes88] José Meseguer. Relating models of polymorphism. Internal Report SRI-CSL-88-13, Computer Science Laboratory, SRI International, Menlo Park, CA, October 1988.

[MH88] John Mitchell and Robert Harper. The essence of ML. In Principles of Programming Languages, pages 28–46. ACM, January 1988.

[ML71] Per Martin-Löf. A theory of types. manuscript, 1971.

[ML84] Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis·Napoli, 1984.

[Mog89] Eugenio Moggi. A category-theoretic account of program modules. In Category Theory and Computer Science. Springer, LNCS 389, 1989.

[Mog90] Eugenio Moggi. Notions of computation and monads. Information and Computation, eingereicht 1990.

[MP88] John C. Mitchell and Gordon D. Plotkin. Abstract types have existential type. ACM Transactions on Programming Languages and Systems, 10(3):470–502, July 1988.

[MT] Thomas S. E. Maibaum and Wladyslaw M. Turski. On what is exactly going on when software is developed step-by-step.

[Nes91] Uwe Nestmann. Parallele Prozesse und Funktionale Sprachen. Diplomarbeit, Universität Erlangen, 1991.

[NPS90] B. Nordström, K. Petersson, and J. M. Smith. Programming in Martin-Löfs Type Theory, An Introduction. Clarendon Press, Oxford, 1990.

[PM86] C. Paulin-Mohring. Exemples de développements de programmes dans la théorie des constructions. Rapports de Recherche 497, INRIA, 1986.

[PM89] Christine Paulin-Mohring. Extracting F^{ω}–programs from proofs in the calculus of constructions. In Proc. POPL, 1989.

[Pol88] Randy Pollack. The Theory of LEGO. draft, 19 1988.

[Rey74] John C. Reynolds. Towards a theory of type structure. In Paris Logic Colloquium on Programming, pages 408–425. Springer, LNCS 19, Berlin, Heidelberg, New York, 1974.

[Rey90] J. C. Reynolds. Introduction to part II (the polymorphic lambdacalculus). In G. Huet, editor, Logical Foundations of Functional Programming. Addison-Wesley, 1990.

[Ros84] H. E. Rose. Subrecursion. Clarendon Press, Oxford, 1984.

[RP88] John C. Reynolds and Gordon D. Plotkin. On functors expressible in the polymorphic typed lambda calculus. Technical Report ECS-LFCS-88-53, University of Edinburgh, May 1988.

[San89] Donald Sannella. Formal program development in Extended ML for the working programmer. Report ECS-LFCS-89-102, Univ. of Edinburgh, December 1989.

[Šče90] André Ščedrov. A guide to polymorphic types. In Piergiorgio Odifreddi, editor, Logic and Computer Science, pages 387–407. Academic Press Ltd., 1990.

[See87] Robert A. G. Seely. Categorical semantics for higher-order polymorphic λ-calculus. Journal of Symbolic Logic, 52(4):969–989, December 1987.

[ST86] Donald Sannella and Andrzej Tarlecki. Extended ML: An institutionindependent framework for formal program development. In Category Theory and Computer Programming, pages 364–389. Springer, 1986. LNCS 240.

[ST87] Donald Sannella and Andrzej Tarlecki. On Observational Equivalence and Algebraic Specification. Journal of Computer and System Sciences, 34:150– 178, 1987. extended abstract in LNCS 185, 308–322, 1985.

[Str89] Thomas Streicher. Correctness and Completeness of a Categorical Semantics of the Calculus of Constructions. PhD thesis, Universität Passau, Passau, West Germany, June 1989.

[Tai61] W. W. Tait. Nested recursion. Math. Ann., 143, 1961.

[Tay89] Paul Taylor. Playing with LEGO: Some Examples of Developing Mathematics in the Calculus of Constructions. Technical Report 89, Laboratory for Foundations of Computer Science, Aug. 1989.

[Wir90] Martin Wirsing. Algebraic specification. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B. Elsevier, 1990.

[Wra89] Gavin C. Wraith. A note on categorical datatypes. LNCS, 389, 1989.