This looks pretty cool. I don't know much about term rewriting, but I get the impression that it provides a unified way of implementing some neat features such as pattern-matching on arbitrary expressions, macros, and other symbolic stuff.
It's not the same thing, in the same sense that "Lazy Evaluation" is not the same thing as "Non-strict Semantics", but "Term Re-Writing" is closely allied with "Graph Reduction. Simon Peyton-Jones' books "The Implementation of Functional Programming Languages" and "Implementing Functional Languages: a tutorial" are excellent works. Now out of print, they can both be found on-line.
It sounds like you certainly know more about term rewriting than I do. Do you know of a decent introductory source? I'd like to get a gist of it, but the Pure site seems to prefer reference/appendix style documentation. That stuff is great to have, but I'm looking for an litmus test for my interests.
"Term rewriting and all that". It's not easy going, however; make sure your category theory and universal algebra are top-notch before touching the burgundy book.
The Maude project [1] (and its documentation) may be of interest; they use term rewriting in a formal modeling and model-checking tool. There's an introductory course at [2].
I can't add much to what others have already recommended, other than Functional Programming by Field and Harrison (out of print, I believe). It covers graph reduction, which I believe is a generalization of term rewriting.
