|
Term Rewriting Systems
(V3 + Ü2, WS 2015/16)
|
|
If you have any question, please write to
florian.frohn@cs.rwth-aachen.de!
News
-
The second exam will be oral. It takes place on Friday, 18th of March. Each registered student will be informed about her or his appointment by email.
-
The exam inspection takes place on Monday, 29th of February, 9:00 - 10:30 am, in room 4201b (seminar room i2).
-
The results of the first exam are now available in the exercise managements system. Some statistics:
-
Average grade: 2.6
-
Median grade: 2.3
-
Success rate: 83.3%
-
You can now see your admission status in the exercise management system. Every student with at
least 45% of the exercise points qualified for the exam.
-
The exam takes place on Monday, 22th of February, 2:30 - 4:30 pm (14:30 - 16:30), in Fo 1.
-
We have posted the old exams from previous years in order to help for the preparation of the exam.
- The last lecture took place on Tuesday, January 19, 2016, and the last exercise
course took place on Friday, January 29, 2016.
-
The exercise management system is available here.
Course of Studies
This lecture is suitable for the following students:
- Master Informatik
- Master Software Systems Engineering
- Master Mathematik
- Bachelor Informatik
- Since this is an "introductory Master course", it can also be attended as
a "Bachelor-Wahlpflichtveranstaltung" (Theory) for students of Bachelor Informatik.
- It is also possible to attend this lecture already as a student of
Bachelor Informatik and to transfer the credits afterwards when enrolling in
the Master Informatik program.
This lecture is also particularly suitable for a combination with "Functional Programming"
and "Logic Programming" in a depth oral colloquium (Schwerpunktkolloquium) for students
of Master Informatik and Master SSE.
Area
Theoretical Computer Science, Theoretical Foundations of SSE
Language
English
Course Notes
The course notes are available here (in German): Course Notes (Version of September 22, 2011)
You can also find
inofficial video
recordings (in German) of a part of the lecture in 2004 provided by Fachschaft I/1 MPI.
Contents
Term rewriting systems are used for computations and mechanized proofs with
equations. All functional programming languages are based on term
rewriting systems, too. Therefore, term rewriting systems are used
in many areas like automated program verification, specification
of programs, and declarative programming. The following questions
will be discussed in the lecture.
- Is the result of a computation always unique (confluence)?
- Does a computation always stop after a finite number of steps (termination)?
- Does a program fulfill its specification (correctness)?
- How can the completion of an incomplete program be handled automatically?
References
- J. Avenhaus. Reduktionssysteme. Springer-Verlag, 1995.
- F. Baader und T. Nipkow: Term Rewriting and All That. Cambridge University Press, 1998.
- R. Bündgen: Termersetzungssysteme. Vieweg, 1998.
- N. Dershowitz and J.-P. Jouannaud. Rewrite Systems. Handbook of Theoretical Computer Science, Vol. B, Chapter 6: Formal Methods and Semantics, J. van Leeuwen (ed.), North-Holland, pp. 243-320, 1990.
- E. Ohlebusch. Advanced Topics in Term Rewriting, Springer-Verlag, 2002.
- Terese. Term Rewriting Systems. Cambridge University Press, 2003.
The exercises have to be solved in groups of two.
50% of the points on the exercise sheets are
needed in order to take part in the final exam. The exercises can be solved in
either German or English.
-
Exercise 1, Solution 1, Slides 1
-
Exercise 2, Solution 2, Slides 2
-
Exercise 3, Solution 3, Slides 3
-
Exercise 4, Solution 4
-
Exercise 5, Solution 5, Slides 5
-
Exercise 6, Solution 6
-
Exercise 7, Solution
7, Slides 7, Haskell implementation of UNIFY
-
Exercise 8, Solution 8
-
Exercise 9, Solution 9, Slides 9
-
Exercise 10, Solution 10, Slides 10
-
Exercise 11, Solution 11, Slides 11
Here are the transparencies used in the lecture.
- Transparency 1 (October 20, 2015)
- Transparency 2 (October 22, 2015)
- Transparency 3 (October 23, 2015)
- Transparency 4 (October 23, 2015)
- Transparency 5 (October 27, 2015)
- Transparency 6 (October 29, 2015)
- Transparency 7 (October 29, 2015)
- Transparency 8 (November 3, 2015)
- Transparency 9 (November 3, 2015)
- Transparency 10 (November 5, 2015)
- Transparency 11 (November 10, 2015)
- Transparency 12 (November 12, 2015)
- Transparency 13 (November 12, 2015)
- Transparency 14 (November 12, 2015)
- Transparency 15 (November 17, 2015)
- Transparency 16 (November 19, 2015)
- Transparency 17 (November 24, 2015)
- Transparency 18 (November 26, 2015)
- Transparency 19 (December 1, 2015)
- Transparency 20 (December 3, 2015)
- Transparency 21 (December 8, 2015)
- Transparency 22 (December 10, 2015)
- Transparency 23 (December 10, 2015)
- Transparency 24 (December 10, 2015)
- Transparency 25 (December 15, 2015)
- Transparency 26 (December 15, 2015)
- Transparency 27 (December 15, 2015)
- Transparency 28 (January 12, 2016)
- Transparency 29 (January 14, 2016)
- Transparency 30 (January 19, 2016)
Here are the notes from the lecture.
- 1. Introduction (October 20, 2015)
- 2.1 Syntax of Equations (October 20, 2015)
- 2.2 Semantics of Equations
(October 20 + 22, 2015)
- 3.1a Deduction of
Equations (Part 1)
(October 22 + 23 + 27, 2015)
- 3.1b Deduction of
Equations (Part 2)
(October 27 + 29, 2015)
- 3.2a Congruence Closure (Part 1)
(October 29 + November 3, 2015)
- 3.2b Congruence Closure (Part 2)
(November 3 + 5, 2015)
- 3.3a Term Rewriting Systems
(Part 1)
(November 5 + 10, 2015)
- 3.3b Term Rewriting Systems
(Part 2)
(November 10 + 12, 2015)
- 4.1 Noetherian Induction
(November 12 + 17, 2015)
- 4.2 Decidability Results
for Termination
(November 17 + 19, 2015)
- 4.3 Termination with
Reduction Relations
(November 19 + 24, 2015)
- 4.4a
Simplification Orders and Recursive Path Orders (Part 1)
(November 24 + 26, 2015)
- 4.4b
Simplification Orders and Recursive Path Orders (Part 2)
(December 1, 2015)
- 5.1 Unification
(December 3 + 8, 2015)
- 5.2 Local Confluence and
Critical Pairs
(December 8 + 10, 2015)
- 5.3 Confluence Without
Termination
(December 10 + 15, 2015)
- 6.1 The Basic Completion
Algorithm
(December 15 + 17, 2015)
- 6.2 An Improved Completion
Algorithm
(December 17, 2015 + January 12, 2016)
- 6.3a Implicit Induction (Part 1)
(January 14, 2016)
- 6.3b Implicit Induction (Part 2)
(January 19, 2016)
There will be a written exam on
the lecture. It takes place on
February 22, 2016.
Here you find two exams from the 2004, 2006/2007, and 2011 lectures on
term rewrite systems (in German). However, as the computer science
curriculum has been changed since these exams took place, the
conditions for these exams were different from the ones for the
exam we will have in this lecture. First, the exams in 2004 and 2006/2007 were not
designed to determine the final grade for the term rewrite systems
course, but only for the acquisition of the Übungsschein.
Second, they only took 90 minutes, while our exam will take 120 minutes.
The exam in 2011 did not cover the full content of the lecture (e.g., implicit induction
was missing from this exam), whereas in 2016
the written exam will cover the full content of the lecture.
Keep these differences in mind when practicing with the old exams.
Furthermore, we strongly recommend that you solve the old exams
without looking into the solutions first and that you also respect
the time limit of 90 minutes for the exams from 2004 and 2006/2007.
