From 68cc32a5e65006651230882e15914e2ff19e9666 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Wed, 1 Nov 2023 10:41:54 +0100
Subject: Untyped lambda-calculus and a recursive type.

---
 transp-inf110-01-calc.tex | 36 ++++++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)

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
@@ -3231,6 +3231,42 @@ ne permet pas d'écrire « bonjour ».
 dans tout langage Turing-complet, la conversion peut devenir
 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}
-- 
cgit v1.2.3