Term rewriting

Kragen Javier Sitaker, 2017-07-19 (3 minutes)

Typical term-rewriting patterns are of the form

x(?y, z) -> foo(?y, ?y)

where the “?” identifies the y as a variable (or, we might say, a metavariable). This poses a certain amount of difficulty for metacircularity, such as a program to determine whether a set of rewrite rules is confluent (normalizing); you might want to look for the literal pattern ?y or especially ??y for any ?y in some rewrite rule you are trying to manipulate.

Prolog, where all this originally came from, is even trickier along this axis, since it spells foo and ?foo as foo and Foo, respectively.

One possible solution to this problem is to declare the metavariables out-of-line:

(rewrite (y) (x y z) (foo y y))

or

metavariable y;
x(y, z) -> foo(y, y)

Another aspect of term-rewriting languages is that they don’t accommodate extensible data structures very easily. Suppose you have a bunch of rules of the following form:

?x + constant(0) -> ?x

Now, you decide that constants should additionally include the line and column number where they were found, thus improving your debugging information. This forces you to modify the above rule as follows:

?x + constant(0, ?_) -> ?x

And you must do the same thing for all similar rules.

Suppose instead that the nodes of your graph instead have arbitrary sets of named properties, perhaps namespaced to avoid unfortunate property collisions, and with the proviso that extra properties not mentioned never cause a match failure. Then we can write the above instead as follows:

{addend1: ?x, addend2: {constant_value: 0}} -> ?x

This version will survive such an augmentation without modification.


This is the same data model as Binate, and suggests that you should be able to write such rewrite systems as Binate relations, making them point-free (and solving the above problem of metacircularity in a different way): the transitive closure of some rewrite relation, perhaps. That is, the above algebraic rewrite rule would be part of a relation called something like algebraically_simplifies_to, so we could ask whether

(4 + 0) algebraically_simplifies_to 4.

or indeed what a given expression simplifies to. The algebraically_simplifies_to arc or arcs from that expression would be in some sense on equal standing with the addend1 node from it to 4. We can take the transitive closure of that relation and subtract a version of its own converse from it to exclude results that can be algebraically simplified further.

I am not sure if this is in practice a feasible thing to do with Binate, or what would be needed to make it feasible, or whether it would be practical, but it is a very appealing simplification and unification!

It also avoids the ugly ad-hoc extension to term-rewriting pattern-matching in Leler’s Bertrand (p.53 of his book) where aNumber matches any number, etc.

I think one big problem here is that in Binate, equality is (I think) necessarily defined by identity rather than content: two point objects with the same x and y properties are not equal, because one of them might have some other property (such as z) which is not supposed to affect the behavior of queries that don’t mention that property.

Topics