Cálculo lambda de digitação simples e lógica de ordem superior

Qual é a relação entre cálculo lambda simplesmente digitado e lógica de ordem superior?

Sob Curry-Howard, parece que o cálculo lambda simplesmente digitado corresponde à lógica proposicional. Como isso está relacionado à lógica de ordem superior? De acordo com este tutorial de Geuvers: http://typessummerschool07.cs.unibo.it/courses/geuvers-1.pdf, o idioma do HOL parece ser STT. Não deveria ser PROP? O que isso significa?

A Igreja tinha em mente a HOL quando definiu STT?

lo.logic typed-lambda-calculus curry-howard lambda2
fonte

Sim, a Igreja tinha HOL em mente. O truque para obter o HOL do STT é usar a igualdade , além da aplicação e abstração de funções. Então você pode escrever

como

, entre outros. Eu gosto de "As Sete Virtudes da Teoria dos Tipos Simples" como uma introdução ao STT, que aborda esse tipo de pergunta. Talvez eu deva escrever uma resposta ...

(\forall x : α . A_{*})

$(\forall x:\alpha.A_*)$

(λ x : α . A_{*}) = (λ x : α . ⊤)

$(\lambda x:\alpha.A_*)=(\lambda x:\alpha.\top)$

Thomas Klimpel

Então, ao falar sobre Curry-Howard, qual seria a lógica correta equivalente ao STT? HOL ou PROP?

lambda2

No que diz respeito a Curry-Howard, não acho que será HOL. Talvez seja o fragmento multiplicativo do PROP intuicionista, ou seja, PROP intuicionista sem "ou". Mas isso foi para o CCC (categoria fechada cartesiana), e estou um pouco cansado no momento. Provavelmente, o Lambda será traduzido como "implicação", que era o "exponencial" no CCC. O "produto" do CCC era "e", então você precisaria de um "par" no STT para isso. E "ou" seria um tipo de "soma" no STT então, ou seja, uma união disjunta, talvez um se "a" então "b" else "c" fizer isso.

Thomas Klimpel

Eu acho que estou confundindo alguma coisa (ou tudo). Se STT ~ = PROP (via Curry-Howard) e STT também são HOL, então posso usar PROP em algum sentido para ter HOL?

precisa saber é o seguinte

@ ThomasKlimpel: você deve transformar seus comentários em uma resposta.

Cody

Respostas:

A distinção é a seguinte: se o STLC for tomado como uma linguagem primitiva no nível de tipo, adicionando construtores e um pequeno número de axiomas é suficiente para fornecer a você todo o poder expressivo do HOL.

$\iota$ $\omicron$

\forall_{τ} : (τ \to ο) \to ο \supset: ο \to ο \to ο

$\forall_\tau:(\tau\rightarrow \omicron)\rightarrow \omicron\quad \supset:\omicron\rightarrow\omicron\rightarrow \omicron$

$\tau$ $\forall$

\frac{ϕ (x)}{\forall_{τ} (λ x . ϕ (x))} x : τ not free in the hypotheses

$\frac{\phi(x)}{\forall_\tau(\lambda x.\phi(x))}\mbox{$x:\tau$ not free in the hypotheses}$

\frac{\begin{matrix} [ψ] \\ . \\ . \\ . \\ ϕ \end{matrix}}{ψ \supset ϕ}

$\frac{\Large{\substack{[\psi]\\ \\ .\\ .\\ .\\ \\ \phi}}}{\psi\supset \phi}$

$[\psi]$ $\psi$ $\exists_\tau, \vee$

$\lambda$

cody
fonte

\forall_{τ}

$\forall_\tau$

\supset

$\supset$

=_{τ} : τ \to τ \to ο

$=_\tau :\tau\rightarrow\tau\rightarrow\omicron$

Quais são esses axiomas inteligentes, por favor? Eu acho que isso tem a ver com fornecer uma maneira de provar a igualdade ... Além disso, você conhece um nome para distinguir explicitamente os níveis de extensões HOL? (com igualdade, depois com tipo polimórfico e depois com tipos dependentes).

precisa saber é o seguinte

@ Hibou57 os axiomas são descritos no excelente artigo As Sete Virtudes da Teoria Simples do Tipo . Não sei se existem nomes explícitos para distinguir diferentes extensões do STT, além daquelas que você usou.

Cody