I wrote a simple TRS that I believe is non-confluent, but I'm not able to find a term with two normal forms for it.

The TRS is defined on the signature $\mathcal F=\{f,\ l,\ s,\ o\}$ and the rewrite rules $\mathcal R$ are defined as follows:

  • $l\to s(o)$
  • $t(x,\ l)\to s(x)$
  • $t(l,\ x)\to s(x)$.

This TRS is clearly finite and terminating.

For the first two rules, we have a critical pair $(t(x,\ s(o)),\ s(x))$ which is not joinable. Therefore, the TRS is not confluent.

It seems that for such a simple example I should be able to find a term with two normal forms. What am I missing?

  • 1
    $\begingroup$ Stating that the critical pair is not joinable means that the original term $t(x,l)$ can reduce along two non-joinable paths. Since the system is normalizing, both paths must end in a normal form. As it were, the two terms you have here are both normal forms for $t(x,l)$. I don't get what you're missing... $\endgroup$ – Gilles 'SO- stop being evil' Mar 27 '15 at 8:45
  • $\begingroup$ Your rewrite system is not confluent (as you have shown) but perhaps what you want to show is that it is not confluent when restricted to ground terms (i.e., terms with no variables). This property, called ground-confluence, is different from confluence (actually, it is a bit weaker). Can you confirm this is indeed your question? $\endgroup$ – phs Mar 27 '15 at 10:27
  • $\begingroup$ I indeed had the two terms that are different normal forms of a given term in front of me. I didn't have a good enough understanding of what the meaning of a critical pair is. Thank you for clarifying that. $\endgroup$ – amaurremi Mar 28 '15 at 0:43

$t(o,l)$ has two normal forms: $t(o,l)\to s(o)$ and $t(o,l)\to t(o,s(o))$.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.