Theory SchnelleinstiegHOL

theory SchnelleinstiegHOL
  imports Main BeispielTac
begin

section‹Schnelleinstieg Isabelle/HOL›

subsection‹Beweise›
text‹Die besondere Fähigkeit im Beweisassistent Isabelle/HOL liegt darin,
maschinengeprüfte Beweise zu machen.

Beispiel:›

lemma ‹3 = 2+1› by simp

text‹In der PDFversion wird der eigentliche Beweis ausgelassen.
Aber keine Sorge, der Computer hat den Beweis überprüft.
Würde der Beweis nicht gelten, würde das PDF garnicht compilieren.

Ich wurde schon für meine furchtbaren Beweise zitiert.
Ist also ganz gut, dass wir nur Ergebnisse im PDF sehen und der eigentliche Beweis ausgelassen ist.
Am besten kann man Beweise sowieso im Isabelle Editor anschauen und nicht im PDF.

Wir werden die meisten Hilfsfakten als @{command lemma} kennzeichnen.
Wichtige Fakten werden wir @{command theorem} nennen.
Zusätzlich führen wir noch das @{command beispiel} Kommando ein,
um Lemmata von Beispielen zu unterscheiden.

Folgende drei Aussagen sind alle equivalent und maschinengeprüft korrekt:
›


lemma ‹3 = 2+1› by simp
theorem ‹3 = 2+1› by simp
beispiel ‹3 = 2+1› by simp

text‹Freitext, so wie der aktuelle Satz, sind nicht (oder nur minimal) maschinell geprüft.›


subsection‹Typen›
text‹Typen werden per ▩‹::› annotiert.
Beispielsweise sagt ⬚‹3::nat›, dass \<^term>‹3::nat› eine natürliche Zahl (Typ \<^typ>‹nat›) ist.›

text‹Einige vordefinierte Typen in Isabelle/HOL:

  ▪ Natürliche Zahlen. Typ \<^typ>‹nat›.
    Beispielsweise  \<^term_type>‹0 :: nat›, \<^term_type>‹1 :: nat›,
    \<^term_type>‹2 :: nat›, \<^term_type>‹3 :: nat›.
    Auf natürlichen Zahlen ist die Nachfolgerfunktion \<^const>‹Suc› definiert.
    Beispielsweise ist @{lemma ‹Suc 2 = 3› by simp}.
  ▪ Ganze Zahlen. Typ \<^typ>‹int›.
    Beispielsweise  \<^term_type>‹0 :: int›, \<^term_type>‹1 :: int›,
    \<^term_type>‹-1 :: int›, \<^term_type>‹-42 :: int›.
  ▪ Listen. Typ \<^typ>‹'α list›.
    Beispielsweise  \<^term_type>‹[] :: nat list›, \<^term_type>‹[] :: int list›,
    \<^term_type>‹[0, 1, 2, 3] :: nat list›, \<^term_type>‹[0, 1, -1, -42] :: int list›.
  ▪ Strings. Typ \<^typ>‹string›.
    Beispielsweise  \<^term_type>‹''Hello, World'' :: string›.
›


subsection‹Mehr Typen›
text‹Jeder Typ der mit einem einfachen Anführungszeichen anfängt ist ein polymorpher Typ.
Beispiel: \<^typ>‹'a› oder \<^typ>‹'α›.
So ein Typ ist praktisch ein generischer Typ,
welcher durch jeden anderen Typen instanziiert werden kann.


Beispielsweise steht \<^typ>‹'nat› für einen beliebigen Typen,
während \<^typ>‹nat› der konkrete Typ der natürlichen Zahlen ist.

Wenn wir nun ⬚‹3::'a› schreiben handelt es sich nur um das generische Numeral 3.
Das ist so generisch, dass z.B. noch nicht einmal die Plusoperation darauf definiert ist.
Im Gegensatz dazu ist ⬚‹3::nat› die natürliche Zahl 3,
mit allen wohlbekannten Rechenoperationen.
Im Beweis obigen ⬚‹lemma‹3 = 2+1›› hat Isabelle die Typen automatisch inferiert.
›

subsection‹Noch mehr Typen›
text‹Eigene Typen können unter Anderem mit dem Keyword @{command datatype} eingeführt werden.
Im folgenden Beispiel führen wir einen @{command datatype} für Farben ein.›

datatype beispiel_farbe = Rot | Gruen | Blau

text‹Eine variable \<^term_type>‹x :: beispiel_farbe› kann entweder den Wert
\<^const>‹Rot›, \<^const>‹Gruen›, oder \<^const>‹Blau› haben.
Dies lässt sich auch beweisen:›

beispiel‹x = Rot ∨ x = Gruen ∨ x = Blau›
  by(cases ‹x›, auto)

text‹Wir können auch einen Schritt weitergehen und eine Liste von \<^typ>‹beispiel_farbe›
selbst implementieren.›

datatype beispiel_farbe_liste = FLLeer | FLKopf ‹beispiel_farbe› ‹beispiel_farbe_liste›

text‹Eine \<^typ>‹beispiel_farbe_liste› ist hier rekursiv definiert:

  ▪ Entweder ist die Liste \<^const>‹FLLeer› und enthält keine Elemente.
  ▪ Oder es gibt bereits eine \<^typ>‹beispiel_farbe_liste› und über den \<^const>‹FLKopf›
    Konstruktor hängen wir eine weitere \<^typ>‹beispiel_farbe› an.
    Die Abkürzung \<^const>‹FLKopf› steht hier für Farben-Listen-Kopf.

Beispielsweise können wir immer länger werdende
\<^typ>‹beispiel_farbe_liste›n welche nur \<^const>‹Rot›e Elemente enthalten wie folgt konstruieren:

  ▪ \<^term>‹(FLLeer) :: beispiel_farbe_liste› enthält 0 Elemente.
  ▪ \<^term>‹(FLKopf Rot FLLeer) :: beispiel_farbe_liste› enthält ein \<^const>‹Rot› Element.
  ▪ \<^term>‹(FLKopf Rot (FLKopf Rot FLLeer)) :: beispiel_farbe_liste›
     enthält zwei \<^const>‹Rot› Elemente.
  ▪ \<^term>‹(FLKopf Rot (FLKopf Rot (FLKopf Rot FLLeer))) :: beispiel_farbe_liste›
     enthält drei \<^const>‹Rot› Elemente.
›

text‹Das Konzept Liste kann weiter verallgemeinert werden.
Wir können eine generische Liste bauen, welche nicht nur \<^typ>‹beispiel_farbe›n aufnehmen kann,
sondern eine polymorphe Liste,
welche beliebige Typen speichern kann.
›

datatype 'α beispiel_liste = Leer | Kopf ‹'α› ‹'α beispiel_liste›

text‹Der Typ \<^typ>‹'α› steht hierbei für einen Platzhalter für beliebige Typen.
Beispielsweise können wir mit der generischen \<^typ>‹'α beispiel_liste› wieder unsere
\<^typ>‹beispiel_farbe_liste› simulieren:

  ▪ \<^term_type>‹(Leer) :: beispiel_farbe beispiel_liste› enthält 0 Elemente.
  ▪ \<^term_type>‹(Kopf Rot Leer) :: beispiel_farbe beispiel_liste›
    enthält ein \<^const>‹Rot› Element.
  ▪ \<^term_type>‹(Kopf Rot (Kopf Rot Leer)) :: beispiel_farbe beispiel_liste›
     enthält zwei \<^const>‹Rot› Elemente.
  ▪ \<^term_type>‹(Kopf Rot (Kopf Rot (Kopf Rot Leer))) :: beispiel_farbe beispiel_liste›
     enthält drei \<^const>‹Rot› Elemente.

Die Liste kann jedoch auch andere Typen von Elementen speichern.

  ▪ \<^term_type>‹(Kopf 2 (Kopf 1 (Kopf 0 Leer))) :: nat beispiel_liste›
  ▪ \<^term_type>‹(Kopf ''Erstes Element'' (Kopf ''Letzes Element'' Leer)) :: string beispiel_liste›
›

text‹Die Länge einer \<^typ>‹'α beispiel_liste› lässt sich über folgende rekursive Funktion
wie folgt definieren:›

fun beispiel_liste_laenge :: ‹'α beispiel_liste ⇒ nat› where
  ‹beispiel_liste_laenge Leer = 0›
| ‹beispiel_liste_laenge (Kopf _ ls) = Suc (beispiel_liste_laenge ls)›

text‹Funktionen werden oft über Pattern-Matching implementiert,
d.h., dass der gegebene Datentyp zerlegt wird und eine Fallunterscheidung getroffen wird.

  ▪ Für den Basisfall \<^const>‹Leer› wird \<^term>‹0::nat› zurückgegeben.
  ▪ Für den rekursiven Fall \<^term>‹Kopf› in dem wir ein Kopfelement haben
    welches wir ignorieren und einer Folgeliste \<^term>‹ls::'α beispiel_liste›
    rufen wir \<^const>‹beispiel_liste_laenge› rekursiv mit der Folgeliste auf und geben den
    Nachfolger der so berechneten Zahl zurück.›

beispiel ‹beispiel_liste_laenge Leer = 0›
  by eval
beispiel ‹beispiel_liste_laenge (Kopf Rot (Kopf Rot (Kopf Rot Leer))) = 3›
  by eval

text‹Zusätzlich können den einzelnen Feldern in Datentypen spezielle Namen gegeben werden.
Beispielsweise:›

datatype 'α beispiel_liste_mit_namen =
    LeerMN | KopfMN (kopfelement: ‹'α›) (schwanzliste: ‹'α beispiel_liste_mit_namen›)

text‹Der Fall \<^const>‹LeerMN› bleibt unverändert.
Um Verwechslung zu vermeiden haben wir den einzelnen Fällen das Suffix MN (Mit-Namen)
gegeben, da die Konstruktoren \<^const>‹Leer› und \<^const>‹Kopf› bereits durch das vorherige Beispiel
definiert sind.
Im \<^const>‹KopfMN›-Fall haben nun die einzelnen Felder Namen.›

beispiel‹kopfelement (KopfMN Rot LeerMN) = Rot› by simp
beispiel‹schwanzliste (KopfMN Rot LeerMN) = LeerMN› by simp

text‹Die von Isabelle mitgelieferte Standardimplementierung einer Liste
sieht unserem Beispiel recht ähnlich,
allerdings liefert Isabelle noch zusätzlichen Syntactic Sugar um Listen komfortabler darzustellen.
Die Implementierung einer Liste in der Standardbibliothek ist: \<^datatype>‹list››


subsection‹Funktionen›
text‹Beispiel:
Eine Funktionen welche eine natürliche Zahl nimmt und
eine natürliche Zahl zurück gibt (\<^typ>‹nat ⇒ nat›):›

fun beispielfunktion :: ‹nat ⇒ nat› where
  ‹beispielfunktion n = n + 10›


text‹Funktionsaufrufe funktionieren ohne Klammern.›

beispiel ‹beispielfunktion 32 = 42› by eval

text‹Funktionen sind gecurried. Hier ist eine Funktion welche 2 natürliche Zahlen nimmt
und eine natürliche Zahl zurück gibt (\<^typ>‹nat ⇒ nat ⇒ nat›):›
fun addieren :: ‹nat ⇒ nat ⇒ nat› where
  ‹addieren a b = a + b›

beispiel ‹addieren 32 10 = 42› by eval

text‹Currying bedeutet auch, wenn wir \<^const>‹addieren› nur mit einem Argument aufrufen
(welches eine natürliche Zahl \<^typ>‹nat› sein muss),
dass wir eine Funktion zurückbekommen, die noch das zweite Argument erwartet,
bevor sie das Ergebnis zurückgeben kann.

Beispiel: \<^term_type>‹(addieren 10) :: (nat ⇒ nat)›

Zufälligerweise ist \<^term>‹addieren 10› equivalent zu \<^term>‹beispielfunktion›:
›
beispiel ‹addieren 10 = beispielfunktion›
  by(simp add: fun_eq_iff)


text‹Zusätzlich lassen sich Funktionen im Lambda Calculus darstellen.
Beispiel:›

beispiel ‹(λn::nat. n+10) 3 = 13› by eval

beispiel ‹beispielfunktion = (λn. n+10)›
  by(simp add: fun_eq_iff)

text‹Im vorhergehenden Beispiel wurden zwei Funktionen
(die \<^const>‹beispielfunktion› die wir oben definiert haben und ein lambda-Ausdruck)
als equivalent bewiesen.
Dafür wurde die Extensionalität verwendet.›

subsection‹Mengen›
text‹Mengen funktionieren wie normale mathematische Mengen.

Beispiel. Die Menge der geraden Zahlen:
›
beispiel ‹{0,2,4,6,8,10,12} ⊆ {n::nat. n mod 2 = 0}›
  by(simp)

beispiel ‹{0,2,4,6,8,10} = {n::nat. n mod 2 = 0 ∧ n ≤ 10}›
  by fastforce

text‹Bei vorherigen Beispiel können wir das Prinzip der (mathematischen) ∗‹Extensionalität› sehen:
Intensional sind die beiden Mengen \<^term>‹{0,2,4,6,8,10}::nat set› und \<^term>‹{n::nat. n mod 2 = 0 ∧ n ≤ 10}›
verschieden, da sie unterschiedlich definiert sind.
Extensional betrachtet, sind die beiden Mengen jedoch gleich,
da sie genau die gleichen äußeren Eigenschaften haben,
d.h. da sie genau die gleichen Elemente enthalten.›

subsection‹First-Order Logic›
text‹First-Order Logic, oder auch Prädikatenlogik erster Stufe, besteht aus folgenden Symbolen.

  ▪ Konjunktion. Der Term \<^term>‹A ∧ B› besagt, dass sowohl \<^term>‹A› als auch \<^term>‹B› wahr sind.
    Dies entspricht dem logischen "Und".
  ▪ Disjunktion. Der Term \<^term>‹A ∨ B› besagt, dass \<^term>‹A› oder \<^term>‹B› (oder beide) wahr sind.
    Dies entspricht dem logischen "Oder".
  ▪ Negation. Der Term \<^term>‹¬ A› besagt, dass \<^term>‹A› nicht wahr ist.
    Dies entspricht dem logischen "Nicht".
  ▪ Implikation. Der Term \<^term>‹A ⟶ B› besagt, dass wenn \<^term>‹A› gilt dann gilt auch \<^term>‹B›.
    Dies entspricht dem logischen "Wenn-Dann".
    Unsere Mathematik ist hardcore klassisch und es gilt
    @{lemma [break=true] ‹A ⟶ B ⟷ ¬A ∨ B› by blast}.
  ▪ All-Quantifier. Der Term \<^term>‹∀x. P x› besagt, dass \<^term>‹P x› wahr ist für alle \<^term>‹x›.
    Dies entspricht dem logischen "Für-Alle".
  ▪ Existenz-Quantifier. Der Term \<^term>‹∃x. P x› besagt, dass es ein \<^term>‹x› gibt,
    für das \<^term>‹P x› gilt.
    Dies entspricht dem logischen "Es-Existiert".
  ▪ Des Weiteren gibt es noch die Abkürzung @{term [source=true] ‹A ⟷ B›}, welche bedeutet,
    dass \<^term>‹A› genau dann gilt wenn \<^term>‹B› gilt.
    Dies entspricht dem logischen "Genau-Dann-Wenn".
    Genau genommen ist @{term [source=true] ‹A ⟷ B›} eine Abkürzung für \<^term>‹A = B›.
    Oft ist @{term [source=true] ‹A ⟷ B›} praktischer zu schreiben, da es schwächer bindet.
    Genau genommen gilt @{lemma [source=true] ‹(A ⟷ B) = ((A) = (B))› by blast}.
    Die schwache Bindung von @{term [source=true] ‹A ⟷ B›} wird dann relevant,
    wenn \<^term>‹A› und \<^term>‹B› komplizierte Ausdrücke sind,
    da wir uns im Gegensatz zu @{term [source=true] ‹(A) = (B)›} Klammern sparen können.
›

subsection‹Higher-Order Logic (HOL)›
text‹First-Order Logic ist in Higher-Order Logic eingebettet.
Higher-Order Logic (HOL) ist die native Sprache von Isabelle/HOL.
Im Vergleich zur First-Order Logic besteht HOL nur aus zwei essentiellen Symbolen:

  ▪ All-Quantifier. Der Term \<^term>‹⋀x. P x› besagt \<^term>‹∀x. P x›.
    Eigentlich ist zwischen dem First-Order und dem Higher-Order All-Quantifier kein
    wesentlicher Unterschied.
    Genau genommen lässt sich der First-Order All-Quantifier via HOL einführen wie folgt:
    @{thm allI}.
    
    Da mathematisch der Ausdruck \<^term>‹P x› besagt, dass \<^term>‹P› für
    beliebiges \<^term>‹x›---sprich: alle \<^term>‹x›---
    gilt, ist folgendes equivalent:
      ▪ \<^term>‹⋀x. P x›
      ▪ \<^term>‹∀x. P x›
      ▪ \<^term>‹P x›
  ▪ Implikation. Der Term \<^term>‹A ⟹ B› besagt \<^term>‹A ⟶ B›.
    Eigentlich ist zwischen der First-Order und der Higher-Order Implikation kein
    wesentlicher Unterschied.

    Die Implikation assoziiert nach rechts.
    Dies bedeutet @{lemma [source=true] ‹A ⟶ B ⟶ C ⟷ (A ⟶ (B ⟶ C))› by blast}.

    Logisch gilt damit auch folgendes:
    @{lemma [source=true] ‹A ⟶ B ⟶ C ⟷ A ∧ B ⟶ C› by blast}.

    In Isabelle/HOL werden wir viele Lemmata der Form @{term [source=true] ‹A ⟹ B ⟹ C›} sehen,
    welche zu lesen sind als: Aus \<^term>‹A› und \<^term>‹B› folgt \<^term>‹C›.
    Dies ist gleichbedeutend mit \<^term>‹A ∧ B ⟹ C›.
    Da die Higher-Order Implikation einer der Kernbausteine von HOL sind ist die Formulierung
    welche nur die Implikation verwendet sehr praktisch für Isabelle.
›

subsection‹Über Isabelle/HOL›
text‹Isabelle/HOL ist ein interaktiver Beweisassistent und kann
von 🌐‹https://isabelle.in.tum.de/› bezogen werden.

Isabelle stammt aus der Tradition der LCF (Logic for Computable Functions) Theorembeweiser.
Die Standardlogik ist Higher-Order Logic (HOL), welche auf der klassischen Mathematik basiert.

Isabelle basiert auf einem mathematischen Microkernel.
Zum aktuellen Zeitpunkt mit Isabelle2022 befindet sich das Herzstück dieses mathematischen
Microkernels in der Datei 🗏‹~~/src/Pure/thm.ML›, welche aus nur ca 2500 Zeilen ML Code besteht.
Dies ist relativ wenig Code welchem wir vertrauen müssen.
Die Korrektheit aller Ergebnisse und Beweise dieser Theory hängen nur von der Korrektheit dieses
Microkernels ab.

Isabelle/HOL ist ein interaktiver Beweisassistent, was bedeutet,
Isabelle hilft einem Benutzer dabei Beweise zu schreiben.
Alle Beweise müssen von Isabelles Microkernel akzeptiert werden, welcher die Korrektheit garantiert.
Im Gegensatz zu interaktiven Beweisassistenten gibt es auch automatische Theorembeweiser,
wie z.B. Z3.
Z3 besteht aus mehreren hunderttausend Zeilen C Code (🌐‹https://github.com/Z3Prover/z3›)
und ist damit im Vergleich zu Isabelles Microkernel riesig.
Dies bedeutet auch, dass einer riesige Menge an Code vertraut werden muss,
um einem Beweis von Z3 zu vertrauen.
Glücklicherweise arbeiten Isabelle und z.B. Z3 sehr gut zusammen:
Z3 kann losgeschickt werden um einen Beweis zu suchen.
Sobald Z3 meldet, dass ein Beweis gefunden wurde,
akzeptiert Isabelle diesen jedoch nicht blind,
sondern Isabelle akzeptiert den gefundenen Beweis nur,
wenn der Beweis sich gegen Isabelles Microkernel wiedergeben lässt.
Somit kombiniert Isabelle das Beste aus vielen Welten:
Die starke Korrektheitsgarantie eines mathematischen Microkernels der LCF Reihe
mit der Automatisierung der neuesten Generationen von automatischen Theorembeweisern.

Der Unterschied zwischen z.B. Z3 und Isabelle/HOL zeigt sich auch in einigen Beispielen:
Während der Z3 Bugtracker sehr viele Soundness Issues zeigt,
d.h. Fälle in denen Z3 etwas falsches beweisen hat,
hat es meines Wissens nach im Isabelle/HOL Kernel in über 30 Jahren keinen logischen Fehler gegeben,
welcher normale Benutzer betroffen hat.
Natürlich gab es auch in Isabelle/HOL Bugs und in künstlich geschaffenen Grenzfällen
konnte Isabelle überzeugt werden einen falschen Fakt zu akzeptieren,
jedoch handelt es sich hier um wenige Einzelfälle welche speziell konstruiert wurden
um Isabelle anzugreifen -- kein einziger Bug hat unter normalen Umständen zu logischer
Inkonsistenz geführt.
Umgekehrt ist Z3 schnell und automatisch.
Während Isabelle vom Benutzer verlangt, dass Beweise manuell gefunden und formalisiert
werden müssen kann Z3 teils extrem komplizierte Probleme schnell und automatisch lösen.

Isabelle integriert nicht nur mit automatischen Beweisern wie Z3,
Isabelle integriert auch mit automatischen Gegenbeispielsfindern,
wie z.B. @{command quickcheck} oder @{command nitpick}.
Dies bedeutet, sobald der Benutzer einen vermeintlichen Fakt in Isabelle eintippt,
schickt Isabelle Prozesse los um ein Gegenbeispiel zu finden.
Diese so gefundenen Gegenbeispiele sind oft unintuitiv.
Allerdings sind es echte Gegenbeispiele und der Computer erweist sich als
grausamer unnachgiebiger Diskussionspartner.
Dies führt dazu, dass wir nicht mit halbgaren oberflächlichen Argumenten durchkommen.
Oft eröffnen diese automatischen Gegenbeispiele auch eine neue Sicht auf die Dinge
und helfen, die eigenen impliziten Annahmen zu erkennen und zu hinterfragen.
Der Computer erweist sich hier als perfekter logischer geduldiger Diskussionspartner,
denn
"der wahre Philosoph ist gewillt, alle vorgefaßten Meinungen einer Prüfung zu unterziehen"
@{cite russellphi}.
Und da alle Fakten welche wir ultimativ als wahr behaupten wollen durch den mathematischen
Microkernel müssen, sind logische Flüchtigkeitsfehler in unserer Argumentation ausgeschlossen.
Allerdings können wir immer noch falsche Annahmen aufstellen,
auf welche wir unsere Ergebnisse stützen.
Jedoch müssen wir diese Annahmen explizit treffen und aufschreiben,
denn sonst ließe sich nichts beweisen.
›

subsection‹Ist das KI?›
text‹Nein!

Dieser Abschnitt ist etwas opinionated und handwavy.
Wenn aktuell von Künstlicher Intelligenz (KI) gesprochen wird,
wird damit oft Machine Learning gemeint.
Ich kürze Machine Learning absichtlich nicht mit ML ab,
da die Verwechslung mit der Programmiersprache Standard Meta Language (ML)
🌐‹https://de.wikipedia.org/wiki/Standard_ML›
zu groß ist.
Isabelle ist in ML geschrieben und wenn im Umfeld von Isabelle von ML geredet wird,
ist meistens nie Machine Learning gemeint.
Genau genommen benutzt Isabelle die Poly/ML Implementierung,
welche das tollste Logo aller Programmiersprachen hat.›

text_raw‹
  \begin{center}
    \includegraphics[height=0.15\textwidth]{Poly_Parrot3.png}\\
    Poly/ML Logo von polyml.org
  \end{center}
›

text‹
Zurück zum Machine Learning.
Eine der aktuell beliebtesten Implementierungen für maschinelles Lernen sind neuronale Netze.
Dabei wird ein Algorithmus mit einer Unmenge an Trainingsdaten gefüttert,
um ein sogenanntes neuronales Netzwerk zu trainieren.
Ist so ein riesiges Netzwerk einmal trainiert ist es quasi unmöglich auf eine einzelne Zahl
im trainierten Netzwerk zu zeigen und zu verstehen
warum das Netz an genau dieser Stelle diese Zahl hat.
Der Einsatz solcher Methoden um moralische Entscheidungen zu treffen ist meiner Meinung nach
zurecht umstritten.
Insbesondere da die Ausgaben eines neuronalen Netzes auf den Trainingsdaten beruhen.
Wenn die Trainingsdaten bereits von versteckten Vorurteilen durchsetzt sind,
werden diese natürlich auch in das Netz übernommen.


Unser Ansatz der Modellierung in einem Theorembeweiser ist grundverschieden von
Entscheidungsfindungsansätzen basierend auf Machine Learning.

  ▪ ∗‹Axiomatische Grundlage›.
    Machine Learning basiert auf den Trainingsdaten.
    Wenn ein neuronales Netzwerk auf mehreren Milliarden Trainingsdaten basiert,
    ließe sich ketzerisch sagen,
    dass das logische System auf mehreren Milliarden Axiomen beruht.
    Diese Axiomatische Grundlage kann schnell inkonsistent werden
    und es ist unmöglich diese riesige Menge an Axiomen zu hinterfragen.

    Im Gegensatz dazu steht die Anzahl der Axiome in Isabelle/HOL.
    Es handelt sich größtenteils um die gewöhnlichen Axiome der klassischen Mathematik,
    über die sich klassische Mathematiker größtenteils seit über 100 Jahren einig sind
    (🌐‹https://en.wikipedia.org/wiki/Axiom_of_choice› sagt
    "The axiom of choice was formulated in 1904 by Ernst Zermelo").
    Auch ist die Anzahl der Axiome minimal.
    Wenn wir die Isabelle Sources nach dem Kommando @{command axiomatization} durchsuchen,
    finden wir außerhalb von Beispielen nur eine Hand voll Axiomen.
    In diesem Artikel verwenden wir das Kommando @{command axiomatization} gar nicht.
    Hinzu kommen noch axiomatische Konstruktionen,
    wobei jede solche Konstruktion jedoch sehr genau auf ihre Korrektheit geprüft wurde.
    In diesem Artikel führen wir keine neuen axiomatischen Konstruktionen ein
    und verlassen uns komplett auf die Konstruktionen der Standardbibliothek,
    wie z.B. @{command datatype} oder @{command fun}.
  ▪ ∗‹Nachvollziehbarkeit der Ergebnisse›.
    Während es bei einem großen neuronalen Netz nahezu unmöglich ist zu verstehen warum ein
    bestimmter Wert an einer bestimmten Stelle steht und was dies zu bedeuten hat,
    lässt sich dieses Dokument immer wieder neu kompilieren und alle Beweise wiederholen.
    Dabei ließe sich genau nachvollziehen wie ein Fakt es in den Isabelle Microkernel geschafft hat.
    Zusätzlich stellt Isabelle diverse ▩‹trace› Kommandos bereit.
    Es lässt sich also nachvollziehen, warum etwas gilt.
  ▪ ∗‹Vertrauen in die Ergebnisse›.
    Wie bereits erwähnt basiert Isabelle auf einem mathematischen Microkernel,
    wodurch ein extrem hohes Vertrauen in alle Ergebnisse erzielt wird.
    

Allerdings darf Machine Learning uns natürlich beim Beweise- und Gegenbeispiel-Finden helfen;
so angebunden wie automatisierte Beweiser wie Z3.
Das bedeutet, Machine Learning hilft bei der Entwicklung,
trifft jedoch selbst keine Entscheidungen und alle Ergebnisse werden von
Isabelles Kernel überprüft.
›

(*find ./Downloads/Isabelle2022/src/HOL -name "*.thy"  | xargs grep axiomatiz | wc -l*)

subsection‹Deep Embedding vs. Shallow Embedding›
text‹Im Bereich der mathematischen Modellierung wird oft
zwischen Deep Embedding und Shallow Embedding unterschieden.

Deep Embedding bedeutet, dass unsere domänenspezifische Logik komplett in der Meta-Logik
neu implementiert wird.
Die Meta-Logik wird von der domänenspezifischen Logik wegabstrahiert.
In Isabelle/HOL ist die Meta-Logik HOL.
Die domänenspezifische Logik ist unsere Logik mit der wir moralische Schlussfolgerungen
treffen wollen.
Wenn wir unsere "moralische Logik" komplett in HOL deep embedden wollen,
bedeutet dass, dass wir alle Konzepte unserer Logik komplett neu implementieren.
So könnten wir beispielsweise definieren:
⬚‹datatype moralisch = Moralisch | NichtMoralisch›.
Ein Deep Embedding hat den Vorteil, dass wir die Semantik unserer Logik komplett
selbst definieren können.
Wenn sich also HOL und unsere Logik verschieden verhalten sollen, ist ein Deep Embedding
unerlässlich.
Der Nachteil ist allerdings, dass wir alles was wir brauchen selbst definieren müssen
und die wir z.B. nicht von der enormen Menge an Lemmata der Isabelle Standardbibliothek
profitieren.

Im Gegensatz dazu steht ein Shallow Embedding.
Dabei wird die domänenspezifische Logik direkt in der Meta-Logik definiert.
Alle Konzepte der Meta-Logik werden übernommen.
Dies funktioniert nur, wenn sich die Meta-Logik so wie unsere domänenspezifische Logik verhält.
Die Abstraktionsebene die unsere domänenspezifische Logik über die Meta-Logik spannt
wird so dünn wie möglich gehalten und so viele Konzepte wie möglich der Meta-Logik
werden Eins-zu-Eins in der domänenspezifischen Logik übernommen.
Beispielsweise könnten wir uns entscheiden keinen neuen Datentyp ⬚‹datatype moralisch› einzuführen.
Wir könnten einen bestehenden HOL Datentyp weiterverwenden,
beispielsweise ⬚‹type_synonym moralisch = bool›.
Dies funktioniert nur, wenn sich der HOL-Typ \<^typ>‹bool› tatsächlich so verhält,
wie wir es gerne für unseren domänenspezifischen "moralisch" Typen hätten.
Ein riesiger Vorteil ist, dass wir bei einem Shallow Embedding die gesamte
Isabelle/HOL Standardbibliothek an bestehenden Theories und Lemmata weiterverwenden können.
Beispielsweise sind alle Lemmata über \<^typ>‹bool› automatisch für uns verfügbar
und bestehende Beweistaktiken funktionieren automatisch auf bestehenden HOL Typen.

Das Beispiel über ⬚‹datatype moralisch› ist etwas übertrieben
und keine neuen Datentypen einzuführen und nur z.B. ⬚‹type_synonym moralisch = bool›
zu verwenden ist natürlich etwas radikal.
Einem Shallow Embedding ist es nicht verboten neue Datentypen einzuführen
und eine eigene Semantik auf diesen Datentypen zu definieren.
Dennoch gilt der allgemeine Grundsatz für ein Shallow Embedding:
Die Meta-Logik wird so weit weiterverwendet wie möglich.

Wir versuchen in diesem Artikel wann immer möglich ein Shallow Embedding zu machen
und so viel von HOL und Isabelles Standardbibliothek weiterzuverwenden wie möglich.
›


end