informatique (MP2I/MPI) · Chapitre 28 · Application directe du cours

Problème — Curry--Howard : une preuve est un programme

Déduction naturelle · niveau 3 (difficile)

Énoncé

Le programme demande d'écrire de petites preuves ; ce problème montre qu'on en a déjà écrit beaucoup, sans le savoir, en programmant en OCaml. On pose la correspondance suivante entre formules et types :

$A \to B$	`'a -> 'b`
$A \land B$	`'a * 'b`
$A \lor B$	`('a, 'b) somme`, avec `type ('a,'b) somme = G of 'a \| D of 'b`
$⊥$	`vide`, avec `type vide = \|` (aucun constructeur)
$\neg A$	`'a -> vide`

Écrire un terme OCaml pour chacune des huit règles du chapitre.
Écrire les termes correspondant à barbara, à l'affaiblissement et au syllogisme disjonctif, et lire leurs types inférés.
Que devient la règle absurde de l'exercice 28.9 ?
Quelle hypothèse la correspondance exige-t-elle des programmes ?

Corrigé de la question 1

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, $\land_{i}$ est la construction d'un couple, $\land_{e}$ est une projection, et $\lor_{e}$ — la règle à trois prémisses, la plus lourde du chapitre — est le match à deux branches. La règle $⊥_{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.

Question 2 : comment l'IA t'aide

2. Écrire les termes correspondant à barbara, à l'affaiblissement et au syllogisme disjonctif, et lire leurs types inférés.

Élève

Pour le syllogisme disjonctif, je filtre la somme : la branche D b rend b. Mais dans la branche G a, je dois produire une valeur de type 'b à partir de rien.

Pas à partir de rien : dans cette branche, de quoi disposes-tu en plus de a ? Quel est le type de cet autre argument, et que peux-tu obtenir en le combinant avec a ?

Élève

J'ai la négation de $p$ , de type 'a -> vide, donc en l'appliquant à a j'obtiens une valeur de type vide. Mais un vide n'est pas un 'b.

Quelle règle du chapitre permet de tirer n'importe quelle conclusion de $⊥$ , et quelle fonction de la question 1 la réalise ? Quel type le compilateur infère-t-il alors pour ta fonction ?

L'IA ne donne pas la réponse : elle pose la question qui fait avancer. À toi de continuer.

Continue cet exercice avec l'IA

Reprends la question 2 là où le dialogue s'arrête, puis la suite de l'exercice.

Continuer avec l'IA — gratuit, sans inscription

Gratuit, sans inscription. L'IA te guide pas à pas, sans te donner la réponse.

Le cours du chapitre · Tous les exercices du chapitre

Continuer avec l'IA, gratuit →