Prova de confluência para um sistema de reescrita simples

14

Suponha que temos uma linguagem simples que consiste nos termos:

  • true
  • false
  • se são termos, o mesmo acontece comt1,t2,t3ift1thent2elset3

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

iftruethent2elset3t2[E-IfTrue]iffalsethent2elset3t3[E-IfFalse]t1t1ift1thent2elset3ift1thent2elset3[E-If]

Suponha que também adicionemos a seguinte regra descolada:

t2t2ift1thent2elset3ift1thent2elset3[E-IfFunny]

Para esta linguagem simples, com as regras de avaliação fornecidas, desejo provar o seguinte:

Teorema: Se rs e rt , existe algum termo u tal que su e tu .

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:

  1. r é uma constante, nada a provar, pois uma forma normal não avalia nada.
  2. r= se true então r2 else r3 . (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 rs foi feito com o E-IfTrue, o outro caso é comprovado de forma equivalente. Agora sabemos que s=r2 . Também sabemos que t= se verdadeiro, então r2 else r3 e que existe alguma derivação r2r2 (a premissa). Se agora escolhermos u=r2 , concluiremos o caso.
  3. r 2 r 3r= se falso, então else . Equivalentemente comprovado como acima.r2r3
  4. r 1 r 2 r 3 r 1s = r 1 r 2 r 3 t = r 1 r 2 r 3 r 1r 1 r 1r 1 r 1 r 1r 1 r 1r 1 u = 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 quer1r2r3r1s=r1r2r3t=r1r2r3r1r1r1r1r1r1r1e . 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.r1r1u= R2R3sutur1r2r3sutu

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.

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:

7

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 . s t s = i fr=ift1thent2elset3stt 1t 1 t = i fs=ift1thent2elset3t1t1t 2t 2t=ift1thent2elset3t2t2

O que estamos procurando é . segue a regra E-Funny e segue a regra E-If.u = i fu s u t uu=ift1thent2elset3sutu

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? su
Codde
@ Jeroen Você está certo - eu os misturei. Corrigido agora.
sepp2k
8

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 * t u s * u t * ursrtusutu

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:t 2 t 2 t 1 it1t2t2t1ifr1thenr2elser3

ifr1thenr2elser3[E-If][E-IfFunny]ifr1thenr2elser3ifr1thenr2elser3[E-IfFunny][E-If]ifr1thenr2elser3

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