diff options
Diffstat (limited to 'exercices-inf110.tex')
| -rw-r--r-- | exercices-inf110.tex | 53 |
1 files changed, 53 insertions, 0 deletions
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} + % % |