Très bien. Dans ce cas, je ne vais pas attendre plus longtemps pour donner la réponse à la question 24, qui est de toute façon une question un peu particulière. Je signale tout de suite que dans le point de vue que je développe ici je suis arrivé aux même conclusions que celles qui ont été exposées par Steki-kun concernant Coq. Pour cela j'ai deux arguments, et je vais exposer le premier plus loin.
La réponse est donc ``non'' pour la question 24, c'est à dire ``non en général'', mais pas forcément non dans tous les cas. En effet si a est tout simplement identique à b (disons alpha-equivalent), il est bien clair que W(E[ a/x ]) et W(E[ b/x ]) sont le même type et donc que c est bien un terme de type W(E[ b/x ]). Mais en général la réponse est ``non'', tout simplement parce que les règles de ce système ne donnent aucun moyen d'identifier les deux types. Si on parcourt le fil, on verra que le seul endroit où on énonce une égalité entre types est la règle dite ``Sémantique de Heyting'' qui identifie W(?x:T E) avec (x:T) -> W(E). C'est clairement insuffisant pour pouvoir répondre ``oui'' à la question 24.
Voyons maintenant les deux arguments évoqués plus haut. Le premier est très simple. Si E=F entrainait W(E) = W(F) alors pour tout énoncé E, démontrable (donc égal à vrai par un axiome d'extentionalité que je n'ai pas encore évoqué; I'm sorry !), toute preuve de vrai serait aussi une preuve de E. Comme il existe une preuve triviale de vrai (on l'a vue plus haut), cette preuve triviale serait une preuve de tout énoncé démontrable. En soi, ce n'est sans doute pas contradictoire, mais on voit bien que vérifier que notre preuve triviale de vrai est une preuve de E revient à rechercher une preuve de E, et donc qu'un compilateur devient incapable de vérifier les preuves.
Par ailleurs, le fait d'identifier W(E[ a/x ]) et W(E[ b/x ]) quand a et b ont la même forme normale rend un appréciable service. Cela nous évite d'avoir à écrire des preuves pour le cas où a=b résulte d'un simple calcul. Enorme simplification pour l'utilisation du système. En fait, si on procédait pas ainsi, chaque règle de calcul devrait faire l'objet d'un axiome. En d'autres termes, il faudrait ``Hilbertiser'' le système, ce qui le rendrait beaucoup moins maniable. L'écriture des preuves serait un vrai cauchemar.
L'autre argument vient de la Théorie des Topos. L'exposer requiert pas mal de préliminaires. Il n'est pas exclu que je le fasse, mais sans doute pas dans un post, plutôt dans un document séparé.
Partager