Computer Science Seminar (Department of Computer Science, Gunma University)


Thursday 17 of April (Library 2F:図書館館長室)
Confluence of Normal Abstract Rewriting Systems,
Jean-Pierre Jouannaud
(University Paris-Sud 名誉教授, Ecole Polytechnique 教授, 清華大学教授)

Normal Abstract Rewriting Systems is a very general rewriting framework
which captures all existing rewriting frameworks for which (uniform)
termination is assumed. In particular, plain rewriting (Knuth and
Bendix), rewriting modulo associativity and commutativity (Peterson and
Stikel), modulo theories which equivalence classes are finite (Jouannaud
and Kirchner),
modulo associativity, commutativity, identity and idempotency (Jouannaud
and Marche), higher-order rewriting at simple types modulo beta/eta
(Nipkow, implemented in the proof-assistant HOL-Isabelle), higher-order
rewriting at arbitrary types (application of NARSes).
We will first give many examples of such rewrite systems, then state and
describe the main ingredients of the abstract confluence theorem and its
applications in the above particular cases.