Calcul des constructions

théorie des types créé par Thierry Coquand

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, 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

modifier

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 »).

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

  •   est un terme (également appelé Type)
  •   est un terme (également appelé Prop, le type de toutes les propositions)
  • Si   et   sont des termes, le sont également :
    •  
    • ( )
    • ( )

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

modifier

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

 

qui peut être lue comme l'implication

si les variables   ont pour types  , alors le terme   a pour type  .

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  , et on écrira K pour désigner soit P soit T.


 

signifie que le terme   est une preuve de la proposition   dans le contexte  .

On notera   pour signifier «   a pour type  , et   a pour type   », et   le résultat de la substitution de la variable   par le terme   dans le terme  .

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

 

ce qui signifie

si   est un jugement valide, alors   l'est aussi.

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

modifier

Sorte :  


Variable :  


Abstraction :  


Application :  

Conversion :  

Définir les opérateurs logiques

modifier

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  . Néanmoins, cet opérateur unique est suffisant pour définir tous les autres opérateurs logiques :

 

Définir des types de données

modifier

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

Booléens
 
Entiers naturels
 
Type produit  
 
Union disjointe  
 

Voir aussi

modifier

Articles connexes

modifier

Théoriciens

modifier

Références

modifier

Source de la traduction

modifier