Name: Term rewriting and all that
ISBN: 9780521455206

What Hacker News says

dtornabeneNov 2020

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, for analysis of program state

thread

triskaDec 2019

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.

thread

zmonxAug 2017

In the terminology (may I say: terms) of term rewriting, you are looking for a so-called completion procedure. This takes a set of axioms and turns it into a convergent term rewriting system (or not, because it may not terminate!).

If the completion procedure succeeds, you end up with rules that always terminate, and which reduce any given term to its normal form. In the literature, search for Knuth-Bendix and Huet completion procedure, if you are interested. For SQL, it may get quite 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.

thread

groovy2shoesJul 2016

Language Implementation Patterns by Terrance Parr might be right up your alley. Implementing Programming Languages by Aarne Ranta is likewise a refreshing take on language implementation instruction. Bonus points for both books being rather concise and affordable.

I've also really enjoyed Elements of Programming Languages by Friedman & Wand (older editions cover different topics than the current 3rd edition, and it may be worth reading both the 1st and 3rd editions). Focuses primarily on interpreters, but most of the topics covered have applications for compilers as well.

Going a slightly more traditional route, I've found Andrew Appel's compiler books, Modern Compiler Implementation in ML and Compiling with Continuations to present pretty wide coverage of techniques at all phases of a compiler. The former is the one I normally recommend for people looking for their first (and hopefully only) compiler book (if they're actually looking for a compiler book rather than a DSL book).

Of course, techniques for processing the Lisp family are well-covered in Christian Quiennec's classic Lisp in Small Pieces (he's written some other books which are quite interesting for Lisp historians as well). Implementors of Lisps will also probably want to look into The Art of the Metaobject Protocol by Kiczales et al. SICP's coverage in chapters 4 and 5 is also pretty good as an introduction, even if it only barely scratches the surface.

Getting into types, you're pretty much limited to Pierce's Types and Programming Languages, but Bob Harper et al. have also written Homotopy Type Theory 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 written in English is pretty small (I've literally found only three, one of which costs $300 USD(!) -- where does Cambridge University Press get off??), but fortunately the Baader and Nipkow book is so good that you probably won't need another book and can proceed straight to the literature.

---

There are tons of books on compilation, but I honestly think they're mostly a waste of time. Each book, for the most part, only re-iterates the basics in another way, so unless you didn't quite grasp it from the first book you tried, maybe look at another one, but once you understand the material, don't waste any more time or money on compiler books. After you've grokked the basics (i.e., worked through one or two introductory books), you'll get far more value from reading books on other related concepts (e.g., type theory, term rewriting, metaobject protocols, etc.), reading research papers, journal articles, dissertations, etc., and, of course, reading code.

I say all this as someone who made the mistake of spending lots of time and money on lots of different compiler books, stupidly hoping to learn something new with each one. The silver lining is that this puts me in a pretty good position to recommend particular compiler books :)

That the Dragon Book is still considered the standard introduction is baffling, even the most recent edition is horrendously outdated and dwells far too much on parsing techniques (where, from the perspective of a compiler writer, parsing is effectively a solved problem -- not to mention that there are quite a few parsing techniques the Dragon Book doesn't cover, despite the amount of text devoted to parsing). And, like you said, the techniques it covers are really only immediately applicable to imperative procedural languages without sophisticated type systems, such as C or Pascal.

thread

practalFeb 2025

Fair enough. My personal motivation is abstraction logic (AL), and one way of viewing it is as a generalisation of equational reasoning. I am just starting to implement rewriting for AL, but I will definitely drop you a line once you can play around with it. Maybe AL can be your common format, instead of just a 15th engine for it :-) There are two reasons why I think that:

1. AL is more general than first-order rewriting, because it has general binders, that is general variable binding constructs.

2. Unlike higher-order logic, which also has general binders, it doesn't have types, so rewrite rules in AL can be taken for face value, and have no hidden type annotations in them, just like in first-order rewriting (that is a consequence of AL having a single mathematical universe).

I must admit, I am quite excited about implementing rewriting for AL! My PhD father has co-authored a book about (mostly) first-order term rewriting [1]. Higher-order 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

thread

peterfireflyAug 2014

Glynn Winskel, "The Formal Semantics of Programming Languages", 1993 -- a bit dated but still quite good. Covers basic semantics/type theory.

Benjamin Pierce, "Types and Programming Languages", 2002 -- y'know, just your basic type theory.

Benjamin Pierce, "Advanced Topics in Types and Programming Languages", 2005 -- Chapter 10 is a juicy 128 pages on Hindley-Milner type inference. Good for both theory and implementation tricks. It looks at HM typing as a constraint system where the rules are Just Right so that if you get a solution you get a solution that is "maximally nice". It describes variants that are perhaps not quite as beautiful but which in some ways are "better" (= can statically check more of your code or where the programmer can express him or herself freer).

If you want to know more about unification, which is how HM type inference and checking is usually/originally stated:

Franz Baader and Wayne Snyder, "Handbook of Automated Reasoning", 2001 -- chapter 8 is called 'Unification theory'.

Peter Norvig, "Correcting 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.

thread