|
Termersetzungssysteme (TErSys)7.5 ECTS (englische Bezeichnung: Term Rewriting)
Modulverantwortliche/r: Sergey Goncharov Lehrende:
Sergey Goncharov
Startsemester: |
SS 2014 | Dauer: |
1 Semester | Turnus: |
jährlich (SS) |
Präsenzzeit: |
60 Std. | Eigenstudium: |
165 Std. | Sprache: |
Deutsch oder Englisch |
Lehrveranstaltungen:
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: Das Modul ist im Kontext der folgenden Studienfächer/Vertiefungsrichtungen verwendbar:
- Informatik (Bachelor of Science)
(Po-Vers. 2009s | Wahlpflichtbereich (5. und 6. Semester) | Wahlpflichtmodule | Vertiefungsmodul Theoretische Informatik)
- Informatik (Bachelor of Science)
(Po-Vers. 2009w | Wahlpflichtbereich (5. und 6. Semester) | Wahlpflichtmodule | Vertiefungsmodul Theoretische Informatik)
- Informatik (Master of Science)
(Po-Vers. 2010 | Wahlpflichtbereich | Säule der theoretisch orientierten Vertiefungsrichtungen | Vertiefungsmodul Theoretische Informatik)
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
|
|
|
|
UnivIS ist ein Produkt der Config eG, Buckenhof |
|
|