Prova de confluência para um sistema de reescrita simples

Suponha que temos uma linguagem simples que consiste nos termos:

$\mathtt{true}$
$\mathtt{false}$
se são termos, o mesmo acontece com $t_1,t_2,t_3$ $\mathtt{if}\: t_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3$

Agora assuma as seguintes regras de avaliação lógica:

\begin{matrix} \frac{}{i f t r u e t h e n t_{2} e l s e t_{3} \to t_{2}} [E-IfTrue] \frac{}{i f f a l s e t h e n t_{2} e l s e t_{3} \to t_{3}} [E-IfFalse] \\ \frac{t_{1} \to t_{1}^{'}}{i f t_{1} t h e n t_{2} e l s e t_{3} \to i f t_{1}^{'} t h e n t_{2} e l s e t_{3}} [E-If] \end{matrix}

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

Suponha que também adicionemos a seguinte regra descolada:

\frac{t_{2} \to t_{2}^{'}}{i f t_{1} t h e n t_{2} e l s e t_{3} \to i f t_{1} t h e n t_{2}^{'} e l s e t_{3}} [E-IfFunny]

$\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 esta linguagem simples, com as regras de avaliação fornecidas, desejo provar o seguinte:

Teorema: Se $r \rightarrow s$ e $r \rightarrow t$ , existe algum termo $u$ tal que $s \rightarrow u$ e $t \rightarrow u$ .

Estou provando isso por indução na estrutura de $r$ . Aqui está a minha prova até agora, tudo funcionou bem, mas estou preso no último caso. Parece que a indução na estrutura de $r$ não é suficiente, alguém pode me ajudar?

Prova. Por indução em $r$ , separaremos todas as formas que $r$ pode assumir:

$r$ é uma constante, nada a provar, pois uma forma normal não avalia nada.
$r=$ se true então $r_2$ else $r_3$ . (a) ambas as derivações foram feitas com a regra E-IfTrue. Nesse caso, $s=t$ , então não há nada a provar. (b) uma derivação foi feita com a regra E-IfTrue, a outra com a regra E-Funny. Suponha que $r \rightarrow s$ foi feito com o E-IfTrue, o outro caso é comprovado de forma equivalente. Agora sabemos que $s = r_2$ . Também sabemos que $t =$ se verdadeiro, então $r'_2$ else $r_3$ e que existe alguma derivação $r_2 \rightarrow r'_2$ (a premissa). Se agora escolhermos $u = r'_2$ , concluiremos o caso.
$r=$ se falso, então else . Equivalentemente comprovado como acima. $r_2$ $r_3$
$r=$ se então else com verdadeiro ou falso. (a) ambas as derivações foram feitas com a regra E-If. Agora sabemos que se então else e se então else . Sabemos também que existe deriviations e (nas instalações). Agora podemos usar a hipótese de indução para dizer que existe algum termo tal que $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$ $r_1 \rightarrow r''_1$ $r'''_1$ $r'_1 \rightarrow r'''_1$ e . Agora concluímos o caso dizendo se então else e percebendo que e pela regra E-If. (b) uma derivação foi feita pela regra E-If e uma pela regra E-Funny. $r''_1 \rightarrow r'''_1$ $u =$ $r'''_1$ $r_2$ $r_3$ $s \rightarrow u$ $t \rightarrow u$

Neste último caso, em que uma derivação foi feita pelo E-If e uma pelo E-Funny é o caso que estou perdendo ... Parece que não consigo usar as hipóteses.

A ajuda será muito apreciada.

logic semantics proof-techniques term-rewriting codd
fonte

@Gilles extremamente bem feito com a edição. Eu não sabia que o motor de TeX da SE era capaz de tudo isso ... :-)

Codd

Estou errado ou este exercício foi retirado do Pierce "Types and Programming Languages"?

Fabio F.

@FabioF. É de fato do livro Tipos e Linguagens de Programação de Pierce. Ele fornece uma prova que acho incerta, devido à maneira como ele realiza a indução. É por isso que tentei provar isso por indução na estrutura. Eu estava pensando em mencionar que era do livro, mas achei que isso seria bastante irrelevante. Bem notado, no entanto!

Codd #

Respostas:

Ok, então vamos considerar o caso em que , foi derivado pela aplicação da regra E-If e foi obtido aplicando a regra E-Funny: Então, que e onde . $r = \mathtt{if}\: t_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3$ $s$ $t$ $s = \mathtt{if}\: t'_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3$ $t_1 \rightarrow t'_1$ $t = \mathtt{if}\: t_1 \:\mathtt{then}\: t'_2 \:\mathtt{else}\: t_3$ $t_2 \rightarrow t'_2$

O que estamos procurando é . segue a regra E-Funny e segue a regra E-If. $u$ $u = \mathtt{if}\: t'_1 \:\mathtt{then}\: t'_2 \:\mathtt{else}\: t_3$ $s \rightarrow u$ $t \rightarrow u$

sepp2k
fonte

Bata-me para isso. Bom trabalho.

precisa saber é o seguinte

Puxa, eu estava realmente olhando muito longe ... Obrigado!

Codd #

Você misturou-se, porém, Decorre E-engraçado. Ou estou vendo algo errado?

s \to u

$s \rightarrow u$

Codde

@ Jeroen Você está certo - eu os misturei. Corrigido agora.

sepp2k

Um pouco de terminologia pode ajudar se você quiser pesquisar isso: essas regras estão reescrevendo regras , elas não têm nada a ver com sistemas de tipos¹. A propriedade que você está tentando provar se chama confluência ; mais especificamente, é uma forte confluência : se um termo pode ser reduzido de maneiras diferentes em uma etapa, ele pode convergir de volta na próxima etapa. Em geral, confluência permite que haja qualquer número de etapas, e não apenas um: se e então há de tal modo que e - se um termo puder ser reduzido de maneiras diferentes, não importa o quanto eles divergam, eles poderão eventualmente voltar a convergir. $r\to^*s$ $r\to^*t$ $u$ $s\to^*u$ $t\to^*u$

A melhor maneira de provar uma propriedade dessas regras de reescrita definidas indutivamente é pela indução sobre a estrutura da derivação da redução, em vez da estrutura do termo reduzido. Aqui, ambos funcionam, porque as regras seguem a estrutura do termo esquerdo, mas o raciocínio sobre as regras é mais simples. Em vez de mergulhar no termo, você adota todos os pares de regras e vê qual termo pode ser o lado esquerdo de ambos. Neste exemplo, você obterá os mesmos casos no final, mas um pouco mais rápido.

No caso de problemas, um lado reduz a parte "se" e o outro lado reduz a parte "então". Não há sobreposição entre as duas partes que mudam ( em [E-If], em [E-IfFunny]) e não há restrições em em [E-If] ou em em [E-IfFunny]. Portanto, quando você tem um termo ao qual ambas as regras se aplicam - que devem ter o formato , você pode escolher para aplicar as regras em qualquer ordem: $t1$ $t_2$ $t_2$ $t_1$ $\mathtt{if}\: r_1 \:\mathtt{then}\: r_2 \:\mathtt{else}\: r_3$

\begin{array}{rcl} i f r_{1} t h e n r_{2} e l s e r_{3} \\ [E-If] ↙ & ↘ [E-IfFunny] \\ i f r_{1}^{'} t h e n r_{2} e l s e r_{3} & i f r_{1} t h e n r_{2}^{'} e l s e r_{3} \\ [E-IfFunny] ↘ & ↙ [E-If] \\ i f r_{1}^{'} t h e n r_{2}^{'} e l s e r_{3} \end{array}

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

Sometimes _{Às vezes, você pode ver tipos e reescrever juntos, mas no fundo eles são conceitos ortogonais.}

Gilles 'SO- parar de ser mau'
fonte