TECHNISCHE UNIVERSITÄT MÜNCHEN INSTITUT FÜR INFORMATIK

Definitorische Konstruktion induktiver Datentypen in

Isabelle/HOL

Diplomarbeit

Stefan Berghofer

[figure]

INSTITUT FÜR INFORMATIK TECHNISCHE UNIVERSITÄT

MÜNCHEN

Definitorische Konstruktion induktiver Datentypen in

Isabelle/HOL

Diplomarbeit

Stefan Berghofer

Aufgabensteller : Prof. Tobias Nipkow, Ph.D.
Betreuer  : Markus Wenzel

David von Oheimb

Abgabedatum : 24. September 1998

Ich versichere, daß ich diese Diplomarbeit selbständig verfaßt und nur die angegebenen Quellen und Hilfsmittel verwendet habe.

\frac{München, den 24. September 1998}{(Stefan Berghofer)}

Zusammenfassung

Induktive Datentypen stellen ein wichtiges Hilfsmittel zur Spezifikation funktionaler Programme dar. Wir beschreiben die Implementierung eines Datentyppakets für Isabelle/HOL, das neue Datentypen definitorisch einführt. Hierfür wird zunächst die repräsentierende Menge des Datentyps induktiv definiert und dann die Isomorphie zwischen dieser Menge und dem neuen Typ durch eine HOL-Typdefinition ausgedrückt. Aus dieser Definition werden dann wichtige charakteristische Eigenschaften des Datentyps wie Verschiedenheit und Injektivität der Konstruktoren sowie eine strukturelle Induktionsregel abgeleitet. Ebenfalls durch eine induktive Definition wird ein Kombinator für primitive Rekursion auf dem Datentyp konstruiert.

Durch die definitorische Vorgehensweise wird sichergestellt, daß durch das Hinzufügen von Datentypen zu Theorien die Existenz von Modellen erhalten bleibt.

Das beschriebene Datentyppaket erlaubt die Definition von verschränkt und verschachtelt rekursiven Datentypen, so daß die meisten für die praktische Anwendung wichtigen Klassen von Datentypen abgedeckt sind. Des weiteren kann das Paket leicht auf Datentypen mit beliebigem Verzweigungsgrad erweitert werden.

Inhaltsverzeichnis

1 Einleitung 1 1.1 Motivation und Einordnung . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Aufgabenstellung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.3 Aufbau der Arbeit . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.4 Einführendes Beispiel . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2

2 Grundlagen und Werkzeuge 6 2.1 Isabelle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.2 Isabelle/HOL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7

2.2.1 Typen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.2.2 Logische Verknüpfungen und Inferenzregeln . . . . . . . . . . . . . . . 9 2.2.3 Definitorische Theorieerweiterung . . . . . . . . . . . . . . . . . . . . . 11

2.3 Theoretische Grundlagen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.3.1 Fixpunkte . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.3.2 Induktive Definitionen . . . . . . . . . . . . . . . . . . . . . . . . . . . 15

3 Arten und Eigenschaften von Datentypen 24 3.1 Grundlagen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 3.2 Verschränkt rekursive Datentypen . . . . . . . . . . . . . . . . . . . . . . . . 26 3.3 Verschachtelt rekursive Datentypen . . . . . . . . . . . . . . . . . . . . . . . . 30

4 Konstruktion von Datentypen in HOL 36 4.1 Auffalten verschachtelt rekursiver Definitionen . . . . . . . . . . . . . . . . . 37 4.2 Konstruktion der repräsentierenden Mengen . . . . . . . . . . . . . . . . . . . 38

4.2.1 Ein Universum für rekursive Typen . . . . . . . . . . . . . . . . . . . . 39 4.2.2 Induktive Definition der repräsentierenden Mengen . . . . . . . . . . . 41

4.3 Beweis von Isomorphie-Eigenschaften . . . . . . . . . . . . . . . . . . . . . . . 43 4.3.1 Definition von Repräsentationsfunktionen . . . . . . . . . . . . . . . . 45 4.3.2 Surjektivität der Repräsentationsfunktionen . . . . . . . . . . . . . . . 47 4.3.3 Injektivität der Repräsentationsfunktionen . . . . . . . . . . . . . . . 49 4.3.4 Wertebereich der Repräsentationsfunktionen . . . . . . . . . . . . . . 52 4.3.5 Umkehrung der Repräsentationsfunktionen . . . . . . . . . . . . . . . 53

4.4 Definition der Konstruktoren . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 4.5 Repräsentationsabhängige Beweise . . . . . . . . . . . . . . . . . . . . . . . . 54

4.5.1 Verschiedenheit von Konstruktoren . . . . . . . . . . . . . . . . . . . . 54 4.5.2 Injektivität von Konstruktoren . . . . . . . . . . . . . . . . . . . . . . 55 4.5.3 Strukturelle Induktion . . . . . . . . . . . . . . . . . . . . . . . . . . . 56

4.6 Repräsentationsunabhängige Beweise . . . . . . . . . . . . . . . . . . . . . . . 60 4.6.1 Fallunterscheidung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61 4.6.2 Primitive Rekursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61

4.6.2.1 Induktive Definition der Funktionsgraphen . . . . . . . . . . 61 4.6.2.2 Totalität und Eindeutigkeit . . . . . . . . . . . . . . . . . . . 63 4.6.2.3 Definition der Kombinatoren . . . . . . . . . . . . . . . . . . 65 4.6.2.4 Charakteristische Gleichungen . . . . . . . . . . . . . . . . . 66

4.6.3 Case-Kombinator . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67

5 Erweiterungsmöglichkeiten 68 5.1 Verschachtelt rekursive Datentypen mit Funktionstypen . . . . . . . . . . . . 68 5.2 Ein Universum für Datentypen mit beliebigem Verzweigungsgrad . . . . . . . 70 5.3 Konstruktion eines Datentyps mit unendlichem Verzweigungsgrad . . . . . . . 72

5.3.1 Repräsentierende Menge . . . . . . . . . . . . . . . . . . . . . . . . . . 72 5.3.2 Konstruktoren . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72 5.3.3 Induktionsregel . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73 5.3.4 Primitive Rekursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74

6 Vergleich mit anderen Arbeiten 77 6.1 Andere auf HOL basierende Datentyppakete . . . . . . . . . . . . . . . . . . . 77 6.2 Alternative Formulierung charakteristischer Theoreme . . . . . . . . . . . . . 78 6.3 Alternative Konstruktionsverfahren . . . . . . . . . . . . . . . . . . . . . . . . 82

7 Schlußbemerkungen 85 7.1 Ausblick auf coinduktive Datentypen . . . . . . . . . . . . . . . . . . . . . . . 85 7.2 Weitere Arbeitspunkte . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86 INHALTSVERZEICHNIS iii A Häufig verwendete HOL-Regeln 87 B Beweislaufzeit einiger Datentypen 88 C Bewiesene Theoreme 89 ”The method of ‘postulating’ what we want has many advantages;

they are the same as the advantages of theft over honest toil. Let us leave them to others and proceed with our honest toil.“

Bertrand Russell, Introduction to Mathematical Philosophy

Kapitel 1

Einleitung

1.1 Motivation und Einordnung

Seit einigen Jahren werden Computerprogramme in immer größerem Ausmaß zur Steuerung von Abläufen eingesetzt, die unser alltägliches Leben betreffen. So enthält z.B. schon jedes handelsübliche Mobiltelefon Software im Umfang von mehreren tausend Lines of Code. Da Software zunehmend auch in sicherheitskritischen Bereichen eingesetzt wird, wo Fehlfunktionen oder Ausfälle teilweise immense Kosten verursachen oder gar Menschenleben gefährden können, kommt der Frage der Korrektheit von Software eine wachsende Bedeutung zu. In besonders spektakulärer Weise wurde diese Problematik durch den Absturz der europäischen Trägerrakete Ariane 5 deutlich gemacht, bei dem ein Schaden von über einer Milliarde DM entstand. Auch wenn viele Praktiker behaupten, durch besonders ausführliches Testen alle Programmierfehler aufdecken zu können, kann der Nachweis der tatsächlichen Korrektheit von Software nur durch einen formalen Beweis erbracht werden.

Aufgrund der hohen Komplexität von Software-Systemen ist es jedoch sehr schwer und auch unübersichtlich, einen derartigen Korrektheitsbeweis nur auf dem Papier zu führen. In diesem Zusammenhang sind daher maschinelle Verifikationswerkzeuge von großem Nutzen. Ein solches Werkzeug ist der generische Theorembeweiser Isabelle [Paulson, 1993a]. Hierbei bedeutet generisch, daß Isabelle nicht auf eine einzige, fest einprogrammierte Logik beschränkt ist, sondern vielmehr eine Implementierungsplattform für eine große Klasse verschiedener Logiken darstellt. Eine solche implementierte Logik ist Isabelle/HOL, die wegen ihrer Ausdrucksstärke und ihres einfachen Typsystems eine gute Ausgangsbasis für die Verifikation von Programmen bietet.

Eine wichtiges Instrument zur Formalisierung von Programmen und deren Eigenschaften sind induktive Datentypen, also Typen, für die ein Induktionsprinzip ähnlich dem aus der Mathematik bekannten Prinzip der vollständigen Induktion für natürliche Zahlen gilt.

1.2 Aufgabenstellung

Für Isabelle/HOL existierte bereits ein Paket zur Beschreibung induktiver Datentypen, das die Eigenschaften des Typs wie z.B. Induktionsregeln als Axiome einführte. Diese Vorgehensweise birgt jedoch die Gefahr in sich, daß durch die Einführung fehlerhafter Axiome Inkonsistenzen entstehen können. Sicherer und methodisch angemessener ist es, Datentypen definitorisch durch Angabe einer geeigneten Repräsentation einzuführen, aus der dann die gewünschten Eigenschaften des Datentyps als Theoreme abgeleitet werden können.

Die im Rahmen der Diplomarbeit zu bearbeitende Aufgabenstellung bestand nun im wesentlichen aus zwei Teilen: Zum einen sollte theoretisch untersucht werden, ob und wie bestimmte Klassen von Datentypen in Isabelle/HOL repräsentiert werden können. Außerdem sollte, aufbauend auf den angestellten theoretischen Überlegungen, die Implementierung eines definitorischen Datentyppakets für Isabelle/HOL vorgenommen werden, das auch die in der Praxis häufig vorkommenden Fälle von induktiven Datentypen mit verschränkter und verschachtelter Rekursion behandeln kann.

1.3 Aufbau der Arbeit

Kapitel 2 führt zunächst die notwendigen Grundlagen ein. Dies umfaßt zum einen das verwendete Beweissystem Isabelle sowie die Logik Isabelle/HOL, wobei insbesondere auf das Prinzip der definitorischen Theorieerweiterung eingegangen wird. Außerdem werden einige wichtige theoretische Konzepte wie Fixpunkte und induktive Definitionen behandelt.

Kapitel 3 beschreibt auf relativ abstraktem Niveau die Klassen der verschränkt und verschachtelt rekursiven Datentypen, die mit dem im Rahmen der Diplomarbeit implementierten Paket definiert werden können. Es wird hierbei ein Überblick über die durch die Definition eingeführten Konstanten und Funktionen sowie die bewiesenen charakteristischen Theoreme gegeben.

Kapitel 4 behandelt anschließend die Repräsentation der in Kapitel 3 beschriebenen Datentypen in Isabelle/HOL sowie die zum Einsatz kommenden Beweistechniken, die auch in Form von Isabelle-Beweisprozeduren implementiert wurden.

Kapitel 5 diskutiert eine mögliche Erweiterung des Datentyppakets auf eine eingeschränkte Klasse verschachtelt rekursiver Datentypen mit Funktionstypen. Das beschriebene Konstruktionsverfahren gehört zwar nicht zum Funktionsumfang des implementierten Pakets, jedoch wurde die Konstruktion für einen speziellen Typ exemplarisch in Isabelle/HOL durchgeführt.

Kapitel 6 enthält einen Vergleich mit anderen auf HOL basierenden Datentyppaketen in Hinblick auf die Formulierung der charakteristischen Theoreme und die zum Einsatz kommenden Konstruktionsverfahren.

1.4 Einführendes Beispiel

Als einführendes Beispiel wollen wir die Formalisierung einer einfachen funktionalen Programmiersprache betrachten. Diese Programmiersprache soll dabei sowohl arithmetische Ausdrücke, dargestellt durch den Typ α aexp, als auch boolesche Ausdrücke, dargestellt durch den Typ α bexp enthalten. Wir beschreiben nun die Typen α aexp und α bexp durch folgende Datentypdefinition

datatype α aexp = If then else (α bexp) (α aexp) (α aexp)
| Sum (α aexp) (α aexp)
| Diff (α aexp) (α aexp)
| Var α
| Num nat
and  α bexp = Less (α aexp) (α aexp)
| And (α bexp) (α bexp)
| Or (α bexp) (α bexp)

Durch diese Definition werden die injektiven Funktionen Sum :: α aexp → α aexp → α aexp, And :: α bexp → α bexp → α bexp, etc. eingeführt, die auch als Konstruktoren des Datentyps bezeichnet werden. Alle zulässigen Ausdrücke der Programmiersprache können mit Hilfe dieser Konstruktoren aufgebaut werden. Ein zulässiger Ausdruck ist beispielsweise

If then else (And (Less (Var x) (Num 2)) (Less (Num 1) (Var y)))

(Sum (Sum (Num 1) (Var x)) (Var y))

(Diff (Var y) (Num 2))

wobei x und y ”Variablennamen“ vom Typ α sind. Damit ist die Syntax der Programmiersprache formalisiert. Auf syntaktischer Ebene kann nun eine Substitution von Variablen durch Ausdrücke vom Typ α aexp mit Hilfe der Funktionen

subst aexp :: (α → α aexp) → α aexp → α aexp
subst bexp :: (α → α aexp) → α bexp → α bexp

durchgeführt werden. Diese Substitutionsfunktionen können mittels primitiver Rekursion durch die Gleichungen

subst aexp f (If then else b a_{1} a_{2}) = If then else (subst bexp f b)

(subst aexp f a_{1}) (subst aexp f a_{2})

subst aexp f (Sum a_{1} a_{2})  = Sum (subst aexp f a_{1}) (subst aexp f a_{2})
subst aexp f (Diff a_{1} a_{2})  = Diff (subst aexp f a_{1}) (subst aexp f a_{2})
subst aexp f (Var v)  = f v
subst aexp f (Num n)  = Num n
subst bexp f (Less a_{1} a_{2})  = Less (subst aexp f a_{1}) (subst aexp f a_{2})
subst bexp f (And b_{1} b_{2})  = And (subst bexp f b_{1}) (subst bexp f b_{2})
subst bexp f (Or b_{1} b_{2})  = Or (subst bexp f b_{1}) (subst bexp f b_{2})

spezifiziert werden. Auffallend hierbei ist, daß die Funktionen mittels Fallunterscheidung über die verschiedenen Konstruktoren definiert werden, wobei als Argumente für die rekursiven Aufrufe von subst aexp und subst bexp immer nur die auf der linken Seite der jeweiligen Gleichung angegebenen Argumente des Konstruktors verwendet werden. Dies stellt sicher, daß die rekursiven Argumente mit jedem Aufruf strukturell kleiner werden und die Funktionen daher stets terminieren.

Die Semantik einer solchen Programmiersprache beschreibt man typischerweise durch Auswertungsfunktionen

eval aexp :: (α → nat) → α aexp → nat
eval bexp :: (α → nat) → α bexp → bool

die den Wert eines Ausdrucks bzgl. einer bestimmten Belegung env der Variablen ermitteln. Ebenfalls mittels primitiver Rekursion können diese Auswertungsfunktionen nun durch die Gleichungen

eval aexp env (If then else b a_{1} a_{2}) = if eval bexp env b then eval aexp env a_{1}

else eval aexp env a_{2}

eval aexp env (Sum a_{1} a_{2})  = eval aexp env a_{1} + eval aexp env a_{2}
eval aexp env (Diff a_{1} a_{2})  = eval aexp env a_{1} − eval aexp env a_{2}
eval aexp env (Var v)  = env v
eval aexp env (Num n)  = n
eval bexp env (Less a_{1} a_{2})  = eval aexp env a_{1} < eval aexp env a_{2}
eval bexp env (And b_{1} b_{2})  = eval bexp env b_{1} ∧ eval bexp env b_{2}
eval bexp env (Or b_{1} b_{2})  = eval bexp env b_{1} ∨ eval bexp env b_{2}

charakterisiert werden. Die Grundidee besteht hierbei darin, die Operatoren der Programmiersprache wie z.B. Sum und And auf die entsprechenden HOL-Operatoren + und ∧ abzubilden.

In vielen Lehrbüchern über Semantik findet man in diesem Zusammenhang oft Theoreme, die Substitutions- und Auswertungsfunktionen miteinander in Beziehung setzten. Für die hier betrachtete Programmiersprache läßt sich dieser Zusammenhang durch

eval aexp env (subst aexp (Var(v := a′)) a) = eval aexp (env(v := eval aexp env a′)) a ∧ eval bexp env (subst bexp (Var(v := a′)) b) = eval bexp (env(v := eval aexp env a′)) b

ausdrücken, wobei

f (x := y) z ≡ if x = z then y else f z

Die Funktion subst aexp (Var(v := a′)) ersetzt genau die Variable v in einem Ausdruck durch a′ und läßt die restlichen Variablen unverändert. Das obige Theorem besagt also, daß die Auswertung jeweils das gleiche Ergebnis liefert, wenn man vor der Auswertung alle Vorkommen von v durch a′ ersetzt, oder wenn man die Belegung env an der Stelle v geeignet verändert. Das in dieser Situation üblicherweise zur Anwendung kommende Beweisprinzip wird meist als strukturelle Induktion bezeichnet, da es sich am Aufbau der Ausdrücke orientiert. Für die Datentypen α aexp und α bexp wird dies durch die Regel

∀b, a_{1}, a_{2}. P_{2} b ∧ P_{1} a_{1} ∧ P_{1} a_{2} ⟹ P_{1} (If then else b a_{1} a_{2})
∀a_{1}, a_{2}. P_{1} a_{1} ∧ P_{1} a_{2}  ⟹ P_{1} (Sum a_{1} a_{2})
∀a_{1}, a_{2}. P_{1} a_{1} ∧ P_{1} a_{2}  ⟹ P_{1} (Diff a_{1} a_{2})
∀v.  P_{1} (Var v)
∀n.  P_{1} (Num n)
∀a_{1}, a_{2}. P_{1} a_{1} ∧ P_{1} a_{2}  ⟹ P_{2} (Less a_{1} a_{2})
∀b_{1}, b_{2}. P_{2} b_{1} ∧ P_{2} b_{2}  ⟹ P_{2} (And b_{1} b_{2})
∀b_{1}, b_{2}. P_{2} b_{1} ∧ P_{2} b_{2}  ⟹ P_{2} (Or b_{1} b_{2})
P_{1} a ∧ P_{2} b

ausgedrückt. Da die Datentypen α aexp und α bexp verschränkt rekursiv sind, müssen die Eigenschaften P_{1} und P_{2} simultan bewiesen werden. Für den Konstruktor If then else müßte beim Beweis des obigen Substitutionstheorems gemäß der Induktionsregel die Implikation

∀b, a_{1}, a_{2}.

eval bexp env (subst bexp (Var(v := a′)) b) = eval bexp (env(v := eval aexp env a′)) b ∧ eval aexp env (subst aexp (Var(v := a′)) a_{1}) = eval aexp (env(v := eval aexp env a′)) a_{1} ∧ eval aexp env (subst aexp (Var(v := a′)) a_{2}) = eval aexp (env(v := eval aexp env a′)) a_{2} ⟹

eval aexp env (subst aexp (Var(v := a′)) (If then else b a_{1} a_{2})) = eval aexp (env(v := eval aexp env a′)) (If then else b a_{1} a_{2})

gezeigt werden, d.h. unter der Induktionsvoraussetzung, daß die zu beweisenden Eigenschaften bereits für b, a_{1} und a_{2} gelten, muß die Gültigkeit der Eigenschaft für If then else b a_{1} a_{2} nachgewiesen werden. Wir können dies leicht durch folgende Umformung zeigen:

eval aexp env (subst aexp (Var(v := a′)) (If then else b a_{1} a_{2}))

=  {charakteristische Gleichungen für subst aexp}

eval aexp env (If then else (subst bexp (Var(v := a′)) b) (subst aexp (Var(v := a′)) a_{1}) (subst aexp (Var(v := a′)) a_{2}))

=  {charakteristische Gleichungen für eval aexp}

if (eval bexp env (subst bexp (Var(v := a′)) b)) then (eval aexp env (subst aexp (Var(v := a′)) a_{1})) else (eval aexp env (subst aexp (Var(v := a′)) a_{2}))

=  {Induktionsvoraussetzung}

if (eval bexp (env(v := eval aexp env a′)) b) then (eval aexp (env(v := eval aexp env a′)) a_{1}) else (eval aexp (env(v := eval aexp env a′)) a_{2})

=  {charakteristische Gleichungen für eval aexp}

eval aexp (env(v := eval aexp env a′)) (If then else b a_{1} a_{2})

Grundlagen und Werkzeuge

2.1 Isabelle

Isabelle ist ein generischer Theorembeweiser, der an der Universität Cambridge in Zusammenarbeit mit der Technischen Universität München unter der Leitung von Dr. Lawrence C. Paulson und Prof. Tobias Nipkow entwickelt wurde. Isabelle wurde in der funktionalen Programmiersprache ML implementiert und ist auf einer Vielzahl verschiedener Plattformen verfügbar.

Im Gegensatz zu anderen Beweisern wie PVS oder dem HOL-System von Gordon und Melham [Gordon, Melham, 1993] ist Isabelle nicht auf eine einzige, fest einprogrammierte Logik beschränkt. Charakteristisch für die Architektur von Isabelle ist die Aufteilung in verschiedene Schichten:

• Die Basis von Isabelle bildet die sogenannte Metalogik, Isabelle/Pure. Dies ist im wesentlichen eine intuitionistische Logik höherer Stufe, die auf dem einfach getypten Lambda-Kalkül aufbaut. Als logische Verknüpfungen stehen auf dieser Ebene Allquantifizierung ⋀ x. ϕ, Implikation ϕ ⟹ ψ und Gleichheit a ≡ b zur Verfügung. Mit Hilfe des Lambda-Kalküls kann unter anderem das für viele Logiken wichtige Konzept der Substitution formal präzise ausgedrückt werden. Das Typsystem von Isabelle/Pure unterstützt Polymorphie sowie das aus der Programmiersprache Haskell bekannte Konzept der Typklassen.

• Innerhalb dieser Metalogik von Isabelle können eine Vielzahl von Objektlogiken wie z.B. Higher Order Logic (HOL) oder Zermelo-Fraenkel Mengenlehre (ZF) formalisiert werden.

Objektlogik-Schlußregeln der Form

\begin{aligned}ϕ_{1} & … & ϕ_{n} \\ & ψ \end{aligned}

können mit Hilfe der Meta-Implikation durch

ϕ_{1} ⟹ (… ⟹ (ϕ_{n} ⟹ ψ) …)  bzw. abkürzend  [[ϕ_{1}; …; ϕ_{n}]] ⟹ ψ

ausgedrückt werden.

Die Schlußregeln der Metalogik von Isabelle sind als ML-Funktionen realisiert, die Theoreme auf Theoreme abbilden. So wird z.B. die Elimination der Meta-Implikation

\begin{matrix}ϕ ⟹ ψ & ϕ \\ ψ \end{matrix}

durch die ML-Funktion implies elim des Typs thm → thm → thm realisiert. Bei thm handelt es sich um einen abstrakten Datentyp, der nur von bestimmten Funktionen verarbeitet werden kann. So ist es insbesondere nicht möglich, völlig unkontrolliert beliebige Theoreme zu erzeugen. Die wohl wichtigste Meta-Inferenzregel stellt die sogenannte Resolutionsregel

\begin{matrix}[[ψ_{1}; …; ψ_{m}]] ⟹ ψ & [[ϕ_{1}; …; ϕ_{n}]] ⟹ ϕ \\ ([[ϕ_{1}; …; ϕ_{i−1}; ψ_{1}; …; ψ_{m}; ϕ_{i+1}; …; ϕ_{n}]] ⟹ ϕ)σ \end{matrix}  wobei  ψσ = ϕ_{i}σ

dar: Sind zwei Theoreme [[ψ_{1}; …; ψ_{m}]] ⟹ ψ und [[ϕ_{1}; …; ϕ_{n}]] ⟹ ϕ gegeben und besitzen die Prämisse ϕ_{i} und die Konklusion ψ einen Unifikator σ, so erhält man ein neues Theorem, indem man ϕ_{i} durch die Prämissen ψ_{1}, …, ψ_{m} ersetzt und den Unifikator σ anwendet. Diese Regel ist für die Konstruktion von Beweisen in Isabelle von entscheidender Bedeutung. Schwerpunktmäßig werden von Isabelle sogenannte Rückwärtsbeweise unterstützt. Beweiszustände werden hierbei durch Theoreme der Art

[[ϕ_{1}; …; ϕ_{n}]] ⟹ ϕ

repräsentiert, wobei ϕ das eigentliche Beweisziel ist und ϕ_{1}, …, ϕ_{n} die noch zu beweisenden Teilziele darstellen. Zum Beweis des Theorems ϕ wird ausgehend vom (trivialen) Theorem

ϕ ⟹ ϕ

der Beweiszustand schrittweise mit Hilfe der Resolutionsregel immer weiter verfeinert, bis der Beweiszustand keine Prämissen mehr hat. Zur Durchführung dieser Beweisschritte dienen sogenannte Taktiken. Hierbei handelt es sich um Funktionen, die aus einem Beweiszustand eine Menge möglicher neuer Beweiszustände erzeugen. So wird z.B. die obige Resolutionsregel durch resolve tac rules i realisiert, wobei versucht wird, die Konklusion einer der Regeln aus rules mit dem Teilziel ϕ_{i} zu unifizieren. Des weiteren ist es möglich, mittels sogenannter Tacticals aus einzelnen Taktiken neue Taktiken zu konstruieren. So liefert z.B. die Taktik ALLGOALS tactic neue Beweiszustände, die sich nach Anwendung von tactic auf alle Teilziele des aktuellen Beweiszustandes ergeben.

Eine detaillierte Beschreibung aller Isabelle zugrundeliegender Konzepte, der bereitgestellten Funktionen und deren Verwendung, sowie einiger implementierter Objektlogiken ist in [Paulson, 1993a], [Paulson, 1993b] und [Paulson, 1993c] zu finden. Für eine genauere theoretische Betrachtung der Metalogik von Isabelle sowie der maßgeblichen Design-Prinzipien sei auf [Paulson, 1989] verwiesen.

2.2 Isabelle/HOL

Eine der in Isabelle implementierten Objektlogiken ist Isabelle/HOL. HOL steht für Higher Order Logic und geht auf Alonzo Churchs Simple Theory of Types [Church, 1940] zurück.

Im Gegensatz zur herkömmlichen Prädikatenlogik erster Stufe, in der sich bekanntlich viele wichtige mathematische Begriffe wie z.B. Endlichkeit nicht charakterisieren lassen, ist HOL relativ ausdrucksstark, was diese Logik insbesondere auch für praktische Anwendungen wie beispielsweise Software- und Hardwareverifikation interessant macht. Die Implementierung von HOL in Isabelle erfolgte in Anlehnung an das HOL-Sytem von Gordon und Melham [Gordon, Melham, 1993]. Im folgenden wollen wir einige Aspekte von HOL genauer beleuchten, die im weiteren Verlauf der Arbeit von Bedeutung sein werden.

2.2.1 Typen

Typen spielen in vielen Bereichen der Informatik eine wichtige Rolle. So dienen sie in Programmiersprachen wie z.B. Java oder ML dazu, festzulegen, welche Arten von Operationen auf bestimmten Elementen zugelassen sind, weshalb viele Fehler bereits zur Übersetzungszeit erkannt werden können. So sollten z.B. Ausdrücke wie sqrt("Hello world" + 5) von Compilern abgewiesen werden. Auch in der Logik sind Typen zur Vermeidung von Inkonsistenzen von Bedeutung. Die Notwendigkeit von Typen wurde hierbei erstmals von Bertrand Russell erkannt, auf den das folgende Paradoxon zurückgeht: Gegeben sei die Menge

M = {x | x ∉ x}

d.h. die Menge aller Mengen, die sich selbst nicht enthalten. Nimmt man nun an, daß M ∈ M gilt, so folgt aufgrund der Definition von M , daß M ∉ M gelten muß. Nimmt man M ∉ M an, so folgt M ∈ M .

Isabelle/HOL übernimmt das Typsystem der Metalogik Isabelle/Pure. Es werden folgende Arten von Typen unterschieden:

Typvariablen α bzw. α :: S Hierbei bezeichnet S eine Sorte der Gestalt {C_{1}, …, C_{n}}, wobei C_{i} eine Typklasse darstellt.

Zusammengesetzte Typen (τ_{1}, …, τ_{n})t Hierbei ist t ein sogenannter Typkonstruktor. Insbesondere ist auch der Fall n = 0 eingeschlossen.

Funktionstypen τ → τ′

Typen, in denen Typvariablen vorkommen, werden auch als polymorph bezeichnet. Sorten bzw. Typklassen dienen dazu, den Grad der Polymorphie genauer zu dosieren. Hierbei steht α :: {C_{1}, …, C_{n}} für einen beliebigen Typ, der den Typklassen C_{1}, …, C_{n} angehört. Typklassen können dabei als eine Ansammlung von Typen mit bestimmten Eigenschaften verstanden werden. So steht z.B. α :: {ord} für einen beliebigen Typ, auf dem ≤ eine Ordnung darstellt.

In Isabelle/HOL werden zahlreiche Typkonstruktoren definiert, unter anderem die nullstelligen Typkonstruktoren bool und nat, die einstelligen Typkonstruktoren set und list, sowie die zweistelligen Typkonstruktoren + (disjunkte Summe) und × (kartesisches Produkt). Typkonstruktoren besitzen sogenannte Aritäten, die die Typklassen-Zugehörigkeit eines Typs (τ_{1}, …, τ_{n})t in Abhängigkeit von der Typklassen-Zugehörigkeit der Typargumente τ_{1}, …, τ_{n} ausdrücken. So kann durch die Arität × :: (ord, ord)ord ausgedrückt werden, daß ≤ auf dem Typ τ × τ′ eine (z.B. lexikographische) Ordnung darstellt, falls ≤ auf τ und τ′ eine Ordnung darstellt.

Auf semantischer Ebene stellt die Interpretation [[τ]] eines Typs τ eine Menge aus dem sogenannten Universum U dar. Bei U handelt es sich um eine Menge von Mengen, die bestimmte theoretisch interessante Eigenschaften wie Abgeschlossenheit unter Bildung von Teilmengen und Funktionenräumen besitzt. Die Interpretation eines nullstelligen Typkonstruktors ist eine Menge aus U, während die Interpretation eines mehrstelligen Typkonstruktors t eine Funktion U ×…×U → U ist. Bei polymorphen Typen ist die Interpretation zusätzlich von der Belegung der Typvariablen abhängig. Für die Korrektheit der im folgenden Abschnitt beschriebenen Inferenzregeln von HOL ist von entscheidender Bedeutung, daß die durch [[τ]] bezeichnete Menge stets nichtleer ist. Eine genauere formale Betrachtung der Semantik von Typen und Termen in HOL ist in [Gordon, Melham, 1993] zu finden.

Die folgende Abbildung zeigt einige in Isabelle/HOL definierte Konstanten und deren Typ.

0 :: nat
Suc :: nat → nat
length :: α list → nat
hd :: α list → α
tl :: α list → α list
≤ :: α → α → bool
∈ :: α → α set → bool

Abbildung 2.1: Konstanten aus Isabelle/HOL

Betrachtet man das anfangs erwähnte Paradoxon, so kann festgestellt werden, daß x ∈ x (und damit auch x ∉ x, was ¬(x ∈ x) entspricht) nicht wohlgetypt ist, da x sonst sowohl vom Typ α als auch vom Typ α set sein müßte. Das Problem liegt – präziser ausgedrückt – darin, daß die Typen α und α set aufgrund des Vorkommens von α in α set nicht unifizierbar sind, was oft mit dem Schlagwort occurs check ausgedrückt wird.

2.2.2 Logische Verknüpfungen und Inferenzregeln

In der Logik Isabelle/HOL stehen alle grundlegenden logischen Operatoren wie

¬ :: bool → bool
∧ :: bool → bool → bool
∨ :: bool → bool → bool
⟶ :: bool → bool → bool

∀ :: (α → bool) → bool
∃ :: (α → bool) → bool
∃_{1} :: (α → bool) → bool

zur Verfügung. Hierbei bezeichnet bool den Typ der Wahrheitswerte in HOL. Beweise in HOL werden mit Hilfe des Kalküls des natürlichen Schließens geführt, das auf Gerhard Gentzen zurückgeht. Für jeden der oben angegebenen logischen Operatoren existieren hierbei Einführungs- und Eliminationsregeln. Wie bereits in Abschnitt 2.1 erwähnt, werden Inferenzregeln von Objektlogiken mit Hilfe der Metalogik von Isabelle formuliert. Eine Inferenzregel wie

\begin{matrix}P & Q \\ P ∧ Q \end{matrix}

wird in Isabelle beispielsweise durch

[[P; Q]] ⟹ P ∧ Q (conjI)

ausgedrückt. Die Regel zur Einführung der Implikation lautet

(P ⟹ Q) ⟹ P ⟶ Q (impI)

Die Objekt-Implikation ⟶ wird hierbei auf die Meta-Implikation ⟹ zurückgeführt, die zur Darstellung der lokalen Annahmen eines Beweisziels dient. Die Regel

(⋀ x. P x ) ⟹ ∀x. P x (allI)

für die Einführung des Allquantors führt den Objekt-Allquantor ∀ auf den Meta-Allquantor ⋀ zurück. Spezielle Meta-Inferenzregeln für ⟹ und ⋀ wie Lifting über Annahmen und Lifting über Parameter, die in [Paulson, 1989, Paulson, 1993a] genauer beschrieben werden, stellen sicher, daß die lokalen Annahmen eines Beweisziels in alle daraus entstehenden Teilziele übernommen und Nebenbedingungen von Quantorenregeln wie ”x nicht frei in …“ eingehalten werden.

Für die Korrektheit der Quantorenregeln

∀x. P x ⟹ P (y :: τ)  (spec)
P (y :: τ) ⟹ ∃x. P x  (exI)

ist bedeutsam, daß die Interpretation [[τ]] des Typs τ stets eine nichtleere Menge ist. So wäre z.B. die mittels (spec) und (exI) ableitbare Formel ∀x. P(x) ⟹ ∃x. P(x) falsch, falls x einen leeren Typ besitzen würde. Erläuterungen zu dieser Problematik finden sich in [Paulson, 1990].

Bemerkung 2.1 Zur Vereinfachung der Notation werden wir bei der Darstellung von Beweisen in den folgenden Kapiteln nicht mehr zwischen Meta- und Objekt-Implikation bzw. Meta- und Objekt-Allquantor unterscheiden. Wir verwenden ∀ für Allquantifikation und ⟹ für Implikation, um Verwechslungen mit Funktionstypen zu vermeiden. Um die Darstellung der Beweise kompakt zu halten, werden außerdem elementare Beweisschritte wie z.B. Implikations- und Allquantor-Einführung meist weggelassen.

In der Form

[P x_{1} … x_{n}]_{x_{1},...,x_{n}} ; ⋮ .

Q x_{1} … x_{n} …

R

notierte Inferenzregeln sind gleichbedeutend mit

((∀x_{1}, …, x_{n}. P x_{1} … x_{n} ⟹ Q x_{1} … x_{n}) ∧ …) ⟹ R

Hilberts ε - Operator Eine Besonderheit von HOL ist der sogenannte Hilbertsche Auswahloperator

ε :: (α → bool) → α

Für ein Prädikat P auf dem Typ α liefert εx. P x ein nicht genauer festgelegtes Element vom Typ α mit der Eigenschaft P, falls ein solches existiert. Hierbei ist zu beachten, daß εx. P x immer ein Ergebnis liefert – auch dann, wenn kein Element mit der Eigenschaft P existiert. Dieses Verhalten von ε kann durch die Gleichung

P (εx. P x) = ∃x. P x (select eq Ex)

beschrieben werden. Falls genau ein Element mit der Eigenschaft P existiert, kann die Regel

∃_{1}x. P x P a
(εx. P x) = a

(select1 equality)

verwendet werden, wobei

∃_{1}x. P x ≡ ∃x. P x ∧ (∀y.P y ⟹ y = x)

Die Konstante arbitrary In manchen Fällen kann es hilfreich sein, ein universell verwendbares, nicht näher spezifiziertes ”don’t care“ - Element zur Verfügung zu haben. Hierzu dient die polymorphe Konstante arbitrary :: α.

2.2.3 Definitorische Theorieerweiterung

Das Ergebnis der Formalisierung eines Sachverhalts in Isabelle/HOL sind sogenannte Theorien. Eine Theorie besteht aus einer Menge von Typkonstruktoren und Konstanten, oft auch Signatur genannt, sowie aus einer Menge von Axiomen. Bei der Entwicklung neuer Theorien geht man in der Regel von bestehenden Theorien aus, die man um zusätzliche Typkonstruktoren, Konstanten und Axiome erweitert. Eine wichtige Grundphilosophie von HOL ist es, hierbei nicht das Hinzufügen beliebiger Axiome zu erlauben, sondern nur sogenannte definitorische Erweiterungsmechanismen zuzulassen. Die Verwendung derartiger Erweiterungsmechanismen garantiert, daß bei der Erweiterung die Existenz von Modellen erhalten bleibt, d.h. die entstehende Theorie ein Modell besitzt, falls die ursprüngliche Theorie ein Modell hatte. Unter einem Modell M versteht man hierbei eine Interpretation von Typkonstruktoren und Konstanten, so daß die Interpretation jedes Axioms der Theorie bzgl. M für jede Belegung der freien Variablen stets ”wahr“ ist. Für eine formale Definition des Modellbegriffs sei wieder auf [Gordon, Melham, 1993] verwiesen.

Die Existenz eines Modells impliziert die sogenannte syntaktische Konsistenz einer Theorie. Eine Theorie heißt hierbei syntaktisch konsistent, wenn in ihr nicht jede Formel – insbesondere nicht False – ableitbar ist. Man beachte, daß die syntaktische Konsistenz einer Theorie jedoch nicht unbedingt die Existenz eines Modells impliziert.

Im wesentlichen werden von HOL folgende Arten der definitorischen Theorieerweiterung unterstützt:

Konstantendefinition Die Konstante c kann zur Signatur hinzugefügt und ein Axiom der Gestalt c v_{1} … v_{n} ≡ t eingeführt werden, falls TVars(t) ⊆ TVars(c) sowie Vars(t) ⊆ {v_{1}, …, v_{n}} gilt, c neu ist und nicht in t vorkommt.

Typdefinition Sei t rep set ein Term vom Typ τ set, der eine nichtleere Menge beschreibt, d.h. es gilt u ∈ t rep set für geeignetes u. Weiterhin sei TVars(t rep set) ⊆ {α_{1}, …, α_{n}}. Dann kann der Typ (α_{1}, …, α_{n})t und die Konstanten

Abs t :: τ → (α_{1}, …, α_{n})t
Rep t :: (α_{1}, …, α_{n})t → τ

zur Signatur hinzugefügt sowie die Axiome

Abs t(Rep t(x)) = x  (Rep t inverse)
y ∈ t rep set ⟹ Rep t(Abs t(y)) = y  (Abs t inverse)
Rep t(x) ∈ t rep set  (Rep t)

eingeführt werden.

Die Grundidee der Typdefinition besteht hierbei darin, neue Typen durch Teilmengen bereits existierender Typen zu repräsentieren. Die Axiome (Rep t inverse), (Abs t inverse) und (Rep t) drücken hierbei die Existenz einer Bijektion zwischen der Menge τ rep set und den Elementen des neuen Typs (α_{1}, …, α_{n})t aus, was oft auch als Isomorphie bezeichnet wird. Dieser Sachverhalt ist in Abbildung 2.2 graphisch dargestellt. Die Beweisbarkeit von u ∈ t rep set ist notwendig, da Typen in HOL, wie bereits in Abschnitt 2.2.1 erwähnt, nur durch nichtleere Mengen repräsentiert werden dürfen.

[figure: Abs t; Rep t; τ; t rep set; (α_{1}, …, α_{n})t]

Abbildung 2.2: Definition eines neuen Typs

Da Rep t die Umkehrfunktion Abs t und Abs t auf der Menge t rep set die Umkehrfunktion Rep t besitzt, folgt sofort die Injektivität von Rep t sowie die Injektivität von Abs t auf der Menge t rep set, d.h.

Rep t(x_{1}) = Rep t(x_{2}) ⟹ x_{1} = x_{2}
y_{1} ∈ t rep set ∧ y_{2} ∈ t rep set ∧ Abs t(y_{1}) = Abs t(y_{2}) ⟹ y_{1} = y_{2}

Die repräsentierende Menge muß hierbei so geschickt gewählt werden, daß sich die für den neuen Typ gewünschten Eigenschaften mit Hilfe der Isomorphie aus den entsprechenden Eigenschaften der repräsentierenden Menge herleiten lassen. Elementare Funktionen auf dem neuen Typ werden hierbei mittels Abs t und Rep t ausgedrückt. Sind die charakteristischen Eigenschaften einmal bewiesen, kann von der konkreten Repräsentation des Typs völlig abstrahiert werden. Im Gegensatz zur axiomatischen Vorgehensweise, die immer die Gefahr von Inkonsistenzen in sich birgt, können mit diesem Verfahren abstrakte Datentypen sicher eingeführt werden.

Ein formaler Beweis der Tatsache, daß die Existenz von Modellen bei Verwendung der obigen Definitionsmechanismen tatsächlich erhalten bleibt, ist wiederum in [Gordon, Melham, 1993] zu finden.

Mit Hilfe des beschriebenen Verfahrens kann so beispielsweise der Typ der disjunkten Summe α + β beschrieben werden. Als repräsentierende Menge wird hierbei

sum :: (α → β → bool → bool)set
sum ≡ {f | (∃a. f = λ x, y, p. x = a ∧ p) ∨ (∃b. f = λ x, y, p. y = b ∧ ¬p)}

verwendet. Die beiden Injektionen Inl :: α → α + β und Inr :: β → α + β sind definiert durch

Inl a ≡ Abs sum(λ x, y, p. x = a ∧ p)
Inr b ≡ Abs sum(λ x, y, p. y = b ∧ ¬p)

An diesem Beispiel wird deutlich, daß selbst die Konstruktion einfacher Typen relativ umständlich und mitunter auch undurchsichtig sein kann. Es ist daher erforderlich, für bestimmte Klassen häufig vorkommender Typen Verfahren für deren systematische Konstruktion zu entwickeln.

2.3 Theoretische Grundlagen

Der folgende Abschnitt behandelt einige theoretische Grundlagen wie Fixpunkte und induktive Definitionen, die für die Konstruktion von Datentypen wichtig sind. Die beschriebenen abstrakten Konzepte sind in Isabelle/HOL in Form von Theorien bzw. generischen Beweisprozeduren implementiert. Die folgenden Beweise werden daher in Anlehnung an Isabelle/HOL oft in einem rückwärtsgerichteten Stil und unter Verwendung von für HOL typischer Notation präsentiert, wobei von konkreten Implementierungsdetails jedoch weitgehend abstrahiert wird.

2.3.1 Fixpunkte

Im folgenden wollen wir kurz auf einige wichtige Ergebnisse aus der Fixpunkttheorie eingehen, die für die präzise mathematische Beschreibung von Datentypen und rekursiven Funktionen sowie induktiven Definitionen von zentraler Bedeutung sind.

Definition 2.2 (Untere Schranke) Sei ⊑ ⊆ S × S eine Ordnungsrelation auf S und T ⊆ S. Dann heißt b ∈ S untere Schranke von T , falls b ⊑ x für alle x ∈ T gilt.

g heißt größte untere Schranke (Infimum) von T , falls b ⊑ g für alle unteren Schranken b von T gilt. Falls eine solche stets eindeutige größte untere Schranke von T existiert, wird diese auch mit ⊓T bezeichnet. □

Definition 2.3 (Vollständiger Verband) Eine Menge S zusammen mit einer Ordnungsrelation ⊑ ⊆ S × S heißt vollständiger Verband (S, ⊑), falls jede Menge T ⊆ S eine größte untere Schranke bzgl. ⊑ besitzt. □

Definition 2.4 (Monotonie von Funktionen) Eine Funktion F : S → S heißt monoton, falls für alle x, y gilt:

x ⊑ y ⟹ F (x) ⊑ F (y)
□

Theorem 2.5 (Knaster-Tarski) Sei (S, ⊑) ein vollständiger Verband und F : S → S eine monotone Funktion. Dann existiert ein durch

lfp(F ) = {x | F (x) ⊑ x}

eindeutig bestimmter kleinster Fixpunkt von F , d.h. es gilt

F (lfp(F )) = lfp(F )  und  F (x) ⊑ x ⟹ lfp(F ) ⊑ x

Beweis Bezeichne

P = {x | F (x) ⊑ x}

die Menge der sogenannten Präfixpunkte von F .

Für jedes x ∈ P gilt lfp(F ) ⊑ x, da lfp(F ) eine untere Schranke der Menge P ist. Aufgrund der Monotonie von F gilt daher auch F (lfp(F )) ⊑ F (x). Wegen F (x) ⊑ x folgt hieraus F (lfp(F )) ⊑ x, d.h. F (lfp(F )) ist ebenfalls eine untere Schranke von P. Da lfp(F ) die größte untere Schranke von P ist, gilt daher F (lfp(F )) ⊑ lfp(F ), d.h. lfp(F ) ist ein Präfixpunkt von F . Aufgrund seiner Definition ist lfp(F ) offensichtlich auch der kleinste Präfixpunkt von F .

Aus F (lfp(F )) ⊑ lfp(F ) folgt F (F (lfp(F ))) ⊑ F (lfp(F )) aufgrund der Monotonie von F . Es gilt also auch F (lfp(F )) ∈ P und damit lfp(F ) ⊑ F (lfp(F )).

Damit gilt F (lfp(F )) = lfp(F ). □

In den folgenden Abschnitten werden hauptsächlich vollständige Verbände der Form (P(S), ⊆) von Bedeutung sein. Hierbei bezeichnet P(S) = {x | x ⊆ S} die Potenzmenge von S, weshalb (P(S), ⊆) auch Potenzmengenverband genannt wird. Die größte untere Schranke einer Menge T ⊆ P(S) ist hierbei durch ⋂ T bestimmt.

Eine Menge M ⊆ S mit der Eigenschaft F (M ) ⊆ M wird auch als unter F abgeschlossen bezeichnet. lfp(F ) stellt also die kleinste unter F abgeschlossene Menge dar.

Die Begriffe kleinste obere Schranke und größter Fixpunkt werden dual dazu definiert. So gilt

gfp(F ) = ⨆{x | x ⊑ F (x)}

Man beachte, daß in einem vollständigen Verband jede beliebige Menge auch eine eindeutige kleinste obere Schranke besitzt, nämlich

⨆ T = {x | ∀y ∈ T . y ⊑ x}

In vielen Arbeiten über Datentypen wie z.B. [Hensel, Jacobs, 1997], die nicht Mengenlehre, sondern Kategorientheorie als Grundlage verwenden, findet man oft die Begriffe initiale Algebren bzw. terminale Coalgebren. Diese stellen das kategorientheoretische Analogon zum Konzept des kleinsten bzw. größten Fixpunkts dar.

2.3.2 Induktive Definitionen

Unter einer induktiv definierten Menge versteht man die kleinste Menge, die unter bestimmten Regeln abgeschlossen ist. So kann z.B. die Menge even der positiven geraden Zahlen durch folgende zwei Regeln charakterisiert werden:

0 ∈ even  n ∈ even ; n + 2 ∈ even

Derartige Regeln bezeichnet man auch als Einführungsregeln. Die erste Regel besagt, daß 0 eine gerade Zahl ist. Die zweite Regel besagt, daß n + 2 ebenfalls eine gerade Zahl ist, falls n eine gerade Zahl ist. Man beachte, daß die Menge der positiven geraden Zahlen nicht die einzige unter diesen Regeln abgeschlossene Menge ist. So ist z.B. auch die Menge IN der natürlichen Zahlen und die Menge IR der reellen Zahlen unter diesen Regeln abgeschlossen, denn 0 ist auch eine reelle Zahl und n + 2 ist auch eine reelle Zahl, falls n eine reelle Zahl ist. Jedoch stellt die Menge der positiven geraden Zahlen die kleinste unter diesen Regeln abgeschlossene Menge dar.

Wie in Abschnitt 2.3.1 angedeutet, ist die kleinste unter einer monotonen Funktion F abgeschlossene Menge genau der kleinste Fixpunkt von F . Die Menge der positiven geraden Zahlen läßt sich daher wie folgt als Fixpunkt einer geeigneten Funktion F , die sich direkt aus den Einführungsregeln ergibt, definieren:

F (M ) = {x | x = 0 ∨ ∃n. x = n + 2 ∧ n ∈ M }
even = lfp(F )
= ⋂{x | F (x) ⊆ x}

Aus dieser Definition lassen sich nun mit Hilfe der Fixpunkteigenschaft die obigen Einführungsregeln ableiten, denn es gilt offensichtlich

0 ∈ {x | x = 0 ∨ ∃n. x = n + 2 ∧ n ∈ lfp(F )} = F (lfp(F )) = lfp(F ) = even KAPITEL 2. GRUNDLAGEN UND WERKZEUGE 16

Ist n ∈ even = lfp(F ) so gilt

n + 2 ∈ {x | x = 0 ∨ ∃n. x = n + 2 ∧ n ∈ lfp(F )} = even Aus der Tatsache, daß lfp(F ) die kleinste unter F abgeschlossene Menge ist, läßt sich unmittelbar die Induktionsregel

mono(F ) F ({x | P(x)}) ⊆ {x | P(x)}
lfp(F ) ⊆ {x | P(x)}

(weakInd)

ableiten. Diese Regel läßt sich noch zu

mono(F ) F (lfp(F ) ∩ {x | P(x)}) ⊆ {x | P(x)}
lfp(F ) ⊆ {x | P(x)}

(strongInd)

verstärken. Beweis Sei F monoton und es gelte F (lfp(F ) ∩ {x | P(x)}) ⊆ {x | P(x)}. Offensichtlich ist

lfp(F ) ∩ {x | P(x)} ⊆ lfp(F ) woraus aufgrund der Monotonie von F sowie der Fixpunkteigenschaft

F (lfp(F ) ∩ {x | P(x)}) ⊆ F (lfp(F )) = lfp(F ) folgt. Damit gilt

F (lfp(F ) ∩ {x | P(x)}) ⊆ lfp(F ) ∩ {x | P(x)} Mit Hilfe von (weakInd) folgt hieraus

lfp(F ) ⊆ lfp(F ) ∩ {x | P(x)} ⊆ {x | P(x)}

□

Aus dieser abstrakten Induktionsregel kann nun für jede induktiv definierte Menge eine spezielle Induktionsregel abgeleitet werden. So erhält man z.B. für die Menge even die Induktionsregel

x ∈ even P(0) ∀n. P(n) ∧ n ∈ even ⟹ P(n + 2)

P(x)

Beweis Im folgenden sei wieder

F (M ) = {x | x = 0 ∨ ∃n. x = n + 2 ∧ n ∈ M }
even = lfp(F )

und es gelte P(0), ∀n. P(n) ∧ n ∈ even ⟹ P(n + 2) sowie x ∈ even. Wir zeigen nun

\underbrace{\{x | x = 0 ∨ ∃n. x = n + 2 ∧ n ∈ even ∩ \{x | P(x)\}\}}_{F(even∩\{x|P(x)\})} ⊆ \{x | P(x)\}

Sei z ∈ {x | x = 0 ∨ ∃n. x = n + 2 ∧ n ∈ even ∩ {x | P(x)}}. Es sind nun zwei Fälle zu unterscheiden:

1. z = 0 Gemäß Voraussetzung gilt P(0) und damit z ∈ {x | P(x)}.

2. z = n + 2 ∧ n ∈ even ∩ {x | P(x)} Es gilt P(n)∧n ∈ even, woraus nach Voraussetzung P(n +2) und damit z ∈ {x | P(x)} folgt.

Mittels (strongInd) folgt also even ⊆ {x | P(x)}. Nach Voraussetzung ist x ∈ even, weshalb P(x) gilt.

□

Aus der Tatsache, daß even ein Fixpunkt ist, läßt sich außerdem noch die folgende Eliminationsregel

x ∈ even x = 0 ⟹ P ∀n. x = n + 2 ∧ n ∈ even ⟹ P

P

ableiten, die eine Fallunterscheidung über alle Entstehungsmöglichkeiten von Elementen aus even darstellt.

Beweis Angenommen, es gelte x ∈ even, x = 0 ⟹ P und ∀n. x = n + 2 ∧ n ∈ even ⟹ P. Aus x ∈ even erhält man aufgrund der Fixpunkteigenschaft von even

x ∈ {x | x = 0 ∨ ∃n. x = n + 2 ∧ n ∈ even}

Analog zum Beweis der Induktionsregel sind die zwei Fälle

1. x = 0 und

2. x = n + 2 ∧ n ∈ even

zu unterscheiden, aus denen gemäß Voraussetzung sofort P folgt. □

Die soeben am Beispiel der Menge even erarbeiteten Konzepte sollen nun im folgenden verallgemeinert werden. Hierbei wird insbesondere auch die simultane induktive Definition mehrerer Mengen erlaubt.

Definition 2.6 (Injektionen, Fallunterscheidung) Seien die Typen τ_{1}, …, τ_{n} gegeben. Dann bezeichne

in_{i} :: τ_{i} → τ_{1} + ⋯ + τ_{n}

eine Funktion mit den Eigenschaften

i ≠ j ⟹ in_{i}(x) ≠ in_{j} (y) x ≠ y ⟹ in_{i}(x) ≠ in_{i}(y)

Weiterhin sei

sum case :: (τ_{1} → τ) → ⋯ → (τ_{n} → τ) → τ_{1} + ⋯ + τ_{n} → τ

eine Funktion mit der Eigenschaft

sum case f_{1} … f_{n} (in_{i}(x)) = f_{i}(x)

zur Formulierung von Fallunterscheidungen auf dem Typ τ_{1} + ⋯ + τ_{n}. □

Definition 2.7 (Inverses Bild) Das inverse Bild vimage f S der Menge S bzgl. einer Funktion f sei definiert durch

vimage f S = {x | f (x) ∈ S}

□

Definition 2.8 (Induktiv definierte Mengen) Seien S_{1}, …, S_{n} Bezeichner für Mengen über den Typen τ_{1}, …, τ_{n}. Ferner sei R eine Menge von Einführungsregeln der Gestalt

… Q_{j} … t_{k} ∈ F_{l}(S_{i′}) …
t ∈ S_{i}

wobei Q_{j} eine beliebige logische Formel ist, die keine der Bezeichner S_{i} enthält. t und t_{k} seien beliebige Terme und F_{l} eine monotone Funktion.

Dann sind die Mengen S_{1}, …, S_{n} durch R induktiv definiert, falls gilt

F (U ) = {x | … ∨

∃v_{1}, …, v_{m}. x = in_{i}(t) ∧ … ∧ Q_{j} ∧ … ∧ t_{k} ∈ F_{l}(vimage in_{i′} U ) ∧ … ∨

…}
T = lfp(F )
S_{1} = vimage in_{1} T
⋮
S_{n} = vimage in_{n} T
□

Hierbei entspricht jedes Glied der Disjunktion innerhalb von {x | …} einer Einführungsregel. Die v_{1}, …, v_{m} sind die in der entsprechenden Einführungsregel frei vorkommenden Variablen. Die Menge T enthält sämtliche Elemente aller Mengen S_{1}, …, S_{n}, ”verpackt“ in die entsprechenden Injektionen in_{1}, …, in_{n}. Die den einzelnen Mengen zugehörigen Elemente werden dann mittels vimage in_{1} T , …, vimage in_{n} T wieder aus T ”ausgepackt“. Um die Monotonie von F sicherzustellen, müssen Einführungsregeln stets die oben beschriebene Gestalt besitzen.

Theorem 2.9 (Charakteristische Eigenschaften induktiver Mengen) Für induktiv definierte Mengen S_{1}, …, S_{n} lassen sich folgenden Regeln ableiten:

• Einführungsregeln der Form

… Q_{j} … t_{k} ∈ F_{l}(S_{i′}) …
t ∈ S_{i}

• Eliminationsregeln für jede der Mengen S_{1}, …, S_{n} der Form

x ∈ S_{i} …

[x = t … Q_{i} … t_{k} ∈ F_{l}(S_{i′}) …]_{v_{1},...,v_{m}}

⋮ .

P …

P

• Eine Induktionsregel für alle Mengen S_{1}, …, S_{n} der Form

…

[… Q_{i} … t_{k} ∈ F_{l}(S_{i′} ∩ {x | P_{i′}(x)}) …]_{v_{1},...,v_{m}}

⋮ .

P_{i}(t) …

x_{1} ∈ S_{1} ⟹ P_{1}(x_{1}) ∧ … ∧ x_{n} ∈ S_{n} ⟹ P_{n}(x_{n})

bzw.

…

[… Q_{i} … t_{k} ∈ S_{i′} P_{i′}(t_{k}) …]_{v_{1},...,v_{m}}

⋮ .

P_{i}(t) …

x_{1} ∈ S_{1} ⟹ P_{1}(x_{1}) ∧ … ∧ x_{n} ∈ S_{n} ⟹ P_{n}(x_{n})

falls F_{l} = Id

Beweis

Monotonie Unter der Voraussetzung S ⊆ T zeigen wir

∀x. x ∈ F (S) ⟹ x ∈ F (T )

Für alle beteiligten Operatoren werden hierbei Monotonieregeln wie z.B.

P ⟹ Q P′ ⟹ Q′
P ∧ P′ ⟹ Q ∧ Q′

P ⟹ Q P′ ⟹ Q′

P ∨ P′ ⟹ Q ∨ Q′

∀x. P(x) ⟹ Q(x)
(∃x. P(x)) ⟹ (∃x. Q(x))

S ⊆ T

x ∈ vimage f S ⟹ x ∈ vimage f T

verwendet, durch deren sukzessive Anwendung das obige Beweisziel auf die Beweisziele S ⊆ S, T ⊆ T und S ⊆ T reduziert werden kann.

Einführungsregeln Unter den Voraussetzungen Q_{j} , t_{k} ∈ F_{l}(S_{i′}), … muß t ∈ S_{i} gezeigt werden. Es gilt

t ∈ S_{i}

⟺ {Definition von S_{i}}

t ∈ vimage in_{i} T

⟺ {Definition von vimage}

in_{i}(t) ∈ T

⟺ {Fixpunkteigenschaft von T , Monotonie von F }

in_{i}(t) ∈ {x | ∃ …. x = in_{1}(…) ∧ … ∨

… ∨
∃v_{1}, …, v_{m}. x = in_{i}(t) ∧ … ∧ Q_{j} ∧ … ∧ t_{k} ∈ F_{l}(vimage in_{i′} T ) ∧ … ∨
… ∨
∃ …. x = in_{n}(…) ∧ …}

Man erhält somit das neue Beweisziel

∃ …. in_{i}(t) = in_{1}(…) ∧ … ∨
… ∨
∃v_{1}, …, v_{m}. in_{i}(t) = in_{i}(t) ∧ … ∧ Q_{j} ∧ … ∧ t_{k} ∈ F_{l}(vimage in_{i′} T ) ∧ … ∨
… ∨
∃ …. in_{i}(t) = in_{n}(…) ∧ …

Durch Auswahl des geeigneten Zweigs der Disjunktion erhält man hieraus das Beweisziel

∃v_{1}, …, v_{m}. in_{i}(t) = in_{i}(t) ∧ … ∧ Q_{j} ∧ … ∧ t_{k} ∈ F_{l}(vimage in_{i′} T ) ∧ …

was sich mit Hilfe von Reflexivität und der Voraussetzungen lösen läßt.

Eliminationsregeln Unter den Voraussetzungen

x ∈ S_{i}
∀v_{1}, …, v_{m}. x = t ∧ Q_{i} ∧ t_{k} ∈ F_{l}(S_{i′}) ∧ … ⟹ P
⋮

muß nun P gezeigt werden. Die Vorgehensweise ist ähnlich wie beim Beweis der Einführungsregeln. Aus der Voraussetzung x ∈ S_{i} erhält man nach Definition x ∈ vimage in_{i} T , was gleichbedeutend ist mit in_{i}(x) ∈ T . Unter Ausnutzung der Fixpunkteigenschaft von T ergibt sich hieraus

in_{i}(x) ∈ {x | ∃ …. x = in_{1}(…) ∧ … ∨
… ∨
∃v_{1}, …, v_{m}. x = in_{i}(t) ∧ … ∧ Q_{j} ∧ … ∧ t_{k} ∈ F_{l}(vimage in_{i′} T ) ∧ … ∨
… ∨
∃ …. x = in_{n}(…) ∧ …}

Nach Aufspaltung der Disjunktion und Berücksichtigung von vimage in_{i′} T = S_{i′} erhält man somit die Beweisziele

∀ …. in_{i}(x) = in_{1}(…) ∧ … ⟹ P
⋮
(⋆) ∀v_{1}, …, v_{m}. in_{i}(x) = in_{i}(t) ∧ … ∧ Q_{j} ∧ … ∧ t_{k} ∈ F_{l}(S_{i′}) ∧ … ⟹ P
⋮
∀ …. in_{i}(x) = in_{n}(…) ∧ … ⟹ P

Die Beweisziele mit Prämissen der Gestalt in_{i}(x) = in_{i′′}(…), wobei i ≠ i′′, sind wegen in_{i}(x) ≠ in_{i′′}(…) trivial. Die verbleibenden Beweisziele mit Prämissen der Gestalt in_{i}(x) = in_{i}(…) lassen sich unter Verwendung der Injektivität von in_{i} umformen. Aus (⋆) erhält man beispielsweise

∀v_{1}, …, v_{m}. x = t ∧ … ∧ Q_{j} ∧ … ∧ t_{k} ∈ F_{l}(S_{i′}) ∧ … ⟹ P

was sich unter Verwendung der Voraussetzungen lösen läßt.

Induktionsregel Zum Beweis der Regel zeigen wir zunächst das Lemma

∀x. x ∈ T ⟹ sum case P_{1} … P_{n} x
x_{1} ∈ S_{1} ⟹ P_{1}(x_{1}) ∧ … ∧ x_{n} ∈ S_{n} ⟹ P_{n}(x_{n})

Aus x_{i} ∈ S_{i} folgt nach Definition x_{i} ∈ vimage in_{i} T . Aufgrund der Eigenschaften von vimage folgt hieraus in_{i}(x_{i}) ∈ T . Nach Voraussetzung gilt daher sum case P_{1} … P_{n} (in_{i}(x_{i})), was gleichbedeutend mit P_{i}(x_{i}) ist.

Dieses Lemma ist notwendig, da die zu beweisende Induktionsregel n verschiedene Prädikate enthält, während die im folgenden Beweis verwendete abstrakte Induktionsregel (strongInd) nur für ein einzelnes Prädikat formuliert ist. Wir zeigen nun die Regel

…  ∀v_{1}, …, v_{m}…. ∧ Q_{i} ∧ … ∧ t_{k} ∈ S_{i′} ∧ P_{i′}(t_{k}) ∧ … ⟹ P_{i}(t)  …
∀x. x ∈ T ⟹ sum case P_{1} … P_{n} x

indem wir unter den Voraussetzungen

∀v_{1}, …, v_{m}…. ∧ Q_{i} ∧ … ∧ t_{k} ∈ S_{i′} ∧ P_{i′}(t_{k}) ∧ … ⟹ P_{i}(t)
⋮

das Beweisziel

∀x. x ∈ T ⟹ sum case P_{1} … P_{n} x

zeigen. Mit Hilfe von (strongInd) und der Monotonie von F erhält man hieraus das neue Beweisziel

∀x. x ∈ {x | ∃ …. x = in_{1}(…) ∧ … ∨
… ∨
∃v_{1}, …, v_{m}. x = in_{i}(t) ∧ … ∧ Q_{j} ∧ … ∧
t_{k} ∈ (vimage in_{i′} (T ∩ {x | sum case P_{1} … P_{n} x})) ∧ … ∨
… ∨
∃ …. x = in_{n}(…) ∧ …} ⟹ sum case P_{1} … P_{n} x

Wegen

vimage in_{i′} (T ∩ {x | sum case P_{1} … P_{n} x})
= {Distributivität von vimage über ∩}
(vimage in_{i′}T ) ∩ (vimage in_{i′} {x | sum case P_{1} … P_{n} x})
= {Vereinfachungsregel für vimage und Mengenkomprehension}
(vimage in_{i′}T ) ∩ {x | P_{i′}(x)}
= {Definition von S_{i′}}
S_{i′} ∩ {x | P_{i′}(x)}

erhält man hieraus das Beweisziel

∀x. x ∈ {x | ∃ …. x = in_{1}(…) ∧ … ∨
… ∨
∃v_{1}, …, v_{m}. x = in_{i}(t) ∧ … ∧ Q_{j} ∧ … ∧ t_{k} ∈ (S_{i′} ∩ {x | P_{i′}(x)}) ∧ … ∨
… ∨
∃ …. x = in_{n}(…) ∧ …} ⟹ sum case P_{1} … P_{n} x

Nach Aufspaltung der Disjunktion erhält man |R| verschiedene Beweisziele:

∀x, …. x = in_{1}(…) ∧ … ⟹ sum case P_{1} … P_{n} x
⋮
(⋆⋆) ∀x, v_{1}, …, v_{m}. x = in_{i}(t) ∧ … ∧ Q_{j} ∧ … ∧
t_{k} ∈ S_{i′} ∧ P_{i′}(t_{k}) ∧ … ⟹ sum case P_{1} … P_{n} x
⋮
∀x, …. x = in_{n}(…) ∧ … ⟹ sum case P_{1} … P_{n} x

Aus (⋆⋆) ergibt sich unter Verwendung der Prämisse x = in_{i}(t) das neue Beweisziel

∀x, v_{1}, …, v_{m}. Q_{j} ∧ … ∧ t_{k} ∈ S_{i′} ∧ P_{i′}(t_{k}) ∧ … ⟹ P_{i}(t)

das sich mit Hilfe der Voraussetzungen lösen läßt. Kombiniert man die soeben bewiesene Regel mit dem obigen Lemma, so erhält man die gewünschte Induktionsregel. □

Viele der hier vorgestellten Beweisprinzipien sowie weitere Hinweise zur Implementierung eines Pakets für induktive Definitionen in Isabelle sind in [Paulson, 1994] zu finden. Dieses Papier weicht allerdings in manchen Punkten, insbesondere bei der Behandlung verschränkt rekursiver Mengendefinitionen, etwas von der hier gegebenen Darstellung ab. Da dies in Isabelle/HOL bisher nur unvollständig implementiert war, wurde das existierende Paket für induktive Definitionen im Rahmen dieser Arbeit dahingehend verbessert.

Arten und Eigenschaften von Datentypen

Wir beschreiben im folgenden die Klassen von Datentypen, die mit Hilfe des im Rahmen dieser Dipomarbeit implementierten Datentyppakets definiert werden können. Im einzelnen sind dies verschränkt und verschachtelt rekursive Datentypen, für die wir jeweils charakteristische Theoreme angeben.

3.1 Grundlagen

Viele funktionale Programmiersprachen wie z.B. Haskell oder ML bieten die Möglichkeit, rekursive Datentypen zu definieren. Ein Beispiel hierfür ist der Datentyp der Listen

datatype α list = Nil | Cons α (α list)

Durch diese Definition werden die Konstanten Nil :: α list und Cons :: α → α list → α list eingeführt, die als Konstruktoren des Datentyps bezeichnet werden. Vom Standpunkt der algebraischen Spezifikation funktionaler Programme aus betrachtet sind folgende charakteristische Eigenschaften derartiger Datentypen von Bedeutung:

• Die Konstruktoren sind verschieden, d.h. Nil ≠ Cons x xs

• Die Konstruktoren sind injektiv, d.h. Cons x xs = Cons y ys ⟺ x = y ∧ xs = ys

• Es gilt eine strukturelle Induktionsregel

P Nil ∀x, xs. P xs ⟹ P (Cons x xs)

P xs

Datentypen, deren Konstruktoren verschieden und injektiv sind, werden oft auch als freie Datentypen bezeichnet. Die Konstruktordarstellung von Elementen des Datentyps ist hierbei stets eindeutig. So gilt

Cons x_{1} (Cons x_{2} (… (Cons x_{m} Nil) …)) = Cons y_{1} (Cons y_{2} (… (Cons y_{n} Nil) …)) genau dann, wenn

m = n ∧ ∀i. 1 ≤ i ≤ m ⟹ x_{i} = y_{i}

Datentypen wie α list, für die eine strukturelle Induktionsregel gilt, bezeichnet man als induktive Datentypen. Charakteristisch für induktive Datentypen ist, daß jedes Element dieses Typs eine Darstellung als Konstruktorterm besitzt, weshalb derartige Datentypen gelegentlich auch termerzeugt genannt werden. Insbesondere sind alle Elemente dieses Typs von endlicher ”Tiefe“. Im Fall des Typs α list bedeutet dies, daß die durch

xs ≺ xs′ ≡ ∃x. xs′ = Cons x xs

definierte Relation ≺ fundiert ist. Mit Hilfe der Induktionsregel läßt sich beispielsweise auch zeigen, daß für alle Listen xs stets xs ≠ Cons x xs gilt.

Funktionen auf derartigen Datentypen werden meist durch Angabe mehrerer charakteristischer Gleichungen unter Verwendung von Pattern Matching spezifiziert. So kann z.B. die Funktion foldl :: (α → β → α) → α → β list → α durch die Gleichungen

foldl f a Nil  = a
foldl f a (Cons x xs) = foldl f (f a x) xs

beschrieben werden. Bei der Umsetzung derartiger Funktionsdefinitionen in HOL ist zu beachten, daß Funktionen in HOL stets total sind. Dies macht Beweise bestimmter Eigenschaften von Funktionen zwar einerseits relativ einfach, erfordert jedoch andererseits bei deren Definition eine gewisse Vorsicht: So läßt sich die durch die Gleichung

undefined(x) = undefined(x) + 1

charakterisierte, für jedes Argument nichtterminierende Funktion in HOL nicht unmittelbar beschreiben. Obige Gleichung würde eine Inkonsistenz zur Folge haben, da sich hieraus leicht 0 = 1 folgern ließe. Zur Beschreibung partieller Funktionen besser geeignet sind Logiken wie HOLCF, wo jedoch viele Beweise schwierigere Konzepte wie Fixpunktinduktion und Zulässigkeit erfordern.

Um eine rekursive Funktion in HOL definieren zu können, muß also stets ein Nachweis für deren Terminierung erbracht werden. Bei sogenannten primitiv rekursiven Funktionen ist die Terminierung besonders offensichtlich. Im Falle des Datentyps α list versteht man hierunter jede Funktion, die sich mit Hilfe eines Kombinators

list rec :: β → (α → α list → β → β) → α list → β

darstellen läßt, der durch die Gleichungen

list rec f_{1} f_{2} Nil  = f_{1}  (list rec Nil)
list rec f_{1} f_{2} (Cons x xs) = f_{2} x xs (list rec f_{1} f_{2} xs)  (list rec Cons)

charakterisiert wird. So kann die obige Funktion foldl durch

foldl = λf′, a′, xs′. list rec (λf , a. a) (λx, xs, r. (λf , a. r f (f a x))) xs′ f′ a′

definiert werden. Wie man leicht nachprüft, gilt

foldl f a (Cons x xs)

= {Definition von foldl}

list rec (λf , a. a) (λx, xs, r. (λf , a. r f (f a x))) (Cons x xs) f a

= {list rec Cons}

list rec (λf , a. a) (λx, xs, r. (λf , a. r f (f a x))) xs f (f a x)

= {Definition von foldl}

foldl f (f a x) xs

Die Existenz eines derartigen Kombinators list rec kann, wie in Kapitel 4 gezeigt wird, aus den charakteristischen Eigenschaften des Datentyps, d.h. aus der Verschiedenheit und Injektivität der Konstruktoren sowie der Induktionsregel abgeleitet werden. Man beachte, daß das hier beschriebene, in HOL verwendete Konzept der primitiven Rekursion mächtiger ist als das gleichnamige, aus der Berechenbarkeitstheorie bekannte Konzept. So muß nur ein ausgezeichnetes Argument – im Falle der Funktion foldl das dritte Argument – bei jedem rekursiven Aufruf strukturell kleiner werden. Obwohl die anderen Argumente jeden beliebigen Wert annehmen dürfen, ist die Terminierung der Funktion damit sichergestellt.

Ein allgemeinerer Mechanismus zur Definition rekursiver Funktionen, bei dem der Nachweis der Terminierung durch die Angabe einer fundierten Ordnung auf dem Typ des rekursiven Arguments erbracht wird, ist in [Slind, 1996] beschrieben.

3.2 Verschränkt rekursive Datentypen

Verschränkt rekursive Datentypen haben die allgemeine Gestalt

datatype (α_{1}, …, α_{h})t_{1} = C_{1}^{1} τ_{1,1}^{1} … τ_{1,m_{1}^{1}}^{1} | … | C_{k_{1}}^{1} τ_{k_{1},1}^{1} … τ_{k_{1},m_{k_{1}}^{1}}^{1}
⋮
and  (α_{1}, …, α_{h})t_{n} = C_{1}^{n} τ_{1,1}^{n} … τ_{1,m_{1}^{n}}^{n} | … | C_{k_{n}}^{n} τ_{k_{n},1}^{n} … τ_{k_{n},m_{kn}^{n}}^{n}

wobei TVars (τ_{i,i′}^{j}) ⊆ {α_{1}, …, α_{h}} gilt und τ_{i,i′}^{j} ein zulässiger Typausdruck sein muß. Die Zulässigkeit eines Typausdrucks ist hierbei wie folgt definiert:

Definition 3.1 (Zulässigkeit von Typausdrücken) Ein Typausdruck τ in einer verschränkt rekursiven Datentypdefinition heißt zulässig, falls gilt:

• τ ist nicht rekursiv, d.h. τ enthält keinen der neu definierten Typkonstruktoren t_{1}, …, t_{n}, oder

• τ = (α_{1}, …, α_{h})t_{j′} für 1 ≤ j′ ≤ n

□

Um die Konstruierbarkeit der Datentypen sicherzustellen, dürfen auf der rechten Seite der ”Typgleichungen“ keine spezielleren Instanzen von Typen auf der linken Seite der Gleichungen vorkommen. Bei echt verschränkt rekursiven Datentypdefinitionen kann diese Bedingung nur dann erfüllt sein, wenn alle neu definierten Typkonstruktoren von gleicher Stelligkeit sind, weshalb alle Typkonstruktoren t_{1}, …, t_{n} in der obigen Definitionen die Typparameter α_{1}, …, α_{h} besitzen.

Wie in Abschnitt 2.2.1 angedeutet wurde, dürfen Typen in HOL nicht leer sein. Jeder neue Datentyp (α_{1}, …, α_{h})t_{j} mit 1 ≤ j ≤ n ist hierbei genau dann nicht leer, falls er einen Konstruktor C_{i}^{j} besitzt, für den gilt: Für alle Argumenttypen τ_{i,i′}^{j} der Form (α_{1}, …, α_{h})t_{j′} ist der Datentyp (α_{1}, …, α_{h})t_{j′} nicht leer. Eine notwendige Bedingung ist offensichtlich, daß mindestens ein Datentyp (α_{1}, …, α_{h})t_{j} einen Konstruktor C_{i}^{j} ohne rekursive Argumente hat.

Konstruktoren Für die Typen der durch diese Datentypdefinition eingeführten Konstruktorfunktionen gilt

C_{i}^{j} :: τ_{i,1}^{j} → … → τ_{i,m_{i}^{j}}^{j} → (α_{1}, …, α_{h})t_{j}

Die Konstruktoren sind verschieden, d.h.

i′ ≠ i′′ ⟹ C_{i′}^{j} x_{1} … x_{m_{i′}^{j}} ≠ C_{i′′}^{j} y_{1} … y_{m_{i′′}^{j}}

und injektiv, d.h.

C_{i}^{j} x_{1} … x_{m_{i}^{j}} = C_{i}^{j} y_{1} … y_{m_{i}^{j}} ⟺ x_{1} = y_{1} ∧ … ∧ x_{m_{i}^{j}} = y_{m_{i}^{j}}

Induktion Für die Typen (α_{1}, …, α_{h})t_{1}, …, (α_{1}, …, α_{h})t_{n} gilt eine simultane Induktionsregel der Form

∀x_{1}, …, x_{m_{1}^{1}}. P_{s_{1,1}^{1}} (x_{r_{1,1}^{1}}) ∧ … ∧ P_{s_{1,l^{1}_{1}}^{1}} (x_{r_{1,l^{1}_{1}}^{1}} )  ⟹ P_{1} (C_{1}^{1} x_{1} … x_{m_{1}^{1}})
⋮
∀x_{1}, …, x_{m_{k_{1}}^{1}} . P_{s_{k_{1},1}^{1}} (x_{r_{k_{1},1}^{1}}) ∧ … ∧ P_{s_{k_{1},l{1 \atop k_{1}}}^{1}} (x_{r_{k_{1},l{1 \atop k_{1}}}^{1}} ) ⟹ P_{1} (C_{k_{1}}^{1} x_{1} … x_{m_{k_{1}}^{1}} )
⋮
∀x_{1}, …, x_{m_{1}^{n}} . P_{s_{1,1}^{n}} (x_{r_{1,1}^{n}}) ∧ … ∧ P_{s_{1,l^{n}_{1}}^{n}} (x_{r_{1,l^{n}_{1}}^{n}} )  ⟹ P_{n} (C_{1}^{n} x_{1} … x_{m_{1}^{n}} )
⋮
∀x_{1}, …, x_{m_{kn}^{n}} . P_{s_{kn ,1}^{n}} (x_{r_{kn ,1}^{n}}) ∧ … ∧ P_{s_{kn ,l{n \atop kn}}^{n}} (x_{r_{kn ,l{n \atop kn}}^{n}} ) ⟹ P_{n} (C_{k_{n}}^{n} x_{1} … x_{m_{kn}^{n}} )
P_{1} (x_{1}) ∧ … ∧ P_{n} (x_{n})

wobei

{(r_{i,1}^{j}, s_{i,1}^{j}) , …, (r_{i,l_{i}^{j}}^{j} , s_{i,l_{i}^{j}}^{j} )} =
{(i′, i′′) | 1 ≤ i′ ≤ m_{i}^{j} ∧ 1 ≤ i′′ ≤ n ∧ τ_{i,i′}^{j} = (α_{1}, …, α_{h})t_{i′′} }

Hierbei bezeichnen r_{i,1}^{j}, …, r_{i,l_{i}^{j}}^{j} die Positionen der rekursiven Argumenttypen für den Kon-

struktor C_{i}^{j} . Die Indizes der in den entsprechenden Positionen vorkommenden rekursiven Typen werden durch s_{i,1}^{j}, …, s_{i,l_{i}^{j}}^{j} angegeben.

Primitive Rekursion Für jeden der n Typen existiert ein Kombinator für primitive Rekursion

t_{j} rec :: (τ_{1,1}^{1} → ⋯ → τ_{1,m_{1}^{1}}^{1} → β_{s_{1,1}^{1}} → ⋯ → β_{s_{1,l^{1}_{1}}^{1}} → β_{1}) →
⋯ →
(τ_{k_{1},1}^{1} → ⋯ → τ_{k_{1},m_{k_{1}}^{1}}^{1} → β_{s_{k_{1},1}^{1}} → ⋯ → β_{s_{k_{1},l{1 \atop k_{1}}}^{1}} → β_{1}) →
⋯ →
(τ_{1,1}^{n} → ⋯ → τ_{1,m_{1}^{n}}^{n} → β_{s_{1,1}^{n}} → ⋯ → β_{s_{1,l^{n}_{1}}^{n}} → β_{n}) →
⋯ →
(τ_{k_{n},1}^{n} → ⋯ → τ_{k_{n},m_{kn}^{n}}^{1} → β_{s_{kn ,1}^{n}} → ⋯ → β_{s_{kn ,l{n \atop kn}}^{n}} → β_{n}) →
(α_{1}, …, α_{h})t_{j} → β_{j}

mit den charakteristischen Gleichungen

t_{j} rec f_{1}^{1} … f_{k_{1}}^{1} … f_{1}^{n} … f_{k_{n}}^{n} (C_{i}^{j} x_{1} … x_{m_{i}^{j}} ) =
f_{i}^{j} x_{1} … x_{m_{i}^{j}} (t_{s_{i,1}^{j}} rec f_{1}^{1} … f_{k_{n}}^{n} x_{r_{i,1}^{j}}) … (t_{s_{i,l{j \atop i}}^{j}} rec f_{1}^{1} … f_{k_{n}}^{n} x_{r_{i,l{j \atop i}}^{j}} )

Für manche Beweise ist anstatt von Induktion bereits eine Fallunterscheidung über alle Konstruktoren des Datentyps t_{j} ausreichend, wofür die Regel

∀x_{1}, …, x_{m_{1}^{j}}. u = C_{1}^{j} x_{1} … x_{m_{1}^{j}} ⟹ P
⋮
∀x_{1}, …, x_{m_{k_{j}}^{j}} . u = C_{k_{j}}^{j} x_{1} … x_{m_{k_{j}}^{j}} ⟹ P

P

verwendet wird, die sich leicht aus der obigen Induktionsregel ableiten läßt. Anstelle des Kombinators t_{j} rec ist zur Definition von Funktionen auf (α_{1}, …, α_{h})t_{j} manchmal auch der einfachere Kombinator

t_{j} case :: (τ_{1,1}^{j} → ⋯ → τ_{1,m_{1}^{j}}^{j} → β) → ⋯ → (τ_{k_{j} ,1}^{j} → ⋯ → τ_{k_{j} ,m_{k_{j}}^{j}}^{j} → β) →
(α_{1}, …, α_{h})t_{j} → β

mit den charakteristischen Gleichungen

t_{j} case f_{1} … f_{k_{j}} (C_{i}^{j} x_{1} … x_{m_{i}^{j}} ) = f_{i} x_{1} … x_{m_{i}^{j}}

ausreichend, der sich leicht auf den entsprechenden Kombinator t_{j} rec zurückführen läßt.

Ein Beispiel für verschränkt rekursive Datentypen sind die bereits aus Abschnitt 1.4 bekannten arithmetischen und booleschen Ausdrücke, die sich wie folgt definieren lassen:

datatype α aexp = If then else (α bexp) (α aexp) (α aexp)
| Sum (α aexp) (α aexp)
| Diff (α aexp) (α aexp)
| Var α
| Num nat
and  α bexp = Less (α aexp) (α aexp)
| And (α bexp) (α bexp)
| Or (α bexp) (α bexp)

für die Typen α aexp und α bexp erhält man die Induktionsregel

∀b, a_{1}, a_{2}. P_{2} b ∧ P_{1} a_{1} ∧ P_{1} a_{2} ⟹ P_{1} (If then else b a_{1} a_{2})
∀a_{1}, a_{2}. P_{1} a_{1} ∧ P_{1} a_{2}  ⟹ P_{1} (Sum a_{1} a_{2})
∀a_{1}, a_{2}. P_{1} a_{1} ∧ P_{1} a_{2}  ⟹ P_{1} (Diff a_{1} a_{2})
∀v.  P_{1} (Var v)
∀n.  P_{1} (Num n)
∀a_{1}, a_{2}. P_{1} a_{1} ∧ P_{1} a_{2}  ⟹ P_{2} (Less a_{1} a_{2})
∀b_{1}, b_{2}. P_{2} b_{1} ∧ P_{2} b_{2}  ⟹ P_{2} (And b_{1} b_{2})
∀b_{1}, b_{2}. P_{2} b_{1} ∧ P_{2} b_{2}  ⟹ P_{2} (Or b_{1} b_{2})
P_{1} a ∧ P_{2} b

Die Kombinatoren aexp rec und bexp rec für primitive Rekursion besitzen die charakteristischen Gleichungen

aexp rec f_{1} … f_{8} (If then else b a_{1} a_{2}) = f_{1} b a_{1} a_{2} (bexp rec f_{1} … f_{8} b) (aexp rec f_{1} … f_{8} a_{1}) (aexp rec f_{1} … f_{8} a_{2})

aexp rec f_{1} … f_{8} (Sum a_{1} a_{2}) = f_{2} a_{1} a_{2} (aexp rec f_{1} … f_{8} a_{1}) (aexp rec f_{1} … f_{8} a_{2})

aexp rec f_{1} … f_{8} (Diff a_{1} a_{2}) = f_{3} a_{1} a_{2} (aexp rec f_{1} … f_{8} a_{1}) (aexp rec f_{1} … f_{8} a_{2})

aexp rec f_{1} … f_{8} (Var v) = f_{4} v

aexp rec f_{1} … f_{8} (Num n) = f_{5} n

bexp rec f_{1} … f_{8} (Less a_{1} a_{2}) = f_{6} a_{1} a_{2} (aexp rec f_{1} … f_{8} a_{1}) (aexp rec f_{1} … f_{8} a_{2})

bexp rec f_{1} … f_{8} (And b_{1} b_{2}) = f_{7} b_{1} b_{2} (bexp rec f_{1} … f_{8} b_{1}) (bexp rec f_{1} … f_{8} b_{2})

bexp rec f_{1} … f_{8} (Or b_{1} b_{2}) = f_{8} b_{1} b_{2} (bexp rec f_{1} … f_{8} b_{1}) (bexp rec f_{1} … f_{8} b_{2})

3.3 Verschachtelt rekursive Datentypen

Wir betrachten nun Datentypdefinitionen der Form

datatype (α_{1}, …, α_{h})t_{1} = C_{1}^{1} τ_{1,1}^{1} … τ_{1,m_{1}^{1}}^{1} | … | C_{k_{1}}^{1} τ_{k_{1},1}^{1} … τ_{k_{1},m_{k_{1}}^{1}}^{1}
⋮
and  (α_{1}, …, α_{h})t_{n} = C_{1}^{n} τ_{1,1}^{n} … τ_{1,m_{1}^{n}}^{n} | … | C_{k_{n}}^{n} τ_{k_{n},1}^{n} … τ_{k_{n},m_{kn}^{n}}^{n}

wobei für die Typen τ_{i,i′}^{j} nun eine gegenüber Abschnitt 3.2 leicht geänderte Zulässigkeitsbedingung gilt.

Definition 3.2 (Zulässigkeit von Typausdrücken) Ein Typausdruck τ in einer verschachtelt rekursiven Datentypdefinition heißt zulässig, falls gilt:

• τ ist nicht rekursiv, d.h. τ enthält keinen der neu definierten Typkonstruktoren t_{1}, …, t_{n}, oder

• τ = (α_{1}, …, α_{h})t_{j′} für 1 ≤ j′ ≤ n, oder

• τ = (τ′_{1}, …, τ ′ ; h̃)t̃_{j′′}, wobei t̃_{j′′} der Typkonstruktor eines bereits durch eine verschränkt rekursive Datentypdefinition

datatype (β_{1}, …, βh̃)t̃_{1} = D_{1}^{1} τ̃_{1,1}^{1} … τ̃_{1,m̃_{1}^{1}}^{1} | … | D1 k̃_{1} τ̃_{k̃_{1},1}^{1} … τ̃_{k̃_{1},m̃1 k̃_{1}}^{1}
⋮
and  (β_{1}, …, βh̃)t̃ñ = Dñ 1 τ̃ ñ ; 1,1 … τ̃ ñ ; 1,m̃ñ 1 | … | Dñ k̃ñ τ̃ ñ ; k̃ñ,1 … τ̃ ñ ; k̃ñ,m̃ñ k̃ñ

im Sinne von Abschnitt 3.2 gegebenen Datentyps ist und für alle Typausdrücke τ̃ j̃ ; ĩ,ĩ′,

die nicht von der Form (β_{1}, …, βh̃)t̃_{j′′′} sind, der Typausdruck τ̃ j̃ ; ĩ,ĩ′ [τ′_{1}/β_{1}, …, τ ′ ; h̃/βh̃] zulässig ist.

□

Bemerkung 3.3 Wie später gezeigt wird, können verschachtelt rekursive Datentypen auf verschränkt rekursive Datentypen ohne Verschachtelungen zurückgeführt werden. Wir dürfen daher o.B.d.A. davon ausgehen, daß es sich bei den in der oben beschriebenen Datentypdefinition vorkommenden, bereits früher definierten Datentypen um verschränkt rekursive Datentypen im Sinne von Abschnitt 3.2 handelt.

Beispiel 3.4 Sei die korrekte Datentypdefinition

datatype (α, β)example1 = C1 (α → bool) (β list)
| C2 ((α, β)example1)

gegeben. Dann ist

datatype γ example2 = C3 ((γ example2, γ)example1)
| C4 γ

keine korrekte Datentypdefinition, denn γ example2 → bool ist kein korrekter Typausdruck im Sinne der obigen Definition. Die Definition

datatype γ example3 = C5 ((γ, γ example3)example1)
| C6 γ

ist jedoch korrekt, denn (γ example3)list und γ → bool sind korrekte Typausdrücke. □

Ein weiteres Beispiel für einen Datentyp mit verschachtelter Rekursion ist der Datentyp der Terme, der durch

datatype (α, β)term = Var α
| App β (((α, β)term)list)

definiert ist. Zur Handhabung derartiger Datentypen sind in der einschlägigen Literatur im wesentlichen zwei verschiedene Verfahren zu finden. Mit einem dieser Verfahren, das auch für das im Rahmen dieser Arbeit implementierte Datentyppaket für Isabelle/HOL gewählt wurde, beschäftigt sich der folgende Abschnitt. Ein etwas anderer Ansatz ist in Abschnitt 6.2 beschrieben.

Formulierung mittels Auffalten In [Gunter, 1992, Gunter, 1993] wird vorgeschlagen, Datentypen mit verschachtelter Rekursion mittels ”Auffalten“ auf verschränkt rekursive Datentypen zurückzuführen: Sei eine Datentypdefinition der Form

datatype (α_{1}, …, α_{h})t_{1} = C_{1}^{1} τ_{1,1}^{1} … τ_{1,m_{1}^{1}}^{1} | … | C_{k_{1}}^{1} τ_{k_{1},1}^{1} … τ_{k_{1},m_{k_{1}}^{1}}^{1}
⋮
and  (α_{1}, …, α_{h})t_{j} = …
| C_{i}^{j} τ_{i,1}^{j} … τ_{i,i′−1}^{j} (τ′_{1}, …, τ ′ ; h̃)t̃_{j′} τ_{i,i′+1}^{j} … τ_{1,m_{i}^{j}}^{1}
| …
⋮
and  (α_{1}, …, α_{h})t_{n} = C_{1}^{n} τ_{1,1}^{n} … τ_{1,m_{1}^{n}}^{n} | … | C_{k_{n}}^{n} τ_{k_{n},1}^{n} … τ_{k_{n},m_{kn}^{n}}^{n}

gegeben, wobei τ′_{1}, …, τ ′ ; h̃ die neu definierten Typkonstruktoren t_{1}, …, t_{n} enthalten und der Datentyp t̃_{j′} durch eine verschränkt rekursive Datentypdefinition der Form

datatype (β_{1}, …, βh̃)t̃_{1} = D_{1}^{1} τ̃_{1,1}^{1} … τ̃_{1,m̃_{1}^{1}}^{1} | … | D1 k̃_{1} τ̃_{k̃_{1},1}^{1} … τ̃_{k̃_{1},m̃1 k̃_{1}}^{1}
⋮
and  (β_{1}, …, βh̃)t̃ñ = Dñ 1 τ̃ ñ ; 1,1 … τ̃ ñ ; 1,m̃ñ 1 | … | Dñ k̃ñ τ̃ ñ ; k̃ñ,1 … τ̃ ñ ; k̃ñ,m̃ñ k̃ñ

beschrieben ist. Wir definieren nun eine Transformationsfunktion trans auf Typausdrücken τ durch

trans(τ) = \{ \begin{matrix}(α_{1}, …, α_{h})t̂_{j′′} & falls τ = (β_{1}, …, βh̃)t̃_{j′′} \\ τ [τ′_{1}/β_{1}, …, τ ′ ; h̃/βh̃] & sonst \end{matrix}

wobei t̂_{1}, …, t̂ñ bisher nicht verwendete Typkonstruktoren sind. Dann kann die obige Typdefinition zu

datatype (α_{1}, …, α_{h})t_{1} = C_{1}^{1} τ_{1,1}^{1} … τ_{1,m_{1}^{1}}^{1} | … | C_{k_{1}}^{1} τ_{k_{1},1}^{1} … τ_{k_{1},m_{k_{1}}^{1}}^{1}
⋮
and  (α_{1}, …, α_{h})t_{j} = …
| C_{i}^{j} τ_{i,1}^{j} … τ_{i,i′−1}^{j} (α_{1}, …, α_{h})t̂_{j′} τ_{i,i′+1}^{j} … τ_{1,m_{i}^{j}}^{1}
| …
⋮
and  (α_{1}, …, α_{h})t_{n} = C_{1}^{n} τ_{1,1}^{n} … τ_{1,m_{1}^{n}}^{n} | … | C_{k_{n}}^{n} τ_{k_{n},1}^{n} … τ_{k_{n},m_{kn}^{n}}^{n}
and  (α_{1}, …, α_{h})t̂_{1} = D_{1}^{1} (trans τ̃_{1,1}^{1}) … (trans τ̃_{1,m̃_{1}^{1}}^{1})
| …
| D1 k̃_{1} (trans τ̃_{k̃_{1},1}^{1}) … (trans τ̃_{k̃_{1},m̃1 k̃_{1}}^{1} )
⋮
and  (α_{1}, …, α_{h})t̂ñ = Dñ 1 (trans τ̃ ñ ; 1,1) … (trans τ̃ ñ ; 1,m̃ñ 1 )
| …
| Dñ k̃ñ (trans τ̃ ñ ; k̃ñ,1) … (trans τ̃ ñ ; k̃ñ,m̃ñ k̃ñ )

umgeformt werden. Durch wiederholtes Anwenden dieser Transformation erhält man schließlich eine Datentypdefinition im Sinne von Abschnitt 3.2, in der die neu definierten Typen nicht mehr verschachtelt vorkommen.

Der eingangs erwähnte Typ term ließe sich demnach zu

datatype (α, β)term  = Var α
| App β ((α, β)term list)
and  (α, β)term list = Nil’
| Cons’ ((α, β)term) ((α, β)term list)

auffalten. Man beachte, daß der Typ term list sowie die Konstruktoren Nil’ und Cons’ nicht wirklich eingeführt werden, da dies zur Folge hätte, daß für den Datentyp list bewiesene Theoreme in Beweisen von Theoremen über term nicht mehr verwendbar wären. Vielmehr muß, wie in Abschnitt 4.3 dargestellt wird, die Isomorphie zwischen dem Typ ((α, β)term)list und der repräsentierenden Menge des ”aufgefalteten“ (nicht wirklich eingeführten) Typs (α, β)term list nachgewiesen werden. Die Induktionsregel für term lautet daher

∀a.  P_{1} (Var a)
∀b, ts. P_{2} ts  ⟹ P_{1} (App b ts)
P_{2} Nil
∀t, ts. P_{1} t ∧ P_{2} ts ⟹ P_{2} (Cons t ts)
P_{1} t ∧ P_{2} ts

Aufgrund der Auffaltung sind für primitive Rekursion nun die zwei Kombinatoren

term rec  : (α → γ) → (β → (((α, β)term)list) → δ → γ) →
δ → ((α, β)term → (((α, β)term)list) → γ → δ → δ) →
(α, β)term → γ
term list rec : (α → γ) → (β → (((α, β)term)list) → δ → γ) →
δ → ((α, β)term → (((α, β)term)list) → γ → δ → δ) →
(((α, β)term)list) → δ

erforderlich, die die charakteristischen Gleichungen

term rec f_{1} … f_{4} (Var a) = f_{1} a

term rec f_{1} … f_{4} (App b ts) = f_{2} b ts (term list rec f_{1} … f_{4} ts)

term list rec f_{1} … f_{4} Nil = f_{3}

term list rec f_{1} … f_{4} (Cons t ts) = f_{4} t ts (term rec f_{1} … f_{4} t) (term list rec f_{1} … f_{4} ts)

besitzen. Bei tiefer verschachtelten Typen wie

datatype (α, β)term2 = Var α
| App β ((((α, β)term2)list)list)

muß mehrmals aufgefaltet werden. So erhält man für term2 die Auffaltung

datatype (α, β)term2  = Var α
| App β ((α, β)term2 list list)
and  (α, β)term2 list list = Nil’
| Cons’ ((α, β)term2 list) ((α, β)term2 list list)
and (α, β)term2 list = Nil”
| Cons” ((α, β)term2) ((α, β)term2 list)

Beispiel 3.5 Um die Anwendung der soeben dargestellten Theoreme für term zu demonstrieren, wollen wir im folgenden die Substitution von Variablen in Termen durch Terme formalisieren. Zu diesem Zweck werden die beiden Funktionen

subst term  :: (α → (α, β)term) → (α, β)term → (α, β)term
subst term list :: (α → (α, β)term) → ((α, β)term)list → ((α, β)term)list

benötigt. Die Idee ist, eine gegebene Funktion f vom Typ α → (α, β)term auf Terme bzw. Listen von Termen zu erweitern. Das Verhalten der primitiv rekursiven Funktionen subst term und subst term list kann durch die Gleichungen

subst term f (Var a)  = f a
subst term f (App b ts)  = App b (subst term list f ts)
subst term list f Nil  = Nil
subst term list f (Cons t ts) = Cons (subst term f t) (subst term list f ts)

charakterisiert werden. Mit Hilfe der Kombinatoren term rec und term list rec definieren wir nun

subst term f  ≡ term rec f (λb, xs, ys. App b ys) Nil (λx, xs, y, ys. Cons y ys)
subst term list f ≡ term list rec f (λb, xs, ys. App b ys) Nil (λx, xs, y, ys. Cons y ys)

woraus sich die obigen charakteristischen Gleichungen sofort ableiten lassen. Für die Komposition von Substitutionsfunktionen auf (α, β)term gilt offenbar

subst term (subst term f_{1} ∘ f_{2}) t = subst term f_{1} (subst term f_{2} t)

Um dies mit der oben angegebenen Induktionsregel beweisen zu können, muß allerdings auch noch eine entsprechende Eigenschaft für Substitutionsfunktionen auf ((α, β)term)list formuliert werden. Wir wählen also das Beweisziel

subst term (subst term f_{1} ∘ f_{2}) t = subst term f_{1} (subst term f_{2} t) ∧

subst term list (subst term f_{1} ∘ f_{2}) ts = subst term list f_{1} (subst term list f_{2} ts)

Mittels simultaner Induktion über t und ts erhält man hieraus die neuen Beweisziele

(1) ∀a. subst term (subst term f_{1} ∘ f_{2}) (Var a) = subst term f_{1} (subst term f_{2} (Var a))
(2) ∀b, xs. subst term list (subst term f_{1} ∘ f_{2}) xs =

subst term list f_{1} (subst term list f_{2} xs) ⟹ subst term (subst term f_{1} ∘ f_{2}) (App b xs) = subst term f_{1} (subst term f_{2} (App b xs))

(3) subst term list (subst term f_{1} ∘ f_{2}) Nil = subst term list f_{1} (subst term list f_{2} Nil)
(4) ∀x, xs. subst term (subst term f_{1} ∘ f_{2}) x = subst term f_{1} (subst term f_{2} x) ∧

subst term list (subst term f_{1} ∘ f_{2}) xs = subst term list f_{1} (subst term list f_{2} xs) ⟹

subst term list (subst term f_{1} ∘ f_{2}) (Cons x xs) = subst term list f_{1} (subst term list f_{2} (Cons x xs))

KAPITEL 3. ARTEN UND EIGENSCHAFTEN VON DATENTYPEN 35 Beweisziel (4) kann nun beispielsweise durch die folgende Umformung gezeigt werden:

subst term list (subst term f_{1} ∘ f_{2}) (Cons x xs)

= {charakteristische Gleichungen für subst term list}

Cons (subst term (subst term f_{1} ∘ f_{2}) x) (subst term list (subst term f_{1} ∘ f_{2}) xs)

= {Induktionsvoraussetzung}

Cons (subst term f_{1} (subst term f_{2} x)) (subst term list f_{1} (subst term list f_{2} xs))

= {charakteristische Gleichungen für subst term list}

subst term list f_{1} (Cons (subst term f_{2} x) (subst term list f_{2} xs))

= {charakteristische Gleichungen für subst term list}

subst term list f_{1} (subst term list f_{2} (Cons x xs))

□

Konstruktion von Datentypen in HOL

Im folgenden Kapitel wird aufgezeigt, wie die Datentypen, deren Eigenschaften in Kapitel 3 abstrakt beschrieben wurden, konkret in Isabelle/HOL konstruiert werden können. Im einzelnen umfaßt diese Konstruktion folgende Teilschritte:

1. Auffalten verschachtelt rekursiver Definitionen

2. Konstruktion der repräsentierenden Mengen

3. Definition der neuen Typen

4. Beweis von Isomorphie-Eigenschaften

5. Definition der Konstruktoren

6. Repräsentationsabhängige Beweise charakteristischer Theoreme • Verschiedenheit von Konstruktoren • Injektivität von Konstruktoren • Strukturelle Induktion

7. Repräsentationsunabhängige Beweise charakteristischer Theoreme • Fallunterscheidung

• Primitive Rekursion

• case-Kombinator

• …

Die hier beschriebenen Verfahren sind im Rahmen dieser Arbeit in Form eines Datentyppakets für Isabelle/HOL implementiert worden. Durch die definitorische Vorgehensweise ist sichergestellt, daß die durch das Paket abgeleiteten Regeln auch korrekt sind. Eine weitere Frage ist, ob die Verfahren auch vollständig sind, d.h. für alle in Kapitel 3 beschriebenen Datentypen funktionieren. Dies soll in den folgenden Abschnitten geklärt werden.

4.1 Auffalten verschachtelt rekursiver Definitionen

In Abschnitt 3.3 wurde bereits erwähnt, daß verschachtelt rekursive Definitionen durch Auffalten realisiert werden sollen. Ergebnis dieser Auffaltung ist eine Typdefinition der Form

datatype (α_{1}, …, α_{h})t_{1}  = C_{1}^{1} … | … | C_{k_{1}}^{1} …
⋮
and  (α_{1}, …, α_{h})t_{ν_{1}−1} = C_{1}^{ν_{1}−1} … | … | C_{k_{ν_{1}−1}}^{ν_{1}−1} …
and  (α_{1}, …, α_{h})t_{ν_{1}} = C_{1}^{ν_{1}} … | … | C_{k_{ν_{1}}}^{ν_{1}} …
⋮
and  (α_{1}, …, α_{h})t_{ν_{2}−1} = C_{1}^{ν_{2}−1} … | … | C_{k_{ν_{2}−1}}^{ν_{2}−1} …
⋮
and  (α_{1}, …, α_{h})t_{ν_{n′}} = C_{1}^{ν_{n′}} … | … | C_{k_{ν_{n′}}}^{ν_{n′}} …
⋮
and  (α_{1}, …, α_{h})t_{n}  = C_{1}^{n} … | … | C_{k_{n}}^{n} …

die im folgenden als Ausgangspunkt für die abstrakte Beschreibung der Konstruktionen und Beweise dienen soll. Hierbei sind nur die Typen (α_{1}, …, α_{h})t_{1}, …, (α_{1}, …, α_{h})t_{ν_{1}−1} tatsächlich neu, während die n′ Gruppen von Typen

(α_{1}, …, α_{h})t_{ν_{1}} … (α_{1}, …, α_{h})t_{ν_{2}−1}
⋮
(α_{1}, …, α_{h})t_{ν_{n′}} … (α_{1}, …, α_{h})t_{n}

jeweils in einem Auffaltungsschritt entstandene Kopien bereits existierender, verschränkt rekursiver Typen

(τ̂_{1}^{ν_{1}}, …, τ̂ ν_{1} ; h̃_{1}) t̃_{ν_{1}}  … (τ̂_{1}^{ν_{2}−1}, …, τ̂ ν_{2}−1 ; h̃_{1}) t̃_{ν_{2}−1}
⋮
(τ̂_{1}^{ν_{n′}} , …, τ̂ ν_{n′} ; h̃_{n′} ) t̃_{ν_{n′}} … (τ̂_{1}^{n}, …, τ̂ n ; h̃_{n′} ) t̃_{n}

sind, wobei die Reihenfolge der Aufschreibung der Reihenfolge der Auffaltung entspricht. Bei der Konstruktion der neuen Typen kann daher auf bereits bewiesene charakteristische Theoreme der schon existierenden Typen wie z.B. simultane Induktionsregeln für [t̃_{ν_{1}}, …, t̃_{ν_{2}−1}], …, [t̃_{ν_{n′}} , …, t̃_{n}] sowie auf die Kombinatoren t̃_{ν_{1}} rec, …, t̃_{n} rec für primitive Rekursion zurückgegriffen werden.

In der aufgefalteten Definition von term taucht beispielsweise der Typ (α, β)term list auf, der eine Kopie des Typs ((α, β)term)list ist. Faltet man die Definition des Typs term2 auf, enthält die entstehende Definition zusätzlich den Typ (α, β)term2 list list, der eine Kopie des Typs (((α, β)term2)list)list ist, sowie den Typ (α, β)term2 list, bei dem es sich um eine Kopie des Typs ((α, β)term2)list handelt.

4.2 Konstruktion der repräsentierenden Mengen

In Abschnitt 2.2.3 wurde erläutert, wie neue Typen durch Angabe einer repräsentierenden Menge mit geeigneten Eigenschaften definitorisch eingeführt werden können. Als repräsentierende Menge dient hierbei eine Teilmenge eines bereits existierenden Typs. Es stellt sich daher die Frage, welcher Typ für diesen Zweck passend ist und wie die entsprechende Teilmenge dieses Typs am besten charakterisiert werden kann. Vergleicht man die gewünschten Eigenschaften der repräsentierenden Menge eines Datentyps mit den in Abschnitt 2.3.2 beschriebenen Eigenschaften induktiv definierter Mengen, so fallen eine Reihe von Gemeinsamkeiten auf. So sollte auch die repräsentierende Menge eines Datentyps unter gewissen Regeln abgeschlossen sein. Ist z.B. xs eine Liste, so sollte auch Cons x xs eine Liste sein. Außerdem sollte auf dem Datentyp eine Induktionsregel gelten. Als Methode zur Charakterisierung der repräsentierenden Menge erscheinen daher induktive Definitionen bzw. kleinste Fixpunkte als angemessen. Die ”Gleichung“

datatype α list = Nil | Cons α (α list)

auf Typebene wird also zur Fixpunktgleichung

list rep set = F (list rep set)

auf Mengenebene, wobei die monotone Funktion F die rechte Seite der obigen ”Typgleichung“ verkörpert.

Soll ein rekursiver Datentyp durch eine Menge vom Typ τ set repräsentiert werden, so müssen auf τ bestimmte Funktionen definiert sein:

• injektive Funktionen f_{i} : τ_{i} → τ zur Einbettung nichtrekursiver Elemente vom Typ τ_{i}

• injektive Funktionen g : τ → τ und g′ : τ → τ mit disjunktem Wertebereich (”disjunkte Summe“) zur Modellierung mehrerer verschiedener Konstruktoren

• eine injektive Funktion p : τ → τ → τ zur Darstellung von Konstruktoren mit mehreren Argumenten (”Produkt“)

Auf den ersten Blick scheint es naheliegend zu sein, zur Repräsentation die in HOL standardmäßig vorhandenen Typen α + β für disjunkte Summen bzw. α × β für das kartesische Produkt mit den injektiven Funktionen

\begin{matrix}Inl  : & α → α + β \\ Inr  : & β → α + β \\ ( , )  : & α → β → α × β \end{matrix}

zu verwenden, wobei Inl x ≠ Inr y gilt. Das Problem liegt jedoch darin, daß der Ergebnistyp der Funktionen Inl, Inr und ( , ) stets strukturell größer als der Typ der Argumente ist. Dies bedeutet im Falle der obigen Fixpunktgleichung, daß auch der Typ von F (list rep set) strukturell größer als der Typ von list rep set ist, weshalb die Fixpunktgleichung bei Verwendung der Funktionen Inl, Inr und ( , ) in F nicht wohlgetypt sein kann. Um die Wohlgetyptheit der Fixpunktgleichung zu gewährleisten, ist daher zur Repräsentation rekursiver Typen ein Typ notwendig, der unter Summen und Produkten abgeschlossen ist. Ein Typ mit derartigen Eigenschaften – im folgenden Universum genannt – wurde in [Paulson, 1997] vorgestellt. Die wichtigsten Eigenschaften dieses Typs werden nun im nächsten Abschnitt kurz beschrieben.

4.2.1 Ein Universum für rekursive Typen

Mit dem in [Paulson, 1997] präsentierten und in Form der Isabelle/HOL-Theorie Univ implementierten Typ können Bäume wie z.B. in Abbildung 4.1 in HOL dargestellt werden. Da sich die Elemente rekursiver Datentypen als Bäume auffassen lassen, ist dieser Typ gut zur Repräsentation von Datentypen geeignet.

[figure: 1; 2; 1; 2; 1; 2; a_{1}; a_{2}; a_{3}; a_{4}]

Abbildung 4.1: Endlicher Baum

Derartige Bäume sind im wesentlichen Mengen von Blättern, die über einen bestimmten Pfad erreichbar sind. Ein Baum wird daher durch eine Menge von Paaren dargestellt, wobei jedes Paar ein Blatt des Baums repräsentiert. Die erste Komponente des Paars enthält dabei den zum Blatt führenden Pfad, kodiert als Funktion vom Typ nat → nat. Die zweite Komponente enthält den eigentlichen Wert des Blatts. Für den Baum aus Abbildung 4.1 ergibt sich somit die Repräsentation^{1}

T = {(f_{1}, a_{1}), (f_{2}, a_{2}), (f_{3}, a_{3}), (f_{4}, a_{4})}

wobei

f_{1} = ⟨1, 0, 0, …⟩
f_{2} = ⟨2, 1, 0, 0, …⟩
f_{3} = ⟨2, 2, 1, 0, 0, …⟩
f_{4} = ⟨2, 2, 2, 0, 0, …⟩

Der Wert 0 markiert hierbei jeweils das Ende eines Pfads. Nach diesem Verfahren lassen sich prinzipiell auch Bäume unendlicher Tiefe bzw. mit unendlichem Verzweigungsgrad beschreiben. Da als Labels für Verzweigungen natürliche Zahlen gewählt wurden, kann der Verzweigungsgrad dabei höchstens abzählbar unendlich sein. In Kapitel 5 werden für diese Labels beliebige Typen zugelassen. Formal haben Bäume den Typ α item, wobei

1f = ⟨y_{0}, y_{1}, …⟩ bedeutet hierbei f (0) = y_{0}, f (1) = y_{1}, …

α node = (nat → nat) × (α + nat)
α item = (α node)set

Hierbei ist zu beachten, daß nicht alle Elemente des Typs α item tatsächlich Bäume bzw. Elemente von Datentypen repräsentieren müssen. Dies ist z.B. dann der Fall, wenn α item Blätter mit unendlich langen Zugriffspfaden enthält. Bei der induktiven Definition der repräsentierenden Menge eines Datentyps werden diese störenden Elemente – gelegentlich auch als ”Junk“ bezeichnet – jedoch ausgeschlossen.

Zur Erzeugung von Bäumen sind die folgenden Funktionen definiert^{2}:

push  :: nat → α node → α node
push c n ≡ (nat case c (fst n), snd n)
Scons  :: α item → α item → α item
Scons i_{1} i_{2} ≡ (push 1 “ i_{1}) ∪ (push 2 “ i_{2})
Leaf  :: α → α item
Leaf a  ≡ {(λx. 0, Inl a)}
Numb  :: nat → α item
Numb k  ≡ {(λx. 0, Inr k)}

Die Funktion push fügt ein Label als Präfix an den Pfad eines Blatts an, d.h.

push c (⟨y_{0}, y_{1}, …⟩, a) = (⟨c, y_{0}, y_{1}, …⟩, a)

Mit Scons können zwei Bäume zu einem neuen Baum verknüpft werden. Hierbei wird an alle Pfade der Blätter aus der Menge i_{1} das Präfix 1, an alle Pfade der Blätter aus der Menge i_{2} das Präfix 2 hinzugefügt und die sich so ergebenden Blättermengen vereinigt. Dies ist in Abbildung 4.2 graphisch dargestellt.

[figure: i_{1}; i_{2}; ⟼^{Scons}; i_{1}; i_{2}; 1; 2]

Abbildung 4.2: Verknüpfen zweier Bäume durch Scons Die Funktionen Leaf und Numb erzeugen jeweils einen Baum der Tiefe 0 mit genau einem Blatt. Mit Hilfe elementarer Eigenschaften von Mengen und Funktionen kann die Injektivität der Funktionen Scons, Leaf und Numb leicht nachgewiesen werden. Darüberhinaus werden noch die Funktionen

2Es gilt

f “ S = {y | ∃x. x ∈ S ∧ y = f (x)} nat case : α → (nat → α) → nat → α nat case f g 0  = f nat case f g (Suc x) = g x

In0 :: α item → α item
In0 i ≡ Scons (Numb 0) i
In1 :: α item → α item
In1 i ≡ Scons (Numb 1) i

definiert. Diese sind ebenfalls injektiv und es gilt In0 x ≠ In1 y, was aus der Injektivität von Scons und Numb sowie 0 ≠ 1 folgt. Mit den Funktionen Leaf, In0, In1 und Scons stehen somit die eingangs geforderten Konstruktionselemente für rekursive Typen zur Verfügung.

4.2.2 Induktive Definition der repräsentierenden Mengen

Mit Hilfe der soeben beschriebenen Funktionen kann somit die den Datentyp α list repräsentierende Menge

list rep set :: (α item)set

induktiv durch die beiden Regeln

In0 arbitrary ∈ list rep set

xs ∈ list rep set In1 (Scons (Leaf x) xs) ∈ list rep set

bzw. als kleinster Fixpunkt durch

F (L) = {x | x = In0 arbitrary ∨ ∃y :: α, ys. x = In1 (Scons (Leaf y) ys) ∧ ys ∈ L}
list rep set = lfp(F )

definiert werden, wobei F vom Typ (α item)set → (α item)set ist.

Für den Typ (α, β)term sind die beiden Mengen

term rep set  :: ((α + β)item)set
term list rep set :: ((α + β)item)set

induktiv durch die Regeln

In0 (Leaf (Inl a)) ∈ term rep set

xs ∈ term list rep set In1 (Scons (Leaf (Inr b)) xs) ∈ term rep set

In0 arbitrary ∈ term list rep set

x ∈ term rep set xs ∈ term list rep set

In1 (Scons x xs) ∈ term list rep set zu definieren. Aus diesen Einführungsregeln ergibt sich gemäß Abschnitt 2.3.2 die Induktionsregel

∀a. Q_{1} (In0 (Leaf (Inl a)))

∀b, ys. Q_{2} ys ∧ ys ∈ term list rep set ⟹ Q_{1} (In1 (Scons (Leaf (Inr b)) ys))

Q_{2} (In0 arbitrary)

∀y, ys. Q_{1} y ∧ y ∈ term rep set ∧ Q_{2} ys ∧ ys ∈ term list rep set ⟹

Q_{2} (In1 (Scons y ys)) y ∈ term rep set ⟹ Q_{1} y ∧ ys ∈ term rep set ⟹ Q_{2} ys

Allgemeines Verfahren Seien τ_{1}, …, τ_{ξ} alle nichtrekursiven Typen, die in der aufgefalteten Datentypdefinition aus Abschnitt 4.1 vorkommen. Dann sind die repräsentierenden Mengen t_{1} rep set, …, t_{n} rep set der Datentypen (α_{1}, …, α_{h})t_{1}, …, (α_{1}, …, α_{h})t_{n} vom Typ ((τ_{1} + ⋯ + τ_{ξ})item)set, wobei TVars(τ_{i}) ⊆ {α_{1}, …, α_{h}} gilt. Enthält eine Datentypdefinition keine nichtrekursiven Typen, so haben die repräsentierenden Mengen den Typ (unit item)set.

Konstruktion von Injektionen Für die Definition der repräsentierenden Mengen werden die Funktionen

in_{i} :: τ_{i} → τ_{1} + ⋯ + τ_{ξ}
\underline{in}_{i} :: α item → α item

mit den Eigenschaften

i ≠ j ⟹ in_{i} x ≠ in_{j} y x ≠ y ⟹ in_{i} x ≠ in_{i} y

i ≠ j ⟹ \underline{in}_{i} x ≠ \underline{in}_{j} y x ≠ y ⟹ \underline{in}_{i} x ≠ \underline{in}_{i} y

verwendet. Die Injektionen in_{i} werden mit Hilfe der bereits erwähnten Funktionen Inl und Inr konstruiert. Hierbei wird eine relativ effiziente, in [Paulson, 1994] vorgeschlagene Kodierung verwendet. So werden die Injektionen beispielsweise für ξ = 4 nicht durch

in_{1} x ≡ Inl x
in_{2} x ≡ Inr (Inl x)
in_{3} x ≡ Inr (Inr (Inl x))
in_{4} x ≡ Inr (Inr (Inr x))

sondern durch

in_{1} x ≡ Inl (Inl x)
in_{2} x ≡ Inl (Inr x)
in_{3} x ≡ Inr (Inl x)
in_{4} x ≡ Inr (Inr x)

d.h. durch ”balancierte“ Kombination von Inl und Inr dargestellt. Bei ξ Typen beträgt die Schachtelungstiefe der Ausdrücke dabei maximal ⌈log_{2}(ξ)⌉ im Gegensatz zu ξ − 1 bei ”unbalancierter“ Kombination. Dies wirkt sich positiv auf den Platzbedarf und die Laufzeit der Beweise aus. Im obigen Beispiel sind die Funktionen inj_{i} vom Typ

τ_{i} → (τ_{1} + τ_{2}) + (τ_{3} + τ_{4})

wobei die Klammerung zu beachten ist. Für \underline{in}_{i} ist die Konstruktion analog, wobei die Funktionen In0 und In1 anstelle von Inl und Inr verwendet werden.

Einführungsregeln Für die verschränkte induktive Definition der Mengen t_{1} rep set, …, t_{n} rep set wird für jeden Konstruktor der beteiligten Datentypen eine Einführungsregel angegeben. Für einen Konstruktor der Form

C_{i}^{j} … ((α_{1}, …, α_{h})t_{j′}) … τ_{i′} …

gibt man hierbei eine Einführungsregel der Form

x ∈ t_{j′} rep set …
\underline{in}_{i} (⋯ • x • ⋯ • Leaf (in_{i′} x′) • ⋯) ∈ t_{j} rep set

an, wobei x_{1} • x_{2} die Infix-Schreibweise von Scons x_{1} x_{2} ist. Für einen Konstruktor C j̃ ; ĩ ohne Argumente wird die Einführungsregel

\underline{in}ĩ arbitrary ∈ tj̃ rep set

angegeben.

Induktionsregel Für die Mengen t_{1} rep set, …, t_{n} rep set kann nun gemäß Abschnitt 2.3.2 die simultane Induktionsregel

[P_{j′}(x) x ∈ t_{j′} rep set …]_{x,x′,...}
⋮ .
P_{j} (\underline{in}_{i} (⋯ • x • ⋯ • Leaf (in_{i′} x′) • ⋯))

…
y_{1} ∈ t_{1} rep set ⟹ P_{1}(y_{1}) ∧ … ∧ y_{n} ∈ t_{n} rep set ⟹ P_{n}(y_{n})

bewiesen werden.

4.3 Beweis von Isomorphie-Eigenschaften

Sind die repräsentierenden Mengen konstruiert, so werden die neuen Typen durch den in Abschnitt 2.2.3 beschriebenen Typdefinitionsmechanismus eingeführt. Für den Typ (α, β)term werden hierbei die Abstraktions- und Repräsentationsfunktionen

Abs term :: (α + β)item → (α, β)term
Rep term :: (α, β)term → (α + β)item

deklariert und die Axiome

Abs term (Rep term x) = x  (Rep term inverse)
y ∈ term rep set ⟹ Rep term (Abs term y) = y  (Abs term inverse)
Rep term x ∈ term rep set  (Rep term)

eingeführt. Damit ist die Isomorphie zwischen der Menge term rep set und dem neuen Typ (α, β)term ausgedrückt. Auch zwischen term list rep set und ((α, β)term)list besteht eine derartige Isomorphie. Da list kein neu eingeführter Typkonstruktor ist, ergibt sich diese Isomorphie allerdings nicht direkt aus entsprechenden Axiomen, sondern muß explizit nachgewiesen werden. Unser Ziel ist daher die Definition einer geeigneten Repräsentationsfunktion

rep term list :: ((α, β)term)list → (α + β)item

mit den Eigenschaften

inv rep term list (rep term list x) = x

y ∈ term list rep set ⟹ rep term list (inv rep term list y) = y rep term list x ∈ term list rep set

die die gleiche Struktur wie die oben beschriebenen Axiome für term aufweisen. Die zugrundeliegende Idee ist in Abbildung 4.3 veranschaulicht.

[figure: list rep set; term list rep set; ((α, β)term)list; Abs list; Rep list; inv rep term list; rep term list; frühere Definition; neue Definition]

Abbildung 4.3: Isomorphie zwischen term list rep set und ((α, β)term)list

Die ersten beiden Eigenschaften erhält man hierbei mit Hilfe von Standardtheoremen über die Umkehrbarkeit von Funktionen

inj f  ⟹ inv f (f x) = x  (inv f f)
y ∈ range f ⟹ f (inv f y) = y  (f inv f)

wofür die Injektivität von rep term list sowie

y ∈ term list rep set ⟹ y ∈ range rep term list zu zeigen ist. Letzteres besagt, daß für jedes Element y aus der repräsentierenden Menge term list rep set eine Liste x mit y = rep term list x existieren muß, d.h. rep term list ist surjektiv. Die Definition von Repräsentationsfunktionen sowie die Ableitung der entsprechenden Eigenschaften wird nun in den folgenden Abschnitten sowohl am Beispiel der Funktion rep term list als auch allgemein beschrieben.

4.3.1 Definition von Repräsentationsfunktionen

Bei der Definition von rep term list kann man sich die Tatsache zunutze machen, daß für list bereits ein Kombinator list rec für primitive Rekursion definiert wurde. Die primitiv rekursive Funktion rep term list läßt sich durch die Gleichungen

rep term list Nil  = In0 arbitrary
rep term list (Cons x xs) = In1 (Scons (Rep term x) (rep term list xs))

charakterisieren. Im Fall des Konstruktors Cons erhält man hierbei die Repräsentation des Arguments x vom Typ (α, β)term durch die bei der Typdefinition eingeführte Funktion Rep term, während die Repräsentation des Arguments xs vom Typ ((α, β)term)list durch einen rekursiven Aufruf von rep term list ermittelt wird. Wir definieren nun rep term list mit Hilfe von list rec durch

rep term list ≡ list rec (In0 arbitrary) (λx, xs, ys. In1 (Scons (Rep term x) ys))

woraus sich die obigen Gleichungen mit Hilfe der charakteristischen Gleichungen für list rec leicht ableiten lassen.

Bei größerer Verschachtelungstiefe sind mehrere Repräsentationsfunktionen erforderlich. So werden für den Typ term2 die Funktionen

rep term2 list  :: ((α, β)term2)list → (α + β)item
rep term2 list list :: (((α, β)term2)list)list → (α + β)item

mit den charakteristischen Gleichungen

rep term2 list Nil  = In0 arbitrary
rep term2 list (Cons x xs)  = In1 (Scons (Rep term2 x) (rep term2 list xs))
rep term2 list list Nil  = In0 arbitrary
rep term2 list list (Cons x xs) = In1 (Scons (rep term2 list x) (rep term2 list list xs))

benötigt, die sich durch

rep term2 list  ≡ list rec (In0 arbitrary)

(λx, xs, ys. In1 (Scons (Rep term2 x) ys)

rep term2 list list ≡ list rec (In0 arbitrary)

(λx, xs, ys. In1 (Scons (rep term2 list x) ys) definieren lassen. Man beachte, daß hierbei in der Definition der Funktion rep term2 list nur auf Rep term2 und in der Definition von rep term2 list list nur auf rep term2 list zurückgegriffen werden muß.

Allgemeines Verfahren Für die in Abschnitt 4.1 angegebene Datentypdefinition werden Funktionen benötigt, mit denen Elemente der bereits existierenden, verschachtelt rekursiv vorkommenden Typen

(τ̂_{1}^{j}, …, τ̂ j h̃_{1}) t̃_{j} mit ν_{1} ≤ j ≤ n

in Elemente der Menge t_{j} rep set und umgekehrt konvertiert werden können. Mittels primitiver Rekursion definieren wir daher für 1 ≤ μ ≤ n′ jeweils simultan für die Typen

(τ̂_{1}^{ν_{μ}}, …, τ̂ ν_{μ} ; h̃_{μ}) t̃_{ν_{μ}} … (τ̂_{1}^{ν_{μ+1}−1}, …, τ̂ ν_{μ+1}−1 ; h̃_{μ}) t̃_{ν_{μ+1}−1}

die verschränkt rekursiven Funktionen

rep_{ν_{μ}} :: (τ̂_{1}^{ν_{μ}}, …, τ̂ ν_{μ} ; h̃_{μ}) t̃_{ν_{μ}} → (τ_{1} + ⋯ + τ_{ξ})item
⋮
rep_{ν_{μ+1}−1} :: (τ̂_{1}^{ν_{μ+1}−1}, …, τ̂ ν_{μ+1}−1 ; h̃_{μ}) t̃_{ν_{μ+1}−1} → (τ_{1} + ⋯ + τ_{ξ})item

Mit Hilfe der bereits definierten Kombinatoren t̃_{ν_{μ}} rec, …, t̃_{ν_{μ+1}−1} rec für primitive Rekursion lassen sich diese Funktionen durch

rep_{ν_{μ}} ≡ t̃_{ν_{μ}} rec f_{1}^{ν_{μ}} … f_{k_{νμ}}^{ν_{μ}} … f_{1}^{ν_{μ+1}−1} … f_{k_{ν_{μ+1}−1}}^{ν_{μ+1}−1}
⋮
rep_{ν_{μ+1}−1} ≡ t̃_{ν_{μ+1}−1} rec f_{1}^{ν_{μ}} … f_{k_{νμ}}^{ν_{μ}} … f_{1}^{ν_{μ+1}−1} … f_{k_{ν_{μ+1}−1}}^{ν_{μ+1}−1}

ausdrücken, wobei jede Funktion f_{i}^{j} mit einem Konstruktor C_{i}^{j} korrespondiert. Für einen Konstruktor der Form

C_{i}^{j} … (α_{1}, …, α_{h})t_{j′} … (α_{1}, …, α_{h})t_{j′′} … (α_{1}, …, α_{h})t_{j′′′} … τ_{i′} …

mit ν_{μ} ≤ j′ < ν_{μ+1}, ν_{μ+1} ≤ j′′ und 1 ≤ j′′′ < ν_{1} hat f_{i}^{j} hierbei die Gestalt

λx_{1}, …, x′, …, x′′, …, x′′′, …, x_{m_{i}^{j}} , y_{1}, …, y, …, y_{l_{i}^{j}} .
\underline{in}_{i} (⋯ • y • ⋯ • rep_{j′′} x′ • ⋯ • Rep t_{j′′′} x′′ • ⋯ • Leaf (in_{i′} x′′′) • ⋯)

Aus der Definition von rep_{j} läßt sich für den Konstruktor C_{i}^{j} dann die charakteristische Gleichung

rep_{j} (C_{i}^{j} … x … x′ … x′′ … x′′′ …) =
\underline{in}_{i} (⋯ • rep_{j′} x • ⋯ • rep_{j′′} x′ • ⋯ • Rep t_{j′′′} x′′ • ⋯ • Leaf (in_{i′} x′′′) • ⋯)

ableiten. Man beachte, daß bei der Definition von rep_{ν_{μ}}, …, rep_{ν_{μ+1}−1} stets nur auf rep_{j} mit ν_{μ+1} ≤ j oder Rep t_{j} mit 1 ≤ j < ν_{1} zurückgegriffen wird. Bei der folgenden allgemeinen Erläuterung der Beweise von Eigenschaften dieser Repräsentationsfunktionen wird jeweils exemplarisch die Behandlung des Konstruktors C_{i}^{j} beschrieben.

4.3.2 Surjektivität der Repräsentationsfunktionen

Wie eingangs erwähnt, muß für rep term list die Eigenschaft

y ∈ term list rep set ⟹ y ∈ range rep term list

nachgewiesen werden. Dies geschieht mittels simultaner Induktion unter Verwendung der Induktionsregel für die Mengen term rep set und term list rep set. Wir gehen hierbei vom Beweisziel

y′ ∈ term rep set ⟹ True ∧ y ∈ term list rep set ⟹ y ∈ range rep term list

aus. Da für term keine Repräsentationsfunktion definiert werden muß und daher für die Menge term rep set nichts zu zeigen ist, hat das erste Glied der Konjunktion die Form … ⟹ True. Durch Anwendung der Induktionsregel erhalten wir die Beweisziele

(1) … ⟹ True
(2) … ⟹ True
(3) In0 arbitrary ∈ range rep term list
(4) ∀y, ys. y ∈ term rep set ∧ ys ∈ term list rep set ∧ ys ∈ range rep term list ⟹

In1 (Scons y ys) ∈ range rep term list

Die Beweisziele (1) und (2) sind trivial. Aus Beweisziel (3) erhält man mittels (range eqI) das neue Beweisziel

rep term list Nil = In0 arbitrary

was sich sofort mit Hilfe der charakteristischen Gleichungen für rep term list lösen läßt. Durch Anwendung von (rangeE) erhält man aus Beweisziel (4) das neue Beweisziel

∀y, ys, xs. y ∈ term rep set ∧ ys ∈ term list rep set ∧ ys = rep term list xs ⟹ In1 (Scons y ys) ∈ range rep term list

Unter Ausnutzung der Prämisse ys = rep term list xs erhält man hieraus das Beweisziel

∀y, ys, xs. y ∈ term rep set ∧ ys ∈ term list rep set ⟹ In1 (Scons y (rep term list xs)) ∈ range rep term list

Mit Hilfe der Prämisse y ∈ term rep set und dem Axiom (Abs term inverse) ergibt sich

∀y, ys, xs. ys ∈ term list rep set ⟹ In1 (Scons (Rep term (Abs term y)) (rep term list xs)) ∈ range rep term list woraus man mittels (range eqI) das Beweisziel

∀y, ys, xs. ys ∈ term list rep set ⟹ rep term list (Cons (Abs term y) xs) = In1 (Scons (Rep term (Abs term y)) (rep term list xs))

erhält. Dies folgt ebenso sofort aus den charakteristischen Gleichungen für rep term list.

Allgemeines Verfahren Wir zeigen

y_{j} ∈ t_{j} rep set ⟹ y_{j} ∈ range rep_{j}

für ν_{1} ≤ j ≤ n. Der Beweis erfolgt unter Verwendung der simultanen Induktionsregel für die Mengen t_{1} rep set, …, t_{n} rep set. Wir gehen hierbei vom Beweisziel

y_{1} ∈ t_{1} rep set ⟹ True ∧ … ∧ y_{ν_{1}−1} ∈ t_{ν_{1}−1} rep set ⟹ True ∧
y_{ν_{1}} ∈ t_{ν_{1}} rep set ⟹ y_{ν_{1}} ∈ range rep_{ν_{1}} ∧ … ∧ y_{n} ∈ t_{n} rep set ⟹ y_{n} ∈ range rep_{n}

aus. Für die Mengen t_{1} rep set, …, t_{ν_{1}−1} rep set ist nichts zu zeigen, weshalb die ersten Glieder der Konjunktion die Gestalt … ⟹ True haben. Die Anwendung der Induktionsregel ergibt nun die neuen Beweisziele

… ⟹ True
⋮
(⋆) ∀x, x′, x′′, x′′′, …. x ∈ range rep_{j′} ∧ x′ ∈ range rep_{j′′} ∧ x′′ ∈ t_{j′′′} rep set ∧ … ⟹
\underline{in}_{i} (⋯ • x • ⋯ • x′ • ⋯ • x′′ • ⋯ • Leaf (in_{i′} x′′′) • ⋯) ∈ range rep_{j}
⋮

Die Beweisziele der Form … ⟹ True sind trivial. Aus dem Beweisziel (⋆) erhält man durch mehrmalige Anwendung von (rangeE) das Beweisziel

∀x, x′, x′′, x′′′, z, z′, …. x = rep_{j′} z ∧ x′ = rep_{j′′} z′ ∧ x′′ ∈ t_{j′′′} rep set ∧ … ⟹
\underline{in}_{i} (⋯ • x • ⋯ • x′ • ⋯ • x′′ • ⋯ • Leaf (in_{i′} x′′′) • ⋯) ∈ range rep_{j}

woraus man unter Ausnutzung der Prämissen x = rep_{j′} z und x′ = rep_{j′′} z′ das Beweisziel

∀x, x′, x′′, x′′′, z, z′, …. x′′ ∈ t_{j′′′} rep set ∧ … ⟹

\underline{in}_{i} (⋯ • rep_{j′} z • ⋯ • rep_{j′′} z′ • ⋯ • x′′ • ⋯ • Leaf (in_{i′} x′′′) • ⋯) ∈ range rep_{j}

erhält. Unter Verwendung der Prämisse x′′ ∈ t_{j′′′} rep set und des bei der Typdefinition eingeführten Axioms

x′′ ∈ t_{j′′′} rep set ⟹ Rep t_{j′′′} (Abs t_{j′′′} x′′) = x′′ (Abs t_{j′′′} inverse)

ergibt sich hieraus das Beweisziel

∀x, x′, x′′, x′′′, z, z′, . . . . . . . ⟹
\underline{in}_{i} (⋯ • rep_{j′} z • ⋯ • rep_{j′′} z′•
⋯ • Rep t_{j′′′} (Abs t_{j′′′} x′′) • ⋯ • Leaf (in_{i′} x′′′) • ⋯) ∈ range rep_{j}

mittels (range eqI) erhält man schließlich

∀x, x′, x′′, x′′′, z, z′, . . . . . . . ⟹
rep_{j} (C_{i}^{j} … z … z′ … (Abs t_{j′′′} x′′) … x′′′ …) =
\underline{in}_{i} (⋯ • rep_{j′} z • ⋯ • rep_{j′′} z′•
⋯ • Rep t_{j′′′} (Abs t_{j′′′} x′′) • ⋯ • Leaf (in_{i′} x′′′) • ⋯)

was sich mit Hilfe der charakteristischen Gleichungen für rep_{j} lösen läßt.

4.3.3 Injektivität der Repräsentationsfunktionen

Der Nachweis der Injektivität von rep term list erfolgt mit Hilfe der Induktionsregel für list. Hierbei gehen wir vom Beweisziel

∀ys′. rep term list ys = rep term list ys′ ⟹ ys = ys′

aus. Induktion über ys liefert die Beweisziele

(1) ∀ys′. rep term list Nil = rep term list ys′ ⟹ Nil = ys′
(2) ∀x, xs. (∀ys′′. rep term list xs = rep term list ys′′ ⟹ xs = ys′′) ⟹

∀ys′. rep term list (Cons x xs) = rep term list ys′ ⟹ Cons x xs = ys′

Mittels Fallunterscheidung über ys′ erhält man aus (1) die neuen Beweisziele

(3) rep term list Nil = rep term list Nil ⟹ Nil = Nil
(4) ∀z, zs. rep term list Nil = rep term list (Cons z zs) ⟹ Nil = Cons z zs

Hierbei läßt sich (3) unmittelbar durch Reflexivität lösen. Aus (4) erhält man mit Hilfe der charakteristischen Gleichungen für rep term list das Beweisziel

∀z, zs. In0 arbitrary = In1 (Scons (Rep term z) (rep term list zs)) ⟹ Nil = Cons z zs

was wegen In0 … ≠ In1 … trivial lösbar ist. Ebenfalls mittels Fallunterscheidung über ys′ erhält man aus (2) die Beweisziele

∀x, xs. (∀ys′′. rep term list xs = rep term list ys′′ ⟹ xs = ys′′) ∧

rep term list (Cons x xs) = rep term list Nil ⟹ Cons x xs = Nil

∀x, xs, z, zs. (∀ys′′. rep term list xs = rep term list ys′′ ⟹ xs = ys′′) ∧ rep term list (Cons x xs) = rep term list (Cons z zs) ⟹

Cons x xs = Cons z zs Mit Hilfe der charakteristischen Gleichungen für rep term list erhält man hieraus die Beweisziele

(5) ∀x, xs. (∀ys′′. rep term list xs = rep term list ys′′ ⟹ xs = ys′′) ∧

In1 (Scons (Rep term x) (rep term list xs)) = In0 arbitrary ⟹ Cons x xs = Nil

(6) ∀x, xs, z, zs. (∀ys′′. rep term list xs = rep term list ys′′ ⟹ xs = ys′′) ∧

In1 (Scons (Rep term x) (rep term list xs)) = In1 (Scons (Rep term z) (rep term list zs)) ⟹

Cons x xs = Cons z zs

Beweisziel (5) ist wegen In1 … ≠ In0 … wieder trivial lösbar. Aus der Prämisse

In1 (Scons (Rep term x) (rep term list xs)) = In1 (Scons (Rep term z) (rep term list zs))

von Beweisziel (6) erhält man aufgrund der Injektivität von In1 und Scons, sowie der aus dem Axiom (Rep term inverse) folgerbaren Injektivität von Rep term die Gleichungen x = z sowie rep term list xs = rep term list zs, woraus sich mit Hilfe der Prämisse

∀ys′′. rep term list xs = rep term list ys′′ ⟹ xs = ys′′

schließlich noch xs = zs folgern läßt. Damit ist auch Beweisziel (6) gelöst.

Bei verschachtelt rekursiven Datentypdefinitionen mit größerer Verschachtelungstiefe müssen die Eigenschaften der Repräsentationsfunktionen für die zuletzt aufgefalteten, also in der Verschachtelung am weitesten innen liegenden Typen als erstes gezeigt werden. So muß z.B. zuerst die Injektivität von rep term2 list und dann die Injektivität von rep term2 list list bewiesen werden, da für letzteres die Injektivität von rep term2 list benötigt wird.

Allgemeines Verfahren Wir zeigen die Injektivität der Funktionen rep_{j} für ν_{1} ≤ j ≤ n. Für alle 1 ≤ μ ≤ n′ wird dies jeweils mit simultaner Induktion für die Funktionen rep_{ν_{μ}}, …, rep_{ν_{μ+1}−1} gezeigt. Da hierbei außer der Injektivität von Rep t_{j} für 1 ≤ j < ν_{1} auch die Injektivität von rep_{j} für ν_{μ+1} ≤ j ≤ n benötigt wird, muß mit μ = n′ begonnen werden.

Wir gehen vom Beweisziel

∀y′. rep_{ν_{μ}} y_{ν_{μ}} = rep_{ν_{μ}} y′ ⟹ y_{ν_{μ}} = y′ ∧ … ∧
∀y′. rep_{j} y_{j} = rep_{j} y′ ⟹ y_{j} = y′ ∧ … ∧
∀y′. rep_{ν_{μ+1}−1} y_{ν_{μ+1}−1} = rep_{ν_{μ+1}−1} y′ ⟹ y_{ν_{μ+1}−1} = y′

KAPITEL 4. KONSTRUKTION VON DATENTYPEN IN HOL 51 aus. Simultane Induktion über y_{ν_{μ}}, …, y_{ν_{μ+1}−1} liefert die Beweisziele

… ⟹ ∀y′. rep_{ν_{μ}} (C_{1}^{ν_{μ}} …) = rep_{ν_{μ}} y′ ⟹ C_{1}^{ν_{μ}} … = y′

⋮
… ⟹ ∀y′. rep_{ν_{μ}} (C_{k_{νμ}}^{ν_{μ}} …) = rep_{ν_{μ}} y′ ⟹ C_{k_{νμ}}^{ν_{μ}} … = y′
⋮
(⋆) ∀x, x′, x′′, x′′′, …. (∀y′′. rep_{j′} x = rep_{j′} y′′ ⟹ x = y′′) ∧ … ⟹
∀y′. rep_{j} (C_{i}^{j} … x … x′ … x′′ … x′′′ …) = rep_{j} y′ ⟹
C_{i}^{j} … x … x′ … x′′ … x′′′ … = y′
⋮
… ⟹ ∀y′. rep_{ν_{μ+1}−1} (C_{1}^{ν_{μ+1}−1} …) = rep_{ν_{μ+1}−1} y′ ⟹ C_{1}^{ν_{μ+1}−1} … = y′
⋮
… ⟹ ∀y′. rep_{ν_{μ+1}−1} (C_{k_{ν_{μ+1}−1}}^{ν_{μ+1}−1} …) = rep_{ν_{μ+1}−1} y′ ⟹ C_{k_{ν_{μ+1}−1}}^{ν_{μ+1}−1} … = y′

Mittels Fallunterscheidung über y′ erhält man aus dem Beweisziel (⋆) die neuen Beweisziele

∀ …. rep_{j} (C_{i}^{j} …) = rep_{j} (C_{1}^{j} …) ⟹ …

⋮
∀x, x′, x′′, x′′′, x̂, x̂′, x̂′′, x̂′′′, …. (∀y′′. rep_{j′} x = rep_{j′} y′′ ⟹ x = y′′)∧
rep_{j} (C_{i}^{j} … x … x′ … x′′ … x′′′ …) =
rep_{j} (C_{i}^{j} … x̂ … x̂′ … x̂′′ … x̂′′′ …) ∧ … ⟹

C_{i}^{j} … x … x′ … x′′ … x′′′ … = C_{i}^{j} … x̂ … x̂′ … x̂′′ … x̂′′′ …

⋮
∀ …. rep_{j} (C_{i}^{j} …) = rep_{j} (C_{k_{j}}^{j} …) ⟹ …

woraus sich nach Anwendung der charakteristischen Gleichungen für rep_{j} die Beweisziele

∀ …. \underline{in}_{i} … = \underline{in}_{1} … ⟹ …

⋮
(⋆⋆) ∀x, x′, x′′, x′′′, x̂, x̂′, x̂′′, x̂′′′, …. (∀y′′. rep_{j′} x = rep_{j′} y′′ ⟹ x = y′′)∧
\underline{in}_{i} (⋯ • rep_{j′} x • ⋯ • rep_{j′′} x′•
⋯ • Rep t_{j′′′} x′′ • ⋯ • Leaf (in_{i′} x′′′) • ⋯) =
\underline{in}_{i} (⋯ • rep_{j′} x̂ • ⋯ • rep_{j′′} x̂′•
⋯ • Rep t_{j′′′} x̂′′ • ⋯ • Leaf (in_{i′} x̂′′′) • ⋯) ∧ … ⟹
C_{i}^{j} … x … x′ … x′′ … x′′′ … =
C_{i}^{j} … x̂ … x̂′ … x̂′′ … x̂′′′ …
⋮
∀ …. \underline{in}_{i} … = \underline{in}_{k_{j}} … ⟹ …

ergeben. Alle Beweisziele bis auf (⋆⋆) sind wegen der Verschiedenheit der Injektionen trivial lösbar. Aufgrund der Injektivität von \underline{in}_{i}, in_{i′}, • bzw. Scons und Leaf, der Prämisse bzw.

Induktionsvoraussetzung ∀y′′. rep_{j′} x = rep_{j′} y′′ ⟹ x = y′′, der wegen ν_{μ+1} ≤ j′′ bereits bewiesenen Injektivität von rep_{j′′} sowie der aus dem Axiom (Rep t_{j′′′} inverse) folgerbaren Injektivität von Rep t_{j′′′} erhält man aus (⋆⋆) schließlich das Beweisziel

∀x, x′, x′′, x′′′, x̂, x̂′, x̂′′, x̂′′′, …. x = x̂ ∧ x′ = x̂′ ∧ x′′ = x̂′′ ∧ x′′′ = x̂′′′ ∧ … ⟹
C_{i}^{j} … x … x′ … x′′ … x′′′ … =
C_{i}^{j} … x̂ … x̂′ … x̂′′ … x̂′′′ …

was sich nach Verwendung der Prämissen x = x̂, … mittels Reflexivität lösen läßt.

4.3.4 Wertebereich der Repräsentationsfunktionen

Es muß nun noch nachgewiesen werden, daß die Funktion rep term list für alle Argumente stets ein Element aus term list rep set liefert. Der Beweis erfolgt ebenfalls wieder mit Hilfe der Induktionsregel für list, wobei wir vom Beweisziel

rep term list y ∈ term list rep set

ausgehen. Induktion über y liefert die Beweisziele

rep term list Nil ∈ term list rep set

∀x, xs. rep term list xs ∈ term list rep set ⟹ rep term list (Cons x xs) ∈ term list rep set

Durch Anwendung der charakteristischen Gleichungen für die Funktion rep term list erhält man

(1) In0 arbitrary ∈ term list rep set
(2) ∀x, xs. rep term list xs ∈ term list rep set ⟹

In1 (Scons (Rep term x) (rep term list xs)) ∈ term list rep set

Beweisziel (1) folgt hierbei sofort aus der entsprechenden Einführungsregel für die Menge term list rep set. Ebenso kann Beweisziel (2) unter Verwendung der Prämisse rep term list xs ∈ term list rep set sowie dem Axiom (Rep term) mit Hilfe einer geeigneten Einführungsregel gelöst werden.

Allgemeines Verfahren Wir zeigen rep_{j} y_{j} ∈ t_{j} rep set für ν_{1} ≤ j ≤ n, wobei analog zum Beweis der Injektivität simultane Induktion verwendet wird. Wir gehen hierbei vom Beweisziel

rep_{ν_{μ}} y_{ν_{μ}} ∈ t_{ν_{μ}} rep set ∧ … ∧ rep_{ν_{μ+1}−1} y_{ν_{μ+1}−1} ∈ t_{ν_{μ+1}−1} rep set

aus. Simultane Induktion über y_{ν_{μ}}, …, y_{ν_{μ+1}−1} liefert die Beweisziele

… ⟹ rep_{ν_{μ}} (C_{1}^{ν_{μ}} …) ∈ t_{ν_{μ}} rep set
⋮
… ⟹ rep_{ν_{μ}} (C_{k_{νμ}}^{ν_{μ}} …) ∈ t_{ν_{μ}} rep set
⋮
(⋆) ∀x, x′, x′′, x′′′, …. rep_{j′} x ∈ t_{j′} rep set ∧ … ⟹
rep_{j} (C_{i}^{j} … x … x′ … x′′ … x′′′ …) ∈ t_{j} rep set
⋮
… ⟹ rep_{ν_{μ+1}−1} (C_{1}^{ν_{μ+1}−1} …) ∈ t_{ν_{μ+1}−1} rep set
⋮
… ⟹ rep_{ν_{μ+1}−1} (C_{k_{ν_{μ+1}−1}}^{ν_{μ+1}−1} …) ∈ t_{ν_{μ+1}−1} rep set

Aus (⋆) erhält man durch Anwendung der charakteristischen Gleichungen für rep_{j} das Beweisziel

∀x, x′, x′′, x′′′, …. rep_{j′} x ∈ t_{j′} rep set ∧ … ⟹
\underline{in}_{i} (⋯ • rep_{j′} x • ⋯ • rep_{j′′} x′•
⋯ • Rep t_{j′′′} x′′ • ⋯ • Leaf (in_{i′} x′′′) • ⋯) ∈ t_{j} rep set

Unter Verwendung der entsprechenden Einführungsregel für die Menge t_{j} rep set erhält man hieraus die Beweisziele

∀x, x′, x′′, x′′′, …. rep_{j′} x ∈ t_{j′} rep set ∧ … ⟹ rep_{j′} x ∈ t_{j′} rep set
… ⟹ rep_{j′′} x′ ∈ t_{j′′} rep set
… ⟹ Rep t_{j′′′} x′′ ∈ t_{j′′′} rep set
⋮

die sich mit Hilfe der Prämisse bzw. Induktionsvoraussetzung rep_{j′} x ∈ t_{j′} rep set, des wegen ν_{μ+1} ≤ j′′ bereits bewiesenen Theorems rep_{j′′} x′ ∈ t_{j′′} rep set und des Axioms (Rep t_{j′′′}) lösen lassen.

4.3.5 Umkehrung der Repräsentationsfunktionen

Mit Hilfe der Theoreme

inj f  ⟹ inv f (f x) = x  (inv f f)
y ∈ range f ⟹ f (inv f y) = y  (f inv f)

erhält man aus den soeben bewiesenen Eigenschaften von rep_{j} die Theoreme

inv rep_{j} (rep_{j} x) = x

y ∈ t_{j} rep set ⟹ rep_{j} (inv rep_{j} y) = y für ν_{1} ≤ j ≤ n. Zusammen mit

rep_{j} x ∈ t_{j} rep set

steht also auch für die zu bereits existierenden Typen isomorphen Mengen t_{ν_{1}} rep set, …, t_{n} rep set der gleiche Satz von Theoremen wie für die repräsentierenden Mengen der neu eingeführten Typen zur Verfügung.

4.4 Definition der Konstruktoren

Unter Verwendung der Abstraktions- und Repräsentationsfunktionen können nun für den Datentyp (α, β)term die Konstruktoren Var und App durch

Var :: α → (α, β)term
Var a ≡ Abs term (In0 (Leaf (Inl a)))
App :: β → ((α, β)term)list → (α, β)term
App b ts ≡ Abs term (In1 (Scons (Leaf (Inr b)) (rep term list ts)))

definiert werden

Allgemeines Verfahren Für die neu eingeführten Typen definieren wir die Konstruktoren C_{1}^{1}, …, C_{k_{1}}^{1}, …, C_{1}^{ν_{1}−1}, …, C_{k_{ν_{1}−1}}^{ν_{1}−1}. Ein Konstruktor der Gestalt

C_{i}^{j} … (α_{1}, …, α_{h})t_{j′} … (α_{1}, …, α_{h})t_{j′′} … τ_{i′} …

mit 1 ≤ j′ < ν_{1} und ν_{1} ≤ j′′ wird hierbei durch

C_{i}^{j} … x … x′ … x′′ … ≡
Abs t_{j} (\underline{in}_{i} (⋯ • Rep t_{j′} x • ⋯ • rep_{j′′} x′ • ⋯ • Leaf (in_{i′′} x′′) • ⋯))

definiert. Für einen Konstruktor C j̃ ; ĩ ohne Argumente lautet die Definition

C j̃ ; ĩ ≡ \underline{in}ĩ arbitrary

4.5 Repräsentationsabhängige Beweise

4.5.1 Verschiedenheit von Konstruktoren

Da die Anzahl von Ungleichungen der Form

C_{i}^{j} … ≠ C_{i′}^{j} … für i ≠ i′

quadratisch mit der Anzahl der Konstruktoren steigt, werden stattdessen Gleichungen der Form

Rep t_{j} (C_{i}^{j} …) = \underline{in}_{i} …

bewiesen. Mit Hilfe des Theorems

Rep t_{j} (C_{i}^{j} …) ≠ Rep t_{j} (C_{i′}^{j} …) ⟹ C_{i}^{j} … ≠ C_{i′}^{j} …

das man durch Kontraposition aus der Kongruenzregel für Funktionen erhält, läßt sich somit die Verschiedenheit von C_{i}^{j} und C_{i′}^{j} auf die Verschiedenheit von \underline{in}_{i} und \underline{in}_{i′} zurückführen, die sich aufgrund der in Abschnitt 4.2 erläuterten Konstruktion der Injektionen in maximal ⌈log_{2}(k_{j} )⌉ Schritten zeigen läßt, wobei k_{j} die Anzahl der Konstruktoren des Datentyps ist.

Im Fall des in Abschnitt 4.4 angegebenen Konstruktors C_{i}^{j} gehen wir vom Beweisziel

Rep t_{j} (C_{i}^{j} … x … x′ … x′′ …) =
\underline{in}_{i}(⋯ • Rep t_{j′} x • ⋯ • rep_{j′′} x′ • ⋯ • Leaf (in_{i′′} x′′) • ⋯)

aus. Mit Hilfe der Regel

inj on f S f a = f b a ∈ S b ∈ S

a = b

(inj onD)

und der Injektivität von Abs t_{j} auf t_{j} rep set erhält man hieraus die neuen Beweisziele

(1) Abs t_{j} (Rep t_{j} (C_{i}^{j} … x … x′ … x′′ …)) =
Abs t_{j} (\underline{in}_{i} (⋯ • Rep t_{j′} x • ⋯ • rep_{j′′} x′ • ⋯ • Leaf (in_{i′′} x′′) • ⋯))
(2) Rep t_{j} (C_{i}^{j} … x … x′ … x′′ …) ∈ t_{j} rep set
(3) \underline{in}_{i} (⋯ • Rep t_{j′} x • ⋯ • rep_{j′′} x′ • ⋯ • Leaf (in_{i′′} x′′) • ⋯) ∈ t_{j} rep set

Beweisziel (1) kann mit Hilfe des Axioms (Rep t_{j} inverse), der Definition des Konstruktors C_{i}^{j} und Reflexivität gelöst werden, Beweisziel (2) mit Hilfe des Axioms (Rep t_{j} ). Beweisziel (3) wird schließlich durch Anwendung der entsprechenden Einführungsregel für die Menge t_{j} rep set mit anschließender Anwendung des Axioms (Rep t_{j′}) und des in Abschnitt 4.3 bewiesenen Theorems rep_{j′′} x′ ∈ t_{j′′} rep set gezeigt.

4.5.2 Injektivität von Konstruktoren

Beim Beweis der Injektivität des Konstruktors C_{i}^{j} gehen wir vom Beweisziel

C_{i}^{j} … x … x′ … x′′ … = C_{i}^{j} … y … y′ … y′′ … ⟹
x = y ∧ x′ = y′ ∧ x′′ = y′′ ∧ …

aus. Durch Anwendung der Kongruenzregel für Funktionen erhalten wir

Rep t_{j} (C_{i}^{j} … x … x′ … x′′ …) = Rep t_{j} (C_{i}^{j} … y … y′ … y′′ …) ⟹
x = y ∧ x′ = y′ ∧ x′′ = y′′ ∧ …

woraus sich mit Hilfe der in Abschnitt 4.5.1 bewiesenen Regeln

\underline{in}_{i}(⋯ • Rep t_{j′} x • ⋯ • rep_{j′′} x′ • ⋯ • Leaf (in_{i′′} x′′) • ⋯) =

\underline{in}_{i}(⋯ • Rep t_{j′} y • ⋯ • rep_{j′′} y′ • ⋯ • Leaf (in_{i′′} y′′) • ⋯) ⟹ x = y ∧ x′ = y′ ∧ x′′ = y′′ ∧ …

ergibt. Dieses Beweisziel läßt sich mit Hilfe der Injektivität von \underline{in}_{i}, in_{i′′} und Leaf, der aus dem Axiom (Rep t_{j′} inverse) folgerbaren Injektivität von Rep t_{j′} sowie der in Abschnitt 4.3 bewiesenen Injektivität von rep_{j′′} lösen. Die andere Richtung

x = y ∧ x′ = y′ ∧ x′′ = y′′ ∧ … ⟹ C_{i}^{j} … x … x′ … x′′ … = C_{i}^{j} … y … y′ … y′′ …

ist trivial.

4.5.3 Strukturelle Induktion

Mit Hilfe der in Abschnitt 4.3 bewiesenen Isomorphie-Eigenschaften können wir aus der konkreten Induktionsregel

∀a. Q_{1} (In0 (Leaf (Inl a)))

∀b, ys. Q_{2} ys ∧ ys ∈ term list rep set ⟹ Q_{1} (In1 (Scons (Leaf (Inr b)) ys))

Q_{2} (In0 arbitrary)

∀y, ys. Q_{1} y ∧ y ∈ term rep set ∧ Q_{2} ys ∧ ys ∈ term list rep set ⟹

Q_{2} (In1 (Scons y ys))

y ∈ term rep set ⟹ Q_{1} y ∧ ys ∈ term rep set ⟹ Q_{2} ys

für die Mengen term rep set und term list rep set die abstrakte Induktionsregel

∀a.  P_{1} (Var a)
∀b, ts. P_{2} ts  ⟹ P_{1} (App b ts)
P_{2} Nil
∀t, ts. P_{1} t ∧ P_{2} ts ⟹ P_{2} (Cons t ts)
P_{1} t ∧ P_{2} ts

für die Typen (α, β)term und ((α, β)term)list herleiten. Hierfür zeigen wir unter den Voraussetzungen

(i) ∀a. P_{1} (Var a)
(ii) ∀b, ts. P_{2} ts ⟹ P_{1} (App b ts)
(iii) P_{2} Nil
(iv) ∀t, ts. P_{1} t ∧ P_{2} ts ⟹ P_{2} (Cons t ts)

das Beweisziel

P_{1} t ∧ P_{2} ts Mit Hilfe der Axiome (Rep term inverse) und (Rep term) sowie der in Abschnitt 4.3 bewiesenen Theoreme

inv rep term list (rep term list ts) = ts (iso1)

und rep term list ts ∈ term list rep set erhalten wir hieraus das Beweisziel

Rep term t ∈ term rep set ⟹ P_{1} (Abs term (Rep term t)) ∧

rep term list ts ∈ term list rep set ⟹ P_{2} (inv rep term list (rep term list ts))

Nun kann die Induktionsregel für die Mengen term rep set und term list rep set angewendet werden, wobei Q_{1} = P_{1} ∘ Abs term, Q_{2} = P_{2} ∘ inv rep term list und y = Rep term t, ys = rep term list ts. Man erhält somit die Beweisziele

(1) ∀a. P_{1} (Abs term (In0 (Leaf (Inl a))))
(2) ∀b, ys. P_{2} (inv rep term list ys) ∧ ys ∈ term list rep set ⟹

P_{1} (Abs term (In1 (Scons (Leaf (Inr b)) ys)))

(3) P_{2} (inv rep term list (In0 arbitrary))
(4) ∀y, ys. P_{1} (Abs term y) ∧ y ∈ term rep set ∧

P_{2} (inv rep term list ys) ∧ ys ∈ term list rep set ⟹ P_{2} (inv rep term list (In1 (Scons y ys)))

Mit Hilfe der Definition des Konstruktors Var erhält man aus (1) das Beweisziel ∀a. P_{1} (Var a) was sofort aus Voraussetzung (i) folgt. Aus (2) erhält man aufgrund der Prämisse ys ∈ term list rep set und des Theorems

ys ∈ term list rep set ⟹ rep term list (inv rep term list ys) = ys (iso2)

aus Abschnitt 4.3 das neue Beweisziel

∀b, ys. P_{2} (inv rep term list ys) ⟹ P_{1} (Abs term (In1 (Scons (Leaf (Inr b)) (rep term list (inv rep term list ys)))))

Aufgrund der Definition des Konstruktors App ergibt sich hieraus das Beweisziel

∀b, ys. P_{2} (inv rep term list ys) ⟹ P_{1} (App b (inv rep term list ys))

was sich mit Hilfe von Voraussetzung (ii) lösen läßt. Aus (3) ergibt sich unter Verwendung der charakteristischen Gleichungen für rep term list das Beweisziel

P_{2} (inv rep term list (rep term list Nil))

Wegen (iso1) ist dies gleichbedeutend mit P_{2} Nil, was wieder direkt aus Voraussetzung (iii) folgt. Aus (4) erhält man unter Verwendung der Prämisse y ∈ term rep set in Verbindung mit dem Axiom (Abs term inverse) sowie der Prämisse ys ∈ term list rep set in Verbindung mit dem Theorem (iso2) das Beweisziel

∀y, ys. P_{1} (Abs term y) ∧ P_{2} (inv rep term list ys) ⟹

P_{2} (inv rep term list (In1 (Scons (Rep term (Abs term y))

(rep term list (inv rep term list ys)))))

Unter Verwendung der charakteristischen Gleichungen für rep term list ergibt sich das Beweisziel

∀y, ys. P_{1} (Abs term y) ∧ P_{2} (inv rep term list ys) ⟹ P_{2} (inv rep term list (rep term list (Cons (Abs term y) (inv rep term list ys))))

Wegen (iso1) ist dies gleichbedeutend mit

∀y, ys. P_{1} (Abs term y) ∧ P_{2} (inv rep term list ys) ⟹ P_{2} (Cons (Abs term y) (inv rep term list ys))

was sich mit Hilfe von Voraussetzung (iv) lösen läßt.

Allgemeines Verfahren Für die abstrakte Erläuterung des Beweises der strukturellen Induktionsregel wollen wir annehmen, daß die aufgefaltete Datentypdefinition aus Abschnitt 4.1 die zwei Konstruktoren C_{i}^{j} mit 1 ≤ j < ν_{1} und 1 ≤ i ≤ k_{j} sowie C j̃ ; ĩ mit ν_{1} ≤ j̃ ≤ n und 1 ≤ ĩ ≤ kj̃ enthält. C_{i}^{j} ist also ein Konstruktor eines neuen Datentyps, während C j̃ ; ĩ ein Konstruktor eines bereits existierenden Datentyps ist. Diese Konstruktoren seien von der Gestalt

C_{i}^{j} … (α_{1}, …, α_{h})t_{j′} … (α_{1}, …, α_{h})t_{j′′} … τ_{i′} …

C j̃ ; ĩ … (α_{1}, …, α_{h})t_{}_{j̃′} … (α_{1}, …, α_{h})t_{}_{j̃′′} … τ_{}_{ĩ′} …

wobei 1 ≤ j′, j̃′ < ν_{1} und ν_{1} ≤ j′′, j̃′′ ≤ n. Die konkrete Induktionsregel für die repräsentierenden Mengen hat die Gestalt

… ⟹ Q_{1} (\underline{in}_{1} …)
⋮
… ⟹ Q_{1} (\underline{in}_{k_{1}} …)
⋮
∀y, y′, y′′, …. Q_{j′} y ∧ y ∈ t_{j′} rep set ∧ Q_{j′′} y′ ∧ y′ ∈ t_{j′′} rep set ∧ … ⟹
Q_{j} (\underline{in}_{i} (⋯ • y • ⋯ • y′ • ⋯ • Leaf (in_{i′} y′′) • ⋯))
⋮
∀y, y′, y′′, …. Q_{}_{j̃′} y ∧ y ∈ t_{}_{j̃′} rep set ∧ Q_{}_{j̃′′} y′ ∧ y′ ∈ t_{}_{j̃′′} rep set ∧ … ⟹
Qj̃ (\underline{in}ĩ (⋯ • y • ⋯ • y′ • ⋯ • Leaf (in_{}_{ĩ′} y′′) • ⋯))
⋮
… ⟹ Q_{n} (\underline{in}_{1} …)
⋮
… ⟹ Q_{n} (\underline{in}_{k_{n}} …)
y_{1} ∈ t_{1} rep set ⟹ Q_{1} y_{1} ∧ … ∧ y_{n} ∈ t_{n} rep set ⟹ Q_{n} y_{n}

Die zu beweisende, abstrakte Induktionsregel hat die Gestalt

⋮
∀x, x′, x′′, …. P_{j′} x ∧ P_{j′′} x′ ∧ … ⟹ P_{j} (C_{i}^{j} … x … x′ … x′′ …)
⋮
∀x, x′, x′′, …. P_{}_{j̃′} x ∧ P_{}_{j̃′′} x′ ∧ … ⟹ Pj̃(C j̃ ; ĩ … x … x′ … x′′ …)
⋮
P_{1} x_{1} ∧ … ∧ P_{ν_{1}−1} x_{ν_{1}−1} ∧ P_{ν_{1}} x_{ν_{1}} ∧ … ∧ P_{n} x_{n}

Unter den Voraussetzungen

∀x, x′, x′′, …. P_{j′} x ∧ P_{j′′} x′ ∧ … ⟹ P_{j} (C_{i}^{j} … x … x′ … x′′ …)

∀x, x′, x′′, …. P_{}_{j̃′} x ∧ P_{}_{j̃′′} x′ ∧ … ⟹ Pj̃(C j̃ ; ĩ … x … x′ … x′′ …)

⋮

zeigen wir nun

P_{1} x_{1} ∧ … ∧ P_{ν_{1}−1} x_{ν_{1}−1} ∧ P_{ν_{1}} x_{ν_{1}} ∧ … ∧ P_{n} x_{n}

Aus diesem Beweisziel erhält man mit Hilfe der Axiome (Rep t_{μ} inverse) und (Rep t_{μ}) sowie der in Abschnitt 4.3 bewiesenen Theoreme inv rep_{μ′} (rep_{μ′} x) = x und rep_{μ′} x ∈ t_{μ′} rep set das neue Beweisziel

Rep t_{1} x_{1} ∈ t_{1} rep set ⟹ P_{1} (Abs t_{1} (Rep t_{1} x_{1})) ∧ … ∧
Rep t_{ν_{1}−1} x_{ν_{1}−1} ∈ t_{ν_{1}−1} rep set ⟹ P_{ν_{1}−1} (Abs t_{ν_{1}−1} (Rep t_{ν_{1}−1} x_{ν_{1}−1}))∧
rep_{ν_{1}} x_{ν_{1}} ∈ t_{ν_{1}} rep set ⟹ P_{ν_{1}} (inv rep_{ν_{1}} (rep_{ν_{1}} x_{ν_{1}})) ∧ … ∧
rep_{n} x_{n} ∈ t_{n} rep set ⟹ P_{n} (inv rep_{n} (rep_{n} x_{n}))

Nun kann die konkrete Induktionsregel für die repräsentierenden Mengen angewendet werden, wobei Q_{1} = P_{1} ∘ Abs t_{1}, …, Q_{n} = P_{n} ∘ inv rep_{n} und y_{1} = Rep t_{1} x_{1}, …, y_{n} = rep_{n} x_{1}. Dies liefert die Beweisziele

⋮
(⋆) ∀y, y′, y′′, …. P_{j′} (Abs t_{j′} y) ∧ y ∈ t_{j′} rep set ∧
P_{j′′} (inv rep_{j′′} y′) ∧ y′ ∈ t_{j′′} rep set ∧ … ⟹
P_{j} (Abs t_{j} (\underline{in}_{i} (⋯ • y • ⋯ • y′ • ⋯ • Leaf (in_{i′} y′′) • ⋯)))
⋮
(⋆⋆) ∀y, y′, y′′, …. P_{}_{j̃′} (Abs t_{}_{j̃′} y) ∧ y ∈ t_{}_{j̃′} rep set ∧
P_{}_{j̃′′} (inv rep_{}_{j̃′′} y′) ∧ y′ ∈ t_{}_{j̃′′} rep set ∧ … ⟹
Pj̃ (inv repj̃ (\underline{in}ĩ (⋯ • y • ⋯ • y′ • ⋯ • Leaf (in_{}_{ĩ′} y′′) • ⋯)))
⋮

Aus (⋆) erhält man mittels (Abs t_{j′} inverse) in Verbindung mit der Prämisse y ∈ t_{j′} rep set, sowie dem Theorem

y′ ∈ t_{j′′} rep set ⟹ rep_{j′′} (inv rep_{j′′} y′) = y′

aus Abschnitt 4.3 in Verbindung mit der Prämisse y′ ∈ t_{j′′} rep set das Beweisziel

∀y, y′, y′′, …. P_{j′} (Abs t_{j′} y) ∧ P_{j′′} (inv rep_{j′′} y′) ∧ … ⟹
P_{j} (Abs t_{j} (\underline{in}_{i} (⋯ • Rep t_{j′} (Abs t_{j′} y) • ⋯ • rep_{j′′} (inv rep_{j′′} y′)•
⋯ • Leaf (in_{i′} y′′) • ⋯)))

Die Anwendung der Definition von C_{i}^{j} ergibt nun

∀y, y′, y′′, …. P_{j′} (Abs t_{j′} y) ∧ P_{j′′} (inv rep_{j′′} y′) ∧ … ⟹
P_{j} (C_{i}^{j} … (Abs t_{j′} y) … (inv rep_{j′′} y′) … y′′ …)

was sich mit Hilfe der Voraussetzungen lösen läßt. In ähnlicher Weise erhält man aus (⋆⋆) das Beweisziel

∀y, y′, y′′, …. P_{}_{j̃′} (Abs t_{}_{j̃′} y) ∧ P_{}_{j̃′′} (inv rep_{}_{j̃′′} y′) ∧ … ⟹
Pj̃ (inv repj̃ (\underline{in}ĩ (⋯ • Rep t_{}_{j̃′} (Abs t_{}_{j̃′} y) • ⋯ • rep_{}_{j̃′′} (inv rep_{}_{j̃′′} y′)•
⋯ • Leaf (in_{}_{ĩ′} y′′) • ⋯)))

Mit Hilfe der charakteristischen Gleichungen für repj̃ erhält man

∀y, y′, y′′, …. P_{}_{j̃′} (Abs t_{}_{j̃′} y) ∧ P_{}_{j̃′′} (inv rep_{}_{j̃′′} y′) ∧ … ⟹
Pj̃ (inv repj̃ (repj̃ (C j̃ ; ĩ … (Abs t_{}_{j̃′} y) … (inv rep_{}_{j̃′′} y′) … y′′ …)))

Wegen inv repj̃ (repj̃ x) = x ergibt sich hieraus nun das Beweisziel

∀y, y′, y′′, …. P_{}_{j̃′} (Abs t_{}_{j̃′} y) ∧ P_{}_{j̃′′} (inv rep_{}_{j̃′′} y′) ∧ … ⟹

Pj̃ (C j̃ ; ĩ … (Abs t_{}_{j̃′} y) … (inv rep_{}_{j̃′′} y′) … y′′ …)

das ebenfalls mit Hilfe der Voraussetzungen gelöst werden kann.

4.6 Repräsentationsunabhängige Beweise

Sind die elementaren Eigenschaften eines Datentyps wie Verschiedenheit und Injektivität von Konstruktoren sowie strukturelle Induktion einmal bewiesen, so können, wie im folgenden beschrieben wird, alle anderen Eigenschaften wie z.B. die Existenz eines Kombinators für primitive Rekursion daraus abgeleitet werden. Dieser Sachverhalt ermöglicht es auch, in Isabelle/HOL manuell konstruierte Typen wie α×β oder α+β, die alle elementaren Eigenschaften eines Datentyps besitzen, nachträglich als Datentyp zu deklarieren. Derartige Typen können somit insbesondere auch in verschachtelt rekursiven Datentypen wie

datatype (α, β)test = C α
| D (((α, β)test + β)list)

verwendet werden. Die Repräsentationsfunktion für den Typ (α, β)test+β wird hierbei, wie in Abschnitt 4.3 beschrieben, mit Hilfe eines Kombinators für primitive Rekursion konstruiert, dessen Existenz sich aus der Injektivität und Verschiedenheit der Konstruktoren Inl und Inr sowie der – etwas degenerierten – Induktionsregel

∀x. P (Inl x) ∀x. P (Inr x)

P s

ergibt.

4.6.1 Fallunterscheidung

Für 1 ≤ j < ν_{1} erhält man aus der strukturellen Induktionsregel

⋮
∀x_{1}, …, x_{m_{1}^{j}}…. ⟹ P_{j} (C_{1}^{j} x_{1} … x_{m_{1}^{j}})
⋮
∀x_{1}, …, x_{m_{k_{j}}^{j}} …. ⟹ P_{j} (C_{k_{j}}^{j} x_{1} … x_{m_{k_{j}}^{j}} )
⋮
P_{1} x_{1} ∧ … ∧ P_{ν_{1}−1} x_{ν_{1}−1} ∧ P_{ν_{1}} x_{ν_{1}} ∧ … ∧ P_{n} x_{n}

leicht die Fallunterscheidungsregel

∀x_{1}, …, x_{m_{1}^{j}}. u = C_{1}^{j} x_{1} … x_{m_{1}^{j}} ⟹ P
⋮
∀x_{1}, …, x_{m_{k_{j}}^{j}} . u = C_{k_{j}}^{j} x_{1} … x_{m_{k_{j}}^{j}} ⟹ P

P

indem P_{j} = λz. u = z ⟹ P und P_{j′} = λz. True für alle j′ ≠ j gesetzt wird.

4.6.2 Primitive Rekursion

Die Kombinatoren für primitive Rekursion erhält man relativ leicht, indem man deren Graph, d.h. die Relation zwischen Funktionsargumenten und Ergebnissen induktiv definiert. Dieses Verfahren wird auch in [Harrison, 1995] vorgeschlagen. Unter Verwendung der Induktionsregel für die beteiligten Datentypen kann dann gezeigt werden, daß die induktiv definierten Relationen tatsächlich totale Funktionen repräsentieren, d.h. linkstotal und rechtseindeutig sind. Mit Hilfe des Hilbertschen Auswahloperators können aus diesen Relationen dann Funktionen gewonnen und deren charakteristische Gleichungen bewiesen werden.

4.6.2.1 Induktive Definition der Funktionsgraphen

Im Falle der Typen (α, β)term und ((α, β)term)list werden die Mengen bzw. Relationen

term rec set f_{1} … f_{4}  :: ((α, β)term × γ)set
term list rec set f_{1} … f_{4} :: (((α, β)term)list × δ)set

induktiv durch die Einführungsregeln

(Var a, f_{1} a) ∈ term rec set f_{1} … f_{4}
(xs, y) ∈ term list rec set f_{1} … f_{4}
(App b xs, f_{2} b xs y) ∈ term rec set f_{1} … f_{4}
(Nil, f_{3}) ∈ term list rec set f_{1} … f_{4}
(x, y) ∈ term rec set f_{1} … f_{4} (xs, y′) ∈ term list rec set f_{1} … f_{4}
(Cons x xs, f_{4} x xs y y′) ∈ term list rec set f_{1} … f_{4}

definiert. Gemäß Abschnitt 2.3.2 erhalten wir für die so definierten Mengen die Eliminationsregeln

r ∈ term rec set f_{1} … f_{4}
∀a. r = (Var a, f_{1} a) ⟹ P
∀b, xs, y. r = (App b xs, f_{2} b xs y) ∧ (xs, y) ∈ term list rec set f_{1} … f_{4}

P

s ∈ term list rec set f_{1} … f_{4}
s = (Nil, f_{3}) ⟹ Q

∀x, xs, y, y′. s = (Cons x xs, f_{4} x xs y y′) ∧ (x, y) ∈ term rec set f_{1} … f_{4} ∧

(xs, y′) ∈ term list rec set f_{1} … f_{4} ⟹ Q Q

Allgemeines Verfahren Wir definieren induktiv die Relationen

t_{1} rec set f_{1}^{1} … f_{k_{1}}^{1} … f_{1}^{n} … f_{k_{n}}^{n} :: ((α_{1}, …, α_{h})t_{1} × β_{1})set
⋮
t_{n} rec set f_{1}^{1} … f_{k_{1}}^{1} … f_{1}^{n} … f_{k_{n}}^{n} :: ((α_{1}, …, α_{h})t_{n} × β_{n})set

wobei wir, wie auch schon bei der Definition der repräsentierenden Mengen, für jeden der Konstruktoren C_{1}^{1}, …, C_{k_{1}}^{1}, …, C_{1}^{n}, …, C_{k_{n}}^{n} der beteiligten Datentypen eine Einführungsregel angeben. Für einen Konstruktor der Form

C_{i}^{j} … (α_{1}, …, α_{h})t_{j′} … τ_{i′} …

gibt man hierbei die Regel

(x, y) ∈ t_{j′} rec set f_{1}^{1} … f_{k_{n}}^{n} …
(C_{i}^{j} x_{1} … x … x′ … x_{m_{i}^{j}} ,
f_{i}^{j} x_{1} … x … x′ … x_{m_{i}^{j}} y_{1} … y … y_{l_{i}^{j}} ) ∈ t_{j} rec set f_{1}^{1} … f_{k_{n}}^{n}

an. Wir erhalten hierbei Eliminationsregeln der Form

r ∈ t_{j} rec set f_{1}^{1} … f_{k_{n}}^{n}
⋮
∀x, x′, y, …. r = (C_{i}^{j} x_{1} … x … x′ … x_{m_{i}^{j}} ,
f_{i}^{j} x_{1} … x … x′ … x_{m_{i}^{j}} y_{1} … y … y_{l_{i}^{j}} ) ∧
(x, y) ∈ t_{j′} rec set f_{1}^{1} … f_{k_{n}}^{n} ∧ … ⟹ P
⋮

P

4.6.2.2 Totalität und Eindeutigkeit

Es muß nun gezeigt werden, daß die soeben definierten Relationen tatsächlich totale Funktionen repräsentieren. Der Beweis erfolgt mit Hilfe der in Abschnitt 4.5.3 bewiesenen strukturellen Induktionsregel. Im Falle der Typen (α, β)term und ((α, β)term)list gehen wir hierbei vom Beweisziel

∃_{1}y. (x, y) ∈ term rec set f_{1} … f_{4} ∧ ∃_{1}y. (xs, y) ∈ term list rec set f_{1} … f_{4}

aus. Durch Induktion über x und xs erhält man die Beweisziele

(1) ∀a. ∃_{1}y. (Var a, y) ∈ term rec set f_{1} … f_{4}
(2) ∀b, xs. (∃_{1}y′. (xs, y′) ∈ term list rec set f_{1} … f_{4}) ⟹
∃_{1}y. (App b xs, y) ∈ term list rec set f_{1} … f_{4}
(3) ∃_{1}y. (Nil, y) ∈ term list rec set f_{1} … f_{4}
(4) ∀x, xs. (∃_{1}y′. (x, y′) ∈ term rec set f_{1} … f_{4}) ∧
(∃_{1}y′′. (xs, y′′) ∈ term rec set f_{1} … f_{4}) ⟹
∃_{1}y. (Cons x xs, y) ∈ term list rec set f_{1} … f_{4}

Da die Vorgehensweise für alle Beweisziele ähnlich ist, wird diese im folgenden exemplarisch am Beweisziel (2) dargestellt. Durch Elimination von ∃_{1} in der Prämisse erhält man aus (2) das Beweisziel

∀b, xs, z. (xs, z) ∈ term list rec set f_{1} … f_{4} ∧
(∀z′. (xs, z′) ∈ term list rec set f_{1} … f_{4} ⟹ z′ = z) ⟹
∃_{1}y. (App b xs, y) ∈ term rec set f_{1} … f_{4}

Mit Hilfe der Einführungsregel für ∃_{1} ergeben sich daraus die Beweisziele

(5) ∀b, xs, z. (xs, z) ∈ term list rec set f_{1} … f_{4} ⟹
(App b xs, f_{2} b xs z) ∈ term rec set f_{1} … f_{4}
(6) ∀b, xs, z, z′′. (∀z′. (xs, z′) ∈ term list rec set f_{1} … f_{4} ⟹ z′ = z) ∧
(App b xs, z′′) ∈ term rec set f_{1} … f_{4} ⟹ z′′ = f_{2} b xs z

Hierbei ergibt sich (5) aus der entsprechenden Einführungsregel für term rec set. Durch Anwendung der Eliminationsregel für term rec set erhält man aus (6) die neuen Beweisziele

(7) ∀b, xs, z, z′′, a. (∀z′. (xs, z′) ∈ term list rec set f_{1} … f_{4} ⟹ z′ = z) ∧
(App b xs, z′′) = (Var a, f_{1} a) ⟹ z′′ = f_{2} b xs z
(8) ∀b, xs, z, z′′, b′, xs′, z′′′. (∀z′. (xs, z′) ∈ term list rec set f_{1} … f_{4} ⟹ z′ = z) ∧
(App b xs, z′′) = (App b′ xs′, f_{2} b′ xs′ z′′′) ∧
(xs′, z′′′) ∈ term rec set f_{1} … f_{4} ⟹ z′′ = f_{2} b xs z

Beweisziel (7) ist wegen App … ≠ Var … trivial lösbar. Aus der Prämisse

(App b xs, z′′) = (App b′ xs′, f_{2} b′ xs′ z′′′)

von (8) erhält man aufgrund der Injektivität von ( , ) und App die Gleichungen b = b′, xs = xs′ sowie z′′ = f_{2} b′ xs′ z′′′. Zusammen mit den Prämissen

(xs′, z′′′) ∈ term rec set f_{1} … f_{4}

und

∀z′. (xs, z′) ∈ term list rec set f_{1} … f_{4} ⟹ z′ = z

erhält man schließlich noch z′′′ = z, womit auch Beweisziel (8) gelöst ist.

Allgemeines Verfahren Wir zeigen

∃_{1}y. (x_{1}, y) ∈ t_{1} rec set f_{1}^{1} … f_{k_{n}}^{n} ∧ … ∧ ∃_{1}y. (x_{n}, y) ∈ t_{n} rec set f_{1}^{1} … f_{k_{n}}^{n}

mit Hilfe der in Abschnitt 4.5.3 bewiesenen strukturellen Induktionsregel. Induktion über x_{1}, …, x_{n} ergibt die Beweisziele

… ⟹ ∃_{1}y. (C_{1}^{1} …, y) ∈ t_{1} rec set f_{1}^{1} … f_{k_{n}}^{n}
⋮
… ⟹ ∃_{1}y. (C_{k_{1}}^{1} …, y) ∈ t_{1} rec set f_{1}^{1} … f_{k_{n}}^{n}
⋮
(⋆) ∀x, x′, …. (∃_{1}y′. (x, y′) ∈ t_{j′} rec set f_{1}^{1} … f_{k_{n}}^{n} ) ∧ … ⟹
∃_{1}y. (C_{i}^{j} … x … x′ …, y) ∈ t_{j} rec set f_{1}^{1} … f_{k_{n}}^{n}
⋮
… ⟹ ∃_{1}y. (C_{1}^{n} …, y) ∈ t_{n} rec set f_{1}^{1} … f_{k_{n}}^{n}
⋮
… ⟹ ∃_{1}y. (C_{k_{n}}^{n} …, y) ∈ t_{n} rec set f_{1}^{1} … f_{k_{n}}^{n}

Durch Elimination von ∃_{1} in der Prämisse erhält man aus (⋆) das Beweisziel

∀x, x′, z, …. (x, z) ∈ t_{j′} rec set f_{1}^{1} … f_{k_{n}}^{n} ∧
(∀z′. (x, z′) ∈ t_{j′} rec set f_{1}^{1} … f_{k_{n}}^{n} ⟹ z′ = z) ∧ … ⟹
∃_{1}y. (C_{i}^{j} … x … x′ …, y) ∈ t_{j} rec set f_{1}^{1} … f_{k_{n}}^{n}

Verwendung der Einführungsregel für ∃_{1} ergibt die Beweisziele

(1) ∀x, x′, z, …. (x, z) ∈ t_{j′} rec set f_{1}^{1} … f_{k_{n}}^{n} ∧ … ⟹
(C_{i}^{j} … x … x′ …, f_{i}^{j} … x … x′ … z …) ∈ t_{j} rec set f_{1}^{1} … f_{k_{n}}^{n}
(2) ∀x, x′, z, z′′, …. (∀z′. (x, z′) ∈ t_{j′} rec set f_{1}^{1} … f_{k_{n}}^{n} ⟹ z′ = z) ∧
(C_{i}^{j} … x … x′ …, z′′) ∈ t_{j} rec set f_{1}^{1} … f_{k_{n}}^{n} ∧ … ⟹
z′′ = f_{i}^{j} … x … x′ … z …

Beweisziel (1) kann mit Hilfe der Einführungsregeln für t_{j} rec set in Verbindung mit den Prämissen gelöst werden. Durch Anwendung der Eliminationsregel für t_{j} rec set erhält man aus (2) die neuen Beweisziele

∀ …. (C_{i}^{j} … x … x′ …, z′′) = (C_{1}^{j} …, f_{1}^{j} …) ∧ … ⟹ …
⋮
(⋆⋆) ∀x, x′, z, z′′, x̂, x̂′, z′′′, …. (∀z′. (x, z′) ∈ t_{j′} rec set f_{1}^{1} … f_{k_{n}}^{n} ⟹ z′ = z) ∧
(C_{i}^{j} … x … x′ …, z′′) =
(C_{i}^{j} … x̂ … x̂′ …, f_{i}^{j} … x̂ … x̂′ … z′′′ …) ∧
(x̂, z′′′) ∈ t_{j′} rec set f_{1}^{1} … f_{k_{n}}^{n} ∧ … ⟹
z′′ = f_{i}^{j} … x … x′ … z …
⋮
∀ …. (C_{i}^{j} … x … x′ …, z′′) = (C_{k_{j}}^{j} …, f_{k_{j}}^{j} …) ∧ … ⟹ …

Alle Beweisziele bis auf (⋆⋆) sind aufgrund der Verschiedenheit der Konstruktoren trivial lösbar. Aufgrund der Injektivität von ( , ) und C_{i}^{j} erhält man aus (⋆⋆) das Beweisziel

∀x, x′, z, z′′, x̂, x̂′, z′′′, …. (∀z′. (x, z′) ∈ t_{j′} rec set f_{1}^{1} … f_{k_{n}}^{n} ⟹ z′ = z) ∧
x = x̂ ∧ x′ = x̂′ ∧ z′′ = f_{i}^{j} … x̂ … x̂′ … z′′′ … ∧
(x̂, z′′′) ∈ t_{j′} rec set f_{1}^{1} … f_{k_{n}}^{n} ∧ … ⟹ z′′ = f_{i}^{j} … x … x′ … z …

Aus den Prämissen x = x̂ und (x̂, z′′′) ∈ t_{j′} rec set f_{1}^{1} … f_{k_{n}}^{n} sowie

∀z′. (x, z′) ∈ t_{j′} rec set f_{1}^{1} … f_{k_{n}}^{n} ⟹ z′ = z

ergibt sich z′′′ = z, womit sich das Beweisziel lösen läßt.

4.6.2.3 Definition der Kombinatoren

Die Kombinatoren für primitive Rekursion können nun mit Hilfe der Mengen t_{1} rec set, …, t_{n} rec set unter Verwendung des Hilbertschen Auswahloperators durch

t_{1} rec f_{1}^{1} … f_{k_{n}}^{n} x ≡ εy. (x, y) ∈ t_{1} rec set f_{1}^{1} … f_{k_{n}}^{n}
⋮
t_{n} rec f_{1}^{1} … f_{k_{n}}^{n} x ≡ εy. (x, y) ∈ t_{n} rec set f_{1}^{1} … f_{k_{n}}^{n}

definiert werden.

4.6.2.4 Charakteristische Gleichungen

Um die definierten Kombinatoren komfortabel verwenden zu können, werden nun noch charakteristische Gleichungen bewiesen, die deren Wirkung auf bestimmte Konstruktoren beschreiben. Für die Kombinatoren term rec und term list rec sind dies die bereits aus Abschnitt 3.3 bekannten Gleichungen

term rec f_{1} … f_{4} (Var a) = f_{1} a
term rec f_{1} … f_{4} (App b ts) = f_{2} b ts (term list rec f_{1} … f_{4} ts)
term list rec f_{1} … f_{4} Nil = f_{3}
term list rec f_{1} … f_{4} (Cons t ts) =
f_{4} t ts (term rec f_{1} … f_{4} t) (term list rec f_{1} … f_{4} ts)

Wir erläutern hier exemplarisch den Beweis von

term rec f_{1} … f_{4} (App b ts) = f_{2} b ts (term list rec f_{1} … f_{4} ts)

Durch Anwendung der Definition von term rec und term list rec erhält man das Beweisziel

εy. (App b ts, y) ∈ term rec set f_{1} … f_{4} =
f_{2} b ts (εy′. (ts, y′) ∈ term list rec set f_{1} … f_{4})

Mit Hilfe der Regel

∃_{1}y. P y P a
(εy. P y) = a

(select1 equality)

und des soeben bewiesenen Theorems

∃_{1}y. (App b ts, y) ∈ term rec set f_{1} … f_{4}

erhält man das neue Beweisziel

(App b ts, f_{2} b ts (εy′. (ts, y′) ∈ term list rec set f_{1} … f_{4})) ∈ term rec set f_{1} … f_{4}

Es ist also noch zu zeigen, daß der auf der rechten Seite der zu beweisenden charakteristischen Gleichung angegebene Wert tatsächlich in Relation mit App b ts steht. Wir wenden nun die entsprechende Einführungsregel für die Menge term rec set an und erhalten so das Beweisziel

(ts, εy′. (ts, y′) ∈ term list rec set f_{1} … f_{4}) ∈ term list rec set f_{1} … f_{4}

das mit Hilfe des Theorems

P (εy. P y) = ∃y. P y (select eq Ex)

und ∃y. (ts, y) ∈ term list rec set f_{1} … f_{4} gelöst werden kann.

Allgemeines Verfahren Wir beweisen

t_{j} rec f_{1}^{1} … f_{k_{n}}^{n} (C_{i}^{j} … x … x′ …) =
f_{i}^{j} … x … x′ … (t_{j′} rec f_{1}^{1} … f_{k_{n}}^{n} x) …

Die Anwendung der Definition von t_{j} rec und t_{j′} rec ergibt das Beweisziel

(εy. (C_{i}^{j} … x … x′ …, y) ∈ t_{j} rec set f_{1}^{1} … f_{k_{n}}^{n} ) =
f_{i}^{j} … x … x′ … (εy′. (x, y′) ∈ t_{j′} rec set f_{1}^{1} … f_{k_{n}}^{n} ) …

Aufgrund der Regel (select1 equality) und des soeben bewiesenen Theorems

∃_{1}y. (C_{i}^{j} … x … x′ …, y) ∈ t_{j} rec set f_{1}^{1} … f_{k_{n}}^{n}

erhält man das neue Beweisziel

(C_{i}^{j} … x … x′ …,

f_{i}^{j} … x … x′ … (εy′. (x, y′) ∈ t_{j′} rec set f_{1}^{1} … f_{k_{n}}^{n} ) …) ∈ t_{j} rec set f_{1}^{1} … f_{k_{n}}^{n}

Unter Verwendung der entsprechenden Einführungsregel für die Menge t_{j} rec set ergeben sich die Beweisziele

(⋆) (x, εy′. (x, y′) ∈ t_{j′} rec set f_{1}^{1} … f_{k_{n}}^{n} ) ∈ t_{j′} rec set f_{1}^{1} … f_{k_{n}}^{n}
⋮

wobei (⋆) mittels (select eq Ex) und ∃y. (x, y) ∈ t_{j′} rec set f_{1}^{1} … f_{k_{n}}^{n} gelöst werden kann.

4.6.3 Case-Kombinator

Für 1 ≤ j < ν_{1} läßt sich der Kombinator t_{j} case mit den charakteristischen Gleichungen der Form

t_{j} case_{j} g_{1} … g_{k_{j}} (C_{i}^{j} x_{1} … x_{m_{i}^{j}} ) = g_{i} x_{1} … x_{m_{i}^{j}}

leicht durch

t_{j} rec f_{1}^{1} … f_{k_{1}}^{1} … f_{1}^{n} … f_{k_{n}}^{n}

ausdrücken, indem

f_{i}^{j} = λx_{1}, …, x_{m_{i}^{j}} , y_{1}, …, y_{l_{i}^{j}} . g_{i} x_{1} … x_{m_{i}^{j}}

für alle 1 ≤ i ≤ k_{j} und f_{i′}^{j′} = arbitrary für alle j′ ≠ j gesetzt wird. Die Ergebnisse y_{1}, …, y_{l_{i}^{j}} der rekursiven Aufrufe werden hierbei also wegprojiziert. Da deshalb auch keine Rekursion über andere Datentypen (α_{1}, …, α_{h})t_{j′} erfolgt, können die für Konstruktoren dieser Datentypen zuständigen Funktionen f_{i′}^{j′} mit beliebigen Werten belegt werden.

Erweiterungsmöglichkeiten

In Kapitel 3 wurden einige Klassen von Datentypen vorgestellt, die sich mit den in Kapitel 4 anschließend dargestellten Verfahren in HOL repräsentieren lassen. Das folgende Kapitel beschäftigt sich nun mit der Frage, welche Datentypen darüberhinaus noch in HOL repräsentierbar sind, wobei insbesondere verschachtelt rekursive Datentypen mit Funktionstypen genauer betrachtet werden sollen. Hierfür werden zunächst grundsätzliche theoretische Einschränkungen der Repräsentierbarkeit von rekursiven Datentypen diskutiert. Sodann wird eine Erweiterung des in Abschnitt 4.2.1 vorgestellten Universums vorgeschlagen. Aufbauend auf diesem Universum wird schließlich exemplarisch die Konstruktion eines solchen Datentyps demonstriert. Die hier beschriebenen Konstruktionsverfahren gehören zwar momentan noch nicht zum Funktionsumfang des im Rahmen dieser Arbeit implementierten Datentyppakets, wurden jedoch in Isabelle/HOL nachvollzogen.

5.1 Verschachtelt rekursive Datentypen mit Funktionstypen

In Abschnitt 3.3 wurde für Datentypdefinitionen als Zulässigkeitsbedingung festgelegt, daß in Argumenttypen von Konstruktoren, die die Form (…, (α_{1}, …, α_{h})t_{j} , …)t′ haben, t′ der Konstruktor eines bereits definierten Datentyps sein muß. Dies ist keinesfalls eine willkürliche Einschränkung, sondern stellt sicher, daß der Datentyp tatsächlich konstruierbar ist. Um die Notwendigkeit dieser Bedingung einzusehen, betrachten wir die Typdefinition

datatype α dt = C α
| D (α dt → bool)

Wie in Kapitel 4 beschrieben wurde, werden neue Datentypen durch die Angabe ihrer repräsentierenden Mengen definiert. Um also den Typ α dt definieren zu können, muß zunächst eine repräsentierende Menge dt rep set gefunden werden. Da der Datentyp α dt die (injektive) Konstruktorfunktion

D :: (α dt → bool) → α dt

besitzen soll, muß eine Injektion von der repräsentierenden Menge des Typs α dt → bool in die Menge dt rep set existieren. Da jede Funktion vom Typ α dt → bool eine Teilmenge von α dt charakterisiert, ist die repräsentierenden Menge des Typs α dt → bool isomorph zu P(dt rep set), es muß also auch eine Injektion von P(dt rep set) in die Menge dt rep set existieren. Dies steht jedoch im Widerspruch zu folgendem Theorem von Cantor:

Theorem 5.1 (Cantor) Für keine Menge S existiert eine Surjektion f : S → P(S) oder eine Injektion g : P(S) → S.

Beweis

1. Angenommen, es gibt eine Surjektion f : S → P(S). Wir definieren nun

R = {x ∈ S | x ∉ f (x)}

Da R ∈ P(S) und f surjektiv ist, gibt es ein r ∈ S mit R = f (r). Gilt nun r ∈ R, so folgt r ∉ f (r) = R. Gilt r ∉ R = f (r), so folgt r ∈ R. Es kann also keine derartige Surjektion existieren.

2. Angenommen, es gibt eine Injektion g : P(S) → S. Dann existiert eine Surjektion f : S → P(S), nämlich f = inv g, wobei inv g = (λy. εx. g(x) = y). Da keine Surjektion f : S → P(S) existiert, kann es also auch keine Injektion g geben.

□

Trotz dieser Erkenntnis ist es möglich, bestimmte verschachtelt rekursive Datentypen mit Funktionstypen zu konstruieren. Es muß hierbei sichergestellt sein, daß die betreffende Datentypdefinition nur Typausdrücke enthält, in denen die gerade definierten rekursiven Typen (α_{1}, …, α_{h})t_{j} ausschließlich strikt positiv vorkommen, was wie folgt definiert ist:

Definition 5.2 (Strikt positives Vorkommmen von Typen) Ein Typ τ′ kommt in einem Typausdruck τ strikt positiv vor, falls eine der folgenden Bedingungen erfüllt ist:

• τ = τ′

• τ = τ_{1} → τ_{2} und τ′ kommt in τ_{2} strikt positiv vor

• τ = (τ_{1}, …, τ_{h′})t′, wobei t′ der Konstruktor eines bereits definierten Datentyps mit den Typparametern β_{1}, …, β_{h′} ist, τ′ strikt positiv in τ_{i} vorkommt und der Typparameter β_{i} in allen Typausdrücken in der Definition von t′ nur strikt positiv vorkommt.

□

Demnach ist auch

datatype α dt = C α
| D ((α dt → bool) → bool)

unzulässig, denn gäbe es eine Injektion

D :: ((α dt → bool) → bool) → α dt könnte man mit Hilfe der Injektion

(λx. (λy. x = y)) :: (α dt → bool) → ((α dt → bool) → bool)

die Injektion

D ∘ (λx. (λy. x = y)) :: (α dt → bool) → α dt

konstruieren, was ebenfalls einen Widerspruch zu Cantors Theorem darstellen würde.

Ein Beispiel für einen gemäß dieser Definition zulässigen Datentyp ist der Typ (α, β, γ)tree der Bäume mit potentiell unendlichem Verzweigungsgrad |γ|

datatype (α, β, γ)tree = Atom α
| Branch β (γ → (α, β, γ)tree)

Die Induktionsregel für diesen Typ hat die Gestalt

∀a. P (Atom a) ∀b, f . (∀x. P (f x)) ⟹ P (Branch b f )

P t

Der Kombinator

tree rec :: (α → δ) →
(β → (γ → (α, β, γ)tree) → (γ → δ) → δ) →
(α, β, γ)tree → δ

für primitive Rekursion besitzt hierbei die charakteristischen Gleichungen

tree rec f_{1} f_{2} (Atom a)  = f_{1} a
tree rec f_{1} f_{2} (Branch b f ) = f_{2} b f ((tree rec f_{1} f_{2}) ∘ f )

Die genaueren Details der Konstruktion dieses Typs werden im folgenden Abschnitt beschrieben. Auch in [Gunter, 1993] wird auf die Handhabung derartiger Typen in HOL eingegangen.

Bemerkung 5.3 Die durch das Theorem von Cantor gegebenen Einschränkungen gelten im Kontext von klassischer Mengenlehre, wobei → den vollen Funktionenraum bezeichnet. Verwendet man anstelle des vollen Funktionenraums den stetigen Funktionenraum, so gelten diese Einschränkungen nicht mehr. Derartige Konstruktionen werden in der Literatur oft mit dem Begriff Scott Domains bezeichnet.

5.2 Ein Universum für Datentypen mit beliebigem Verzweigungsgrad

Der in Abschnitt 4.2.1 eingeführte Typ zur Darstellung von Bäumen wird nun wie folgt verändert:

(α, β)node = (nat → (β + nat)) × (α + nat)
(α, β)item = ((α, β)node)set

Als Labels für Verzweigungen werden hier nun neben Elementen vom Typ nat auch Elemente des Typs β zugelassen. Bei der Repräsentation von Datentypen, in deren Definition Typausdrücke der Form τ_{j} → (α_{1}, …, α_{h})t_{i} mit 1 ≤ j ≤ ξ vorkommen, wird für β die Summe τ_{1} + ⋯ + τ_{ξ} aller Verzweigungstypen τ_{1}, …, τ_{ξ} gewählt. Bei einem komplexeren Typausdruck der Form τ′_{1} → ⋯ → τ′_{μ} → (α_{1}, …, α_{h})t_{i} wird τ′_{1} × ⋯ × τ′_{μ} als Verzweigungstyp verwendet.

Die Definition der in Abschnitt 4.2.1 angegebenen Funktionen auf item lautet nun

push  :: (β + nat) → (α, β)node → (α, β)node
push c n ≡ (nat case c (fst n), snd n)
Scons  :: (α, β)item → (α, β)item → (α, β)item
Scons i_{1} i_{2} ≡ (push (Inr 1) “ i_{1}) ∪ (push (Inr 2) “ i_{2})
Leaf  :: (α, β) → (α, β)item
Leaf a  ≡ {(λx. Inr 0, Inl a)}
Numb  :: nat → (α, β)item
Numb k  ≡ {(λx. Inr 0, Inr k)}

Zur Repräsentation von Funktionen des Typs β → (α, β)item durch ein Element vom Typ (α, β)item definieren wir

Lim :: (β → (α, β)item) → (α, β)item
Lim f ≡ ⋃{z | ∃x. z = push (Inl x) “ (f x)}

Durch Lim f wird die Menge von Knoten bezeichnet, die sich ergibt, wenn für alle x jeweils an alle Pfade der Knoten in der Menge f x das Präfix x angefügt wird und die so entstehenden Knotenmengen vereinigt werden. Dies ist in Abbildung 5.1 graphisch dargestellt.

[figure: f x_{1}; f x_{2}; …; x_{2}; x_{1}]

Abbildung 5.1: Repräsentation von Funktionen durch Bäume

Injektivität von Lim Mittels elementarer Eigenschaften von Funktionen und Mengen läßt sich nun für Lim die Eigenschaft

Lim f = Lim g ⟹ f = g

nachweisen.

Beweis Der Beweis erfolgt durch Widerspruch: Angenommen, es gilt Lim f = Lim g und f ≠ g, d.h. es existiert ein x mit f x ≠ g x. Da es sich bei f x und g x um Mengen handelt, bedeutet dies nun, daß ein Element y existiert, für das • y ∈ f x und y ∉ g x oder

• y ∈ g x und y ∉ f x

gilt. Wir betrachten hier exemplarisch den ersten dieser beiden Fälle: Gilt y ∈ f x, so folgt push (Inl x) y ∈ Lim f aufgrund der Definition von Lim und damit auch push (Inl x) y ∈ Lim g. Dies bedeutet wiederum wegen der Definition von Lim, daß y′ ∈ g x′ und push (Inl x) y = push (Inl x′) y′ für geeignete x′ und y′ gelten muß. Aufgrund der Injektivität von push und Inl erhält man hieraus x = x′ und y = y′, was zusammen mit y′ ∈ g x′ und y ∉ g x zu einem Widerspruch führt. □

5.3 Konstruktion eines Datentyps mit unendlichem Verzweigungsgrad

Mit Hilfe der soeben eingeführten Konstruktionselemente kann nun der Typ

datatype (α, β, γ)tree = Atom α
| Branch β (γ → (α, β, γ)tree)

konstruiert werden.

5.3.1 Repräsentierende Menge

Die repräsentierende Menge tree rep set ist hierbei vom Typ ((α + β, γ)item)set und wird induktiv durch die Regeln

In0 (Leaf (Inl a)) ∈ tree rep set

g ∈ Funs tree rep set In1 (Scons (Leaf (Inr b)) (Lim g)) ∈ tree rep set

definiert, wobei die in der zweiten Regel verwendete monotone Funktion Funs die Definition

Funs  :: β set → (α → β)set
Funs S ≡ {g | range g ⊆ S}

hat. Mit der Prämisse g ∈ Funs tree rep set der zweiten Einführungsregel wird also ausgedrückt, daß alle Bildelemente der Funktion g Repräsentationen von Bäumen sind.

5.3.2 Konstruktoren

Die Konstruktoren

Atom :: α → (α, β, γ)tree
Branch :: β → (γ → (α, β, γ)tree) → (α, β, γ)tree

werden durch

Atom a  ≡ Abs tree (In0 (Leaf (Inl a)))
Branch b f ≡ Abs tree (In1 (Scons (Leaf (Inr b)) (Lim (Rep tree ∘ f ))))

definiert. Im Falle des Konstruktors Branch wird hierbei die Repräsentation des Arguments f :: γ → (α, β, γ)tree berechnet, indem zuerst durch die Komposition von Rep tree mit f die Repräsentationen der Bildelemente von f berechnet werden. Die Repräsentation der sich so ergebenden Funktion vom Typ γ → (α + β, γ)item wird dann mittels Lim berechnet. Beim Beweis der Injektivität des Konstruktors Branch wird zusätzlich die Injektivität von Lim benötigt.

5.3.3 Induktionsregel

Die in 5.1 angegebene Induktionsregel kann nun, ähnlich wie in Abschnitt 4.5.3 beschrieben, mit Hilfe der Induktionsregel

∀a. Q (In0 (Leaf (Inl a)))

∀b, g. range g ⊆ tree rep set ∩ {x | Q x} ⟹ Q (In1 (Scons (Leaf (Inr b)) (Lim g))) u ∈ tree rep set ⟹ Q u

für die Menge tree rep set bewiesen werden. Hierbei muß unter den Annahmen

(i) ∀a. Atom a
(ii) ∀b, f . (∀x. P (f x)) ⟹ P (Branch b f )

das Beweisziel P t gezeigt werden. Mittels (Rep tree inverse) und (Rep tree) erhält man hieraus das Beweisziel

Rep tree t ∈ tree rep set ⟹ P (Abs tree (Rep tree t))

Die Anwendung der obigen Induktionsregel mit Q = P ∘ Abs tree und u = Rep tree t liefert nun die Beweisziele

(1) ∀a. P (Abs tree (In0 (Leaf (Inl a))))
(2) ∀b, g. range g ⊆ tree rep set ∩ {x | P (Abs tree x)} ⟹

P (Abs tree (In1 (Scons (Leaf (Inr b)) (Lim g))))

Wir erläutern hier exemplarisch die Behandlung von (2). Aufgrund des Theorems

range g ⊆ tree rep set ⟹ Rep tree ∘ (Abs tree ∘ g) = g

das man leicht mittels Extensionalität aus (Abs tree inverse) erhält, ergibt sich aus (2) das neue Beweisziel

∀b, g. range g ⊆ tree rep set ∩ {x | P (Abs tree x)} ⟹ P (Abs tree (In1 (Scons (Leaf (Inr b)) (Lim (Rep tree ∘ (Abs tree ∘ g))))))

Aufgrund der Definition des Konstruktors Branch läßt sich dies zu

∀b, g. range g ⊆ tree rep set ∩ {x | P Abs tree x)} ⟹ P (Branch b (Abs tree ∘ g)) umformen. Unter Verwendung von Voraussetzung (ii) erhält man das Beweisziel

∀b, g, x′. range g ⊆ tree rep set ∩ {x | P (Abs tree x)} ⟹ P (Abs tree (g x′))

das sich leicht mit Hilfe elementarer Eigenschaften von range zeigen läßt.

5.3.4 Primitive Rekursion

Der Graph des Kombinators

tree rec :: (α → δ) →
(β → (γ → (α, β, γ)tree) → (γ → δ) → δ) →
(α, β, γ)tree → δ

ist durch die Menge

tree rec set f_{1} f_{2} :: ((α, β, γ)tree × δ)set

gegeben, die induktiv durch die Regeln

(Atom a, f_{1} a) ∈ tree rec set f_{1} f_{2}

f′ ∈ compose f (tree rec set f_{1} f_{2}) (Branch b f , f_{2} b f f′) ∈ tree rec set f_{1} f_{2}

definiert ist. Die monotone Funktion compose ist hierbei definiert durch

compose  :: (α → β) → (β × γ)set → (α → γ)set
compose f R ≡ {f′ | ∀x. (f x, f′ x) ∈ R}

Die zweite Einführungsregel drückt aus, daß die durch die Relation tree rec set repräsentierte Funktion rekursiv auf alle Bildelemente der Funktion f , also auf alle Unterbäume des Baums Branch b f angewendet werden muß. Ergebnis dieser rekursiven Anwendung ist die Funktion f′, die man durch die Komposition der Funktion f mit der Relation tree rec set erhält. Dieser Sachverhalt wird mit Hilfe von compose ausgedrückt. Die etwas umständlich anmutende Formulierung ist notwendig, da die Einführungsregeln induktiver Mengen eine bestimmte, in Abschnitt 2.3.2 festgelegte Struktur aufweisen müssen, um die Monotonie der sich aus den Regeln ergebenden Funktion zu gewährleisten.

Totalität und Eindeutigkeit Mit Hilfe der in Abschnitt 5.3.3 bewiesenen Induktionsregel für (α, β, γ)tree kann nun, ähnlich wie in Abschnitt 4.6.2 gezeigt werden, daß die soeben definierte Relation linkstotal und rechtseindeutig ist, d.h.

∃_{1}y. (x, y) ∈ tree rec set f_{1} f_{2}

Induktion über x liefert die Beweisziele

(1) ∀a. ∃_{1}y. (Atom a, y) ∈ tree rec set f_{1} f_{2}
(2) ∀b, f . (∀x. ∃_{1}y. (f x, y) ∈ tree rec set f_{1} f_{2}) ⟹
∃_{1}y. (Branch b f , y) ∈ tree rec set f_{1} f_{2})

wobei wir wieder nur die Behandlung von (2) betrachten. Wir wenden auf (2) zunächst die Einführungsregel für ∃_{1} an, wobei wir als ”Zeugen“ für die Existenzaussage den Term

f_{2} b f ((λx. εy. (x, y) ∈ tree rec set f_{1} f_{2}) ∘ f )

angeben. Dies liefert die neuen Beweisziele

(3) ∀b, f . (∀x. ∃_{1}y. (f x, y) ∈ tree rec set f_{1} f_{2}) ⟹

(Branch b f , f_{2} b f ((λx. εy. (x, y) ∈ tree rec set f_{1} f_{2}) ∘ f )) ∈ tree rec set f_{1} f_{2}

(4) ∀b, f , z. (∀x. ∃_{1}y. (f x, y) ∈ tree rec set f_{1} f_{2}) ∧

(Branch b f , z) ∈ tree rec set f_{1} f_{2} ⟹ z = f_{2} b f ((λx. εy. (x, y) ∈ tree rec set f_{1} f_{2}) ∘ f )

Aus (3) erhält man nach Anwendung der entsprechenden Einführungsregel für tree rec set und der Definition von compose schließlich

∀b, f . (∀x. ∃_{1}y. (f x, y) ∈ tree rec set f_{1} f_{2}) ⟹
∀x. (f x, εy. (f x, y) ∈ tree rec set f_{1} f_{2}) ∈ tree rec set f_{1} f_{2}

was sich leicht mittels (select eq Ex) lösen läßt. Aus (4) erhält man mit Hilfe der Eliminationsregel

r ∈ tree rec set f_{1} f_{2}
∀a. r = (Atom a, f_{1} a) ⟹ P
∀b, f′, g. r = (Branch b f′, f_{2} b f′ g) ∧ (∀x. (f′ x, g x) ∈ tree rec set f_{1} f_{2}) ⟹ P

P

für tree rec set die Beweisziele

(5) ∀b, f , z, a. (∀x. ∃_{1}y. (f x, y) ∈ tree rec set f_{1} f_{2}) ∧

(Branch b f , z) = (Atom a, f_{1} a) ⟹ z = f_{2} b f ((λx. εy. (x, y) ∈ tree rec set f_{1} f_{2}) ∘ f )

(6) ∀b, f , z, b′, f′, g. (∀x. ∃_{1}y. (f x, y) ∈ tree rec set f_{1} f_{2}) ∧

(Branch b f , z) = (Branch b′ f′, f_{2} b′ f′ g) ∧ (∀x. (f′ x, g x) ∈ tree rec set f_{1} f_{2}) ⟹

z = f_{2} b f ((λx. εy. (x, y) ∈ tree rec set f_{1} f_{2}) ∘ f )

wobei (5) wegen Branch … ≠ Atom … trivial ist. Unter Ausnutzung der Injektivität von ( , ) und Branch ergibt sich aus (6) das Beweisziel

∀b, f , z, b′, f′, g. (∀x. ∃_{1}y. (f x, y) ∈ tree rec set f_{1} f_{2}) ∧
(∀x. (f′ x, g x) ∈ tree rec set f_{1} f_{2}) ⟹
f_{2} b′ f′ g = f_{2} b′ f′ ((λx. εy. (x, y) ∈ tree rec set f_{1} f_{2}) ∘ f′)

woraus man mit Hilfe von Kongruenz und Extensionalität das Beweisziel

∀f′, g, x′. (∀x. ∃_{1}y. (f x, y) ∈ tree rec set f_{1} f_{2}) ∧
(∀x. (f′ x, g x) ∈ tree rec set f_{1} f_{2}) ⟹
g x′ = εy. (f′ x′, y) ∈ tree rec set f_{1} f_{2}

erhält. Durch Anwendung von (select1 equality) erhält man schließlich die leicht lösbaren Beweisziele

(7) ∀f′, g, x′. (∀x. ∃_{1}y. (f x, y) ∈ tree rec set f_{1} f_{2}) ⟹
∃_{1}y. (f′ x′, y) ∈ tree rec set f_{1} f_{2}
(8) ∀f′, g, x′. (∀x. (f′ x, g x) ∈ tree rec set f_{1} f_{2}) ⟹
(f′ x′, g x′) ∈ tree rec set f_{1} f_{2}

Die Definition des Kombinators tree rec mittels tree rec set sowie die Ableitung der charakteristischen Gleichungen für tree rec erfolgt nahezu genauso wie in Abschnitt 4.5.3.

Vergleich mit anderen Arbeiten

Die in Kapitel 3 und 4 beschriebenen Ansätze zur Realisierung von Datentypen sollen nun mit anderen Arbeiten verglichen werden. Hierfür geben wir zunächst einen kurzen Überblick über bisher vorhandene Datentyppakete. Eines dieser Pakete wird dann in Hinblick auf die Formulierung der charakteristischen Theoreme und die zum Einsatz kommenden Konstruktionsverfahren mit dem im Rahmen dieser Diplomarbeit implementierten Paket verglichen.

6.1 Andere auf HOL basierende Datentyppakete

Das erste definitorische Datentyppaket für das HOL-System wurde 1989 von Tom Melham [Melham, 1989] implementiert. Auch hier wird zunächst ein allgemeiner Typ von Bäumen wie in Abschnitt 4.2.1 definiert, mit dessen Hilfe alle Datentypen repräsentiert werden. Dieses Paket wurde von Elsa Gunter [Gunter, 1992] um verschränkt und verschachtelt rekursive Datentypen erweitert. In [Gunter, 1993] wird beschrieben, wie dieses Paket auf unendlich verzweigende Datentypen ähnlich wie in Kapitel 5 erweitert werden kann. Von Lawrence C. Paulson wurde in [Paulson, 1994] vorgeschlagen, die repräsentierenden Mengen von Datentypen durch induktive Definitionen zu konstruieren, die mittels einer allgemeinen Theorie von Fixpunkten und monotonen Funktionen realisiert werden. Dieser Ansatz wurde auch von John Harrison [Harrison, 1995] verfolgt, der für seinen Theorembeweiser HOL Light ebenfalls ein Datentyppaket implementierte. Sowohl Gunter als auch Harrison realisieren verschachtelt rekursive Datentypen durch Auffalten. Anhang B enthält einen Vergleich von John Harrisons Paket mit dem im Rahmen dieser Diplomarbeit implementierten Paket in Hinblick auf die Beweislaufzeiten für einige ausgewählte Datentypen.

Von Norbert Völker [Völker, 1995, Völker, 1997] wurde für Isabelle/HOL ein Datentyppaket implementiert, mit dem auch verschachtelt rekursive, jedoch keine verschränkt rekursiven Datentypen definiert werden können. Anstatt diese Datentypen durch Auffaltung wie in Kapitel 3 und 4 zu realisieren, wird hier ein etwas anderer Ansatz gewählt, der in den folgenden Abschnitten kurz beschrieben werden soll.

6.2 Alternative Formulierung charakteristischer Theoreme

Für verschachtelt rekursive Datentypen wie

datatype (α, β)term = Var α
| App β (((α, β)term)list)

wird in [Völker, 1995, Völker, 1997] für Induktionsregeln sowie für die charakteristischen Gleichungen der Rekursionskombinatoren eine etwas kompaktere Formulierung präsentiert. Es werden hierbei zahlreiche vordefinierte Standardfunktionen für Datentypen genutzt. Für den Typ list sind dies die Funktionen

map  :: (α → β) → α list → β list
list all  :: (α → bool) → α list → bool
set of list :: α list → α set

mit den charakteristischen Gleichungen

map f Nil  = Nil
map f (Cons x xs)  = Cons (f x) (map f xs)
list all Q Nil  = True
list all Q (Cons x xs) = Q x ∧ (list all Q xs)
set of list Nil  = {}
set of list (Cons x xs) = {x} ∪ (set of list xs)

Unter Verwendung der Funktion list all kann die Induktion über term nun durch die Regel

∀a. P (Var a) ∀b, ts. list all P ts ⟹ P (App b ts)

P t

bzw. mit set of list durch

∀a. P (Var a) ∀b, ts. set of list ts ⊆ {x | P x} ⟹ P (App b ts)

P t

ausgedrückt werden. Der Kombinator

term rec :: (α → γ) → (β → (((α, β)term)list) → γ list → γ) → (α, β)term → γ

für primitive Rekursion läßt sich hierbei mit Hilfe von map durch die Gleichungen

term rec f_{1} f_{2} (Var a)  = f_{1} a
term rec f_{1} f_{2} (App b ts) = f_{2} b ts (map (term rec f_{1} f_{2}) ts)

charakterisieren. Auch wenn die obige Induktionsregel im Vergleich zur ”aufgefalteten“ Induktionsregel aus Abschnitt 3.3 etwas kompakter wirkt, kann deren Anwendung in Beweisen gelegentlich noch eine zusätzliche Induktion über den Typ list erfordern. Die kompakte Induktionsregel für term läßt sich leicht mit Hilfe der ”aufgefalteten“ Induktionsregel herleiten, indem P_{1} mit P und P_{2} mit list all P instantiiert wird.

Beweis Angenommen, es gilt ∀a. P (Var a) und ∀b, ts. list all P ts ⟹ P (App b ts). Ausgehend vom Beweisziel

P t ∧ list all P ts

liefert die Anwendung der simultanen Induktionsregel aus Abschnitt 3.3 die neuen Beweisziele

(1) ∀a. P (Var a)
(2) ∀b, ts. list all P ts ⟹ P (App b ts)
(3) list all P Nil
(4) ∀t, ts. P t ∧ list all P ts ⟹ list all P (Cons t ts)

Die Beweisziele (1) und (2) lassen sich mit Hilfe der Voraussetzungen lösen. Durch Anwendung der charakteristischen Gleichungen von list all erhält man aus (3) und (4) die trivial beweisbaren Beweisziele True und

∀t, ts. P t ∧ list all P ts ⟹ P t ∧ list all P ts

□

Umgekehrt läßt sich aus der kompakten Induktionsregel mit Hilfe von Induktion über list die ”aufgefaltete“ Regel herleiten. Auch bei den Kombinatoren für primitive Rekursion kann man die kompakte Variante term rec leicht aus der ”aufgefalteten“ Variante (im folgenden zur Vermeidung von Verwechslungen mit term rec’ und term list rec’ bezeichnet) erhalten. Es gilt

term rec f_{1} f_{2} t = term rec’ f_{1} f_{2} Nil (λx, xs. Cons) t

map (term rec f_{1} f_{2}) ts = term list rec’ f_{1} f_{2} Nil (λx, xs. Cons) ts

wie man durch simultane Induktion über t und ts unter Verwendung der Induktionsregel aus Abschnitt 3.3 nachweisen kann. Umgekehrt gilt

term rec’ f_{1} f_{2} f_{3} f_{4} t =

term rec f_{1}

(λb, ts, xs. f_{2} b ts (list rec f_{3} (λy, ys, z. f_{4} (fst y) (map fst ys) (snd y) z) (zip ts xs))) t

term list rec’ f_{1} f_{2} f_{3} f_{4} ts =

list rec f_{3}

(λy, ys, z. f_{4} (fst y) (map fst ys) (snd y) z) (zip ts (map

(term rec f_{1}

(λb, ts′, xs. f_{2} b ts′ (list rec f_{3} (λy, ys, z. f_{4} (fst y) (map fst ys) (snd y) z) (zip ts′ xs)))) ts)) was sich analog beweisen läßt. Für die Funktion

zip :: α list → β list → (α × β)list

gilt hierbei

zip Nil Nil  = Nil
zip (Cons x xs) (Cons y ys) = Cons (x, y) (zip xs ys)

Kommt der Typ term selbst wieder in einer verschachtelt rekursiven Datentypdefinition vor, so benötigt man zur kompakten Formulierung der charakteristischen Theoreme des resultierenden Datentyps auch für term entsprechende Varianten der eingangs erwähnten Standardfunktionen

map term :: (α → γ) → (β → δ) → (α, β)term → (γ, δ)term
term all  :: (α → bool) → (β → bool) → (α, β)term → bool
set of term :: (α, β)term → (α + β)set

die in diesem Fall durch die Gleichungen

map term f_{1} f_{2} (Var a)  = Var (f_{1} a)
map term f_{1} f_{2} (App b ts) = App (f_{2} b) (map (map term f_{1} f_{2}) ts)
term all Q_{1} Q_{2} (Var a)  = Q_{1} a
term all Q_{1} Q_{2} (App b ts) = Q_{2} b ∧ (list all Id (map (term all Q_{1} Q_{2}) ts))
set of term (Var a)  = {Inl a}
set of term (App b ts)  = {Inr b} ∪ ⋃(set of list (map set of term ts))

charakterisiert werden. Derartige Funktionen lassen sich auf beliebige Datentypen verallgemeinern. Für einen Datentyp (α_{1}, …, α_{n})t haben die entsprechenden Funktionen die Typen

map t :: (α_{1} → β_{1}) → ⋯ → (α_{n} → β_{n}) → (α_{1}, …, α_{n})t → (β_{1}, …, β_{n})t
t all  :: (α_{1} → bool) → ⋯ → (α_{n} → bool) → (α_{1}, …, α_{n})t → bool
set of t :: (α_{1}, …, α_{n})t → (α_{1} + ⋯ + α_{n})set

Dies gilt allerdings nur für sogenannte reine Datentypen, in deren Definition nur Datentypen vorkommen. Andernfalls weisen die Typen dieser Funktionen nicht mehr diese einfache Struktur auf. So hätte z.B. die Funktion map example für den Datentyp

datatype (α, β)example = C (α → bool) α (β list)
| D ((α, β)example)

nicht den Typ

(α → γ) → (β → γ′) → (α, β)example → (γ, γ′)example sondern

((α → bool) → (δ → bool)) → (α → δ) → (β → δ′) → (α, β)example → (δ, δ′)example

Da derartige Datentypen mit dem oben angegebenen allgemeinen Typschema nicht so gut vereinbar sind und daher deren Handhabung technisch aufwendiger wäre, beschränkt man sich in [Völker, 1995, Völker, 1997] auf reine Datentypen.

Beispiel 6.1 Wir wollen nun Beispiel 3.5 aus Abschnitt 3.3 erneut betrachten, wobei wir diesmal die kompakte Induktionsregel und die mit Hilfe von map formulierten charakteristischen Gleichungen für den Rekursionskombinator verwenden werden. Wir benötigen nun nur noch eine Substitutionsfunktion

subst term :: (α → (α, β)term) → (α, β)term → (α, β)term

die sich durch die Gleichungen

subst term f (Var a)  = f a
subst term f (App b ts) = App b (map (subst term f ) ts)

charakterisieren läßt. Wir definieren also

subst term f ≡ term rec f (λb, xs, ys. App b ys)

woraus sich die obigen Gleichungen sofort ableiten lassen. Als Beweisziel wählen wir nun

subst term (subst term f_{1} ∘ f_{2}) t = subst term f_{1} (subst term f_{2} t)

Mit Hilfe der alternative Induktionsregel erhalten wir durch Induktion über t die Beweisziele

(1) ∀a. subst term (subst term f_{1} ∘ f_{2}) (Var a) = subst term f_{1} (subst term f_{2} (Var a))
(2) ∀b, ts. list all (λu. subst term (subst term f_{1} ∘ f_{2}) u =

subst term f_{1} (subst term f_{2} u)) ts ⟹ subst term (subst term f_{1} ∘ f_{2}) (App b ts) = subst term f_{1} (subst term f_{2} (App b ts))

Beweisziel (1) läßt sich leicht mit Hilfe der charakteristischen Gleichungen für subst term lösen. Zum Beweis von (2) werden die beiden Lemmata

map (f ∘ g) xs = map f (map g xs)  (map compose)
list all (λx. f x = g x) xs ⟹ map f xs = map g xs  (list all map eq)

verwendet, die sich leicht mittels Induktion über xs zeigen lassen. Aus der Prämisse

list all (λu. subst term (subst term f_{1} ∘ f_{2}) u = subst term f_{1} (subst term f_{2} u)) ts von Beweisziel (2) erhalten wir wegen (list all map eq) somit

map (subst term (subst term f_{1} ∘ f_{2})) xs = map (λu. subst term f_{1} (subst term f_{2} u)) xs

was aufgrund der Definition von ∘ gleichbedeutend ist mit

map (subst term (subst term f_{1} ∘ f_{2})) xs = map (subst term f_{1} ∘ subst term f_{2}) xs (⋆)

Wir erhalten schließlich

subst term (subst term f_{1} ∘ f_{2}) (App b ts)

= {charakteristische Gleichungen für subst term}

App b (map (subst term (subst term f_{1} ∘ f_{2})) ts)

= {(⋆)}

App b (map (subst term f_{1} ∘ subst term f_{2}) ts)

= {(map compose)}

App b (map (subst term f_{1}) (map (subst term f_{2}) ts))

= {charakteristische Gleichungen für subst term}

subst term f_{1} (subst term f_{2} (App b ts))

womit Beweisziel (2) gelöst ist. □

Offensichtlich sind für den effektiven Einsatz der kompakten Induktionsregel entsprechende Hilfstheoreme für map, list all etc. nützlich, da sie in einigen Beweisen eine zusätzliche Induktion über Listen ersparen. Beim Beweis von komplexeren Eigenschaften kann jedoch u.U. eine zusätzliche Induktion über Listen notwendig sein.

6.3 Alternative Konstruktionsverfahren

Auch bei der Konstruktion der repräsentierenden Mengen von verschachtelt rekursiven Datentypen wird in [Völker, 1995, Völker, 1997] ein etwas anderer Weg beschritten. Zur Repräsentation von Datentypen wird zunächst, aufbauend auf dem in 4.2.1 dargestellten Universum, manuell der Datentyp

datatype α univ = ONE
| LEAF α
| SCONS (α univ) (α univ)
| IN0 (α univ)
| IN1 (α univ)
| WRAP nat (α univ)

konstruiert. Die Konstruktoren LEAF, SCONS, IN0 und IN1 haben den gleichen Zweck wie die entsprechenden Funktionen aus Abschnitt 4.2.1. Der Konstruktor ONE wird zur Darstellung nullstelliger Konstruktoren verwendet. Auf den Konstruktor WRAP wird später genauer eingegangen. Die Tatsache, daß α univ selbst ein Datentyp ist, hat gegenüber dem relativ allgemeinen Universum aus 4.2.1 den Vorteil, daß auf α univ Funktionen mittels primitiver Rekursion definiert werden können, die dann bei der Konstruktion von repräsentierenden Mengen zum Einsatz kommen.

Berechnung von Repräsentationen Wir wollen zunächst voraussetzen, daß der Typ (α, β)term bereits durch die Angabe einer repräsentierenden Menge term rep set vom Typ ((α + β)univ)set definiert wurde und die Funktionen

Rep term :: (α, β)term → (α + β)univ
Abs term :: (α + β)univ → (α, β)term

sowie

Rep list :: γ list → γ univ

zur Verfügung stehen. Für die Definition des Konstruktors App mit den Argumenten b :: β und ts :: ((α, β)term)list muß nun die Repräsentation von ts berechnet werden. Dies geschieht mit Hilfe der Funktionen Rep list, Rep term und map. Die Grundidee hierbei ist, zunächst die Repräsentation aller Listenelemente und dann die Repräsentation der Gesamtliste zu berechnen:

Rep list (\overbrace{map Rep term ts}^{((α+β)univ)list})

((α+β)univ)univ

Hierdurch erhält man nun allerdings ein Element des Typs ((α + β)univ)univ. Die Elemente von term rep set müssen jedoch den Typ (α+β)univ besitzen. Um dieses Problem zu beheben, wird in [Völker, 1997] die injektive Funktion

flat univ :: (δ univ)univ → δ univ

eingeführt. Der Name wurde dabei in Anlehnung an die bekannte Funktion flat für Listen gewählt. Die Funktion flat univ wird nun mittels primitiver Rekursion auf univ durch die Gleichungen

flat univ ONE  = ONE
flat univ (LEAF u)  = WRAP 0 u
flat univ (SCONS v_{1} v_{2}) = SCONS (flat univ v_{1}) (flat univ v_{2})
flat univ (IN0 v)  = IN0 (flat univ v)
flat univ (IN1 v)  = IN1 (flat univ v)
flat univ (WRAP n v) = WRAP (Suc n) (flat univ v)

definiert. Als Argumente des Konstruktors LEAF auftretende Elemente u vom Typ δ univ werden hierbei – mit dem Index 0 versehen – mit Hilfe des Konstruktors WRAP ”eingepackt“. Um Kollisionen mit bereits früher ”eingepackten“ Elementen zu vermeiden, werden deren Indizes inkrementiert. Die Injektivität von flat univ wird hierbei durch die Angabe einer entsprechenden Umkehrfunktion

expand univ :: δ univ → (δ univ)univ

nachgewiesen, die die Eigenschaft

expand univ (flat univ u) = u besitzt, was sich mittels Induktion über u zeigen läßt. Die Funktion expand univ wird ebenfalls mittels primitiver Rekursion durch die Gleichungen

expand univ ONE  = ONE
expand univ (LEAF a)  = arbitrary
expand univ (SCONS u_{1} u_{2}) = SCONS (expand univ v_{1}) (expand univ v_{2})
expand univ (IN0 u)  = IN0 (expand univ u)
expand univ (IN1 u)  = IN1 (expand univ u)
expand univ (WRAP n u) = if n = 0 then LEAF u else

WRAP (n − 1) (expand univ u)

definiert. Mit Hilfe von flat univ erhalten wir nun die Repräsentation der Liste ts vom Typ ((α, β)term)list durch

flat univ (\underbrace{Rep list (\overbrace{map Rep term ts}^{((α+β)univ)list})}_{((α+β)univ)univ})

(α+β)univ

Die Repräsentationsfunktion wird hierbei also ausschließlich aus bereits vorhandenen Funktionen zusammengesetzt. Dies setzt natürlich voraus, daß für alle beteiligten Typen t eine Funktion Rep t existieren muß. Um Typen wie α × β in Datentypdefinitionen verwenden zu können, muß daher zunächst manuell eine geeignete Repräsentationsfunktion Rep prod definiert werden.

Repräsentierende Menge Die repräsentierende Menge term rep set wird nun induktiv durch die Regeln

IN0 (LEAF (Inl a)) ∈ term rep set

xs ∈ list set term rep set IN1 (SCONS (LEAF (Inr b)) (flat univ (Rep list xs)))

definiert, wobei die monotone Funktion list set durch

list set  :: γ set → (γ list)set
list set S ≡ {xs | set of list xs ⊆ S}

definiert ist. Mit xs ∈ list set term rep set wird also ausgedrückt, daß xs :: ((α + β)univ)list eine Liste ist, deren Elemente aus der Menge term rep set stammen.

Schlußbemerkungen

Induktive Datentypen sind für viele Spezifikationsaufgaben von Bedeutung. So können z.B. Ausdrücke einer Programmiersprache oder Datenstrukturen für Algorithmen durch induktive Datentypen modelliert werden. Mit dem im Rahmen dieser Diplomarbeit implementierten Datentyppaket sind die wichtigsten in der Praxis vorkommenden Fälle wie verschränkt und verschachtelt rekursive Datentypen abgedeckt. Durch die definitorische Vorgehensweise ist die Korrektheit der abgeleiteten Regeln sichergestellt.

7.1 Ausblick auf coinduktive Datentypen

Gelegentlich kann es hilfreich sein, auch Datentypen mit Elementen unendlicher Tiefe zur Verfügung zu haben. Bei der Spezifikation verteilter, reaktiver Systeme treten beispielsweise sehr oft unendliche Abläufe auf. Die Komponenten eines solchen Systems lassen sich als sogenannte stromverarbeitende Funktionen auffassen. Eine Möglichkeit ist es, Datenströme durch unendliche Listen α llist mit den Konstruktoren

LNil :: α llist
LCons :: α → α llist → α llist

darzustellen [Paulson, 1997]. Die in Kapitel 3 beschriebenen Methoden der strukturellen Induktion und der primitiven Rekursion sind typischerweise nur für induktive Datentypen anwendbar, da diese nur Elemente endlicher Tiefe besitzen. Im Gegensatz dazu gibt es Listen xs :: α llist mit der Eigenschaft

xs = LCons x xs

Wie in Abschnitt 3.1 erwähnt wurde, ist dieser Fall für endliche Listen α list durch das Prinzip der strukturellen Induktion ausgeschlossen.

Für Datentypen wie α llist, die in der Literatur oft auch als coinduktive Datentypen bezeichnet werden, existieren andere Beweisprinzipien und Methoden zur Definition rekursiver Funktionen. Die Gleichheit zweier Listen xs und ys des Typs α llist kann durch Angabe einer geeigneten Bisimulation, d.h. einer speziellen Relation r :: (α llist × α llist)set nachgewiesen werden, die das Paar (xs, ys) enthält. Diese Methode wird auch im Kontext von Prozeßalgebren wie CCS [Milner, 1989] zum Nachweis der Äquivalenz zweier Prozesse verwendet. Zur Definition rekursiver Funktionen existiert das Prinzip der Corekursion. Die Definition primitiv rekursiver Funktionen auf endlichen Listen α list ist eingabeorientiert, d.h. abhängig von der Gestalt der als Funktionsargument angegebenen Liste erfolgt eine bestimmte Ausgabe. Im Gegensatz dazu werden corekursive Funktionen ausgabeorientiert definiert: Das Funktionsergebnis ist stets eine potentiell unendliche Liste vom Typ α llist, wobei eine Fallunterscheidung danach erfolgt, ob eine leere Liste LNil oder eine Liste der Gestalt LCons x xs als Ergebnis geliefert wird. Dieser Umstand führt gelegentlich zu etwas unnatürlichen Definitionen. Besonders schwierig zu definieren sind Funktionen wie filter: Um zu entscheiden, ob das Ergebnis nun die Gestalt LNil oder LCons x xs hat, muß um eine unbekannte Anzahl von Elementen ”vorausgeschaut“ werden.

Verschiedene Möglichkeiten der Definition von filter mittels Corekursion werden in der Dissertation von Olaf Müller [Müller, 1998] beschrieben. Diese Arbeit enthält auch einen Vergleich von mehreren, teilweise auf coinduktiven Datentypen basierenden Formalisierungen unendlicher Listen, wobei deren Eignung für die Verifikation verteilter Systeme genauer untersucht wird. In [Paulson, 1997] wird beschrieben, wie coinduktive Datentypen, ebenfalls aufbauend auf dem in 4.2.1 beschriebenen Universum für rekursive Datentypen, in HOL definitorisch konstruiert werden können. Auch diese dort beschriebenen Konstruktionsverfahren könnten in Form eines Datentyppakets implementiert werden.

In diesem Zusammenhang ist insbesondere interessant, inwieweit sich die in Kapitel 4 beschriebenen Verfahren zur Konstruktion verschränkt und verschachtelt rekursiver Typen auch auf coinduktive Datentypen anwenden lassen. Bislang unklar ist, wie induktive und coinduktive Datentypen sinnvoll kombiniert werden können und welche Beweisprinzipien hierfür geeignet sind.

7.2 Weitere Arbeitspunkte

Im Zusammenhang mit dem implementierten Datentyppaket sind für die Zukunft noch folgende weitere Arbeitspunkte denkbar:

• Standardfunktionen für Datentypen wie z.B. t map und t all sowie geeignete Hilfstheoreme könnten vom Datentyppaket bereitgestellt werden.

• Für verschachtelt rekursive Datentypen könnte eine kompakte Induktionsregel, wie in Abschnitt 6.2 beschrieben, abgeleitet werden.

• Von Konrad Slind [Slind, 1996] wurde für HOL ein Paket namens TFL entwickelt, das die Definition von Funktionen mittels fundierter Rekursion erlaubt. Da hiermit momentan keine Funktionen auf verschränkt oder verschachtelt rekursiven Datentypen definiert werden können, wäre es wünschenswert, dieses Paket dahingehend zu erweitern. Hierbei ist von Interesse, ob die Funktionsdefinitionen dabei wie bisher auf den allgemeinen Kombinator wfrec für fundierte Rekursion abgestützt werden sollten, oder ob eine induktive Definition des Funktionsgraphen, wie dies in Abschnitt 4.6.2 für primitive Rekursion dargestellt wurde, evtl. einfacher ist.

Anhang A

Häufig verwendete HOL-Regeln

Regeln für ∃_{1}

P a [P x]_{x} ⋮ . x = a ∃_{1}x. P x (ex1I)

∃_{1}x. P x

[P x ∀y. P y ⟹ y = x]_{x}

⋮ . Q

Q

(ex1E)

Regeln für range

b = f x ; b ∈ range f (range eqI)

b ∈ range f [b = f x]_{x} ⋮ . P

P

(rangeE)

Regeln für ε P (εx. P x) = ∃x. P x (select eq Ex)

∃_{1}x. P x P a

(εx. P x) = a

(select1 equality)

Regeln für inv

inj f ⟹ inv f (f x) = x (inv f f)
y ∈ range f ⟹ f (inv f y) = y  (f inv f)

Anhang B

Beweislaufzeit einiger Datentypen

Die folgende Tabelle zeigt die Beweislaufzeit für einige ausgewählte Datentypen. Es sind hierbei Laufzeiten sowohl für das im Rahmen dieser Arbeit implementierte Datentyppaket für Isabelle/HOL als auch für das von John Harrison implementierte Datentyppaket für HOL Light angegeben. Isabelle/HOL wurde hierbei mit dem New Jersey SML Compiler (Version 110.7) übersetzt. Die Werte wurden auf einer Sun Ultra-2 Workstation mit 512 MB Hauptspeicher ermittelt. Die Laufzeiten für HOL Light wurden von John Harrison mit CAML Light auf einem Pentium II mit einer Taktfrequenz von ca. 200-300 MHz ermittelt.

Konstruk- Verschrän- Verschach-  Gesamtlaufzeit [s]
Beschreibung  toren  kungen  telungen Isabelle HOL Light
Datentypen für krypto-  34  -  -
graphisches Protokoll  24  3  -  133.37  76.13
3  -  -
8  -  -
8  -  -
68000 Instruction Set  2  -  - 1281.42  498.53
14  -  -
10  -  -
98  -  -
SML Grammatik  62  13  10 2759.88  3243.61
Verilog Grammatik  124  15  11 17516.06  15267.35

Bei der Definition der Verilog Grammatik mit Isabelle wurde eine maximale Prozeßgröße von ca. 300 MB ermittelt. Sind für ein Testbeispiel mehrere Zeilen angegeben, so bedeutet dies, daß das Beispiel aus mehreren Datentypen (d.h. einem großen und einigen wesentlich kleineren) bestand, für die eine gemeinsame Zeit ermittelt wurde.

Nach der Integration des neuen Datentyppakets war keine signifikante Verlängerung der Übersetzungszeit von Isabelle/HOL festzustellen, da hierbei nur relativ kleine Datentypen vorkommen. Größere Datentypen benötigen mit dem neuen Paket natürlich signifikant länger als mit dem alten axiomatischen Paket. Für den interaktiven Gebrauch ist jedoch nützlich, daß die charakteristischen Eigenschaften von Datentypen durch Setzen des Flags quick and dirty als Axiome eingeführt werden können, wobei die obigen Beispiele wesentlich weniger Zeit benötigen (7 s, 42 s, 34 s und 110 s).

Anhang C

Bewiesene Theoreme

Für die verschränkt rekursiven Datentypen t_{1}, …, t_{n} werden die folgenden Theoreme bewiesen und in der Theorie gespeichert:

• t_{1} … t_{n}.induct Simultane Induktionsregel für die Datentypen t_{1}, …, t_{n}

• t_{1} … t_{n}.recs Charakteristische Gleichungen für Rekursionskombinatoren

• t_{1} … t_{n}.size Charakteristische Gleichungen für Maßfunktion size für fundierte Rekursion (siehe [Slind, 1996])

Für jeden Datentyp t_{j} werden die folgenden Theoreme bereitgestellt:

• t_{j} .exhaust

Fallunterscheidungsregel für den Datentyp t_{j}

• t_{j} .cases

Charakteristische Gleichungen für case-Kombinator des Datentyps t_{j}

• t_{j} .distinct

Verschiedenheits-Theoreme für Konstruktoren des Datentyps t_{j}

• t_{j} .inject

Injektivitäts-Theoreme für Konstruktoren des Datentyps t_{j}

• t_{j} .case cong

case-Kongruenz-Theorem (siehe [Slind, 1996])

• t_{j} .nchotomy

Alternatives Fallunterscheidungstheorem (siehe [Slind, 1996])

Literaturverzeichnis

[Church, 1940] Alonzo Church. A Formulation of the Simple Theory of Types. Journal of Symbolic Logic, 5, pp. 56–68, 1940.

[Gordon, Melham, 1993] M. J. C. Gordon and T. F. Melham (eds.). Introduction to HOL: A theorem proving environment for higher order logic, Cambridge University Press, 1993.

[Gunter, 1992] Elsa L. Gunter. Why We Can’t have SML Style datatype Declarations in HOL, in Higher Order Logic Theorem Proving and its Applications: Proceedings of the IFIP TC10/WG10.2 International Workshop, Leuven, September 1992, edited by L. J. M. Claesen and M. J. C. Gordon, IFIP Transactions A-20 (North-Holland, 1993), pp. 561-568.

[Gunter, 1993] Elsa L. Gunter. A Broader Class of Trees for Recursive Type Definitions for HOL, in Higher Order Logic Theorem Proving and its Applications: 6th International Workshop, HUG’93, Vancouver, B.C., August 11-13 1993: Proceedings, edited by J. J. Joyce and C.-J. H. Seger, Lecture Notes in Computer Science, vol. 780, Springer-Verlag, 1994, pp. 141-154.

[Harrison, 1995] John Harrison. Inductive Definitions: automation and applications, in Higher Order Logic Theorem Proving and Its Applications: 8th International Workshop, Aspen Grove, Utah, September 1995: Proceedings, edited by E. T. Schubert, P. J. Windley, and J. Alves-Foss, Lecture Notes in Computer Science, Volume 971 (Springer-Verlag, 1995), pp. 200-213.

[Hensel, Jacobs, 1997] Ulrich Hensel and Bart Jacobs, Proof Principles for Datatypes with Iterated Recursion. In E. Moggi and G. Rosolini (eds), Category Theory and Computer Science, LNCS 1290, p. 220-241, Springer-Verlag, 1997.

[Melham, 1989] T. F. Melham, Automating Recursive Type Definitions in Higher Order Logic, in Current Trends in Hardware Verification and Automated Theorem Proving, edited by G. Birtwistle and P. A. Subrahmanyam (Springer-Verlag, 1989), pp. 341-386.

[Milner, 1989] Robin Milner. Communication and Concurrency. Prentice-Hall, 1989.

[Müller, 1998] Olaf Müller. A Verification Environment for I/O Automata Based on Formalized Meta-Theory. Dissertation, Technische Universität München, 1998.

[Paulson, 1989] Lawrence C. Paulson. The foundation of a generic Theorem Prover. Journal of Automated Reasoning, 5(3), pp. 363–397, 1989.

[Paulson, 1990] Lawrence C. Paulson. A formulation of the simple theory of types (for Isabelle). In P. Martin-Löf and G. Mints, editors, COLOG-88: International Conference on Computer Logic, Tallin, Estonian Academy of Sciences. LNCS 417, 1990.

[Paulson, 1993a] Lawrence C. Paulson. Introduction to Isabelle. Technical Report 280, University of Cambridge, Computer Laboratory, 1993. Aktuelle Version erhältlich unter

http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/

[Paulson, 1993b] Lawrence C. Paulson. The Isabelle Reference Manual. Technical Report 283, University of Cambridge, Computer Laboratory, 1993. Aktuelle Version erhältlich unter

http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/

[Paulson, 1993c] Lawrence C. Paulson. Isabelle’s Object-Logics. Technical Report 286, University of Cambridge, Computer Laboratory, 1993. Aktuelle Version erhältlich unter

http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/

[Paulson, 1994] Lawrence C. Paulson. A fixedpoint approach to implementing (co)inductive definitions. In Alan Bundy, editor, Proceedings of the 12th International Conference on Automated Deduction, pages 148-161, Nancy, France, June 1994. Springer-Verlag LNAI 814.

[Paulson, 1997] Lawrence C. Paulson. Mechanizing coinduction and corecursion in higherorder logic. Journal of Logic and Computation, 7(2):175-204, March 1997.

[Slind, 1996] Konrad Slind. Function Definition in Higher Order Logic, in Theorem Proving in Higher Order Logics: 9th International Conference, Turku, Finland, August 1996: Proceedings, edited by J. von Wright, J. Grundy, and J. Harrison, Lecture Notes in Computer Science, Volume 1125 (Springer-Verlag, 1996), pp. 381-397.

[Völker, 1995] Norbert Völker. On the Representation of Datatypes in Isabelle/HOL. In Lawrence C. Paulson (Ed.), Proceedings of the First Isabelle Users Workshop, University of Cambridge Computer Laboratory, Technical Report 379, 1995.

[Völker, 1997] Norbert Völker. Über Datentypen und die Verifikation reaktiver Systeme in HOL. Dissertation, Fernuniversität Hagen, 1997.