Theoretische Informatik

Gegenstand und Bedeutung

Die theoretische Informatik untersucht durch Abstraktion und Modellbildung grundlegende Fragen zur Struktur, Verarbeitung, Übertragung und Wiedergabe von Informationen. Zu ihren zentralen Gebieten gehören Automatentheorie, formale Sprachen, Berechenbarkeitstheorie, Komplexitätstheorie, Logik, formale Semantik, Informations-, Algorithmen- und Datenbanktheorie.

Sie liefert mathematische Grundlagen für Programmiersprachen, Compilerbau, die Definition und Verifikation von Programmen sowie die Untersuchung meist diskreter Problemstellungen. Dazu werden formale Systeme, Automaten, Graphen, Syntaxdiagramme, Grammatiken und Semantiken entworfen. Diese Modelle bilden die innere Logik eines Problems ab und ermöglichen formale Beweise, Definitionen, Sätze und Algorithmen. Die Berechenbarkeitstheorie zeigt, welche Probleme grundsätzlich unlösbar sind; die Komplexitätstheorie grenzt praktisch effizient lösbare Probleme von solchen mit hohem Ressourcenbedarf ab.

Die theoretische Informatik ist eng mit Mathematik und Logik verbunden und entwickelte sich im 20. Jahrhundert zu einer eigenständigen Disziplin. Zu den genannten Pionieren gehören Kurt Gödel, Alonzo Church, Alan Turing, Stephen C. Kleene, Claude Shannon, John von Neumann, Hans Hermes und Noam Chomsky. 1936 erhielt Heinrich Scholz von Turing ein Exemplar von dessen Arbeit „On Computable Numbers, with an Application to the Entscheidungsproblem“; laut Achim Clausing hielt Scholz daraufhin das weltweit erste Seminar über Informatik.

Automaten, Grammatiken und formale Sprachen

Die Automatentheorie formalisiert Automaten beziehungsweise Rechenmaschinen und untersucht deren Eigenschaften und Berechnungsstärke. Eine zentrale Frage lautet, welche Probleme von unterschiedlichen Klassen von Rechenmaschinen gelöst werden können.

Die Theorie der formalen Sprachen untersucht Grammatiken und die durch sie erzeugten Sprachen über einem Alphabet. Dabei werden syntaktische und semantische Merkmale betrachtet. Ob ein Wort zu einer formalen Sprache gehört, kann durch einen passenden Automaten entschieden werden. Deshalb besteht ein enger Zusammenhang zwischen Grammatiken, die Sprachen erzeugen, und Automaten, die diese Sprachen erkennen.

Für kontextfreie Grammatiken wird die Backus-Naur-Form (BNF) verwendet. Sie ist eine Notationskonvention, mit der beispielsweise die Syntax von Programmiersprachen beschrieben wird. Die erweiterte Backus-Naur-Form (EBNF) unterscheidet sich von der BNF durch zusätzliche Notationserweiterungen. Die Syntax der Programmiersprachen Pascal und Modula-2 wurde in EBNF definiert.

Chomsky-Hierarchie und Sprachklassen

Die Chomsky-Hierarchie ordnet formale Sprachen nach ihrer Mächtigkeit und Komplexität. Sie umfasst vier Klassen:

• reguläre Sprachen (Typ 3, ℛ),
• kontextfreie Sprachen (Typ 2, 𝓛_CF),
• kontextsensitive Sprachen (Typ 1, 𝓛_ECS),
• rekursiv aufzählbare Sprachen (Typ 0, 𝓛_RE).

Die Klassen sind ineinander enthalten: Typ 3 ⊂ Typ 2 ⊂ Typ 1 ⊂ Typ 0 beziehungsweise ℛ ⊂ 𝓛_CF ⊂ 𝓛_ECS ⊂ 𝓛_RE.

Den Sprachklassen entsprechen Maschinenklassen: Reguläre Sprachen werden von endlichen Automaten erkannt, kontextfreie Sprachen von nichtdeterministischen Kellerautomaten, kontextsensitive Sprachen von linear beschränkten Turingmaschinen und rekursiv aufzählbare Sprachen von allgemeinen Turingmaschinen. Zwischen Grammatik- und Maschinenklassen besteht Äquivalenz: Die jeweiligen Grammatikklassen erzeugen genau die Sprachklassen, die von den entsprechenden Maschinenklassen erkannt werden.

Die Pumping-Lemmata liefern notwendige, aber nicht hinreichende Bedingungen dafür, dass eine Sprache regulär oder kontextfrei ist. Das Pumping-Lemma für reguläre Sprachen heißt wegen seiner Struktur auch uvw-Theorem, das für kontextfreie Sprachen uvwxy-Theorem. Erweiterungen wie das Lemma von Jaffe liefern dagegen ein hinreichendes Kriterium.

Berechenbarkeit und Grenzen von Algorithmen

Die Berechenbarkeitstheorie untersucht, ob mathematische Probleme algorithmisch lösbar sind. Sie analysiert die innere Struktur von Problemen und ordnet sie nach verschiedenen Graden der Lösbarkeit oder Unlösbarkeit.

Ausgehend von der intuitiven Berechenbarkeit, also der Vorstellung, für welche Probleme sich Lösungen formulieren lassen, wurde ein formal-mathematischer Berechenbarkeitsbegriff entwickelt. Die Churchsche These besagt, dass der Begriff der mathematischen Berechenbarkeit durch die Turingmaschine und gleich starke formale Berechnungsmodelle erfasst wird. Auf dieser Grundlage lassen sich Berechenbarkeitsaussagen mathematisch beweisen oder widerlegen.

Ein wichtiges Ergebnis ist die Unentscheidbarkeit des Halteproblems. Es gibt keinen Algorithmus, der beliebige Programme für eine bestimmte Eingabe daraufhin untersucht, ob sie irgendwann anhalten oder nicht. Nach dem Satz von Rice ist außerdem jede nicht-triviale Eigenschaft eines Programms in einer turingmächtigen Programmiersprache unentscheidbar. Mit Methoden der Berechenbarkeitstheorie lässt sich auch Kurt Gödels Unvollständigkeitssatz formulieren und beweisen.

Komplexität und effiziente Lösbarkeit

Die Komplexitätstheorie untersucht, welche Ressourcen ein Algorithmus zur Lösung eines Problems benötigt, insbesondere Rechenzeit und Speicherplatz. Probleme werden dazu in Komplexitätsklassen eingeteilt.

P ist die Klasse der Probleme, die eine deterministische Turingmaschine in Polynomialzeit entscheiden kann. NP ist die Klasse der Probleme, deren Lösungen effizient überprüft werden können; äquivalent ist NP die Klasse der Probleme, die eine nichtdeterministische Turingmaschine in Polynomialzeit entscheiden kann.

Ein konkreter Lösungsalgorithmus liefert eine Oberschranke für den Ressourcenbedarf. Untere Schranken sind schwieriger: Dafür muss gezeigt werden, dass alle Algorithmen, die nur eine bestimmte Ressourcenmenge verwenden, das Problem nicht lösen können. Eine zentrale, seit Jahrzehnten offene Frage lautet, ob P und NP übereinstimmen. Es würde genügen, ein NP-vollständiges Problem in deterministischer Polynomialzeit zu lösen, um diese Gleichheit zu beweisen.

Die parametrisierte Algorithmik untersucht, welche Instanzen von NP-vollständigen Problemen effizient lösbar sind. Die „fine-grained complexity“ erforscht Beziehungen zwischen Problemen in P, besonders zwischen Problemen mit quadratischer und kubischer Laufzeit aus der Graphentheorie.

Semantik, Information und Logik

Die formale Semantik beschreibt die Bedeutung von Programmen, die in einer formalen Sprache angegeben sind. Dazu wird eine Semantikfunktion konstruiert:

𝒞: 𝒫 → f

Dabei steht 𝒞 für die Semantikfunktion, 𝒫 für die Menge der syntaktisch korrekten Programme, f:⊆ Σ → Σ für die vom Programm berechnete Funktion und Σ für die Menge der möglichen Speicherbelegungen. Unterschieden werden axiomatische, denotationelle, dialogische und Fixpunktsemantik.

Die Informationstheorie beschreibt Information mathematisch. Der Informationsgehalt einer Nachricht wird durch ihre Entropie charakterisiert. Damit kann die Übertragungskapazität eines Informationskanals bestimmt werden. Die enge Verbindung zur Kodierungstheorie zeigt sich außerdem in Anwendungen der Informationstheorie in der Kryptologie; das One-Time-Pad wird als informationstheoretisch sicheres Verschlüsselungsverfahren genannt.

Mathematische Logik wird unter anderem zur Beschreibung von Schaltkreisen, zur Programmierung und zur formalen Spezifikation eingesetzt. Aussagenlogik und Boolesche Algebra dienen der Schaltkreisbeschreibung; dabei kann Craig-Interpolation verwendet werden. Prädikatenlogik, Temporale Logik, Modallogik und dynamische Logik beschreiben das beabsichtigte Verhalten von Software- und Hardwaresystemen. Dieses Verhalten kann mit Model Checking oder Theorembeweisern verifiziert werden. Modallogiken können außerdem Wissen eines Agenten darstellen, während kombinatorische Logik in der Theorie der funktionalen Programmierung verwendet wird.