Proseminar Perlen der Informatik Professor Tobias Nipkow, PhD

HOL Stefan Richter 22.2.2000

Betreut von Markus Wenzel

1 Was ist HOL 2 Syntax und Semantik 3 Ableitungsregeln 4 Theorien 5 Beispiel: die Theorie PROD 6 Schlussbemerkung

Inhab : Jedes Element von U ist eine nichtleere Menge. Sub : Wenn X ∈ U und ∅ ≠ Y ⊆ X, dann Y ∈ U. Prod : Aus X ∈ U und Y ∈ U folgt X × Y ∈ U. ^{a} Pow : Wenn X ∈ U, dann ist auch die Potenzmenge P(X) = {Y : Y ⊆ X} Element von U. Infty : U enthält eine ausgewiesene unendliche Menge I. Choice : Es existiert ein ausgewiesenes Element ch ∈ Π_{X∈U}X.

aDabei wird das kartesische Produkt X × Y dargestellt durch {(x, y) = {{x}, {x, y}} : x ∈ X ∧ y ∈ Y }.

Aus diesen Regeln lassen sich weitere Eigenschaften ableiten, die für die HOL-Semantik wichtig sind: Da sich Funktionen als Teilmengen von kartesischen Produkten darstellen lassen, folgt aus Sub, Prod und Pow : Fun : Wenn (X ∈ U ∧ Y ∈ U), dann (X → Y ∈ U). Durch Anwendung von Sub auf eine beliebige Menge in U (Infty garantiert die Existenz einer solchen Menge) erhält man ein- bzw. zweielementige Mengen, von denen jeweils eine bestimmte ausgewählt werde: Unit : U enthält die ausgezeichnete einelementige Menge 1 = {0}. Bool : U enthält die ausgewählte zweielementige Menge 2 = {0, 1}.

Typen in HOL:

σ ::= α | c | (σ_{1}, …, σ_{n})op | σ_{1} → σ_{2}

Typvariablen stehen für beliebige Mengen im Universum.

Typkonstanten haben die Form (σ_{1}, …, σ_{n})op und stehen für Funktionen auf Typen. Spezielle:

atomare Typen (Basistypen) Funktionstypen Terme in HOL:

t_{σ} ::= x_{σ} | c_{σ} | (t_{σ′→σ} t′_{σ′})_{σ}
t_{α→β} ::= (λx_{α}.t_{β})_{α→β}

Variablen sind Paare x_{σ} in Indexnotation, wobei x ein Name und σ ein Typ sei. Konstanten c_{σ} sind genau dann gültige Terme, wenn c für ein Element einer Menge steht, von deren Typ σ eine Instanz ist. λ-Abstraktionen (λx_{σ_{1}}.t_{σ_{2}})_{σ_{1}→σ_{2}} bezeichnen totale Funktionen v_{σ_{1}} → t[v/x]_{σ_{2}}, wenn x eine Variable vom Typ σ_{1} und t ein gültiger Term vom Typ σ_{2} ist. Funktionsapplikationen (t_{σ′→σ} t′_{σ′})_{σ} bezeichnen das Ergebnis der Anwendung der Funktion t_{σ′→σ} auf das Argument t′_{σ′} Primitive Konstanten: ⇒: 2 → 2 → 2

(a ⇒ b) = \{ \begin{matrix}0 & falls a = 1 und b = 0 \\ 1 & sonst \end{matrix}

=_{X}: X → X → 2

(x =_{X} y) = \{ \begin{matrix}1 & falls x = y \\ 0 & sonst \end{matrix}

ε : (X → 2) → X

ch_{X}(f) = \{ \begin{matrix}ch(f^{−1}\{1\}) & falls f^{−1}\{1\} ≠ ∅ \\ ch(X) & sonst \end{matrix}

Assumption introduction

\overline{t ⊢ t}

Reflexitivity

\overline{⊢ t = t}

Beta − conversion

\overline{⊢ (λx.t_{1})t_{2} = t_{1}[t_{2}/x]}

Substitution

\frac{Γ_{1} ⊢ t_{1} = t′_{1} ⋯ Γ_{n} ⊢ t_{n} = t′_{n} Γ ⊢ t[t_{1}, …, t_{n}]}{Γ_{1} ∪ ⋯ ∪ Γ_{n} ∪ Γ ⊢ t[t′_{1}, …, t′_{n}]}

Abstraction

\frac{Γ ⊢ t_{1} = t_{2}}{Γ ⊢ (λx.t_{1}) = (λx.t_{2})}

• Wenn x nicht frei in Γ Type instantiation

\frac{Γ ⊢ t}{Γ ⊢ t[σ_{1}, …, σ_{n}/α_{1}, …, α_{n}]}

• Wo t[σ_{1}, …, σ_{n}/α_{1}, …, α_{n}] das Ergebnis der parallelen Ersetzung der Typvariablen α_{1}, …, α_{n} durch Typen σ_{1}, …, σ_{n} in t ist, mit der Einschränkung, daß keine der Typvariablen α_{1}, …, α_{n} in Γ vorkommt.

Discharging an assumption

\frac{Γ ⊢ t_{2}}{Γ\\{t_{1}\} ⊢ t_{1} ⇒ t_{2}}

Modus Ponens

\frac{Γ_{1} ⊢ t_{1} ⇒ t_{2} Γ_{2} ⊢ t_{1}}{Γ_{1} ∪ Γ_{2} ⊢ t_{2}}

Die Theorie LOG:

⊢ T_{bool} = ((λx_{bool}.x) = (λx_{bool}.x))

⊢ ∀_{(α→bool)→bool} = λP_{α→bool}.P = (λx.T)

⊢ ∃_{(α→bool)→bool} = λP_{α→bool}.P (εP)

⊢ F_{bool} = ∀b_{bool}.b

⊢ ¬_{bool→bool} = λb.b ⇒ F

⊢ ∧_{bool→bool→bool} = λb_{1}b_{2}.∀b.(b_{1} ⇒ (b_{2} ⇒ b)) ⇒ b

⊢ ∨_{bool→bool→bool} = λb_{1}b_{2}.∀b.(b_{1} ⇒ b) ⇒ ((b_{2} ⇒ b) ⇒ b)

⊢ One One_{(α→β)→bool} = λf_{α→β}.∀x_{1}x_{2}.(fx_{1} = fx_{2}) ⇒ (x_{1} = x_{2})

⊢ Onto_{(α→β)→bool} = λf_{α→β}.∀y.∃x.y = fx

⊢ Type Definition_{(α→bool)→(β→α)→bool} = λP_{α→bool} rep_{β→α}.One One rep ∧ (∀x.P x = (∃y.x = rep y))

⊢ Inv = λf_{α→β}.λy.εx.y = fx Die Theorie INIT fügt nur die folgenden fünf Axiome der Theorie LOG hinzu:

BOOL CASES AX  ⊢ ∀b.(b = T) ∨ (b = F)
IMP ANTYSIM AX  ⊢ ∀b_{1}b_{2}.(b_{1} ⇒ b_{2}) ⇒ (b_{2} ⇒ b_{1}) ⇒ (b_{1} = b_{2})
ETA AX  ⊢ ∀f_{α→β}.(λx.fx) = f
SELECT AX  ⊢ ∀P_{α→bool}x.P x ⇒ P (εP)
INFINITY AX  ⊢ ∃f_{ind→ind}.One One f ∧ ¬(Ontof)

Eine Konstantendefinition ist eine Formel der Form c_{σ} = t_{σ}, so daß:

1. c ein neuer Name ist

2. t ein geschlossener gültiger Term ist

3. alle Typvariablen in t auch in σ vorkommen

Eine Typdefinition beinhaltet:

1. Spezifizierung eines existierenden Repräsentationstyps

2. Angabe einer Teilmenge davon durch ein Teilmengenprädikat 3. Beweis, daß die Teilmenge nicht leer ist

4. Forderung von Isomophie mittels einer Repräsentationsfunktion Typ-Definition PROD: ⊢ Mk Pair = λab. λxy. (x = a) ∧ (y = b) ⊢ Is Pair = λf. ∃ab. f = Mk Pair a b.

⊢ Type Definition Rep Pair
⊢ Abs Pair = Inv Rep Pair

⊢ Pair = λ x_{α} y_{β}. Abs Pair (Mk Pair x y) ⊢ Fst = λp_{(α,β)prod}. εx. ∃y. p = (x, y) ⊢ Snd = λp_{(α,β)prod}. εy. ∃x. p = (x, y).

⊢ ∀ x y. Fst(x, y) = x

⊢ ∀ x y. Snd(x, y) = y

⊢ ∀ p_{(α,β)prod}. p = (Fst p, Snd p)