From 24a48fb29b64cc71eef8a2b1a0e46eb69c78c475 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Fri, 12 Jan 2024 15:59:37 +0100
Subject: An exercise on Girard's system F.

---
 exercices-inf110.tex | 211 ++++++++++++++++++++++++++++++++++++++++++++++++++-
 1 file 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}$
@@ -3002,6 +3004,211 @@ sémantique des ouverts) elle ne peut pas être démontrable.
 \end{corrige}
 
 
+%
+%
+%
+
+\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}
+
+
 %
 %
 %
-- 
cgit v1.2.3