diff options
| -rw-r--r-- | exercices-inf110.tex | 211 |
1 files changed, 209 insertions, 2 deletions
diff --git a/exercices-inf110.tex b/exercices-inf110.tex index 93f7afe..14b337c 100644 --- a/exercices-inf110.tex +++ b/exercices-inf110.tex @@ -15,6 +15,7 @@ \usepackage{mathrsfs} \usepackage{wasysym} \usepackage{url} +\usepackage{mathpartir} \usepackage{flagderiv} % \usepackage{graphics} @@ -1699,7 +1700,7 @@ posent pas.) % -\exercice\ (${\star}{\star}$)\par\nobreak +\exercice\label{exercise-coding-of-pairs-untyped}\ (${\star}{\star}$)\par\nobreak On s'intéresse à une façon d'implémenter les couples en $\lambda$-calcul non-typé : $\Pi := \lambda xyf.fxy$ (servant à faire @@ -1825,7 +1826,8 @@ polymorphes, pas des fonctions attendant une fonction polymorphe en argument, si bien que OCaml ne peut pas typer correctement la fonction \texttt{tonative} (et selon l'expression précise utilisée, on obtient des approximations plus ou moins bonnes du « vrai » type qu'on vient -de dire). +de dire). Voir l'exercice \ref{exercise-system-f}(2) pour un cadre +donnant un sens précis aux types intervenant dans ce paragraphe. Dans un quelconque de ces langages, si on implémente la fonction \texttt{pairing} comme on vient de le dire, la valeur de $\mathtt{x}$ @@ -3006,6 +3008,211 @@ sémantique des ouverts) elle ne peut pas être démontrable. % % +\section{Quantificateurs} + +\exercice\label{exercise-system-f}\ (${\star}{\star}{\star}$)\par\nobreak + +On appelle \textbf{système F} de Girard (dit aussi $\lambda 2$), ou +plus exactement le système F étendu par types produits, sommes, 1, 0 +et quantificateur existentiel, le système de logique et/ou typage de +la manière décrite ci-dessous. L'idée générale est que le système F +ajoute au calcul propositionnel intuitionniste la capacité à +quantifier sur des propositions ; ou, si on voit ça comme un système +de typage, un polymorphisme explicite. + +On part des règles du $\lambda$-calcul simplement typé étendu par +types produits, sommes, 1, 0, qu'on notera avec les notations logiques +($\land,\lor,\top,\bot$), ou, ce qui revient au même, du calcul +propositionnel intuitionniste. On ajoute un symbole spécial $*$ pour +représenter le « type des propositions » (ou types) avec les règles de +typage suivantes définissant la construction des propositions (ou +types) : +\begin{center} +$\inferrule{\Gamma\vdash P:*\\\Gamma\vdash Q:*}{\Gamma\vdash P\Rightarrow Q:*}$ +\penalty0\quad +$\inferrule{\Gamma\vdash P:*\\\Gamma\vdash Q:*}{\Gamma\vdash P\land Q:*}$ +\penalty0\quad +$\inferrule{\Gamma\vdash P:*\\\Gamma\vdash Q:*}{\Gamma\vdash P\lor Q:*}$ +\penalty-100\quad +$\inferrule{ }{\Gamma\vdash \top:*}$ +\penalty0\quad +$\inferrule{ }{\Gamma\vdash \bot:*}$ +\end{center} +On ajoute des règles permettant de quantifier sur $*$ : +\begin{center} +$\inferrule{\Gamma,\;T:*\;\vdash\; Q:*}{\Gamma\;\vdash\; (\forall(T:*).\,Q):*}$ +\penalty0\quad +$\inferrule{\Gamma,\;T:*\;\vdash\; Q:*}{\Gamma\;\vdash\; (\exists(T:*).\,Q):*}$ +\end{center} +Et on ajoute les règles d'introduction et d'élimination de des +quantificateurs : +\begin{center} +$\inferrule{\Gamma,\; T:*\;\vdash\; s:Q}{\Gamma\vdash\; (\lambda(T:*).\,s)\;:\;(\forall (T:*).\, Q)}$ +\penalty0\quad +$\inferrule{\Gamma\vdash\; f \;:\; (\forall (T:*).\, Q)\\\Gamma\vdash P:*}{\Gamma\vdash\; fP \;:\; Q[T\backslash P]}$ +\penalty0\quad +$\inferrule{\Gamma\vdash P:*\\\Gamma\vdash\; z \;:\; Q[T\backslash P]}{\Gamma\vdash\; \langle P,z\rangle \;:\; (\exists (T:*).\, Q)}$ +\penalty0\quad +$\inferrule{\Gamma\vdash\; z \;:\; (\exists (T:*).\, P)\\\Gamma,\, T:*,\, h:P\;\vdash\; Q}{\Gamma\vdash (\texttt{match~}z\texttt{~with~}\langle T,h\rangle \mapsto s) \;:\; Q}$ +\end{center} + +Pour abréger les notations, on écrit souvent, et on le fera dans la +suite, « $\Lambda T$ » plutôt que « $\lambda(T:*)$ » (abstraction sur +les propositions/types), et « $\forall T$ » / « $\exists T$ » plutôt +que « $\forall(T:*)$ » / « $\exists(T:*)$ » (puisque c'est la seule +forme de quantification autorisée par le système F). + +À titre d'exemple, dans le système F, on peut écrire le terme $\Lambda +A.\, \Lambda B.\, \lambda(x:A).\, \lambda(y:B).\, x$, qui prouve (ou a +pour type) $\forall A.\, \forall B.\, (A\Rightarrow B\Rightarrow A)$, +ou encore $\Lambda A.\, \lambda(f:\forall B.B).\, fA$ qui prouve (ou a +pour type) $\forall A.\, ((\forall B.\, B) \Rightarrow A)$. + +\smallskip + +\textbf{(1)} Montrer (en donnant des $\lambda$-termes) dans le +système F que $\forall A.\,(A \Rightarrow \forall C.((A\Rightarrow +C)\Rightarrow C))$ et que $\forall A.\,((\forall C.((A\Rightarrow +C)\Rightarrow C)) \Rightarrow A)$. Si on voit ces termes comme des +programmes ayant les types en question, décrire brièvement ce que font +ces programmes. + +\textbf{(2)} Montrer de même que $\forall A.\,\forall B.\,(A\land B +\Rightarrow \forall C.((A\Rightarrow B\Rightarrow C)\Rightarrow C))$ +et que $\forall A.\,\forall B.\,((\forall C.((A\Rightarrow +B\Rightarrow C)\Rightarrow C)) \Rightarrow A\land B)$. Quel rapport +avec l'exercice \ref{exercise-coding-of-pairs-untyped} ? + +\textbf{(3)} La question précédente indique que dans le système F, +$P\land Q$ peut être considéré comme un synonyme de $\forall C.\, +(P\Rightarrow Q\Rightarrow C)\Rightarrow C$ (ces deux propositions +sont équivalentes ; ceci ne montre pas tout à fait qu'on peut se +dispenser entièrement du signe $\land$ car il n'est pas évident qu'on +n'en ait pas besoin dans les démonstrations, mais il s'avère que c'est +le cas). Proposer de façon semblable un synonyme de $P\lor Q$ ne +faisant intervenir que $\Rightarrow$ et $\forall$, et montrer +l'équivalence. + +\textbf{(4)} Proposer une piste pour réécrire $\exists T.\,Q$ (où $T$ +peut apparaître libre dans $Q$) en ne faisant intervenir que +$\Rightarrow$ et $\forall$. (Comme le système F ne permet pas de +quantifier sur les propositions dépendant d'une autre +proposition\footnote{Il faudrait pour cela faire apparaître le type +$*\to *$ et quantifier dessus, ce qui dépasse le système F (le système +appelé « F$\omega$ » le permet).}, on se contentera d'écrire les +équivalences sur un $Q$ quelconque.) + +\begin{corrige} +\textbf{(1)} La formule $\forall A.\,(A \Rightarrow \forall +C.((A\Rightarrow C)\Rightarrow C))$ est prouvée par le $\lambda$-terme +$\Lambda A.\, \lambda(x:A).\, \Lambda C.\, \lambda(k:A\Rightarrow +C).\, kx$. Dans l'autre sens, la formule $\forall A.\,((\forall +C.((A\Rightarrow C)\Rightarrow C)) \Rightarrow A)$ est prouvée par le +$\lambda$-terme $\Lambda A.\, \lambda(h:\forall C.((A\Rightarrow +C)\Rightarrow C)).\, hA(\lambda(x:A).x)$. + +Si on voit ces termes comme des programmes, le premier qu'on vient de +décrire prend un type $A$ et une valeur $x$ de ce type et convertit +cette valeur en un « passage par continuation » (ou « cachée dans une +clôture »), c'est-à-dire en une fonction qui prend un type $C$ et une +fonction $k$ (qu'il faut imaginer comme une sorte continuation) et +passe $x$ comme argument à $k$. Le second fait la conversion +inverse : il prend un type $A$ et une valeur $h$ passée par +continuation et extrait la valeur en appliquant $h$ au type $A$ +lui-même et à la continuation-de-fait donnée par la fonction identité. + +\textbf{(2)} La formule $\forall A.\,\forall B.\,(A\land B \Rightarrow +\forall C.((A\Rightarrow B\Rightarrow C)\Rightarrow C))$ est prouvée +par $\Lambda A.\, \Lambda B.\, \lambda(z:A\land B).\, \Lambda C.\, +\lambda(k:A\Rightarrow B\Rightarrow C).\, k(\pi_1 z)(\pi_2 z)$. Dans +l'autre sens, la formule $\forall A.\,\forall B.\,((\forall +C.((A\Rightarrow B\Rightarrow C)\Rightarrow C)) \Rightarrow A\land B)$ +est prouvée par $\Lambda A.\, \Lambda B.\, \lambda(h:\forall +C.((A\Rightarrow B\Rightarrow C)\Rightarrow C)).\, h(A\land +B)(\lambda(x:A).\lambda(y:B).\langle x,y\rangle)$. + +Si on voit ces termes comme des programmes, le premier prend en entrée +deux types et un couple dont les coordonnées ont ces deux types, et le +transforme en la fonction qui attend une fonction de deux arguments et +l'appelle avec les deux coordonnées du couple comme arguments +successifs : c'est la fonction notée \texttt{fromnative} dans la +correction de l'exercice \ref{exercise-coding-of-pairs-untyped} (i.e., +elle prend un couple « natif » et le convertit en sa représentation +sous forme de clôture). Le second programme fait la conversion +inverse et correspond à la fonction notée \texttt{tonative} dans la +correction de l'exercice \ref{exercise-coding-of-pairs-untyped}. La +subtilité évoquée dans la correction dudit exercice revient à observer +que le typage de OCaml n'est pas aussi riche que le système F. + +\textbf{(3)} L'idée est que pour passer un type somme $P\lor Q$ par +continuation on va recevoir deux fonctions, l'une invoquée dans le +cas $P$ et l'autre dans le cas $Q$. On peut aussi prendre son +inspiration d'un des axiomes du système de Hilbert $(A\Rightarrow C) +\Rightarrow (B\Rightarrow C)\Rightarrow A\lor B\Rightarrow C$. Bref, +on va représenter $P\lor Q$ par $\forall C.\,(P\Rightarrow C) +\Rightarrow (Q\Rightarrow C)\Rightarrow C$. + +La formule $\forall A.\,\forall B.\,(A\lor B \Rightarrow +\forall C.((A\Rightarrow C) \Rightarrow (B\Rightarrow C)\Rightarrow +C))$ est prouvée par $\Lambda A.\, \Lambda B.\, \lambda(z:A\lor B).\, +\Lambda C.\, \lambda(k:A\Rightarrow C).\, \lambda(\ell:B\Rightarrow +C).\, (\texttt{match~}z\texttt{~with~}\iota_1 x \mapsto kx,\; \iota_2 +y \mapsto \ell y)$. Dans l'autre sens, la formule $\forall +A.\,\forall B.\,((\forall C.((A\Rightarrow C)\Rightarrow (B\Rightarrow +C)\Rightarrow C)) \Rightarrow A\lor B)$ est prouvée par $\Lambda A.\, +\Lambda B.\, \lambda(h:\forall C.((A\Rightarrow C)\Rightarrow +(B\Rightarrow C)\Rightarrow C)).\, h(A\lor +B)(\lambda(x:A).\iota_1^{(A,B)} x) (\lambda(y:B).\iota_2^{(A,B)} y)$. + +\textbf{(4)} Enfin, la quantification existentielle $\exists T.\,Q(T)$ +va être représentée par $\forall C.\,((\forall U. (Q(U)\Rightarrow +C))\Rightarrow C)$. La formule $(\exists T. Q(T)) \Rightarrow \forall +C.((\forall U. (Q(U)\Rightarrow C))\Rightarrow C)$ est prouvée par +$\lambda(z:\exists T. Q(T)).\, \Lambda C.\, \lambda(k:\forall +U. (Q(U)\Rightarrow C)).\, (\texttt{match~}z\texttt{~with~}\langle +T,t\rangle \mapsto kTt)$. Dans l'autre sens, la formule $(\forall +C.((\forall U. (Q(U)\Rightarrow C))\Rightarrow C)) \Rightarrow +(\exists T. Q(T))$ est prouvée par $\lambda(h:\forall C.((\forall +U. (Q(U)\Rightarrow C))\Rightarrow C)).\, h(\exists T. Q(T)) (\Lambda +U. \lambda(u:U). \langle U,u\rangle)$. + +\emph{Remarque :} grâce à ces manipulations, on peut réécrire tout +terme du système F pour ne faire intervenir que $\Rightarrow$ +et $\forall$ (il est facile de voir que $\bot$ se réécrit comme +$\forall C.C$, et $\top$ comme $\forall C.(C\Rightarrow C)$). On peut +même montrer que le système F limité à ces seuls connecteurs est +équivalent à celui que nous avons défini, et c'est la définition la +plus habituelle de ce lui-ci. Le système ainsi obtenu est plus +économique et plus élégant car il ne comporte comme seule +constructions des termes que l'application et les deux niveaux +d'abstraction, $\lambda$ et $\Lambda$. + +\emph{Remarque 2 :} les règles de Coq incorporent notamment celles du +système F (même F$\omega$). Par exemple, les termes que nous avons +construits à la question (2) peuvent se décrire ainsi : + +{\tt\noindent +Theorem fromnative : forall (A B:Prop), (A/\textbackslash B) -> forall (C:Prop), ((A->B->C)->C).\\ +Proof. intros A B z C k. destruct z as [x y]. exact (k x y). Qed.\\ +Theorem tonative : forall (A B:Prop), (forall (C:Prop), ((A->B->C)->C)) -> A/\textbackslash B.\\ +Proof. intros A B h. apply (h (A/\textbackslash B)). intros x y. split. exact x. exact y. Qed. +\par} + +Les $\lambda$-termes s'écrivent alors, en syntaxe +Coq :\penalty0\hskip1emplus5em \texttt{fun (A B : Prop) (z : A + /\textbackslash\ B) (C : Prop) (k : A -> B -> C) => match z with + conj x y => k x y end}\penalty0\hskip1emplus5em pour le premier +et\penalty0\hskip1emplus5em \texttt{fun (A B : Prop) (h : forall C : + Prop, (A -> B -> C) -> C) => h (A /\textbackslash\ B) (fun (x : A) + (y : B) => conj x y)}\penalty0\hskip1emplus5em pour le second, ce +qui correspond bien à ce qui a été proposé ci-dessus. +\end{corrige} + + +% +% +% + \section{Divers} \exercice\label{exercise-dragon-riddle}\ (${\star}{\star}{\star}{\star}{\star}$)\par\nobreak |