Fix display and numbering, esp. that of printed version.

3 files changed, 133 insertions, 112 deletions

diff --git a/transp-inf110-01-calc.tex b/transp-inf110-01-calc.tex
index 2970367..649fd14 100644
--- a/transp-inf110-01-calc.tex
+++ b/transp-inf110-01-calc.tex
@@ -1,7 +1,13 @@
 %% This is a LaTeX document.  Hey, Emacs, -*- latex -*- , get it?
+\newif\ifbeamermode
+\beamermodetrue
+\ifbeamermode
 \documentclass[mathserif,a4paper,aspectratio=169]{beamer}
-%\documentclass[a4paper]{article}
-%\usepackage{beamerarticle}
+\else
+\documentclass[a4paper]{article}
+\usepackage{beamerarticle}
+\usepackage[a4paper,margin=2.5cm]{geometry}
+\fi
 \usepackage[shorthands=off,french]{babel}
 \usepackage[utf8]{inputenc}
 \usepackage[T1]{fontenc}
@@ -38,19 +44,20 @@
     \newcommand{\myitemmark}{\hbox{$\blacktriangleright$}}
     \renewcommand{\itempoint}{\strut\myitemmark\nobreak\hskip.5em plus.5em\relax}
     \setlength{\parindent}{0pt}
+    \renewcommand{\thepage}{I–\arabic{page}}
 }
 %
 %
 %
-\title{Calculabilité}
+\title{{\footnotesize Partie I:} Calculabilité}
 \subtitle{INF110 (Logique et Fondements de l'Informatique)}
 \author[David Madore]{David A. Madore\\
 {\footnotesize Télécom Paris}\\
 \texttt{david.madore@enst.fr}}
-\date{2023–2024}
+\date{2023–2025}
 \mode<presentation>{%
 \beamertemplatenavigationsymbolsempty
-\usenavigationsymbolstemplate{\vbox{\hbox{\footnotesize\hyperlinkslideprev{$\leftarrow$}\insertframenumber/\inserttotalframenumber\hyperlinkslidenext{$\rightarrow$}}}}
+\usenavigationsymbolstemplate{\vbox{\hbox{\footnotesize(I) \hyperlinkslideprev{$\leftarrow$}\insertframenumber/\inserttotalframenumber\hyperlinkslidenext{$\rightarrow$}}}}
 }
 \setbeamercolor{myhighlight}{fg=black,bg=white!90!green}
 \begin{document}
@@ -909,8 +916,8 @@ Pseudocode :
 \smallskip
 
 {\footnotesize\texttt{%
-str="somefunc(code) \{ /*...*/ \}\textbackslash nsomefunc(\textbackslash"str=\textbackslash"+quote(str)+str);\textbackslash n";\\
-somefunc(code) \{ /*...*/ \}\\
+str="somefunc(code) \{ /*...*/ \}\textbackslash nsomefunc(\textbackslash"str=\textbackslash"+quote(str)+str);\textbackslash n";\newline
+somefunc(code) \{ /*...*/ \}\newline
 somefunc("str="+quote(str)+str);
 }\par}
 
@@ -1653,14 +1660,14 @@ Pseudocode :
 \smallskip
 
 {\footnotesize\texttt{%
-fibonacci(n) \{\\
-str = "self = \textbackslash"fibonacci(n) \{\textbackslash \textbackslash nstr = \textbackslash" + quote(str) + str;\textbackslash n\textbackslash\\
-if (n==0 || n==1) return n;\textbackslash n\textbackslash\\
-return interpret(self, n-1) + interpret(self, n-2);\textbackslash n\textbackslash\\
-\}";\\
-self = "fibonacci(n) \{\textbackslash nstr = " + quote(str) + str;\\
-if (n==0 || n==1) return n;\\
-return interpret(self, n-1) + interpret(self, n-2);\\
+fibonacci(n) \{\newline
+str = "self = \textbackslash"fibonacci(n) \{\textbackslash \textbackslash nstr = \textbackslash" + quote(str) + str;\textbackslash n\textbackslash\newline
+if (n==0 || n==1) return n;\textbackslash n\textbackslash\newline
+return interpret(self, n-1) + interpret(self, n-2);\textbackslash n\textbackslash\newline
+\}";\newline
+self = "fibonacci(n) \{\textbackslash nstr = " + quote(str) + str;\newline
+if (n==0 || n==1) return n;\newline
+return interpret(self, n-1) + interpret(self, n-2);\newline
 \}
 }\par}
 
@@ -1773,7 +1780,7 @@ Supposons par l'absurde $h$ est calculable : alors cette fonction
 (partielle) $v$ est calculable, disons $v = \varphi_c$.
 
 Si $\varphi_c(c)\downarrow$ alors $h(c,c)=1$ donc $v(c)\uparrow$,
-c'est-à-dire $\varphi_c(c)\uparrow$, contradiction.\\ Si
+c'est-à-dire $\varphi_c(c)\uparrow$, contradiction.\newline Si
 $\varphi_c(c)\uparrow$ alors $h(c,c)=0$ donc $v(c)\downarrow$,
 c'est-à-dire $\varphi_c(c)\downarrow$, contradiction.\qed
 
@@ -3614,13 +3621,13 @@ non-évalué (exemple transp. suivant).
 \itempoint Récursion sans combinateurs :
 
 {\tt
-(define proto-fibonacci\\
-\ \ (lambda (self) ; Pass me as argument!\\
-\ \ \ \ (lambda (n)\\
-\ \ \ \ \ \ (if (<= n 1) n\\
-\ \ \ \ \ \ \ \ \ \ (+ ((self self) (- n 1)) ((self self) (- n 2)))))))\\
-(define fibonacci (proto-fibonacci proto-fibonacci))\\
-(map fibonacci '(0 1 2 3 4 5 6))\\
+(define proto-fibonacci\newline
+\ \ (lambda (self) ; Pass me as argument!\newline
+\ \ \ \ (lambda (n)\newline
+\ \ \ \ \ \ (if (<= n 1) n\newline
+\ \ \ \ \ \ \ \ \ \ (+ ((self self) (- n 1)) ((self self) (- n 2)))))))\newline
+(define fibonacci (proto-fibonacci proto-fibonacci))\newline
+(map fibonacci '(0 1 2 3 4 5 6))\newline
 $\rightarrow$ (0 1 1 2 3 5 8)
 \par}
 
@@ -3641,19 +3648,19 @@ cette construction.
 \frametitle{Digression (suite) : exemple en Scheme}
 
 {\tt
-;; (define y-combinator\\
-;; \ \ (lambda (f)\\
-;; \ \ \ \ ((lambda (x) (f (x x))) (lambda (x) (f (x x))))))\\
-(define z-combinator\\
-\ \ (lambda (f)\\
-\ \ \ \ ((lambda (x) (f (lambda (v) ((x x) v))))\\
-\ \ \ \ \ (lambda (x) (f (lambda (v) ((x x) v)))))))\\
-(define pre-fibonacci\\
-\ \ (lambda (fib)\\
-\ \ \ \ (lambda (n)\\ 
-\ \ \ \ \ \ (if (<= n 1) n\\
-\ \ \ \ \ \ \ \ \ \ (+ (fib (- n 1)) (fib (- n 2)))))))\\
-(define fibonacci (z-combinator pre-fibonacci))\\
+;; (define y-combinator\newline
+;; \ \ (lambda (f)\newline
+;; \ \ \ \ ((lambda (x) (f (x x))) (lambda (x) (f (x x))))))\newline
+(define z-combinator\newline
+\ \ (lambda (f)\newline
+\ \ \ \ ((lambda (x) (f (lambda (v) ((x x) v))))\newline
+\ \ \ \ \ (lambda (x) (f (lambda (v) ((x x) v)))))))\newline
+(define pre-fibonacci\newline
+\ \ (lambda (fib)\newline
+\ \ \ \ (lambda (n)\newline 
+\ \ \ \ \ \ (if (<= n 1) n\newline
+\ \ \ \ \ \ \ \ \ \ (+ (fib (- n 1)) (fib (- n 2)))))))\newline
+(define fibonacci (z-combinator pre-fibonacci))\newline
 \par}
 
 \end{frame}
@@ -3860,15 +3867,15 @@ 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))) *)}\\
+\texttt{type t = T of (t -> t)}\newline
+\texttt{let apply : t -> t -> t = fun (T rator) -> fun rand -> rator rand}\newline
+\texttt{let id : t = T (fun x -> x)}\hfill\texttt{(* }$\lambda x.x$\texttt{ *)}\newline
+\texttt{let ch0 : t = T (fun f -> T (fun x -> x))}\hfill\texttt{(* }$\lambda fx.x$\texttt{ *)}\newline
+\texttt{let ch1 : t = T (fun f -> T (fun x -> apply f x))}\hfill\texttt{(* }$\lambda fx.fx$\texttt{ *)}\newline
+\texttt{let ch2 : t = T (fun f -> T (fun x -> apply f (apply f x)))}\hfill\texttt{(* }$\lambda fx.f(fx)$\texttt{ *)}\newline
+\texttt{let om : t = T (fun x -> apply x x)}\hfill\texttt{(* }$\lambda x.xx$\texttt{ *)}\newline
+\texttt{let loop : t = apply om om}\hfill\texttt{(* }$(\lambda x.xx)(\lambda x.xx)$\texttt{ *)}\newline
+\texttt{(* let loop = (fun (T h) -> h (T h)) (T (fun (T h) -> h (T h))) *)}\newline
 \par}
 
 \medskip
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 1368bc0..67e6687 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -1,7 +1,13 @@
 %% This is a LaTeX document.  Hey, Emacs, -*- latex -*- , get it?
+\newif\ifbeamermode
+\beamermodetrue
+\ifbeamermode
 \documentclass[mathserif,a4paper,aspectratio=169]{beamer}
-%\documentclass[a4paper]{article}
-%\usepackage{beamerarticle}
+\else
+\documentclass[a4paper]{article}
+\usepackage{beamerarticle}
+\usepackage[a4paper,margin=2.5cm]{geometry}
+\fi
 \usepackage[shorthands=off,french]{babel}
 \usepackage[utf8]{inputenc}
 \usepackage[T1]{fontenc}
@@ -49,19 +55,20 @@
     \newcommand{\myitemmark}{\hbox{$\blacktriangleright$}}
     \renewcommand{\itempoint}{\strut\myitemmark\nobreak\hskip.5em plus.5em\relax}
     \setlength{\parindent}{0pt}
+    \renewcommand{\thepage}{II–\arabic{page}}
 }
 %
 %
 %
-\title{Typage simple et calcul propositionnel}
+\title{{\footnotesize Partie II:} Typage simple et calcul propositionnel}
 \subtitle{INF110 (Logique et Fondements de l'Informatique)}
 \author[David Madore]{David A. Madore\\
 {\footnotesize Télécom Paris}\\
 \texttt{david.madore@enst.fr}}
-\date{2023–2024}
+\date{2023–2025}
 \mode<presentation>{%
 \beamertemplatenavigationsymbolsempty
-\usenavigationsymbolstemplate{\vbox{\hbox{\footnotesize\hyperlinkslideprev{$\leftarrow$}\insertframenumber/\inserttotalframenumber\hyperlinkslidenext{$\rightarrow$}}}}
+\usenavigationsymbolstemplate{\vbox{\hbox{\footnotesize(II) \hyperlinkslideprev{$\leftarrow$}\insertframenumber/\inserttotalframenumber\hyperlinkslidenext{$\rightarrow$}}}}
 }
 \setbeamercolor{myhighlight}{fg=black,bg=white!90!green}
 \colorlet{mydarkgreen}{green!50!black}
@@ -822,26 +829,26 @@ $\sigma_1,\ldots,\sigma_k$ :
   par quelques exemples.\par}
 
 \begin{itemize}
-\item $f:\alpha\to\beta,\; x:\alpha \;\vdash\; fx:\beta$\\ Lire : « dans le
+\item $f:\alpha\to\beta,\; x:\alpha \;\vdash\; fx:\beta$\newline Lire : « dans le
   contexte où $f$ est une variable de type $\alpha\to\beta$ et $x$ une
   variable de type $\alpha$, alors $fx$ est de type $\beta$ ».
 \item $f:\beta\to\alpha\to\gamma,\; x:\alpha,\; y:\beta \;\vdash\; fyx
-  : \gamma$\\ {\footnotesize (Parenthéser $\beta\to\alpha\to\gamma$
+  : \gamma$\newline {\footnotesize (Parenthéser $\beta\to\alpha\to\gamma$
   comme $\beta\to(\alpha\to\gamma)$ et $fyx$ comme $(fy)x$.)}
 \item $f:\beta\to\alpha\to\gamma,\; x:\alpha \;\vdash\;
-  \lambda(y:\beta).fyx \;:\; \beta\to\gamma$\\ {\footnotesize
+  \lambda(y:\beta).fyx \;:\; \beta\to\gamma$\newline {\footnotesize
     Comprendre $\lambda(y:\beta).fyx$ comme « fonction prenant $y$ de
     type $\beta$ et renvoyant $fyx$ ».}
 \item $x:\alpha \;\vdash\;
-  \lambda(f:\alpha\to\beta).fx\;:\;(\alpha\to\beta)\to\beta$\\ « Si
+  \lambda(f:\alpha\to\beta).fx\;:\;(\alpha\to\beta)\to\beta$\newline « Si
   $x$ est de type $\alpha$ alors le terme
   $\lambda(f:\alpha\to\beta).fx$ est de type
   $(\alpha\to\beta)\to\beta$. »
 \item $\vdash\; \lambda(x:\alpha).
-  \lambda(f:\alpha\to\beta).fx\;:\;\alpha\to(\alpha\to\beta)\to\beta$\\ « Le
+  \lambda(f:\alpha\to\beta).fx\;:\;\alpha\to(\alpha\to\beta)\to\beta$\newline « Le
   terme $\lambda(x:\alpha).\lambda(f:\alpha\to\beta).fx$ a type
   $\alpha\to(\alpha\to\beta)\to\beta$ dans le contexte
-  vide. »\\ {\footnotesize (Parenthéser
+  vide. »\newline {\footnotesize (Parenthéser
     $\alpha\to(\alpha\to\beta)\to\beta$ comme
     $\alpha\to((\alpha\to\beta)\to\beta)$.)}
 \end{itemize}
@@ -2346,18 +2353,18 @@ B)\land (A\lor C)$ typée par OCaml :
 \bigskip
 
 {\footnotesize\tt
-let pi1 = fun (x,y) -> x ;; (* $\pi_1$ *)\\
-{\color{purple}val pi1 : 'a * 'b -> 'a = <fun>}\\
-let pi2 = fun (x,y) -> y ;; (* $\pi_2$ *)\\
-{\color{purple}val pi2 : 'a * 'b -> 'b = <fun>}\\
-type ('a, 'b) sum = Inj1 of 'a | Inj2 of 'b ;; (* $\alpha+\beta$ *)\\
-{\color{purple}type ('a, 'b) sum = Inj1 of 'a | Inj2 of 'b}\\
-fun u -> match u with Inj1 v -> (Inj1 v, Inj1 v)\\
-\ \ | Inj2 w -> (Inj2 (pi1 w), Inj2 (pi2 w)) ;;\\
-{\color{purple}- : ('a, 'b * 'c) sum -> ('a, 'b) sum * ('a, 'c) sum = <fun>}\\
-fun u -> (match (pi1 u) with Inj1 v -> Inj1 v\\
-\ \ | Inj2 v\_ -> (match (pi2 u) with Inj1 w -> Inj1 w\\
-\ \ \ \ | Inj2 w\_ -> Inj2 (v\_,w\_))) ;;\\
+let pi1 = fun (x,y) -> x ;; (* $\pi_1$ *)\newline
+{\color{purple}val pi1 : 'a * 'b -> 'a = <fun>}\newline
+let pi2 = fun (x,y) -> y ;; (* $\pi_2$ *)\newline
+{\color{purple}val pi2 : 'a * 'b -> 'b = <fun>}\newline
+type ('a, 'b) sum = Inj1 of 'a | Inj2 of 'b ;; (* $\alpha+\beta$ *)\newline
+{\color{purple}type ('a, 'b) sum = Inj1 of 'a | Inj2 of 'b}\newline
+fun u -> match u with Inj1 v -> (Inj1 v, Inj1 v)\newline
+\ \ | Inj2 w -> (Inj2 (pi1 w), Inj2 (pi2 w)) ;;\newline
+{\color{purple}- : ('a, 'b * 'c) sum -> ('a, 'b) sum * ('a, 'c) sum = <fun>}\newline
+fun u -> (match (pi1 u) with Inj1 v -> Inj1 v\newline
+\ \ | Inj2 v\_ -> (match (pi2 u) with Inj1 w -> Inj1 w\newline
+\ \ \ \ | Inj2 w\_ -> Inj2 (v\_,w\_))) ;;\newline
 {\color{purple}- : ('a, 'b) sum * ('a, 'c) sum -> ('a, 'b * 'c) sum = <fun>}
 \par}
 
@@ -2557,7 +2564,7 @@ de tout déduire !).
   le terme $\lambda (u :
   \tau_1+\tau_2). (\texttt{match~}u\texttt{~with~}\iota_1 v_1 \mapsto
   \iota_1^{(\tau_1',\tau_2')} (t_1v_1),\; \iota_2 v_2 \mapsto
-  \iota_2^{(\tau_1',\tau_2')} (t_2v_2))$\\est de type $\tau_1+\tau_2 \to
+  \iota_2^{(\tau_1',\tau_2')} (t_2v_2))$\\ est de type $\tau_1+\tau_2 \to
   \tau_1'+\tau_2'$.
 \item Donnés $s : \sigma' \to \sigma$ (\textcolor{olive}{attention au
   sens !}) et $t : \tau \to \tau'$, le terme $\lambda (u :
@@ -3394,16 +3401,16 @@ val callcc = fn g => SMLofNJ.Cont.callcc (fn k => g (fn v => SMLofNJ.Cont.throw
 \frametitle{Exemples en Scheme}
 
 {\tt
-(define call/cc call-with-current-continuation)\hfill ;; Shorthand\\
-(call/cc (lambda (k) 42))\hfill ;; Return normally\\
-$\rightarrow$ 42\\
-(call/cc (lambda (k) (k 42)))\hfill ;; Return by invoking continuation\\
-$\rightarrow$ 42\\
-(call/cc (lambda (k) (+ (k 42) 1)))\hfill ;; (+ \_ 1) never reached\\
-$\rightarrow$ 42\\
-(* (call/cc (lambda (k) (k 42))) 2)\hfill ;; Nothing weird here\\
-$\rightarrow$ 84\\
-((call/cc (lambda (k) k))\\
+(define call/cc call-with-current-continuation)\hfill ;; Shorthand\newline
+(call/cc (lambda (k) 42))\hfill ;; Return normally\newline
+$\rightarrow$ 42\newline
+(call/cc (lambda (k) (k 42)))\hfill ;; Return by invoking continuation\newline
+$\rightarrow$ 42\newline
+(call/cc (lambda (k) (+ (k 42) 1)))\hfill ;; (+ \_ 1) never reached\newline
+$\rightarrow$ 42\newline
+(* (call/cc (lambda (k) (k 42))) 2)\hfill ;; Nothing weird here\newline
+$\rightarrow$ 84\newline
+((call/cc (lambda (k) k))\newline
 \ (call/cc (lambda (k) k)))\hfill ;; Endless loop: why?
 \par}
 
@@ -3414,9 +3421,9 @@ $\rightarrow$ 84\\
 Très difficile à comprendre :
 
 {\tt
-((lambda (yin)\\
-\ \ \ ((lambda (yang) (yin yang))\\
-\ \ \ \ ((lambda (kk) (display \#\textbackslash *) kk) (call/cc (lambda (k) k)))))\\
+((lambda (yin)\newline
+\ \ \ ((lambda (yang) (yin yang))\newline
+\ \ \ \ ((lambda (kk) (display \#\textbackslash *) kk) (call/cc (lambda (k) k)))))\newline
 \ ((lambda (kk) (newline) kk) (call/cc (lambda (k) k))))
 \par}
 
@@ -3515,8 +3522,8 @@ Que fait ce code ?
 En SML/NJ :
 
 {\tt
-val callcc = fn g => SMLofNJ.Cont.callcc (fn k => g (fn v => SMLofNJ.Cont.throw k v))\\
-datatype ('a,'b) sum = Inj1 of 'a | Inj2 of 'b\\
+val callcc = fn g => SMLofNJ.Cont.callcc (fn k => g (fn v => SMLofNJ.Cont.throw k v))\newline
+datatype ('a,'b) sum = Inj1 of 'a | Inj2 of 'b\newline
 val exclmiddle = callcc (fn k => Inj2 (fn v => k (Inj1 v)))
 ;;
 }
@@ -3586,20 +3593,20 @@ réécrire le code en « Continuation Passing Style » :
 \frametitle{Continuation Passing Style : exemple en OCaml}
 
 {\footnotesize\tt
-let sum\_cps = fun x -> fun y -> fun k -> k(x+y) ;;\\
-{\color{purple}val sum\_cps : int -> int -> (int -> 'a) -> 'a = <fun>}\\
-let minus\_cps = fun x -> fun y -> fun k -> k(x-y) ;;\\
-{\color{purple}val minus\_cps : int -> int -> (int -> 'a) -> 'a = <fun>}\\
-let rec fibonacci\_cps = fun n -> fun k -> if n <= 1 then k n\\
-\ \ else minus\_cps n 1 (fun n1 -> minus\_cps n 2 (fun n2 ->\\
-\ \ \ \ fibonacci\_cps n1 (fun v1 -> fibonacci\_cps n2 (fun v2 ->\\
-\ \ \ \ \ \ sum\_cps v1 v2 k)))) ;;\\
-{\color{purple}val fibonacci\_cps : int -> (int -> 'a) -> 'a = <fun>}\\
-fibonacci\_cps 8 (fun x -> x) ;;\\
-{\color{purple}- : int = 21}\\
-let callcc\_cps = fun g -> fun k -> g (fun v -> fun k0 -> k v) k ;;\\
-(* translation of: callcc (fun kf -> ((kf 42) + 1)) *)\\
-callcc\_cps (fun kf -> fun k -> kf 42 (fun v -> sum\_cps v 1 k)) (fun x -> x) ;;\\
+let sum\_cps = fun x -> fun y -> fun k -> k(x+y) ;;\newline
+{\color{purple}val sum\_cps : int -> int -> (int -> 'a) -> 'a = <fun>}\newline
+let minus\_cps = fun x -> fun y -> fun k -> k(x-y) ;;\newline
+{\color{purple}val minus\_cps : int -> int -> (int -> 'a) -> 'a = <fun>}\newline
+let rec fibonacci\_cps = fun n -> fun k -> if n <= 1 then k n\newline
+\ \ else minus\_cps n 1 (fun n1 -> minus\_cps n 2 (fun n2 ->\newline
+\ \ \ \ fibonacci\_cps n1 (fun v1 -> fibonacci\_cps n2 (fun v2 ->\newline
+\ \ \ \ \ \ sum\_cps v1 v2 k)))) ;;\newline
+{\color{purple}val fibonacci\_cps : int -> (int -> 'a) -> 'a = <fun>}\newline
+fibonacci\_cps 8 (fun x -> x) ;;\newline
+{\color{purple}- : int = 21}\newline
+let callcc\_cps = fun g -> fun k -> g (fun v -> fun k0 -> k v) k ;;\newline
+(* translation of: callcc (fun kf -> ((kf 42) + 1)) *)\newline
+callcc\_cps (fun kf -> fun k -> kf 42 (fun v -> sum\_cps v 1 k)) (fun x -> x) ;;\newline
 {\color{purple}- : int = 42}
 \par}
 
@@ -5044,8 +5051,8 @@ $\lambda$CST.
 \texttt{ocaml -rectypes} :
 
 {\tt
-\$ ocaml -rectypes\\
-fun x -> x x ;;\\
+\$ ocaml -rectypes\newline
+fun x -> x x ;;\newline
 - : ('a -> 'b as 'a) -> 'b = <fun>
 }
 
@@ -5081,11 +5088,11 @@ en OCaml :
 \smallskip
 
 {\footnotesize\tt
-let twice = fun f -> fun x -> f(f x) in (twice ((+)1) 42, twice not true) ;;\\
-{\color{purple}- : int * bool = (44, true)}\\
-(fun twice -> (twice ((+)1) 42, twice not true))(fun f -> fun x -> f(f x)) ;;\\
-{\color{purple}\alert{Error}: This expression has type bool -> bool\\
-       but an expression was expected of type int -> int\\
+let twice = fun f -> fun x -> f(f x) in (twice ((+)1) 42, twice not true) ;;\newline
+{\color{purple}- : int * bool = (44, true)}\newline
+(fun twice -> (twice ((+)1) 42, twice not true))(fun f -> fun x -> f(f x)) ;;\newline
+{\color{purple}\alert{Error}: This expression has type bool -> bool\newline
+       but an expression was expected of type int -> int\newline
        Type bool is not compatible with type int}
 \par}
 
diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex
index 770627e..8afb00c 100644
--- a/transp-inf110-03-quantif.tex
+++ b/transp-inf110-03-quantif.tex
@@ -1,7 +1,13 @@
 %% This is a LaTeX document.  Hey, Emacs, -*- latex -*- , get it?
+\newif\ifbeamermode
+\beamermodetrue
+\ifbeamermode
 \documentclass[mathserif,a4paper,aspectratio=169]{beamer}
-%\documentclass[a4paper]{article}
-%\usepackage{beamerarticle}
+\else
+\documentclass[a4paper]{article}
+\usepackage{beamerarticle}
+\usepackage[a4paper,margin=2.5cm]{geometry}
+\fi
 \usepackage[shorthands=off,french]{babel}
 \usepackage[utf8]{inputenc}
 \usepackage[T1]{fontenc}
@@ -49,19 +55,20 @@
     \newcommand{\myitemmark}{\hbox{$\blacktriangleright$}}
     \renewcommand{\itempoint}{\strut\myitemmark\nobreak\hskip.5em plus.5em\relax}
     \setlength{\parindent}{0pt}
+    \renewcommand{\thepage}{III–\arabic{page}}
 }
 %
 %
 %
-\title{Introduction aux quantificateurs}
+\title{{\footnotesize Partie III:} Introduction aux quantificateurs}
 \subtitle{INF110 (Logique et Fondements de l'Informatique)}
 \author[David Madore]{David A. Madore\\
 {\footnotesize Télécom Paris}\\
 \texttt{david.madore@enst.fr}}
-\date{2023–2024}
+\date{2023–2025}
 \mode<presentation>{%
 \beamertemplatenavigationsymbolsempty
-\usenavigationsymbolstemplate{\vbox{\hbox{\footnotesize\hyperlinkslideprev{$\leftarrow$}\insertframenumber/\inserttotalframenumber\hyperlinkslidenext{$\rightarrow$}}}}
+\usenavigationsymbolstemplate{\vbox{\hbox{\footnotesize(III) \hyperlinkslideprev{$\leftarrow$}\insertframenumber/\inserttotalframenumber\hyperlinkslidenext{$\rightarrow$}}}}
 }
 \setbeamercolor{myhighlight}{fg=black,bg=white!90!green}
 \colorlet{mydarkgreen}{green!50!black}
@@ -701,7 +708,7 @@ des couples, fonctions, etc., des individus).
 \itempoint Néanmoins, elle a une \alert{grande importance
   mathématique} car le dogme « orthodoxe » est que :
 \begin{center}
-Les mathématiques se font dans la « théorie des ensembles\\de
+Les mathématiques se font dans la « théorie des ensembles\\ de
 Zermelo-Fraenkel en logique du premier ordre » ($\mathsf{ZFC}$).
 \end{center}
 
@@ -1406,7 +1413,7 @@ f(n,u_n)$, ou en OCaml
 
 {\footnotesize\tt
 let recurr = fun c -> fun f -> let rec u = fun n -> if n==0 then c
-else f (n-1) (u (n-1)) in u ;;\\
+else f (n-1) (u (n-1)) in u ;;\newline
 {\color{purple}val recurr : 'a -> (int -> 'a -> 'a) -> int -> 'a = <fun>}
 \par}