Robin Milner arbeitete an drei scheinbar getrennten Fragen: Wie kann ein Computer einen Beweis prüfen, wie kann ein Compiler die Typen eines Programms ableiten und wie lässt sich über mehrere kommunizierende Prozesse nachdenken? Er behandelte sie mit derselben Forderung: Formalismen sollten streng genug sein, um Eigenschaften zu beweisen, und zugleich praktisch genug, um von Informatikern benutzt zu werden.
Daraus entstanden LCF, eine grundlegende Architektur für Beweisassistenten, ML, ursprünglich die Sprache zur Steuerung dieses Systems, sowie CCS und der Pi-Kalkül, zwei wichtige Modelle von Nebenläufigkeit und Interaktion. Der Turing Award 1991 würdigte genau diese breite Wirkung.
Von der Mathematik zur Programmierung
Arthur John Robin Gorell Milner wurde 1934 in Yealmpton im englischen Devon geboren. Nach einem Mathematikstudium in Cambridge arbeitete er unter anderem bei Ferranti und später in Forschung und Lehre, bevor er Anfang der 1970er-Jahre nach Stanford ging.
Komplexere Software stellte die Frage nach Vertrauen. Ein hochautomatisiertes Beweisprogramm konnte selbst einen Fehler enthalten. Milner suchte deshalb einen Mittelweg: Nutzer und Programme sollten Beweise weitgehend automatisiert konstruieren können, das Endergebnis musste aber einen kleinen, kontrollierbaren Prüfmechanismus passieren.
LCF: Vertrauen auf einen kleinen Kern konzentrieren
LCF steht für Logic for Computable Functions. Milner entwickelte 1972 in Stanford ein interaktives Beweissystem auf Grundlage einer Logik von Dana Scott; in Edinburgh wurde das Projekt mit Michael Gordon, Christopher Wadsworth und weiteren Forschern fortgeführt.
Die entscheidende Architektur repräsentiert einen bewiesenen Satz als Wert eines abstrakten Typs. Beliebiger Code kann einen solchen Wert nicht erzeugen. Nur wenige Funktionen, die Axiomen und zulässigen Schlussregeln entsprechen, dürfen dies tun.
Dadurch können Taktiken zur Beweissuche komplex und sogar fehlerhaft sein: Solange sie den abstrakten Theoremtyp nicht umgehen können, führt ein Fehler eher zum Scheitern als zu einem falschen Beweis. HOL und Isabelle übernahmen diesen als LCF-Architektur bekannten Ansatz.
Warum LCF eine neue Sprache brauchte
Nutzer eines Beweisassistenten wollen Strategien programmieren: Ziele zerlegen, Ausdrücke vereinfachen, Regeln ausprobieren und Teilbeweise kombinieren. Dafür entwickelte das Edinburgh-Team eine Metasprache, kurz ML.
ML setzt auf Funktionen als Werte, algebraische Datentypen, Pattern Matching, Rekursion und automatische Speicherverwaltung. Diese funktionale Ausrichtung passt gut zur Transformation von Ausdrücken und zur Komposition von Beweistaktiken. Aus der Sprache eines Spezialwerkzeugs wurde bald eine allgemeine Programmiersprache.
Typinferenz: Garantien ohne ständige Annotationen
Statische Typisierung kann Fehler vor der Ausführung erkennen, doch vollständige Typannotationen machen funktionalen Code schwerfällig. ML löst das mit polymorpher Typinferenz. Der Compiler sammelt die durch Operationen erzeugten Bedingungen und leitet einen möglichst allgemeinen Typ ab.
Eine Identitätsfunktion kann so ohne Annotation den Typ 'a -> 'a erhalten. Die Geschichte des Hindley-Milner-Systems verbindet mehrere Arbeiten: Roger Hindley hatte ein verwandtes Ergebnis in der kombinatorischen Logik erzielt; Milner entwickelte unabhängig ein Typsystem und den praktischen Algorithmus W für ML; Luis Damas untersuchte später mit ihm die theoretischen Eigenschaften, darunter Haupttypen.
Typinferenz beweist nicht, dass ein Algorithmus das beabsichtigte Problem löst. Sie garantiert jedoch Typkonsistenz und verbindet Kürze mit einer starken Klasse statisch erkennbarer Fehler.
Von Edinburgh ML zu Standard ML
Als ML außerhalb von LCF genutzt wurde, entstanden mehrere Dialekte. In den 1980er-Jahren definierte eine Gemeinschaft Standard ML. Neben einer strikt ausgewerteten funktionalen Sprache erhielt es ein ausgearbeitetes Modulsystem mit Strukturen, Signaturen und Funktoren.
Milner spielte mit Mads Tofte, Robert Harper und anderen eine zentrale Rolle bei Entwurf und formaler Definition. Standard ML beeinflusste direkt OCaml; Ideen der ML-Familie finden sich außerdem in Haskell, F#, Rust, Swift und modernen Typsystemen.
CCS: über interagierende Programme nachdenken
Bei nebenläufigen Systemen hängt Verhalten nicht nur von Eingaben und Ausgaben ab, sondern von möglichen Interaktionen. Milner entwickelte den Calculus of Communicating Systems (CCS) als mathematische Sprache dafür.
Prozesse können Aktionen ausführen, zwischen Entwicklungen wählen, parallel laufen und interne Kommunikation verbergen. Mit der Bisimulation lässt sich fragen, ob zwei unterschiedlich aufgebaute Systeme dasselbe beobachtbare Verhalten besitzen: Jede relevante Aktion des einen muss vom anderen passend nachvollzogen werden können.
Der Pi-Kalkül: wenn Verbindungen selbst beweglich werden
Verteilte Systeme verändern ihre Kommunikationsstruktur: Ein Prozess erhält die Adresse eines Dienstes, übergibt einen Kanal oder erzeugt eine private Verbindung. Ende der 1980er- und Anfang der 1990er-Jahre entwickelte Milner mit Joachim Parrow und David Walker den Pi-Kalkül.
Prozesse können darin Kanalnamen kommunizieren. Dadurch kann sich das Netz der Verbindungen während der Berechnung verändern. Der Kalkül modelliert Sitzungen, Fähigkeiten, Rekonfiguration und Mobilität mit wenigen präzisen Konstruktionen.
Berechnung, Beweis und Interaktion verbinden
Milner wechselte 1973 nach Edinburgh und trug dazu bei, die Stadt zu einem Zentrum für Grundlagen der Informatik zu machen. 1995 ging er nach Cambridge und leitete dort von 1996 bis 1999 das Computer Laboratory. Später suchte er mit Bigraphen nach noch allgemeineren Modellen von Ort und Verbindung.
Der rote Faden seiner Arbeit ist eine Wissenschaft des Rechnens, die nicht beim Ergebnis einer Funktion endet. Ein Beweis ist eine kontrollierte Konstruktion, ein Typ eine Einschränkung, ein Prozess durch mögliche Interaktionen bestimmt.
Warum Robin Milner weiterhin wichtig ist
Moderne Sprachen leiten viele Typen automatisch ab, Beweisassistenten verbinden Automatisierung mit kleinen Vertrauenskernen und Verifikationswerkzeuge vergleichen Zustände und Übergänge von Protokollen. Milners Arbeiten halfen, die Grundlagen all dieser Praktiken zu legen.
Seine Laufbahn zeigt außerdem, dass eine spezialisierte Sprache allgemeine Bedeutung gewinnen kann. ML sollte zunächst nur Beweistaktiken ausdrücken; gerade die strengen Anforderungen dieses Bereichs brachten Mechanismen hervor, die weit darüber hinaus nützlich wurden.
Chronologie
- 1934: Geburt in Yealmpton, Devon.
- 1950er-Jahre: Mathematikstudium in Cambridge und Arbeit bei Ferranti.
- 1972: Entwicklung des ersten LCF-Systems in Stanford.
- 1973: Wechsel an die University of Edinburgh.
- 1970er-Jahre: Entwicklung von ML für LCF.
- 1980er-Jahre: Arbeiten an CCS und Standard ML.
- 1991: Turing Award.
- Anfang der 1990er-Jahre: Entwicklung des Pi-Kalküls mit Parrow und Walker.
- 1995: Wechsel nach Cambridge.
- 1996–1999: Leitung des Cambridge Computer Laboratory.
- 2010: Tod im Alter von 76 Jahren.
Häufig gestellte Fragen
Hat Robin Milner ML allein entwickelt?
Nein. Milner entwarf zentrale Grundlagen, doch ML und Standard ML entstanden in Teams und Gemeinschaften mit zahlreichen Forschern und Implementierern.
Was ist Hindley-Milner-Typinferenz?
Ein System, das aus der Verwendung von Ausdrücken allgemeine statische Typen ableitet. Es ermöglicht polymorphen Code, ohne dass jeder Typ ausdrücklich notiert werden muss.
Warum ist die LCF-Architektur wichtig?
Sie konzentriert das notwendige Vertrauen auf einen kleinen logischen Kern. Komplexe Automatisierung darf Beweise suchen, kann aber nur Ergebnisse erzeugen, die der Kern über zugelassene Regeln bestätigt.
Was ist der Unterschied zwischen CCS und Pi-Kalkül?
CCS modelliert kommunizierende Prozesse mit weitgehend fester Kommunikationsstruktur. Der Pi-Kalkül erlaubt zusätzlich, Kanalnamen selbst zu übertragen, sodass sich die Verbindungsstruktur dynamisch ändern kann.
Wo wirken Milners Ideen heute weiter?
In funktionalen Sprachen und Typsystemen, Beweisassistenten, Protokollverifikation sowie in der Theorie nebenläufiger und verteilter Systeme.
