Comment obtenez-vous le calcul des constructions à partir des autres points du Lambda Cube?

Le CoC serait le point culminant des trois dimensions du Lambda Cube. Cela ne m’apparaît pas du tout. Je pense que je comprends les dimensions individuelles, et la combinaison de deux semble entraîner une union relativement simple (peut-être que je manque quelque chose?). Mais quand je regarde le CoC, au lieu de ressembler à une combinaison des trois, cela ressemble à une chose complètement différente. De quelle dimension les types Type, Prop et petits / grands proviennent-ils? Où les produits dépendants ont-ils disparu? Et pourquoi l'accent est-il mis sur les propositions et les preuves plutôt que sur les types et les programmes? Y a-t-il quelque chose d'équivalent qui se concentre sur les types et les programmes?

Edit: Au cas où ce ne serait pas clair, je demande une explication sur la façon dont le CoC est équivalent à l'union simple des dimensions du Lambda Cube. Et y a-t-il une union réelle des trois là où je peux étudier (c'est-à-dire en termes de programmes et de types, pas de preuves et de propositions)? C'est en réponse aux commentaires sur la question, et non aux réponses actuelles.

Tout d'abord, pour réitérer l'un des points de cody, le calcul des constructions inductives (sur lequel le noyau de Coq est basé) est très différent du calcul des constructions. Il est préférable de commencer par la théorie des types de Martin-Löf avec des univers, puis d'ajouter un tri Prop au bas de la hiérarchie des types. Il s'agit d'une bête très différente du CoC d'origine, qui est mieux considérée comme une version dépendante du F-oméga. (Par exemple, CiC a des modèles de théorie des ensembles et pas le CoC.)

Cela dit, le lambda-cube (dont le CoC est membre) est généralement présenté comme un système de type pur pour des raisons d'économie dans le nombre de règles de typage. En traitant les tris, les types et les termes comme des éléments de la même catégorie syntaxique, vous pouvez écrire beaucoup moins de règles et vos preuves deviennent également un peu moins redondantes.

Cependant, pour la compréhension, il peut être utile de séparer explicitement les différentes catégories. Nous pouvons introduire trois catégories syntaxiques, les types ( classés par la métavariable k), les types (classés par la métavariable A) et les termes (classés par la métavariable e). Les huit systèmes peuvent alors être considérés comme des variations de ce qui est autorisé à chacun des trois niveaux.

λ → (calcul lambda simplement tapé)

 k ::= ∗
 A ::= p | A → B
 e ::= x | λx:A.e | e e

Il s'agit du calcul lambda typé de base. Il existe un seul type ∗, qui est le type de types. Les types eux-mêmes sont des types atomiques pet des types de fonction A → B. Les termes sont des variables, des abstractions ou des applications.

λω_ (STLC + opérateurs de type supérieur)

 k ::= ∗ | k → k
 A ::= a | p | A → B | λa:k.A | A B
 e ::= x | λx:A.e | e e

Le STLC n'autorise l'abstraction qu'au niveau des termes. Si nous l'ajoutons au niveau des types, nous ajoutons un nouveau type k → kqui est le type des fonctions au niveau du type, ainsi que l'abstraction λa:k.Aet l'application A Bau niveau du type. Alors maintenant, nous n'avons pas de polymorphisme, mais nous avons des opérateurs de type.

Si la mémoire est bonne, ce système n'a pas plus de puissance de calcul que le STLC; il vous donne simplement la possibilité d'abréger les types.

λ2 (système F)

 k ::= ∗
 A ::= a | p | A → B  | ∀a:k. A 
 e ::= x | λx:A.e | e e | Λa:k. e | e [A]

Au lieu d'ajouter des opérateurs de type, nous aurions pu ajouter du polymorphisme. Au niveau du type, nous ajoutons ∀a:k. Aqui est un formateur de type polymorphe, et au niveau du terme, nous ajoutons l'abstraction sur les types Λa:k. eet l'application de type e [A].

Ce système est beaucoup plus puissant que le STLC - il est aussi fort que l'arithmétique de second ordre.

λω (Système F-oméga)

 k ::= ∗ | k → k 
 A ::= a | p | A → B  | ∀a:k. A | λa:k.A | A B
 e ::= x | λx:A.e | e e | Λa:k. e | e [A]

Si nous avons à la fois des opérateurs de type et du polymorphisme, nous obtenons F-oméga. Ce système est plus ou moins la théorie du type de noyau de la plupart des langages fonctionnels modernes (comme ML et Haskell). Il est également beaucoup plus puissant que le système F - il est équivalent en force à l'arithmétique d'ordre supérieur.

λP (LF)

 k ::= ∗ | Πx:A. k 
 A ::= a | p | Πx:A. B | Λx:A.B | A [e]
 e ::= x | λx:A.e | e e

Au lieu du polymorphisme, nous aurions pu aller dans le sens de la dépendance à partir du calcul lambda simplement typé. Si vous avez autorisé le type de fonction à laisser son argument être utilisé dans le type de retour (c'est-à-dire, écrire Πx:A. B(x)au lieu de A → B), alors vous obtenez λP. Pour rendre cela vraiment utile, nous devons étendre l'ensemble des types avec une sorte d'opérateurs de type qui prennent les termes en arguments Πx:A. k, et nous devons donc également ajouter une abstraction Λx:A.Bet une application correspondantes A [e]au niveau du type.

Ce système est parfois appelé LF, ou le cadre logique d'Édimbourg.

Il a la même puissance de calcul que le calcul lambda simplement tapé.

λP2 (pas de nom spécial)

 k ::= ∗ | Πx:A. k 
 A ::= a | p | Πx:A. B | ∀a:k.A | Λx:A.B | A [e]
 e ::= x | λx:A.e | e e | Λa:k. e | e [A]

Nous pouvons également ajouter du polymorphisme à λP, pour obtenir λP2. Ce système n'est pas souvent utilisé, il n'a donc pas de nom particulier. (Le seul article que j'ai lu qui l'utilise est l' induction d' Herman Geuvers n'est pas dérivable dans la théorie des types dépendants du second ordre .)

Ce système a la même force que le système F.

λPω_ (pas de nom spécial)

 k ::= ∗ | Πx:A. k | Πa:k. k'
 A ::= a | p | Πx:A. B | Λx:A.B | A [e] | λa:k.A | A B 
 e ::= x | λx:A.e | e e 

Nous pourrions également ajouter des opérateurs de type à λP, pour obtenir λPω_. Cela implique l'ajout d'un type Πa:k. k'pour les opérateurs de type, ainsi que l'abstraction Λx:A.Bet l'application correspondantes au niveau du type A [e].

Puisqu'il n'y a à nouveau aucun saut dans la puissance de calcul par rapport au STLC, ce système devrait également constituer une base fine pour un cadre logique, mais personne ne l'a fait.

λPω (le calcul des constructions)

 k ::= ∗ | Πx:A. k | Πa:k. k'
 A ::= a | p | Πx:A. B | ∀a:k.A | Λx:A.B | A [e] | λa:k.A | A B 
 e ::= x | λx:A.e | e e | Λa:k. e | e [A]

Enfin, nous arrivons à λPω, le calcul des constructions, en prenant λPω_ et en ajoutant un ancien de type polymorphe ∀a:k.Aet une abstraction au niveau du terme Λa:k. eet une application e [A]pour celui-ci.

Les types de ce système sont beaucoup plus expressifs que dans le F-oméga, mais il a la même force de calcul.

$\lambda$

Mais d'abord, il faut probablement essayer de dissocier les différents problèmes. Le prouveur de théorème interactif Coq est basé sur une théorie de type sous-jacente, parfois appelée avec amour le calcul des constructions inductives avec des univers . Vous remarquerez qu'il s'agit plus d'une bouchée que simplement du "calcul des constructions", et en effet, il y a beaucoup plus de choses là-dedans que le CoC. En particulier, je pense que vous ne savez pas exactement quelles fonctionnalités sont dans CoC proprement dit. En particulier, la distinction Set / Prop et les univers n'apparaissent pas dans CoC.

Je ne donnerai pas ici un aperçu complet des systèmes de type pur, mais la règle importante (pour les PTS fonctionnels comme le CoC) est la suivante

$$\frac{\Gamma\vdash A:s\qquad \Gamma,x:A\vdash B:k}{\Gamma\vdash \Pi x:A.B\ :\ k}\ (s,k)\in R$$

$s,k$$S$$(s,k)$$R$$S$

$S$$R$$\Pi x:A.B$

$S$

$$\{*, \square\}$$ $$R=\{(*,*),(\square,\square),(\square,*),(*,\square)\}$$

Et donc nous avons 4 règles qui correspondent à 4 objectifs différents:

• $(*,*)$

• $(\square,\square)$

• $(\square,*)$

• $(*,\square)$

Je vais expliquer chacun de ces éléments plus en détail.

---

$A\rightarrow B$$\Pi x:A.B$$x$$B$

$*$$\mathrm{nat}$$\mathrm{bool}$$x=y$$x$$y$$*$

$\mathrm{list}$$\mathrm{list}:*\rightarrow *$$\mathrm{list}_{\mathrm{nat}}, \mathrm{list}_{\mathrm{bool}}$$*\rightarrow *$$(\square,\square)$

$$\Pi t:*.\ t\rightarrow t$$ $\lambda (t:*)(x:t).x$$\Pi t:*.\_$$(\square, *)$$t\rightarrow t$$(*,*)$

$$A\wedge B := \Pi t:*.\ (A \rightarrow B\rightarrow t)\rightarrow t$$ $$A\vee B := \Pi t:*.\ (A \rightarrow t)\rightarrow(B\rightarrow t)\rightarrow t$$ $$\bot := \Pi t:*.\ t$$ $$\top := \Pi t:*.\ t\rightarrow t$$ $$\exists x:A.\ P(x):= \Pi t:*.\ (\Pi y: A.\ P(y)\rightarrow t)\rightarrow t$$ $(*,\square)$

$*$$*$$(\square, *)$

$(\square,\square)$

$$\Pi c:*\rightarrow *.\ \ c\ \mathrm{nat}\rightarrow c\ \mathrm{nat}$$

$0=1$

$$=\ :\ \mathrm{nat}\rightarrow\mathrm{nat}\rightarrow *$$ $$=\ :\ \Pi t:*.\ t\rightarrow t\rightarrow *$$ $\mathrm{nat}\rightarrow\mathrm{nat}\rightarrow *$$(*,\square)$

$\square \rightarrow \square$$\square$ $\square$$\square_i$$i=1,2,3,\ldots$$\square_i:\square_{i+1}$

$(\square_i, \square_i)$

$$\frac{\Gamma\vdash A:\square_i}{\Gamma\vdash A:\square_j}\ i\leq j$$

Avec ces sortes et règles supplémentaires, vous obtenez quelque chose qui n'est pas un PTS, mais quelque chose de proche. C'est (presque) le calcul étendu des constructions , qui est plus proche de la base de Coq. La grande pièce manquante ici est les types inductifs, dont je ne parlerai pas ici.

Edit: Il y a une référence plutôt sympa qui décrit les différentes fonctionnalités des langages de programmation dans le cadre des PTS, en décrivant un PTS qui est un bon candidat pour une représentation intermédiaire d'un langage de programmation fonctionnel:

Henk: A Typed Intermediate Language , SP Jones et E. Meijer.