Curryfication, dans les deux sens

Premier sens. Posons $A=(p\wedge q)\to r$ et $\Gamma =\{A,p,q\}$.

$$\frac{\frac{\frac{\frac{\frac{}{\Gamma ⊢A}\text{ax}\frac{\frac{}{\Gamma ⊢p}\text{ax}\frac{}{\Gamma ⊢q}\text{ax}}{\Gamma ⊢p\wedge q}{\wedge }_i}{\Gamma ⊢r}{\to }_e}{\{A,p\}⊢q\to r}{\to }_i}{\{A\}⊢p\to (q\to r)}{\to }_i}{⊢A\to (p\to (q\to r))}{\to }_i$$

Second sens. Posons $B=p\to (q\to r)$ et $\Delta =\{B,p\wedge q\}$.

$$\frac{\frac{\frac{\frac{\frac{}{\Delta ⊢B}\text{ax}\frac{\frac{}{\Delta ⊢p\wedge q}\text{ax}}{\Delta ⊢p}{\wedge }_e^g}{\Delta ⊢q\to r}{\to }_e\frac{\frac{}{\Delta ⊢p\wedge q}\text{ax}}{\Delta ⊢q}{\wedge }_e^d}{\Delta ⊢r}{\to }_e}{\{B\}⊢(p\wedge q)\to r}{\to }_i}{⊢B\to ((p\wedge q)\to r)}{\to }_i$$

Les deux arbres ont été vérifiés règle par règle : $8$ nœuds pour le premier, $9$ pour le second.

Ce que dit cette équivalence. « Prendre deux arguments à la fois » et « prendre le premier, puis le second » sont la même chose. C'est trivial en logique, et c'est un mécanisme central en OCaml : la fonction fun (a, b) -> ... et la fonction fun a b -> ... portent la même information, et le passage de l'une à l'autre porte le nom de Haskell Curry. Le problème 28.3 montre que ce n'est pas une analogie : les deux arbres ci-dessus sont, à l'écriture près, les fonctions curry et decurry du chapitre chap:langage-ocaml.

Le détail qui compte dans le second arbre : l'hypothèse $p\wedge q$ est utilisée deux fois, une fois par ${\wedge }_e^g$ et une fois par ${\wedge }_e^d$. Rien ne l'interdit — le contexte est un ensemble, pas une réserve qu'on épuise. Des logiques linéaires interdisent au contraire de réutiliser une hypothèse, et servent à décrire les ressources ; elles sont hors programme.