TU München - Fakultät für
Informatik
Software- and Systems Engineering Research Group
|
|
TU München - Fakultät für
Informatik |
|
|
Home | Forschung/Kompetenz | Lehre | Personen | Publikationen | Abschlussarbeiten | Sonstiges | Kontakt | |
 |
Vorlesung | Wintersemester 2004/05 |
 |
Inhalt:Diese Vorlesung konzentriert sich ausschliesslich auf Gleichungslogik statt der sonst üblichen erststufigen Logik. Sie kombiniert die Themen Termersetzung und Lambda-Kalkül mit einer logischen Sicht.Teil I: Termersetzung
Grundlegende Definitionen: reflexive, transitive, symmetrische Hüllen; Termination, Konfluenz, Church-Rosser. Satz: Church-Rosser gdw Konfluenz. Satz: Äquivalenz ist für konvergente Reduktionen durch Vergleich von Normalformen entscheidbar. Satz: Fundierte Induktion gilt gdw die Reduktion terminiert. Königs Lemma. Einbettung in (N,>). Satz: Endlich verzweigte Reduktionen terminieren gdw sie in (N,>) einbettbar sind. Lexikographisches Produkt von Ordnungen. Satz: Lex. Produkt terminiert gdw die Komponenten terminieren. Lexikographische Ordnung auf Strings. Satz: Die lex. Ordnung terminiert gdw die zugrundeliegende Ordnung terminiert. Multimengen und die Multimengenordnung von Dershowitz und Manna. Satz: Die Multimengenordnung termiert gdw die zugrundeliegende Ordnung terminiert. Satz: Halbkonfluenz = Konfluenz. Satz: Termination & Lokale Konfluenz => Konfluenz. Signaturen, Terme, Positionen in Termen, Subterme an Positionen, Ersetzung von Subtermen, Substitutionen, Komposition von Substitutionen. Identitäten, Termersetzung ($\to_E$), Gleichungslogik ($=_E$). Äquivalenz von Gleichungslogik und Termersetzung. Algebren. Gültigkeit und semantische Konsequenz (|=). Birkhoffs Theorem über die Äquivalenz von |- und |=. Wortproblem, Unifikation, Matching. Unentscheidbar für kombinatorische Logik und Halbgruppen; entscheidbar für konvergente TRS. Grundbegriffe: Quasiordnung auf Substitutionen, allgemeinster Unifikator, Idempotenz. Von einem exponentiellen zu einem quasilinearen Algorithmus. Im Schnelldurchlauf, ohne Beweise: Reduktion des uniformen Halteproblems von Turingmaschinen auf das Terminationsproblem von TRS. Ein TRS terminiert gdw es in einer Reduktionsordnung enthalten ist. Interpretation mit monotone Funktionen liefert eine Reduktionsordnung. Anwendung: Polynomordnungen. Satz: Im allgemeinen unentscheidbar. Das Kritische Paar Lemma. Korollar: Konfluenz ist entscheidbar für endliche terminierende TRSs. Knuth-Bendix Algorithmus. Beispiel: Gruppen. Entscheidbarkeit des Wortproblems für endliche Mengen von Grundidentitäten mit Hilfe von Vervollständigung. Satz: Orthogonale TRSs sind konfluent. Beweis mit paralleler Reduktion. Anwendung: Funktionale Programme sind konfluent. Interaktive Experimente mit dem Waldmeister System. Teil II: Lambda-Kalkül
Terme; Klammerungsregeln; Currying; Statische Bindung; Freie und gebundene Variablen; Substitution; alpha-Konversion. Definitionen: Reduktion in Teilterm. Beta hat die Diamanteigenschaft nicht; braucht parallele Reduktion. Parallels beta hat die D.E. auch nicht: braucht geschachtelte Reduktion. Definition der parallelen bottom-up Reduktion >. Lemma: Hat > die D.E. so ist beta konfluent. Thm: > hat die Diamanteigenschaft (ohne Beweis). Lemma: Eta ist lokal konfluent. Fact: Eta terminiert. Korollar: Eta ist konfluent. Lemma: Beta* und eta* kommutieren (ohne Beweis). Lemma von Hindley und Rosen. Korollar: Beta+eta ist konfluent. Thm (ohne Beweis): Reduktion des jeweils linkesten beta-Redexes führt zu einer beta-Normalform, falls eine existiert. Entscheidbarkeit der Konvertibilität von Termen mit Normalform. Unentscheidbarkeit der Konvertibilität bei beta und beta+eta (ohne Beweis), Entscheidbarkeit bei eta (wg. Termination von eta). Äquivalenz von eta und Extensionalität. Datentypen: Wahrheitswerte, Paare Motivation: Typen vermeiden logische Widersprüche (Frege, Russel, Church) und Programmierfehler. Kategorisierung von Typsystemen: statisch/dynamisch und monomorph/polymorph. Syntax der Typen. Implizit und explizit typisierte Terme. Typüberprüfungsregeln. Eigenschaften: 1. Teilterme typkorrekter Terme sind typkorrekt (ohne Beweis). 2. Beta-Reduktion erhält Typen ("Subject reduction") (ohne Beweis). 3. Beta-Reduktion auf typkorrekten Termen terminiert (ohne Beweis). Beta-äquivalenz ist daher entscheidbar, Komplexität aber nicht-elementar; in der Praxis aber gutartig. Korollar: Im einfach typisierte Lambda-Kalkül sind nur totale Funktionen repräsentierbar. Thm (ohne Beweis): Jede berechenbare Funktion ist als geschlossener typkorrekter lambda-Term darstellbar, der als einzige Konstante den Fixpunktoperator enthät. Die Regeln. Typkorrekte Terme haben keinen eindeutigen Typ mehr, aber immer einen allgemeinsten Typ. Dieser kann durch eine Prolog-artige Interpretation der Regeln berechnet werden ("rückwärts rechnen"). Erweiterung des Typsystems um allquantifizierte Typschemata. Erweiterte Typisierungsregeln mit expliziten Quantorregelen. Syntax-gesteuertes Regelsystem. Die Grundidee: Typen = Formeln, Lambda-Terme = Beweise. Beta-Reduktion = Beweis-Reduktion. Beweis der Entscheidbarkeit der konstruktiven Aussagenlogik (nur mit ->) durch Suche nach Beweisen in Normalform. Voraussetzungen: Vordiplom Empfehlenswert für: jegliche Fragestellungen und Anwendungen von Logik-basierten Formalismen (ein Pleonasmus!), von der Softwarespezifikation bis zur Künstlichen Intelligenz. Übungsschein: Einen
Schein erhält, wer mindestens 40% der Punkte aus den Hausaufgaben
und Programmieraufgaben erreicht und erfolgreich an der Semestralprüfung
teilnimmt.
Literatur:Die Vorlesung orientiert sich stark an
|