Prueba de confluencia para un sistema de reescritura simple

Supongamos que tenemos un lenguaje simple que consiste en los términos:

• $\mathtt{true}$
• $\mathtt{false}$
• si son términos, entonces también lo es i $t_1,t_2,t_3$$\mathtt{if}\: t_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3$

Ahora asuma las siguientes reglas de evaluación lógica:

$$\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*}$$

Supongamos que también agregamos la siguiente regla funky:

$$\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]}$$

Para este lenguaje simple con las reglas de evaluación dadas, deseo demostrar lo siguiente:

Teorema: Si y r → t entonces hay algún término u tal que s → T y T → T .$r \rightarrow s$$r \rightarrow t$$u$$s \rightarrow u$$t \rightarrow u$

Estoy probando esto por inducción en la estructura de . Aquí está mi prueba hasta ahora, todo funcionó bien, pero estoy atrapado en el último caso. Parece que la inducción en la estructura de r no es suficiente, ¿alguien puede ayudarme?$r$$r$

Prueba. Por inducción en , separaremos todas las formas que r puede tomar:$r$$r$

1. es una constante, nada que demostrar ya que una forma normal no evalúa nada.$r$
2. si es verdadero, entonces r 2 más r 3 . (a) ambas derivaciones se realizaron con la regla E-IfTrue. En este caso s = t , entonces no hay nada que probar. (b) una derivación se realizó con la regla E-IfTrue, la otra con la regla E-Funny. Suponga que r → s se realizó con E-IfTrue, el otro caso se prueba de manera equivalente. Ahora sabemos que s = r 2 . También sabemos que t = si es verdadero, entonces r ′ 2 más r 3 y que existe alguna derivación r 2$r=$$r_2$$r_3$$s=t$$r \rightarrow s$$s = r_2$$t =$$r'_2$$r_3$ (la premisa). Si ahora elegimosu=r ′ 2 , concluimos el caso.$r_2 \rightarrow r'_2$$u = r'_2$
3. si es falso entonces r 2 más r 3 . Equivalentemente probado como arriba.$r=$$r_2$$r_3$
4. si r 1 entonces r 2 más r 3 con r 1 ≠ verdadero o falso. (a) ambas derivaciones se realizaron con la regla E-If. Ahora sabemos que s = si r ′ 1 entonces r 2 más r 3 y t = si r ″ 1 entonces r 2 más r 3 . También sabemos que existen derivaciones r 1 → r ′ $r=$$r_1$$r_2$$r_3$$r_1 \neq$$s =$$r'_1$$r_2$$r_3$$t =$$r''_1$$r_2$$r_3$$r_1 \rightarrow r'_1$y (las premisas). Ahora podemos usar la hipótesis de inducción para decir que existe algún término r ‴ 1 tal que r ′ 1 → r ‴ 1 y r ″ 1 → r ‴ 1 . Ahora concluimos el caso diciendo u = si r ‴ 1 entonces r 2 más r 3 y notando que s → u y t $r_1 \rightarrow r''_1$$r'''_1$$r'_1 \rightarrow r'''_1$$r''_1 \rightarrow r'''_1$$u =$$r'''_1$$r_2$$r_3$$s \rightarrow u$$t \rightarrow u$por la regla E-If. (b) una derivación fue realizada por la regla E-If y otra por la regla E-Funny.

Este último caso, donde una derivación fue realizada por E-If y otra por E-Funny es el caso que me falta ... Parece que no puedo usar las hipótesis.

Ayuda será muy apreciada.

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.

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.}