Calcul des constructions

Un article de Wikipédia, l'encyclopédie libre.

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 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 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 à l'aide de leur fonction de destruction.

[modifier] 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 »).

[modifier] Termes

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

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

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

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

[modifier] 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 $Γ$ 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. 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.

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

${{} \over {} \vdash P : T}$
${\Gamma \vdash A : K \over {\Gamma, x:A \vdash x : A}}$
${\Gamma, x:A \vdash t : B : K \over {\Gamma \vdash (\lambda x:A . t) : (\forall x:A . B) : K}}$
${\Gamma \vdash M : (\forall x:A . B)\qquad\qquad\Gamma \vdash N : A \over {\Gamma \vdash M N : B(x := N)}}$

[modifier] Définir les opérateurs logique

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:P . (A \Rightarrow B \Rightarrow C) \Rightarrow C & \\ A \vee B & \equiv & \forall C:P . (A \Rightarrow C) \Rightarrow (B \Rightarrow C) \Rightarrow C & \\ \neg A & \equiv & \forall C:P . (A \Rightarrow C) & \\ \exists x:A.B & \equiv & \forall C:P . (\forall x:A.(B \Rightarrow C)) \Rightarrow C & \end{matrix}$

[modifier] Définir des types de données

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

Booléens: $\forall A: P . A \Rightarrow A \Rightarrow A$
Entiers naturels: $\forall A:P . (A \Rightarrow A) \Rightarrow (A \Rightarrow A)$
Type produit $A \times B$: $A \wedge B$
Union disjointe $A + B$: $A \vee B$

[modifier] Voir aussi

[modifier] Articles connexes

[modifier] Théoriciens

Thierry Coquand
Jean-Yves Girard

[modifier] 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).