diff options
| -rw-r--r-- | transp-inf110-01-calc.tex | 36 |
1 files changed, 36 insertions, 0 deletions
diff --git a/transp-inf110-01-calc.tex b/transp-inf110-01-calc.tex index b16e46b..811e6d9 100644 --- a/transp-inf110-01-calc.tex +++ b/transp-inf110-01-calc.tex @@ -3233,4 +3233,40 @@ extrêmement inefficace, malcommode ou illible. \end{frame} % +\begin{frame} +\frametitle{$\lambda$-calcul non typé et type récursif} + +{\footnotesize\textcolor{gray}{Remarque faite pour plus tard.}\par} + +\smallskip + +Le fait d'avoir un type $t$ tel que $t \,\cong\, (t\rightarrow t)$ +permet d'implémenter dans ce type le $\lambda$-calcul « non typé » +(donc tue l'espoir de décider la terminaison). + +\bigskip + +Exemple en OCaml (ici, \texttt{loop} produit une boucle infinie) : + +\smallskip + +{\footnotesize +\texttt{type t = T of (t -> t)}\\ +\texttt{let apply : t -> t -> t = fun (T rator) -> fun rand -> rator rand}\\ +\texttt{let id : t = T (fun x -> x)}\hfill\texttt{(* }$\lambda x.x$\texttt{ *)}\\ +\texttt{let ch0 : t = T (fun f -> T (fun x -> x))}\hfill\texttt{(* }$\lambda fx.x$\texttt{ *)}\\ +\texttt{let ch1 : t = T (fun f -> T (fun x -> apply f x))}\hfill\texttt{(* }$\lambda fx.fx$\texttt{ *)}\\ +\texttt{let ch2 : t = T (fun f -> T (fun x -> apply f (apply f x)))}\hfill\texttt{(* }$\lambda fx.f(fx)$\texttt{ *)}\\ +\texttt{let om : t = T (fun x -> apply x x)}\hfill\texttt{(* }$\lambda x.xx$\texttt{ *)}\\ +\texttt{let loop : t = apply om om}\hfill\texttt{(* }$(\lambda x.xx)(\lambda x.xx)$\texttt{ *)}\\ +\texttt{(* let loop = (fun (T h) -> h (T h)) (T (fun (T h) -> h (T h))) *)}\\ +\par} + +\medskip + +Remarquer qu'ici on arrive à provoquer une boucle infinie sans aucun +\texttt{let rec} (et malgré le typage). + +\end{frame} +% \end{document} |