slides/slides10.tex
author Christian Urban <christian.urban@kcl.ac.uk>
Mon, 14 Dec 2020 19:22:12 +0000
changeset 818 6928a677d26f
parent 744 99c5916d9a8f
child 864 b5b1bc0a603b
permissions -rw-r--r--
updated
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
704
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
     1
% !TEX program = xelatex
744
99c5916d9a8f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 704
diff changeset
     2
\documentclass[dvipsnames,14pt,t,xelatex,aspectratio=169,xcolor={table}]{beamer}
315
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
     3
\usepackage{../slides}
215
828303e8e4af updated slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
     4
\usepackage{../langs}
828303e8e4af updated slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
     5
\usepackage{../data}
315
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
     6
\usepackage{../graphics}
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
     7
\usepackage{soul}
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     8
223
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
     9
\tikzset{onslide/.code args={<#1>#2}{%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    10
  \only<#1>{\pgfkeysalso{#2}} % \pgfkeysalso doesn't change the path
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    11
}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    12
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    13
\makeatletter
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    14
\newenvironment<>{btHighlight}[1][]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    15
{\begin{onlyenv}#2\begingroup\tikzset{bt@Highlight@par/.style={#1}}\begin{lrbox}{\@tempboxa}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    16
{\end{lrbox}\bt@HL@box[bt@Highlight@par]{\@tempboxa}\endgroup\end{onlyenv}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    17
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    18
\newcommand<>\btHL[1][]{%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    19
  \only#2{\begin{btHighlight}[#1]\bgroup\aftergroup\bt@HL@endenv}%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    20
}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    21
\def\bt@HL@endenv{%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    22
  \end{btHighlight}%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    23
  \egroup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    24
}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    25
\newcommand{\bt@HL@box}[2][]{%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    26
  \tikz[#1]{%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    27
    \pgfpathrectangle{\pgfpoint{1pt}{0pt}}{\pgfpoint{\wd #2}{\ht #2}}%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    28
    \pgfusepath{use as bounding box}%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    29
    \node[anchor=base west, fill=orange!30,outer sep=0pt,inner xsep=1pt, inner ysep=0pt, rounded corners=3pt, minimum height=\ht\strutbox+1pt,#1]{\raisebox{1pt}{\strut}\strut\usebox{#2}};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    30
  }%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    31
}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    32
\makeatother
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    33
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    34
315
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
    35
% beamer stuff
459
780486571e38 updated
Christian Urban <urbanc@in.tum.de>
parents: 315
diff changeset
    36
\renewcommand{\slidecaption}{CFL 10, King's College London}
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    37
\newcommand{\bl}[1]{\textcolor{blue}{#1}}       
315
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
    38
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    39
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    40
\begin{document}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    41
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    42
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
315
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
    43
\begin{frame}[t]
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    44
\frametitle{%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    45
  \begin{tabular}{@ {}c@ {}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    46
  \\[-3mm]
459
780486571e38 updated
Christian Urban <urbanc@in.tum.de>
parents: 315
diff changeset
    47
  \LARGE Compilers and \\[-2mm] 
744
99c5916d9a8f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 704
diff changeset
    48
  \LARGE Formal Languages\\[3mm] 
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    49
  \end{tabular}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    50
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    51
  \normalsize
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    52
  \begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    53
  \begin{tabular}{ll}
704
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
    54
    Email:  & christian.urban at kcl.ac.uk\\
744
99c5916d9a8f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 704
diff changeset
    55
    %Office Hours: & Thursdays 12 -- 14\\
99c5916d9a8f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 704
diff changeset
    56
    %Location: & N7.07 (North Wing, Bush House)\\
704
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
    57
    Slides \& Progs: & KEATS (also homework is there)\\  
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    58
  \end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    59
  \end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    60
744
99c5916d9a8f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 704
diff changeset
    61
  \begin{center}
99c5916d9a8f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 704
diff changeset
    62
    \begin{tikzpicture}
99c5916d9a8f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 704
diff changeset
    63
      \node[drop shadow,fill=white,inner sep=0pt] 
99c5916d9a8f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 704
diff changeset
    64
      {\footnotesize\rowcolors{1}{capri!10}{white}
99c5916d9a8f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 704
diff changeset
    65
        \begin{tabular}{|p{4.8cm}|p{4.8cm}|}\hline
99c5916d9a8f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 704
diff changeset
    66
          1 Introduction, Languages          & 6 While-Language \\
99c5916d9a8f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 704
diff changeset
    67
          2 Regular Expressions, Derivatives & 7 Compilation, JVM \\
99c5916d9a8f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 704
diff changeset
    68
          3 Automata, Regular Languages      & 8 Compiling Functional Languages \\
99c5916d9a8f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 704
diff changeset
    69
          4 Lexing, Tokenising               & 9 Optimisations \\
99c5916d9a8f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 704
diff changeset
    70
          5 Grammars, Parsing                & \cellcolor{blue!50}10 LLVM \\ \hline
99c5916d9a8f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 704
diff changeset
    71
        \end{tabular}%
99c5916d9a8f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 704
diff changeset
    72
      };
99c5916d9a8f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 704
diff changeset
    73
    \end{tikzpicture}
99c5916d9a8f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 704
diff changeset
    74
  \end{center}
315
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
    75
\end{frame}
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    76
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    77
704
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
    78
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
    79
\begin{frame}[c,fragile]
818
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
    80
\frametitle{Static Single-Assignment}  
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
    81
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
    82
\bl{$(1 + a) + (3 + (b * 5))$}\bigskip\bigskip  
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
    83
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
    84
\begin{lstlisting}[language=LLVMIR,numbers=left]
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
    85
let tmp0 = add 1 a in   
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
    86
let tmp1 = mul b 5 in 
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
    87
let tmp2 = add 3 tmp1 in 
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
    88
let tmp3 = add tmp0 tmp2
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
    89
  in tmp3 
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
    90
\end{lstlisting}  
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
    91
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
    92
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
    93
\end{frame}
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
    94
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
    95
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
    96
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
    97
\begin{frame}[c,fragile]
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
    98
\small
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
    99
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   100
\mbox{}\bigskip\bigskip\bigskip
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   101
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   102
\begin{lstlisting}[language={},numbers=left]
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   103
define i32 @fact (i32 %n) {
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   104
   %tmp_20 = icmp eq i32  %n, 0
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   105
   br i1 %tmp_20, label %if_branch_24, label %else_branch_25
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   106
 if_branch_24:
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   107
   ret i32 1
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   108
 else_branch_25:
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   109
   %tmp_22 = sub i32  %n, 1
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   110
   %tmp_23 = call i32 @fact (i32 %tmp_22)
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   111
   %tmp_21 = mul i32  %n, %tmp_23
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   112
   ret i32 %tmp_21
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   113
}  
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   114
\end{lstlisting}  
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   115
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   116
\begin{lstlisting}[language={},numbers=none]
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   117
def fact(n) = if n == 0 then 1 else n * fact(n - 1)
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   118
\end{lstlisting}  
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   119
\end{frame}
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   120
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   121
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   122
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   123
\begin{frame}[c,fragile]
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   124
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   125
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   126
\begin{lstlisting}[language=LLVM,numbers=none]
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   127
br i1 %var, label %if_br, label %else_br
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   128
  
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   129
icmp eq i32  %x, %y     ; for equal
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   130
icmp sle i32 %x, %y     ;   signed less or equal
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   131
icmp slt i32 %x, %y     ;   signed less than
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   132
icmp ult i32 %x, %y     ;   unsigned less than 
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   133
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   134
%var = call i32 @foo(...args...)
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   135
\end{lstlisting}  
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   136
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   137
\end{frame}
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   138
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   139
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   140
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
6928a677d26f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   141
\begin{frame}[c,fragile]
704
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   142
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   143
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   144
\begin{lstlisting}[language=Scala, numbers=none, xleftmargin=-6mm]
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   145
def fact(n: Int) : Int = {
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   146
  if (n == 0) 1 else n * fact(n - 1) 
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   147
}
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   148
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   149
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   150
def factC(n: Int, ret: Int => Int) : Int = {
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   151
  if (n == 0) ret(1) 
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   152
  else factC(n - 1, x => ret(n * x)) 
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   153
}
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   154
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   155
fact(10)
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   156
factC(10, identity)
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   157
\end{lstlisting}
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   158
\end{frame}
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   159
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   160
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   161
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   162
\begin{frame}[c,fragile]
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   163
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   164
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   165
\begin{lstlisting}[language=Scala, numbers=none, xleftmargin=-6mm]
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   166
def fibC(n: Int, ret: Int => Int) : Int = {
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   167
  if (n == 0 || n == 1) ret(1) else
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   168
  fibC(n - 1,
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   169
       r1 => fibC(n - 2,
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   170
        r2 => ret(r1 + r2)))
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   171
}
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   172
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   173
fibC(10, identity)
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   174
\end{lstlisting}
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   175
\end{frame}
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   176
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   177
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   178
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   179
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   180
543
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   181
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   182
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   183
\begin{frame}[c]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   184
704
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   185
  \Large\bf Are there more strings in \\ \hfill\bl{$L(a^*)$} or
617
f7de0915fff2 updated
Christian Urban <urbanc@in.tum.de>
parents: 616
diff changeset
   186
  \bl{$L((a + b)^*)$}?
543
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   187
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   188
\end{frame}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   189
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   190
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   191
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   192
\begin{frame}[c]
704
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   193
\frametitle{Can you remember this HW?}
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   194
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   195
  \begin{itemize}
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   196
  \item (1) How many basic regular expressions are there to match
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   197
      the string \bl{$abcd$}? 
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   198
  \item (2) How many if they cannot include
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   199
      \bl{$\ONE$} and \bl{$\ZERO$}? 
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   200
  \item (3) How many if they are also not
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   201
      allowed to contain stars? 
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   202
  \item (4) How many if they are also
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   203
      not allowed to contain \bl{$\_ + \_$}?
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   204
   \end{itemize}  
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   205
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   206
\end{frame}
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   207
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   208
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   209
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   210
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6d9c960a2b26 updated
Christian Urban <urbanc@in.tum.de>
parents: 617
diff changeset
   211
\begin{frame}[c]
543
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   212
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   213
\Large\bf There are more problems, than there are
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   214
programs.\bigskip\bigskip\pause\\
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   215
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   216
There must be a problem for which there is no program.
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   217
\end{frame}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   218
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   219
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   220
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   221
\begin{frame}[c]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   222
\frametitle{Subsets}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   223
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   224
\Large
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   225
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
   226
than \bl{$B$}\bigskip\bigskip
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   227
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   228
\Large
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   229
\bl{$A \subseteq B$} and \bl{$B \subseteq A$}\bigskip
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   230
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   231
then \bl{$A = B$}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   232
\end{frame}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   233
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
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
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   236
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   237
  \begin{frame}[c]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   238
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   239
  \begin{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   240
  \begin{tikzpicture}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   241
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   242
  \draw (-4,2.5) node [scale=2.5] (X) 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   243
    {\begin{tabular}{l}
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
     \!\includegraphics[scale=0.02]{../pics/o1.jpg},
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   246
     \includegraphics[scale=0.02]{../pics/o2.jpg},
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   247
     \!\includegraphics[scale=0.02]{../pics/o3.jpg},
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   248
     \includegraphics[scale=0.02]{../pics/o4.jpg},
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   249
     \!\includegraphics[scale=0.027]{../pics/o5.jpg}
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
    \end{tabular}};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   252
    
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   253
    \draw (-5.6,-2.5) node [scale=2.5] (Y) 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   254
    {\begin{tabular}{l}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   255
     $\{$  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   256
     \!\includegraphics[scale=0.059]{../pics/a1.jpg},
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   257
     \includegraphics[scale=0.048]{../pics/a2.jpg},
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   258
     \includegraphics[scale=0.02]{../pics/a3.jpg}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   259
     $\}$
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   260
    \end{tabular}};
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
     \draw (0,1.5) node (X1) {5 elements};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   263
     \draw (0,-3.5) node (y1) {3 elements};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   264
  \end{tikzpicture}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   265
  \end{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   266
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   267
  \end{frame}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   268
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   269
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
  \begin{frame}[c]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   272
  \frametitle{Newton vs Feynman}
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
  \begin{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   275
  \begin{tabular}{cc}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   276
  \includegraphics[scale=0.2]{../pics/newton.jpg} &
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   277
  \includegraphics[scale=0.2]{../pics/feynman.jpg}\\
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   278
  classical physics & quantum physics
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   279
  \end{tabular}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   280
  \end{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   281
  \end{frame}
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
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   284
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   285
  \begin{frame}[c]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   286
  \frametitle{The Goal of the Talk}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   287
 \large
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   288
  \begin{itemize}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   289
  \item show you that something very unintuitive happens with very large sets	
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   290
  \bigskip\bigskip
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
  \item convince you that there are more {\bf problems} than {\bf programs}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   293
  \end{itemize}	
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   294
  \end{frame}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   295
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   298
\begin{frame}[t]
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
  \begin{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   301
  \begin{tikzpicture}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   302
 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   303
  \draw (-5,2.5) node [scale=2.3] (X) 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   304
    {\begin{tabular}{@ {\hspace{-3mm}}l}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   305
     \bl{$B$ $=$ $\{$  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   306
     \!\includegraphics[scale=0.02]{../pics/o1.jpg},
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   307
     \includegraphics[scale=0.02]{../pics/o2.jpg},
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   308
     \!\includegraphics[scale=0.02]{../pics/o3.jpg},
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   309
     \includegraphics[scale=0.02]{../pics/o4.jpg},
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   310
     \!\includegraphics[scale=0.027]{../pics/o5.jpg}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   311
     $\}$}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   312
    \end{tabular}};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   313
    
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   314
    \draw (-6.6,-0.5) node [scale=2.3] (Y) 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   315
    {\begin{tabular}{@ {\hspace{-3mm}}l}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   316
     \bl{$A$ $=$ $\{$  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   317
     \!\includegraphics[scale=0.059]{../pics/a1.jpg},
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   318
     \includegraphics[scale=0.048]{../pics/a2.jpg},
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   319
     \includegraphics[scale=0.02]{../pics/a3.jpg}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   320
     $\}$}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   321
     \end{tabular}};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   322
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   323
     \only<1>{\draw (-5, -3) node[scale=2] 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   324
       {\bl{$|A|$ $=$ $5$}, \bl{$|B|$ $=$ $3$}};}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   325
     \only<2>{
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   326
       \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
   327
       \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
   328
       \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
   329
       \draw (-5, -3) node[scale=2] {then \bl{$|A|$ $\le$ $|B|$}};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   330
       }
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   331
    \only<3>{
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   332
       \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
   333
       \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
   334
       \draw [<-, line width=1mm, red] (-6, 0.2) -- (-7.5, 2.1);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   335
       \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
   336
       \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
   337
       
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   338
       \draw (-5, -3) node[scale=1.5] {\small{}for \bl{$=$}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   339
        has to be a {\bf one-to-one} mapping};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   340
       }
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   341
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   342
    
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   343
  \end{tikzpicture}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   344
  \end{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   345
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   346
\end{frame}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   347
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   348
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   349
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   350
\begin{frame}[c]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   351
\frametitle{Cardinality}
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
\Large
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   354
\bl{$|A|$} $\dn$ ``how many elements''\bigskip\\
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   355
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   356
\bl{$A \subseteq B  \Rightarrow |A| \leq |B|$}\bigskip\\\pause
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
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
   359
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   360
\begin{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   361
\bl{\large$\forall x y.\; f(x) = f(y) \Rightarrow x = y$}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   362
\end{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   363
\end{frame}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   364
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   365
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
\begin{frame}[t]
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
  \begin{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   370
  \begin{tikzpicture}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   371
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   372
  \draw (-6.6,2.5) node [scale=2.3] (X) 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   373
    {\begin{tabular}{@ {\hspace{-3mm}}l}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   374
     $A$ $=$ $\{$  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   375
     \!\includegraphics[scale=0.02]{../pics/o1.jpg},
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   376
     \includegraphics[scale=0.02]{../pics/o2.jpg},
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   377
     \!\includegraphics[scale=0.02]{../pics/o3.jpg}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   378
     $\}$
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   379
    \end{tabular}};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   380
    
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   381
    \draw (-6.6,-0.5) node [scale=2.3] (Y) 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   382
    {\begin{tabular}{@ {\hspace{-3mm}}l}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   383
     $B$ $=$ $\{$  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   384
     \!\includegraphics[scale=0.059]{../pics/a1.jpg},
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   385
     \includegraphics[scale=0.048]{../pics/a2.jpg},
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   386
     \includegraphics[scale=0.02]{../pics/a3.jpg}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   387
     $\}$
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   388
     \end{tabular}};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   389
   \onslide<3->{\draw (-7, -3) node[scale=1.5] 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   390
      {then \bl{$|A|$ \alert{$=$} $|B|$}};}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   391
     \only<1>{
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   392
       \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
   393
       \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
   394
       \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
   395
     }
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   396
    \only<2->{
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   397
       \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
   398
       \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
   399
       \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
   400
       }
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   401
   
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
  \end{tikzpicture}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   404
  \end{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   405
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   406
\end{frame}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   407
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
315
470922b46a63 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 224
diff changeset
   408
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   409
543
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
\begin{frame}[c]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   412
\frametitle{Natural Numbers}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   413
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   414
\Large
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   415
\bl{$\mathbb{N}$} \bl{$\dn$} \bl{$\{0, 1, 2, 3, .......\}$}\bigskip\pause 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   416
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   417
\bl{$A$} is \alert{countable} iff \bl{$|A| \leq |\mathbb{N}|$}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   418
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   419
\end{frame}
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
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   423
\begin{frame}[c]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   424
\frametitle{First Question}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   425
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   426
\Large
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   427
\bl{$|\mathbb{N} - \{0\}|   \;\;\;\alert{?}\;\;\;  |\mathbb{N}| $}\bigskip\bigskip 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   428
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   429
\large
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   430
\bl{$\geq$} or \bl{$\leq$} or \bl{$=$} ?
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   431
\bigskip\bigskip\bigskip\pause
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   432
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   433
\bl{$x$ $\mapsto$ $x + 1$},\\  \bl{$|\mathbb{N} - \{0\}|$ $=$  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   434
$|\mathbb{N}|$}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   435
\end{frame}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   436
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   437
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   438
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   439
\mode<presentation>{
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   440
\begin{frame}[c]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   441
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   442
\Large
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   443
\bl{$|\mathbb{N} - \{0, 1\}|   \;\;\;\alert{?}\;\;\;  |\mathbb{N}| $}\bigskip\pause 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   444
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   445
\bl{$|\mathbb{N} - \mathbb{O}|   \;\;\;\alert{?}\;\;\;  |\mathbb{N}| $}\bigskip\bigskip
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   446
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   447
\normalsize
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   448
\bl{$\mathbb{O}$} $\dn$ odd numbers\quad   \bl{$\{1,3,5......\}$}\\ \pause
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   449
\bl{$\mathbb{E}$} $\dn$ even numbers\quad   \bl{$\{0,2,4......\}$}\\
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   450
\end{frame}}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   451
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   452
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   453
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   454
\mode<presentation>{
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   455
\begin{frame}[c]
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
\Large
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   458
\bl{$|\mathbb{N} \cup \mathbb{-N}|   \;\;\;\alert{?}\;\;\;  |\mathbb{N}| $}\bigskip\bigskip
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   459
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
\normalsize
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   462
\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
   463
\bl{$\mathbb{-N}$} $\dn$ negative numbers\quad   \bl{$\{0,-1,-2,-3,......\}$}\\
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   464
\end{frame}}
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
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   467
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   468
\mode<presentation>{
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   469
\begin{frame}[c]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   470
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   471
\Large
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   472
\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
   473
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   474
\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
   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
countable:  \bl{$|A| \leq |\mathbb{N}|$}\\
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   478
uncountable:  \bl{$|A| > |\mathbb{N}|$}\pause\bigskip
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   479
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
Does there exist such an \bl{$A$} ?
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   482
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   483
\end{frame}}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   484
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   485
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   486
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   487
  \mode<presentation>{
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   488
  \begin{frame}[c]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   489
  \frametitle{Hilbert's Hotel}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   490
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   491
  \begin{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   492
 \includegraphics[scale=0.8]{../pics/hilberts_hotel.jpg}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   493
  \end{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   494
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   495
  \begin{itemize}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   496
  \item \ldots has as many rooms as there are natural numbers
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   497
  \end{itemize}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   498
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   499
  \end{frame}}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   500
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
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
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   503
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   504
\begin{frame}[t]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   505
 \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
   506
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   507
  \begin{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   508
  \begin{tikzpicture}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   509
  \draw [fill, color=black!50] (1,4) rectangle (2, 3);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   510
  \draw [fill, color=black!50] (2,3) rectangle (3, 2);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   511
  \draw [fill, color=black!50] (3,2) rectangle (4, 1);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   512
  \draw [fill, color=black!50] (4,1) rectangle (5, 0);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   513
  \draw (0, 0) grid (8, 5);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   514
  \draw [line width = 1.mm] (1,0) -- (1, 5);    
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   515
  \draw [line width = 1.mm] (0, 4) -- (8, 4);    
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   516
  \draw (0.5,3.5) node {$1$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   517
  \draw (0.5,2.5) node {$2$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   518
  \draw (0.5,1.5) node {$3$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   519
  \draw (0.5,0.5) node {$4$};
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
  \draw (1.5,3.5) node {\only<1>{$3$}\only<2->{$4$}};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   522
  \draw (2.5,3.5) node {$3$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   523
  \draw (3.5,3.5) node {$3$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   524
  \draw (4.5,3.5) node {$3$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   525
  \draw (5.5,3.5) node {$3$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   526
  \draw (6.5,3.5) node {$3$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   527
  \draw (7.5,3.5) node {$\ldots$};
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
  \draw (1.5,2.5) node {$1$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   530
  \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
   531
  \draw (3.5,2.5) node {$3$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   532
  \draw (4.5,2.5) node {$4$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   533
  \draw (5.5,2.5) node {$5$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   534
  \draw (6.5,2.5) node {$6$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   535
  \draw (7.5,2.5) node {$7$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   536
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   537
  \draw (1.5,1.5) node {$0$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   538
  \draw (2.5,1.5) node {$1$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   539
  \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
   540
  \draw (4.5,1.5) node {$1$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   541
  \draw (5.5,1.5) node {$0$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   542
  \draw (6.5,1.5) node {$\ldots$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   543
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   544
   \draw (1.5,0.5) node {$7$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   545
  \draw (2.5,0.5) node {$8$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   546
  \draw (3.5,0.5) node {$5$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   547
  \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
   548
  \draw (5.5,0.5) node {$9$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   549
  \draw (6.5,0.5) node {$\ldots$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   550
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   551
   \draw (1.5,-0.5) node {$\ldots$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   552
   \draw (8.5,3.5) node {$\ldots$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   553
  \end{tikzpicture}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   554
  \end{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   555
  \mbox{}\\[-20mm]\mbox{}
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
  \onslide<6->{
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   558
  \begin{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   559
  \Large\bl{$|\mathbb{N}| < |R|$}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   560
  \end{center}
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
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   563
\end{frame}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   564
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   565
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   566
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   567
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   568
\mode<presentation>{
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   569
\begin{frame}[t]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   570
 \frametitle{The Set of Problems}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   571
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   572
  $\aleph_0$
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   573
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   574
  \begin{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   575
  \begin{tikzpicture}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   576
  \draw [fill, color=black!50] (1,4) rectangle (2, 3);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   577
  \draw [fill, color=black!50] (2,3) rectangle (3, 2);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   578
  \draw [fill, color=black!50] (3,2) rectangle (4, 1);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   579
  \draw [fill, color=black!50] (4,1) rectangle (5, 0);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   580
  \draw (0, 0) grid (8, 5);
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   581
  \draw [line width = 1.mm] (1,0) -- (1, 5);    
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   582
  \draw [line width = 1.mm] (0, 4) -- (8, 4);    
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   583
  \draw (0.5,3.5) node {$1$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   584
  \draw (0.5,2.5) node {$2$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   585
  \draw (0.5,1.5) node {$3$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   586
  \draw (0.5,0.5) node {$4$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   587
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   588
  \draw (1.5,4.5) node {$0$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   589
  \draw (2.5,4.5) node {$1$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   590
  \draw (3.5,4.5) node {$2$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   591
  \draw (4.5,4.5) node {$3$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   592
  \draw (5.5,4.5) node {$4$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   593
  \draw (6.5,4.5) node {$5$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   594
  \draw (7.5,4.5) node {$\ldots$}; 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   595
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   596
  \draw (1.5,3.5) node {$0$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   597
  \draw (2.5,3.5) node {$1$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   598
  \draw (3.5,3.5) node {$0$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   599
  \draw (4.5,3.5) node {$1$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   600
  \draw (5.5,3.5) node {$0$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   601
  \draw (6.5,3.5) node {$1$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   602
  \draw (7.5,3.5) node {$\ldots$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   603
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   604
  \draw (1.5,2.5) node {$0$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   605
  \draw (2.5,2.5) node {$0$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   606
  \draw (3.5,2.5) node {$0$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   607
  \draw (4.5,2.5) node {$1$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   608
  \draw (5.5,2.5) node {$1$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   609
  \draw (6.5,2.5) node {$0$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   610
  \draw (7.5,2.5) node {$0$};
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
  \draw (1.5,1.5) node {$0$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   613
  \draw (2.5,1.5) node {$0$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   614
  \draw (3.5,1.5) node {$0$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   615
  \draw (4.5,1.5) node {$0$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   616
  \draw (5.5,1.5) node {$0$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   617
  \draw (6.5,1.5) node {$\ldots$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   618
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   619
   \draw (1.5,0.5) node {$1$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   620
  \draw (2.5,0.5) node {$1$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   621
  \draw (3.5,0.5) node {$0$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   622
  \draw (4.5,0.5) node {$1$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   623
  \draw (5.5,0.5) node {$1$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   624
  \draw (6.5,0.5) node {$\ldots$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   625
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   626
  \draw (1.5,-0.5) node {$\ldots$};
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   627
   \draw (8.5,3.5) node {$\ldots$};
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
  \end{tikzpicture}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   630
  \end{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   631
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   632
  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   633
  \onslide<2>{
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   634
  \begin{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   635
  \large \bl{|Progs| $=$ $|\mathbb{N}|$ $<$ |Probs|}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   636
 \end{center}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   637
  }
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   638
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   639
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   640
\end{frame}}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   641
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
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
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   644
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   645
\mode<presentation>{
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   646
\begin{frame}[c]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   647
\frametitle{Halting Problem}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   648
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   649
\large
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   650
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
   651
input data \bl{$D$} whether\bigskip
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   652
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   653
\begin{itemize}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   654
\item \bl{$H(A, D) \dn 1$} iff \bl{$A(D)$} terminates
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   655
\item \bl{$H(A, D) \dn 0$} otherwise
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   656
\end{itemize}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   657
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   658
\end{frame}}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   659
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   660
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   661
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   662
\mode<presentation>{
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   663
\begin{frame}[c]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   664
\frametitle{Halting Problem (2)}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   665
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   666
\large
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   667
Given such a program \bl{$H$} define the following program \bl{$C$}:
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   668
for all programs \bl{$A$}\bigskip
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   669
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   670
\begin{itemize}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   671
\item \bl{$C(A) \dn 0$} iff \bl{$H(A, A) = 0$} 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   672
\item \bl{$C(A) \dn$ loops} otherwise
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   673
\end{itemize}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   674
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   675
\end{frame}}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   676
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   677
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   678
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   679
\mode<presentation>{
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   680
\begin{frame}[c]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   681
\frametitle{Contradiction}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   682
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
\bl{$H(C, C)$} is either \bl{$0$} or \bl{$1$}.
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   685
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   686
\begin{itemize}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   687
\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
   688
\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
   689
\hspace{7cm}\bl{$H(C, C)=1$} 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   690
\end{itemize}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   691
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   692
Contradiction in both cases. So \bl{$H$} cannot exist.
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
\end{frame}}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   695
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
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
  \mode<presentation>{
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   699
  \begin{frame}[c]
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   700
  \frametitle{Take Home Points}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   701
 \large
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   702
 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   703
  \begin{itemize}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   704
  \item there are sets that are more infinite than others\bigskip
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   705
  \item even  with the most powerful computer we can imagine, there 
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   706
  are problems that cannot be solved by any program\bigskip\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
  \item in CS we actually hit quite often such problems (halting problem)
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   709
  \end{itemize}
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   710
16adebf18ef9 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   711
  \end{frame}}
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
  
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   714
\end{document}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   715
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   716
%%% Local Variables:  
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   717
%%% mode: latex
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   718
%%% TeX-master: t
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   719
%%% End: 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   720