|
Termersetzungssysteme (TErSys)7.5 ECTS (englische Bezeichnung: Term Rewriting)
(Prüfungsordnungsmodul: Vertiefungsmodul Theoretische Informatik)
Modulverantwortliche/r: Sergey Goncharov Lehrende:
Sergey Goncharov
Start semester: |
SS 2014 | Duration: |
1 semester | Cycle: |
jährlich (SS) |
Präsenzzeit: |
60 Std. | Eigenstudium: |
165 Std. | Language: |
Deutsch oder Englisch |
Lectures:
Inhalt:
Grundlegende Begriffe und Kernergebnisse der Theorie der Termersetzungssysteme und ihr Zusammenhang mit anderen Gebieten der Theoretischen Informatik werden behandelt:
Terminierung, Konfluenz, Normalformen, kanonische Termersetzungssysteme.
Techniken für Konfluenzbeweise: Newman's Lemma, Hindley-Rosen Lemma, kritische Paare, Knuth-Bendix Vervollständigungsverfahren.
Techniken für Terminierungsbeweise: polynomische Interpretation, wohlfundierte syntaktische Ordnungen (lexikographische Pfadordnung, Multimengen-Pfadordnung).
Starke Normalisierung für typisiertes Lambda-Kalkül, Konfluenz von typisiertem Lambda-Kalkül mit Fixpunkten (PCF).
Beziehung zwischen Termersetzungssystemen und Logik durch Curry-Howard Korrespondenz und Gentzens Cut-Eliminations-Beweis für intuitionistische Logik.
Termersetzungssysteme als Turing-vollständige Programmierungssprache.
Lernziele und Kompetenzen:
- Die Studierenden kennen die Kernbegrieffe von Termersetzungssystemen (Konfluenz, Terminierung, Normalform, kanonische Termersetzungssysteme, kritisches Paar) und erklären diese.
Die Studierenden kennen die Kernergebnisse von Termersetzungssystemen (Newman's Lemma, Hindley-Rosen Lemma, starke Normalisierung für typisiertes Lambda-Kalkül) und können diese auf konkrete Beispiele anwenden.
Die Studierenden beherrschen die Methoden und Techniken zur Sicherstellung von Terminierung und Konfluenz (polynomische Interpretation, Knuth-Bendix Vervollständigungsverfahren, Terminierungsbeweise durch wohlfundierte syntaktische Ordnungen).
Die Studierenden wenden die Werkzeuge von Termersetzungssystemen an um formale Definitionen durch Termersetzungssysteme zu entwickeln. Sie können dabei Zwischenergebnise analysieren und bearbeiten um notwendige Eigenschaften (Konfluenz, Terminierung, starke/schwache Normalisierung) sicherzustellen.
Literatur:
- Baader, Franz; Nipkow, Tobias (1998). Term Rewriting and All That. Cambridge University Press.
Marc Bezem, Jan Willem Klop, Roel de Vrijer ("Terese"), Term rewriting systems, Cambridge University Press, 2003.
Weitere Informationen:
www: http://www8.cs.fau.de/course:rewr
Verwendbarkeit des Moduls / Einpassung in den Musterstudienplan:
- Informatik (Bachelor of Science)
(Po-Vers. 2009w | Wahlpflichtbereich (5. und 6. Semester) | Wahlpflichtmodule | Vertiefungsmodul Theoretische Informatik)
Dieses Modul ist daneben auch in den Studienfächern "Informatik (Master of Science)" verwendbar. Details
Studien-/Prüfungsleistungen:
Prüfung Termersetzungssysteme (Prüfungsnummer: 148641)
(englischer Titel: Term rewriting exam)
- Prüfungsleistung, mehrteilige Prüfung, Dauer (in Minuten): 30, benotet
- Anteil an der Berechnung der Modulnote: 100.0 %
- weitere Erläuterungen:
In die Prüfungsnote gehen zu 50% die Leistungen aus der Bearbeitung von Übungsaufgaben ein.
- Erstablegung: SS 2014, 1. Wdh.: WS 2014/2015
|
|
|