Skip navigation

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 t_1, t_2, \ldots with t_1\ (R \cup S)\ t_2\ (R \cup S)\ \ldots, there is no infinite subsequence s_1, s_2,\ldots where we have s_1\ R\ s_2\ R\ \ldots.  That means that every path in the graph of R\cup S has only finitely many R-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 \rightarrow_R induced by a set of rewrite rules R.  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 R terminating to mean that \rightarrow_R is terminating (and similarly for “relatively terminating”).  So now the example is this.  Suppose R = \{ s(x)+y \rightarrow s(x+y) \}, and S = \{ x+y \rightarrow y + x \}.  Obviously S is not terminating, since we have x+y \rightarrow y+x \rightarrow x+y \rightarrow \ldots.  But R is terminating.  The proof of this can be done by assigning a natural-number measure m(t) to terms: m(t) is just the sum of the depths of occurrences of s in the term t.  So for example, m((s(x)+y)+s(s(z))) = 2+1+2 = 5 (adding up the depths of the three occurrences of s, from left to right in the term). This measure m is decreased by every application of the sole rule in R.  The rewrite system R\cup S is not terminating, since it includes non-terminating S.  But — and this is the interesting part — R is terminating relative to S.  Any sequence of rewrite steps using rules from either R or S can only have finitely many R-steps.  I’ll prove this below, but intuitively, once we have pulled all the occurrences of s 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 R-work (so to speak) to be done for any term.  After that, we can only take S-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 R and S, R is terminating relative to S if there is a terminating quasi-order \ge such that R \subset > (where > is the strict part of \le) and R \subset \ge.  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 \rightarrow_R terminating relative to \rightarrow_S using the ordering that makes t \ge t' iff m(t) \ge m(t'), where m is the measure given above (the sum of the depths of the occurrences of s in the term).  The value of the measure is decreased by R and unchanged by S, 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.

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: