From 8f7490be3ab838894a87471e732810c651acc191 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Fri, 1 Dec 2023 16:35:58 +0100
Subject: An exercise on a possible representation of pairs in functional
 programming languages.

---
 exercices-inf110.tex | 151 +++++++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 146 insertions(+), 5 deletions(-)

diff --git a/exercices-inf110.tex b/exercices-inf110.tex
index 1d1e8cc..71a7beb 100644
--- a/exercices-inf110.tex
+++ b/exercices-inf110.tex
@@ -1224,7 +1224,7 @@ z.xz)y \rightarrow_\beta \lambda y.\lambda z.yz = \lambda yz.yz
 
 %
 
-\exercice\ (${\star}$)\par\nobreak
+\exercice\ (${\star}{\star}$)\par\nobreak
 
 \textbf{(1)} Considérons le terme $T_2 := (\lambda x.xxx)(\lambda
 x.xxx)$ du $\lambda$-calcul non typé.  Étudier le graphe des
@@ -1343,7 +1343,7 @@ $\lambda v_1 v_2. Rv_2v_1$ : ce n'est pas du tout la même chose !).
 
 %
 
-\exercice\ (${\star}{\star}$)\par\nobreak
+\exercice\label{exercise-traduction-entiers-de-church}\ (${\star}{\star}{\star}$)\par\nobreak
 
 On considère la traduction évidente des termes du $\lambda$-calcul
 en langage Python et/ou en Scheme définie de la manière suivante :
@@ -1527,11 +1527,11 @@ let fromchurch = \textbackslash ch -> ch (\textbackslash n->(n+1)) 0\\
 let churchadd = \textbackslash m -> \textbackslash n -> \textbackslash f -> \textbackslash x -> (n f)(m f x)\\
 let churchmul = \textbackslash m -> \textbackslash n -> \textbackslash f -> n (m f)\\
 let churchpow = \textbackslash m -> \textbackslash n -> n m\\
-\# Check 2+3 == 5:\\
+-- Check 2+3 == 5:\\
 fromchurch(churchadd churchtwo churchthree)\\
-\# Check 2*3 == 6:\\
+-- Check 2*3 == 6:\\
 fromchurch(churchmul churchtwo churchthree)\\
-\# Check 2\textasciicircum 3 == 8:\\
+-- Check 2\textasciicircum 3 == 8:\\
 fromchurch(churchpow churchtwo churchthree)
 }
 
@@ -1563,6 +1563,147 @@ des termes fortement normalisants sur lesquels ces difficultés ne se
 posent pas.)
 \end{corrige}
 
+%
+
+\exercice\ (${\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
+un couple) et $\pi_1 := \lambda p.p(\lambda xy.x)$ et $\pi_2 :=
+\lambda p.p(\lambda xy.y)$ (servant à en extraire la première et la
+seconde composantes).
+
+\textbf{(1)} Montrer que, pour tous termes $X,Y$, le terme $\pi_1(\Pi
+XY)$ se $\beta$-réduit en $X$ et $\pi_2(\Pi XY)$ se $\beta$-réduit en
+$Y$.
+
+\textbf{(2)} Expliquer intuitivement comment fonctionnent $\Pi$,
+$\pi_1$, $\pi_2$ : comment est représentée le couple $(x,y)$ par $\Pi$
+(c'est-à-dire $\Pi xy$) ?
+
+\textbf{(3)} Écrire les fonctions $\Pi$, $\pi_1$, $\pi_2$ (on pourra
+les appeler par exemple \texttt{pairing}, \texttt{proj1},
+\texttt{proj2}) dans un langage de programmation fonctionnel (on
+pourra prendre connaissance de l'énoncé de
+l'exercice \ref{exercise-traduction-entiers-de-church}), et vérifier
+leur bon fonctionnement.  (Mieux vaut, ici, choisir un langage
+fonctionnel non typé, c'est-à-dire dynamiquement typé, pour mieux
+refléter le $\lambda$-calcul non typé et éviter d'éventuels tracas
+liés au typage.  Si le langage a des couples natifs, on pourra écrire
+des conversions des couples natifs dans le codage défini ici, et vice
+versa.)  Si on a des notions de compilation : sous quelle forme est
+stockée l'information du couple dans la représentation faite
+par $\Pi$ ?
+
+\begin{corrige}
+\textbf{(1)} Effectuons par exemple la $\beta$-réduction extérieure
+gauche (mais on rappelle que le théorème de Church-Rosser affirme que
+la normalisation est confluente : tout chemin de $\beta$-réduction
+peut rejoindre tout autre chemin, notamment si on arrive à une forme
+normale ce sera la même) : $\pi_1(\Pi XY) = (\lambda p.p(\lambda
+xy.x))((\lambda xyf.fxy)XY) \rightarrow ((\lambda xyf.fxy)XY)(\lambda
+xy.x) \rightarrow \rightarrow (\lambda f.fXY)(\lambda xy.x)
+\rightarrow (\lambda xy.x)XY \rightarrow \rightarrow X$.  Le résultat
+est le même, \textit{mutatis mutandis}, pour $\pi_2$, à savoir :
+$\pi_2(\Pi XY) = (\lambda p.p(\lambda xy.y))((\lambda xyf.fxy)XY)
+\rightarrow ((\lambda xyf.fxy)XY)(\lambda xy.y) \rightarrow
+\rightarrow (\lambda f.fXY)(\lambda xy.y) \rightarrow (\lambda xy.y)XY
+\rightarrow \rightarrow Y$.
+
+\textbf{(2)} Le couple $(x,y)$ est codé par $\Pi$ en le terme $\Pi xy$
+c'est-à-dire (à $\beta$-réduction près) la fonction $\lambda f.fxy$
+qui prend une fonction $f$ et l'applique (de façon « currifiée ») aux
+deux composantes du couple.  (Autrement dit, pour appliquer une
+fonction au couple, on applique la représentation du couple à la
+fonction !)  Pour décoder le couple, il s'agit simplement d'utiliser
+pour $f$ la fonction $\lambda xy.x$ qui renvoie son premier argument
+lorsqu'on veut récupérer celui-ci, et c'est ce que fait $\pi_1$, ou la
+fonction $\lambda xy.x$ qui renvoie son premier argument lorsqu'on
+veut récupérer celui-ci, et c'est ce que fait $\pi_2$.
+
+\textbf{(3)} Voici une implémentation en Scheme, dans laquelle on a
+pris la liberté d'utiliser des fonctions de plusieurs variables (le
+Scheme permet de définir des fonctions de plusieurs variables sans
+passer les arguments un par un de façon « curryfiée » : la notation
+est \texttt{(f x y)} pour appeler une telle fonction \texttt{f} sur
+deux arguments \texttt{x} et \texttt{y}, et \texttt{(lambda (x y)
+  ...)} pour en définir une ; par ailleurs, les fonction
+\texttt{cons}, \texttt{car} et \texttt{cdr} du Scheme sont les
+fonctions servant nativement à créer et projeter des paires, i.e., ce
+sont les équivalents natifs des fonctions \texttt{pairing},
+\texttt{proj1} et \texttt{proj2} qu'on définit ici) :
+
+\noindent\texttt{%
+(define pairing (lambda (x y) (lambda (f) (f x y))))\\
+(define proj1 (lambda (p) (p (lambda (x y) x))))\\
+(define proj2 (lambda (p) (p (lambda (x y) y))))\\
+(define fromnative (lambda (z) (pairing (car z) (cdr z))))\\
+(define tonative (lambda (p) (p cons)))
+}
+
+On peut ensuite faire différents tests, par exemple \texttt{(proj1
+  (pairing 42 "coucou"))} renvoie \texttt{42}, comme \texttt{(proj1
+  (fromnative (cons 42 "coucou")))} ; et \texttt{(tonative (pairing 42
+  "coucou"))} renvoie la paire native, notée \texttt{(42 . "coucou")}
+en Scheme.
+
+Voici maintenant le code équivalent en OCaml : il n'était pas évident
+\textit{a priori} que le codage puisse être implémenté dans ce langage
+(i.e., qu'il soit typable), mais il s'avère qu'il l'est, modulo la
+subtilité qui sera expiquée ci-dessous :
+
+\noindent\texttt{%
+let pairing = fun x -> fun y -> fun f -> f x y\\
+let proj1 = fun p -> p (fun x -> fun y -> x)\\
+let proj2 = fun p -> p (fun x -> fun y -> y)\\
+(* Conversion from and to native pairs *)\\
+let fromnative = fun (x,y) -> pairing x y\\
+let tonative = fun p -> p (fun x -> fun y -> (x,y))\\
+;;
+}
+
+On peut alors tester que \texttt{proj1 (pairing 42 "coucou")} renvoie
+\texttt{42}, comme \texttt{proj1 (fromnative (42,"coucou"))} ; et
+\texttt{tonative (pairing 42 "coucou")} renvoie la paire native, notée
+\texttt{(42, "coucou")} en OCaml.
+
+\textbf{Subtilité :} Même si cette version OCaml fonctionne bien, une
+petite variation apparemment anodine, à savoir écrire \texttt{let
+  tonative = fun p -> (proj1 p, proj2 p)} (notons que l'équivalent
+Scheme, \texttt{(define tonative (lambda (p) (cons (proj1 p) (proj2
+  p))))}, fonctionne parfaitement) pose des problèmes de typage : avec
+cette nouvelle définition, \texttt{tonative (pairing 42 1729)}
+fonctionne toujours, mais \texttt{tonative (pairing 42 "coucou")}
+conduit à une erreur de typage.  Sans entrer dans les détails de cette
+erreur, le problème est que comme le type du résultat de la fonction
+\texttt{pairing} appliquée à deux types $a$ et $b$ est $(\forall c) (a
+\to b \to c) \to c$ (par exemple, celui du couple \texttt{pairing 42
+  "coucou"} est $(\forall c) (\texttt{int} \to \texttt{string} \to c)
+\to c$), c'est-à-dire une fonction polymorphe acceptant $f : a \to b
+\to c$ pour n'importe quel type $c$ et renvoyant ce même type $c$ ; la
+fonction \texttt{tonative} « devrait » donc avoir pour type $(\forall
+a,b) ((\forall c) ((a \to b \to c) \to c)) \to a \times b$ (ce qui
+\emph{n'est pas} la même chose que $(\forall a,b,c) ((a \to b \to c)
+\to c) \to a \times b$), i.e., elle devrait recevoir une fonction
+polymorphe en argument ; mais le système de typage de OCaml, basé sur
+l'algorithme de Hindley-Milner, ne peut exprimer que des fonctions
+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).
+
+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}$
+et $\mathtt{y}$ dans $\texttt{pairing}\ \mathtt{x}\ \mathtt{y}$ est
+stockée dans la \emph{clôture} de la fonction renvoyée, c'est-à-dire
+les liaisons locales (de $\mathtt{x}$ et $\mathtt{y}$ à leurs valeurs
+respectives) qui ont été faites lors de la création de la fonction et
+qui peuvent, ainsi que le montre cet exemple, survivre bien au-delà de
+la portée de définition de la fonction dans un langage fonctionnel.
+\end{corrige}
+
+
 
 %
 %
-- 
cgit v1.2.3