2) Le -terme

   Dans le Calcul des Construction tout se passe autour de -termes. C'est le nom donné aux définitions est aux preuves. Notre exemple n'y fait pas exception. Voici un mini exemple de développement sur les relations.

Definition Rel := E:Set.EEProp. Definition Inv := E:Set.R:(Rel E).x,y:E.(R y x). Definition Trans :=   E:Set.R:(Rel E).x,y,z:E.(R x y)(R y z)(R x z). Definition InvTrans : E:Set.R:(Rel E).(Trans E R)(Trans E (Inv E R)) =   E:Set.     R:(Rel E).       H:(x,y,z:E.(R x y)(R y z)(R x z)).         x,y,z:E.H0:(R y x).H1:(R z y).(H z y x H1 H0).

   Ceci étant difficilement compréhensible sans une bonne connaissance du -calcul et du Calcul des Constructions, nous allons tenter d'expliquer ces instructions une à une. L'idée générale d'un tel développement est de redéfinir petit à petit sous une forme formelle tout un ensemble de notions mathématiques habituelles. On fait correspondre à chacune de ces notions une constante au nom explicite.

• Ici, nous commençons par définir la constante Rel qui désigne les relations. Cette définition signifie que si E est un ensemble, si x et y sont deux élément de cet ensemble, et si R, est une relation sur cet ensemble, alors le fait que le couple (x,y) appartienne à la relation R, ou que x et y, (dans cet ordre) soient en relation par R, se note (R x y).
• Nous définissons ensuite par la constante Inv ce qu'est l'inverse d'une relation. Tout simplement, le couple (x,y) appartient à la l'inverse de R, ce que l'on note (Inv E R x y), si et seulement si le couple (y,x) appartient à R.
• La constante Trans représente la transitivité. Elle s'applique à un ensemble E et une relation R sur cet ensemble. Cette relation R est dite transitive si et seulement si pour tout triplet d'éléments x, y et z tel que (R x y) et (R y z), on a (R x z)
• La constante InvTrans représente une preuve. C'est la preuve que l'inverse d'une relation transitive est elle-même transitive. Cela peut sembler étonnant de définir une preuve de la sorte, mais l'intérêt du Calcul des Constructions est justement de pouvoir représenter des preuves et de vérifier leur validité

   Les quelques lignes précédentes avaient pour but de définir cette preuve. Le système a maintenant vérifié qu'elle ne comporte aucune erreur. Nous nous avons maintenant la certitude que l'inverse d'une fonction transitive est transitive. Cependant, nous n'avons aucun document compréhensible pour en expliquer la raison. C'est ici que mon travail de thèse intervient. Il consiste à écrire un programme qui traduise ces quelques lignes en français. Je vais ici tacher de vous monter de quelle façon il procède. (Suite)

Yann Coscoy