Congruence of terms

There is concept of Term Rewriting. If one have rules for rewriting terms, one can obtain some term from another. For example, rule1: a -> f(b); rule2: b->t. Term A(f(t)) can be obtained from term A(a) by rule1 and rule2. Terms A(f(t)) and A(a) are congruent terms.

Are there algorithms, which can answer is some term T1 can be obtained from some term T2, by some rules. In other words, whether the two terms are congruent?

I’m also interested in terms with variables.

Solutions Collecting From Web of "Congruence of terms"

If your term rewrite rules are sufficiently flexible, then the answer is that this problem is undecidable. The reason is that one can reduce the halting problem for Turing machines to the question of whether a certain term generates another with respect to a certain system.

The idea of the proof is to use terms to represent the configuration of a Turing machine computation. For example, the term $a(b(H_s(c(b(a(.))))))$ would represent the Turing machine having tape $abcba$, with the head on the “c” in state $s$. Now, you write down term rewrite rules that correspond to the steps of computation, so that $b(H_s(c(t)))\to H_u(b(a(t))$ would be a rule, where $t$ is a wildcard for any further subterm, if the Turing machine was supposed to move left when reading symbol $c$ in state $s$, writing $a$ over the $c$ and changing to state $u$. If you also add rules that if a halt state is achieved, then the terms begin to absorb their arguments and containing terms into a constant “halt” term. Thus, the system has the property that the given Turing machine halts if and only if we can generate this “halt” term from the term corresponding to the initial configuration of the machine. Since we cannot decide the halting problem, it now follows that we cannot decide the generation problem for this term rewrite system.

Notice that the type of rules I used in this argument are somewhat more complicated than the example rules in your question. For example, in the Turing machine computation step, we have preserved the (unknown) subterm $t$. So this argument applies only to systems in which such rules are allowed.

This kind of rewrite system is somewhat easier to think about in terms of strings, with rewrite rules about substrings, and this is known as a semi-Thue system. I also wrote this MathOverflow answer on the same topic, showing that the special case where the terms on each side of the rewrite rules have the same length is decidable, but NP-hard.

Lastly, I would like to object to the “congruent” terminology, since I find that word to suggest a symmetric relation, but the term-rewrite-generation relation is not generally symmetric, unless you allow the rules to be applied backwards.

I am not sure what the $f$ and $A$ are in your “example”, but I think that this page should be of interested:

I’m not sure what you’re trying to ask.

The general strategy, as your book probably points out, is to apply the given term rewriting system to each of the two terms. If the rewriting ends such that the results are the same, then the terms are equivalent, or “congruent” in your usage.

  1. If you mean to ask: “Are there programs which can rewrite terms given a set of rewrite rules?”, then yes, there are plenty of them: Mathematica, Prolog, and Pure can all do this, more or less; there are probably many others.

  2. If you mean to ask: “Can the congruence of two arbitrary terms in an arbitrary sytem always be decided?”, then no, as JDH has explained very well in his reply.

  3. If you mean to ask: “How does one create a rewrite system from a set of equations?”, then your book will probably explain the various conditions, limitations, and techniques that apply. Very briefly, the rewrite system has to be terminating and confluent to guarantee the ability to decide equality of terms. This Wikipedia article gives a quick overview; I also seem to recall that the Handbook of Theoretical Computer Science also has a very decent, amazingly readable chapter on the subject of term rewriting.