Mathematische Klarheit durch guten Schreibstil

BLOG: Heidelberg Laureate Forum

Laureates of mathematics and computer science meet the next generation
Heidelberg Laureate Forum

Leslie Lamport passiert das häufiger. Er ist nicht allein: Peter Ustinov wurde offenbar bevorzugt von Menschen auf seine Rolle als Nero in “Quo vadis” angesprochen, Alec Guiness auf seine Rolle als Obi Wan Kenobi in “Star Wars”, und Lamport wird eben häufig auf das Softwarepaket LaTeX angesprochen.

Seiner Reaktion (Beschleunigen des Schrittes = internationale Körpersprache für “Neeeein! Nicht schon wieder dieses Thema!”) entnehme ich, dass er den wenig originellen Dank eines glücklichen LaTeX-Nutzers mit, sagen wir mal: eher gemischten Gefühlen aufnimmt.

Leslie Lamport Credit: hlff / Kreutzer
Leslie Lamport Credit: hlff / Kreutzer

Aber es hilft nichts: In weiten Teilen der naturwissenschaftlichen, Mathematik- und Informatik-Communities ist Lamport nun einmal für LaTeX bekannt. Als Donald Knuth (den wir wahrscheinlich nie auf dem HLF sehen werden) das Textsatzsystem TeX schuf, führten einige derjenigen Eigenschaften, die das System besonders vielfältig einsetzbar und elegant machten, zu einer deutlichen Einschränkung in der Einfachheit der Nutzung. LaTeX begann als Lamports Sammlung von Macros für TeX, ursprünglich in den 1980er Jahren für ein Buch programmiert, das er damals schrieb. Inzwischen sind LaTeX und seine diversen Inkarnationen in weiten Teilen der Wissenschaft Standard: Auf dem arXiv – der größten Sammlung elektronischer Vorabveröffentlichungen in Physik, Astronomie und einer Reihe weiterer Wissenschaften – dominieren die LaTeX-Artikel; die meisten Fachzeitschriften der betreffenden Fächer erwarten von Autoren, dass sie ihre Manuskripte im LaTeX-Stil der Zeitschrift einreichen; bei Fachbüchern läuft es ähnlich.

Aber die LaTeX-Weiterentwicklung liegt längs bei anderen, und Lamports eigentliche Forschungs- und Entwicklungsarbeit (die ihm immerhin 2013 den Turing Award eingebracht hat – daher auch seine Anwesenheit beim HLF) hat nichts mit Textverarbeitung im engeren Sinne zu tun. Stattdessen geht es dabei um verteilte Systeme, etwa um separate Teilsysteme, die sich gegenseitig über ein Netzwerk Nachrichten zusenden und die unabhängig voneinander (und damit auch: gleichzeitig nebeneinander her) Rechnungen ausführen können.

In diesen Zusammenhang gehört auch TLA, kurz für “Temporal Logic of Actions” (wörtlich etwa die “zeitliche Logik von Aktionen”). Dabei geht es darum, Systeme und die Arten und Weisen zu beschreiben, wie sie sich (z.B. Schritt für Schritt) mit der Zeit ändern können (weitere Informationen gibt’s auf Lamports TLA Homepage). Seine dafür erfundene Sprache TLA+ erlaubt es Benutzern, Systeme dadurch zu beschreiben, dass sie deren mögliche Zustände und Änderungsmöglichkeiten mithilfe einfacher Mathematik (insbes. Prädikatenlogik) definieren.

Was das für Vorteile bringt, ist in der Einführung zu Lamports Buch Specifying Systems sehr schön ausgeführt. Einem der Abschnitte hat Lamport ein Zitat des Comiczeichners Richard Guindon vorangestellt: “Writing is nature’s way of letting you know how sloppy your thinking is”, frei übersetzt “Die Natur hat das Schreiben erfunden, um den Menschen zu zeigen, wie schludrig sie denken.” (Ich liebe dieses Zitat!)

Lamport spinnt Guindons Gedankengang weiter mit “Die Natur hat die Mathematik erfunden, um den Menschen zu zeigen, wie schludrig sie schreiben” und, noch weiter unten, “Die Natur hat formale mathematische Systeme erfunden, um den Menschen zu zeigen, wie schludrig sie Mathematik betreiben.”

Mann muss weder Sapir noch Whorf sein, um zu sehen, wo das hinführt: In einer Sprache mit klar definierter Struktur wird man weniger leicht Flüchtigkeitsfehler machen, die nicht allein schon aufgrund ihrer mangelhaften Syntax oder Grammatik auffallen, als in einer Sprache, die größere Ungenauigkeiten zulässt. Wenn ich recht erinnere, galt das vor längerer Zeit auch als einer der Gründe, warum Wissenschaftlern als Gemeinschaftssprache Latein nutzten.

Wem das als Overkill erscheint – warum so eine überaus formale Beschreibung für Alltagssysteme? – sollte sich das folgende klar machen: Wir Menschen mögen zwar bei einfacheren Systemen recht gut auf einen Blick erfassen, wie sich das System mit der Zeit verändern kann. Aber ab einem bestimmten Komplexitätsgrad verlieren wir zwangsläufig den Überblick. Da hilft eine formale Beschreibung, in deren Rahmen man das mögliche Systemverhalten Schritt für Schritt berechnen kann (und die formalisiert genug ist, dass auch ein Computer die Zwischenschritte übernehmen kann!) ganz beträchtlich weiter – und kann unter Umständen sogar der einzige Weg sein, das Systemverhalten vollständig auszuloten. Es ist kein Zufall, dass auch Amazon TLA nutzt, um Schlüsseleigenschaften seiner Basissysteme zu verifizieren – und sicherzugehen, dass komplexe Wechselwirkungen zwischen den verschiedenen dort aktiven Algorithmen nicht zu unangenehmen (und kostspieligen) Überraschungen führen.

Das wäre, für das HLF sehr passend, ein schönes Beispiel, wie formale Mathematik den Informatikern hilft. Der Vortrag Lamports am Dienstag ging allerdings in die andere Richtung: Es ging darum, wie man mathematische Beweise in möglichst einfacher, systematischer Weise schreibt – so dass möglichst direkt einsehbar ist, wenn/wo an dem Beweis etwas schiefläuft. Die Konventionen zur Beweis-Schreibweise, die Lamport vorschlägt sind nicht besonders kompliziert – etwa eine klare, hierarchische Darstellung der Beweisschritte, explizite Rückverweise auf die verwendeten Voraussetzungen oder vorangehenden Schritte – können auch jeweils für sich umgesetzt werden.

image

Ich fand die Beispiele und Argumente in Lamports Vortrag durchaus überzeugend (und habe mich derweil gefragt, wieviel davon sich auf die Physik oder auf andere Wissenschaften übertragen lässt); der allgemeinen Stimmung im Hörsaal nach zu urteilen war ich damit bei weitem nicht der einzige. Aber selbst wenn die Anwesenden bei zukünftigem Aufschreiben von Beweisen an Lamports Vorschläge denken: Wahrscheinlicher ist leider, dass die Natur Lamports Ideen zu diesem Thema erfunden hat, um ihm zu zeigen, wie schwierig es ist, Mathematiker von ihren alten Gewohnheiten abzubringen.


Für Interessierte: Lamports Vortrag komplett als Video

Avatar photo

Markus Pössel hatte bereits während des Physikstudiums an der Universität Hamburg gemerkt: Die Herausforderung, physikalische Themen so aufzuarbeiten und darzustellen, dass sie auch für Nichtphysiker verständlich werden, war für ihn mindestens ebenso interessant wie die eigentliche Forschungsarbeit. Nach seiner Promotion am Max-Planck-Institut für Gravitationsphysik (Albert-Einstein-Institut) in Potsdam blieb er dem Institut als "Outreach scientist" erhalten, war während des Einsteinjahres 2005 an verschiedenen Ausstellungsprojekten beteiligt und schuf das Webportal Einstein Online. Ende 2007 wechselte er für ein Jahr zum World Science Festival in New York. Seit Anfang 2009 ist er wissenschaftlicher Mitarbeiter am Max-Planck-Institut für Astronomie in Heidelberg, wo er das Haus der Astronomie leitet, ein Zentrum für astronomische Öffentlichkeits- und Bildungsarbeit. Pössel bloggt, ist Autor/Koautor mehrerer Bücher, und schreibt regelmäßig für die Zeitschrift Sterne und Weltraum.

2 comments

  1. Nun ja, mit alten Gewohnheiten hat das eher weniger zu tun. Der von Lamport propagierte Schreibstil wurde von Hilbert und seinen Nachfolgern am Anfang des 20. Jahrhunderts popularisiert, in der Mitte des 20. Jahrhunderts dann von der Bourbaki-Gruppe, um nur die bekanntesten Namen zu nennen. Die Gegenmeinung vertrat zum Beispiel William Thurston in seinem vor 20 Jahren erschienen Artikel http://arxiv.org/pdf/math/9404236.pdf Es handelt sich also um unterschiedliche Sichtweisen, die es schon das gesamte 20. Jahrhundert gegeben hat, was Lamport vermutlich auch wüßte, wenn er in der Mathematik aktiv wäre. (Es kam dann ja auch nach dem Vortrag die Zuschauerfrage, ob er seine Ideen schon einmal in einer Mathematik-Vorlesung umgesetzt hätte bzw. ob er in den letzten Jahrzehnten überhaupt Mathematik-Vorlesungen gehalten hätte, was er verneinte.)

    Richtig ist aber auf jeden Fall, dass das elektronische Publizieren in Zukunft neue Möglichkeiten schaffen wird. Der Vorschlag, Beweise als Hypertext mit klickbaren Details zu schreiben, klingt sehr interessant und es wird, sobald mehr Lehrbücher als E-Buch erscheinen, sicher recht bald Autoren geben, die diese Idee ausprobieren und umsetzen.

  2. Thilo Kuessner schrieb (24. September 2014 9:05):
    > Der Vorschlag, Beweise als Hypertext mit klickbaren Details zu schreiben, klingt sehr interessant […]

    Die Möglichkeit, Bestandteile von Beweistexten als klickbaren Hypertext zu schreiben, um sie mit
    anderen (Beweis-)Texten in Verbindung zu setzen, empfiehlt sich ja schon seit der Erfindung des
    Hypertexts an sich;
    und erst recht, seit die entsprechende Notation so einfach sein kann wie

    “[[ <Text_B> | <Bestandteil_von_Text_A> ]]”.

    Der umfassendere, ambitioniertere Vorschlag, der dabei nicht übersehen werden sollte,
    nämlich die Beziehung zwischen Bestandteilen des eines Textes und einem bestimmten (duch Hypertext klickbar zugeordneten) anderen Text als Beweismittel aufzufassen und zu nutzen (ggf. sogar automatisiert),
    ist allerdings erst vorstellbar, seit die Notation

    “[[ <Text_B>#<Beweisrichtung> | <Bestandteil_von_Text_A> ]]”

    zur Verfügung steht.

Leave a Reply


E-Mail-Benachrichtigung bei weiteren Kommentaren.
-- Auch möglich: Abo ohne Kommentar. +