Fakultät für Informatik

TU München - Fakultät für Informatik
Software- and Systems Engineering Research Group

TUM

Vorlesung | Wintersemester 2006/07
Logik (Gleichungslogik)
Prof. Tobias Nipkow

 
 

 
Umfang:  4 Std. (+2Ü)
Zeit und Ort: Mi. 10:15-11:45, Do. 12:15-13:45, HS 2 (MI 00.04.011)
Beginn: Die Vorlesung beginnt in der ersten Woche.
Zentralübung: Do. 15:00 - 16:30
Übungsleitung: Norbert Schirmer

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 (|=). Birkhoffs 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.
Interaktiver Lambda-Kalkül Reduzierer

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.
 

Literatur:

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. An Introduction to Lambda Calculi for Computer Scientists, King's College Publications, 2004 
  • J. Roger Hindley and Jonathan P. Seldin. Introduction to Combinators and Lambda Calculus, Cambridge University Press, 1986 

© Software & Systems Engineering Research Group
Sitemap |  Kontakt/Impressum
Letzte Änderung: 2006-12-13 19:34:51