I'm a bit tripped up by this fundamental notion of an equational theory with respect to how we can possibly get termination if we have that we can always orient a set of equations either right to left or left to right. For example, consider the set of equations just being $E=\{1+x=x\}$. For signature $\Sigma$ we consider the equational theory $(\Sigma, E)$ as equivalently the term rewrite system $(\Sigma, E' \cup E'')$ where $E' = \{t \rightarrow t'\ |\ t = t' \in E\}$, and $E'' = \{t' \rightarrow t\ |\ t = t' \in E\}$ (source, which I may be misunderstanding; attached below). Hence, we have the set of rewrite rules in this equational theory from my understanding being $\{1+x\rightarrow x,\ x \rightarrow 1+x\}$. Hence, if we were to try and rewrite $1+x$, we would run into the issue of looping:

$$1+x \rightarrow x \rightarrow 1+x \rightarrow x \rightarrow 1+x \rightarrow\ ...$$

Hence I don't see how it would be possible to have in an equational theory any termination due to this—it's not possible to have a well-founded reduction ordering from what I can tell when equations are oriented in both directions.

I was reading about Knuth-Benedix completion algorithm and that seems to be on the right track of what I was thinking, but I'm still somewhat confused on how we can consider sets of equations oriented in both directions as a TRS without running into the above aforementioned problem.

Here is the source I mentioned above:

facsimile of part of a book

  • $\begingroup$ Where in the text you showed us is there any talk of "termination"? And what does it even mean for a theory to terminating? A rewrite system may be terminating, but the quoted text does not speak about termination, nor is termination of the rewrite system it considers of any concern in that passage. There will of course be other texts (probably in the same book) which do deal with termination. $\endgroup$ Mar 29, 2020 at 23:05
  • $\begingroup$ @AndrejBauer thanks for bringing that up—here is a portion which explains where it talks about a terminating equational theory. But it seems that we only define termination for a rewrite theory (source in the same text), not an equational theory. So what I'm wondering is if we're considering a given equational theory as a rewrite theory, then wouldn't we have the equations oriented both left and right based on the cited photo in my question (since we can rewrite in both directions), and hence it would never be terminating? $\endgroup$
    – rb612
    Mar 29, 2020 at 23:44
  • $\begingroup$ I'm starting to gather from the above links and this that maybe we are referring to the oriented equations left-to-right being terminating, but that motivates my question, confirming it indeed wouldn't be possible for applying equations bidirectionally to be terminating since $a = b \Leftrightarrow a \rightarrow b \wedge b \rightarrow a$ means we could have $a \rightarrow b \rightarrow a \rightarrow b ...$. $\endgroup$
    – rb612
    Mar 30, 2020 at 0:11
  • 1
    $\begingroup$ Yes, of course, if you convert $a = b$ to two rewrite rules $a \to b$ and $b \to a$ you obviously get a non-terminating system. And I don't think anyone ever suggested you wouldn't. The point is that an equational theory $E$ sometimes may be equivalent to a terminating rewrite system $R$ in the sense that $E$ proves $a = b$ if and only if $R : a \to c$ and $R b \to c$. One way of getting such an $R$ from $E$ is to orient equations of $E$ (so you take only one of the two possible options). $\endgroup$ Apr 1, 2020 at 11:26


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.