Re: Le web

Au sujet du « faux », ne penses-tu pas que les développeurs OCaml peuvent utiliser le type polymorphe 'a option pour représenter cette notion ? L'idée m'est venue en relisant l'article du programme de Hilbert aux programmes tout court de Jean-Louis Krivine, en particulier ce passage au sujet de la correspondance de Curry-Howard :

Ce sont des logiciens qui l'ont découverte, tout au moins en ce qui concerne la logique intuitionniste. Mais c'est un informaticien, T. Griffin qui a opéré son extension à la logique classique, trente ans après, en 1990. C'est, de nouveau, une découverte capitale et tout à fait inattendue : en effet, le raisonnement par l'absurde est associé à une instruction très sophistiquée du langage SCHEME (une variante de LISP), qui a été inventée pour gérer, entre autres, les exceptions et le multi-tâches.

Or le type 'a option est une manière de gérer les exceptions de manière plus fonctionnelle en OCaml que de lever une exception de type exn. Je m'explique sur l'exemple du calcul du prédécesseur pour les entiers unaires :

type nat = Zero | S of nat
let pred n =
 match n with
 | Zero -> None
 | S n' -> n'

Un entier qui aurait zéro pour successeur est absurde, mais pas pour les autres entiers. Cela se passe comme si lorsque l'hypothèse est absurde on renvoie None, alors que lorsque ce n'est pas le cas on renvoie une conclusion du bon type Some 'a. Ce qui me fait penser à l'interprétation gödelienne de la logique intuitionniste : dans chaque étude de cas, on dispose soit d'une preuve de l'absurdité de l'hypothèse, soit de la prouvabilité du théorème sous l'hypothèse donnée. Cette interprétation te semble-t-elle recevable ? Les leçons de M. Krivine sont trop lointaines pour moi (une dizaine d'années, et déjà à l'époque je n'avais suivi son cours sur le lambda-calcul typé qu'en option) pour que je puisse avancer avec assurance sur ce genre de question.

Autrement, je viens de commencer la lecture de ta thèse et j'apprécie beaucoup ton sens de l'humour :-) En conclusion des remerciements, tu en adresses à Jean-Yves et Jean-Louis, que je suppose être MM. Girard et Krivine. J'aurais aimé me procurer les deux tomes de l'ouvrage Le point aveugle, mais le premier tome est en rupture de stock chez tous les distributeurs que j'ai regardé. Sais tu s'il en est prévu une réédition ?

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.