Term Rewriting Systems are widely used throughout computer science as they provide an abstract model of computation while retaining a relatively simple and concrete syntax. However, some problems require a semantics to abstract away from this concrete syntax and expose more fundamental, underlying structure. Abstract Reduction Systems provide a relational semantics for TRSs but unfortunately these relations do not possess enough structure to adequately model key rewriting concepts such as substitution, context, layer structure etc. Hence this relational model is used mainly as an organisational tool with the difficult results proved directly at the syntactic level.Category Theory can be used to provide a semantics for rewriting at an intermediate level of abstraction between the syntax and the relational model. Very recently several advances in categorical rewriting have been made in which category theory leads to new insights into rewriting, see for instance: Ghani's Adjoint Rewriting, Masahito Hasegawa's categorical semantics for cyclic graph rewriting, Lüth's categorical proof of Toyama's theorem and Melliès' Axiomatic Rewriting. (See the pointers to literature below.) We believe that the present state of the art is promising enough to warrant its presentation to the wider term rewriting community.
The workshop consists of tutorials only and is intended to provide the participants of RTA'98 with an opportunity to learn more about categorical term rewriting. In order to attract as wide as possible an audience, we shall minimise the categorical jargon and concentrate instead on the underlying principles of the subject.
Programme (13.45 - 18.00)
13.45: An Introduction to Category Theory in Rewriting (slides) Fer-Jan de Vries 14.30: TRSs as Algebraic Structures (slides) Neil Ghani 15.15: A Monadic Proof of Toyama's Theorem (slides) Christoph Lüth 16.00: break 16.30: Models of Cyclic Structures: Knots, Term Graphs, and Recursion Masahito Hasegawa 17.15: Adjoint Rewriting (slides) Neil Ghani 18.00: end The workshop took place on March 31st, 1998 on the RTA'98 conference site at Tsukuba University.
Some pointers to recent literature
- Neil Ghani. Adjoint Rewriting. Ph.D. Thesis, University of Edinburgh. Published as CST-122-95 and ECS-LFCS-95-339, 1995.
- Masahito Hasegawa. Recursion from cyclic sharing: traced monoidal categories and models of cyclic lambda calculi. In Proc. TLCA'97, LNCS 1210, pages 196--213, 1997. Springer Verlag.
- Christoph Lüth. Compositional Term Rewriting: An Algebraic Proof of Toyama's Theorem. In Proc. RTA'96 , LNCS 1103, pages 261--275, 1996. Springer Verlag.
- Neil Ghani and Christoph Lüth. Monads and Modular Term Rewriting. In Proc. CTCS'97, LNCS 1290, pages 49--68, 1997. Springer Verlag.
- Paul-André Melliès A Factorisation Theorem in Rewriting Theory. In Proc. CTCS'97, LNCS 1290, pages 49--68, 1997. Springer Verlag.