From e4b7f3f6fb971ce0ceba78ff86f32b9956ed912e Mon Sep 17 00:00:00 2001 From: "David A. Madore" Date: Wed, 8 Jan 2025 12:36:55 +0100 Subject: Fix display and numbering, esp. that of printed version. --- transp-inf110-02-typage.tex | 127 +++++++++++++++++++++++--------------------- 1 file changed, 67 insertions(+), 60 deletions(-) (limited to 'transp-inf110-02-typage.tex') 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{% \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 = }\\ -let pi2 = fun (x,y) -> y ;; (* $\pi_2$ *)\\ -{\color{purple}val pi2 : 'a * 'b -> 'b = }\\ -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 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 = }\newline +let pi2 = fun (x,y) -> y ;; (* $\pi_2$ *)\newline +{\color{purple}val pi2 : 'a * 'b -> 'b = }\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 = }\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 = } \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 = }\\ -let minus\_cps = fun x -> fun y -> fun k -> k(x-y) ;;\\ -{\color{purple}val minus\_cps : int -> int -> (int -> 'a) -> 'a = }\\ -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 = }\\ -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 = }\newline +let minus\_cps = fun x -> fun y -> fun k -> k(x-y) ;;\newline +{\color{purple}val minus\_cps : int -> int -> (int -> 'a) -> 'a = }\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 = }\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 = } @@ -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} -- cgit v1.2.3