Some exercises on the untyped lambda-calculus.

1 files changed, 286 insertions, 0 deletions

diff --git a/exercices-inf110.tex b/exercices-inf110.tex
index 4613d8b..1045209 100644
--- a/exercices-inf110.tex
+++ b/exercices-inf110.tex
@@ -1,5 +1,6 @@
 %% This is a LaTeX document.  Hey, Emacs, -*- latex -*- , get it?
 \documentclass[12pt,a4paper]{article}
+\usepackage[a4paper,hmargin=2cm,vmargin=3cm]{geometry}
 \usepackage[french]{babel}
 \usepackage[utf8]{inputenc}
 \usepackage[T1]{fontenc}
@@ -1162,4 +1163,289 @@ inséparables.
 %
 %
 %
+
+\section{\texorpdfstring{$\lambda$}{Lambda}-calcul non typé}
+
+
+\exercice\ (${\star}$)\par\nobreak
+
+Pour chacun des termes suivants du $\lambda$-calcul non typé, dire
+s'il est en forme normale, ou en donner la forme normale s'il y en a
+une.
+\textbf{(a)} $(\lambda x.x)(\lambda x.x)$
+\hskip 1emplus1emminus1em
+\textbf{(b)} $(\lambda x.xx)(\lambda x.x)$
+\hskip 1emplus1emminus1em
+\textbf{(c)} $(\lambda x.xx)(\lambda x.xx)$
+\hskip 1emplus1emminus1em
+\textbf{(d)} $(\lambda xx.x)(\lambda xx.x)$
+\hskip 1emplus1emminus1em
+\textbf{(e)} $(\lambda xy.x)(\lambda xy.x)$
+\hskip 1emplus1emminus1em
+\textbf{(f)} $(\lambda xy.xy)y$
+\hskip 1emplus1emminus1em
+\textbf{(g)} $(\lambda xy.xy)(\lambda xy.xy)$
+
+\begin{corrige}
+\textbf{(a)} $(\lambda x.x)(\lambda x.x) \rightarrow_\beta \lambda x.x$
+\hskip 1emplus1emminus1em
+\textbf{(b)} $(\lambda x.xx)(\lambda x.x) \rightarrow_\beta (\lambda
+x.x)(\lambda x.x) \rightarrow_\beta \lambda x.x$
+\hskip 1emplus1emminus1em
+\textbf{(c)} $(\lambda x.xx)(\lambda x.xx) \rightarrow_\beta (\lambda
+x.xx)(\lambda x.xx) \rightarrow_\beta \cdots$ la seule
+$\beta$-réduction possible boucle donc il n'y a pas de forme normale.
+\hskip 1emplus1emminus1em
+\textbf{(d)} On renomme d'abord les variables liées en se rappelant
+que chaque variable est liée par le $\lambda$ le plus \emph{intérieur}
+sur son nom : $(\lambda xx.x)(\lambda xx.x) = (\lambda x.\lambda
+x.x)(\lambda x.\lambda x.x) \mathrel{\equiv_\alpha} (\lambda x.\lambda
+y.y)(\lambda u.\lambda v.v) \rightarrow_\beta \lambda y.y
+\mathrel{\equiv_\alpha} \lambda x.x$
+\hskip 1emplus1emminus1em
+\textbf{(e)} $(\lambda xy.x)(\lambda xy.x) = (\lambda x.\lambda
+y.x)(\lambda x.\lambda y.x) \rightarrow_\beta \lambda y.\lambda
+x.\lambda y.x \mathrel{\equiv_\alpha} \lambda y.\lambda x.\lambda z.x
+= \lambda yxz.x$
+\hskip 1emplus1emminus1em
+\textbf{(f)} $(\lambda xy.xy)y = (\lambda x.\lambda y.xy)y$ ici pour
+faire la $\beta$-réduction on doit d'abord renommer la variable liée
+par le second $\lambda$ pour éviter qu'elle capture le $y$ libre :
+$(\lambda x.\lambda y.xy)y \mathrel{\equiv_\alpha} (\lambda x.\lambda
+z.xz)y \rightarrow_\beta \lambda z.yz$ (le piège serait de répondre
+$\lambda y.yy$ ici !)
+\hskip 1emplus1emminus1em
+\textbf{(g)} $(\lambda xy.xy)(\lambda xy.xy) = (\lambda x.\lambda
+y.xy)(\lambda x.\lambda y.xy) \rightarrow_\beta \lambda y.(\lambda
+x.\lambda y.xy)y \mathrel{\equiv_\alpha} \lambda y.(\lambda x.\lambda
+z.xz)y \rightarrow_\beta \lambda y.\lambda z.yz = \lambda yz.yz
+\mathrel{\equiv_\alpha} \lambda xy.xy$
+\end{corrige}
+
+%
+
+\exercice\ (${\star}{\star}$)\par\nobreak
+
+On considère la traduction évidente des termes du $\lambda$-calcul pur
+en langage Python et/ou en Scheme définie de la manière suivante :
+\begin{itemize}
+\item une variable se traduit en elle-même (i.e., en
+  l'identificateur de ce nom),
+\item une application $(P Q)$ du $\lambda$-calcul se traduit par
+  $\mathtt{P}(\mathtt{Q})$ pour le Python et par $(\mathtt{P}\ 
+  \mathtt{Q})$ pour le Scheme (dans les deux cas, c'est la notation
+  pour l'application d'une fonction à un terme), où
+  $\mathtt{P},\mathtt{Q}$ sont les traductions de $P,Q$
+  respectivement,
+\item une abstraction $\lambda v. E$ du $\lambda$-calcul se traduit
+  par $\texttt{(lambda $\mathtt{v}$: $\mathtt{E}$)}$ en Python et
+  $\texttt{(lambda ($\mathtt{v}$) $\mathtt{E}$)}$ en Scheme (dans les
+  deux cas, c'est la notation pour la création d'une fonction
+  anonyme), où $\mathtt{E}$ est la traduction de $E$ et $\mathtt{v}$
+  l'identificateur ayant pour nom celui de la variable $v$.
+\end{itemize}
+
+\textbf{(a)} Traduire les entiers de Church $\overline{0},
+\overline{1}, \overline{2}, \overline{3}$ en Python et en Scheme.
+
+\textbf{(b)} Écrire une fonction dans chacun de ces langages prenant
+en entrée (la conversion d')un entier de Church et renvoyant l'entier
+natif (c'est-à-dire au sens usuel du langage) correspondant.  On
+pourra pour cela utiliser la fonction successeur qui s'écrit
+$\texttt{(lambda n: n+1)}$ en Python et $\texttt{(lambda (n) (+ n
+  1))}$ en Scheme.
+
+\textbf{(c)} Traduire les fonctions $\lambda mnfx.nf(mfx)$, $\lambda
+mnf.n(mf)$ et $\lambda mn.nm$ qui représentent $(m,n)\mapsto m+n$,
+$(m,n)\mapsto mn$ et $(m,n)\mapsto m^n$ sur les entiers de Church en
+Python et en Scheme, et vérifier leur bon fonctionnement sur quelques
+exemples (en utilisant la fonction écrite en (b) pour décoder le
+résultat).
+
+\textbf{(d)} Traduire le terme non-normalisable $(\lambda x.xx)
+(\lambda x.xx)$ en Python et Scheme : que se passe-t-il quand on le
+fait exécuter à un interpréteur de ces langages ?  Expliquer
+brièvement cette différence.
+
+\textbf{(e)} Proposer une tentative de traduction des termes du
+$\lambda$-calcul en OCaml ou Haskell : reprendre les questions
+précédentes en indiquant ce qui change pour ces langages.
+
+\begin{corrige}
+\textbf{(a)} En Python : $\overline{0}$ devient \texttt{lambda f:
+  lambda x: x}, $\overline{1}$ devient \texttt{lambda f: lambda x:
+  f(x)}, $\overline{2}$ devient \texttt{lambda f: lambda x: f(f(x))}
+(chacun sur une ligne) et $\overline{3}$ devient \texttt{lambda f:
+  lambda x: f(f(f(x)))} (chacun sur une ligne).  En Scheme :
+$\overline{0}$ devient \texttt{(lambda (f) (lambda (x) x))},
+$\overline{1}$ devient \texttt{(lambda (f) (lambda (x) (f x)))},
+$\overline{2}$ devient \texttt{(lambda (f) (lambda (x) (f (f x))))} et
+$\overline{3}$ devient \texttt{(lambda (f) (lambda (x) (f (f (f
+  x)))))} (espacement indifférent mais les parenthèses sont
+critiques).
+
+\textbf{(b)} Pour convertir un entier de Church en entier natif, il
+suffit d'itérer la fonction successeur la nombre de fois représenté
+par l'entier de Church, ce que l'entier de Church permet justement de
+faire, en l'appliquant au final à $0$.  En Python, cela donne :
+\texttt{def fromchurch(ch): return (ch (lambda n: n+1))(0)} (ou
+\texttt{fromchurch = lambda ch: (ch (lambda n: n+1))(0)} mais dans
+tous les cas sur une seule ligne) ; en Scheme : \texttt{(define
+  (fromchurch ch) ((ch (lambda (n) (+ n 1))) 0))} ce qui est du sucre
+syntaxique pour \texttt{(define fromchurch (lambda (ch) ((ch (lambda
+  (n) (+ n 1))) 0)))}.
+
+\textbf{(c)} Voici un exemple de code vérifiant que $2+3=5$, que
+$2\times 3=6$ et que $2^3=8$ sur les entiers de Church, d'abord en
+Python :
+
+\noindent\texttt{%
+churchzero = (lambda f: lambda x: x)\\
+churchone = (lambda f: lambda x: f(x))\\
+churchtwo = (lambda f: lambda x: f(f(x)))\\
+churchthree = (lambda f: lambda x: f(f(f(x))))\\
+fromchurch = lambda ch: (ch (lambda n: n+1))(0)\\
+churchadd = lambda m: lambda n: lambda f: lambda x: (n(f))((m(f))(x))\\
+churchmul = lambda m: lambda n: lambda f: n(m(f))\\
+churchpow = lambda m: lambda n: n(m)\\
+\# Check 2+3 == 5:\\
+fromchurch((churchadd(churchtwo))(churchthree))\\
+\# Check 2*3 == 6:\\
+fromchurch((churchmul(churchtwo))(churchthree))\\
+\# Check 2\textasciicircum 3 == 8:\\
+fromchurch((churchpow(churchtwo))(churchthree))
+}
+
+\noindent …puis en Scheme :
+
+\noindent\texttt{%
+(define churchzero (lambda (f) (lambda (x) x)))\\
+(define churchone (lambda (f) (lambda (x) (f x))))\\
+(define churchtwo (lambda (f) (lambda (x) (f (f x)))))\\
+(define churchthree (lambda (f) (lambda (x) (f (f (f x))))))\\
+(define fromchurch (lambda (ch) ((ch (lambda (n) (+ n 1))) 0)))\\
+(define churchadd (lambda (m) (lambda (n) (lambda (f) (lambda (x)\\
+\ \ ((n f) ((m f) x)))))))\\
+(define churchmul (lambda (m) (lambda (n) (lambda (f) (n (m f))))))\\
+(define churchpow (lambda (m) (lambda (n) (n m))))\\
+;; Check 2+3 == 5:\\
+(fromchurch ((churchadd churchtwo) churchthree))\\
+;; Check 2*3 == 6:\\
+(fromchurch ((churchmul churchtwo) churchthree))\\
+;; Check 2\textasciicircum 3 == 8:\\
+(fromchurch ((churchpow churchtwo) churchthree))
+}
+
+Dans les deux cas, les valeurs retournées sont successivement $5$, $6$
+et $8$.
+
+Noter que dans les deux langages la syntaxe est rendue lourdingue par
+le fait que (conformément aux conventions du $\lambda$-calcul dont on
+a mécaniquement traduit des termes) on ne crée que des fonctions
+d'\emph{un} argument, ce qui oblige les fonctions d'opération à
+prendre les arguments sous forme « curryfiée ».  Il serait bien plus
+naturel d'écrire par exemple \texttt{churchpow = lambda m,n: n(m)} en
+Python et \texttt{(define churchpow (lambda (m n) (n m)))} en Scheme
+pour définir directement une fonction de \emph{deux} arguments, qu'on
+peut ensuite utiliser comme \texttt{churchpow(churchtwo,churchthree)}
+et \texttt{(churchpow churchtwo churchthree)} respectivement.
+
+\texttt{(d)} En Python : $\texttt{(lambda x: x(x))(lambda x: x(x))}$ ;
+en Scheme : \texttt{((lambda (x) (x x)) (lambda (x) (x x)))}.  Le
+premier termine rapidement avec un débordement de pile (au moins dans
+la version actuelle Python 3.11), le second, quel que soit
+l'interpréteur Scheme (au moins tous ceux que j'ai pu tester), boucle
+indéfiniment (mais sans consommation de pile supplémentaire ni d'autre
+forme de mémoire).
+
+La raison de cette différence est que Scheme effectue (et la
+spécification du langage impose) une \emph{récursion terminale
+propre} : lorsque le code d'une fonction $f$ termine par l'appel à une
+autre fonction $g$ (en renvoyant sa valeur), le contrôle de
+l'exécution est simplement passé de $f$ à $g$ sans empilement
+d'adresse de retour (qui n'a pas lieu d'être puisque la valeur de
+retour de $f$ sera justement celle de $g$) ; en Python, en revanche,
+la récursion terminale n'est pas traitée spécialement, donc chaque
+appel à \texttt{x(x)} est empilé et jamais dépilé et la pile déborde
+rapidement.
+
+\texttt{(e)} La traduction du $\lambda$-calcul en OCaml ou Haskell est
+évidente en utilisant $\texttt{fun $\mathtt{v}$ -> $\mathtt{E}$}$
+(noté $\texttt{\textbackslash $\mathtt{v}$ -> $\mathtt{E}$}$ en
+Haskell) pour traduire $\lambda v.E$ (et toujours
+$(\mathtt{P}\ \mathtt{Q})$ pour $(P Q)$).  Néanmoins, il n'est pas
+évident qu'on puisse toujours écrire les termes qu'on souhaite, parce
+qu'ils ne seront pas forcément typables.
+
+En OCaml, le test sur les entiers de Church donne :
+
+\noindent\texttt{%
+let churchzero = fun f -> fun x -> x\\
+let churchone = fun f -> fun x -> f x\\
+let churchtwo = fun f -> fun x -> f (f x)\\
+let churchthree = fun f -> fun x -> f (f (f x))\\
+let fromchurch = fun ch -> ch (fun n->(n+1)) 0\\
+let churchadd = fun m -> fun n -> fun f -> fun x -> (n f)(m f x)\\
+let churchmul = fun m -> fun n -> fun f -> n (m f)\\
+let churchpow = fun m -> fun n -> n m\\
+;;\\
+(* Check 2+3 == 5: *)\\
+fromchurch(churchadd churchtwo churchthree) ;;\\
+(* Check 2*3 == 6: *)\\
+fromchurch(churchmul churchtwo churchthree) ;;\\
+(* Check 2\textasciicircum 3 == 8: *)\\
+fromchurch(churchpow churchtwo churchthree) ;;
+}
+
+\noindent …et en Haskell :
+
+\noindent\texttt{%
+let churchzero = \textbackslash f -> \textbackslash x -> x\\
+let churchone = \textbackslash f -> \textbackslash x -> f x\\
+let churchtwo = \textbackslash f -> \textbackslash x -> f (f x)\\
+let churchthree = \textbackslash f -> \textbackslash x -> f (f (f x))\\
+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:\\
+fromchurch(churchadd churchtwo churchthree)\\
+\# Check 2*3 == 6:\\
+fromchurch(churchmul churchtwo churchthree)\\
+\# Check 2\textasciicircum 3 == 8:\\
+fromchurch(churchpow churchtwo churchthree)
+}
+
+Il se trouve que sur ces exemples simples le typage n'empêche pas la
+construction, mais si on essayait de faire la fonction $n \mapsto
+n^n$, par exemple, la fonction \texttt{fun n -> churchpow n n} ne type
+pas.  De même, le terme non normalisant de la question (d), qui se
+traduirait \texttt{(fun x -> x x)(fun x -> x x)} en OCaml, et
+\texttt{(\textbackslash x -> x x)(\textbackslash x -> x x)} en
+Haskell, est refusé par le système de typage : ni le OCaml ni le
+Haskell ne permet de traduire tous les termes du $\lambda$-calcul non
+typé, précisément parce qu'ils sont typés.
+
+(\textbf{Attention :} si le Python comme le Scheme permettent de
+\emph{traduire} tous les termes du $\lambda$-calcul non typé, le
+comportement de l'évaluateur, dans les deux cas, ne correspond pas
+forcément à une stratégie évidente de $\beta$-réduction du
+$\lambda$-calcul.  Notamment, le terme $(\lambda uz.z)((\lambda
+x.xx)(\lambda x.xx))$, bien que faiblement normalisable en
+$\lambda$-calcul, conduira une fois traduit à une boucle dans ces deux
+langages, parce que l'évaluateur commence par évaluer les arguments
+d'une fonction avant d'appliquer la fonction ; inversement, le terme
+$\lambda u.(\lambda x.xx)(\lambda x.xx)$, bien qu'il ne soit même pas
+faiblement normalisable en $\lambda$-calcul, est accepté sans broncher
+par ces deux langages car le corps d'une fonction n'est évalué qu'à
+l'application de la fonction.  Cependant, les calculs de fonctions
+primitives récursives sur les entiers de Church ne font intervenir que
+des termes fortement normalisants sur lesquels ces difficultés ne se
+posent pas.)
+\end{corrige}
+
+
+%
+%
+%
 \end{document}