Sorry for the long hiatus: the end of the semester was first a blaze of emails and wrapping up classes, and then quiescence for a little R&R. I’ve also been dragging my feet on posting about relative termination, which is what I’ve been planning to write about for a while. Maybe I should explain why.
Relative termination is an intriguing generalization of termination, explored mostly (as far as I know) in the context of term rewriting. A good source for the concept is Alfons Geser’s dissertation (cached here). The basic definition Geser attributes to Klop. Suppose R and S are binary relations. Then R is called terminating relative to S iff every time we have a sequence of terms with , there is no infinite subsequence where we have . That means that every path in the graph of has only finitely many -edges.
This is pretty abstract, and perhaps seems unmotivated. Reading Chapter 2 of Geser’s thesis, part of the historic motivation seems to have been the older concept of “termination modulo” (which I did not know about before reading that chapter), where we are interested in termination modulo a (non-terminating) equational theory. To explain this, I’ll give a simple example, modified slightly from one in Geser’s thesis. For this, we just need the standard idea of the rewrite relation induced by a set of rewrite rules . The rewrite relation is what you get when you close the rules under substitution (of terms for variables) and embedding rewrites steps in bigger terms (also called “closure under contexts”). It is customary to speak of terminating to mean that is terminating (and similarly for “relatively terminating”). So now the example is this. Suppose , and . Obviously is not terminating, since we have . But is terminating. The proof of this can be done by assigning a natural-number measure to terms: is just the sum of the depths of occurrences of in the term . So for example, (adding up the depths of the three occurrences of , from left to right in the term). This measure is decreased by every application of the sole rule in . The rewrite system is not terminating, since it includes non-terminating . But — and this is the interesting part — is terminating relative to . Any sequence of rewrite steps using rules from either or can only have finitely many -steps. I’ll prove this below, but intuitively, once we have pulled all the occurrences of out of the left and right hand sides of occurrences of , then all we can do is swap the arguments of -terms back and forth forever. So there is only a finite amount of -work (so to speak) to be done for any term. After that, we can only take -steps.
Let me tell you why I’m interested in relative termination, and why I’ve been hesitant to try to write about it. Relative termination turns out to be an incredibly powerful idea for term rewriting. One of the central modern techniques for proving termination of term rewriting systems, the so-called dependency pairs method (see the seminal paper Termination of Term Rewriting Using Dependency Pairs, by Aarts and Giesl), can be viewed as based on relative termination. The connection — apparently not drawn at first by the authors of the method — is made in Matrix Interpretations for Proving Termination of Term Rewriting, by Endrullis, Waldmann, and Zantema (I am guessing the connection was made earlier than that paper, but I don’t know the first reference). For another connection, a paper which will definitely be one of my two favorite papers of 2010, Decreasing Diagrams and Relative Termination, by Hirokawa and Middeldorp, is (as the title suggests) based on relative termination. I hope to post about that paper later.
So that’s why I’ve been interested to learn more about relative termination. But the concept is a bit unintuitive, and the treatment in some of the papers I’ve looked at does not improve the situation. Chapter 2 of Geser’s thesis definitely helped, though.
Anyhow, I’ll write more about relative termination in some subsequent posts, but to wrap up this one: let’s see how to do the proof for the above example. The basic sufficient condition, given in Section 2.4 of Geser’s thesis (page 24) is that for binary relations and , is terminating relative to if there is a terminating quasi-order such that (where is the strict part of ) and . A quasi-order is just a reflexive and transitive relation, and a terminating one is one whose strict part is a terminating relation. For the example above, we can prove terminating relative to using the ordering that makes iff , where is the measure given above (the sum of the depths of the occurrences of in the term). The value of the measure is decreased by and unchanged by , so the requirements of the sufficient condition are met. More sophisticated versions of this kind of reasoning are developed in the literature, for example in the Endrullis et al. paper cited above.