Grosso modo, com uma incorporação profunda de uma lógica, você (1) define um tipo de dados que representa a sintaxe para sua lógica e (2) fornece um modelo da sintaxe e (3) prova que axiomas sobre sua sintaxe são sólidos com respeito para o modelo. Com uma incorporação superficial, você pula as etapas (1) e (2) e apenas começa com um modelo e prova as vinculações entre as fórmulas. Isso significa que casamentos superficiais geralmente são menos trabalhosos para decolar, pois representam o trabalho que você normalmente acabaria fazendo de qualquer maneira com uma incorporação profunda.
No entanto, se houver uma incorporação profunda, geralmente é mais fácil escrever procedimentos de decisão reflexivos, já que você está trabalhando com fórmulas que possuem realmente sintaxe que você pode recorrer. Além disso, se o seu modelo é estranho ou complicado, geralmente você não deseja trabalhar diretamente com a semântica. (Por exemplo, se você usar a biorrogonalidade para forçar o fechamento admissível, ou usar os modelos do estilo Kripke para forçar as propriedades do quadro em lógicas de separação ou jogos semelhantes.) No entanto, os embeddings profundos quase certamente o forçarão a pensar muito sobre ligações e substituições variáveis , que encherá seu coração de raiva, já que isso é (a) trivial e (b) uma fonte inesgotável de aborrecimento.
A sequência correta que você deve seguir é: (1) tente sobreviver com uma incorporação superficial. (2) Quando isso acabar, tente usar táticas e cotações para executar os procedimentos de decisão que você deseja executar. (3) Se isso também acabar, desista e use uma sintaxe do tipo dependente para sua incorporação profunda.
- Planeje levar alguns meses em (3) se esta for sua primeira vez. Você vai precisar para se familiarizar com a fantasia características de seu assistente de prova para manter a sanidade. (Mas este é um investimento que será recompensado em geral.)
- Se o seu assistente de prova não tiver tipos dependentes, permaneça no nível 2.
- Se o idioma do seu objeto for digitado de forma independente, mantenha-se no nível 2.
Além disso, não tente subir gradualmente a escada. Ao decidir subir a escada da complexidade, dê um passo completo de cada vez. Se você fizer as coisas pouco a pouco, obterá muitos teoremas estranhos e inutilizáveis (por exemplo, obterá várias sintaxes meia-boca e teoremas que misturam sintaxe e semântica de maneiras estranhas), que você eventualmente tem que jogar fora.
Edição: Aqui está um comentário explicando por que subir a escada gradualmente é tão tentador e por que leva (em geral) ao sofrimento.
Concretamente, suponha que você tenha um banco de areia a incorporação da lógica de separação, com os conectivos e unidade . Então, você provará teoremas como e e assim por diante. Agora, quando você tentar realmente usar a lógica para provar que um programa está correto, você terá algo como e realmente desejará algo como .I A ⋆ BA⋆BI( A ⋆ B ) ⋆ CA⋆B⟺B⋆A( I ⋆ A ) ⋆ ( B ⋆ C ) A ⋆ ( B ⋆ ( C ⋆ I ) )(A⋆B)⋆C⟺A⋆(B⋆C)(I⋆A)⋆(B⋆C)A⋆(B⋆(C⋆I))
Nesse ponto, você ficará aborrecido com a necessidade de reassociar manualmente as fórmulas e pensará: "Eu sei! Vou interpretar um tipo de dados de listas como uma lista de fórmulas separadas. Dessa forma, posso interpretar como concatenação dessas listas e, em seguida, as fórmulas acima serão definitivamente iguais! "⋆
Isso é verdade e funciona! No entanto, observe que a conjunção também é ACUI, assim como disjunção. Portanto, você passará pelo mesmo processo em outras provas, com tipos de dados de lista diferentes e, em seguida, terá três sintaxes para fragmentos diferentes da lógica de separação, além de ter metateoremas para cada um deles, que inevitavelmente serão diferentes, e você se sentirá querendo um metateorema comprovado para separar a conjunção por disjunção e, em seguida, desejará misturar sintaxes e, em seguida, ficará louco.
É melhor direcionar o maior fragmento possível com um esforço razoável e apenas fazê-lo.
É importante entender que existe um espectro de profundo a raso. Você modela profundamente as partes de sua linguagem que de alguma forma devem participar de algum argumento indutivo sobre a construção dela; o restante fica melhor na visão superficial da semântica direta do substrato da lógica.
Por exemplo, quando você deseja discutir sobre o Hoare Logic, pode modelar a linguagem da expressão de maneira superficial, mas o contorno da linguagem atribuir se enquanto deve ser um tipo de dados concreto. Você não precisa inserir a estrutura de x + y ou a <b, mas precisa trabalhar com
while
etc.Nas outras respostas, houve alusões a tipos dependentes. Isso lembra o antigo problema de representar linguagens com ligantes de maneira sã, de modo que elas sejam tão superficiais quanto possível, mas ainda admitam alguns argumentos indutivos. Minha impressão é que o júri ainda está julgando todas as diferentes abordagens e documentos que surgiram nos últimos 10 a 20 anos sobre esse assunto. O "desafio POPLmark" para as diferentes comunidades de assistentes de provas também foi sobre isso em certa medida.
Estranhamente, no HOL clássico sem tipos dependentes, a abordagem HOL-Nominal de C. Urban funcionou muito bem para encadernação superficial, embora não acompanhasse as mudanças culturais nessas comunidades de formalização da linguagem de programação.
fonte