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

1 files changed, 67 insertions, 60 deletions

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}