diff options
| -rw-r--r-- | exercices-inf110.tex | 151 |
1 files 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} + + % % |