Term rewriting and all that
by Franz Baader · first published 1998
8mentions
4recommended by
7HN commenters
2009–2025first – last mentioned
57% recommend29% neutral14% critical
Affiliate links. As an Amazon Associate I earn from qualifying purchases.
…complex, but still doable, potentially with some extensions of the primary method. There are all kinds of variations on the general scheme. If you are interested in term rewriting, a solid starting point is Term rewriting and all that by Baader and Nipkow.
on “Recognizing when two arithmetic expressions are essentially the same” ↗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…
on “Ask HN: Design and Implementation of Term Rewriting Systems” ↗…which is freely available on the Web. I haven't finished HoTT yet, so I can't comment on how accessible it is or how broad/deep its coverage is. Those interested in rewriting systems should start with Term Rewriting and All That by Baader and Nipkow, which I've found to be extremely accessible and fairly comprehensive (covering abstract rewriting systems, string rewriting, graph rewriting, etc.). Your choices for books on rewriting…
on “Resources for Amateur Compiler Writers” ↗A good book on Term Re-Writing is "Term Rewriting and All That". It uses Standard ML for implementation of the algorithms, just an excellent text overall. Also, there's a component of BAP, the Binary Analysis Platform, that uses term rewriting situated in lisp,…
on “Exotic Programming Ideas, Part 2: Term Rewriting” ↗…A[sic] Widespread Error in Unification Algorithms", 1991 -- many published algorithms were subtly wrong. Unification is really an example of a term rewriting system: Franz Baader and Tobias Nipkow, "Term Rewriting and All That", 1998. It is amazing how much there is to say about a 10-line algorithm (Algorithm W) / such a short set of typing rules / such a small constraint system as the HM type system.
on “Safely Composable Type-Specific Languages [pdf]” ↗…macros. Lisp macros are not generic "macros", unless you're in the company of Lispers, but lisp macros :-P If you want to explore the highest level of code transformation, grab a nice little book called "Term-Rewriting and all That". P.S. It's actually not a nice book. It's a theoretical mindfuck that will have you chasing abstract algebra down rabbit holes. It took a good year of my life and I still have no clue. </confession>
on “Ask HN: Are macros still an enormous edge in the power of a language?” ↗"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.
on “The Pure programming language” ↗…rewriting based on the lambda calculus is mentioned briefly in it (and of course implemented in Isabelle), and I am wondering if rewriting based on AL instead will bring new insights and/or techniques. [1] Term Rewriting and All That. https://doi.org/10.1017/CBO9781139172752
on “Where are all the rewrite rules?” ↗