Estrutura lógica vs teoria dos tipos

Resumo. Uma estrutura lógica é uma meta-linguagem para a formalização de sistemas dedutivos, onde deduções se tornam objetos sintáticos.

Obviamente, o que conta como meta-linguagem é bastante vago e é útil entender o desenvolvimento histórico de estruturas lógicas. O primeiro arcabouço lógico foi o Automath (1) de Bruijn, baseado em -calculus. Muitas das idéias da família de idiomas Automath chegaram às estruturas lógicas modernas. O trabalho de Martin-Löf sobre teorias construtivas de tipos, também baseado em -calculi, também foi influente. $\lambda$ $\lambda$

O LF de Edimburgo (2) é uma estrutura lógica muito influente. Edinburgh LF é o que você obtém quando enriquece o -calculus simplesmente digitado com dependência de tipo. Isso é tudo. Para tornar a dependência de tipo precisa, é necessário substituir o operador de espaço de função nos tipos pela abstração de tipo, geralmente escrita e introduza o tipo de tipos, bem como a abstração de tipos. Em termos de regras, a chave está na regra de eliminação para , resp. : $\lambda$ $A \rightarrow B$ $\Pi x^A. B$ $A \rightarrow B$ $\Pi x^A. B$

\frac{Γ ⊢ M : A \to B Γ ⊢ N : A}{Γ ⊢ M N : B} \frac{Γ ⊢ M : Π x^{A} . B Γ ⊢ N : A}{Γ ⊢ M N : B {N / x}}

$\newcommand{\TYPES}[3]{#1 \vdash #2 : #3} \newcommand{\SUBST}[2]{\{#1/#2\}} \frac{ \TYPES{\Gamma}{\color{red}{M}}{A \rightarrow B} \qquad \TYPES{\Gamma}{\color{red}{N}}{A} }{ \TYPES{\Gamma}{\color{red}{MN}}{B} } \qquad \frac{ \TYPES{\Gamma}{{\color{red}M}}{\Pi x^A. B} \qquad \TYPES{\Gamma}{\color{red}{N}}{A} }{ \TYPES{\Gamma}{{\color{red}{MN}}}{B\SUBST{{\color{red}N}}{x}} }$

À esquerda, temos a regra para o -calculus simplesmente digitado ; à direita, a regra que generaliza a esquerda com dependência de tipo. Vemos que um valor 'flui' para o tipo na conclusão à direita. $\lambda$

Eu acho que a assistente interativa de provas Isabelle usa lógica intuicionista de segunda ordem com base em -calculus, sem nenhum número ou tipos de dados recursivos como estrutura lógica. Vários outros foram propostos. $\lambda$

Uma vantagem de usar -calculi como estrutura lógica é que construções de ligação como quantificadores universais podem ser implementadas usando o encadernador estrutura. Observe que a maioria das estruturas lógicas é expressivamente fraca: as estruturas suportam o raciocínio no nível do objeto, mas são insuficientes para executar muito raciocínio metateórico, além do fato de que uma determinada instrução no nível do objeto é um teorema. De fato, a lógica do metal é geralmente tão fraca que até provar o teorema da dedução para uma lógica de objetos no estilo Hilbert é impossível. Obviamente, nada impede você de usar teorias de tipos mais poderosas como estrutura lógica. $\lambda$ $\lambda$

Por essas razões práticas e históricas, a maioria das estruturas lógicas em uso atualmente são do tipo -calculi, isto é, teorias de tipos. Veja (3, 4) para discussões mais aprofundadas sobre estruturas lógicas. $\lambda$

N. de Bruijn: A linguagem matemática AUTOMATH, seu uso e algumas de suas extensões.
RF Harper, F. Honsell, G. Plotkin: Uma estrutura para definir lógicas .
F. Pfenning: estruturas lógicas.
F. Pfenning: Estruturas Lógicas - Uma Breve Introdução .

Martin Berger
fonte

Você conhece algum livro introdutório sobre assistentes de prova (estruturas lógicas) adequados para alguém que já conhece os conceitos básicos de cálculo lambda simplesmente digitado e lógica de primeira ordem?

Trismegistos

@Trismegistos Acho que não. Sugiro aprender um assistente específico. O Agda é o mais fácil de entrar, pois é basicamente Haskell, mas com tipos dependentes. Na minha experiência, a estrutura lógica não é tão importante quanto outras dimensões dos assistentes de prova. Por exemplo, Isabelle é um provador genérico que você pode instanciar com diferentes lógicas, expondo realmente a estrutura lógica. Mas Isabelle / HOL é a única instanciação usada na prática. Isso ocorre porque todas as táticas de prova, todo o suporte do testador foram escritos para a lógica do objeto HOL. E a usabilidade de um provador depende disso.

Martin Berger

Estrutura lógica vs teoria dos tipos

Respostas: