Hat Informatik mit Logik zu tun?#
Persoenlicher Rueckblick auf 50 Jahre im Bannkreis der Informatik#
Von
Egon Boerger (Pisa)
Zur Informatik bin ich von der Philosophie ueber die mathematische Logik gekommen, was meine Stationen in der Wissenschaft (2 Jahrzehnte in der Logik, 3 Jahrzehnte in der Informatik) kennzeichnet (ein Buch ueber Modellierungsmethodik ist unterwegs):
Bertrand Russell paraphrasierend kann man das auch so ausdruecken, dass ich mich in jungen Jahren mit Mathematik und Logik, in Mannesjahren mit Softwareengineering und im beginnenden Alter mit der Modellierung von Geschaeftsprozessen beschaeftigt habe. Honit soit qui mal y pense.
Eigentlich wollte ich ja Dirigent werden, aber da meine Musiklehrer warnten, mit solchen Leute koenne man Strassen pflastern und mich stattdessen wer zum Pianisten wer zum Organisten machen wollten, was ich aber nicht wollte, habe ich mich zum Studium der Philosophie entschieden. Von einem humanistischen Gymnasiums kommend wollte ich die Grundgesetze der Welt verstehen. Die Vorlesungen an der Sorbonne (Paris) und am Institut Superieur de Philosophie in Louvain, insbesondere der in der Tradition von Robert Feys stehenden Professoren Joseph Dopp und Jean Ladriere, erweckten mein Interesse an mathematischer Logik und Grundlagenforschung, was mich 1966 an das gleichnamige Institut in Muenster in Westfalen und damit zurueck in meine Heimatstadt gebracht hat---wo ich doch garnicht hatte studieren wollen und schon garnicht Mathematik! Dort hat mich der damalige Geist des Instituts gepackt: der Institutsgruender Heinrich Scholz wie sein Schueler und Nachfolger Hans Hermes gehoerten zu den wenigen, die Turings Loesung des fundamentalen Hilbertschen Entscheidungsproblems sofort in seiner epochalen Wirkung erkannt haben und sich der engen Beziehungen zwischen abstrakten Maschinen und sie beschreibenden (wie wir heute sagen 'formalen') Sprachen der Logik bewusst und an deren Entwicklung interessiert waren (siehe Rainer Glaschick: Alan Turings Wirkung in Münster, Mitt. Dtsch. Math.-Ver. 2012, 20(1), 42-48). Die resultierende Muensteraner Tradition einer computerorientierten Ausrichtung der Logik wurde von Gisbert Hasenjaeger, Hans Hermes (siehe das einflussreiche Lehrbuch ueber Aufzaehlbarkeit, Entscheidbarkeit und Berechenbarkeit) und Dieter Roeddingweiterentwickelt, wozu auch die Vorlesungen von Wilhelm Ackermann in Muenster und insbesondere sein in Muenster verfasstes einflussreiches Buch ueber "Solvable Cases of the Decision Problem” (1954) beigetragen haben.
So lernte man seit 1966 in den Roeddingschen Vorlesungen und Seminaren nicht nur klassische Themen mathematischer Logik kennen---Logiksprachen und Kalkuele fuer Praedikatenlogik, Typentheorie, modale Logik, Mengenlehre, Modell- und Beweistheorie usw.--- sondern aufs Intensivste viele Begriffe `rechnender Maschinen’ wie Netzwerke endlicher Automaten, cellulare Automaten, Petrinetze, Automaten der Chomskyhierarchie, Turingmaschinen, Registermaschinen, auf komplexen Datenstrukturen arbeitende Maschinen (!), Lambda- und Fitchkalkuel, Kombinatorische Logik, Markov Algorithmen, usw. Im Vordergrund stand im Geiste Turings das Studium der algorithmischen Komplexitaet von Entscheidungsproblemen und Hierarchien maschinell berechenbarer Funktionen.
Foto: Archiv Ottmann
Im von Hasenjaeger begruendeten und von seinem Schueler Roedding weitergefuehrten (aber nach Roeddings Tod kurzum aufgeloesten) Turingraum des Instituts wurden die in Vorlesungen behandelten Automaten, sogar kleine universelle Turing- und Registermaschinen mit einfachsten Mitteln gebaut und in Uebungen vorgefuehrt. Siehe hier das Foto von Hasenjaegers MiniWang, einer kleinen universellen Turingmaschine, nebst einem (vermutlich) Zaehlband, das von Walburga Roedding zusammen mit weiteren Artefakten als Teil des Roedding Nachlasses aus der Aufloesung des Turingraums gerettet werden konnte und heute mit diesen und denen aus dem Hasenjaeger Nachlass im Heinz Nixdorf MuseumsForum in Paderborn http://www.hnf.de/start.html auf eine naehere Untersuchung wartet. Dass diese Arbeiten keineswegs nutzlos waren zeigt der Artikel "Wangs’s B machines are efficiently universal, as is Hasenjaeger’s small universal electromechanical toy" von T. Neary, D. Woods, N. Murphy und R. Glaschick (J.of Complexity 30 (2014) 634-646 sowie https://arxiv.org/abs/1304.0053) und das unabhaengig und gleichzeitig mit Minsky und Sheperdson und Sturgis von Roedding entwickelte Konzept der Registermaschinen (s. G. Hasenjaeger: "On the early history of register machines", LNCS 270, 181-188).
Wie ich es geschafft habe, als Student und Assistent nicht selbst im Turingraum haben mitloeten zu muessen, ist mir ein Raetsel geblieben. Doch habe ich dieser computernahen mathematischen Ausbildung am damaligen Logikinstitut in Muenster mein Interesse an der gerade als wissenschaftliche Disziplin entstehenden Informatik zu verdanken.
So bin ich ein Jahr nach der Promotion (mit einer Dissertation zur Komplexitaet logischer Entscheidungsprobleme) der Einladung des Physikers und Kybernetikers Edoardo Caianello gefolgt, als Dozent beim Aufbau eines Informatikinstituts an der Universitaet Salerno (Italien) zu helfen (1972-1976). Dort habe ich durch Vorlesungen (!) ueber die verschiedenen Gebiete der Informatik die technischen Kenntnisse des Fachs erworben und sie (nach der Habilitation 1976 in Muenster mit einer Schrift zur Komplexitaetstheorie und 2 Jahren Dozentur) vertieft durch meine Lehrtaetigkeit an den Universitaeten Dortmund 1978-1985 und 1983/4 Udine (Italien). Die gewonnenen Erfahrungen haben die Erkenntnis verstaerkt, dass die wesentlichen neuen, nicht nur komplexitaetstheoretischen Herausforderungen an die Logik aus den Grundlagen der Informatik kommen.
Die Beziehungen zwischen Logiksprachen und Maschinenklassen bestimmten das eingangs zitierte (urspruenglich in Deutsch veroeffentlichte, von Roedding angeregte und in meiner Dortmunder Zeit verfasste) Lehrbuch zu "Computability Complexity Logic” wie auch die spaetere Monographie "The Classical Decision Problem”. In beiden Buechern, wie schon in meiner Dissertation, spielen die Registermaschinen (!) eine entscheidende Rolle. Mit dem Ziel, die wechselseitige Befruchtung von Logik und Informatik auch organisatorisch zu foerdern, habe ich angefangen, zum damals in deutschen Logikkreisen hart umstrittenen interdisziplinaeren Thema `Logik und Informatik’ systematisch Sommerkurse sowie Tagungen (insgesamt drei Dutzend) zu veranstalten und Sammelbaende (insgesamt mehr als zwei Dutzend) herauszugeben, beginnend mit dem 1984 am CISM in Udine veranstalteten "Course on Computation Theory” (ueberarbeitet und veroeffentlicht 1988 bei Computer Science Press als "Trends in Theoretical Computer Science”), dem gemeinsam mit Hasenjaeger und Roedding 1984 in Muenster veranstalteten (intern Drei-Generationen-Tagung genannten) Symposium "Rekursive Kombinatorik “ (Springer LNCS 171) und dem in Pisa (Italien) erarbeiteten Roedding-Gedaechtnisband "Computation Theory and Logic” (1987, Springer LNCS 270).
Einen institutionellen Rahmen erhielten diese Tagungsaktivitaeten durch die nach dem ploetzlichen Tode von Dieter Roedding gemeinsam mit Hans Kleine Buening (aus der Muensteraner Logikschule) und Michael Richter realisierte Idee einer Jahrestagung "Computer Science Logic (CSL)”. Dies war 1985, ein Jahr bevor die Nachricht ueber die frisch etablierte Konferenz "Logic in Computer Science” (LICS) ueber den Atlantik kam. Dass die CSL-Serie nicht auch schon 1986 und nicht am Logikinstitut in Muenster startete, sondern erst 1987 und am Institut fuer angewandte Informatik und Formale Beschreibungsverfahren in Karlsruhe ist widrigen lokalen Interessen und meinem dadurch veranlassten Wechsel an die Universitaet Pisa zuzuschreiben. 1992 wurde die CSL-Konferenzreihe im Verlaufe eines Dagstuhlseminars von Logikern und Informatikern aus 14 Laendern in die erstmalig in San Miniato (Pisa) ausgerichtete Jahrestagung der European Association for Computer Science Logic (EACSL) ueberfuehrt (s. https://eacsl.kahle.ch/goals.html) und ist auch heute noch mit LICS ein Markenzeichen in der theoretischen Informatik; s. den Bericht "Ten Years of CSL Conferences (1987-1997)" http://www.di.unipi.it/~boerger/Curriculum/HistoryCslEacsl87-97.pdf im EATCS Bulletin 63 (October 1997) ueber meine Taetigkeit als erster EACSL Vorsitzender sowie die aktuelle Tagungsliste https://eacsl.kahle.ch/conferences.html.
Um die Probleme der Erstellung korrekter Softwaresysteme aus erster Hand und vor Ort kennenzulernen habe ich in den mir in Pisa seit 1985 gewaehrten 5 Forschungsfreijahren in einschlaegigen Firmen (IBM, Siemens, Microsoft, SAP) sowie an der ETH Zuerich gearbeitet. Dies hat mich ungeahnte praktische Anwendungen von Methoden der Logik im Softwareengineering erkennen lassen, insbesondere a) zur Erstellung praeziser Pflichtenhefte, verstanden als technisch und juristisch bindende Blaupausen des zu konstruierenden Softwaresystems, und b) fuer deren zuverlaessige, sprich praezis dokumentierte und damit objektiv nachpruefbare Ueberfuehrung in maschinell ausfuehrbare Programme. Punkt a) ist eine erkenntnistheoretische Problematik, bestehend aus Zweierlei:
- gruendlichem Verstehen gewuenschten Systemverhaltens (nicht nur mathematischer durch Gleichungen beschreibbarer Funktionen, wie wir sie vor 50 Jahren als Studenten der Numerik mittels ganzer Kisten von Lochkarten zu programmieren hatten),
- einer eindeutigen, sachlich korrekten und lueckenlosen Formulierung dieses Verstaendnisses in formalen (letztendlich Programmier-) Sprachen,
womit sich der Kreis zu praezisen Analysen natuerlichsprachiger Texte---intensiv trainiert in den Doppschen Uebungen zur Logik in Louvain!---schliesst. Punkt b) beruehrt eine Problematik angewandter Modelltheorie, naemlich der Definition beweisbar korrekter Modelltransformationen, insbesondere durch kontrolliertes (sprich: als korrekt verifiziertes) schrittweises Einbringen von Entwurfs- und Programmierentscheidungen in sog. Modellverfeinerungen. Das moderne, in Antwort auf Anforderungen der Informatik entwickelte reiche Instrumentarium der heutigen Computational Logic liefert viele praktische, maschinell unterstuetzte Verfahren zur mathematischen Analyse zwecks Verifikation von Softwaresystemmodellen, die deren experimentelle Ueberpruefung durch Testen sachlich und kostenguenstig ergaenzen. Beispielhaft illustriert in den eingangs zitierten Buechern zu Java/JVM, ASMs und SBPM. Das Einbringen von Methoden der Logik fuer die Konstruktion nachweisbar korrekter Softwaresysteme ist auch das Hauptthema einer 1996 wiederum im Laufe eines Dagstuhlseminars!
Gemeinsam mit Jean-Raymond Abrial, Uwe Glaesser und weiteren Kollegen gegruendeten internationalen, alle zwei Jahre stattfindenden Tagungsreihe mit dem Drei-Buchstaben-Acronym ABZ. Nomen est omen, so auch hier die Initialen der involvierten Methoden Abstract State Machines, B, Z, die wenngleich auf verschiedene Weise alle drei auf dem Fundament mathematischer Logik und axiomatischer Mengenlehre gegruendet sind.
Eine mittlerweilen unueberschaubare Vielzahl von Personen und Institutionen weltweit haben in den vergangenen 50 Jahren ein sachgemaesses Verstaendnis der heute nicht mehr umstrittenen wechselseitigen Befruchtung von Logik und sowohl theoretischer wie praktischer Informatik erarbeitet. Pars pro toto moechte ich aus europaeischer Perspektive zwei Personen hervorheben, deren Beitrag nur Eingeweihten deutlich ist: Alfred Hofmann vom Springer-Verlag fuer die bereitwillige Aufnahme zahlreicher (gerade auch frueher, damals noch kontroverser) LNCS-Baende ueber interdisziplinaere Arbeit im Feld zwischen Logik und Informatik und Reinhard Wilhelm fuer die weitsichtige Foerderung vieler einflussreicher Dagstuhlseminare zum facettenreichen Themenkreis.
Die fruchtbare Entwicklung von Computational Logic und den weit verzweigten praktischen Anwendungen mathematischer Logik in der Informatik, fuer mich persoenlich auch die Anerkennung meines Beitrags durch den 2007 verliehenen Alexander von Humboldt Forschungspreis meines Heimatlandes, haben, wenn man es global betrachtet, entschaedigt fuer den Preis, den die mathematische Logik in der BRD wissenschaftspolitisch (betroffen hat es auch mich persoenlich) hat zahlen muessen durch die im letzten Viertel des vorigen Jahrhunderts obstruktive und mancherorts destruktive Haltung einiger ihrer damaligen Professoren, einer Gruppe, der das von der Informatik offerierte Potential fuer die Zukunft ihres Fachs nichts wert war und zu der ich 1985 durch die Annahme eines Rufes ad personam an die Informatikabteilung der Universitaet Pisa auf Distanz gegangen bin.