Regra de eliminação baseada na unificação para igualdade

10

Alguns anos atrás, encontrei a seguinte regra de esquerda para a igualdade no cálculo sequencial:

stθθ(Γ)θ(C)Γ,stC

Aqui, stθ calcula o unificador geral mais θ para s e t , e, em seguida, aplica-se o substition à conclusão C e todas as hipóteses no contexto Γ .

O interessante dessa unificação é que ela equivale a encontrar uma substituição para variáveis ​​universais (isto é, skolem).

No entanto, não me lembro onde li isso e fiquei pensando se alguém poderia me ajudar a encontrar uma referência a ele.

Neel Krishnaswami
fonte

Respostas:

9

Eu sempre atribuí isso a Regras de reflexão de definição de Schroeder-Heister, embora a idéia remova além disso a Girard e outros; a regra que você procura é uma instância da primeira exibição na Seção 4. Você também precisa de uma regra que diga que, se a instância de unificação for insatisfatória, a suposição de igualdade terá a força de uma contradição.

Uma descrição mais geral foi usada recentemente em muitos trabalhos de Dale Miller, David Baelde e da empresa (veja, por exemplo, Menos e maiores pontos fixos na lógica linear ). A formulação mais geral - que também não se origina de Miller et al - é que a regra é

{θcsu(t,s)θΓθC}Γ,tsC

onde é o conjunto completo de unificadores - o conjunto de todas as substituições unificadoras de e . Você também pode preferir a maneira equivalente de escrever esta regra que eu prefiro (veja aqui, por exemplo).t scsu(t,s)ts

θ.θt=θsθΓθCΓ,tsC

Em qualquer caso, em uma linguagem de termo com unificação decidível em que a existência de um unificador implica a existência de um unificador mais geral, uma das regras acima pode mostrar-se equivalente a ter essas duas regras:

no mgvocê(t,s)Γ,tsCmgvocê(t,s)=θθΓθCΓ,tsC

(PS Frank discutiu isso em seu curso de programação lógica nas aulas 6, 7 e 8, que podem ser de onde você se lembra.)

Rob Simmons
fonte
11
Obrigado! Eu estava olhando os papéis errados de Schroeder-Heister.
Neel Krishnaswami
2
Eu provavelmente devo acrescentar que estive pensando sobre isso no contexto de digitação de textos para GADTs.
Neel Krishnaswami
11
Hã. Eu tenho escrito sobre isso no contexto de OMG THESIS DEVE GRADUAR-SE, por isso não estou autorizado a pensar sobre isso no contexto de datilografia para GADTs ;-).
Rob Simmons