How these systems relate to graph reduction: graph reduction is one way to implement term rewriting. Laziness is an orthogonal issue related to your operationa

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