Technische Universität Ilmenau

Spezielle Kapitel der Komplexitätstheorie und Berechenbarkeit - Modultafeln der TU Ilmenau

Die Modultafeln sind ein Informationsangebot zu unseren Studiengängen. Rechtlich verbindliche Angaben zum Verlauf des Studiums entnehmen Sie bitte dem jeweiligen Studienplan (Anlage zur Studienordnung). Bitte beachten Sie diesen rechtlichen Hinweis. Angaben zum Raum und Zeitpunkt der einzelnen Lehrveranstaltungen entnehmen Sie bitte dem aktuellen Vorlesungsverzeichnis.

Fachinformationen zu Spezielle Kapitel der Komplexitätstheorie und Berechenbarkeit im Studiengang Master Informatik 2013
Fachnummer101183
Prüfungsnummer2200471
FakultätFakultät für Informatik und Automatisierung
Fachgebietsnummer 224 (Institut für Theoretische Informatik)
Fachverantwortliche(r)PD Dr. Karl-Heinz Niggl
TurnusSommersemester
SpracheDeutsch
Leistungspunkte5
Präsenzstudium (h)45
Selbststudium (h)105
VerpflichtungWahlpflicht
Abschlussmündliche Prüfungsleistung, 30 Minuten
Details zum Abschluss
Anmeldemodalitäten für alt. Leistungen
max. Teilnehmerzahl
Vorkenntnisse

- Automaten, Sprachen und Komplexität

- Logik und Logikprogrammierung

Lernergebnisse

Version 1:  Zertifizierung von FP, FLINSPACE und FPSPACE für imperative Programme

Fachkompetenz:

Die Studierenden kennen die in der Vorlesung vorgestellten Konstruktionen und Beweise im Gebiet der Impliziten Komplexitätstheorie.  Sie kennen die notwendigen Grundlagen aus der Komplexitätstheorie.

Methodenkompetenz:

Die Studierenden können die Konstruktionsmethoden von Beschränkungspolynomen und Zertifikaten präzise beschreiben und die jeweiligen Kriterien für eine Zertifizierung im Fall einer Schleife benennen. Sie können die wesentlichen Konstruktionen und Beweise nachvollziehen und präzise wiedergeben, insbesondere der Nachweis, dass die von einem zertifizierten Programm berechneten Funktionen in einer der fraglichen Komplexitätsklassen (FP, FLINSPACE oder FPSPACE) liegen. Umgekehrt können sie mittels der Basistheoreme zeigen, dass jede  Funktion aus einer der fraglichen  Komplexitätsklassen durch ein zertifiziertes Programm berechnet werden kann.

Version 2:  Polynomialzeit im Kontext funktionaler Programmierung

Fachkompetenz:

Die Studierenden kennen das in der Vorlesung vorgestellte, von Hilbert eingeführte und durch Gödel bekannt gewordene System T, das für das Studium höherstufiger Funktionale und die Entwicklung funktionaler Programmiersprachen grundlegend war.  Ferner kennen sie die Funktionenalgebra BC von  Bellantoni  und  Cook, in dem genau die Funktionen aus FP definiert werden können, sowie das System RA ("ramified affinable" Terms") von Bellantoni, N. und Schwichtenberg, ein Teilsystem von System T, jedoch basierend auf Rekursion auf Notation in allen endlichen Typen, in dem genau die Funktionen aus FP durch RA-Programme berechnet werden können.

Methodenkompetenz:

Die Studierenden können neben Syntax und denotationaler Semantik auch die operationale Semantik von System T (ein via "Reduktionsregeln" basierter Auswertungsmechanismus von T-Programmen) präzise beschreiben und klassische Ergebnisse wie Korrektheit der operationalen Semantik, Starke Normalisierung und Eindeutigkeit der Normalform präzise formulieren und  ihre Beweisstruktur (nach W. Tait) wiedergeben. Ferner können sie die Funktionenalgebra BC präzise beschreiben und die Konstruktion für den Nachweis, dass jede FP-Funktion in BC definierbar ist (die Umkehrung ist einfach), im Kern präzise wiedergeben.

Schließlich können die Studierenden das System RA präzise beschreiben und die Kernideen für seine Konstruktion darlegen. Ferner können sie das induktive Argument, dass jede BC-Funktion in RA definierbar ist, sauber wiedergeben und den vorgestellten Polynomialzeit-Algorithmus zur Auswertung von RA-Programmen in seiner Grundstruktur präzise beschreiben.

Version 3 (alternierend zu Version 1 bzw. Version 2) : Berechenbarkeit

Fachkompetenz:

Die Studierenden kennen die in der Vorlesung vertieften partiell rekursiven Funktionen auf Basis der µ-rekursiven Funktionen sowie die davon abgeleiteten Begriffe der entscheidbaren und rekursiv aufzählbaren Mengen, Nummerierungen für das Rechnen auf nicht-natürlichen Zahlen und Standardnummerierungen der berechenbaren Zahlenfunktionen und ihre Charakterisierung. Sie sind mit den Konzepten Reduzierbarkeit von Problemen und das Rechnen mit Indizes von berechenbaren Zahlenfunktionen vertraut, insbesondere mit dem Fixpunktsatz, dem Satz von Rice und dem Satz von Rice/Shapiro. Ferner kennen sie die Konzepte einer produktiven, kreativen und simplen Menge zur Klärung der Frage, ob es rekursiv aufzählbare, aber nicht entscheidbare  Mengen gibt, die nicht zum Halteproblem H oder dem Selbstanwendungs-problem K äquivalent und somit "leichter" sind. Sie sind mit unlösbaren Problemen wie das Postsche Korrespondenzproblem und der Unentscheidbarkeit der Prädikatenlogik 1. Stufe vertraut, sowie mit einer Variante des ersten Gödelschen Unvollständikeitssatzes, wonach jedes korrekte Beweissystem für arithmetische Formeln unvollständig ist. Sie kennen die arithmetische Hierarchie und die damit verbundenen Fragestellungen.

Methodenkompetenz:

Die Studierenden können mittels µ-Kalkül  bzw. Kalkül  PR der primitiv rekursiven Funktionen nachweisen, dass konkrete einfache Funktionen partiell bzw. primitiv rekursiv sind und grundlegende Abschlusseigenschaften der partiell bzw. primitiv rekursiven Funktionen bzw. der rekursiv aufzählbaren oder entscheidbaren bzw. primitiv rekursiven Mengen gelten.  Sie können die Konstruktion einer Aufzählungsfunktion aller k-stelligen partiell rekursiven Funktionen wiedergeben und mittels des S-m-n-Theorems zeigen, dass man zu jeder aufgezählten Funktion f mit Nummer i die Gödelnummer eines GOTO-Programms berechnen kann, das f berechnet.  Ferner können die Studierenden präzise formulieren und beweisen: Kleenes Normalformsatz und Rekursionssatz, sowie Fixpunktsatz, der Satz von Rice und Rice/Shapiro. Sie können damit die Unentscheidbarkeit von grundlegenden konkreten semantischen Fragen an Programmen zeigen. Die Studierenden können die vorgestellte Codierung der prädikatenlogischen Formeln und Herleitungen in einem vollständigen Kalkül des natürlichen Schließens wiedergeben und die Konstruktion angeben, dass jede partiell rekursive Funktion arithmetisch repräsentierbar und jede rekursiv aufzählbare Menge arithmetisch ist. Sie können die arithmetische Hierarchie definieren und die entscheidbaren und rekursiv aufzählbaren Mengen korrekt einordnen sowie von konkreten Problemen ihre Lage in der Hierarchie angeben.

Inhalt

Version 1:

Die Vorlesung gibt Antworten auf die Grundfrage (der impliziten Komplexitätstheorie), ob man aus der Syntax von imperativen Programmen auf ihre Laufzeit bzw. ihren Platzbedarf schließen kann. 

Es werden dazu zunächst Stack- und Loop-Programme eingeführt  und Ergebnisse (Basistheoreme) aus einer Arbeit von Kristiansen und N. erarbeitet und bewiesen:

  • FP = Stackprogramme mit µ-Maß 0
  • FLINSPACE = Loop-Programme mit µ-Maß 0

Das µ-Maß ist dabei ein effizientes Verfahren, das jedem solchen Programm eine natürliche Zahl  zuordnet. Das Fehlen wesentlicher Konzepte moderner Programmiersprachen -- wie z.B. das Zuweisungskonzept, gemischte Datenstrukturen und benutzerfreundliche Bibliotheksfunktionen -- gibt Anlass zu der Frage, in wieweit die Basistheoreme und die darin tragenden Kernideen auf moderne Programmiersprachen erweitert werden können.

Es werden daher imperative Programme betrachtet, die aus beliebigen Basisanweisungen mittels Anweisungsfolgen, bedingten Anweisungen und FOR-Schleifen (loop, foreach und powerloop) aufgebaut sind. Solche Programme arbeiten auf Variablen X1, ..., X, wovon jede eine beliebige Datenstruktur (Stack, Register, Array, Baum, Graph, ...) repräsentieren kann, solange dafür implizit ein (sinnvoller) Größenbegriff  |Xi| definiert ist.  Ziel der Vorlesung ist eine effiziente Methode zur Zertifizierung von 

  • polynomiellem Zeitbedarf (FP) und
  • linearem bzw. polynomiellem Platzbedarf (FLINSPACE bzw. FPSPACE)

für solche Programme. Kern der Methode ist ein effizienter Matrizen-Kalkül für die Zertifizierung der polynomiellen Größenbeschränktheit von solchen imperativen Programmen mit polynomiell größenbeschränkten Basisanweisungen.  Das Zertifikat für ein Programm in n Variablen ist eine (n+ 1)x(n+1)-Matrix über der Vergißmenge {0,1,unendlich}. Die Methode ist konstruktiv in dem Sinne, dass neben dem Zertifikat -- wie bei den Basistheoremen -- auch stets Beschränkungspolynome für X1, ..., Xbestimmt werden.

Die folgenden Charakterisierungstheoreme (N. und Wunderlich 2006) werden erarbeitet und bewiesen:  

  • FP = Zertifizierte Stringprogramme (Stack-Programme mit beliebigen polynomialzeit-berechenbaren Basisanweisungen)
  • FLINSPACE = Zertifizierte verallgemeinerte Loop-Programme (Loop-Programme mit beliebigen in linearem Platzbedarf berechenbaren Basisanweisungen)
  • FPSPACE = Zertifizierte Power-Stringprogramme (Stringprogramme erweitert um Schleifen, deren Rumpf exponentiell oft in der Größe der Kontrollvariablen iteriert wird, mit beliebigen in polynomiellem Platzbedarf berechenbaren Basisanweisungen)

Das Verfahren steht als Java-Applet zur Verfügung. An Schulbeispielen wie binäres Addieren, binäres Multiplizieren oder Insertion-Sort kann man die Theorie "laufen" lassen, also  Zertifikate berechnen und Beschränkungspolynome extrahieren.

Version 2: 

Das von Hilbert eingeführte und durch Gödel bekannt gewordene System T war grundlegend für das Studium höherstufiger Funktionale und die Entwicklung von funktionalen Programmiersprachen mit komplexen (Daten) Typen. Zentral darin ist das Prinzip der "höherstufigen Rekursion", eine Verallgemeinerung der primitiv rekursiven Rekursion: Die in einer Rekursion berechneten Objekte sind nicht Grunddaten (z. B. natürliche Zahlen in Binärdarstellungen), sondern "Funktionale beliebigen Typs", d. h. Abbildungen, die andere Abbildungen als Argumente nehmen und wieder Abbildungen oder Grunddaten als Resultate liefern. Objekte in System T sind einfach getypte Lambda-Terme, angereichert um Konstanten für den zugrunde liegenden Datentyp (z.B. Null und Nachfolger zur Darstellung der natürlichen Zahlen) sowie Konstanten R6 für "Rekursion in allen endlichen Typen 6".

Die Vorlesung bespricht zunächst Syntax, denotationale und operationale Semantik von System T, wobei Letzteres ein Auswertungsmechanismus von Termen in T via "Reduktionsregeln"  ist. Es werden u.a. folgende klassische Ergebnisse bewiesen:

  • Korrektheit der operationalen Semantik
  • Starke Normalisierung und Eindeutigkeit der Normalform (jede Reduktionsfolge für einen Term in T bricht nach endlich vielen Schritten mit einem eindeutig bestimmten Term in Normalform ab.)

Geschlossene Terme t vom Grundtyp (Programme) reduzieren also zu einem eindeutig bestimmten Numeral, das den Wert von t darstellt. Dies stellt den Auswertungsmechanismus von Programmen in T dar.

Danach wendet sich die Vorlesung der bis vor wenigen Jahren offenen Frage (seit den 1960er Jahren)  zu, wie man System T syntaktisch so einschränken kann, dass darin genau die Funktionen aus FP berechnet werden. In T kann man ja schon durch eine einzige höherstufige  Rekursion (des Typs nat -> nat) -- und darin geschachtelt eine primitive Rekursion -- die Ackermannfunktion definieren, die bekanntlich  jedes primitiv rekursive Wachstum überschreitet.

Die Vorlesung bespricht zunächst einen ersten Durchbruch zu dieser Frage für grundstufige Rekursion, nämlich die "Funktionenalgebra" 

  • BC = [0, S0, S1, c, n; SCOMP, SRN]

von Bellantoni und Cook (1992), ein Baukasten zur Beschreibung von Polynomialzeitalgorithmen zur Berechnung von zahlentheoretischen Funktionen in Binärdarstellung (FPTIME, eine Variante von FP).  Darin werden die Argumentpositionen jeder Funktion  in "normale" und "sichere" klassifiziert, wobei "normale" Argumentpositionen Rekursionen (auf Binärdarstellungen von natürlichen Zahlen, daher 0 und die binären Nachfolger S0, S1) kontrollieren können, während "sichere" Argumentpositionen keine Rekursion kontrollieren dürfen. Entsprechend gibt es die Schemata "sichere Komposition" (SCOMP) und "sichere Rekursion auf Notation"  (SRN). In der Vorlesung wird dann der folgende wichtige Satz in einer modernen Fassung bewiesen:

  • BC = FPTIME

Die darin tragenden Ideen plus "Zähmung" der höherstufigen Rekursion führten 2000 auf eine syntaktische Variante RA von System T, basierend auf Konstanten S0, S1 für Binärzahldarstellungen und Konstanten RN6 für höherstufiger Rekursion auf Notation des Typs

  • 6 ->  !(!nat -> 6 -> 6)  ->  !nat -> 6 für jeden "sicheren" Typ 6.

Im weiteren Fortgang der Vorlesung wird zunächst die Syntax von RA ("ramified affinable terms") zusammen mit den zentralen Ideen für das Design von RA besprochen und dann der folgende Satz (Bellantoni, N. und Schwichtenberg) bewiesen:

  • RA = FPTIME (in RA sind genau die Funktionen aus FPTIME berechenbar)

Dazu werden die Funktionen aus BC in RA eingebettet und es wird ein Polynomialzeitalgo-rithmus zur Auswertung von RA-Programmen angegeben.

Version 3: 

Die Vorlesung behandelt klassische Resultate aus der Rekursionstheorie zu Fragen der Berechenbarkeit auf Basis der µ-rekursiven Funktionen, zu Entscheidbarkeit und Unentscheidbarkeit. Sie beginnt mit den primitiv rekursiven Funktionen PR und Relationen Rel(PR) und beweist grundlegende Abschusseigenschaften:   

  • Abgeschlossenheit von PR unter Fallunterscheidung, beschränktem µ-Operator, und Wertverlaufsrekursion
  • Abgeschlossenheit von Rel(PR) unter Aussagenlogik und beschränkter Quantifikation

Insbesondere wird eine primitiv rekursive Paarcodierung pi und Dekodierung pi_0 und pi_1 eingeführt sowie eine darauf aufbauende längen-selbstverwaltende Codierung endlicher Zahlenfolgen (nach W. Buchholz) mit primitiv rekursiver Längen- und Dekodierungsfunktion. Jedem GOTO-Programm kann so in eleganter Weise eine Gödelnummer zugeordnet werden. Die Menge G solcher Gödelnummern ist selbst primitiv rekursiv.

Für festes k1 >= 1 wird eine Aufzählungsfunktion phi^k aller k-stelligen partiell rekursiven Funktionen konstruiert. phi^k ist selbst partiell rekursiv (UTM-Eigenschaft) und mit Hilfe des S-m-n-Theorem wird gezeigt, dass sich jede (k+1)-stellige Funktion f in der Form f(i, n1, ..., nk) = phi^k (s(i), n1, ..., nk) für ein s in PR darstellen lässt (SMN- Eigenschaft). Darauf aufbauend werden gezeigt:

  • Die partiell rekursiven Funktionen sind abgeschlossen unter Fallunterscheidung und starker Fallunterscheidung.
  • Normalformsatz der partiell rekursiven Funktionen
  • Rekursionssatz
  • Fixpunktsatz

Nach Einführung der bekannten Konzepte der entscheidbaren, rekursiv aufzählbaren und semi-entscheidbaren Mengen, des Halteproblems H und Selbstanwendungsproblem K sowie der Reduzierbarkeit (<=_m) mit Merkregeln für die Reduktionsmethode werden folg. Themen behandelt:

  • Charakterisierung der rekursiv aufzählbaren Mengen
  • H und K sind reduktionsäquivalent (=m)
  • Der Satz von Rice mit Anwendungen bzgl. konkreter unentscheidbarer Mengen wie Tot, Nonempty, Fin, Inf, Cof, Rec, Corf , Equ
  • Der Satz von Rice/Shapiro mit Anwendungen -- obige Beispielmengen sind nicht einmal rekursiv aufzählbar.

Nach Einführung der Konzepte einer produktiven, kreativen und simplen Menge werden gezeigt:

  • Merkregeln für produktive Mengen
  • Charakterisierung der produktiven und kreativen Mengen
  • Es gibt simple Mengen, d. h. rekursiv aufzählbare Mengen, die nicht entscheidbar, aber "leichter" als K und H sind.

Nach Wiederholung des binären Postschen Korrespondenzproblems 0-1-PKP wird behandelt:

  • Unentscheidbarkeit der Prädikatenlogik Stufe
  • Arithmetische Repräsentierbarkeit der partiell rekursiven Funktionen
  • Jede rekursiv aufzählbare Menge ist arithmetisch.
  • Codierung der prädikatenlogischen Formeln und Herleitungen in einem vollständigen Kalkül (natürliches Schließen formuliert als Sequenzenkalkül)
  • Gödelscher Unvollständigkeitssatz: Jedes korrekte Beweissystem für arithmetische Formeln ist unvollständig.
  • Die arithmetische Hierarchie: Eine Schichtung der arithmetischen Mengen in eine echt aufsteigende Hierarchie von Klassen, definiert durch Folgen alternierender Quantorenpräfixe entscheidbarer Mengen. Die unterste Schicht besteht aus den entscheidbaren Mengen, die zweit-unterste aus den rekursiv aufzählbaren Mengen, alle anderen Schichten also aus nicht rekursiv aufzählbaren Mengen.
Medienformen

Folien (auch Beamer) mit Definitionen, Lemmata und Theoremen, und Tafelvortrag für  Beispiele, Beweisen oder Konstruktionen.

Literatur
  • Kristiansen, K.-H. Niggl. On the computational complexity of imperative programming languages. Theoretical Computer Science, Special issue on Implicit Computational Complexity, Editor J.-Y. Marion, 318(1-2):139--161, Elsevier 2004.
  • H. Niggl, H. Wunderlich. Certifying polynomial time and linear/polynomial space for imperative programs. SIAM Journal on Computing, 35(5):1122--1147, March 3, 2006.
  • J. Bellantoni, S. Cook. A new recursion-theoretic characterization of the polytime functions. Computational Complexity, 2 (1992), pp. 401-415.
  • J. Bellantoni, K.-H. Niggl, H. Schwichtenberg. Higher type recursion, ramification and polynomial time. Annals of Pure and Applied Logic, 104:17--30, 2000.
  • Rogers, Jr. Theory of Recursive Functions and Effective Computability. The MIT Press, Cambridge, Massachusetts, 1987.
Lehrevaluation

Informationen und Handreichungen zur Pflege von Modul- und Fachbeschreibungen durch den Modul- oder Fachverantwortlichen finden Sie auf den Infoseiten zum Modulkatalog.