From 9d42fd28dabb7832adaa22c4e9590ca7efe9a0eb Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Fri, 12 Jan 2024 17:12:15 +0100
Subject: An easy exercise on first-order logic.

---
 exercices-inf110.tex | 53 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 53 insertions(+)

diff --git a/exercices-inf110.tex b/exercices-inf110.tex
index 14b337c..57abfbd 100644
--- a/exercices-inf110.tex
+++ b/exercices-inf110.tex
@@ -3208,6 +3208,59 @@ et\penalty0\hskip1emplus5em \texttt{fun (A B : Prop) (h : forall C :
 qui correspond bien à ce qui a été proposé ci-dessus.
 \end{corrige}
 
+%
+
+\exercice\ (${\star}$)\par\nobreak
+
+\textbf{(1)} Montrer chacune des propositions suivantes en pure
+logique du premier ordre (où $A,B$ désignent des relations unaires) en
+donnant un $\lambda$-terme de preuve : \textbf{(a)} $(\forall
+x. A(x)\Rightarrow B(x)) \Rightarrow (\forall x. A(x)) \Rightarrow
+(\forall x. B(x))$\hskip 1emplus5em \textbf{(b)} $(\forall
+x. A(x)\Rightarrow B(x)) \Rightarrow (\exists x. A(x)) \Rightarrow
+(\exists x. B(x))$\hskip 1emplus5em \textbf{(c)} $(\exists
+x. A(x)\Rightarrow B(x)) \Rightarrow (\forall x. A(x)) \Rightarrow
+(\exists x. B(x))$
+
+\textbf{(2)} En interprétant chacun de ces termes comme un programme,
+en en oubliant les types tels qu'on vient de les écrire, qu'obtient-on
+si on demande à OCaml (c'est-à-dire en fait à l'algorithme de
+Hindley-Milner étendu avec des types produits) de leur reconstruire
+des types ?  Commenter brièvement.
+
+\begin{corrige}
+\textbf{(1)} \textbf{(a)} $\lambda(h:\forall x. A(x)\Rightarrow
+B(x)).\, \lambda(u:\forall x. A(x)).\, \lambda(x:I).\, hx(ux)$\hskip
+1emplus5em \textbf{(b)} $\lambda(h:\forall x. A(x)\Rightarrow B(x)).\,
+\lambda(v:\exists x. A(x)).\, (\texttt{match~}v\texttt{~with~}\langle
+z,w\rangle \mapsto \langle z,hzw\rangle)$\hskip 1emplus5em
+\textbf{(c)} $\lambda(p:\exists x. A(x)\Rightarrow B(x)).\,
+\lambda(u:\forall x. A(x)).\, (\texttt{match~}p\texttt{~with~}\langle
+z,q\rangle \mapsto \langle z,q(uz)\rangle)$
+
+\textbf{(2)} On demande à OCaml de typer les trois expressions
+\texttt{fun h -> fun u -> fun x -> h x (u x)} et \texttt{fun h -> fun
+  v -> match v with (z,w) -> (z, h z w)} et \texttt{fun p -> fun u ->
+  match p with (z,q) -> (z, q(u z))} : les réponses, réécrites avec
+des variables et des lettres collant mieux avec ce qu'on a trouvé
+ci-desus, sont : $(I \to A \to B) \to (I\to A) \to (I\to B)$ pour le
+premier, $(I\to A\to B) \to (I\times A) \to (I\times B)$ pour le
+second, et $I\times(A\to B) \to (I\to A) \to (I\times C)$ pour le
+troisième.  Ces types sont, forcément, moins précis que les types
+$(\prod_{x:I} A(x) \to B(x)) \to (\prod_{x:I} A(x)) \to (\prod_{x:I}
+B(x))$ et $(\prod_{x:I} A(x) \to B(x)) \to (\sum_{x:I} A(x)) \to
+(\sum_{x:I} B(x))$ et $(\sum_{x:I} A(x) \to B(x)) \to (\prod_{x:I}
+A(x)) \to (\sum_{x:I} B(x))$ des types que nous avons écrits à la
+question (1), puisque OCaml ne permet pas les types dépendants.
+
+(On peut aussi remarquer au passage que le premier terme $\lambda
+hux.hx(ux)$, détypé, est le même que le combinateur $\mathsf{S}$ : le
+combinateur $\mathsf{S}$ est l'axiome permettant d'appliquer le
+\textit{modus ponens} sous une implication, de même que notre premier
+terme permet d'applique le \textit{modus ponens} sous un
+quantificateur universel.)
+\end{corrige}
+
 
 %
 %
-- 
cgit v1.2.3