Term Rewriting

July 10, 2016

Term rewriting is a declarative computational model in which subterms of a compound term are progressively replaced with other subterms, until the term reaches a normal form—or, in a Turing-complete rewrite engine, perhaps until the universe ends. This is quite similar to how humans do algebra, and is sometimes used as a pedagogical device for teaching functional programming; for example, the "substitution model" employed in the first chapter of SICP is an intuitive rewrite system.

In rewrite systems, program state is generally an object of some kind that then gets transformed during each step of computation into another object — for instance, in a rewrite system with arithmetic, one step might transform the expression 32 + 10 into the expression 42. Many rewrite systems can perform symbolic rewriting, where an expression like 2 * x could be rewritten to x + x even if the value of x isn't bound. Unfortunately, that latter characteristic has the potential to obscure certain programming errors, because a mistyped variable name becomes indistinguishable from a symbolic rewriting expression. In a rewriting-based language, an expression like 2 + "horse" isn't necessarily a type error, but just a normal form — no rewrite rules match an abominable expression like that, so no further rewriting is done. Thus, some logical errors in rewrite systems don't produce error messages, but half-reduced programs.

Nevertheless, there are many interesting things that can be done with rewrite systems. In particular, I like their implications for how programming language tooling can fit into a coherent story with the language itself. Macro expanders, stepping debuggers, data visualizers, partial evaluators, even compiler frontends cease to be magical extralinguistic devices, and become programs explainable in the language's own terms. It also seems to me that term rewriting forms a logical continuation of the classic Lisp "code is data" dictum: "Code is data … and it remains data at runtime".

Some general-purpose term rewriting languages include Pure and Aardappel. I think Mathematica / the Wolfram Language is also based on term rewriting, but I have no actual experience with it — it's proprietary, quite expensive, and I'd prefer not to give any money or attention to Stephen Wolfram if I can avoid it.



Academic References

Powered by Plutonium