Wystarczy wpisać rachunek lambda i logikę wyższego rzędu

Jaki jest związek między prostym typem rachunku lambda a logiką wyższego rzędu?

Pod Curry-Howardem wydaje się, że prosty typ rachunku lambda odpowiada logice zdań. Jak to się ma do logiki wyższego rzędu? Według tego poradnika Geuversa: http://typessummerschool07.cs.unibo.it/courses/geuvers-1.pdf językiem HOL wydaje się być STT. Czy nie powinno to być PROP? Co to znaczy?

Czy Church miał na myśli HOL, gdy zdefiniowano STT?

lo.logic typed-lambda-calculus curry-howard

— lambda2
źródło

Tak, Kościół miał na myśli HOL. Sztuką na uzyskanie HOL z STT jest użycie równości , oprócz aplikacji funkcji i abstrakcji funkcji. Następnie możesz napisać

jako

, między innymi. Podoba mi się „Siedem cnót teorii prostych typów” jako wprowadzenie do STT, które odpowiada na tego rodzaju pytania. Może powinienem napisać odpowiedź ...

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

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

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

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

— Thomas Klimpel

Kiedy mówimy o Curry-Howardzie, jaka byłaby poprawna logika odpowiadająca STT? HOL czy PROP?

— lambda2

W odniesieniu do Curry-Howarda, nie sądzę, że będzie to HOL. Być może jest to multiplikatywny fragment intuicyjnego PROP, tj. Intuicyjnego PROP bez „lub”. Ale to dotyczyło CCC (kartezjańska kategoria zamknięta) i jestem teraz trochę zmęczony. Lambda będzie prawdopodobnie tłumaczona jako „implikacja”, która była „wykładniczą” w CCC. „Produktem” z CCC było „i”, więc do tego potrzebna byłaby „para” w STT. A „lub” byłoby wówczas typem „sumy” w STT, tj. Rozłącznym związkiem, może i jeśli „a”, to „b”, inaczej „c” to zrobi.

— Thomas Klimpel

Myślę, że coś mylę (lub wszystko). Jeśli STT ~ = PROP (przez Curry-Howard), a STT jest również HOL, to mogę użyć PROP w pewnym sensie, aby mieć HOL?

— lambda2

@ThomasKlimpel: powinieneś zamienić swoje komentarze w odpowiedź.

— cody

Różnica jest następująca: jeśli STLC jest traktowane jako prymitywny język na poziomie konstruktorów sumujących, a niewielka liczba aksjomatów jest wystarczająca, aby dać ci pełną moc ekspresyjną 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
źródło

\forall_{τ}

$\forall_\tau$

\supset

$\supset$

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

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

Jakie są te sprytne aksjomaty? Wydaje mi się, że ma to związek z zapewnieniem sposobu na udowodnienie równości… Czy znasz też nazwę, która wyraźnie rozróżnia poziomy rozszerzeń HOL? (z równością, następnie z typem polimorficznym, następnie z typami zależnymi).

— Hibou57

@ Hibou57 aksjomaty zostały przedstawione w doskonałym artykule Siedem cnót teorii prostych typów . Nie wiem, czy istnieją wyraźne nazwy odróżniające różne rozszerzenia STT, inne niż te, których użyłeś.

— cody