Induktive Prädikate und die zugehörigen induktiven Beweise sind das A und ? im maschinengestützten interaktiven Beweisen, etwa mit dem Theorembeweisprüfer Isabelle. Daher biete Isabelle auch eingebaute Unterstützung bei der Definition und Verwendung eines induktiven Prädikats. So definiert

inductive rel :: "[nat] => bool" where
  | rel1 : "rel [1]"
  | rel2 : "rel (x # z) ==> rel (x + 1 # x # z)"

ein induktives Prädikat, und

lemma rel_sorted: "rel l => sorted (rev l)"
proof (induction)
case rel1 
case rel2 
qed.

beweist etwas per Induktion.

Will man nämlich nun das Prädikat noch um einen weiteren Fall

   | rel3: "(x # y # z)  ==> rel (x + y # x # z)"

erweitern, so muss man ein neues induktives Prädikat definieren, die anderen Introduktionsregeln wie auch die zugehörigen Beweise in rel_sorted kopieren, oder die vorhandenen Beweiseschritte kopieren.

In dieser Masterarbeit soll eine Modularisierung von induktiven Prädikaten entwickelt werden, die dies vermeidet. Eine mögliche Syntax könnte dabei wie folgt aussehen

open inductive rel :: "[nat] => bool"
open inductive rule rel1 : "rel [1]"
open inductive rule rel2 : "rel (x # z) ==> rel (x + 1 # x # z)"

open lemma rel_sorted for rel "rel l ==> sorted (rev l)"

open case rel_sorted for rel1
  

open case rel_sorted for rel2
  

close inductive real_rel_A = rel1 | rel2

open inductive rule rel2 : rel3: "(x # y # z) ==> rel (x + y # x # z)"
open case rel_sorted for rel3
  

close inductive real_rel_A = rel1 | rel2 | rel3

Diese Modularisierung erlaubt es auch, induktive Prädikate und deren Beweise neu zu strukturieren. Wo man bisher die Konjunktion zweier Aussagen induktiv beweisen musste, kann nun im Befehl "open case" explizit angegeben werden, welche Aussagen für die Annahmen der induktiven Regel vorausgesetzt werden. Erst der "close inductive"-Befehl prüft die Beweise auf Vollständigkeit und setzt sie geeignet zusammen. Auch Implikationen zwischen Prädikaten, die es erlauben eine schwächere Aussage von stärkeren Annahmen zu zeigen, könnte in diese Maschinerie eingebaut werden. Weiter kann wechselseitige Rekursion zwischen mehreren induktiven Prädikaten ad-hoc im Befehl "open case" verwendet werden.

Eine weitere mögliche und wichtige Erweiterung ist, diese Modularisierung auch für induktive Datentypen (datatype) zu ermöglichen, die ja auch aus mehr oder weniger unabhängigen Fällen und zugehörigen Induktionsregeln bestehen. Hier ist auch zu überlegen, wie rekursive Funktionsdefinitionen erweiterbar zu gestalten sind.

Aufgabe:

Sie arbeiten die theoretischen Grundlagen hinter dieser Syntax aus, und beschreiben die generierten Beweisobligationen und induktiven Prädikate sowie die Kombination dieser beim Erzeugen der tatsächlichen Definition und beim Beweisen der tatsächlichen Aussagen.

Sie konkretisieren die Syntax für dieses Feature.

Weiter arbeiten Sie sich in die Programmierung mit ML ein und machen sich mit der Code-Basis von Isabelle und der Implementierung des "inductive"-Befehls und der "induction"-Methode vertraut. Darauf hin implementieren sie obiges Feature in Isabelle.

Sie dokumentieren die neuen Befehle und mit einem oder mehreren geeigneten Beispielen evaluieren Sie die Nützlichkeit und Praktikabilität dieses Ansatz und zeigen seine Grenzen und Einschränkungen auf.

Sie diskutieren die möglichen Erweiterungen und ggf. implementieren diese sogar.

Voraussetzungen

Sie haben mit Isabelle gearbeitet, sind mit funktionaler Programmierung vertraut und können sich selbstständig in komplexe System einarbeiten.

Schlüsselworte

Isabelle 

Veröffentlichungen

Veröffentlichung

Open Inductive Predicates

Betreuer

Ehemalige Mitarbeiter
Dr. rer. nat. Joachim Breitner

Studenten

Ehemalige Studenten
Richard Molitor