Theoretische Informatik

Mindmap zu einem Teilbereich der Theoretischen Informatik

Die Theoretische Informatik beschäftigt sich unter anderem mit formalen Sprachen, Automatentheorie, Berechenbarkeits-, Komplexitätstheorie, Kryptologie, Logik (Aussagen-, Prädikatenlogik und Logikprogrammierung), formaler Semantik, Informations-, Algorithmen-, Datenbank- und Spieltheorie. Die theoretische Informatik bietet Grundlagen für die Definition, Prüfung und Ausführung der Programme von Programmiersprachen, den Bau der Compiler von Programmiersprachen - dem Compilerbau - und die mathematische Formalisierung und Untersuchung von meist diskreten Problemstellungen und deren Modellen. Mit Hilfe mathematischer Abstraktion der Eigenschaften von gewonnenen Modellen ergaben sich nützliche Definitionen, Sätze, Algorithmen, Anwendungen und Lösungen von Problemen. Die Theoretische Informatik bildet mit ihren zeitlosen, mathematischen Wahrheiten und Methoden ein formales Skelett, das die Informatik im der Praxis mit konkreten Implementierungen durchdringt. Die Theoretische Informatik identifizierte viele unlösbare Problemstellungen mittels der Berechenbarkeitstheorie und erlaubt, häufig mit konstruktiever Beweisführung der Komplexitätstheorie, die Abgrenzung von praktisch effizient lösbaren Problemen von den Problemen für die das Gegenteil gilt.

Zu den konstruktiven Methoden der Theoretischen Informatik zählt auch das Entwerfen von formalen Systemen, Automaten, Graphen und Syntaxdiagrammen. Die Konstrukte beschreiben dann, die innere Logik eines Problems und ermöglichen Beweisführung und Algorithmenentwurf. Diese Formalisierung hat einen wesentlichen Anteil an der Lösung der betrachteten Problemstellung, deren Implementierung durch Maschinensemantik dem Mensch einen automatisierten Vorteil der Mathematik- und Computer-Nutzung verschaft.

Automatentheorie und Formale Sprachen

Automaten erkennen und Grammatiken erzeugen formale Sprachen.

Die Automatentheorie definiert und fomalisiert Automaten oder Rechenmaschinen und beschäftigt sich mit deren Eigenschaften und Berechnungskraft. Unter anderem untersucht die Automatentheorie, welche Probleme von den unterschiedlichen Rechenmaschinen gelöst werden können.

Die Theorie der formalen Sprachen betrachtet formalisierte Grammatiken und die durch diese Grammatiken erzeugten formalen Sprachen. Sie beschäftigt sich mit syntaktischen und semantischen Merkmalen dieser formalen Sprachen über einem Alphabet.

Die meisten in der Praxis auftretenden formalen Sprachen, wie beispielsweise Programmiersprachen, besitzen eine einfache Struktur und können nach ihrer Komplexität in eine der bekannten Sprachklassen der Chomsky-Hierarchie eingeteilt werden. Die Chomsky-Hierarchie, nach Noam Chomsky - einem Pionier der Sprachtheorie, besteht aus vier Klassen. Diese sind, nach ihrer Mächtigkeit aufsteigend geordnet, die regulären Sprachen, (Typ 3), die kontextfreien Sprachen (Typ 2), die kontextsensitiven Sprachen (Typ 1) und die rekursiv aufzählbaren Sprachen (Typ 0).

Reguläre Sprachen können von endlichen Automaten,

kontextfreie Sprachen von Kellerautomaten,

kontextsensitive Sprachen von linear beschränkten Turingmaschinen und

rekursiv aufzählbare Srachen von allgemeinen Turingmaschinen erkannt werden.

Somit lässt sich die Chomsky-Hierarchie auf Maschinenklassen der Automatentheorie übertragen. Genauer: die fomalen Sprachen, die durch die entsprechenden Grammatikklassen der Chomsky-Hierarchie erzeugt werden, können von den oben aufgeführten Maschinen erkannt werden.

Bekannte praktische Hilfsmittel in der Charakterisierung von regulären und kontextfreien Sprachen sind die Pumping-Lemmata, die eine notwendige, aber nicht hinreichende Bedingung liefern, dass eine von einer Grammatik erzeugte Sprache regulär oder kontextfrei ist. Erweiterungen, wie das Lemma von Jaffe, liefern dagegen ein hinreichendes Kriterium.

Die Backus-Naur-Form oder BNF ist eine Notationskonvention für kontextfreie Grammatiken und somit für kontextfreie Sprachen. Die BNF wird in der Praxis beispielsweise dazu benutzt, die Syntaxen von Programmiersprachen zu definieren. Die jeweilige Syntax der Programmiersprachen Pascal und Modula-2 ist in der erweiterten Backus-Naur-Form, EBNF, definiert worden. Die erweiterte Bauckus-Naur-Form unterscheidet sich nur in einigen Notationserweiterungen von der BNF.

Berechenbarkeitstheorie

In der Berechenbarkeitstheorie wird die algorithmische Lösbarkeit von Problemen - also deren Berechenbarkeit - untersucht. Insbesondere geht es um die Analyse der internen Struktur von Problemen und um die Klassifikation von Problemen nach verschiedenen Graden der Lösbarkeit oder deren Unlösbarkeit.

Ausgehend von der intuitiven Berechenbarkeit, der gefühlsmäßigen Vorstellung welche Probleme formalisierbar sind, entwickelte die Berechenbarkeitstheorie eine mathematische Definition von Berechenbarkeit mit der sich mathematische Beweise führen lassen. Versuche den Berechenbarkeitsbegriff formal zu fassen endeten in der Churchschen These, die beansprucht, dass der Begriff der mathematischen Berechenbarkeit mit der Turingmaschine und gleichstarken formalen Berechnungsmodellen gefunden wurde. Auf dem Fundament der mathematischen Modelle der Berechenbarkeit und der Churchschen These fußen die eigentlichen Erkenntnisse und Aussagen der Berechenbarkeitstheorie. Mit den Methoden der Berechenbarkeitstheorie lässt sich beispielsweise auch Gödels Unvollständigkeitssatz formulieren und beweisen.

Ein weiteres Ergebnis der Berechenbarkeitstheorie ist die Erkenntnis, dass das Halteproblem unentscheidbar ist, man also keinen Algorithmus finden kann, der beliebige Programme daraufhin untersucht, ob sie bei einer bestimmten Eingabe jemals anhalten oder nicht. Ebenfalls unentscheidbar ist laut dem Satz von Rice jedwede nicht-triviale Eigenschaft eines Programms zu entscheiden.

Komplexitätstheorie

Die Komplexitätstheorie untersucht, welche Ressourcen (zum Beispiel Rechenzeit und Speicherplatz) in welchem Maße höchstens aufgewendet werden müssen, um bestimmte Probleme algorithmisch zu lösen. In der Regel erfolgt eine Einteilung der Probleme in Komplexitätsklassen. Die bekanntesten derartigen Klassen sind vermutlich P und NP. P ist die Klasse der effizient lösbaren Probleme (genauer: P ist die Klasse der Probleme, die von einer deterministischen Turingmaschine in Polynomialzeit entschieden werden können), NP die Klasse der Probleme, deren Lösungen effizient überprüft werden können (oder äquivalent: NP ist die Klasse der Probleme, die von einer nichtdeterministischen Turingmaschine in Polynomialzeit entschieden werden können).

Durch die Angabe eines Algorithmus zur Lösung eines Problemes lässt sich eine Oberschranke für den oben erwähnten Bedarf an Ressourcen angeben. Die Suche nach unteren Schranken stellt sich hingegen als weitaus schwieriger dar. Hierzu muss nachgewiesen werden, dass alle möglichen Algorithmen, die nur eine bestimmte Menge von Ressourcen verwenden, ein Problem nicht lösen können.

Eine (wenn nicht sogar die) zentrale und seit Jahrzehnten offene Frage in der Komplexitätstheorie ist, ob die Klassen NP und P übereinstimmen - ein NP-vollständiges Problem in deterministischer Polynomialzeit zu lösen würde als Beweis reichen. Äquivalent dazu kann versucht werden, ein NP-vollständiges Problem auf einem general purpose Computer effizient zu lösen (siehe auch Churchsche These).

Die parametrisierte Algorithmik ist ein relativ junges Teilgebiet der theoretischen Informatik, in dem genauer untersucht wird, welche Instanzen von NP-vollständigen Problemen effizient zu lösen sind.

Formale Semantik

Die formale Semantik beschäftigt sich mit der Bedeutung von in einer formalen Sprache beschriebenen Programmen. Mathematisch ausgedrückt wird eine Semantikfunktion konstruiert, die ein gegebenes Programm auf die von ihm berechnete Funktion abbildet.

${\mathcal {C}}:{\mathcal {P}}\to f$

Dabei steht ${\mathcal {C}}$ für die Semantikfunktion, ${\mathcal {P}}$ für die Menge der syntaktisch korrekten Programme, $f:\subseteq \Sigma \to \Sigma$ für die von dem Programm berechnete Funktion und $\Sigma$ für die Menge der möglichen Speicherbelegungen.

Je nach mathematischem Ansatz unterscheidet man

Modelle für Rechensysteme

Stichpunkte wie Auftragssysteme, Funktionseinheiten, Nebenläufigkeit, Synchronisation, Unteilbarkeit, Wartesysteme (M/M/m/k), Bedienstrategien (M/G/1) etc.

Siehe auch

Bedeutende Forscher

Literatur

Alexander Asteroth, Christel Baier: Theoretische Informatik. Eine Einführung in Berechenbarkeit, Komplexität und formale Sprachen, Pearson, München 2003, ISBN 3-8273-7033-7
Katrin Erk, Lutz Priese: Theoretische Informatik. Eine umfassende Einführung, Springer, Berlin 2002, ISBN 3-540-42624-8
Herbert Göttler Theoretische Grundlagen der Informatik, Skript, Uni Mainz 2007 http://www.informatik.uni-mainz.de/lehre/tgi/skript.php
Bernhard Heinemann, Klaus Weihrauch: Logik für Informatiker. Eine Einführung, Teubner, Stuttgart 2000, ISBN 3-519-12248-0
John E. Hopcroft u.a.: Einführung in die Automatentheorie, formale Sprachen und Komplexitätstheorie, Pearson, München 2003, ISBN 3-8273-7020-5
John Kelly: Logik im Klartext, Pearson, München 2003, ISBN 3-8273-7070-1
Uwe Schöning: Theoretische Informatik - kurzgefasst, Spectrum Akadem. Verlag, Heidelberg 2003, ISBN 3-8274-1099-1
Ingo Wegener: Theoretische Informatik. Eine algorithmische Einführung, Teubner, Stuttgart 1999, ISBN 3-519-12123-9
Klaus W. Wagner: Einführung in die Theoretische Informatik. Grundlagen und Modelle, Springer, Berlin 1997, ISBN 3-540-58139-1
Klaus Weihrauch: Computability, Springer, Berlin 1987, ISBN 3-540-13721-1
Renate Winter: Theoretische Informatik. Grundlagen mit Übungsaufgaben und Lösungen, Oldenbourg, München 2002, ISBN 3-486-25808-7
Rolf Socher: Theoretische Grundlagen der Informatik, Hanser Verlag, München 2005, ISBN 3-446-22987-6
George M. Reed, A. W. Roscoe, R. F. Wachter: Topology and Category Theory in Computer Science, Oxford University Press 1991, ISBN 0198537603
Klaus Keimel: Domains and Processes, Springer 2001, ISBN 0792371437

Weblinks