Confluence proof for a simple rewriting system

Question

Assume we have a simple language that consists of the terms:

• $\mathtt{true}$
• $\mathtt{false}$
• if $t_1,t_2,t_3$ are terms then so is $\mathtt{if}\: t_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3$

Now assume the following logical evaluation rules:

$$ \begin{gather*} \dfrac{} {\mathtt{if}\: \mathtt{true} \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3 \to t_2} \text{[E-IfTrue]} \quad \dfrac{} {\mathtt{if}\: \mathtt{false} \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3 \to t_3} \text{[E-IfFalse]} \\ \dfrac{t_1 \to t_1'} {\mathtt{if}\: t_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3 \to \mathtt{if}\: t_1' \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3} \text{[E-If]} \\ \end{gather*} $$

Suppose we also add the following funky rule:

$$ \dfrac{t_2 \to t_2'} {\mathtt{if}\: t_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3 \to \mathtt{if}\: t_1 \:\mathtt{then}\: t_2' \:\mathtt{else}\: t_3} \text{[E-IfFunny]} $$

For this simple language with the given evaluation rules I wish to prove the following:

Theorem: If $r \rightarrow s$ and $r \rightarrow t$ then there is some term $u$ such that $s \rightarrow u$ and $t \rightarrow u$.

I am proving this by induction on the structure of $r$. Here is my proof so far, it all worked out well, but I am stuck at the very last case. It seems like induction on the structure of $r$ is not sufficing, can anyone help me out?

Proof. By induction on $r$, we will seperate all the forms that $r$ can take:

1. $r$ is a constante, nothing to prove since a normal form does not evaluate to anything.
2. $r=$ if true then $r_2$ else $r_3$. (a) both derivations were done with the E-IfTrue rule. In this case $s=t$, so there is nothing to prove. (b) one deriviation was done with the E-IfTrue rule, the other with the E-Funny rule. Assume $r \rightarrow s$ was done with E-IfTrue, the other case is equivalently proven. We now know that $s = r_2$. We also know that $t =$ if true then $r'_2$ else $r_3$ and that there exists some deriviation $r_2 \rightarrow r'_2$ (the premise). If we now choose $u = r'_2$, we conclude the case.
3. $r=$ if false then $r_2$ else $r_3$. Equivalently proven as above.
4. $r=$ if $r_1$ then $r_2$ else $r_3$ with $r_1 \neq $ true or false. (a) both deriviations were done with the E-If rule. We now know that $s =$ if $r'_1$ then $r_2$ else $r_3$ and $t =$ if $r''_1$ then $r_2$ else $r_3$. We also know that there exists deriviations $r_1 \rightarrow r'_1$ and $r_1 \rightarrow r''_1$ (the premises). We can now use the induction hypothese to say that there exists some term $r'''_1$ such that $r'_1 \rightarrow r'''_1$ and $r''_1 \rightarrow r'''_1$. We now conclude the case by saying $u =$ if $r'''_1$ then $r_2$ else $r_3$ and noticing that $s \rightarrow u$ and $t \rightarrow u$ by the E-If rule. (b) one derivation was done by the E-If rule and one by the E-Funny rule.

This latter case, where one derivation was done by E-If and one by E-Funny is the case I am missing... I can't seem to be able to use the hypotheses.

Help will be much appreciated.

Answer 1

Okay, so let's consider the case that $r = \mathtt{if}\: t_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3$, $s$ has been derived by applying the E-If rule and $t$ has been derived by applying the E-Funny rule: So $s = \mathtt{if}\: t'_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3$ where $t_1 \rightarrow t'_1$ and $t = \mathtt{if}\: t_1 \:\mathtt{then}\: t'_2 \:\mathtt{else}\: t_3$ where $t_2 \rightarrow t'_2$.

The $u$ we're looking for is $u = \mathtt{if}\: t'_1 \:\mathtt{then}\: t'_2 \:\mathtt{else}\: t_3$. $s \rightarrow u$ follows from rule E-Funny and $t \rightarrow u$ follows from rule E-If.

Answer 2

A little terminology may help if you want to look this up: these rules are rewriting rules, they have nothing to do with type systems¹. The property you're trying to prove is called confluence; more specifically, it's strong confluence: if a term can be reduced in different ways at one step, they can converge back at the next step. In general, confluence allows there to be any number of steps and not just one: if $r\to^*s$ and $r\to^*t$ then there is $u$ such that $s\to^*u$ and $t\to^*u$ — if a term can be reduced in different ways, no matter how far they've diverged, they can eventually converge back.

The best way to prove a property of such inductively defined rewriting rules is by induction over the structure of the derivation of the reduction, rather than the structure of the reduced term. Here, either works, because the rules follow the structure of the left-hand term, but reasoning on the rules is simpler. Instead of diving into the term, you take all pairs of rules, and see what term could be a left-hand side for both. In this example, you will get the same cases in the end, but a bit faster.

In the case that gives you trouble, one side reduces the “if” part and the other side reduces the “then” part. There's no overlap between the two parts that change ($t1$ in [E-If], $t_2$ in [E-IfFunny]), and there's no constraint on $t_2$ in [E-If] or on $t_1$ in [E-IfFunny]. So when you have a term to which both rules apply — which must be of the form $\mathtt{if}\: r_1 \:\mathtt{then}\: r_2 \:\mathtt{else}\: r_3$, you can choose to apply the rules in either order:

$$\begin{array}{rcl} & \mathtt{if}\: r_1 \:\mathtt{then}\: r_2 \:\mathtt{else}\: r_3 & \\ {\small \text{[E-If]}} \swarrow & & \searrow {\small \text{[E-IfFunny]}} \\ \mathtt{if}\: r_1' \:\mathtt{then}\: r_2 \:\mathtt{else}\: r_3 & & \mathtt{if}\: r_1 \:\mathtt{then}\: r_2' \:\mathtt{else}\: r_3 \\ {\small \text{[E-IfFunny]}} \searrow & & \swarrow {\small \text{[E-If]}} \\ & \mathtt{if}\: r_1' \:\mathtt{then}\: r_2' \:\mathtt{else}\: r_3 & \\ \end{array} $$

¹ _{You'll sometimes see types and rewriting together, but at their core they're orthogonal concepts.}