slides/slides10.tex
author Christian Urban <urbanc@in.tum.de>
Tue, 20 Nov 2018 08:00:16 +0000
changeset 606 a50feaa0c4b3
parent 543 16adebf18ef9
child 616 24bbe4e4b37b
permissions -rw-r--r--
updated
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     1
\documentclass[dvipsnames,14pt,t]{beamer}
315
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
     2
\usepackage{../slides}
215
828303e8e4af updated slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
     3
\usepackage{../langs}
828303e8e4af updated slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
     4
\usepackage{../data}
315
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
     5
\usepackage{../graphics}
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
     6
\usepackage{soul}
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     7
223
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
     8
\tikzset{onslide/.code args={<#1>#2}{%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
     9
  \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
    10
}}
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
\makeatletter
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    13
\newenvironment<>{btHighlight}[1][]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    14
{\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
    15
{\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
    16
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    17
\newcommand<>\btHL[1][]{%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    18
  \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
    19
}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    20
\def\bt@HL@endenv{%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    21
  \end{btHighlight}%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    22
  \egroup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    23
}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    24
\newcommand{\bt@HL@box}[2][]{%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    25
  \tikz[#1]{%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    26
    \pgfpathrectangle{\pgfpoint{1pt}{0pt}}{\pgfpoint{\wd #2}{\ht #2}}%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    27
    \pgfusepath{use as bounding box}%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    28
    \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
    29
  }%
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
\makeatother
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    32
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    33
315
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
    34
% beamer stuff
459
780486571e38 updated
Christian Urban <urbanc@in.tum.de>
parents: 315
diff changeset
    35
\renewcommand{\slidecaption}{CFL 10, King's College London}
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    36
\newcommand{\bl}[1]{\textcolor{blue}{#1}}       
315
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
    37
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    38
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    39
\begin{document}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    40
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    41
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
315
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
    42
\begin{frame}[t]
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    43
\frametitle{%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    44
  \begin{tabular}{@ {}c@ {}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    45
  \\[-3mm]
459
780486571e38 updated
Christian Urban <urbanc@in.tum.de>
parents: 315
diff changeset
    46
  \LARGE Compilers and \\[-2mm] 
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    47
  \LARGE Formal Languages (10)\\[3mm] 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    48
  \end{tabular}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    49
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    50
  \normalsize
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    51
  \begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    52
  \begin{tabular}{ll}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    53
  Email:  & christian.urban at kcl.ac.uk\\
500
c502933be072 updated
Christian Urban <urbanc@in.tum.de>
parents: 459
diff changeset
    54
  Office: & N7.07 (North Wing, Bush House)\\
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    55
  Slides: & KEATS (also home work is there)\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    56
  \end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    57
  \end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    58
315
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
    59
\end{frame}
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    60
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    61
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    62
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    63
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    64
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    65
315
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
    66
\large\bf
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
    67
Using a compiler, \\how can you mount the\\ perfect attack against a system?
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    68
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    69
\end{frame}}
223
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    70
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    71
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    72
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    73
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    74
\begin{frame}[c]
223
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    75
315
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
    76
{\large\bf
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
    77
What is a \alert{perfect} attack?}\bigskip
223
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    78
315
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
    79
\begin{enumerate}
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
    80
\item you can potentially completely take over a target system
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
    81
\item your attack is (nearly) undetectable
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
    82
\item the victim has (almost) no chance to recover
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
    83
\end{enumerate}
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    84
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    85
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    86
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    87
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    88
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    89
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    90
\begin{frame}[c]
315
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
    91
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    92
315
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
    93
  \begin{center}
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
    94
  \begin{tikzpicture}[scale=1]
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
    95
  
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
    96
  \onslide<1->{
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
    97
  \node (A) at (0,0)  [draw=black, rectangle, very thick, minimum height=18mm, minimum width=17mm] {};
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
    98
  \node [below right] at (A.north west) {\footnotesize\begin{tabular}{@{}l@{}}
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
    99
  \only<1,2>{clean}\only<3->{\alert{hacked}}\\compiler\end{tabular}};}
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   100
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   101
315
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   102
  \onslide<2->{
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   103
  \node (B) at (-2,2)  [draw=black, rectangle, very thick, minimum height=10mm, minimum width=12mm] {};
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   104
  \node [below right] at (B.north west) {\footnotesize\begin{tabular}{@{}l@{}}login\\(src)\end{tabular}};
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   105
  
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   106
  \node (C) at (2,2)  [draw=black, rectangle, very thick, minimum height=10mm, minimum width=12mm] {};
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   107
  \node [below right] at (C.north west) {\footnotesize\begin{tabular}{@{}l@{}}login\\(bin)\end{tabular}};
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   108
315
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   109
  \draw[->, line width=2mm] (B) -- (C);
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   110
  }
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   111
  
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   112
 \onslide<3->{\node [above left=-1.5mm] at (C.south east) {\footnotesize \alert{$\blacksquare$}};}
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   113
315
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   114
  \end{tikzpicture}
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   115
  \end{center}
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   116
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   117
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   118
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   120
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   121
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   122
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   123
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   124
315
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   125
  \begin{center}
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   126
  \begin{tikzpicture}[scale=1]
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   127
  
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   128
  \onslide<1->{
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   129
  \node (A) at (0,0)  [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   130
  \node [below right] at (A.north west) {\small V0.01};
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   131
  \node [below right] (A1) at (A.south west) {\small Scala};
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   132
  \node [below right] (A1) at (A1.south west) {\small\textcolor{gray}{host language}};
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   133
  \node [above right] at (A.north west) {my compiler (src)};}
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   134
315
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   135
  \onslide<2->{
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   136
  \node (B) at (1.8,0)  [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   137
  \node [below right] at (B.north west) {\small V0.02};
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   138
  \node [below right] at (B.south west) {\small Scala};
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   139
  \node at (3,0) {\ldots};
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   140
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   141
  \node (C) at (5,0)  [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   142
  \node [below right] at (C.north west) {\small V1.00};
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   143
  \node [below right] at (C.south west) {\small Scala};}
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   144
315
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   145
  \onslide<3->{
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   146
  \node (D) at (6.8,0)  [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   147
  \node [below right] at (D.north west) {\small V1.00};
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   148
315
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   149
  \node (E) at (6.8,2)  [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   150
  \node [below right] at (E.north west) {\small V1.01};}
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   151
  
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   152
  \onslide<4->{
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   153
  \node (F) at (8.6,0)  [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   154
  \node [below right] at (F.north west) {\small V1.01};
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   155
315
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   156
  \node (G) at (8.6,2)  [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   157
  \node [below right] at (G.north west) {\small V1.02};
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   158
  \node at (9.8,0) {\ldots};
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   159
  \node at (9.8,2) {\ldots};
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   160
  \node at (8,-2) {\textcolor{gray}{\begin{tabular}{@{}l@{}}no host language\\needed\end{tabular}}};
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   161
  }
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   162
  
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   163
  \end{tikzpicture}
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   164
  \end{center}
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   165
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   166
\end{frame}}
315
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   167
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   168
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   169
315
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   170
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   171
  \mode<presentation>{
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   172
  \begin{frame}<1-3>
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   173
  \frametitle{\LARGE\begin{tabular}{c}Hacking Compilers 
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   174
  \end{tabular}}
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   175
  
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   176
  %Why is it so paramount to have a small trusted code base (TCB)?
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   177
  \bigskip\bigskip
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   178
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   179
  \begin{columns}
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   180
  \begin{column}{2.7cm}
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   181
  \begin{minipage}{2.5cm}%
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   182
  \begin{tabular}{c@ {}}
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   183
  \includegraphics[scale=0.2]{../pics/ken-thompson.jpg}\\[-1.8mm]
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   184
  \footnotesize Ken Thompson\\[-1.8mm]
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   185
  \footnotesize Turing Award, 1983\\
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   186
  \end{tabular}
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   187
  \end{minipage}
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   188
  \end{column}
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   189
  \begin{column}{9cm}
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   190
  \begin{tabular}{l@ {\hspace{1mm}}p{8cm}}
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   191
 
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   192
  & Ken Thompson showed how to hide a Trojan Horse in a 
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   193
  compiler \textcolor{red}{without} leaving any traces in the source code.\\[2mm]
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   194
  
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   195
  & No amount of source level verification will protect 
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   196
  you from such Thompson-hacks.\\[2mm]
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   197
315
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   198
  \end{tabular}
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   199
  \end{column}
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   200
  \end{columns}
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   201
315
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   202
  \only<2>{
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   203
  \begin{textblock}{6}(4,2)
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   204
  \begin{tikzpicture}
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   205
  \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   206
  {\normalsize
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   207
  \begin{minipage}{8cm}
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   208
  \begin{quote}
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   209
  \includegraphics[scale=0.05]{../pics/evil.png}
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   210
  \begin{enumerate}
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   211
  \item[1)] Assume you ship the compiler as binary and also with sources.
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   212
  \item[2)] Make the compiler aware when it compiles itself.
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   213
  \item[3)] Add the Trojan horse.
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   214
  \item[4)] Compile.
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   215
  \item[5)] Delete Trojan horse from the sources of the compiler.
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   216
  \item[6)] Go on holiday for the rest of your life. ;o)\\[-7mm]\mbox{}
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   217
  \end{enumerate}
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   218
  \end{quote}
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   219
  \end{minipage}};
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   220
  \end{tikzpicture}
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   221
  \end{textblock}}
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   222
315
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   223
  \end{frame}}
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   224
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   225
543
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   226
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   227
\begin{frame}[c]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   228
\frametitle{Compilers \& Boeings 777}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   229
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   230
First flight in 1994. They want to achieve triple redundancy in hardware
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   231
faults.\bigskip
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   232
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   233
They compile 1 Ada program to\medskip
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   234
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   235
\begin{itemize}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   236
\item Intel 80486
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   237
\item Motorola 68040 (old Macintosh's)
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   238
\item AMD 29050 (RISC chips used often in laser printers)
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   239
\end{itemize}\medskip
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   240
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   241
using 3 independent compilers.\bigskip\pause
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   242
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   243
\small Airbus uses C and static analysers. Recently started using CompCert.
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   244
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   245
\end{frame}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   246
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   247
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   248
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   249
\begin{frame}[c]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   250
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   251
{\Large\bf  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   252
How many strings are in \bl{$L(a^*)$}?}\bigskip\pause 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   253
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   254
\normalsize
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   255
\begin{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   256
\begin{tabular}{llllll}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   257
  \bl{$[]$} &  \bl{$a$} &  \bl{$aa$} & \bl{$aaa$} & \bl{$aaaa$} & \ldots\\
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   258
  \bl{0}  &  \bl{1} &  \bl{2}  & \bl{3}   & \bl{4}  & \ldots    
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   259
\end{tabular}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   260
\end{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   261
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   262
\end{frame}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   263
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   264
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   265
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   266
\begin{frame}[c]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   267
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   268
\Large\bf There are more problems, than there are
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   269
programs.\bigskip\bigskip\pause\\
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   270
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   271
There must be a problem for which there is no program.
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   272
\end{frame}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   273
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   274
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   275
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   276
\begin{frame}[c]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   277
\frametitle{Subsets}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   278
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   279
\Large
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   280
If \bl{$A \subseteq B$} then \bl{$A$} has fewer or equal elements 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   281
than \bl{$B$}\bigskip\bigskip
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   282
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   283
\Large
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   284
\bl{$A \subseteq B$} and \bl{$B \subseteq A$}\bigskip
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   285
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   286
then \bl{$A = B$}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   287
\end{frame}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   288
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   289
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   290
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   291
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   292
  \begin{frame}[c]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   293
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   294
  \begin{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   295
  \begin{tikzpicture}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   296
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   297
  \draw (-4,2.5) node [scale=2.5] (X) 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   298
    {\begin{tabular}{l}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   299
     $\{$  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   300
     \!\includegraphics[scale=0.02]{../pics/o1.jpg},
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   301
     \includegraphics[scale=0.02]{../pics/o2.jpg},
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   302
     \!\includegraphics[scale=0.02]{../pics/o3.jpg},
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   303
     \includegraphics[scale=0.02]{../pics/o4.jpg},
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   304
     \!\includegraphics[scale=0.027]{../pics/o5.jpg}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   305
     $\}$
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   306
    \end{tabular}};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   307
    
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   308
    \draw (-5.6,-2.5) node [scale=2.5] (Y) 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   309
    {\begin{tabular}{l}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   310
     $\{$  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   311
     \!\includegraphics[scale=0.059]{../pics/a1.jpg},
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   312
     \includegraphics[scale=0.048]{../pics/a2.jpg},
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   313
     \includegraphics[scale=0.02]{../pics/a3.jpg}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   314
     $\}$
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   315
    \end{tabular}};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   316
    
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   317
     \draw (0,1.5) node (X1) {5 elements};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   318
     \draw (0,-3.5) node (y1) {3 elements};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   319
  \end{tikzpicture}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   320
  \end{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   321
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   322
  \end{frame}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   323
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   324
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   325
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   326
  \begin{frame}[c]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   327
  \frametitle{Newton vs Feynman}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   328
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   329
  \begin{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   330
  \begin{tabular}{cc}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   331
  \includegraphics[scale=0.2]{../pics/newton.jpg} &
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   332
  \includegraphics[scale=0.2]{../pics/feynman.jpg}\\
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   333
  classical physics & quantum physics
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   334
  \end{tabular}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   335
  \end{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   336
  \end{frame}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   337
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   338
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   339
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   340
  \begin{frame}[c]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   341
  \frametitle{The Goal of the Talk}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   342
 \large
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   343
  \begin{itemize}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   344
  \item show you that something very unintuitive happens with very large sets	
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   345
  \bigskip\bigskip
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   346
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   347
  \item convince you that there are more {\bf problems} than {\bf programs}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   348
  \end{itemize}	
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   349
  \end{frame}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   350
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   351
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   352
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   353
\begin{frame}[t]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   354
%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   355
  \begin{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   356
  \begin{tikzpicture}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   357
 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   358
  \draw (-5,2.5) node [scale=2.3] (X) 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   359
    {\begin{tabular}{@ {\hspace{-3mm}}l}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   360
     \bl{$B$ $=$ $\{$  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   361
     \!\includegraphics[scale=0.02]{../pics/o1.jpg},
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   362
     \includegraphics[scale=0.02]{../pics/o2.jpg},
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   363
     \!\includegraphics[scale=0.02]{../pics/o3.jpg},
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   364
     \includegraphics[scale=0.02]{../pics/o4.jpg},
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   365
     \!\includegraphics[scale=0.027]{../pics/o5.jpg}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   366
     $\}$}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   367
    \end{tabular}};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   368
    
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   369
    \draw (-6.6,-0.5) node [scale=2.3] (Y) 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   370
    {\begin{tabular}{@ {\hspace{-3mm}}l}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   371
     \bl{$A$ $=$ $\{$  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   372
     \!\includegraphics[scale=0.059]{../pics/a1.jpg},
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   373
     \includegraphics[scale=0.048]{../pics/a2.jpg},
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   374
     \includegraphics[scale=0.02]{../pics/a3.jpg}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   375
     $\}$}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   376
     \end{tabular}};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   377
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   378
     \only<1>{\draw (-5, -3) node[scale=2] 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   379
       {\bl{$|A|$ $=$ $5$}, \bl{$|B|$ $=$ $3$}};}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   380
     \only<2>{
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   381
       \draw [->, line width=1mm, red] (-7.4, 0.2) -- (-6.1, 2.1);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   382
       \draw [->, line width=1mm, red] (-5.8, 0.2) -- (-3.1, 2.1);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   383
       \draw [->, line width=1mm, red] (-4.5, 0.2) -- (-7.6, 2.1);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   384
       \draw (-5, -3) node[scale=2] {then \bl{$|A|$ $\le$ $|B|$}};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   385
       }
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   386
    \only<3>{
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   387
       \draw [<-, line width=1mm, red] (-7.5, 0.2) -- (-6.1, 2.1);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   388
       \draw [<-, line width=1mm, red] (-7.3, 0.2) -- (-3.1, 2.1);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   389
       \draw [<-, line width=1mm, red] (-6, 0.2) -- (-7.5, 2.1);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   390
       \draw [<-, line width=1mm, red] (-4.5, 0.2) -- (-4.5, 2.1);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   391
       \draw [<-, line width=1mm, red] (-4.3, 0.2) -- (-1.3, 2.1);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   392
       
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   393
       \draw (-5, -3) node[scale=1.5] {\small{}for \bl{$=$}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   394
        has to be a {\bf one-to-one} mapping};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   395
       }
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   396
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   397
    
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   398
  \end{tikzpicture}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   399
  \end{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   400
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   401
\end{frame}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   402
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   403
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   404
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   405
\begin{frame}[c]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   406
\frametitle{Cardinality}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   407
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   408
\Large
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   409
\bl{$|A|$} $\dn$ ``how many elements''\bigskip\\
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   410
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   411
\bl{$A \subseteq B  \Rightarrow |A| \leq |B|$}\bigskip\\\pause
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   412
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   413
if there is an injective function \bl{$f: A \rightarrow B$} then \bl{$|A| \leq |B|$}\
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   414
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   415
\begin{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   416
\bl{\large$\forall x y.\; f(x) = f(y) \Rightarrow x = y$}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   417
\end{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   418
\end{frame}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   419
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   420
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   421
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   422
\begin{frame}[t]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   423
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   424
  \begin{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   425
  \begin{tikzpicture}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   426
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   427
  \draw (-6.6,2.5) node [scale=2.3] (X) 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   428
    {\begin{tabular}{@ {\hspace{-3mm}}l}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   429
     $A$ $=$ $\{$  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   430
     \!\includegraphics[scale=0.02]{../pics/o1.jpg},
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   431
     \includegraphics[scale=0.02]{../pics/o2.jpg},
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   432
     \!\includegraphics[scale=0.02]{../pics/o3.jpg}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   433
     $\}$
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   434
    \end{tabular}};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   435
    
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   436
    \draw (-6.6,-0.5) node [scale=2.3] (Y) 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   437
    {\begin{tabular}{@ {\hspace{-3mm}}l}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   438
     $B$ $=$ $\{$  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   439
     \!\includegraphics[scale=0.059]{../pics/a1.jpg},
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   440
     \includegraphics[scale=0.048]{../pics/a2.jpg},
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   441
     \includegraphics[scale=0.02]{../pics/a3.jpg}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   442
     $\}$
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   443
     \end{tabular}};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   444
   \onslide<3->{\draw (-7, -3) node[scale=1.5] 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   445
      {then \bl{$|A|$ \alert{$=$} $|B|$}};}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   446
     \only<1>{
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   447
       \draw [->, line width=1mm, red] (-7.4, 0.2) -- (-6.1, 2.1);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   448
       \draw [->, line width=1mm, red] (-5.8, 0.2) -- (-4.3, 2.1);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   449
       \draw [->, line width=1mm, red] (-4.5, 0.2) -- (-7.6, 2.1);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   450
     }
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   451
    \only<2->{
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   452
       \draw [<-, line width=1mm, blue] (-7.5, 0.2) -- (-7.5, 2.1);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   453
       \draw [<-, line width=1mm, blue] (-5.8, 0.2) -- (-4.3, 2.1);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   454
       \draw [<-, line width=1mm, blue] (-4.5, 0.2) -- (-6.1, 2.1);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   455
       }
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   456
   
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   457
    
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   458
  \end{tikzpicture}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   459
  \end{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   460
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   461
\end{frame}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   462
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
315
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   463
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   464
543
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   465
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   466
\begin{frame}[c]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   467
\frametitle{Natural Numbers}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   468
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   469
\Large
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   470
\bl{$\mathbb{N}$} \bl{$\dn$} \bl{$\{0, 1, 2, 3, .......\}$}\bigskip\pause 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   471
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   472
\bl{$A$} is \alert{countable} iff \bl{$|A| \leq |\mathbb{N}|$}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   473
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   474
\end{frame}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   475
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   476
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   477
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   478
\begin{frame}[c]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   479
\frametitle{First Question}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   480
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   481
\Large
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   482
\bl{$|\mathbb{N} - \{0\}|   \;\;\;\alert{?}\;\;\;  |\mathbb{N}| $}\bigskip\bigskip 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   483
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   484
\large
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   485
\bl{$\geq$} or \bl{$\leq$} or \bl{$=$} ?
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   486
\bigskip\bigskip\bigskip\pause
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   487
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   488
\bl{$x$ $\mapsto$ $x + 1$},\\  \bl{$|\mathbb{N} - \{0\}|$ $=$  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   489
$|\mathbb{N}|$}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   490
\end{frame}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   491
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   492
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   493
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   494
\mode<presentation>{
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   495
\begin{frame}[c]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   496
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   497
\Large
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   498
\bl{$|\mathbb{N} - \{0, 1\}|   \;\;\;\alert{?}\;\;\;  |\mathbb{N}| $}\bigskip\pause 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   499
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   500
\bl{$|\mathbb{N} - \mathbb{O}|   \;\;\;\alert{?}\;\;\;  |\mathbb{N}| $}\bigskip\bigskip
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   501
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   502
\normalsize
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   503
\bl{$\mathbb{O}$} $\dn$ odd numbers\quad   \bl{$\{1,3,5......\}$}\\ \pause
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   504
\bl{$\mathbb{E}$} $\dn$ even numbers\quad   \bl{$\{0,2,4......\}$}\\
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   505
\end{frame}}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   506
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   507
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   508
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   509
\mode<presentation>{
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   510
\begin{frame}[c]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   511
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   512
\Large
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   513
\bl{$|\mathbb{N} \cup \mathbb{-N}|   \;\;\;\alert{?}\;\;\;  |\mathbb{N}| $}\bigskip\bigskip
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   514
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   515
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   516
\normalsize
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   517
\bl{$\mathbb{\phantom{-}N}$} $\dn$ positive numbers\quad   \bl{$\{0,1,2,3,......\}$}\\
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   518
\bl{$\mathbb{-N}$} $\dn$ negative numbers\quad   \bl{$\{0,-1,-2,-3,......\}$}\\
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   519
\end{frame}}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   520
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   521
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   522
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   523
\mode<presentation>{
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   524
\begin{frame}[c]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   525
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   526
\Large
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   527
\bl{$A$} is \alert{countable} if there exists an injective \bl{$f : A \rightarrow \mathbb{N}$}\bigskip
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   528
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   529
\bl{$A$} is \alert{uncountable} if there does not exist an injective \bl{$f : A \rightarrow \mathbb{N}$}\bigskip\bigskip 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   530
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   531
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   532
countable:  \bl{$|A| \leq |\mathbb{N}|$}\\
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   533
uncountable:  \bl{$|A| > |\mathbb{N}|$}\pause\bigskip
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   534
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   535
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   536
Does there exist such an \bl{$A$} ?
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   537
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   538
\end{frame}}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   539
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   540
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   541
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   542
  \mode<presentation>{
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   543
  \begin{frame}[c]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   544
  \frametitle{Hilbert's Hotel}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   545
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   546
  \begin{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   547
 \includegraphics[scale=0.8]{../pics/hilberts_hotel.jpg}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   548
  \end{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   549
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   550
  \begin{itemize}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   551
  \item \ldots has as many rooms as there are natural numbers
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   552
  \end{itemize}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   553
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   554
  \end{frame}}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   555
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   556
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   557
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   558
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   559
\begin{frame}[t]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   560
 \frametitle{\begin{tabular}{c}Real Numbers between\\[-2mm] 0 and 1\end{tabular}}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   561
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   562
  \begin{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   563
  \begin{tikzpicture}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   564
  \draw [fill, color=black!50] (1,4) rectangle (2, 3);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   565
  \draw [fill, color=black!50] (2,3) rectangle (3, 2);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   566
  \draw [fill, color=black!50] (3,2) rectangle (4, 1);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   567
  \draw [fill, color=black!50] (4,1) rectangle (5, 0);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   568
  \draw (0, 0) grid (8, 5);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   569
  \draw [line width = 1.mm] (1,0) -- (1, 5);    
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   570
  \draw [line width = 1.mm] (0, 4) -- (8, 4);    
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   571
  \draw (0.5,3.5) node {$1$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   572
  \draw (0.5,2.5) node {$2$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   573
  \draw (0.5,1.5) node {$3$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   574
  \draw (0.5,0.5) node {$4$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   575
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   576
  \draw (1.5,3.5) node {\only<1>{$3$}\only<2->{$4$}};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   577
  \draw (2.5,3.5) node {$3$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   578
  \draw (3.5,3.5) node {$3$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   579
  \draw (4.5,3.5) node {$3$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   580
  \draw (5.5,3.5) node {$3$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   581
  \draw (6.5,3.5) node {$3$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   582
  \draw (7.5,3.5) node {$\ldots$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   583
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   584
  \draw (1.5,2.5) node {$1$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   585
  \draw (2.5,2.5) node {\only<1-2>{$2$}\only<3->{$3$}};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   586
  \draw (3.5,2.5) node {$3$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   587
  \draw (4.5,2.5) node {$4$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   588
  \draw (5.5,2.5) node {$5$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   589
  \draw (6.5,2.5) node {$6$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   590
  \draw (7.5,2.5) node {$7$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   591
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   592
  \draw (1.5,1.5) node {$0$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   593
  \draw (2.5,1.5) node {$1$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   594
  \draw (3.5,1.5) node {\only<1-3>{$0$}\only<4->{$1$}};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   595
  \draw (4.5,1.5) node {$1$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   596
  \draw (5.5,1.5) node {$0$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   597
  \draw (6.5,1.5) node {$\ldots$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   598
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   599
   \draw (1.5,0.5) node {$7$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   600
  \draw (2.5,0.5) node {$8$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   601
  \draw (3.5,0.5) node {$5$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   602
  \draw (4.5,0.5) node {\only<1-4>{$3$}\only<5->{$4$}};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   603
  \draw (5.5,0.5) node {$9$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   604
  \draw (6.5,0.5) node {$\ldots$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   605
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   606
   \draw (1.5,-0.5) node {$\ldots$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   607
   \draw (8.5,3.5) node {$\ldots$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   608
  \end{tikzpicture}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   609
  \end{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   610
  \mbox{}\\[-20mm]\mbox{}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   611
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   612
  \onslide<6->{
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   613
  \begin{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   614
  \Large\bl{$|\mathbb{N}| < |R|$}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   615
  \end{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   616
  }
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   617
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   618
\end{frame}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   619
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   620
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   621
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   622
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   623
\mode<presentation>{
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   624
\begin{frame}[t]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   625
 \frametitle{The Set of Problems}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   626
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   627
  $\aleph_0$
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   628
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   629
  \begin{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   630
  \begin{tikzpicture}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   631
  \draw [fill, color=black!50] (1,4) rectangle (2, 3);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   632
  \draw [fill, color=black!50] (2,3) rectangle (3, 2);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   633
  \draw [fill, color=black!50] (3,2) rectangle (4, 1);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   634
  \draw [fill, color=black!50] (4,1) rectangle (5, 0);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   635
  \draw (0, 0) grid (8, 5);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   636
  \draw [line width = 1.mm] (1,0) -- (1, 5);    
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   637
  \draw [line width = 1.mm] (0, 4) -- (8, 4);    
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   638
  \draw (0.5,3.5) node {$1$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   639
  \draw (0.5,2.5) node {$2$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   640
  \draw (0.5,1.5) node {$3$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   641
  \draw (0.5,0.5) node {$4$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   642
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   643
  \draw (1.5,4.5) node {$0$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   644
  \draw (2.5,4.5) node {$1$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   645
  \draw (3.5,4.5) node {$2$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   646
  \draw (4.5,4.5) node {$3$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   647
  \draw (5.5,4.5) node {$4$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   648
  \draw (6.5,4.5) node {$5$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   649
  \draw (7.5,4.5) node {$\ldots$}; 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   650
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   651
  \draw (1.5,3.5) node {$0$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   652
  \draw (2.5,3.5) node {$1$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   653
  \draw (3.5,3.5) node {$0$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   654
  \draw (4.5,3.5) node {$1$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   655
  \draw (5.5,3.5) node {$0$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   656
  \draw (6.5,3.5) node {$1$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   657
  \draw (7.5,3.5) node {$\ldots$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   658
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   659
  \draw (1.5,2.5) node {$0$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   660
  \draw (2.5,2.5) node {$0$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   661
  \draw (3.5,2.5) node {$0$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   662
  \draw (4.5,2.5) node {$1$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   663
  \draw (5.5,2.5) node {$1$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   664
  \draw (6.5,2.5) node {$0$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   665
  \draw (7.5,2.5) node {$0$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   666
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   667
  \draw (1.5,1.5) node {$0$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   668
  \draw (2.5,1.5) node {$0$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   669
  \draw (3.5,1.5) node {$0$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   670
  \draw (4.5,1.5) node {$0$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   671
  \draw (5.5,1.5) node {$0$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   672
  \draw (6.5,1.5) node {$\ldots$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   673
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   674
   \draw (1.5,0.5) node {$1$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   675
  \draw (2.5,0.5) node {$1$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   676
  \draw (3.5,0.5) node {$0$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   677
  \draw (4.5,0.5) node {$1$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   678
  \draw (5.5,0.5) node {$1$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   679
  \draw (6.5,0.5) node {$\ldots$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   680
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   681
  \draw (1.5,-0.5) node {$\ldots$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   682
   \draw (8.5,3.5) node {$\ldots$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   683
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   684
  \end{tikzpicture}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   685
  \end{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   686
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   687
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   688
  \onslide<2>{
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   689
  \begin{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   690
  \large \bl{|Progs| $=$ $|\mathbb{N}|$ $<$ |Probs|}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   691
 \end{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   692
  }
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   693
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   694
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   695
\end{frame}}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   696
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   697
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   698
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   699
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   700
\mode<presentation>{
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   701
\begin{frame}[c]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   702
\frametitle{Halting Problem}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   703
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   704
\large
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   705
Assume a program \bl{$H$} that decides for all programs \bl{$A$} and all 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   706
input data \bl{$D$} whether\bigskip
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   707
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   708
\begin{itemize}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   709
\item \bl{$H(A, D) \dn 1$} iff \bl{$A(D)$} terminates
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   710
\item \bl{$H(A, D) \dn 0$} otherwise
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   711
\end{itemize}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   712
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   713
\end{frame}}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   714
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   715
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   716
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   717
\mode<presentation>{
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   718
\begin{frame}[c]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   719
\frametitle{Halting Problem (2)}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   720
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   721
\large
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   722
Given such a program \bl{$H$} define the following program \bl{$C$}:
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   723
for all programs \bl{$A$}\bigskip
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   724
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   725
\begin{itemize}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   726
\item \bl{$C(A) \dn 0$} iff \bl{$H(A, A) = 0$} 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   727
\item \bl{$C(A) \dn$ loops} otherwise
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   728
\end{itemize}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   729
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   730
\end{frame}}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   731
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   732
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   733
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   734
\mode<presentation>{
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   735
\begin{frame}[c]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   736
\frametitle{Contradiction}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   737
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   738
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   739
\bl{$H(C, C)$} is either \bl{$0$} or \bl{$1$}.
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   740
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   741
\begin{itemize}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   742
\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$} 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   743
\item \bl{$H(C, C) = 0$} $\stackrel{\text{def}\,H}{\Rightarrow}$ \bl{$C(C)$} loops $\stackrel{\text{def}\,C}{\Rightarrow}$\\ 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   744
\hspace{7cm}\bl{$H(C, C)=1$} 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   745
\end{itemize}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   746
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   747
Contradiction in both cases. So \bl{$H$} cannot exist.
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   748
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   749
\end{frame}}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   750
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   751
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   752
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   753
  \mode<presentation>{
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   754
  \begin{frame}[c]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   755
  \frametitle{Take Home Points}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   756
 \large
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   757
 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   758
  \begin{itemize}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   759
  \item there are sets that are more infinite than others\bigskip
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   760
  \item even  with the most powerful computer we can imagine, there 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   761
  are problems that cannot be solved by any program\bigskip\bigskip
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   762
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   763
  \item in CS we actually hit quite often such problems (halting problem)
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   764
  \end{itemize}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   765
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   766
  \end{frame}}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   767
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   768
  
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   769
\end{document}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   770
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   771
%%% Local Variables:  
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   772
%%% mode: latex
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   773
%%% TeX-master: t
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   774
%%% End: 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   775