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