| author | Christian Urban <christian.urban@kcl.ac.uk> | 
| Thu, 10 Nov 2022 23:44:35 +0000 | |
| changeset 895 | 550676e542d2 | 
| parent 871 | 358a72d7bf71 | 
| child 904 | 3faf015b7e24 | 
| permissions | -rw-r--r-- | 
| 704 | 1 | % !TEX program = xelatex | 
| 744 | 2 | \documentclass[dvipsnames,14pt,t,xelatex,aspectratio=169,xcolor={table}]{beamer}
 | 
| 315 
470922b46a63
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
224diff
changeset | 3 | \usepackage{../slides}
 | 
| 215 
828303e8e4af
updated slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 4 | \usepackage{../langs}
 | 
| 
828303e8e4af
updated slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
93diff
changeset | 5 | \usepackage{../data}
 | 
| 871 | 6 | \usepackage{../graphicss}
 | 
| 315 
470922b46a63
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
224diff
changeset | 7 | \usepackage{soul}
 | 
| 86 
6a7fe83820c8
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 8 | |
| 223 
e4b29b57f6a3
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 9 | \tikzset{onslide/.code args={<#1>#2}{%
 | 
| 
e4b29b57f6a3
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 10 |   \only<#1>{\pgfkeysalso{#2}} % \pgfkeysalso doesn't change the path
 | 
| 
e4b29b57f6a3
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 11 | }} | 
| 
e4b29b57f6a3
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 12 | |
| 
e4b29b57f6a3
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 13 | \makeatletter | 
| 
e4b29b57f6a3
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 14 | \newenvironment<>{btHighlight}[1][]
 | 
| 
e4b29b57f6a3
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 15 | {\begin{onlyenv}#2\begingroup\tikzset{bt@Highlight@par/.style={#1}}\begin{lrbox}{\@tempboxa}}
 | 
| 
e4b29b57f6a3
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 16 | {\end{lrbox}\bt@HL@box[bt@Highlight@par]{\@tempboxa}\endgroup\end{onlyenv}}
 | 
| 
e4b29b57f6a3
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 17 | |
| 
e4b29b57f6a3
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 18 | \newcommand<>\btHL[1][]{%
 | 
| 
e4b29b57f6a3
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 19 |   \only#2{\begin{btHighlight}[#1]\bgroup\aftergroup\bt@HL@endenv}%
 | 
| 
e4b29b57f6a3
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 20 | } | 
| 
e4b29b57f6a3
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 21 | \def\bt@HL@endenv{%
 | 
| 
e4b29b57f6a3
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 22 |   \end{btHighlight}%   
 | 
| 
e4b29b57f6a3
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 23 | \egroup | 
| 
e4b29b57f6a3
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 24 | } | 
| 
e4b29b57f6a3
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 25 | \newcommand{\bt@HL@box}[2][]{%
 | 
| 
e4b29b57f6a3
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 26 |   \tikz[#1]{%
 | 
| 
e4b29b57f6a3
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 27 |     \pgfpathrectangle{\pgfpoint{1pt}{0pt}}{\pgfpoint{\wd #2}{\ht #2}}%
 | 
| 
e4b29b57f6a3
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 28 |     \pgfusepath{use as bounding box}%
 | 
| 
e4b29b57f6a3
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 29 |     \node[anchor=base west, fill=orange!30,outer sep=0pt,inner xsep=1pt, inner ysep=0pt, rounded corners=3pt, minimum height=\ht\strutbox+1pt,#1]{\raisebox{1pt}{\strut}\strut\usebox{#2}};
 | 
| 
e4b29b57f6a3
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 30 | }% | 
| 
e4b29b57f6a3
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 31 | } | 
| 
e4b29b57f6a3
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 32 | \makeatother | 
| 
e4b29b57f6a3
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 33 | |
| 86 
6a7fe83820c8
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 34 | |
| 315 
470922b46a63
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
224diff
changeset | 35 | % beamer stuff | 
| 459 | 36 | \renewcommand{\slidecaption}{CFL 10, King's College London}
 | 
| 86 
6a7fe83820c8
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 37 | \newcommand{\bl}[1]{\textcolor{blue}{#1}}       
 | 
| 315 
470922b46a63
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
224diff
changeset | 38 | |
| 86 
6a7fe83820c8
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 39 | |
| 
6a7fe83820c8
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 40 | \begin{document}
 | 
| 
6a7fe83820c8
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 41 | |
| 
6a7fe83820c8
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 42 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 315 
470922b46a63
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
224diff
changeset | 43 | \begin{frame}[t]
 | 
| 86 
6a7fe83820c8
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 44 | \frametitle{%
 | 
| 
6a7fe83820c8
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 45 |   \begin{tabular}{@ {}c@ {}}
 | 
| 
6a7fe83820c8
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 46 | \\[-3mm] | 
| 459 | 47 | \LARGE Compilers and \\[-2mm] | 
| 744 | 48 | \LARGE Formal Languages\\[3mm] | 
| 86 
6a7fe83820c8
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 49 |   \end{tabular}}
 | 
| 
6a7fe83820c8
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 50 | |
| 
6a7fe83820c8
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 51 | \normalsize | 
| 
6a7fe83820c8
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 52 |   \begin{center}
 | 
| 
6a7fe83820c8
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 53 |   \begin{tabular}{ll}
 | 
| 704 | 54 | Email: & christian.urban at kcl.ac.uk\\ | 
| 744 | 55 | %Office Hours: & Thursdays 12 -- 14\\ | 
| 56 | %Location: & N7.07 (North Wing, Bush House)\\ | |
| 704 | 57 | Slides \& Progs: & KEATS (also homework is there)\\ | 
| 86 
6a7fe83820c8
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 58 |   \end{tabular}
 | 
| 
6a7fe83820c8
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 59 |   \end{center}
 | 
| 
6a7fe83820c8
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 60 | |
| 744 | 61 |   \begin{center}
 | 
| 62 |     \begin{tikzpicture}
 | |
| 63 | \node[drop shadow,fill=white,inner sep=0pt] | |
| 64 |       {\footnotesize\rowcolors{1}{capri!10}{white}
 | |
| 65 |         \begin{tabular}{|p{4.8cm}|p{4.8cm}|}\hline
 | |
| 66 | 1 Introduction, Languages & 6 While-Language \\ | |
| 67 | 2 Regular Expressions, Derivatives & 7 Compilation, JVM \\ | |
| 68 | 3 Automata, Regular Languages & 8 Compiling Functional Languages \\ | |
| 69 | 4 Lexing, Tokenising & 9 Optimisations \\ | |
| 70 |           5 Grammars, Parsing                & \cellcolor{blue!50}10 LLVM \\ \hline
 | |
| 71 |         \end{tabular}%
 | |
| 72 | }; | |
| 73 |     \end{tikzpicture}
 | |
| 74 |   \end{center}
 | |
| 315 
470922b46a63
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
224diff
changeset | 75 | \end{frame}
 | 
| 864 | 76 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 77 | ||
| 78 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 79 | \tikzstyle{sensor}=[draw, fill=blue!20, text width=3.8em, line width=1mm,
 | |
| 80 | text centered, minimum height=2em,drop shadow] | |
| 81 | \tikzstyle{ann} = [above, text width=4em, text centered]
 | |
| 82 | \tikzstyle{sc} = [sensor, text width=7em, fill=red!20, 
 | |
| 83 | minimum height=6em, rounded corners, drop shadow,line width=1mm] | |
| 84 | ||
| 85 | \begin{frame}[fragile,c]
 | |
| 86 | \frametitle{LLVM: Overview}
 | |
| 87 | ||
| 88 | \begin{tikzpicture}
 | |
| 89 | % Validation Layer is the same except that there are a set of nodes and links which are added | |
| 90 | ||
| 91 |     \path (0,0) node (IR) [sc] {\textbf{LLVM-IR}\\ Optimisations};
 | |
| 92 |     \path (IR.west)+(-2.2,1.7) node (sou1) [sensor] {C++};
 | |
| 93 |     \path (IR.west)+(-2.2,0.5) node (sou2)[sensor] {C};
 | |
| 94 |     \path (IR.west)+(-2.2,-1.0) node (dots)[ann] {$\vdots$}; 
 | |
| 95 |     \path (IR.west)+(-2.2,-1.8) node (sou3)[sensor] {Haskell};    
 | |
| 96 | ||
| 97 |     \path [draw,->,line width=1mm] (sou1.east) -- node [above] {} (IR.160);
 | |
| 98 |     \path [draw,->,line width=1mm] (sou2.east) -- node [above] {} (IR.180);
 | |
| 99 |     \path [draw,->,line width=1mm] (sou3.east) -- node [above] {} (IR.200);
 | |
| 100 | ||
| 101 |     \path (IR.east)+(2.2,2.0)  node (tar1)[sensor] {x86};
 | |
| 102 |     \path (IR.east)+(2.2,0.8)  node (tar2)[sensor] {ARM};
 | |
| 103 |     \path (IR.east)+(2.2,-0.4) node (tar3)[sensor] {MIPS}; 
 | |
| 104 |     \path (IR.east)+(2.2,-1.6) node (tar4)[sensor] {RISC}; 
 | |
| 105 |     \path (IR.east)+(2.2,-2.8) node (tar5)[sensor] {Power PC};
 | |
| 106 |     \path (IR.east)+(2.2,-4.2) node (dots2)[ann] {$\vdots$};
 | |
| 107 | ||
| 108 |     \path [draw,<-,line width=1mm] (tar1.west) -- node [above] {} (IR.10);
 | |
| 109 |     \path [draw,<-,line width=1mm] (tar2.west) -- node [above] {} (IR.5);
 | |
| 110 |     \path [draw,<-,line width=1mm] (tar3.west) -- node [above] {} (IR.0);
 | |
| 111 |     \path [draw,<-,line width=1mm] (tar4.west) -- node [above] {} (IR.-5);
 | |
| 112 |     \path [draw,<-,line width=1mm] (tar5.west) -- node [above] {} (IR.-10);
 | |
| 113 | ||
| 114 | \end{tikzpicture}
 | |
| 115 | \end{frame}
 | |
| 116 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 117 | ||
| 86 
6a7fe83820c8
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 118 | |
| 704 | 119 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 120 | \begin{frame}[c,fragile]
 | |
| 818 | 121 | \frametitle{Static Single-Assignment}  
 | 
| 122 | ||
| 123 | \bl{$(1 + a) + (3 + (b * 5))$}\bigskip\bigskip  
 | |
| 124 | ||
| 125 | \begin{lstlisting}[language=LLVMIR,numbers=left]
 | |
| 126 | let tmp0 = add 1 a in | |
| 127 | let tmp1 = mul b 5 in | |
| 128 | let tmp2 = add 3 tmp1 in | |
| 129 | let tmp3 = add tmp0 tmp2 | |
| 130 | in tmp3 | |
| 131 | \end{lstlisting}  
 | |
| 132 | ||
| 133 | ||
| 134 | \end{frame}
 | |
| 135 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 136 | ||
| 137 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 138 | \begin{frame}[c,fragile]
 | |
| 139 | \small | |
| 140 | ||
| 141 | \mbox{}\bigskip\bigskip\bigskip
 | |
| 142 | ||
| 864 | 143 | \begin{lstlisting}[language=llvm,numbers=left]
 | 
| 818 | 144 | define i32 @fact (i32 %n) {
 | 
| 145 | %tmp_20 = icmp eq i32 %n, 0 | |
| 146 | br i1 %tmp_20, label %if_branch_24, label %else_branch_25 | |
| 147 | if_branch_24: | |
| 148 | ret i32 1 | |
| 149 | else_branch_25: | |
| 150 | %tmp_22 = sub i32 %n, 1 | |
| 151 | %tmp_23 = call i32 @fact (i32 %tmp_22) | |
| 152 | %tmp_21 = mul i32 %n, %tmp_23 | |
| 153 | ret i32 %tmp_21 | |
| 154 | } | |
| 155 | \end{lstlisting}  
 | |
| 156 | ||
| 157 | \begin{lstlisting}[language={},numbers=none]
 | |
| 158 | def fact(n) = if n == 0 then 1 else n * fact(n - 1) | |
| 159 | \end{lstlisting}  
 | |
| 160 | \end{frame}
 | |
| 161 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 162 | ||
| 864 | 163 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 164 | \begin{frame}[fragile,c]
 | |
| 165 | \frametitle{LLVM Types}
 | |
| 166 | ||
| 167 | \tt | |
| 168 | \begin{center}
 | |
| 169 | \begin{tabular}{ll}
 | |
| 170 | boolean & i1 \\ | |
| 171 | byte & i8 \\ | |
| 172 | short & i16\\ | |
| 173 | char & i16\\ | |
| 174 | integer & i32\\ | |
| 175 | long & i64\\ | |
| 176 | float & float\\ | |
| 177 | double & double\\ | |
| 178 | *\_ & pointer to \\ | |
| 179 | **\_ & pointer to a pointer to\\ | |
| 180 | \mbox{}[\_]    & arrays of\\
 | |
| 181 | \end{tabular}
 | |
| 182 | \end{center}
 | |
| 183 | ||
| 184 | \end{frame}
 | |
| 185 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 186 | ||
| 187 | ||
| 818 | 188 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 189 | \begin{frame}[c,fragile]
 | |
| 190 | ||
| 191 | ||
| 192 | \begin{lstlisting}[language=LLVM,numbers=none]
 | |
| 193 | br i1 %var, label %if_br, label %else_br | |
| 194 | ||
| 195 | icmp eq i32 %x, %y ; for equal | |
| 196 | icmp sle i32 %x, %y ; signed less or equal | |
| 197 | icmp slt i32 %x, %y ; signed less than | |
| 198 | icmp ult i32 %x, %y ; unsigned less than | |
| 199 | ||
| 200 | %var = call i32 @foo(...args...) | |
| 201 | \end{lstlisting}  
 | |
| 202 | ||
| 203 | \end{frame}
 | |
| 204 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 205 | ||
| 864 | 206 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 207 | \begin{frame}[fragile,c]
 | |
| 208 | \frametitle{Abstract Syntax Trees}
 | |
| 209 | \footnotesize | |
| 210 | ||
| 211 | \begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-3mm]
 | |
| 212 | // Fun language (expressions) | |
| 213 | abstract class Exp | |
| 214 | abstract class BExp | |
| 215 | ||
| 216 | case class Call(name: String, args: List[Exp]) extends Exp | |
| 217 | case class If(a: BExp, e1: Exp, e2: Exp) extends Exp | |
| 218 | case class Write(e: Exp) extends Exp | |
| 219 | case class Var(s: String) extends Exp | |
| 220 | case class Num(i: Int) extends Exp | |
| 221 | case class Aop(o: String, a1: Exp, a2: Exp) extends Exp | |
| 222 | case class Sequence(e1: Exp, e2: Exp) extends Exp | |
| 223 | case class Bop(o: String, a1: Exp, a2: Exp) extends BExp | |
| 224 | \end{lstlisting}
 | |
| 225 | ||
| 226 | \end{frame}
 | |
| 227 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 228 | ||
| 229 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 230 | \begin{frame}[fragile,c]
 | |
| 231 | \frametitle{K-(Intermediate)Language}
 | |
| 232 | \footnotesize | |
| 233 | ||
| 234 | \begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-3mm]
 | |
| 235 | abstract class KExp | |
| 236 | abstract class KVal | |
| 237 | ||
| 238 | // K-Values | |
| 239 | case class KVar(s: String) extends KVal | |
| 240 | case class KNum(i: Int) extends KVal | |
| 241 | case class Kop(o: String, v1: KVal, v2: KVal) extends KVal | |
| 242 | case class KCall(o: String, vrs: List[KVal]) extends KVal | |
| 243 | case class KWrite(v: KVal) extends KVal | |
| 244 | ||
| 245 | // K-Expressions | |
| 246 | case class KIf(x1: String, e1: KExp, e2: KExp) extends KExp | |
| 247 | case class KLet(x: String, v: KVal, e: KExp) extends KExp | |
| 248 | case class KReturn(v: KVal) extends KExp | |
| 249 | \end{lstlisting}
 | |
| 250 | ||
| 251 | \end{frame}
 | |
| 252 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 253 | ||
| 254 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 255 | \begin{frame}[fragile,c]
 | |
| 256 | \frametitle{KLet}
 | |
| 257 | ||
| 258 | \begin{lstlisting}[language=LLVM]
 | |
| 259 | tmp0 = add 1 a | |
| 260 | tmp1 = mul b 5 | |
| 261 | tmp2 = add 3 tmp1 | |
| 262 | tmp3 = add tmp0 tmp2 | |
| 263 | \end{lstlisting}
 | |
| 264 | ||
| 265 | \begin{lstlisting}[language=LLVMIR]
 | |
| 266 | KLet tmp0 , add 1 a in | |
| 267 | KLet tmp1 , mul b 5 in | |
| 268 | KLet tmp2 , add 3 tmp1 in | |
| 269 | KLet tmp3 , add tmp0 tmp2 in | |
| 270 | ... | |
| 271 | \end{lstlisting}
 | |
| 272 | ||
| 273 | \begin{lstlisting}[language=Scala,numbers=none]
 | |
| 274 | case class KLet(x: String, e1: KVal, e2: KExp) | |
| 275 | \end{lstlisting}
 | |
| 276 | ||
| 277 | \end{frame}
 | |
| 278 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 279 | ||
| 280 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 281 | \begin{frame}[fragile,c]
 | |
| 282 | \frametitle{KLet}
 | |
| 283 | ||
| 284 | \begin{lstlisting}[language=LLVM]
 | |
| 285 | tmp0 = add 1 a | |
| 286 | tmp1 = mul b 5 | |
| 287 | tmp2 = add 3 tmp1 | |
| 288 | tmp3 = add tmp0 tmp2 | |
| 289 | \end{lstlisting}
 | |
| 290 | ||
| 291 | \begin{lstlisting}[language=LLVMIR]
 | |
| 292 | let tmp0 = add 1 a in | |
| 293 | let tmp1 = mul b 5 in | |
| 294 | let tmp2 = add 3 tmp1 in | |
| 295 | let tmp3 = add tmp0 tmp2 in | |
| 296 | ... | |
| 297 | \end{lstlisting}
 | |
| 298 | ||
| 299 | \begin{lstlisting}[language=Scala,numbers=none]
 | |
| 300 | case class KLet(x: String, e1: KVal, e2: KExp) | |
| 301 | \end{lstlisting}
 | |
| 302 | ||
| 303 | \end{frame}
 | |
| 304 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 305 | ||
| 306 | ||
| 307 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 308 | \begin{frame}[fragile,c]
 | |
| 309 | \frametitle{CPS-Translation}
 | |
| 310 | \small | |
| 311 | ||
| 312 | \begin{lstlisting}[language=Scala,numbers=none]
 | |
| 313 | def CPS(e: Exp)(k: KVal => KExp) : KExp = | |
| 314 |   e match { ... }
 | |
| 315 | \end{lstlisting}
 | |
| 316 | \bigskip\bigskip | |
| 317 | ||
| 318 | the continuation \texttt{k} can be thought of:\medskip
 | |
| 319 | ||
| 320 | \small | |
| 321 | \begin{lstlisting}[language=LLVMIR,numbers=none,xleftmargin=30mm,escapeinside={(*@}{@*)}]
 | |
| 322 | let tmp0 = add 1 a in | |
| 323 | let tmp1 = mul (*@$\Box$@*) 5 in | |
| 324 | let tmp2 = add 3 tmp1 in | |
| 325 | let tmp3 = add tmp0 tmp2 in | |
| 326 | KReturn tmp3 | |
| 327 | \end{lstlisting}
 | |
| 328 | ||
| 329 | \end{frame}
 | |
| 330 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 331 | ||
| 332 | ||
| 333 | ||
| 818 | 334 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 335 | \begin{frame}[c,fragile]
 | |
| 704 | 336 | |
| 337 | ||
| 338 | \begin{lstlisting}[language=Scala, numbers=none, xleftmargin=-6mm]
 | |
| 339 | def fact(n: Int) : Int = {
 | |
| 340 | if (n == 0) 1 else n * fact(n - 1) | |
| 341 | } | |
| 342 | ||
| 343 | ||
| 344 | def factC(n: Int, ret: Int => Int) : Int = {
 | |
| 345 | if (n == 0) ret(1) | |
| 346 | else factC(n - 1, x => ret(n * x)) | |
| 347 | } | |
| 348 | ||
| 349 | fact(10) | |
| 350 | factC(10, identity) | |
| 351 | \end{lstlisting}
 | |
| 352 | \end{frame}
 | |
| 353 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 354 | ||
| 355 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 356 | \begin{frame}[c,fragile]
 | |
| 357 | ||
| 358 | ||
| 359 | \begin{lstlisting}[language=Scala, numbers=none, xleftmargin=-6mm]
 | |
| 360 | def fibC(n: Int, ret: Int => Int) : Int = {
 | |
| 361 | if (n == 0 || n == 1) ret(1) else | |
| 362 | fibC(n - 1, | |
| 363 | r1 => fibC(n - 2, | |
| 364 | r2 => ret(r1 + r2))) | |
| 365 | } | |
| 366 | ||
| 367 | fibC(10, identity) | |
| 368 | \end{lstlisting}
 | |
| 369 | \end{frame}
 | |
| 370 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 371 | ||
| 372 | ||
| 373 | ||
| 374 | ||
| 543 | 375 | |
| 376 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 377 | \begin{frame}[c]
 | |
| 378 | ||
| 704 | 379 |   \Large\bf Are there more strings in \\ \hfill\bl{$L(a^*)$} or
 | 
| 617 | 380 |   \bl{$L((a + b)^*)$}?
 | 
| 543 | 381 | |
| 382 | \end{frame}
 | |
| 383 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 384 | ||
| 385 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 386 | \begin{frame}[c]
 | |
| 704 | 387 | \frametitle{Can you remember this HW?}
 | 
| 388 | ||
| 389 |   \begin{itemize}
 | |
| 390 | \item (1) How many basic regular expressions are there to match | |
| 391 |       the string \bl{$abcd$}? 
 | |
| 392 | \item (2) How many if they cannot include | |
| 393 |       \bl{$\ONE$} and \bl{$\ZERO$}? 
 | |
| 394 | \item (3) How many if they are also not | |
| 395 | allowed to contain stars? | |
| 396 | \item (4) How many if they are also | |
| 397 |       not allowed to contain \bl{$\_ + \_$}?
 | |
| 398 |    \end{itemize}  
 | |
| 399 | ||
| 400 | \end{frame}
 | |
| 401 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 402 | ||
| 403 | ||
| 404 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 405 | \begin{frame}[c]
 | |
| 543 | 406 | |
| 407 | \Large\bf There are more problems, than there are | |
| 408 | programs.\bigskip\bigskip\pause\\ | |
| 409 | ||
| 410 | There must be a problem for which there is no program. | |
| 411 | \end{frame}
 | |
| 412 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 413 | ||
| 414 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 415 | \begin{frame}[c]
 | |
| 416 | \frametitle{Subsets}
 | |
| 417 | ||
| 418 | \Large | |
| 419 | If \bl{$A \subseteq B$} then \bl{$A$} has fewer or equal elements 
 | |
| 420 | than \bl{$B$}\bigskip\bigskip
 | |
| 421 | ||
| 422 | \Large | |
| 423 | \bl{$A \subseteq B$} and \bl{$B \subseteq A$}\bigskip
 | |
| 424 | ||
| 425 | then \bl{$A = B$}
 | |
| 426 | \end{frame}
 | |
| 427 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 428 | ||
| 429 | ||
| 430 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 431 |   \begin{frame}[c]
 | |
| 432 | ||
| 433 |   \begin{center}
 | |
| 434 |   \begin{tikzpicture}
 | |
| 435 | ||
| 436 | \draw (-4,2.5) node [scale=2.5] (X) | |
| 437 |     {\begin{tabular}{l}
 | |
| 438 |      $\{$  
 | |
| 439 |      \!\includegraphics[scale=0.02]{../pics/o1.jpg},
 | |
| 440 |      \includegraphics[scale=0.02]{../pics/o2.jpg},
 | |
| 441 |      \!\includegraphics[scale=0.02]{../pics/o3.jpg},
 | |
| 442 |      \includegraphics[scale=0.02]{../pics/o4.jpg},
 | |
| 443 |      \!\includegraphics[scale=0.027]{../pics/o5.jpg}
 | |
| 444 | $\}$ | |
| 445 |     \end{tabular}};
 | |
| 446 | ||
| 447 | \draw (-5.6,-2.5) node [scale=2.5] (Y) | |
| 448 |     {\begin{tabular}{l}
 | |
| 449 |      $\{$  
 | |
| 450 |      \!\includegraphics[scale=0.059]{../pics/a1.jpg},
 | |
| 451 |      \includegraphics[scale=0.048]{../pics/a2.jpg},
 | |
| 452 |      \includegraphics[scale=0.02]{../pics/a3.jpg}
 | |
| 453 | $\}$ | |
| 454 |     \end{tabular}};
 | |
| 455 | ||
| 456 |      \draw (0,1.5) node (X1) {5 elements};
 | |
| 457 |      \draw (0,-3.5) node (y1) {3 elements};
 | |
| 458 |   \end{tikzpicture}
 | |
| 459 |   \end{center}
 | |
| 460 | ||
| 461 |   \end{frame}
 | |
| 462 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 463 | ||
| 464 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 465 |   \begin{frame}[c]
 | |
| 466 |   \frametitle{Newton vs Feynman}
 | |
| 467 | ||
| 468 |   \begin{center}
 | |
| 469 |   \begin{tabular}{cc}
 | |
| 470 |   \includegraphics[scale=0.2]{../pics/newton.jpg} &
 | |
| 471 |   \includegraphics[scale=0.2]{../pics/feynman.jpg}\\
 | |
| 472 | classical physics & quantum physics | |
| 473 |   \end{tabular}
 | |
| 474 |   \end{center}
 | |
| 475 |   \end{frame}
 | |
| 476 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 477 | ||
| 478 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 479 |   \begin{frame}[c]
 | |
| 480 |   \frametitle{The Goal of the Talk}
 | |
| 481 | \large | |
| 482 |   \begin{itemize}
 | |
| 483 | \item show you that something very unintuitive happens with very large sets | |
| 484 | \bigskip\bigskip | |
| 485 | ||
| 486 |   \item convince you that there are more {\bf problems} than {\bf programs}
 | |
| 487 |   \end{itemize}	
 | |
| 488 |   \end{frame}
 | |
| 489 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 490 | ||
| 491 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 492 | \begin{frame}[t]
 | |
| 493 | % | |
| 494 |   \begin{center}
 | |
| 495 |   \begin{tikzpicture}
 | |
| 496 | ||
| 497 | \draw (-5,2.5) node [scale=2.3] (X) | |
| 498 |     {\begin{tabular}{@ {\hspace{-3mm}}l}
 | |
| 499 |      \bl{$B$ $=$ $\{$  
 | |
| 500 |      \!\includegraphics[scale=0.02]{../pics/o1.jpg},
 | |
| 501 |      \includegraphics[scale=0.02]{../pics/o2.jpg},
 | |
| 502 |      \!\includegraphics[scale=0.02]{../pics/o3.jpg},
 | |
| 503 |      \includegraphics[scale=0.02]{../pics/o4.jpg},
 | |
| 504 |      \!\includegraphics[scale=0.027]{../pics/o5.jpg}
 | |
| 505 | $\}$} | |
| 506 |     \end{tabular}};
 | |
| 507 | ||
| 508 | \draw (-6.6,-0.5) node [scale=2.3] (Y) | |
| 509 |     {\begin{tabular}{@ {\hspace{-3mm}}l}
 | |
| 510 |      \bl{$A$ $=$ $\{$  
 | |
| 511 |      \!\includegraphics[scale=0.059]{../pics/a1.jpg},
 | |
| 512 |      \includegraphics[scale=0.048]{../pics/a2.jpg},
 | |
| 513 |      \includegraphics[scale=0.02]{../pics/a3.jpg}
 | |
| 514 | $\}$} | |
| 515 |      \end{tabular}};
 | |
| 516 | ||
| 517 |      \only<1>{\draw (-5, -3) node[scale=2] 
 | |
| 518 |        {\bl{$|A|$ $=$ $5$}, \bl{$|B|$ $=$ $3$}};}
 | |
| 519 |      \only<2>{
 | |
| 520 | \draw [->, line width=1mm, red] (-7.4, 0.2) -- (-6.1, 2.1); | |
| 521 | \draw [->, line width=1mm, red] (-5.8, 0.2) -- (-3.1, 2.1); | |
| 522 | \draw [->, line width=1mm, red] (-4.5, 0.2) -- (-7.6, 2.1); | |
| 523 |        \draw (-5, -3) node[scale=2] {then \bl{$|A|$ $\le$ $|B|$}};
 | |
| 524 | } | |
| 525 |     \only<3>{
 | |
| 526 | \draw [<-, line width=1mm, red] (-7.5, 0.2) -- (-6.1, 2.1); | |
| 527 | \draw [<-, line width=1mm, red] (-7.3, 0.2) -- (-3.1, 2.1); | |
| 528 | \draw [<-, line width=1mm, red] (-6, 0.2) -- (-7.5, 2.1); | |
| 529 | \draw [<-, line width=1mm, red] (-4.5, 0.2) -- (-4.5, 2.1); | |
| 530 | \draw [<-, line width=1mm, red] (-4.3, 0.2) -- (-1.3, 2.1); | |
| 531 | ||
| 532 |        \draw (-5, -3) node[scale=1.5] {\small{}for \bl{$=$}
 | |
| 533 |         has to be a {\bf one-to-one} mapping};
 | |
| 534 | } | |
| 535 | ||
| 536 | ||
| 537 |   \end{tikzpicture}
 | |
| 538 |   \end{center}
 | |
| 539 | ||
| 540 | \end{frame}
 | |
| 541 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 542 | ||
| 543 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 544 | \begin{frame}[c]
 | |
| 545 | \frametitle{Cardinality}
 | |
| 546 | ||
| 547 | \Large | |
| 548 | \bl{$|A|$} $\dn$ ``how many elements''\bigskip\\
 | |
| 549 | ||
| 550 | \bl{$A \subseteq B  \Rightarrow |A| \leq |B|$}\bigskip\\\pause
 | |
| 551 | ||
| 552 | if there is an injective function \bl{$f: A \rightarrow B$} then \bl{$|A| \leq |B|$}\
 | |
| 553 | ||
| 554 | \begin{center}
 | |
| 555 | \bl{\large$\forall x y.\; f(x) = f(y) \Rightarrow x = y$}
 | |
| 556 | \end{center}
 | |
| 557 | \end{frame}
 | |
| 558 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 559 | ||
| 560 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 561 | \begin{frame}[t]
 | |
| 562 | ||
| 563 |   \begin{center}
 | |
| 564 |   \begin{tikzpicture}
 | |
| 565 | ||
| 566 | \draw (-6.6,2.5) node [scale=2.3] (X) | |
| 567 |     {\begin{tabular}{@ {\hspace{-3mm}}l}
 | |
| 568 |      $A$ $=$ $\{$  
 | |
| 569 |      \!\includegraphics[scale=0.02]{../pics/o1.jpg},
 | |
| 570 |      \includegraphics[scale=0.02]{../pics/o2.jpg},
 | |
| 571 |      \!\includegraphics[scale=0.02]{../pics/o3.jpg}
 | |
| 572 | $\}$ | |
| 573 |     \end{tabular}};
 | |
| 574 | ||
| 575 | \draw (-6.6,-0.5) node [scale=2.3] (Y) | |
| 576 |     {\begin{tabular}{@ {\hspace{-3mm}}l}
 | |
| 577 |      $B$ $=$ $\{$  
 | |
| 578 |      \!\includegraphics[scale=0.059]{../pics/a1.jpg},
 | |
| 579 |      \includegraphics[scale=0.048]{../pics/a2.jpg},
 | |
| 580 |      \includegraphics[scale=0.02]{../pics/a3.jpg}
 | |
| 581 | $\}$ | |
| 582 |      \end{tabular}};
 | |
| 583 |    \onslide<3->{\draw (-7, -3) node[scale=1.5] 
 | |
| 584 |       {then \bl{$|A|$ \alert{$=$} $|B|$}};}
 | |
| 585 |      \only<1>{
 | |
| 586 | \draw [->, line width=1mm, red] (-7.4, 0.2) -- (-6.1, 2.1); | |
| 587 | \draw [->, line width=1mm, red] (-5.8, 0.2) -- (-4.3, 2.1); | |
| 588 | \draw [->, line width=1mm, red] (-4.5, 0.2) -- (-7.6, 2.1); | |
| 589 | } | |
| 590 |     \only<2->{
 | |
| 591 | \draw [<-, line width=1mm, blue] (-7.5, 0.2) -- (-7.5, 2.1); | |
| 592 | \draw [<-, line width=1mm, blue] (-5.8, 0.2) -- (-4.3, 2.1); | |
| 593 | \draw [<-, line width=1mm, blue] (-4.5, 0.2) -- (-6.1, 2.1); | |
| 594 | } | |
| 595 | ||
| 596 | ||
| 597 |   \end{tikzpicture}
 | |
| 598 |   \end{center}
 | |
| 599 | ||
| 600 | \end{frame}
 | |
| 601 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 315 
470922b46a63
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
224diff
changeset | 602 | |
| 86 
6a7fe83820c8
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 603 | |
| 543 | 604 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 605 | \begin{frame}[c]
 | |
| 606 | \frametitle{Natural Numbers}
 | |
| 607 | ||
| 608 | \Large | |
| 609 | \bl{$\mathbb{N}$} \bl{$\dn$} \bl{$\{0, 1, 2, 3, .......\}$}\bigskip\pause 
 | |
| 610 | ||
| 611 | \bl{$A$} is \alert{countable} iff \bl{$|A| \leq |\mathbb{N}|$}
 | |
| 612 | ||
| 613 | \end{frame}
 | |
| 614 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 615 | ||
| 616 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 617 | \begin{frame}[c]
 | |
| 618 | \frametitle{First Question}
 | |
| 619 | ||
| 620 | \Large | |
| 621 | \bl{$|\mathbb{N} - \{0\}|   \;\;\;\alert{?}\;\;\;  |\mathbb{N}| $}\bigskip\bigskip 
 | |
| 622 | ||
| 623 | \large | |
| 624 | \bl{$\geq$} or \bl{$\leq$} or \bl{$=$} ?
 | |
| 625 | \bigskip\bigskip\bigskip\pause | |
| 626 | ||
| 627 | \bl{$x$ $\mapsto$ $x + 1$},\\  \bl{$|\mathbb{N} - \{0\}|$ $=$  
 | |
| 628 | $|\mathbb{N}|$}
 | |
| 629 | \end{frame}
 | |
| 630 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 631 | ||
| 632 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 633 | \mode<presentation>{
 | |
| 634 | \begin{frame}[c]
 | |
| 635 | ||
| 636 | \Large | |
| 637 | \bl{$|\mathbb{N} - \{0, 1\}|   \;\;\;\alert{?}\;\;\;  |\mathbb{N}| $}\bigskip\pause 
 | |
| 638 | ||
| 639 | \bl{$|\mathbb{N} - \mathbb{O}|   \;\;\;\alert{?}\;\;\;  |\mathbb{N}| $}\bigskip\bigskip
 | |
| 640 | ||
| 641 | \normalsize | |
| 642 | \bl{$\mathbb{O}$} $\dn$ odd numbers\quad   \bl{$\{1,3,5......\}$}\\ \pause
 | |
| 643 | \bl{$\mathbb{E}$} $\dn$ even numbers\quad   \bl{$\{0,2,4......\}$}\\
 | |
| 644 | \end{frame}}
 | |
| 645 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 646 | ||
| 647 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 648 | \mode<presentation>{
 | |
| 649 | \begin{frame}[c]
 | |
| 650 | ||
| 651 | \Large | |
| 652 | \bl{$|\mathbb{N} \cup \mathbb{-N}|   \;\;\;\alert{?}\;\;\;  |\mathbb{N}| $}\bigskip\bigskip
 | |
| 653 | ||
| 654 | ||
| 655 | \normalsize | |
| 656 | \bl{$\mathbb{\phantom{-}N}$} $\dn$ positive numbers\quad   \bl{$\{0,1,2,3,......\}$}\\
 | |
| 657 | \bl{$\mathbb{-N}$} $\dn$ negative numbers\quad   \bl{$\{0,-1,-2,-3,......\}$}\\
 | |
| 658 | \end{frame}}
 | |
| 659 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 660 | ||
| 661 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 662 | \mode<presentation>{
 | |
| 663 | \begin{frame}[c]
 | |
| 664 | ||
| 665 | \Large | |
| 666 | \bl{$A$} is \alert{countable} if there exists an injective \bl{$f : A \rightarrow \mathbb{N}$}\bigskip
 | |
| 667 | ||
| 668 | \bl{$A$} is \alert{uncountable} if there does not exist an injective \bl{$f : A \rightarrow \mathbb{N}$}\bigskip\bigskip 
 | |
| 669 | ||
| 670 | ||
| 671 | countable:  \bl{$|A| \leq |\mathbb{N}|$}\\
 | |
| 672 | uncountable:  \bl{$|A| > |\mathbb{N}|$}\pause\bigskip
 | |
| 673 | ||
| 674 | ||
| 675 | Does there exist such an \bl{$A$} ?
 | |
| 676 | ||
| 677 | \end{frame}}
 | |
| 678 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 679 | ||
| 680 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 681 |   \mode<presentation>{
 | |
| 682 |   \begin{frame}[c]
 | |
| 683 |   \frametitle{Hilbert's Hotel}
 | |
| 684 | ||
| 685 |   \begin{center}
 | |
| 686 |  \includegraphics[scale=0.8]{../pics/hilberts_hotel.jpg}
 | |
| 687 |   \end{center}
 | |
| 688 | ||
| 689 |   \begin{itemize}
 | |
| 690 | \item \ldots has as many rooms as there are natural numbers | |
| 691 |   \end{itemize}
 | |
| 692 | ||
| 693 |   \end{frame}}
 | |
| 694 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 695 | ||
| 696 | ||
| 697 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 698 | \begin{frame}[t]
 | |
| 699 |  \frametitle{\begin{tabular}{c}Real Numbers between\\[-2mm] 0 and 1\end{tabular}}
 | |
| 700 | ||
| 701 |   \begin{center}
 | |
| 702 |   \begin{tikzpicture}
 | |
| 703 | \draw [fill, color=black!50] (1,4) rectangle (2, 3); | |
| 704 | \draw [fill, color=black!50] (2,3) rectangle (3, 2); | |
| 705 | \draw [fill, color=black!50] (3,2) rectangle (4, 1); | |
| 706 | \draw [fill, color=black!50] (4,1) rectangle (5, 0); | |
| 707 | \draw (0, 0) grid (8, 5); | |
| 708 | \draw [line width = 1.mm] (1,0) -- (1, 5); | |
| 709 | \draw [line width = 1.mm] (0, 4) -- (8, 4); | |
| 710 |   \draw (0.5,3.5) node {$1$};
 | |
| 711 |   \draw (0.5,2.5) node {$2$};
 | |
| 712 |   \draw (0.5,1.5) node {$3$};
 | |
| 713 |   \draw (0.5,0.5) node {$4$};
 | |
| 714 | ||
| 715 |   \draw (1.5,3.5) node {\only<1>{$3$}\only<2->{$4$}};
 | |
| 716 |   \draw (2.5,3.5) node {$3$};
 | |
| 717 |   \draw (3.5,3.5) node {$3$};
 | |
| 718 |   \draw (4.5,3.5) node {$3$};
 | |
| 719 |   \draw (5.5,3.5) node {$3$};
 | |
| 720 |   \draw (6.5,3.5) node {$3$};
 | |
| 721 |   \draw (7.5,3.5) node {$\ldots$};
 | |
| 722 | ||
| 723 |   \draw (1.5,2.5) node {$1$};
 | |
| 724 |   \draw (2.5,2.5) node {\only<1-2>{$2$}\only<3->{$3$}};
 | |
| 725 |   \draw (3.5,2.5) node {$3$};
 | |
| 726 |   \draw (4.5,2.5) node {$4$};
 | |
| 727 |   \draw (5.5,2.5) node {$5$};
 | |
| 728 |   \draw (6.5,2.5) node {$6$};
 | |
| 729 |   \draw (7.5,2.5) node {$7$};
 | |
| 730 | ||
| 731 |   \draw (1.5,1.5) node {$0$};
 | |
| 732 |   \draw (2.5,1.5) node {$1$};
 | |
| 733 |   \draw (3.5,1.5) node {\only<1-3>{$0$}\only<4->{$1$}};
 | |
| 734 |   \draw (4.5,1.5) node {$1$};
 | |
| 735 |   \draw (5.5,1.5) node {$0$};
 | |
| 736 |   \draw (6.5,1.5) node {$\ldots$};
 | |
| 737 | ||
| 738 |    \draw (1.5,0.5) node {$7$};
 | |
| 739 |   \draw (2.5,0.5) node {$8$};
 | |
| 740 |   \draw (3.5,0.5) node {$5$};
 | |
| 741 |   \draw (4.5,0.5) node {\only<1-4>{$3$}\only<5->{$4$}};
 | |
| 742 |   \draw (5.5,0.5) node {$9$};
 | |
| 743 |   \draw (6.5,0.5) node {$\ldots$};
 | |
| 744 | ||
| 745 |    \draw (1.5,-0.5) node {$\ldots$};
 | |
| 746 |    \draw (8.5,3.5) node {$\ldots$};
 | |
| 747 |   \end{tikzpicture}
 | |
| 748 |   \end{center}
 | |
| 749 |   \mbox{}\\[-20mm]\mbox{}
 | |
| 750 | ||
| 751 |   \onslide<6->{
 | |
| 752 |   \begin{center}
 | |
| 753 |   \Large\bl{$|\mathbb{N}| < |R|$}
 | |
| 754 |   \end{center}
 | |
| 755 | } | |
| 756 | ||
| 757 | \end{frame}
 | |
| 758 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 759 | ||
| 760 | ||
| 761 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 762 | \mode<presentation>{
 | |
| 763 | \begin{frame}[t]
 | |
| 764 |  \frametitle{The Set of Problems}
 | |
| 765 | ||
| 766 | $\aleph_0$ | |
| 767 | ||
| 768 |   \begin{center}
 | |
| 769 |   \begin{tikzpicture}
 | |
| 770 | \draw [fill, color=black!50] (1,4) rectangle (2, 3); | |
| 771 | \draw [fill, color=black!50] (2,3) rectangle (3, 2); | |
| 772 | \draw [fill, color=black!50] (3,2) rectangle (4, 1); | |
| 773 | \draw [fill, color=black!50] (4,1) rectangle (5, 0); | |
| 774 | \draw (0, 0) grid (8, 5); | |
| 775 | \draw [line width = 1.mm] (1,0) -- (1, 5); | |
| 776 | \draw [line width = 1.mm] (0, 4) -- (8, 4); | |
| 777 |   \draw (0.5,3.5) node {$1$};
 | |
| 778 |   \draw (0.5,2.5) node {$2$};
 | |
| 779 |   \draw (0.5,1.5) node {$3$};
 | |
| 780 |   \draw (0.5,0.5) node {$4$};
 | |
| 781 | ||
| 782 |   \draw (1.5,4.5) node {$0$};
 | |
| 783 |   \draw (2.5,4.5) node {$1$};
 | |
| 784 |   \draw (3.5,4.5) node {$2$};
 | |
| 785 |   \draw (4.5,4.5) node {$3$};
 | |
| 786 |   \draw (5.5,4.5) node {$4$};
 | |
| 787 |   \draw (6.5,4.5) node {$5$};
 | |
| 788 |   \draw (7.5,4.5) node {$\ldots$}; 
 | |
| 789 | ||
| 790 |   \draw (1.5,3.5) node {$0$};
 | |
| 791 |   \draw (2.5,3.5) node {$1$};
 | |
| 792 |   \draw (3.5,3.5) node {$0$};
 | |
| 793 |   \draw (4.5,3.5) node {$1$};
 | |
| 794 |   \draw (5.5,3.5) node {$0$};
 | |
| 795 |   \draw (6.5,3.5) node {$1$};
 | |
| 796 |   \draw (7.5,3.5) node {$\ldots$};
 | |
| 797 | ||
| 798 |   \draw (1.5,2.5) node {$0$};
 | |
| 799 |   \draw (2.5,2.5) node {$0$};
 | |
| 800 |   \draw (3.5,2.5) node {$0$};
 | |
| 801 |   \draw (4.5,2.5) node {$1$};
 | |
| 802 |   \draw (5.5,2.5) node {$1$};
 | |
| 803 |   \draw (6.5,2.5) node {$0$};
 | |
| 804 |   \draw (7.5,2.5) node {$0$};
 | |
| 805 | ||
| 806 |   \draw (1.5,1.5) node {$0$};
 | |
| 807 |   \draw (2.5,1.5) node {$0$};
 | |
| 808 |   \draw (3.5,1.5) node {$0$};
 | |
| 809 |   \draw (4.5,1.5) node {$0$};
 | |
| 810 |   \draw (5.5,1.5) node {$0$};
 | |
| 811 |   \draw (6.5,1.5) node {$\ldots$};
 | |
| 812 | ||
| 813 |    \draw (1.5,0.5) node {$1$};
 | |
| 814 |   \draw (2.5,0.5) node {$1$};
 | |
| 815 |   \draw (3.5,0.5) node {$0$};
 | |
| 816 |   \draw (4.5,0.5) node {$1$};
 | |
| 817 |   \draw (5.5,0.5) node {$1$};
 | |
| 818 |   \draw (6.5,0.5) node {$\ldots$};
 | |
| 819 | ||
| 820 |   \draw (1.5,-0.5) node {$\ldots$};
 | |
| 821 |    \draw (8.5,3.5) node {$\ldots$};
 | |
| 822 | ||
| 823 |   \end{tikzpicture}
 | |
| 824 |   \end{center}
 | |
| 825 | ||
| 826 | ||
| 827 |   \onslide<2>{
 | |
| 828 |   \begin{center}
 | |
| 829 |   \large \bl{|Progs| $=$ $|\mathbb{N}|$ $<$ |Probs|}
 | |
| 830 |  \end{center}
 | |
| 831 | } | |
| 832 | ||
| 833 | ||
| 834 | \end{frame}}
 | |
| 835 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 836 | ||
| 837 | ||
| 838 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 839 | \mode<presentation>{
 | |
| 840 | \begin{frame}[c]
 | |
| 841 | \frametitle{Halting Problem}
 | |
| 842 | ||
| 843 | \large | |
| 844 | Assume a program \bl{$H$} that decides for all programs \bl{$A$} and all 
 | |
| 845 | input data \bl{$D$} whether\bigskip
 | |
| 846 | ||
| 847 | \begin{itemize}
 | |
| 848 | \item \bl{$H(A, D) \dn 1$} iff \bl{$A(D)$} terminates
 | |
| 849 | \item \bl{$H(A, D) \dn 0$} otherwise
 | |
| 850 | \end{itemize}
 | |
| 851 | ||
| 852 | \end{frame}}
 | |
| 853 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 854 | ||
| 855 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 856 | \mode<presentation>{
 | |
| 857 | \begin{frame}[c]
 | |
| 858 | \frametitle{Halting Problem (2)}
 | |
| 859 | ||
| 860 | \large | |
| 861 | Given such a program \bl{$H$} define the following program \bl{$C$}:
 | |
| 862 | for all programs \bl{$A$}\bigskip
 | |
| 863 | ||
| 864 | \begin{itemize}
 | |
| 865 | \item \bl{$C(A) \dn 0$} iff \bl{$H(A, A) = 0$} 
 | |
| 866 | \item \bl{$C(A) \dn$ loops} otherwise
 | |
| 867 | \end{itemize}
 | |
| 868 | ||
| 869 | \end{frame}}
 | |
| 870 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 871 | ||
| 872 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 873 | \mode<presentation>{
 | |
| 874 | \begin{frame}[c]
 | |
| 875 | \frametitle{Contradiction}
 | |
| 876 | ||
| 877 | ||
| 878 | \bl{$H(C, C)$} is either \bl{$0$} or \bl{$1$}.
 | |
| 879 | ||
| 880 | \begin{itemize}
 | |
| 881 | \item \bl{$H(C, C) = 1$} $\stackrel{\text{def}\,H}{\Rightarrow}$ \bl{$C(C)\downarrow$} $\stackrel{\text{def}\,C}{\Rightarrow}$ \bl{$H(C, C)=0$} 
 | |
| 882 | \item \bl{$H(C, C) = 0$} $\stackrel{\text{def}\,H}{\Rightarrow}$ \bl{$C(C)$} loops $\stackrel{\text{def}\,C}{\Rightarrow}$\\ 
 | |
| 883 | \hspace{7cm}\bl{$H(C, C)=1$} 
 | |
| 884 | \end{itemize}
 | |
| 885 | ||
| 886 | Contradiction in both cases. So \bl{$H$} cannot exist.
 | |
| 887 | ||
| 888 | \end{frame}}
 | |
| 889 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 890 | ||
| 891 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 892 |   \mode<presentation>{
 | |
| 893 |   \begin{frame}[c]
 | |
| 894 |   \frametitle{Take Home Points}
 | |
| 895 | \large | |
| 896 | ||
| 897 |   \begin{itemize}
 | |
| 898 | \item there are sets that are more infinite than others\bigskip | |
| 899 | \item even with the most powerful computer we can imagine, there | |
| 900 | are problems that cannot be solved by any program\bigskip\bigskip | |
| 901 | ||
| 902 | \item in CS we actually hit quite often such problems (halting problem) | |
| 903 |   \end{itemize}
 | |
| 904 | ||
| 905 |   \end{frame}}
 | |
| 906 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 864 | 907 | |
| 908 | \begin{frame}<1-20>[c]
 | |
| 909 | \end{frame}
 | |
| 910 | ||
| 911 | ||
| 86 
6a7fe83820c8
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 912 | \end{document}
 | 
| 
6a7fe83820c8
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 913 | |
| 
6a7fe83820c8
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 914 | %%% Local Variables: | 
| 
6a7fe83820c8
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 915 | %%% mode: latex | 
| 
6a7fe83820c8
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 916 | %%% TeX-master: t | 
| 
6a7fe83820c8
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 917 | %%% End: | 
| 
6a7fe83820c8
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 918 |