Proving non-confluency and adding an equation to make it confluent and terminating

Question

I currently have a system that has {f(a) = b, f(f(x)) = x} (part of an exam question - look at page 5 - exercise 1).

To start off with proving non-confluency, I am thinking along these lines:

f(f(x)) and f(a) can be unified by using {a -> f(x)}. 

Then we can rewrite:

f(f(x)) = x                 [eq.1]
f(f(x)) = b                 [eq.2]

The above two cannot be reduced any further, and do not have any common ancestor or successor. Therefore the system is not confluent.

To make this confluent, we can add a third equation to the system:

x = b

This way, the equation will both be confluent and terminate. Another alternative would be:

f(x) = b

Is there anything I have missed? Or is this pretty much the gist of it?

Answer 1

I do not think $f(f(x))$ and $f(a)$ can be unified. You can not map constant $a$ to the term $f(x)$.

My example would be $f(f(a)) = f(b)$ while otherwise $f(f(a)) = a$.

It seems the equation $x=b$ maps all terms to $b$. That is too much. I would add $f(b) = a$. This leaves two classes of terms, those equivalent to $a = f(b) = f(f(a)) = \dots$ and those equivalent to $b = f(a) = f(f(b)) = \dots$

Here, $a=a$ and $b=b$ and never the twain shall meet ...

Answer 2

The notion you are looking for is that of critical pair (see the wikipedia entry for instance). The idea is to find the "most simple" term which allows both rewrite rules to be applied. In this case the rewrite rules are:

$$ f(f(x))\rightarrow x$$ $$ f(a) \rightarrow b$$

To find a critical pair, you look for the most general (in a precise sense) instance of the variables on the left-hand side which allow one term to be the (non-trivial) subterm of another. In this case, we can instantiate $x$ to $a$ and obtain

$$ a\leftarrow f(f(a)) \rightarrow f(b)$$

This is a most general instantiation: we can't apply both rules if $x$ isn't sent to $a$. The equations you gave imply $a = f(b)$. To obtain a confluent rewrite system, we therefore need to add one of two rules:

$$ a \rightarrow f(b)$$ or $$ f(b)\rightarrow a $$

Note that either rule will not make more terms equal, as the equality already holds! We can choose either rule to add to our system, but it is tempting to add the second one, as it seems more "computational". Now you have made your critical pair harmless: $f(f(a))$ rewrites to $a$ regardless of our choice of rule applications.

But we are not done! We have a new critical pair:

$$ b\leftarrow f(f(b))\rightarrow f(a)$$

However that critical pair is harmless, as both sides reduce to $b$.

Now every critical pair is harmless, and so we have verified the property of local confluence. This by itself is not enough to have confluence! However in your case, you have the additional property of termination: no term has an infinite rewrite sequence. This, in combination with local confluence, implies confluence, thanks to Newman's lemma.

Note that this whole approach (find critical pairs, add rewrite rules, check for termination, repeat) can be made systematic, to attempt turning any rewrite system into a terminating one; it is often called Knuth-Bendix completion.