Untyped lambda-calculus and a recursive type.

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}