Probleme – Curry--Howard : une preuve est un programme

1. Les huit règles, en huit fonctions. Tout ce qui suit a été compilé et exécuté.

type vide = |                          (* le faux : un type SANS valeur *)
type ('a, 'b) somme = G of 'a | D of 'b
type 'a negation = 'a -> vide

let et_i a b = (a, b)                  (* et_i   : Gamma|-A, Gamma|-B => A/\B *)
let et_e_g (a, _) = a                  (* et_e^g : le premier membre *)
let et_e_d (_, b) = b                  (* et_e^d : le second *)
let imp_i (f : 'a -> 'b) = f           (* imp_i  : l'abstraction EST la décharge *)
let imp_e (f : 'a -> 'b) (x : 'a) = f x  (* imp_e : l'application EST le modus ponens *)
let ou_i_g a = G a
let ou_i_d b = D b
let ou_e s fg fd = match s with G a -> fg a | D b -> fd b   (* le filtrage *)
let bot_e (x : vide) : 'c = match x with _ -> .             (* le cas impossible *)

Les correspondances qui frappent : ${\to }_i$ est la définition d'une fonction, ${\to }_e$ est l'application, ${\wedge }_i$ est la construction d'un couple, ${\wedge }_e$ est une projection, et ${\vee }_e$ — la règle à trois prémisses, la plus lourde du chapitre — est le match à deux branches. La règle ${\perp }_e$ est le filtrage sur un type vide : le compilateur accepte match x with _ -> . précisément parce qu'il vérifie qu'aucun cas n'est possible.

2. Trois preuves, trois programmes. Types inférés par le compilateur, non annotés :

Et le syllogisme disjonctif, qui emploie ${\perp }_e$ :

(* p \/ q,  p |- q *)
let syllogisme_disjonctif s (np : 'a negation) =
  match s with G a -> bot_e (np a) | D b -> b

Le type de fun f g x -> g (f x) est le syllogisme barbara, littéralement. La composition de fonctions et la transitivité de l'implication sont le même objet ; les trois nœuds de l'arbre du cours sont les trois symboles g, f et x. Et fun a _ -> a ignore son second argument, ce qui est exactement l'observation de l'exercice 28.4 : l'hypothèse $q$ ne sert pas.

3. La règle absurde n'a pas de programme. Son type serait (('a -> vide) -> vide) -> 'a, c'est-à-dire « d'une réfutation de la réfutation de $A$, produire un $A$ ». Or produire un 'a quel que soit le type $\alpha$ est impossible : il n'y a pas de valeur qui soit à la fois un entier, une chaîne et une fonction. Aucune fonction totale n'a ce type. L'absence de la règle du côté logique et l'absence du terme du côté programme sont le même fait.

Le pendant de ${\vee }_i$ le dit encore mieux : un terme de type ('a, 'a negation) somme devrait être G ou D, c'est-à-dire décider, pour tout type, s'il est habité ou non. Le tiers exclu est un programme qui répondrait à toute question — d'où son absence.

4. L'hypothèse cachée : les programmes doivent terminer. La correspondance ne tient que pour des termes totaux, sans exception ni boucle infinie. OCaml, lui, en autorise :

let rec absurde () = absurde ()      (* type inféré : unit -> 'a *)

Ce terme a le type unit -> 'a : il « démontre » n'importe quelle formule. Il ne rend simplement jamais de valeur. De même, assert false a le type 'a et prouve tout ce qu'on veut, en levant une exception.

La conclusion, et elle boucle sur le chapitre chap:algo-prog : une preuve est un programme qui termine. Un programme qui boucle est une preuve incorrecte, et la terminaison — le variant — n'est pas une propriété annexe, c'est ce qui donne au programme le droit d'être lu comme une preuve. C'est pourquoi les assistants de preuve comme Rocq (anciennement Coq) refusent toute récursion dont ils ne peuvent pas établir la terminaison. Tout ce chapitre est hors programme ; il n'est là que pour montrer que le formalisme qu'on vient d'apprendre est celui qu'on manipule depuis le chapitre chap:langage-ocaml.