Como eu aprenderia a teoria subjacente do assistente de prova Coq?
40
Vou recapitular as anotações do curso no CIS 500: Software Foundations e os exercícios são muito divertidos. Estou apenas no terceiro exercício, mas gostaria de saber mais sobre o que está acontecendo quando uso táticas para provar coisas comoforall (n m : nat), n + n = m + m -> n = m.
Um ponto de partida é o manual de referência Coq ( pdf ). O capítulo 4 descreve a lógica subjacente da Coq e, finalmente, tudo se baseia nisso. É chamado de cálculo de construções (co) indutivas, e muitos trabalhos descrevem. Colocar as mãos no livro Coq'Art Provas de teoremas interativos e desenvolvimento de programas fornece uma introdução mais divertida, mas não barata, à Coq.
Para construir a teoria necessária, você precisa aprender sobre a teoria dos tipos . O mais intimamente relacionado à teoria subjacente a um assistente de prova é provavelmente as notas (ou livro ) da Teoria Intucionista de Per Martin-Löf ou o livro Programação na teoria dos tipos de Martin-Löf , que trata realmente de escrever e provar teoremas na teoria dos tipos. Uma perspectiva da linguagem de programação sobre a teoria dos tipos pode ser obtida nos Tipos e Linguagens de Programação de Pierce . As provas e tipos de Girard et al. , Que também abordam a importância da correspondência de Curry-Howard , são outra excelente referência. Então você provavelmente está bem e verdadeiramente pronto para ler os livros de Coquand e Huet.O cálculo das construções . Finalmente, procure algumas das referências no final do manual Coq.
Existem outros assistentes de prova , HOL, NuPRL, Mizar, Twelf, etc., e eles também têm sua teoria, para que você possa aprender muito também lendo nessa direção.
Por fim, para uma visão geral da história e do futuro dos assistentes de provas, confira o artigo recente de Herman Geuvers.
Boa lista. Vou adicionar uma ordem de leitura. O TAPL de Pierce cobre o fundo; a maior parte do resto não fará sentido até você se familiarizar com as regras de digitação. O capítulo 2 do ATTAPL apresenta tipos dependentes de forma relativamente suave. Depois, você pode ler o capítulo 4 do manual Coq, que possui as regras de digitação (você precisa verificar a bibliografia para obter informações avançadas, como as regras exatas para recursão). Paralelamente, o livro Coq'Art tem uma visão mais prática. Dica de bônus: Show Treeem coq.
Gilles 'SO- stop be evil'
2
Eu sou alguém mais ou menos na mesma posição do OP, embora um pouco mais adiante. Após algumas experiências, finalmente encontrei a ordem 1) Aprenda programação funcional 2) leia TAPL 3) Leia sobre tipos dependentes no ATTAPL para funcionar melhor do que outras coisas. Fico feliz em saber que estou aproximadamente no caminho certo.
John Salvatier
11
Eu também estava aqui e peguei o livro Coq'Art. É absolutamente perfeito para a compreensão, eles detalham cada tática e explicam quando e como usá-la. O livro também orienta você rapidamente em todas as regras básicas da teoria dos tipos, ensinando a notação e como usá-la no Coq. Amando este livro.
Lance Pollard
15
Quanto ao cálculo lambda digitado, lógica intuicionista, vários sistemas de prova e isomorfismo de Curry-Howard, que são todas partes da formação matemática da Coq, recomendo vivamente "Palestras sobre o isomorfismo de Curry-Howard" (de P. Urzyczyn e M. Sørensen).
O livro de Luo sobre o Cálculo Estendido de Construções também é uma boa referência. O ECC foi bastante influente no projeto da teoria dos tipos de Coq.
Show Treeem coq.Quanto ao cálculo lambda digitado, lógica intuicionista, vários sistemas de prova e isomorfismo de Curry-Howard, que são todas partes da formação matemática da Coq, recomendo vivamente "Palestras sobre o isomorfismo de Curry-Howard" (de P. Urzyczyn e M. Sørensen).
fonte
O livro de Luo sobre o Cálculo Estendido de Construções também é uma boa referência. O ECC foi bastante influente no projeto da teoria dos tipos de Coq.
fonte
O livro atual do Software Foundations explica tudo isso posteriormente: https://softwarefoundations.cis.upenn.edu/lf-current/ProofObjects.html
Então, se você está seguindo o livro, continue lendo :)
fonte