Ce chapitre sort explicitement du programme officiel de l’option informatique de MP : la correspondance de Curry-Howard n’y figure pas, et rien de ce qui suit ne peut être exigé à une épreuve. On le propose néanmoins en complément de culture, parce qu’il relie d’un coup deux pans du cours qui, jusqu’ici, semblaient sans rapport : la logique formelle étudiée aux chapitres Règles de déduction et Preuves formelles, et la programmation fonctionnelle en OCaml pratiquée depuis le début de l’année. L’observation, due au logicien Haskell Curry dans les années 1930 puis précisée par William Howard dans une note de 1969 restée longtemps informelle, est qu’une preuve en déduction naturelle et un programme fonctionnel bien typé partagent, du point de vue de leur structure, un seul et même squelette. On la résume par le slogan « les preuves sont des programmes, les formules sont des types ».
Ce que ce chapitre présente est une analogie structurale forte et féconde, pas un théorème que l’on démontre : on ne construira pas de lambda-calcul simplement typé en toute rigueur (grammaire, jugement de typage, règles de réduction), et on ne prouvera aucun isomorphisme en général. L’objectif est plus modeste et plus concret : reprendre des déductions déjà construites, et montrer, sur ces exemples, qu’un terme OCaml explicite en est une transcription littérale.
Ce chapitre est un chapitre de culture, entièrement hors-programme. Il ne sera jamais évalué en tant que tel ; il est là pour éclairer rétrospectivement les chapitres Règles de déduction et Preuves formelles à la lumière de ce que vous savez déjà faire en OCaml.
Avant de détailler chaque connecteur logique sur un exemple, il est utile de fixer d’emblée le vocabulaire général de la correspondance sous la forme d’un tableau : à chaque notion logique répond une notion de typage, et réciproquement.
La correspondance se lit comme un dictionnaire terme à terme entre les objets de la logique propositionnelle et ceux de la programmation fonctionnelle :
| Logique | Programmation (OCaml) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| proposition A | type a | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| preuve de A | programme de type a | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| implication A→B | type fonction a -> b | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| introduction de → | abstraction fun x -> ... | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| élimination de → (modus ponens) | application f x | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| conjonction A∧B | type produit a * b | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| introduction de ∧ | couple (x, y) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| élimination de ∧ | projections fst, snd | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| disjonction A∨B | type somme Gauche of a \| Droite of b | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| introduction de ∨ | constructeurs Gauche, Droite | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| élimination de ∨ | filtrage par motif (match ... with) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Les quatre premières lignes fixent le vocabulaire : une proposition devient un type, et une preuve de cette proposition devient un programme de ce type. Les lignes suivantes détaillent, connecteur par connecteur, comment les règles vues au chapitre Règles de déduction se retrouvent dans la syntaxe d’OCaml ; les trois sous-sections suivantes développent chacune de ces lignes sur un exemple complet.
Encore 14 blocs dans ce document. Le reste du programme est écrit de la même main, avec les figures interactives et votre progression.