Gödel, Escher, Bach, Isabelle

Sofie Czernik, Christoph Lüth

Sommersemester 1998 Geschichte

• Früheste Anfänge: Frege, Hilbert’s Programm (vor 1900)

• λ-Kalkül (Church, 1931)

• Edinburgh LCF (Milner, Gordon, Wadsworth; 1979)

• HOL (Gordon), Nuprl (Constable), Isabelle (Paulson, Nipkow)

• Andere Ansätze: PVS, Typentheorie (Lego, Alf, Coq), Algebra (Boyer-Moore, Nqthm), diverse automatische Theorembeweiser.

C. Lüth  Gödel, Escher, Bach, Isabelle  1

• Implementierung einer Logik erfordert formalen Rahmen (Meta-Logik)

• Anforderung: einfach, aber mächtig

• Hier: Intuitionistische Logik höherer Stufe

Implikation ==>  P Q, P ⟹ Q
Allquantor !! ⋀
Gleichheit  == ≡

• Einfach getypter λ-Kalkül für die Syntax:

Applikation P Q  P Q
Bindung  %x.P x λx.P (x)
C. Lüth  Gödel, Escher, Bach, Isabelle  2

Isabelle’s Objektlogiken • Zermelo-Fränkel-Mengenlehre

• Prädikatenkalkül erster Stufe (klassisch/intuitionistisch)

• Sequenzenkalkül LK (Gentzen, 1934)

• Typentheorie (Martin-Löf, 1972)

• LCF (Logic of Computable Functions; Scott, 1969)

• … und HOL: klassische Logik höherer Stufe (Church, 1940)

C. Lüth  Gödel, Escher, Bach, Isabelle  3

Isabelle/HOL: Grundoperatoren

Negation  not ¬
Wahr  True ⊤
Falsch  False ⊥
Allquantor  !  ∀
Existenzquantor  ?  ∃
Eindeutige Existenz  ?! ∃!
Hilbert-Operator  @  ε
Gleichheit  =  =
Konjunktion  &  ∧
Disjunktion  |  ∨
Implikation  --> →

ferner Funktionskomposition, Fallunterscheidung, Let-Blöcke Isabelle/HOL: Regeln

t = t refl          \begin{matrix}s = t & P (s) \\ P (t) \end{matrix} subst          ⋀ x.f(x) = g(x) ; λx.f(x) = λx.g(x) ext

{P (x) \atop P (εx.P (x))} selectI            P Q ; P → Q impI            \begin{matrix}P → Q & P \\ Q \end{matrix} mp

P = ⊤ ∨ P = ⊥ True or False                     {x = y \atop x ≡ y} eq reflection

(P → Q) → (Q → P) → (P = Q) iff

C. Lüth  Gödel, Escher, Bach, Isabelle  5

Isabelle/HOL: Definitionen

⊤ ≡ λx.x = λx.x
⊥ ≡ ∀P.P
∀P ≡ P = λx.⊤
∃P ≡ P (εx.P (x))
¬P ≡ P → ⊥
P ∧ Q ≡ ∀R.(P → Q → R) → R
P ∨ Q ≡ ∀R.(P → R) → (Q → R) → R
∃!P ≡ ∃x.P (x) ∧ (∀y.P (y) → y = x)

Isabelle/HOL: Beweisregeln I

{s = t \atop t = s} sym    \begin{matrix}r = s & s = t \\ r = t \end{matrix} trans

{P (x) \atop ∃P} exI      \begin{aligned}∃P & ⋀ x.P (x) ; Q \\ & Q \end{aligned} ; exE

⋀ x.P (x) ; ∀P allI      {∀P \atop P (x)} spec

C. Lüth  Gödel, Escher, Bach, Isabelle  7

Isabelle/HOL: Beweisregeln II

\begin{matrix}P Q & {Q \atop P} \\ P = Q \end{matrix} iffI    \begin{aligned}P = Q & \begin{aligned}P → Q & & Q → P \\ & R \end{aligned} \\ & R \end{aligned} ; iffE

      \begin{matrix}P = Q & P \\ Q \end{matrix} iffD1      \begin{matrix}P = Q & Q \\ P \end{matrix} iffD2

          P ⊥ ; ¬P notI            \begin{aligned}P & ¬P \\ & R \end{aligned} notE        {¬¬P \atop P} notnotD

C. Lüth  Gödel, Escher, Bach, Isabelle  8

Isabelle/HOL: Beweisregeln III

 \begin{matrix}P & Q \\ P ∧ Q \end{matrix} conjI  {P ∧ Q \atop P} conjunct1    {P ∧ Q \atop Q} conjunct2    \begin{matrix}P ∧ Q & \begin{aligned}P & & Q \\ & R \end{aligned} \\ R \end{matrix} ; conjE

 {P \atop P ∨ Q} disjI1   {Q \atop P ∨ Q} disjI2   \begin{aligned}P ∨ Q & & P R & {Q \atop R} \\ & R \end{aligned} disjE

C. Lüth  Gödel, Escher, Bach, Isabelle  9

Isabelle/HOL: Der Hilbert-Operator

• Der Hilbert-Operator macht HOL klassisch:

           ¬P ∨ P excluded middle   \begin{aligned}P Q & & {¬P \atop Q} \\ & Q \end{aligned}case split thm

Nützlich für Fallunterscheidungen:

      fun case_tac a = res_inst_tac [("P",a)] case_split_thm;

• Wird auch benutzt, um Undefiniertheit zu modellieren: undef ⇔ εx.⊤

C. Lüth  Gödel, Escher, Bach, Isabelle  10

Unifikation

• Gegeben zwei Terme t_{1}, t_{2}. Der Unifikator von t_{1}, t_{2} ist eine Substitution σ der Meta-Variablen in t_{1}, t_{2} so daß σ(t_{1}) = σ(t_{2}).

• Für Logik erster Stufe: Unifikation ist entscheidbar. Kleinster Unifikator ist eindeutig, falls er existiert.

• Hier: Logik höherer Stufe Unifikation im Allgemeinen unentscheidbar. Mehrere kleinste Unifikatoren möglich.

• Aber: für Terme in bestimmter Form entscheidbar (Nipkow), in linearer Zeit.

Vorwärtsresolution

• RS, RSN scheitern bei mehrdeutigem Unifikator:

- refl RS exI handle e=> print_exn e;
Exception THM 1 raised:
RSN: multiple unifiers
?t = ?t, ?P ?x ==> ? x. ?P x

• Abhilfe: RL: thm list * thm list -> thm list
- [refl] RL [exI];
val it = ["? x. x  [term]",
          "?t3 ?x =?= ?t2 ?x ==> ? x. ?t3 x = ?t2 x"] : thm list

Meta-Implikation und Meta-Quantoren

• Meta-Annahmen können während des Beweises als Theoreme benutzt werden; werden nicht im Beweiszustand angezeigt

• goal gibt Meta-Annahmen zurück, premises: unit-> thm list liefert Meta-Annahmen des aktuellen Beweises

• Meta-Quantoren: Behandlung von Eigenvariablenbedingungen.

• Beweiszustand ist ein Meta-Theorem der Form

{Φ_{1}, …, Φ_{n} \atop Φ}

C. Lüth  Gödel, Escher, Bach, Isabelle  13

Rückwärtsresolution I

• Gegeben Beweiszustand {Φ_{1}, …, Φ_{n} \atop Φ} und (ggf. gelifteter) Regel {Ψ_{1}, …, Ψ_{n} \atop Ψ} mit Unifikator σ(Ψ) = σ(Φ_{i}).

• Bei Rückwärtsresolution auf Ziel i neuer Beweiszustand:

{σ(Φ_{1}), …, σ(Ψ_{1}), …, σ(Ψ_{n}), …, σ(Φ_{n}) \atop σ(Φ)}

C. Lüth  Gödel, Escher, Bach, Isabelle  14

Rückwärtsresolution II

• Problem: Unfikation kann mehrere Lösungen haben

• Lösung: Beweiszustand ist eine Sequenz (lazy list) der möglichen Unifikatoren

• back: unit-> unit erzeugt nächstes Element der Sequenz

• Beispiel: Beweis von sym.

C. Lüth  Gödel, Escher, Bach, Isabelle  15

Rückwärtsresolution III: Lifting

• Problem: Regeln wie impI oder allI haben nicht-atomare Prämissen.

• Lösung: “Lifting” von Regeln

– (P ⟹ Q) ⟹ P → Q wird zu (Φ ⟹ P ⟹ Q) ⟹ (Φ ⟹ P → Q)

– ⋀ x.P x ⟹ P x wird zu ⋀ yx.P′yx ⟹ ⋀ P′y

• Bei Unifikation wird, wenn nötig, die erste Regel geliftet.

C. Lüth  Gödel, Escher, Bach, Isabelle  16

Eliminations-Rückwärtsresolution

• In Isabelles Regel conjE wird P ∧Q nie “aufgebraucht” und sammelt sich im Beweiszustand an; vgl. Sequenzenkalkül:

{Γ, P, Q, Δ ⊢ Ψ \atop Γ, P ∧ Q, Δ ⊢ Ψ} ∧ − I

• Eliminationsrückwärtsresolution auf Ziel i versucht zusätzlich Ψ_{1} durch Annahme zu beweisen

• Beispiel: Beweis von P (εx.P x) = ∃x.P x Destruktions-Rückwärtsresolution

• Destruktive Regeln: \begin{matrix}P → Q & P \\ Q \end{matrix} mp {P ∧ Q \atop P} conjunct1

• Destruktionsregeln besser für Vorwärtsresolution geeignet als Eliminationsregeln, einfacher herzuleiten, aber nicht so allgemein.

• Jede Destruktionsregel kann zu einer Eliminationsregel transformiert werden.

• Destruktionsresolution transformiert erst die Regel und wendet dann Eliminationsresolution an.

C. Lüth  Gödel, Escher, Bach, Isabelle  18

Basistaktiken

• Beweis durch Annahme: assume tac : int -> tactic
• Rückwärtsresolution: resolve tac : thm list-> int-> tactic
• Elim-Resolution: eresolve tac : thm list-> int-> tactic
• Destruktive Resolution: dresolve tac : thm list-> int-> tactic
• Definition auf/zufalten: rewrite goals tac: thm list-> tactic, (sel-
  tener) fold goals tac: thm list-> tactic

C. Lüth  Gödel, Escher, Bach, Isabelle  19

Theoreme gesucht & gefunden

• In der HTML-Dokumentation.

• findI : int-> (string* thm) list

Auf i-tes Subgoal anwendbare Einführungsregeln.

• findE: int -> int-> (string* thm) list

Auf die n-te Prämisse des i-ten Subgoals anwendbare Eliminationsregeln.

• findEs : int-> (string* thm) list

Auf das i-te Subgoal anwendbare Eliminationsregeln.

Nützliche Abkürzungen

• ba i für by (atac i) für by (assume tac i)
• br th i für by (rtac th i) für by (resolve tac [th] i)
• be th i für by (etac th i) für by (eresolve tac [th] i)
• bd th i für by (dtac th i) für by (dresolve tac [th] i)
• bw th für rewrite goals tac [th] i

C. Lüth  Gödel, Escher, Bach, Isabelle  21

Isabelle’s Typsystem

• Typen sind Mengen von Termen, z.B. (in ML) int, bool, string (Basistypen), int-> string, bool* string (zusammengesetzte Typen)

• Isabelle’s Typsystem hat

– Polymorphie erlaubt Typvariablen: In 'a list kann 'a durch jeden anderen Typ ersetzt werden. (Abstraktion über Typen).

– Typklassen erlauben ”kontrolliertes Überladen“ von Operationen, z.B. Klasse aller Typen mit einer Operation = :: ['a, 'a]

==> bool

Selbstdefinierte Typen und Klassen in Isabelle

• Typen durch Typkonstruktoren

• Klassen stehen in Subklassenbeziehung

• Axiomatische Typklassen Isabelle/HOL’s Typsystem I

• Basisklassen:

– prop und bool Formeln der (Meta-)Logik

– logic Beliebige andere Ausdrücke

– term < logic Alle HOL-Terme

• Typkonstruktoren:

– => ::(term, term) term

C. Lüth  Gödel, Escher, Bach, Isabelle  24

Isabelle/HOL’s Typsystem II

• Vordefinierte Typklassen:

– plus < term, + :: ['a::plus, 'a] => 'a
– minus < term, - :: ['a::plus, 'a] => 'a
– times < term, * :: ['a::plus, 'a] => 'a
– ord < term, <, <= :: ['a::ord, 'a] => bool

Typvariablen, Klassen und Sorten • Typ eines Ausdrück wird durch Typinferenz bestimmt.

• Typvariablen werden durch Sorten (Mengen von Klassen) eingeschränkt.

C. Lüth  Gödel, Escher, Bach, Isabelle  26

Beispiele

• a+ b= b+ a
Typen: a, b :: 'a
Sorten : 'a :: plus

• a- b< a- b
Typen: a, b :: 'a
Sorten: 'a :: {minus, ord}

• a
Typen: a :: bool

Tips & Tricks

• Achtung: Typisierung beeinflußt Unifikation und Anwendbarkeit von Regeln!

• Inferierte Typen und Sorten ausgeben:

  show sorts:= true, show types:= true

• Achtung: die arithmetischen Operatoren +, -, * sind überladen!

  goal Arith.thy "a+b= b+a" dann sind a, b :: 'a :: plus

• Explizite Annotierung von Typen und Sorten:

  goal Arith.thy "a+b= b+(a::nat)"

Theorien: Logiken selbst definiert

• Theorien enthalten Definitionen von – Elterntheorien;

– Klassendeklarationen, Sorten;

– Konstanten in Mixfix-Deklaration, Konstantendefinitionen;

– Regeln (Axiome)

Theorien: externe Repräsentation • Textdateien mit der Endung .thy

• Lesen mit use thy

• Format:

Name = T_{1}+ T_{2}+ T_{3}+ … + Keyword_{1} Definitions _{1} Keyword_{2} Definitions _{2} Keyword_{3} Definitions _{3} … end

Bestandteile von Theorien • consts — Konstantendeklarationen (Typ und Syntax)

• rules — Axiome

• defs — Definitionen

• datatype — Datentypdefinitionen

• primrec — Primitiv rekursive Funktionen

C. Lüth  Gödel, Escher, Bach, Isabelle  31

Taktiken

• Taktiken verändern den Beweiszustand. Jeder Beweiszustand wird auf eine Sequenz möglicher Folgezustände abgebildet:

  type tactic = thm -> thm Seq.seq;

• Taktiken sind entweder Basistaktiken oder können mit Tacticals kombiniert werden.

• Taktiken werden mit by: tactic-> unit angewandt.

• back: unit-> unit und undo: unit-> unit sind keine Taktiken.

C. Lüth  Gödel, Escher, Bach, Isabelle  32

Basistaktiken: Resolution und Beweis durch Annahme

• Rückwärtsresolution  resolve_tac  : thm list-> int-> tactic
Eliminationsresolution eresolve_tac : thm list-> int-> tactic
Destruktive Resolution eresolve_tac : thm list-> int-> tactic
Vorwärtsresolution:  forward_tac  : thm list-> int-> tactic

• Wie oben, aber mit Instantiierung:

res_inst_tac  : (string* string) list-> thm -> int-> tactic
eres_inst_tac : (string* string) list-> thm -> int-> tactic
dres_inst_tac : (string* string) list-> thm -> int-> tactic
forw_inst_tac : (string* string) list-> thm -> int-> tactic

• Beweis durch Annahme: assume_tac, eq_assume_tac: int-> tactic

Weitere Taktiken

• cut_facts_tac: thm list-> int-> tactic fügt Theoreme als zusätz-

liche Prämissen im i-ten Subgoal ein.

• thin_tac: string-> int-> tactic löscht die (als String angebenen) Prämissen des i-tes Subgoal.

• rotate_tac: int-> int-> tactic “rotiert” die Annahmen des i-ten Subgoals um n Stellen.

Automatisches Beweisen: Simplifikation

• Simplifikation ist Termersetzung.

• Theoreme der Form t ≡ u werden zu Regeln t → u, Theoreme der Form P ⇒ t ≡ u werden zu bedingten Regeln P ⇒ t → u.

• Simplifikation des i-ten Subgoals mit dem Simplikationsset der

aktuellen Theorie:  Simp_tac : int-> tactic
. . . mit lokalen Prämissen:  Asm_simp_tac : int-> tactic

… mit Vereinfachung der Präm.: Full_simp_tac : int-> tactic

alles zusammen:  Asm_full_simp_tac : int-> tactic

• trace_simp : bool ref um angewandte Regeln anzuzeigen.

Automatisches Beweisen: Klassische Beweiser • Simuliert Sequenzenkalkül in Isabelle.

• Sichere vs. unsichere, Introduktions vs. Eliminationsregeln.

• Blast_tac: int-> tactic Schnell & mächtig.
• Fast_tac, Best_tac: int-> tactic Tiefen- bzw. Breitensuche.

• Auto_tac: int-> tactic kombiniert klass. Bew. und Simplifikation.

C. Lüth  Gödel, Escher, Bach, Isabelle  36

Tacticals I

• THEN  : tactic* tactic-> tactic

Wendet erst t_{1} an, und dann t_{2};

• ORELSE: tactic* tactic-> tactic

Wendet erst t_{1} an, und genau wenn das fehlschlägt, t_{2}.

• EVERY: tactic list-> tactic

EVERY[t_{1}, …, t_{n}] = t_{1} THEN … THEN t_{n}

• FIRST: tactic list-> tactic

FIRST[t_{1}, …, t_{n}] = t_{1} ORELSE … ORELSE t_{n} Tacticals II: Repetition, Repetition, Repetition

• TRY : tactic-> tactic wendet Taktik höchstens einmal an;

• REPEAT : tactic-> tactic wendet Taktik auf Beweiszustand an, und rekursiv auf jedes Element der resultierenden Beweiszustände (evtl. gar nicht).

• Varianten: REPEAT_DETERM (rekursiv nur auf den Kopf der Sequenz anwenden), REPEAT1: tactic-> tactic (mindestens einmal anwenden).

• Vorsicht: REPEAT muß nicht termininieren!

Tacticals III: Ein Subgoal, viele Subgoals

• SELECT_GOAL:tactic-> int-> tactic wendet Taktik auf das i-te Sub-

goal an. Scheitert, falls es kein Subgoal gibt, oder Maingoal verändert wird. Nützlich für Termersetzung.

• ALLGOALS : (int-> tactic)-> tactic wendet Taktik, die ein Sub-

goal als Parameter hat, auf alle Subgoals an.

• TRYALL, SOMEGOAL, FIRSTGOAL,  REPEAT_SOME, REPEAT_FIRST

Frei erzeugte Datentypen

• Schlüsselwort datatype, Notation á la ML.

• Definition primitiv rekursiver Funktionen mit primrec.

• Erweitert Simplifikationsmenge der momentanen Theorie.

• Erzeugt Taktiken für Fallunterscheidung und Induktion.

C. Lüth  Gödel, Escher, Bach, Isabelle  40

Frei erzeugte Datentypen: Theoreme & Taktiken

• Definition von Typ t erzeugt Struktur t mit folgendem: – distinct : thm list Disjunktheit der Konstruktoren – inject : thm list Injektivität der Konstruktoren – cases : thm list Vollständige Fallunterscheidung

– simps : thm list = inject + distinct + cases

– induct : thm Induktionstheorem

– induct_tac : string-> int-> tactic  Induktionstactic

C. Lüth  Gödel, Escher, Bach, Isabelle  41

Primitiv rekursiv definierte Funktionen • Schlüsselwort primrec

• Für jeden Konstruktor C eine Reduktionsregel:

fx_{1} … x_{m}(Cy_{1} … y_{k})z_{1} … z_{n} = E

E kann rekursive Aufrufe von f in der Form f … y_{i} … enthalten.

• Beispiel: rev für Listen.

• Beweisprinzip: strukturelle Induktion

C. Lüth  Gödel, Escher, Bach, Isabelle  42

Wohlfundierte Rekursion

• Format: recdef f R simpset S r_{1} … r_{n} wobei f :: τ → σ

• r_{1} … r_{n}: Reduktionsregeln der Form ft = E, wobei t ein pattern sein kann, und E rekursive Aufrufe von f enthalten kann, aber mit kleineren Argumenten (Terminationsbedingung).

• Wohlfundierte Rekursionsordnung R :: (τ × τ)set, u.a.:

less_than : < auf natürlichen Zahlen

measure f : f :: τ → nat, und x ≺ y iff f(x) < f(y)

• Simplifikationsmenge S für Wohlfundiertheit und Termination Tour de HOL

• Muttertheorie: HOL

• Nat — natürliche Zahlen, Arith— Arithmetik

• Set — Mengen in HOL (Menge = Prädikat)

• Prod — Kartesisches Produkt, Sum — Summen von Typen

• Relation — Relationen ((α × β)set)

• List — Listen

C. Lüth  Gödel, Escher, Bach, Isabelle  44