Uma pergunta sobre lógica e a correspondência Curry-Howard

Question

Você poderia me explicar qual é a conexão básica entre os fundamentos da programação lógica e o fenômeno da semelhança sintática entre sistemas de tipos e lógica convencional?

Answer 1

A correspondência Curry-Howard não trata de programação lógica, mas de programação funcional.A mecânica fundamental do Prolog é justificada na teoria da prova pela teoria de John Robinson técnica de resolução, que mostra como é possível verificar se as fórmulas lógicas expressas como cláusulas de Horn são satisfatório, isto é, se você pode encontrar termos para substituir suas variáveis ​​lógicas que os tornam verdadeiros.

Assim, a programação lógica consiste em especificar programas como fórmulas lógicas, e o cálculo do programa é alguma forma de inferência de prova, em resolução Prolog, como eu disse.Em contraste, a correspondência Curry-Howard mostra como as provas em uma formulação especial da lógica, chamada dedução natural, correspondem a programas do cálculo lambda, sendo o tipo de programa correspondente à fórmula que a prova comprova;a computação no cálculo lambda corresponde a um fenômeno importante na teoria da prova chamado normalização, que transforma as provas em provas novas e mais diretas.Portanto, a programação lógica e a programação funcional correspondem a diferentes níveis nestas lógicas:os programas lógicos correspondem às fórmulas de uma lógica, enquanto os programas funcionais correspondem às provas das fórmulas.

Há outra diferença:as lógicas usadas são geralmente diferentes.A programação lógica geralmente usa lógicas mais simples - como eu disse, o Prolog é baseado em cláusulas de Horn, que são uma classe altamente restrita de fórmulas onde as implicações podem não ser aninhadas e não há disjunções, embora o Prolog recupere toda a força da lógica clássica usando o regra de corte.Por outro lado, linguagens de programação funcionais como Haskell fazem uso intenso de programas cujos tipos têm implicações aninhadas e são decorados por todos os tipos de formas de polimorfismo.Eles também se baseiam na lógica intuicionista, uma classe de lógica que proíbe o uso do princípio do terceiro excluído, no qual se baseia o mecanismo computacional de Robinson.

Alguns outros pontos:

1. É possível basear a programação lógica em lógicas mais sofisticadas do que as cláusulas de Horn;por exemplo, Lambda-prolog é baseado na lógica intuicionista, com um mecanismo de computação diferente da resolução.
2. Dale Miller chamou o paradigma da teoria da prova por trás da programação lógica de pesquisa de prova como programação metáfora, para contrastar com a provas como programas metáfora que é outro termo usado para a correspondência Curry-Howard.

Answer 2

A programação lógica é fundamentalmente sobre a busca de objetivos em busca de provas. A relação estrutural entre idiomas digitados e lógica geralmente envolve linguagens funcionais, embora às vezes imperativas e outras línguas - mas não diretamente de linguagens de programação lógica. Esse relacionamento relaciona provas aos programas.

Portanto, a pesquisa de prova de programação lógica pode ser usada para encontrar provas que são interpretadas como programas funcionais. Este parece ser o relacionamento mais direto entre os dois (como você pediu).

Construir programas inteiros dessa maneira não é prático, mas pode ser útil para preencher detalhes tediosos em programas, e há alguns exemplos importantes disso na prática. Um exemplo básico disso é a subtipagem estrutural - que corresponde ao preenchimento de algumas etapas de prova por meio de uma prova simples. Um exemplo muito mais sofisticado é o sistema de classe de tipo de Haskell, que envolve um tipo específico de pesquisa direcionada a meta - no extremo, isso envolve uma forma de programação lógica completa a Turing no momento da compilação.