Re: Reason

J'ai hésité avant de te répondre pour plusieurs raisons. Tout d'abord il y a des questions d'ordre historique sur lesquelles je ne sais pas tout, ensuite je craignais de faire encore une réponse à rallonge assez rebutante, et enfin je n'ai pas compris ta dernière question sur les littéraux. Je vais essayer de répondre comme je le peux, sans faire trop long.

Sur le plan historique, les paradoxes de Burali-Forti et Russell dans la théorie des ensembles de Cantor-Frege ont donné naissance à l'axiomatique de Zermelo-Fraenkel. C'est plutôt dans ce cadre axiomatique (avec quelques variantes) que l'on pratique de nos jours la théorie des ensembles.

De leur côté, Russel et Withehead écrivirent les Principia Mathematica pour tenter de fonder l'édifice mathématique sur la seule logique. C'est leur notation utilisée pour les fonctions propositionnelles qui inspira Church pour son lambda-calcul. Ils notaient la proposition f appliquée à un objet singulier a : fa, et la fonction qui à un objet a indéterminé faisait correspondre la valeur de vérité fa ainsi : fâ. Ils avaient aussi une notation du type : âfa. Comme l'éditeur de Church ne pouvait pas mettre d'accents circonflexes sur toutes les lettres, ils ont remplacer l'accent circonflexe par un lambda majuscule qui est ensuite devenu un lambda minuscule. Et l'on note depuis la fonction x -> f x ainsi : \lambda x.fx.

La théorie des catégories fut introduite originellement dans le cadre de la topologie algébrique. Elle avait pour but d'étudier les relations entres structures mathématiques qui préservent certaines propriétés des dites structures : les morphismes. Ce n'est qu'ensuite qu'un lien a été fait avec la logique et la sémantique des langages de programmation.

En ce qui concerne le lien entre typage et logique, cela concerne la théorie de la démonstration. Il y a un bon ouvrage de vulgarisation sur la logique : La logique ou l'art de raisonner qui expose simplement les différents point de vue sur la logique. Le plan de l'ouvrage est en quatre parties :

• Formaliser : des objets aux énoncés
• Interpréter : des énoncés aux objets
• Prouver : des énoncés aux énoncés
• Axiomatiser : des objets aux ensembles

La notion de vérité relève de la seconde partie, celle sur l'interprétation, et fait intervenir la notion de modèles dont s'occupe la théorie des modèles. Pour prendre un exemple simple. Si on prend un langage qui dispose d'une fonction binaire (disons +) et de deux constantes I et II. Alors si on interprète l'énoncé II + II = I dans l'ensemble N des entiers naturels, munis de son addition et en associant 1 à I et II à 2, alors cet énoncé sera faux. En revanche si on fait de même dans le groupe Z/3Z alors il sera vrai. Dans cette branche de la logique, on développe la notion de modèle d'une théorie et celle de conséquence sémantique : si un énoncé est vrai dans tout modèle d'une théorie alors on dit qu'il est une conséquence sémantique de la théorie. Dans l'ouvrage sus-cité, ils écrivent une des choses les plus importante à comprendre : « [...] quand il existe une structure naturelle pour interpréter les énoncés (par exemple N dans le cas des énoncés arithmétiques), il est nécessaire d'envisager toutes les autres, même celles qui semblent n'avoir aucun rapport intuitif avec les énoncés. C'est en faisant varier les interprétations possibles, et en constatant que certaines notions ne sont pas sensibles à ces variations, que l'on touche à l'essence de la logique ». (Tu pourras penser, par exemple, à mon journal sur l'interprétation avec la méthode tagless final où je faisais plusieurs interprétations pour un même terme syntaxique).

De son côté la théorie de la démonstration avec ses formalismes comme la déduction naturelle ou le calcul des séquents de Gentzen, ou les systèmes à la Hilbert, ne s'occupe pas du rapport que les énoncés entretiennent avec des objets (modèles) mais seulement du rapport que les jugements (ou énoncés) entretiennent entre eux. Son cheval de bataille, c'est l'inférence : à quelles conditions peut-on inférer une conclusion donnée de prémisses données ? On obtient alors la notion de conséquence déductive : un énoncé est une conséquence déductive d'une théorie si on peut l'établir comme conclusion d'une preuve dont les prémisses sont toutes des axiomes de la théorie. Les deux questions qui se posent alors sont :

• si un énoncé est conséquence déductive est-il aussi conséquence sémantique ?
• réciproquement, s'il est conséquence sémantique est-il conséquence déductive ?

La première a trait à la cohérence du système (on ne peut pas trouver tout et n'importe quoi avec) et la seconde a trait à sa complétude (il peut prouver tout ce qui est prouvable) qui renvoie à un théorème fameux de Gödel (moins connus que son théorème d'incomplétude, mais tout aussi important).

C'est cette deuxième branche de la logique qui est en lien avec le typage des langages de programmations, elle donne lieu à la correspondance de Curry-Howard ou correspondance preuve-programme : le type d'un programme est une énoncé dont le programme est une preuve. Ce qui apporte de la sécurité dans l'écriture de code, comme le montre le chapitre sur les systèmes de type du livre de Benjamin C. Pierce : well typed programm never gets stuck, autrement dit un programme bien typé ne se retrouvera jamais dans un état indéfini où aucune transition n'est possible. Puis, selon la richesse d'expressivité du système de type, il permet d'exprimer au mieux la sémantique du code : il limite les interprétations possibles, via la complétude.

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