Bereich: |
III, Wahlpflichtvorlesung: 4 Std.
(+2Ü)
Die diesjährige Logik-Vorlesung kann
wegen der starken Überlappung nicht zusammen mit Termersetzung oder
Lambda-Kalkül in die DHP eingebracht werden. |
Zeit und Ort: |
Mo 8:30 - 10:00, MI 00.04.011 (HS
2); Fr 10:15 - 11:45, MI HS 3 |
Beginn: |
Die Vorlesung beginnt am
Montag, den 7. April. |
Zentralübung: |
Mo 16:00 - 17:30, MI 00.04.011,
beginnt am Montag, den 14. April.
Übungsblätter. |
Übungsleitung: |
Clemens Ballarin |
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
- Abstrakte Reduktionssysteme
- Abstrakte Reduktionssysteme
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.
- Fundierte Induktion
Satz: Fundierte Induktion gilt gdw die
Reduktion terminiert. Königs Lemma.
- Terminationsbeweise
Einbettung in (N,>). Satz: Endlich
verzweigte Reduktionen terminieren gdw sie in (N,>) einbettbar sind.
- Lexikographische Ordnungen
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.
- Multimengenordnung
Multimengen und die Multimengenordnung
von Dershowitz und Manna. Satz: Die Multimengenordnung termiert gdw
die zugrundeliegende Ordnung terminiert.
- Konfluenz
Satz: Halbkonfluenz = Konfluenz. Satz:
Termination & Lokale Konfluenz => Konfluenz.
- Gleichungslogik
- Terme und Substitutionen
Signaturen, Terme, Positionen in
Termen, Subterme an Positionen, Ersetzung von Subtermen,
Substitutionen, Komposition von Substitutionen.
- Termersetzung und
Gleichungslogik
Identitäten, Termersetzung ($\to_E$),
Gleichungslogik ($=_E$). Äquivalenz von Gleichungslogik und
Termersetzung.
- Semantik der Gleichungslogik
Algebren. Gültigkeit und semantische
Konsequenz (|=). Birhoffs Theorem über die Äquivalenz von |- und |=.
- Gleichungsprobleme
Wortproblem, Unifikation, Matching.
- Wortproblem
Unentscheidbar für kombinatorische
Logik und Halbgruppen; entscheidbar für konvergente TRS.
- Syntaktische Unifikation
Grundbegriffe: Quasiordnung auf
Substitutionen, allgemeinster Unifikator, Idempotenz.
- Unifikation durch Transformation
- Unifikation von Termgraphen
Von einem exponentiellen zu einem
quasilinearen Algorithmus.
- Termination von
Termersetzungssystemen
Im Schnelldurchlauf, ohne Beweise:
- Termination ist unentscheidbar
Reduktion des uniformen Halteproblems
von Turingmaschinen auf das Terminationsproblem von TRS.
- Einige (un)entscheidbare
Teilklassen Entscheidbar falls rechts keine Variablen.
Unentscheidbar schon für eine Regel. Falls alle Funktionen
einstellig, dann schon mit 3 oder mehr Regeln unentscheidbar; offen
für 1 oder 2 Regeln.
- Reduktionsordnungen
Ein TRS terminiert gdw es in einer
Reduktionsordnung enthalten ist.
- Die Interpretationsmethode
Interpretation mit monotone Funktionen
liefert eine Reduktionsordnung. Anwendung: Polynomordnungen.
- Konfluenz von Termersetzungssystemen
Satz: Im allgemeinen unentscheidbar.
- Kritische Paare
Das Kritische Paar Lemma. Korollar:
Konfluenz ist entscheidbar für endliche terminierende TRSs.
- Vervollständigung von
Termersetzungssystemen
Knuth-Bendix Algorithmus. Beispiel:
Gruppen. Entscheidbarkeit des Wortproblems für endliche Mengen von
Grundidentitäten mit Hilfe von Vervollständigung.
- Orthogonale TRSs
Satz: Orthogonale TRSs sind konfluent.
Beweis mit paralleler Reduktion. Anwendung: Funktionale Programme
sind konfluent.
Ein Beispiel für Gleichungsbeweise:
Kleine
Axiome für Boolesche Algebra
Interaktive Experimente mit dem
Waldmeister System.
Teil II: Lambda-Kalkül
- Untypisierter lambda-Kalkül
- Syntax
Terme; Klammerungsregeln; Currying;
Statische Bindung; Freie und gebundene Variablen; Substitution;
alpha-Konversion.
- Beta-Reduktion
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).
- Eta-Reduktion
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.
- Reduktionsstrategien
Thm (ohne Beweis): Reduktion des
jeweils linkesten beta-Redexes führt zu einer beta-Normalform, falls
eine existiert.
- Lambda-Kalkül als
Gleichungstheorie
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.
- Lambda-Kalkül als
Programmiersprache
Datentypen: Wahrheitswerte, Paare
- Typisierte lambda-Kalküle
Motivation: Typen vermeiden logische
Widersprüche (Frege, Russel, Church) und Programmierfehler.
Kategorisierung von Typsystemen: statisch/dynamisch und monomorph/polymorph.
- Der einfach typisierte
Lambda-Kalkül
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.
- Typinferenz für einfach
typisierte Terme
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").
- Let-Polymorphismus
Erweiterung des Typsystems um
allquantifizierte Typschemata. Erweiterte Typisierungsregeln mit
expliziten Quantorregelen. Syntax-gesteuertes Regelsystem.
- Der Curry-Howard Isomorphismus
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.
Hörerkreis:
Studenten/-innen der Informatik und Mathematik
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.
Die Vorlesung orientiert sich stark an
Weitere Literatur:
- Jürgen Avenhaus. Reduktionssyteme,
Springer, 1995
- Hendrik Pieter Barendregt. The
Lambda Calculus, its Syntax and Semantics, North-Holland, 2nd
edition, 1984
- Jean-Yves Girard, Yves Lafont, and Paul
Taylor. Proofs and Types, Cambridge Tracts in Theoretical
Computer Science, Cambridge University Press, 1989
- Chris Hankin. Lambda Calculi. A
Guide for Computer Scientists, Ofxord University Press, 1994
- J. Roger Hindley and Jonathan P.
Seldin. Introduction to Combinators and Lambda Calculus,
Cambridge University Press, 1986
|