The book Term Rewriting and All That by Baader and Nipkow includes a lot of code in ML, I highly recommend it.

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.

Thank you for the recommendation.

How these systems relate to graph reduction: graph reduction is one way to implement term rewriting.

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

Thank you.