2
$\begingroup$

Consider a term rewriting system $\mathcal{R} = (\Sigma, R)$ over a signature $\Sigma$ with basic rewrite rules $R$. If $\mathcal{R}$ is weakly normalizing and confluent, then we know that each $\Sigma$-term has a unique normal form (with respect to $\mathcal{R}$). Is the converse also true? I.e. if each term has a unique normal form with respect to $\mathcal{R}$, then does it follow that $\mathcal{R}$ is weakly normalizing and confluent? Obviously if each term has a unique normal form, then the system is weakly normalizing, so it remains to ask whether it will be confluent.

In short, I am wondering whether the property of a term rewriting system to be weakly normalizing and confluent is strictly stronger than the property of each term having a unique normal form (with respect to the system).

$\endgroup$
  • 2
    $\begingroup$ This question is not reaearch level and would have been more suitable for CS.SE. Anyway, beware that the standard definition of unique normal form property (commonly abbreviated UN) does not include existence, i.e., UN = "if two normal forms are related by rewriting (in any direction), then they are equal". This is implied, but does not imply CR. What you call "having a unique normal form" is UN+WN, which obviously implies CR. $\endgroup$ – Damiano Mazza Jun 18 '18 at 7:09
4
$\begingroup$

It is a little bit sketchy, but here is my argument: Suppose that there are three terms t, u, v such that t reduces to u, t reduces to v and suppose that each term has a unique normal form. Since you are weakly normalizing as you said, there exists a normal form for v and u. But since the normal form is unique, then v and u are joinable. Hence, the system is confluent.

$\endgroup$
  • $\begingroup$ So the argument at the end of your answer is that if $v$ and $u$ were NOT joinable, then $t$ would have two distinct normal forms, contradicting the assumption that $t$ has a unique normal form? Am I understanding correctly? $\endgroup$ – User7819 Jun 18 '18 at 1:00
  • 1
    $\begingroup$ Yes, that is exactly my argument. $\endgroup$ – Saroupille Jun 18 '18 at 7:31

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.