3) Une première tentative

   Notre première tentative de traduction est une simple verbalisation. Chaque opérateur du formalisme est traduit par une phrase « explicative » en français. Nous allons voir immédiatement l'insuffisance de cette approche.

Théorème InvTrans. Énoncé : E:Set.R:(Rel E).(Trans E R)(Trans E (Inv E R)). Preuve : Considérons un terme E quelconque de type Set.   Considérons un terme R quelconque de type (Rel E).     Considérons un terme H quelconque de type (Trans R E).       Considérons un terme x quelconque de type E.         Considérons un terme y quelconque de type E.           Considérons un terme z quelconque de type E.             Considérons un terme H1 quelconque de type (Inv E R x y).               Considérons un terme H2 quelconque de type (Inv E R y z).                             * Le terme H nous avons (Trans E R).                             * Le terme z a le type E.                           * Par application nous obtenons un terme de type y0:E.z0:E.(R z y0)(R y0 z0)(R z z0).                           * Le terme y a le type E.                       * Par application nous obtenons un terme de type z0:E.(R z y)(R y z0)(R z z0).                       * Le terme x a le type E.                     * Par application nous obtenons un terme de type (R z y)(R y x)(R z x).                     * Le terme H2 a le type (Inv E R y z).                   * Par application nous obtenons un terme de type (R y x)(R z x).                   * Le terme H1 a le type (Inv E R x y).                 Par application nous obtenons un terme de type (R z x).               Nous avons construit un terme de type (Inv E R y z)(R z x).             Nous avons construit un terme de type (Inv E R x y)(Inv E R y z)(R z x).           Nous avons construit un terme de type z:E.(Inv E R x y)(Inv E R y z)(R z x).         Nous avons construit un terme de type y:E.z:E.(Inv E R x y)(Inv E R y z)(R z x).       Nous avons construit un terme de type x:E.y:E.z:E.(Inv E R x y)(Inv E R y z)(R z x).     Nous avons construit un terme de type (Trans E R)x:E.y:E.z:E.(Inv E R x y)(Inv E R y z)(R z x).   Nous avons construit un terme de type R:(Rel E).(Trans E R)x:E.y:E.z:E.(Inv E R x y)(Inv E R y z)(R z x). Nous avons construit un terme de type E:Set.R:(Rel E).(Trans E R)x:E.y:E.z:E.(Inv E R x y)(Inv E R y z)(R z x). Qed.

   C'est en français, mais cela n'est pas plus compréhensible pour autant. Un gros problème est bien sûr que cela prend une place énorme pour pour une petite preuve rien du tout, mais il y a plus urgent. Ce qui rend ce texte totalement incompréhensible est que l'on ne sait pas de quoi on parle. Il faut être un expert du Calcul des Constructions pour comprendre que E est ensemble, R une relation et que H représente l'hypothèse qui affirme que R est transitive. Cette ambiguïté n'est qu'apparente. Pour donné une idée, nous pouvons dire qu'elle est due à une spécificité du Calcul des Constructions qui permet représenter de façon identique des objets très différents comme des ensembles, des fonctions, des assertions, des preuves etc... (cf Isomorphisme de Curry-Howard)

   Voyons ce que l'on obtient une fois cette ambiguïté résolue. (Suite)

Retour

Sommaire

Suite

Yann Coscoy