Calcul lambda simplement tapé et logique d'ordre supérieur

Quelle est la relation entre le calcul lambda simplement typé et la logique d'ordre supérieur?

Sous Curry-Howard, il semble que le calcul lambda simplement typé correspond à la logique propositionnelle. Comment est-il lié à une logique d'ordre supérieur? Selon ce tutoriel de Geuvers: http://typessummerschool07.cs.unibo.it/courses/geuvers-1.pdf la langue de HOL semble être STT. Cela ne devrait-il pas être PROP? Qu'est-ce que ça veut dire?

L'Église avait-elle en tête HOL lorsqu'elle a défini STT?

lo.logic typed-lambda-calculus curry-howard lambda2
la source

Oui, Church avait en tête HOL. L'astuce pour obtenir HOL à partir de STT consiste à utiliser l' égalité , en plus de l'application de fonction et de l'abstraction de fonction. Ensuite, vous pouvez écrire

comme

, entre autres. J'aime "Les sept vertus de la théorie des types simples" comme introduction à STT, qui répond à ce genre de questions. Je devrais peut-être écrire une réponse ...

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

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

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

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

Thomas Klimpel

Donc, quand on parle de Curry-Howard, quelle serait la logique correcte équivalente à STT? HOL ou PROP?

lambda2

En ce qui concerne Curry-Howard, il ne pense pas que ce sera HOL. C'est peut-être le fragment multiplicatif de PROP intuitionniste, c'est-à-dire PROP intuitionniste sans "ou". Mais c'était pour CCC (catégorie fermée cartésienne), et je suis un peu fatigué pour le moment. Lambda sera probablement traduit par «implication», qui était «exponentielle» dans CCC. Le "produit" de CCC était "et", vous auriez donc besoin d'une "paire" en STT pour cela. Et "ou" serait alors un type "somme" dans STT, c'est-à-dire une union disjointe, peut-être un si "a" puis "b" sinon "c" fait cela.

Thomas Klimpel

Je pense que je confond quelque chose (ou tout). Si STT ~ = PROP (via Curry-Howard), et STT est également HOL, alors je peux utiliser PROP dans un certain sens pour avoir HOL?

lambda2

@ThomasKlimpel: vous devriez transformer vos commentaires en réponse.

cody

Réponses:

La distinction est la suivante: si STLC est considéré comme un langage primitif au niveau du type, ajouter des constructeurs et un petit nombre d'axiomes est suffisant pour vous donner toute la puissance expressive de 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
la source

\forall_{τ}

$\forall_\tau$

\supset

$\supset$

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

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

Quels sont ces axiomes intelligents, s'il vous plaît? Je suppose que cela a à voir avec la fourniture d'un moyen de prouver l'égalité… Connaissez-vous également un nom pour distinguer explicitement les niveaux des extensions HOL? (avec égalité, puis avec type polymorphe, puis avec types dépendants).

Hibou57

@ Hibou57 les axiomes sont décrits dans l'excellent article Les sept vertus de la théorie des types simples . Je ne sais pas qu'il existe des noms explicites pour distinguer différentes extensions de STT, autres que celles que vous avez utilisées.

cody