Calcul des constructions

Le calcul des constructions (CoC de l'anglais calculus of constructions) est un lambda-calcul typé d'ordre supérieur dans lequel les types sont des valeurs de première classe. Il est par conséquent possible, dans le CoC, de définir des fonctions qui vont des entiers vers les entiers, mais aussi des entiers vers les types, des types vers les entiers ou des types vers les types.

Le CoC est fortement normalisant, bien que, d'après le théorème d'incomplétude de Gödel, il soit impossible de démontrer cette propriété dans le CoC lui-même, puisqu'elle implique sa cohérence.

Le CoC a été développé initialement par Thierry Coquand.

Le CoC a été à l'origine des premières versions de l'assistant de preuves Coq. Les versions suivantes, ainsi que dans l'assistant de preuve Lean, ont été construites à partir du calcul des constructions inductives qui est une extension du CoC qui intègre des types de données inductives. Dans le CoC originel, les types de données inductives devaient être émulés via un catamorphisme polymorphe (comme dans les entiers de Church).

La façon de définir le calcul des constructions par trois types de dépendances est appelée le lambda cube et est due à Henk Barendregt.

Bases du calcul des constructions

Le calcul des constructions peut être considéré comme une extension de la correspondance de Curry-Howard. Cette dernière associe chaque terme du lambda-calcul simplement typé à une preuve en déduction naturelle dans la logique propositionnelle intuitionniste, et réciproquement. Le calcul des constructions étend cet isomorphisme aux preuves dans le calcul des prédicats intuitionniste dans son ensemble, ce qui inclut par conséquent des preuves de formules quantifiées (que l'on appellera également « propositions »).

Termes

Un terme du calcul des constructions est construit à l'aide des règles suivantes :

• $\mathbb {T}$ est un terme (également appelé Type)
• $\mathbb {P}$ est un terme (également appelé Prop, le type de toutes les propositions)
• Si $A$ et $B$ sont des termes, le sont également :
  • $\mathbf {(} AB)$
  • ($\mathbf {\lambda } x:A.B$)
  • ($\forall x:A.B$)

Le calcul des constructions possède cinq types d'objets :

1. les preuves, qui sont des termes dont les types sont des propositions ;
2. les propositions, qui sont aussi appelées petits types ;
3. les prédicats, qui sont des fonctions qui retournent des propositions ;
4. les types larges, qui sont des types de prédicats (par exemple P est un type large) ;
5. T lui-même, qui est le type des types larges.

Jugements

Dans le calcul des constructions, un jugement est une inférence de typage :

$x_{1}:A_{1},x_{2}:A_{2},\ldots \vdash t:B$

qui peut être lue comme l'implication

si les variables $x_{1},x_{2},\ldots$ ont pour types $A_{1},A_{2},\ldots$, alors le terme $t$ a pour type $B$.

Les jugements valides pour le calcul des constructions sont dérivables à partir d'un ensemble de règle d'inférences. Dans la suite, on utilisera $\Gamma$ pour signifier une suite d'associations de type $x_{1}:A_{1},x_{2}:A_{2},\ldots$, et on écrira K pour désigner soit P soit T.

${\Gamma \vdash A:P}$

signifie que le terme $A$ est une preuve de la proposition $P$ dans le contexte $\Gamma$.

On notera $A:B:C$ pour signifier « $A$ a pour type $B$, et $B$ a pour type $C$ », et $B(x:=N)$ le résultat de la substitution de la variable $x$ par le terme $N$ dans le terme $B$.

Une règle d'inférence est écrite sous la forme

${\Gamma \vdash A:B} \over {\Gamma '\vdash C:D}$

ce qui signifie

si $\Gamma \vdash A:B$ est un jugement valide, alors $\Gamma '\vdash C:D$ l'est aussi.

Règles d'inférence du calcul des constructions

Sorte : ${{} \over {}\Gamma \vdash \mathbb {P} :\mathbb {T} }$

Variable : ${\Gamma \vdash A:K \over {\Gamma ,x:A\vdash x:K}}$

Abstraction : ${\Gamma ,x:A\vdash t:B:K \over {\Gamma \vdash (\lambda x:A.t):(\forall x:A.B):K}}$

Application : ${\Gamma \vdash M:(\forall x:A.B)\qquad \qquad \Gamma \vdash N:A \over {\Gamma \vdash MN:B(x:=N)}}$

Conversion : ${\Gamma \vdash M:A\qquad \qquad A=_{\beta }B\qquad \qquad \Gamma \vdash B:K \over {\Gamma \vdash M:B}}$

Définir les opérateurs logiques

Le calcul des constructions est très parcimonieux quand on considère uniquement ses opérateurs de base : le seul opérateur logique pour former les propositions est $\forall$. Néanmoins, cet opérateur unique est suffisant pour définir tous les autres opérateurs logiques :

${\begin{matrix}A\Rightarrow B&\equiv &\forall x:A.B&(x\notin B)\\A\wedge B&\equiv &\forall C:\mathbb {P} .(A\Rightarrow B\Rightarrow C)\Rightarrow C&\\A\vee B&\equiv &\forall C:\mathbb {P} .(A\Rightarrow C)\Rightarrow (B\Rightarrow C)\Rightarrow C&\\\neg A&\equiv &\forall C:\mathbb {P} .(A\Rightarrow C)&\\\exists x:A.B&\equiv &\forall C:\mathbb {P} .(\forall x:A.(B\Rightarrow C))\Rightarrow C&\end{matrix}}$

Définir des types de données

Les types de données de base utilisés en informatique peuvent être définis dans le calcul des constructions :

Booléens

$\forall A:\mathbb {P} .A\Rightarrow A\Rightarrow A$

Entiers naturels

$\forall A:\mathbb {P} .(A\Rightarrow A)\Rightarrow (A\Rightarrow A)$

Type produit $A\times B$

$A\wedge B$

Union disjointe $A+B$

$A\vee B$

Voir aussi

Articles connexes

• Correspondance de Curry-Howard
• Logique intuitionniste
• Théorie des types
• Lambda-calcul
• Système F

Théoriciens

• Thierry Coquand
• Jean-Yves Girard
• Henk Barendregt

Références

• (en) Thierry Coquand et Gerard Huet, « The Calculus of Constructions ». Information and Computation, vol. 76, n^o  2-3 (1988).
• (en) Pour une source accessible librement, voir Coquand et Huet, « The calculus of constructions ». Rapport technique 530, INRIA, Centre de Rocquencourt (1986).
• (en) M. W. Bunder et Jonathan P. Seldin, « Variants of the Basic Calculus of Constructions » (2004).

Source de la traduction

• (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Calculus of constructions » (voir la liste des auteurs).