250123 VO Einführung in die Theoretische Informatik WS 2008

Kann man "Algorithmus", "berechenbar" etc überhaupt (befriedigend) definieren? (Ja!)
Gibt es Funktionen die man nicht berechnen, Probleme die man nicht entscheiden kann? (Ja!)
Kann man das auch beweisen? (Ja!)
Auch für natürliche Beispiele in der Mathematik? (Ja! ZB Wortproblem in Gruppen, Diophantische Gleichungen, Halteproblem, Logische Folgerung.)

Eckdaten:

Vortragende: Jakob Kellner, Ajdin Halilovic, Kurt Gödel Research Center.
Inhalt: Rekursionstheorie, Komplexitaetstheorie.

Ort:

UZA 2, Ebene 1, Seminarraum Mathematik 2A180.
Das UZA 2 erreich man über die Althanstrasse oder die Nordbergstrasse.

Vorkenntnisse/Voraussetzungen:

Die Vorlesung richtet sich an MathematikerInnen und interessierte InformatikerInnen. Es sind keine logischen Vorkenntnisse erforderlich. Der Beginn der Vorlesung behandelt die ersten Abschnitte von Sebastiaan Terwijns Skriptum.

Jedenfalls tut man sich mit der Vorlesung wesentlich leichter, wenn man schon einmal etwas programmiert hat (egal in welcher Sprache, Basic, C, perl, was auch immer). Und mit elementaren Kenntnissen in Logik (zB aus der Vorlesung Grundbegriffe der mathematischen Logik) kann man die Bedeutung der Resultate besser würdigen.

Genauere Beschreibung:

Die Vorlesung beschränkt sich auf die gebiete der theoretischen Informatik, die für MathematikerInnen am relevantesten sind: Rekursionstheorie und Komplexitätstheorie.

Wir definieren berechenbar (rekursiv) und rekursiv aufzählbar (mit Hilfe von zB Turing Maschinen); beweisen grundlegende Eigenschaften dieser Begriffe; zeigen die Unentscheidbarkeit des Halteproblems (es gibt kein Verfahren das entscheidet ob ein gegebenes Programm terminiert oder nicht).

Wir erwähnen grundlegende Konzepte der Komplexitätstheorie (hier fragt man nicht nur, ob eine Funktion berechenbar ist, sondern auch zB wie schnell sie berechnet werden kann).

Weitere mögliche Themen (abhängig von Interesse und Vorbildung der TeilnehmerInnen):

Rekursionstheorie:

• Fixpunktsatz. Anwendung: Satz von Rice. (Nicht nur die Halte-Eigenschaft, sondern jede funktionelle Programmeigenschaft ist unentscheidbar.)
• Für logisch vorgebildetes Publikum: (Vollständigkeitssatz) Die logischen Folgerungen einer aufzählbaren (first order) Axiomenmenge sind aufzählbar. Die logischen Folgerungen einer entscheidbaren Axiomenmenge (selbst der leeren) sind aber nicht entscheidbar. Gödelscher Unvollständigkeitssatz: keine (unter Folgerungen abgeschlossene) Theorie die Robinsons Q enthält ist rekursiv.
• Anwendungen in anderen mathematischen Gebieten, je nach Interesse: Zahlentheorie/diophantische Gleichungen: Das 10te Hilbertsche Problem (entscheide, ob polynom ganzzahlige Lösung hat) ist unentscheidbar. Algebra: Das Wortproblem in Gruppen ist unentscheidbar.

Komplexitätstheorie:

• Verschiedene Begriffe der Komplexität: statisch (Kolmogorov: was ist die kürzeste Programmlänge, um einen gegebenen Output zu generieren?); dynamisch (benötigte Zeit, benötigter Speicher etc); worst-case und average-case etc.
• P/NP: nichtdeterministische Maschinen, NP vollständige Probleme (SAT etc), das P/NP Problem
• Wichtige Beispiele für Problemen mit optimalen Algorithmen, zB Sortieralgorithmen.
• Für jedes Komplexitätsmaß und jedes Maschinenmodell gibt es berechenbare Funktionen, die keine optimale Lösung (Algorithmus) haben.
• Für logisch vorgebildetes Publikum: Presburger Arithmetik oder die Theorie der reell abgeschlossenen Körper ist entscheidbar. Man kann aber beweisen dass jeder Algorithmus notwendigerweise enorm kompliziert (hyperexponentiell) sein muss.

Literatur:

• Für die Rekursionstheorie folgen wir weitgehend dem Skriptum (ver 2008, PDF) von Sebastiaan Terwijn, ausgenommen Kapitel 5 und 6. Zusätzlich behandeln wir ein wenig Komplexitätstheorie, dazu wird ein eigenes Skriptum erstellt.
• Boolos, Geoffrey: Computability and Logic. Eine sehr einfache und schöne Einführung.
• Oddifreddi: Classical Recursion theory. Eine recht vollständiges Nachschlagwerk.

Zusammenfassung:

Eine Kurz-Zusammenfassung und ein paar Bemerkungen hier.