I’m looking for resources on the design and implementation of Term Rewriting Systems. I’m particularly interested in systems for use in discrete math and computer algebra systems, but any resource is welcome.
Also, how do these systems relate to graph reduction in lazy functional languages?
Thank you!
The code is available online:
https://www21.in.tum.de/~nipkow/TRaAT/
The book also contains many useful references, which I also recommend to check out for your other questions.
Also, in my experience, logic programming languages like Prolog are especially useful for reasoning about term rewriting systems, because they provide built-in features such as unification, subsumption checks and implicit search and backtracking which are very useful when working with and reasoning about term rewriting systems.
Laziness is an orthogonal issue related to your operational semantics.
The designs of TRS implementations are mainly to address an issue - your reduction rules as written are not ordered. In implementing them you need to impose an order. This is not so desirable, so parallel reduction may be required, but that introduces a whole new bunch of issues.
Baader and Nipkow is pretty good, but I would also highly suggest writing a lambda calculus in an imperative programming language to get a feel for the operational semantics