Giovanni Sommaruga ist Vize-Präsident der SGLPW und Dozent für Philosophie der Mathematik und Logik an der ETH Zürich; Thomas Strahm ist Präsident der SGLPW und Dozent für Informatik und Logik an der Universität Bern.

Unter einem Algorithmus (Al Chwarizmi 825) versteht man eine endliche, eindeutige Beschreibung eines effektiven Verfahrens zur Lösung eines Problems. "Effektiv" soll dabei bedeuten, dass das Verfahren auf ausschlies- slich mechanische Art und Weise, d.h. im Prinzip von einer Maschine durchge- führt werden kann. Beispiele von Algorithmen sind etwa die Regeln zur Addition und Multiplikation von natürlichen Zahlen, das Verfahren zur Bestimmung der n-ten Primzahl, gegeben eine Zahl n, sowie der berühmte Algorithmus von Euklid zur Berechnung des grössten gemeinsamen Teilers zweier Zahlen.


Muhammed al-Chwarizmi (etwa 783 - 850), auf einer Brief- marke der Sowjetunion von 1983

Die Schweizerische Gesellschaft für Logik und Philosophie der Wissenschaften und die Turing-Tagung 2012

Giovanni Sommaruga und Thomas Strahm

 

Aufgaben und Ziele

Die Schweizerische Gesellschaft für Logik und Philosophie der Wissenschaften SGLPW wurde im Jahre 1948 in Zürich gegründet. Ziel der Gesellschaft ist es, die mathematische und philosophische Logik sowie die Wissenschaftsphilosophie in der Schweiz zu fördern und all denjenigen eine Plattform für die Diskussion und den Austausch zu bieten, die an diesen Disziplinen interessiert sind. Zu diesem Zweck organisiert die SGLPW jährlich eine Tagung, welche abwechslungsweise einem besonderen Thema der mathematischen oder der philosophischen Logik oder der Wissenschaftsphilosophie gewidmet ist. Die SGLPW ist auch Teil der Plattform MAP (Mathematik, Astronomie, Physik) der Schweizerischen Akademie der Naturwissenschaften SCNAT.

SGLPW Jahrestagungen

Die folgende Übersicht mag einen Einblick in die Vielfalt von Themen vermitteln, mit welchen sich die SGLPW in den letzten Jahren beschäftigt hat. Die Jahrestagung 2006 fand in Fribourg zum Thema "Foundational theories of mathematics" statt. Im folgenden Jahr stand in Lausanne das wissenschaftsphilosophische Thema "Structuralism" zur Debatte. Die Jahrestagung 2008 in Bern beschäftigte sich mit "Recent trends in proof theory". Im Jahr 2009 fand die Jahrestagung in Genf zum Thema aus der philosophischen Logik "Plurals and Plural Quantification" statt. 2010 ehrte die SGLPW den 80. Geburtstag ihres früheren Präsidenten und des bedeutenden Logikers Erwin Engeler mit einem Engeler Colloquium in Bern. 2011 befasste sich die SGLPW in Lausanne mit einem Thema im Grenzbereich von Logik und theoretischer Informatik "On the Posterity of Büchi (Logic and Automata)". Und 2012 organisierte die SGLPW zu Ehren von Alan Turing im weltweiten Rahmen des Turing Centenary ihre Jahrestagung in Zürich mit dem Titel "Turing under discussion". Das Thema der letzten Jahrestagung, d.h. der Turing Tagung, soll im Folgenden etwas näher vorgestellt werden.

SGLPW Turing Tagung 2012

Am 23. Juni 2012 wäre der geniale englische Mathematiker Alan Turing (1912-1954) hundert Jahre alt geworden. In diesem Jahr fanden weltweit zahlreiche Veranstaltungen statt, um Turings Leben und Werk zu würdigen. Viele dieser Tagungen wurden an Orten abgehalten, die in Turings Leben eine ausgezeichnete Rolle gespielt haben, z.B. Cambridge, Manchester und Bletchley Park. Die SGLPW feierte Turings weitreichenden Einfluss auf die Informatik, mathematische Logik, Kryptographie und künstliche Intelligenz mit einer Tagung, welche am 26. und 27. Oktober an der ETH in Zürich organisiert wurde. Daran nahmen weltweit führende Turing-Experten aus aller Welt teil. Im Folgenden soll nur eines der zentralen Gebiete von Turings Werk, namentlich seine bahnbrechenden Beiträge zur sogenannten Berechenbarkeitstheorie, etwas eingehender diskutiert werden.

Berechenbarkeitstheorie

Der zentrale Begriff, welcher der Berechenbarkeitstheorie zugrunde liegt, ist derjenige des Algorithmus. Damit bringt man einen intuitiven Berechenbarkeitsbegriff zum Ausdruck und beschreibt auf informelle Art und Weise, was ein Computer im Prinzip, d.h. ohne Rechenzeit- und Rechenplatzbeschränkung, berechnen kann. Dieser nicht-formalisierte Algorithmusbegriff mag zwar genügen, um von bestimmten Problemen zu zeigen, dass sie eine algorithmische Lösung besitzen; er ist jedoch unbrauchbar um nachzuweisen, dass ein gegebenes Problem aus prinzipiellen Gründen nicht berechenbar ist, d.h. keine algorithmische Lösung besitzen kann. Wünschenswert ist deshalb eine streng mathematische Fassung des Algorithmusbegriffs, d.h. die Definition von formal-mathematischen Berechenbarkeitsmodellen. Solche Modelle wurden in den dreissiger Jahren des letzten Jahrhunderts von den mathematischen Logikern Church, Gödel, Herbrand, Kleene, Post und Turing gefunden. Das heute bekannteste Modell, welches von Alan Turing um 1936 entwickelt wurde, ist wohl dasjenige der Turing-Maschine.

Turing-Maschine

Bei einer Turing-Maschine handelt es sich nicht um eine konkrete Maschine, sondern um eine bloss hypothetische "Rechenmaschine", welche als formal-mathematisches Modell zu verstehen ist. Sie basiert auf einem zweiseitig unendlichen Band, welches in einzelne Felder unterteilt ist. In jedem dieser Felder kann ein Symbol aus einem endlichen Alphabet stehen, und zu jedem Zeitpunkt wird genau ein Feld von einem Lese-/Schreibkopf abgetastet. Die Maschine besitzt zudem eine endliche Menge von internen Zuständen. Das Verhalten der Turing-Maschine zu einem bestimmten Zeitpunkt ist eindeutig bestimmt durch deren momentanen internen Zustand und das Symbol im eben abgetasteten Feld. Das aktuell gelesene Zeichen wird durch ein anderes Zeichen (eventuell dasselbe!) ersetzt, und der Lese-/Schreibkopf bewegt sich ein Feld nach links oder nach rechts. Am Anfang einer Berechnung wird die Eingabe auf das Band geschrieben. Danach beginnt die Maschine zu "rechnen", und bevor die Rechnung beendet wird (falls sie überhaupt abbricht!), geht die Maschine in einen ausgezeichneten Zustand über, den sogenannten Haltezustand. Das Resultat der Berechnung steht dann auf dem Band.

Die Turing-Maschine liefert nur eine mögliche Formalisierung des intuitiven Algorithmusbegriffes. In den dreissiger Jahren wurde eine ganze Reihe weiterer Berechenbarkeitsmodelle präsentiert, die bis heute von zentraler Bedeutung sind. Dazu gehören der ungetypte Lambdakalkül (Church), die partiell-rekursiven Funktionen (Kleene) sowie der Gödel-Herbrand Gleichungskalkül. Obschon diese Modelle den Algorithmusbegriff auf sehr unterschiedliche Art und Weise charakterisieren, lässt sich zeigen, dass jedes Modell dieselbe Klasse von Funktionen definiert, d.h. die Modelle sind äquivalent. Diese Tatsache bildet ein sehr starkes Indiz dafür, dass der intuitive Algorithmusbegriff adäquat formalisiert wird, d.h. jeder (terminierende) Algorithmus lässt sich mit Hilfe eines und damit aller erwähnten Modelle formalisieren. Dies ist genau die Aussage der sogenannten Church'schen These, benannt nach dem Logiker Alonzo Church (1903-1995). Die These lässt sich nicht formal-mathematisch beweisen, da sie sich auf einen intuitiven Berechenbarkeitsbegriff bezieht; trotzdem zweifelt niemand an ihrer Gültigkeit.

Mit den verschiedenen formalen Berechenbarkeitsmodellen hat man nun ein Instrument zur Verfügung, das gestattet, von bestimmten Problemen nachzuweisen, dass sie keine algorithmische Lösung besitzen oder anders ausgedrückt, dass diese Probleme unentscheidbar sind. Die zwei wohl berühmtesten Ergebnisse in dieser Hinsicht sind die Unentscheidbarkeit des Halteproblems (Turing 1936) sowie die Unentscheidbarkeit der Prädikatenlogik erster Stufe (Church, Turing 1936). Die Unentscheidbarkeit des Halteproblems etwa besagt, dass es keinen Algorithmus H gibt, der für jeden Algorithmus F und jede Eingabe a entscheidet, ob F auf a terminiert.

Auswirkungen auf Digitalcomputer

Es steht ausser Zweifel, dass die erwähnten Arbeiten über die Formalisierung des Algorithmusbegriffes sowie die Grenzen der Berechenbarkeit nicht nur für die (konstruktiven) Grundlagen der Mathematik von Interesse sind, sondern vor allem auch von fundamentaler Bedeutung für die Grundlagen der Informatik; so gehört Berechenbarkeitstheorie auch heute zum Grundstock jedes Informatikstudiums. Im Weiteren ist zu betonen, dass vor allem Turings Ideen einen nicht zu unterschätzenden Einfluss auf den Bau von digitalen Computern in den vierziger Jahren ausübten. Turing selbst hat den Elektronen-Rechner ACE entworfen und das Programmierhandbuch für den ersten in Serie produzierten speicherprogrammierten Computer geschrieben.

Die Berechenbarkeits- und Rekursionstheorie hat sich in den letzten fünfzig Jahren rasant weiterentwickelt. Im Vordergrund der Arbeiten standen Fragen nach einer Verallgemeinerung des Berechenbarkeitsbegriffs; die entsprechenden Antworten führten zu zentralen Zusammenhängen mit Teilsystemen der Mengenlehre sowie zu einem noch umfassenderen Verständnis der gewöhnlichen Berechenbarkeitstheorie.

 

Weitere Informationen: SGLPW, Turing Tagung

 

 

[Veröffentlicht: März 2013]