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