[Solved]: Confluence proof for a simple rewriting system

ignougroup
Problem Detail: 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.

Asked By : codd

Answered By : sepp2k

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.
Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/1060