diff options
| -rw-r--r-- | exercices-inf110.tex | 286 |
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} |