Zusammenfassung

  • Eine Edinburgh-LCF-Taktik zerlegte ein Ziel in Teilziele und lieferte eine Validierung. Erst wenn diese aus anerkannten Teilziel-Theoremen mittels primitiver Schlussregeln das Ausgangstheorem erzeugte, war das Ergebnis angenommen.
  • Der abstrakte Typ thm verkleinerte den Codebereich mit direkter Theorem-Autorität. Er bewies weder die Konsistenz der Logik noch die Angemessenheit der Spezifikation oder die Fehlerfreiheit von Compiler, Laufzeit und Hardware.
  • Die Entwicklung war Teamarbeit: Dana Scott lieferte die zugrunde liegende Logik; Stanford LCF kam zuerst; Michael Gordon, Christopher Wadsworth, Lockwood Morris, Malcolm Newey und weitere Forschende wirkten an Edinburgh LCF und ML mit.

Sucherfolg ist kein Theorem

Interaktives Beweisen arbeitet häufig rückwärts. Aus einem Ziel erzeugt eine Taktik kleinere Teilziele, probiert Umformungen, kombiniert Verfahren und verwirft erfolglose Wege. Ein ausführliches Protokoll kann überzeugend aussehen. Für LCF blieb jedoch eine andere Frage maßgeblich: Lässt sich der behauptete Satz über die geschützte Schnittstelle tatsächlich konstruieren?

Die Taktik gab neben den Teilzielen eine Validierung zurück. Diese Funktion erwartete die Theoreme der Teilziele und musste daraus das Theorem des ursprünglichen Ziels bilden. Damit wurde die rückwärts gerichtete Suche später durch eine vorwärts gerichtete Ableitung eingelöst. Versagte die Validierung, war die Erfolgsmeldung wertlos.

Das löste einen Zielkonflikt. Ein erweiterbarer Beweiser braucht neue, von Nutzern geschriebene Verfahren. Solcher Code kann fehlerhaft sein. Könnte jede Erweiterung eigenmächtig Theoreme erzeugen, würde die Vertrauensfläche mit jeder Taktik wachsen. Edinburgh LCF kapselte Theoreme daher in einem abstrakten Typ, üblicherweise thm, und erlaubte nur Axiomen und primitiven Schlussregeln, Werte dieses Typs zurückzugeben.

Die Taktiken wurden dadurch nicht korrekt. Sie konnten divergieren, schlechte Teilziele wählen, Ausnahmen auslösen oder eine unbrauchbare Validierung liefern. Die engere Zusage lautete: Ein Fehler außerhalb der Schnittstelle eröffnet keinen zweiten Konstruktor. Er führt im Regelfall dazu, dass das verlangte Theorem nicht entsteht.

Von Stanford nach Edinburgh – mit mehreren Urhebern

Milner beschrieb 1972 einen implementierten Prüfer für Dana Scotts Logic for Computable Functions. Stanford LCF zeigte die Möglichkeit maschineller Beweisunterstützung, aber lange Beweise waren mühsam und speicherintensiv. Nach Milners Wechsel nach Edinburgh 1973 entstand eine programmierbarere Umgebung.

Das Standardwerk von 1979 wurde von Michael J. C. Gordon, Robin Milner und Christopher P. Wadsworth verfasst. Der ML-Aufsatz von 1978 nennt zusätzlich Lockwood Morris und Malcolm Newey. Rückblicke von Larry Paulson und Gordon zeichnen die Linie weiter zu Cambridge LCF, HOL und Isabelle. Milners zentrale architektonische Einsicht rechtfertigt keine Alleinzuschreibung von ML, Taktiken oder interaktivem Beweisen.

ML hieß zunächst „Meta Language“ und diente der Programmierung von Beweisverfahren. Sein polymorphes Typsystem wurde später zu einer eigenständigen Leistung. Milners Arbeit von 1978 formulierte semantische und syntaktische Soundness-Ergebnisse und beschrieb einen bereits in Edinburgh LCF eingesetzten Inferenzalgorithmus. Der Turing-Preis von 1991 würdigte LCF, ML und CCS; die technische Entstehung bleibt dennoch kollektiv.

Schlussregeln arbeiteten vorwärts, von vorhandenen Theoremen zu einem neuen. Taktiken arbeiteten rückwärts, vom Ziel zu Teilzielen. Die Validierung verband beide Richtungen. Tacticals kombinierten Taktiken als Folge, Wiederholung oder Auswahl; sie erweiterten die Steuerung der Suche, nicht die primitiven Wahrheiten.

Was der abstrakte Typ leistet – und was nicht

Ein abstrakter Datentyp verbirgt seine Darstellung und stellt nur ausgewählte Operationen bereit. Gewöhnlicher Code darf einen thm-Wert weiterreichen, aber nicht dessen interne Felder bearbeiten und daraus einen neuen Wert fälschen. Die Typabstraktion sichert diese Trennung.

Die Prüfung kann sich dadurch auf einen kleineren Satz von Axiomen und Regelimplementierungen konzentrieren. Neue Automation darf kompliziert sein, weil ihr Ergebnis weiterhin denselben Annahmeweg nehmen muss. Komplexer Code und Code mit unmittelbarer Zulassungsmacht sind nicht mehr deckungsgleich.

Ein „kleiner Kern“ bedeutet jedoch nicht „kein Vertrauen“. Die Regeln müssen für die gewählte Logik gültig sein. ML-Implementierung, Compiler und Laufzeit müssen die Abstraktion erhalten. Unsichere Sprachmittel oder Hardwarefehler können die Voraussetzung verletzen. Auch Parser und Drucker können Nutzer über den tatsächlich gespeicherten Term täuschen. Die Vertrauensbasis wird verkleinert, nicht abgeschafft.

Kern-Soundness ist außerdem nicht dasselbe wie logische Konsistenz. Dass ein Wert nur durch bestimmte Funktionen entstand, ist eine Herkunftsaussage. Es beweist nicht unabhängig, dass jede Funktion eine gültige Schlussregel umsetzt. Ebenso belegt ein Satz über ein Modell nicht, dass das Modell eine reale Anlage, eine Vorschrift oder menschliche Absicht zutreffend erfasst. Ein fehlerfreier Kern kann die falsche formale Frage tadellos beantworten.

Validierung als aufgeschobene Verpflichtung

Mit ihren Teilzielen verspricht die Taktik, dass deren Theoreme für das Ausgangsziel genügen. Die Validierung muss dieses Versprechen später mit anerkannten Regeln erfüllen. Ein Ziel bloß aus der Benutzeroberfläche zu entfernen, ist kein Beweis.

Wenn Tacticals Suchverfahren zusammensetzen, werden auch ihre Validierungen zusammengesetzt. Die Steuerungsebene kann sehr groß werden, doch die Annahmekette führt weiterhin zu primitiven Operationen zurück. Protokoll, Skript und grüner Status erklären Aktivität; sie besitzen nicht dieselbe Autorität wie der erzeugte Theoremwert.

HOL und Isabelle erbten Teile der Idee, aber nicht dieselbe Architektur. Paulson beschreibt für Isabelle eine gemeinsame Repräsentation von Regeln und Beweiszuständen und damit andere Grundlagen als beim klassischen LCF. Andere Systeme speichern Beweisterme oder exportieren Zertifikate. Coq und typentheoretische Assistenten ziehen ihre Grenze anders. Taktiken allein machen ein System nicht zu LCF.

Quellen und Grenzen

Der Text ist eine historische Architekturanalyse, kein Audit eines heutigen Beweisers und keine Messung der Kerngröße. Die Verbindung zu einer minimalen, lokal prüfbaren gemeinsamen Regel bei offenen künftigen Methoden ist eine redaktionelle Anwendung von Lu Hengs Prinzip einer minimalen Anfangsspezifikation; sie wird Milner nicht als institutionelle Position zugeschrieben.