afl-material: slides/slides10.tex@cd6066f1056a (annotated)

86 6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1	\documentclass[dvipsnames,14pt,t]{beamer}
215 828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	2	\usepackage{beamerthemeplaincu}
86 6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	3	\usepackage[absolute,overlay]{textpos}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	4	\usepackage{ifthen}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	5	\usepackage{tikz}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	6	\usepackage{pgf}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	7	\usepackage{calc}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	8	\usepackage{ulem}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	9	\usepackage{courier}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	10	\usepackage{listings}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	11	\renewcommand{\uline}[1]{#1}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	12	\usetikzlibrary{arrows}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	13	\usetikzlibrary{automata}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	14	\usetikzlibrary{shapes}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	15	\usetikzlibrary{shadows}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	16	\usetikzlibrary{positioning}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	17	\usetikzlibrary{calc}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	18	\usetikzlibrary{plotmarks}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	19	\usepackage{graphicx}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	20	\usepackage{pgfplots}
215 828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	21	\usepackage{../langs}
828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	22	\usepackage{../data}
86 6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	23
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	24
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	25
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	26	% beamer stuff
215 828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	27	\renewcommand{\slidecaption}{AFL 10, King's College London, 4.~December 2013}
86 6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	28	\newcommand{\bl}[1]{\textcolor{blue}{#1}}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	29	\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	30
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	31
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	32	% The data files, written on the first run.
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	33	\begin{filecontents}{compiled.data}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	34	%1 0.234146
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	35	%5000 0.227539
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	36	%10000 0.280748
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	37	50000 1.087897
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	38	100000 3.713165
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	39	250000 21.6624545
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	40	500000 85.872613
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	41	750000 203.6408015
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	42	1000000 345.736574
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	43	\end{filecontents}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	44
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	45	\begin{filecontents}{interpreted.data}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	46	%1 0.00503
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	47	200 1.005863
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	48	400 7.8296765
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	49	500 15.43106
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	50	600 27.2321885
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	51	800 65.249271
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	52	1000 135.4493445
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	53	1200 232.134097
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	54	1400 382.527227
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	55	\end{filecontents}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	56
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	57	\begin{filecontents}{interpreted2.data}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	58	%1 0.00503
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	59	200 1.005863
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	60	400 7.8296765
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	61	600 27.2321885
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	62	800 65.249271
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	63	1000 135.4493445
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	64	1200 232.134097
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	65	1400 382.527227
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	66	\end{filecontents}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	67
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	68	\begin{filecontents}{compiled2.data}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	69	200 0.222058
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	70	400 0.215204
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	71	600 0.202031
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	72	800 0.21986
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	73	1000 0.205934
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	74	1200 0.1981615
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	75	1400 0.207116
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	76	\end{filecontents}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	77
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	78	\begin{document}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	79
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	80	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	81	\mode<presentation>{
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	82	\begin{frame}<1>[t]
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	83	\frametitle{%
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	84	\begin{tabular}{@ {}c@ {}}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	85	\\[-3mm]
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	86	\LARGE Automata and \\[-2mm]
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	87	\LARGE Formal Languages (10)\\[3mm]
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	88	\end{tabular}}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	89
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	90	\normalsize
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	91	\begin{center}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	92	\begin{tabular}{ll}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	93	Email: & christian.urban at kcl.ac.uk\\
215 828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	94	Office: & S1.27 (1st floor Strand Building)\\
86 6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	95	Slides: & KEATS (also home work is there)\\
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	96	\end{tabular}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	97	\end{center}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	98
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	99	\end{frame}}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	100	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	101
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	102	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	103	\mode<presentation>{
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	104	\begin{frame}[c]
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	105
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	106	\Large\bf
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	107	There are more problems, than there are programs.\bigskip\bigskip\pause\\
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	108
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	109	There must be a problem for which there is no program.
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	110	\end{frame}}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	111	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	112
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	113	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	114	\mode<presentation>{
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	115	\begin{frame}[c]
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	116	\frametitle{Revision: Proofs}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	117
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	118	\begin{center}
215 828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	119	%%\includegraphics[scale=0.4]{river-stones.jpg}
86 6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	120	\end{center}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	121
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	122	\end{frame}}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	123
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	124	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	125	\mode<presentation>{
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	126	\begin{frame}[c]
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	127	\frametitle{Subsets}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	128
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	129	\Large
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	130	\bl{$A \subseteq B$}\bigskip\bigskip\\
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	131
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	132	\bl{$\forall e.\; e \in A \Rightarrow e \in B$}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	133	\end{frame}}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	134	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	135
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	136	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	137	\mode<presentation>{
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	138	\begin{frame}[c]
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	139	\frametitle{Subsets}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	140
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	141	\Large
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	142	\bl{$A \subseteq B$} and \bl{$B \subseteq A$}\bigskip
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	143
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	144	then \bl{$A = B$}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	145	\end{frame}}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	146	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	147
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	148	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	149	\mode<presentation>{
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	150	\begin{frame}[c]
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	151	\frametitle{Injective Function}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	152
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	153	\Large
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	154	\bl{f} is an injective function iff \bigskip
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	155
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	156	\bl{$\forall x y.\; f(x) = f(y) \Rightarrow x = y$}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	157
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	158	\end{frame}}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	159	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	160
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	161	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	162	\mode<presentation>{
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	163	\begin{frame}[c]
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	164	\frametitle{Cardinality}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	165
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	166	\Large
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	167	\bl{$\|A\|$} $\dn$ ``how many elements''\bigskip\\
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	168
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	169	\bl{$A \subseteq B \Rightarrow \|A\| \leq \|B\|$}\bigskip\\\pause
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	170
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	171	if there is an injective function \bl{$f: A \rightarrow B$} then \bl{$\|A\| \leq \|B\|$}\
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	172
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	173	\end{frame}}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	174	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	175
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	176	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	177	\mode<presentation>{
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	178	\begin{frame}[c]
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	179	\frametitle{Natural Numbers}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	180
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	181	\Large
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	182	\bl{$\mathbb{N}$} \bl{$\dn$} \bl{$\{0, 1, 2, 3, .......\}$}\bigskip\pause
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	183
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	184	\bl{$A$} is \alert{countable} iff \bl{$\|A\| \leq \|\mathbb{N}\|$}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	185
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	186	\end{frame}}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	187	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	188
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	189	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	190	\mode<presentation>{
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	191	\begin{frame}[c]
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	192	\frametitle{First Question}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	193
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	194	\Large
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	195	\bl{$\|\mathbb{N} - \{0\}\| \;\;\;\alert{?}\;\;\; \|\mathbb{N}\| $}\bigskip\bigskip
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	196
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	197	\normalsize
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	198	\bl{$\geq$} or \bl{$\leq$} or \bl{$=$}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	199	\end{frame}}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	200	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	201
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	202	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	203	\mode<presentation>{
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	204	\begin{frame}[c]
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	205
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	206	\Large
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	207	\bl{$\|\mathbb{N} - \{0, 1\}\| \;\;\;\alert{?}\;\;\; \|\mathbb{N}\| $}\bigskip\pause
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	208
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	209	\bl{$\|\mathbb{N} - \mathbb{O}\| \;\;\;\alert{?}\;\;\; \|\mathbb{N}\| $}\bigskip\bigskip
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	210
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	211	\normalsize
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	212	\bl{$\mathbb{O}$} $\dn$ odd numbers\quad \bl{$\{1,3,5......\}$}\\ \pause
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	213	\bl{$\mathbb{E}$} $\dn$ even numbers\quad \bl{$\{0,2,4......\}$}\\
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	214	\end{frame}}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	215	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	216
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	217	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	218	\mode<presentation>{
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	219	\begin{frame}[c]
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	220
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	221	\Large
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	222	\bl{$\|\mathbb{N} \cup \mathbb{-N}\| \;\;\;\alert{?}\;\;\; \|\mathbb{N}\| $}\bigskip\bigskip
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	223
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	224
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	225	\normalsize
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	226	\bl{$\mathbb{\phantom{-}N}$} $\dn$ positive numbers\quad \bl{$\{0,1,2,3,......\}$}\\
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	227	\bl{$\mathbb{-N}$} $\dn$ negative numbers\quad \bl{$\{0,-1,-2,-3,......\}$}\\
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	228	\end{frame}}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	229	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	230
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	231	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	232	\mode<presentation>{
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	233	\begin{frame}[c]
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	234
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	235	\Large
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	236	\bl{$A$} is \alert{countable} if there exists an injective \bl{$f : A \rightarrow \mathbb{N}$}\bigskip
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	237
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	238	\bl{$A$} is \alert{uncountable} if there does not exist an injective \bl{$f : A \rightarrow \mathbb{N}$}\bigskip\bigskip
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	239
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	240
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	241	countable: \bl{$\|A\| \leq \|\mathbb{N}\|$}\\
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	242	uncountable: \bl{$\|A\| > \|\mathbb{N}\|$}\pause\bigskip
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	243
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	244
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	245	Does there exist such an \bl{$A$} ?
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	246
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	247	\end{frame}}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	248	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	249
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	250	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	251	\mode<presentation>{
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	252	\begin{frame}[c]
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	253	\frametitle{Halting Problem}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	254
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	255	\large
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	256	Assume a program \bl{$H$} that decides for all programs \bl{$A$} and all
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	257	input data \bl{$D$} whether\bigskip
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	258
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	259	\begin{itemize}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	260	\item \bl{$H(A, D) \dn 1$} iff \bl{$A(D)$} terminates
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	261	\item \bl{$H(A, D) \dn 0$} otherwise
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	262	\end{itemize}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	263
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	264	\end{frame}}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	265	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	266
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	267	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	268	\mode<presentation>{
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	269	\begin{frame}[c]
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	270	\frametitle{Halting Problem (2)}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	271
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	272	\large
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	273	Given such a program \bl{$H$} define the following program \bl{$C$}:
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	274	for all programs \bl{$A$}\bigskip
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	275
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	276	\begin{itemize}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	277	\item \bl{$C(A) \dn 0$} iff \bl{$H(A, A) = 0$}
87 72d0b688e942 typo Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 86 diff changeset	278	\item \bl{$C(A) \dn$ loops} otherwise
86 6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	279	\end{itemize}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	280
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	281	\end{frame}}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	282	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	283
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	284	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	285	\mode<presentation>{
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	286	\begin{frame}[c]
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	287	\frametitle{Contradiction}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	288
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	289
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	290	\bl{$H(C, C)$} is either \bl{$0$} or \bl{$1$}.
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	291
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	292	\begin{itemize}
87 72d0b688e942 typo Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 86 diff changeset	293	\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$}
72d0b688e942 typo Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 86 diff changeset	294	\item \bl{$H(C, C) = 0$} $\stackrel{\text{def}\,H}{\Rightarrow}$ \bl{$C(C)$} loops $\stackrel{\text{def}\,C}{\Rightarrow}$\\
86 6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	295	\hspace{7cm}\bl{$H(C, C)=1$}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	296	\end{itemize}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	297
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	298	Contradiction in both cases. So \bl{$H$} cannot exist.
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	299
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	300	\end{frame}}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	301	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	302
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	303	\end{document}
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	304
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	305	%%% Local Variables:
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	306	%%% mode: latex
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	307	%%% TeX-master: t
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	308	%%% End:
6a7fe83820c8 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	309

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Sun, 01 Dec 2013 10:17:17 +0000
changeset 217	cd6066f1056a
parent 215	828303e8e4af
child 223	e4b29b57f6a3
permissions	-rw-r--r--