slides10.tex
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Wed, 05 Dec 2012 12:38:24 +0000
changeset 88 6e716ecf2db4
parent 87 72d0b688e942
permissions -rw-r--r--
typo
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     1
\documentclass[dvipsnames,14pt,t]{beamer}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     2
\usepackage{beamerthemeplainculight}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     3
\usepackage[T1]{fontenc}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     4
\usepackage[latin1]{inputenc}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     5
\usepackage{mathpartir}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     6
\usepackage[absolute,overlay]{textpos}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     7
\usepackage{ifthen}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     8
\usepackage{tikz}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     9
\usepackage{pgf}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    10
\usepackage{calc} 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    11
\usepackage{ulem}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    12
\usepackage{courier}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    13
\usepackage{listings}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    14
\renewcommand{\uline}[1]{#1}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    15
\usetikzlibrary{arrows}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    16
\usetikzlibrary{automata}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    17
\usetikzlibrary{shapes}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    18
\usetikzlibrary{shadows}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    19
\usetikzlibrary{positioning}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    20
\usetikzlibrary{calc}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    21
\usetikzlibrary{plotmarks}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    22
\usepackage{graphicx} 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    23
\usepackage{pgfplots}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    24
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    25
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    26
\definecolor{javared}{rgb}{0.6,0,0} % for strings
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    27
\definecolor{javagreen}{rgb}{0.25,0.5,0.35} % comments
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    28
\definecolor{javapurple}{rgb}{0.5,0,0.35} % keywords
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    29
\definecolor{javadocblue}{rgb}{0.25,0.35,0.75} % javadoc
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    30
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    31
\lstset{language=Java,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    32
	basicstyle=\ttfamily,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    33
	keywordstyle=\color{javapurple}\bfseries,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    34
	stringstyle=\color{javagreen},
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    35
	commentstyle=\color{javagreen},
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    36
	morecomment=[s][\color{javadocblue}]{/**}{*/},
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    37
	numbers=left,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    38
	numberstyle=\tiny\color{black},
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    39
	stepnumber=1,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    40
	numbersep=10pt,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    41
	tabsize=2,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    42
	showspaces=false,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    43
	showstringspaces=false}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    45
\lstdefinelanguage{scala}{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    46
  morekeywords={abstract,case,catch,class,def,%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    47
    do,else,extends,false,final,finally,%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    48
    for,if,implicit,import,match,mixin,%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    49
    new,null,object,override,package,%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    50
    private,protected,requires,return,sealed,%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    51
    super,this,throw,trait,true,try,%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    52
    type,val,var,while,with,yield},
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    53
  otherkeywords={=>,<-,<\%,<:,>:,\#,@},
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    54
  sensitive=true,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    55
  morecomment=[l]{//},
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    56
  morecomment=[n]{/*}{*/},
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    57
  morestring=[b]",
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    58
  morestring=[b]',
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    59
  morestring=[b]"""
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    60
}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    61
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    62
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    63
\lstset{language=Scala,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    64
	basicstyle=\ttfamily,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    65
	keywordstyle=\color{javapurple}\bfseries,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    66
	stringstyle=\color{javagreen},
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    67
	commentstyle=\color{javagreen},
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    68
	morecomment=[s][\color{javadocblue}]{/**}{*/},
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    69
	numbers=left,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    70
	numberstyle=\tiny\color{black},
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    71
	stepnumber=1,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    72
	numbersep=10pt,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    73
	tabsize=2,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    74
	showspaces=false,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    75
	showstringspaces=false}
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
\lstdefinelanguage{while}{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    78
  morekeywords={if,then,else,while,do,true,false,write},
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    79
  otherkeywords={=,!=,:=,<,>,;},
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    80
  sensitive=true,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    81
  morecomment=[n]{/*}{*/},
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    82
}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    83
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    84
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    85
\lstset{language=While,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    86
	basicstyle=\ttfamily,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    87
	keywordstyle=\color{javapurple}\bfseries,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    88
	stringstyle=\color{javagreen},
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    89
	commentstyle=\color{javagreen},
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    90
	morecomment=[s][\color{javadocblue}]{/**}{*/},
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    91
	numbers=left,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    92
	numberstyle=\tiny\color{black},
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    93
	stepnumber=1,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    94
	numbersep=10pt,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    95
	tabsize=2,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    96
	showspaces=false,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    97
	showstringspaces=false}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    98
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    99
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   100
% beamer stuff 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   101
\renewcommand{\slidecaption}{AFL 10, King's College London, 5.~December 2012}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   102
\newcommand{\bl}[1]{\textcolor{blue}{#1}}       
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   103
\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   104
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   105
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   106
% The data files, written on the first run.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   107
\begin{filecontents}{compiled.data}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   108
%1 0.234146
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   109
%5000 0.227539
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   110
%10000 0.280748
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   111
50000 1.087897
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   112
100000 3.713165
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   113
250000 21.6624545
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   114
500000 85.872613
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   115
750000 203.6408015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   116
1000000 345.736574
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   117
\end{filecontents}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   118
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   119
\begin{filecontents}{interpreted.data}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   120
%1 0.00503
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   121
200 1.005863
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   122
400 7.8296765
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   123
500 15.43106
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   124
600 27.2321885
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   125
800 65.249271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   126
1000 135.4493445
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   127
1200 232.134097
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   128
1400 382.527227
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   129
\end{filecontents}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   130
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   131
\begin{filecontents}{interpreted2.data}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   132
%1 0.00503
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   133
200 1.005863
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   134
400 7.8296765
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   135
600 27.2321885
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   136
800 65.249271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   137
1000 135.4493445
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   138
1200 232.134097
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   139
1400 382.527227
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   140
\end{filecontents}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   141
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   142
\begin{filecontents}{compiled2.data}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   143
200 0.222058
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   144
400 0.215204
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   145
600 0.202031
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   146
800 0.21986
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   147
1000 0.205934
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   148
1200 0.1981615
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   149
1400 0.207116
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   150
\end{filecontents}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   151
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   152
\begin{document}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   153
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   154
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   155
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   156
\begin{frame}<1>[t]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   157
\frametitle{%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   158
  \begin{tabular}{@ {}c@ {}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   159
  \\[-3mm]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   160
  \LARGE Automata and \\[-2mm] 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   161
  \LARGE Formal Languages (10)\\[3mm] 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   162
  \end{tabular}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   163
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   164
  \normalsize
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   165
  \begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   166
  \begin{tabular}{ll}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   167
  Email:  & christian.urban at kcl.ac.uk\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   168
  Of$\!$fice: & S1.27 (1st floor Strand Building)\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   169
  Slides: & KEATS (also home work is there)\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   170
  \end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   171
  \end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   172
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   173
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   174
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   175
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   176
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   177
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   178
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   179
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   180
\Large\bf
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   181
There are more problems, than there are programs.\bigskip\bigskip\pause\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   182
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   183
There must be a problem for which there is no program.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   184
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   185
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   186
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   187
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   188
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   189
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   190
\frametitle{Revision: Proofs}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   191
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   192
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   193
\includegraphics[scale=0.4]{river-stones.jpg}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   194
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   195
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   196
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   197
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   198
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   199
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   200
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   201
\frametitle{Subsets}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   202
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   203
\Large
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   204
\bl{$A \subseteq B$}\bigskip\bigskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   205
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   206
\bl{$\forall e.\; e \in A \Rightarrow e \in B$}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   207
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   208
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   209
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   210
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   211
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   212
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   213
\frametitle{Subsets}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   214
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   215
\Large
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   216
\bl{$A \subseteq B$} and \bl{$B \subseteq A$}\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   217
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   218
then \bl{$A = B$}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   219
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   220
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   221
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   222
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   223
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   224
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   225
\frametitle{Injective Function}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   226
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   227
\Large
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   228
\bl{f} is an injective function iff \bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   229
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   230
\bl{$\forall x y.\; f(x) = f(y) \Rightarrow x = y$}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   231
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   232
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   233
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   234
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   235
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   236
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   237
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   238
\frametitle{Cardinality}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   239
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   240
\Large
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   241
\bl{$|A|$} $\dn$ ``how many elements''\bigskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   242
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   243
\bl{$A \subseteq B  \Rightarrow |A| \leq |B|$}\bigskip\\\pause
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   244
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   245
if there is an injective function \bl{$f: A \rightarrow B$} then \bl{$|A| \leq |B|$}\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   247
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   248
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   249
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   250
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   251
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   252
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   253
\frametitle{Natural Numbers}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   254
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   255
\Large
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   256
\bl{$\mathbb{N}$} \bl{$\dn$} \bl{$\{0, 1, 2, 3, .......\}$}\bigskip\pause 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   257
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   258
\bl{$A$} is \alert{countable} iff \bl{$|A| \leq |\mathbb{N}|$}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   259
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   260
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   261
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   262
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   263
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   264
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   265
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   266
\frametitle{First Question}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   267
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   268
\Large
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   269
\bl{$|\mathbb{N} - \{0\}|   \;\;\;\alert{?}\;\;\;  |\mathbb{N}| $}\bigskip\bigskip 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   270
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   271
\normalsize
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   272
\bl{$\geq$} or \bl{$\leq$} or \bl{$=$} 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   273
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   274
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   275
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   276
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   277
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   278
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   279
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   280
\Large
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   281
\bl{$|\mathbb{N} - \{0, 1\}|   \;\;\;\alert{?}\;\;\;  |\mathbb{N}| $}\bigskip\pause 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   282
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   283
\bl{$|\mathbb{N} - \mathbb{O}|   \;\;\;\alert{?}\;\;\;  |\mathbb{N}| $}\bigskip\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   284
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   285
\normalsize
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   286
\bl{$\mathbb{O}$} $\dn$ odd numbers\quad   \bl{$\{1,3,5......\}$}\\ \pause
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   287
\bl{$\mathbb{E}$} $\dn$ even numbers\quad   \bl{$\{0,2,4......\}$}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   288
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   289
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   290
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   291
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   292
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   293
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   294
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   295
\Large
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   296
\bl{$|\mathbb{N} \cup \mathbb{-N}|   \;\;\;\alert{?}\;\;\;  |\mathbb{N}| $}\bigskip\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   297
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   298
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   299
\normalsize
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   300
\bl{$\mathbb{\phantom{-}N}$} $\dn$ positive numbers\quad   \bl{$\{0,1,2,3,......\}$}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   301
\bl{$\mathbb{-N}$} $\dn$ negative numbers\quad   \bl{$\{0,-1,-2,-3,......\}$}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   302
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   303
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   304
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   305
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   306
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   307
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   308
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   309
\Large
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   310
\bl{$A$} is \alert{countable} if there exists an injective \bl{$f : A \rightarrow \mathbb{N}$}\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   311
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   312
\bl{$A$} is \alert{uncountable} if there does not exist an injective \bl{$f : A \rightarrow \mathbb{N}$}\bigskip\bigskip 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   313
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   314
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   315
countable:  \bl{$|A| \leq |\mathbb{N}|$}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   316
uncountable:  \bl{$|A| > |\mathbb{N}|$}\pause\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   317
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   318
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   319
Does there exist such an \bl{$A$} ?
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   320
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   321
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   322
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   323
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   324
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   325
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   326
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   327
\frametitle{Halting Problem}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   328
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   329
\large
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   330
Assume a program \bl{$H$} that decides for all programs \bl{$A$} and all 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   331
input data \bl{$D$} whether\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   332
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   333
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   334
\item \bl{$H(A, D) \dn 1$} iff \bl{$A(D)$} terminates
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   335
\item \bl{$H(A, D) \dn 0$} otherwise
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   336
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   337
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   338
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   339
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   340
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   341
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   342
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   343
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   344
\frametitle{Halting Problem (2)}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   345
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   346
\large
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   347
Given such a program \bl{$H$} define the following program \bl{$C$}:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   348
for all programs \bl{$A$}\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   349
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   350
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   351
\item \bl{$C(A) \dn 0$} iff \bl{$H(A, A) = 0$} 
87
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 86
diff changeset
   352
\item \bl{$C(A) \dn$ loops} otherwise
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   353
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   354
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   355
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   356
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   357
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   358
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   359
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   360
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   361
\frametitle{Contradiction}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   362
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   363
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   364
\bl{$H(C, C)$} is either \bl{$0$} or \bl{$1$}.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   365
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   366
\begin{itemize}
87
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 86
diff changeset
   367
\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$} 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 86
diff changeset
   368
\item \bl{$H(C, C) = 0$} $\stackrel{\text{def}\,H}{\Rightarrow}$ \bl{$C(C)$} loops $\stackrel{\text{def}\,C}{\Rightarrow}$\\ 
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   369
\hspace{7cm}\bl{$H(C, C)=1$} 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   370
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   371
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   372
Contradiction in both cases. So \bl{$H$} cannot exist.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   373
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   374
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   375
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   376
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   377
\end{document}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   378
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   379
%%% Local Variables:  
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   380
%%% mode: latex
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   381
%%% TeX-master: t
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   382
%%% End: 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   383