2
$\begingroup$

I am looking for a name for the property $\mathbf{?_2}$ (and for that, it is sufficient to find a name for the property $\mathbf{?_1}$ since "Uniform" could then be added in front of it).


Confluence : If $t_1\leftarrow^* t \rightarrow ^* t_2$, then one of the following is true:

  • There is $t'$ such that $t_1\rightarrow^* t' \leftarrow^* t_2$.

Uniform confluence : If $t_1\leftarrow t \rightarrow t_2$, then one of the following is true:

  • There is $t'$ such that $t_1\rightarrow t' \leftarrow t_2$;
  • $t_1=t_2$.

$\mathbf{?_1}$ : If $t_1\leftarrow^* t \rightarrow^* t_2$, then one of the following is true:

  • There is $t'$ such that $t_1\rightarrow^* t' \leftarrow^* t_2$;
  • Both $t_1$ and $t_2$ are strongly normalising.

$\mathbf{?_2}$ : If $t_1\leftarrow t \rightarrow t_2$, then one of the following is true:

  • There is $t'$ such that $t_1\rightarrow t' \leftarrow t_2$;
  • $t_1=t_2$;
  • Both $t_1$ and $t_2$ are normal forms.

One way this property arises, is if you have two rewriting systems $S_1=(X_1,\rightarrow_1)$ and $S_2=(X_2,\rightarrow_2)$ and then look at $S=(X_1\times X_2, \rightarrow)$ where $(x_1,x_2)\rightarrow (x_1',x_2')$ iff $x_1\rightarrow_1 x_1'$ and $x_2\rightarrow_2 x_2'$ (i.e. you reduce in parallel in both components). Then if both $S_1$ and $S_2$ are confluent (resp. uniformly confluent), $S$ is $\mathbf{?_1}$ (resp. $\mathbf{?_2}$).

For a minimal example, take $X_1=\{u,l,r,d\}$ (up, left, right, down) with $u\rightarrow_1l$, $u\rightarrow_1r$, $l\rightarrow_1d$ and $r\rightarrow_1d$ (i.e. $\rightarrow_1$ only moves downwards) , and $X_2=\{0,1\}$ with $0\rightarrow_2 1$. The pair $(l,1)\leftarrow (u,0)\rightarrow (r,1)$ can not be closed because $1$ is normal so that the system is not confluent.

$\endgroup$

Your Answer

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

Browse other questions tagged or ask your own question.