slides/slides10.tex
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Thu, 05 Dec 2013 10:29:35 +0000
changeset 224 70198792c2aa
parent 223 e4b29b57f6a3
child 315 470922b46a63
permissions -rw-r--r--
added
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}
215
828303e8e4af updated slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
     2
\usepackage{beamerthemeplaincu}
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     3
\usepackage[absolute,overlay]{textpos}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     4
\usepackage{ifthen}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     5
\usepackage{tikz}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     6
\usepackage{pgf}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     7
\usepackage{calc} 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     8
\usepackage{ulem}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     9
\usepackage{courier}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    10
\usepackage{listings}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    11
\renewcommand{\uline}[1]{#1}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    12
\usetikzlibrary{arrows}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    13
\usetikzlibrary{automata}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    14
\usetikzlibrary{shapes}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    15
\usetikzlibrary{shadows}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    16
\usetikzlibrary{positioning}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    17
\usetikzlibrary{calc}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    18
\usetikzlibrary{plotmarks}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    19
\usepackage{graphicx} 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    20
\usepackage{pgfplots}
223
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    21
\usepackage{soul}
215
828303e8e4af updated slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    22
\usepackage{../langs}
828303e8e4af updated slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    23
\usepackage{../data}
86
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
223
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    26
\tikzset{onslide/.code args={<#1>#2}{%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    27
  \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
    28
}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    29
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    30
\makeatletter
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    31
\newenvironment<>{btHighlight}[1][]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    32
{\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
    33
{\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
    34
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    35
\newcommand<>\btHL[1][]{%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    36
  \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
    37
}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    38
\def\bt@HL@endenv{%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    39
  \end{btHighlight}%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    40
  \egroup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    41
}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    42
\newcommand{\bt@HL@box}[2][]{%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    43
  \tikz[#1]{%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    44
    \pgfpathrectangle{\pgfpoint{1pt}{0pt}}{\pgfpoint{\wd #2}{\ht #2}}%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    45
    \pgfusepath{use as bounding box}%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    46
    \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
    47
  }%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    48
}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    49
\makeatother
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    50
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    51
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    52
% beamer stuff 
215
828303e8e4af updated slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    53
\renewcommand{\slidecaption}{AFL 10, King's College London, 4.~December 2013}
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    54
\newcommand{\bl}[1]{\textcolor{blue}{#1}}       
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    55
\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    56
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    57
\begin{document}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    58
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    59
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    60
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    61
\begin{frame}<1>[t]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    62
\frametitle{%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    63
  \begin{tabular}{@ {}c@ {}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    64
  \\[-3mm]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    65
  \LARGE Automata and \\[-2mm] 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    66
  \LARGE Formal Languages (10)\\[3mm] 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    67
  \end{tabular}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    68
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    69
  \normalsize
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    70
  \begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    71
  \begin{tabular}{ll}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    72
  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
    73
  Office: & S1.27 (1st floor Strand Building)\\
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    74
  Slides: & KEATS (also home work is there)\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    75
  \end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    76
  \end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    77
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    78
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    79
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    80
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    81
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    82
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    83
\begin{frame}[c]
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
\Large\bf
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    86
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
    87
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    88
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
    89
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    90
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    91
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    92
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    93
\mode<presentation>{
223
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    94
\begin{frame}[t]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    95
\frametitle{Last Week}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    96
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    97
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    98
if \bl{$\varnothing$} does not occur in \bl{$r$} \;\;then\;\;\bl{$L(r) \not= \{\}$}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    99
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   100
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   101
\noindent
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   102
holds, or equivalently
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   103
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   104
\begin{center}
223
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   105
\bl{$L(r) = \{\}$} \;\;implies\;\; \bl{$\varnothing$} occurs in \bl{$r$}.\pause
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   106
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   107
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   108
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   109
\bl{\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   110
$occurs(\varnothing)$      & $\dn$ & $true$\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   111
$occurs(\epsilon)$           & $\dn$ &  $f\!alse$\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   112
$occurs (c)$                    & $\dn$ &  $f\!alse$\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   113
$occurs (r_1 + r_2)$       & $\dn$ &  $occurs(r_1) \vee occurs(r_2)$\\ 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   114
$occurs (r_1 \cdot r_2)$ & $\dn$ &  $occurs(r_1) \vee occurs(r_2)$\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   115
$occurs (r^*)$                & $\dn$ & $occurs(r)$ \\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   116
\end{tabular}}
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   117
\end{center}
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
\end{frame}}
223
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   120
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   121
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   122
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   123
\begin{frame}[c,fragile]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   124
\frametitle{Functional Programming}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   125
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   126
\footnotesize
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   127
\begin{textblock}{13}(0.9,3)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   128
\lstset{emph={def,if,then,else},emphstyle=\color{javapurple}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   129
\begin{lstlisting}[basicstyle=\ttfamily, numbers=none]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   130
def fib(n) = if n == 0 then 0 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   131
             else if n == 1 then 1 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   132
             else fib(n - 1) + fib(n - 2);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   133
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   134
def fact(n) = if n == 0 then 1 else n * fact(n - 1);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   135
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   136
def ack(m, n) = if m == 0 then n + 1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   137
                else if n == 0 then ack(m - 1, 1)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   138
                else ack(m - 1, ack(m, n - 1));
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   139
                
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   140
def gcd(a, b) = if b == 0 then a else gcd(b, a % b);                
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   141
\end{lstlisting}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   142
\end{textblock}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   144
\end{frame}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   145
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   146
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   147
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   148
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   149
\begin{frame}[c]
223
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   150
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   151
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   152
\bl{\begin{tabular}{@{}lcl@{}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   153
\textit{Exp} & $\rightarrow$ &  \textit{Var} $|$ \textit{Num}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   154
              & $|$ & \textit{Exp} \texttt{+} \textit{Exp} $|$ ... $|$ ( \textit{Exp} )\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   155
              & $|$ & \texttt{if}\; \textit{BExp} \;\texttt{then}\; \textit{Exp} \;\texttt{else}\; \textit{Exp}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   156
              & $|$ & \texttt{write}\;\textit{Exp}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   157
              & $|$ & \textit{Exp}\;\texttt{;}\;\textit{Exp}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   158
              & $|$ & \textit{FunName} \texttt{(}\textit{Exp},...,\textit{Exp}\texttt{)}\medskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   159
\textit{BExp} & $\rightarrow$ & \ldots\medskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   160
\textit{Decl} & $\rightarrow$ &  \textit{Def} \;\texttt{;}\; \textit{Decl}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   161
              & $|$ & \textit{Exp}\medskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   162
\textit{Def} & 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   163
$\rightarrow$ &  \texttt{def} \textit{FunName}\texttt{(}\textit{x}$_1$,..., \textit{x}$_n$\texttt{)} \texttt{=} \textit{Exp}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   164
\end{tabular}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   165
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   166
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   167
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   168
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   169
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   170
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   171
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   172
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   173
\begin{frame}[c, fragile]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   174
\frametitle{Abstract Syntax Tree}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   175
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   176
\footnotesize
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   177
\begin{textblock}{13}(0.3,2)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   178
\begin{lstlisting}[language=Scala,basicstyle=\ttfamily, numbers=none]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   179
abstract class Exp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   180
abstract class BExp 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   181
abstract class Decl
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   182
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   183
case class 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   184
  Def(name: String, args: List[String], body: Exp) 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   185
                                          extends Decl
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   186
case class Main(e: Exp) extends Decl
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   187
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   188
case class Call(name: String, args: List[Exp]) extends Exp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   189
case class If(a: BExp, e1: Exp, e2: Exp) extends Exp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   190
case class Write(e: Exp) extends Exp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   191
case class Var(s: String) extends Exp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   192
case class Num(i: Int) extends Exp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   193
case class Aop(o: String, a1: Exp, a2: Exp) extends Exp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   194
case class Sequ(e1: Exp, e2: Exp) extends Exp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   195
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   196
case class Bop(o: String, a1: Exp, a2: Exp) extends BExp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   197
\end{lstlisting}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   198
\end{textblock}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   199
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   200
\end{frame}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   201
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   202
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   203
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   204
\begin{frame}[c, fragile]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   205
\frametitle{Mathematical Functions}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   206
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   207
Compilation of some mathematical functions:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   208
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   209
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   210
\begin{tabular}{lcl}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   211
\texttt{Aop("+", a1, a2)} & $\Rightarrow$ & \texttt{...iadd}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   212
\texttt{Aop("-", a1, a2)} & $\Rightarrow$ & \texttt{...isub}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   213
\texttt{Aop("*", a1, a2)} & $\Rightarrow$ & \texttt{...imul}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   214
\texttt{Aop("/", a1, a2)} & $\Rightarrow$ & \texttt{...idiv}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   215
\texttt{Aop("\%", a1, a2)} & $\Rightarrow$ & \texttt{...irem}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   216
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   217
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   218
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   219
\end{frame}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   220
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   221
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   222
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   223
\begin{frame}[c, fragile]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   224
\frametitle{Boolean Expressions}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   225
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   226
Compilation of boolean expressions:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   227
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   228
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   229
\begin{tikzpicture}[node distance=2mm and 4mm,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   230
 block/.style={rectangle, minimum size=1cm, draw=black, line width=1mm},
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   231
 point/.style={rectangle, inner sep=0mm, minimum size=0mm, fill=red},
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   232
 skip loop/.style={red, line width=1mm, to path={-- ++(0,-10mm) -| (\tikztotarget)}}]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   233
\node (A1) [point] {};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   234
\node (b) [block, right=of A1] {code of \bl{$b$}};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   235
\node (A2) [point, right=of b] {};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   236
\node (cs1) [block, right=of A2] {code of \bl{$cs_1$}};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   237
\node (A3) [point, right=of cs1] {};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   238
\node (cs2) [block, right=of A3] {code of \bl{$cs_2$}};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   239
\node (A4) [point, right=of cs2] {};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   240
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   241
\only<1>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   242
\draw (A1) edge [->, red, line width=1mm] (b);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   243
\draw (b) edge [->, red, line width=1mm] (A2);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   244
\draw (A2) edge [skip loop] (A3);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   245
\draw (A3) edge [->, red, line width=1mm] (cs2);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   246
\draw (cs2) edge [->,red, line width=1mm] (A4);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   247
\node [below=of cs1] {\raisebox{-5mm}{\small{}conditional jump}};}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   248
\end{tikzpicture}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   249
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   250
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   251
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   252
\begin{tabular}{lcl}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   253
\texttt{Bop("==", a1, a2)} & $\Rightarrow$ & \texttt{...if\_icmpne...}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   254
\texttt{Bop("!=", a1, a2)} & $\Rightarrow$ & \texttt{...if\_icmpeq...}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   255
\texttt{Bop("<", a1, a2)} & $\Rightarrow$ & \texttt{...if\_icmpge...}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   256
\texttt{Bop("<=", a1, a2)} & $\Rightarrow$ & \texttt{...if\_icmpgt...}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   257
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   258
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   259
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   260
\end{frame}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   261
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   262
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   263
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   264
\begin{frame}[t, fragile]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   265
\frametitle{Sequences}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   266
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   267
Compiling \texttt{arg1 ; arg2}:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   268
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   269
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   270
\begin{textblock}{7}(2,5)\footnotesize
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   271
\begin{minipage}{6cm}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   272
\begin{lstlisting}[language=JVMIS,basicstyle=\ttfamily, numbers=none]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   273
...arg1...
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   274
pop
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   275
...arg1...
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   276
\end{lstlisting}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   277
\end{minipage}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   278
\end{textblock}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   279
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   280
  
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   281
\end{frame}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   282
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   283
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   284
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   285
\begin{frame}[t, fragile]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   286
\frametitle{Write}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   287
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   288
Compiling \texttt{write(arg)}:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   289
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   290
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   291
\begin{textblock}{7}(2,4)\footnotesize
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   292
\begin{minipage}{6cm}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   293
\begin{lstlisting}[language=JVMIS,basicstyle=\ttfamily, numbers=none]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   294
...arg...
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   295
dup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   296
invokestatic XXX/XXX/write(I)V
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   297
\end{lstlisting}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   298
\end{minipage}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   299
\end{textblock}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   300
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   301
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   302
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   303
\begin{textblock}{7}(2,8)\footnotesize
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   304
\begin{minipage}{6cm}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   305
\begin{lstlisting}[language=Scala,basicstyle=\ttfamily, numbers=none]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   306
case Write(a1) => {
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   307
    compile_exp(a1, env) ++
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   308
    List("dup\n",
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   309
         "invokestatic XXX/XXX/write(I)V\n")
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   310
  }
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   311
\end{lstlisting}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   312
\end{minipage}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   313
\end{textblock}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   314
  
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   315
\end{frame}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   316
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   317
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   318
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   319
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   320
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   321
\begin{frame}[c, fragile]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   322
\frametitle{Functions}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   323
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   324
\begin{textblock}{7}(1,2)\footnotesize
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   325
\begin{minipage}{6cm}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   326
\begin{lstlisting}[language=JVMIS,basicstyle=\ttfamily, numbers=none]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   327
.method public static write(I)V 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   328
   .limit locals 5 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   329
   .limit stack 5 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   330
   iload 0 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   331
   getstatic java/lang/System/out Ljava/io/PrintStream; 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   332
   swap 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   333
   invokevirtual java/io/PrintStream/println(I)V 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   334
   return 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   335
.end method
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   336
\end{lstlisting}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   337
\end{minipage}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   338
\end{textblock}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   339
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   340
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   341
\begin{textblock}{10}(1,9.8)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   342
\small We will need for definitions\\[-8mm]\mbox{}\footnotesize
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   343
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   344
\begin{lstlisting}[language=JVMIS,basicstyle=\ttfamily, numbers=none]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   345
.method public static f (I...I)I
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   346
  .limit locals ??
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   347
  .limit stack ?? 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   348
  ??
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   349
.end method
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   350
\end{lstlisting}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   351
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   352
\end{textblock}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   353
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   354
\end{frame}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   355
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   356
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   357
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   358
\begin{frame}[c, fragile]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   359
\frametitle{Stack Estimation}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   360
\footnotesize
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   361
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   362
\begin{lstlisting}[language=Scala,basicstyle=\ttfamily, numbers=none]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   363
def max_stack_exp(e: Exp): Int = e match {
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   364
  case Call(_, args) => args.map(max_stack_exp).sum
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   365
  case If(a, e1, e2) => max_stack_bexp(a) + 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   366
  	(List(max_stack_exp(e1), max_stack_exp(e1)).max)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   367
  case Write(e) => max_stack_exp(e) + 1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   368
  case Var(_) => 1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   369
  case Num(_) => 1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   370
  case Aop(_, a1, a2) => 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   371
  	max_stack_exp(a1) + max_stack_exp(a2)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   372
  case Sequ(e1, e2) => 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   373
  	List(max_stack_exp(e1), max_stack_exp(e2)).max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   374
}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   375
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   376
def max_stack_bexp(e: BExp): Int = e match {
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   377
  case Bop(_, a1, a2) => 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   378
  	max_stack_exp(a1) + max_stack_exp(a2)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   379
}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   380
\end{lstlisting}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   381
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   382
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   383
\end{frame}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   384
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   385
223
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   386
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   387
\begin{frame}[fragile]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   388
\frametitle{Successor}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   389
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   390
\begin{textblock}{7}(1,2.5)\footnotesize
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   391
\begin{minipage}{6cm}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   392
\begin{lstlisting}[language=JVMIS,basicstyle=\ttfamily, numbers=none]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   393
.method public static suc(I)I 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   394
.limit locals 1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   395
.limit stack
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   396
  iload 0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   397
  ldc 1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   398
  iadd
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   399
  ireturn
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   400
.end method 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   401
\end{lstlisting}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   402
\end{minipage}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   403
\end{textblock}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   404
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   405
\begin{textblock}{7}(6,8)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   406
\begin{tikzpicture}\small
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   407
\draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   408
{\begin{minipage}{5cm}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   409
\begin{lstlisting}[language=Lisp,basicstyle=\ttfamily, numbers=none]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   410
def suc(x) = x + 1;
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   411
\end{lstlisting}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   412
\end{minipage}};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   413
\end{tikzpicture}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   414
\end{textblock}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   415
\end{frame}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   416
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   417
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   418
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   419
\begin{frame}[fragile]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   420
\frametitle{Addition}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   421
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   422
\begin{textblock}{7}(1,1.5)\footnotesize
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   423
\begin{minipage}{6cm}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   424
\begin{lstlisting}[language=JVMIS,basicstyle=\ttfamily, numbers=none]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   425
.method public static add(II)I 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   426
.limit locals 2
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   427
.limit stack 4
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   428
  iload 0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   429
  ldc 0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   430
  if_icmpne If_else_2
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   431
  iload 1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   432
  goto If_end_3
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   433
If_else_2:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   434
  iload 0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   435
  ldc 1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   436
  isub
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   437
  iload 1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   438
  invokestatic defs/defs/add(II)I
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   439
  invokestatic defs/defs/suc(I)I
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   440
If_end_3:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   441
  ireturn
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   442
.end method
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   443
\end{lstlisting}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   444
\end{minipage}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   445
\end{textblock}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   446
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   447
\begin{textblock}{7}(6,6.2)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   448
\begin{tikzpicture}\small
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   449
\draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   450
{\begin{minipage}{7cm}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   451
\begin{lstlisting}[language=Lisp,basicstyle=\ttfamily, numbers=none]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   452
def add(x, y) = 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   453
    if x == 0 then y 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   454
    else suc(add(x - 1, y));
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   455
\end{lstlisting}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   456
\end{minipage}};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   457
\end{tikzpicture}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   458
\end{textblock}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   459
\end{frame}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   460
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   461
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   462
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   463
\begin{frame}[fragile]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   464
\frametitle{Factorial}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   465
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   466
\begin{textblock}{7}(1,1.5)\footnotesize
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   467
\begin{minipage}{6cm}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   468
\begin{lstlisting}[language=JVMIS,basicstyle=\ttfamily, numbers=none]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   469
.method public static facT(II)I 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   470
.limit locals 2
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   471
.limit stack 4
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   472
  iload 0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   473
  ldc 0	
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   474
  if_icmpne If_else_2
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   475
  iload 1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   476
  goto If_end_3
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   477
If_else_2:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   478
  iload 0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   479
  ldc 1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   480
  isub
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   481
  iload 0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   482
  iload 1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   483
  imul
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   484
  invokestatic fact/fact/facT(II)I
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   485
If_end_3:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   486
  ireturn
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   487
.end method 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   488
\end{lstlisting}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   489
\end{minipage}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   490
\end{textblock}
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   491
223
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   492
\begin{textblock}{7}(6,7)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   493
\begin{tikzpicture}\small
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   494
\draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   495
{\begin{minipage}{7cm}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   496
\begin{lstlisting}[language=Lisp,basicstyle=\ttfamily, numbers=none]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   497
def facT(n, acc) = 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   498
  if n == 0 then acc 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   499
  else facT(n - 1, n * acc);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   500
\end{lstlisting}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   501
\end{minipage}};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   502
\end{tikzpicture}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   503
\end{textblock}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   504
\end{frame}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   505
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   506
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   507
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   508
\begin{frame}[fragile]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   509
%\frametitle{Factorial}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   510
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   511
\begin{textblock}{7}(1,-0.2)\footnotesize
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   512
\begin{minipage}{6cm}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   513
\begin{lstlisting}[language=JVMIS,basicstyle=\ttfamily, numbers=none, escapeinside={(*@}{@*)}]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   514
.method public static facT(II)I 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   515
.limit locals 2
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   516
.limit stack 4
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   517
(*@\hl{facT\_Start:} @*)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   518
  iload 0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   519
  ldc 0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   520
  if_icmpne If_else_2
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   521
  iload 1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   522
  goto If_end_3
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   523
If_else_2:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   524
  iload 0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   525
  ldc 1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   526
  isub
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   527
  iload 0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   528
  iload 1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   529
  imul
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   530
  (*@\hl{istore 1} @*)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   531
  (*@\hl{istore 0} @*)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   532
  (*@\hl{goto facT\_Start} @*)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   533
If_end_3:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   534
  ireturn
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   535
.end method 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   536
\end{lstlisting}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   537
\end{minipage}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   538
\end{textblock}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   539
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   540
\begin{textblock}{7}(6,7)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   541
\begin{tikzpicture}\small
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   542
\draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   543
{\begin{minipage}{7cm}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   544
\begin{lstlisting}[language=Lisp,basicstyle=\ttfamily, numbers=none]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   545
def facT(n, acc) = 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   546
  if n == 0 then acc 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   547
  else facT(n - 1, n * acc);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   548
\end{lstlisting}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   549
\end{minipage}};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   550
\end{tikzpicture}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   551
\end{textblock}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   552
\end{frame}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   553
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   554
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   555
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   556
\begin{frame}[c, fragile]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   557
\frametitle{Tail Recursion}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   558
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   559
A call to \texttt{f(args)} is usually compiled as\medskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   560
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   561
{\small\begin{lstlisting}[basicstyle=\ttfamily, numbers=none]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   562
  args onto stack
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   563
  invokestatic  .../f 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   564
\end{lstlisting}}\pause
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   565
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   566
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   567
A call is in tail position provided:\medskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   568
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   569
{\small\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   570
\item \texttt{if Bexp then \hl{Exp} else \hl{Exp}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   571
\item \texttt{Exp ; \hl{Exp}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   572
\item \texttt{Exp  op Exp}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   573
\end{itemize}}\medskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   574
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   575
then a call \texttt{f(args)} can be compiled as\medskip\small
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   576
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   577
\begin{lstlisting}[basicstyle=\ttfamily, numbers=none]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   578
  prepare environment
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   579
  jump to start of function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   580
\end{lstlisting}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   581
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   582
\end{frame}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   583
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   584
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   585
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   586
\begin{frame}[c, fragile]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   587
\frametitle{Tail Recursive Call}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   588
\footnotesize
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   589
\begin{textblock}{13}(0.3,2)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   590
\begin{lstlisting}[language=Scala,basicstyle=\ttfamily, numbers=none]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   591
def compile_expT(a: Exp, env: Mem, name: String): Instrs = 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   592
  ...
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   593
  case Call(n, args) => if (name == n) 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   594
  { 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   595
    val stores = args.zipWithIndex.map 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   596
       { case (x, y) => "istore " + y.toString + "\n" } 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   597
    args.flatMap(a => compile_expT(a, env, "")) ++
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   598
    stores.reverse ++ 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   599
    List ("goto " + n + "_Start\n") 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   600
  } 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   601
  else 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   602
  {
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   603
    val is = "I" * args.length
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   604
    args.flatMap(a => compile_expT(a, env, "")) ++
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   605
    List ("invokestatic XXX/XXX/" + n + "(" + is + ")I\n")
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   606
  }
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   607
\end{lstlisting}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   608
\end{textblock}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   609
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   610
\end{frame}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   611
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   612
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   613
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   614
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   615
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   616
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   617
\Large\bf
224
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 223
diff changeset
   618
There are more problems, than there are programs.\bigskip\bigskip\\
223
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
   619
There must be a problem for which there is no program.
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   620
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   621
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   622
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   623
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   624
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   625
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   626
\frametitle{Subsets}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   627
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   628
\Large
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   629
\bl{$A \subseteq B$} and \bl{$B \subseteq A$}\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   630
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   631
then \bl{$A = B$}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   632
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   633
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   634
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   635
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   636
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   637
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   638
\frametitle{Injective Function}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   639
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   640
\Large
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   641
\bl{f} is an injective function iff \bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   642
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   643
\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
   644
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   645
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   646
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   647
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   648
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   649
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   650
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   651
\frametitle{Cardinality}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   652
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   653
\Large
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   654
\bl{$|A|$} $\dn$ ``how many elements''\bigskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   655
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   656
\bl{$A \subseteq B  \Rightarrow |A| \leq |B|$}\bigskip\\\pause
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   657
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   658
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
   659
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   660
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   661
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   662
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   663
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   664
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   665
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   666
\frametitle{Natural Numbers}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   667
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   668
\Large
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   669
\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
   670
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   671
\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
   672
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   673
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   674
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   675
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   676
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   677
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   678
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   679
\frametitle{First Question}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   680
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   681
\Large
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   682
\bl{$|\mathbb{N} - \{0\}|   \;\;\;\alert{?}\;\;\;  |\mathbb{N}| $}\bigskip\bigskip 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   683
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   684
\normalsize
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   685
\bl{$\geq$} or \bl{$\leq$} or \bl{$=$} 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   686
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   687
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   688
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   689
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   690
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   691
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   692
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   693
\Large
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   694
\bl{$|\mathbb{N} - \{0, 1\}|   \;\;\;\alert{?}\;\;\;  |\mathbb{N}| $}\bigskip\pause 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   695
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   696
\bl{$|\mathbb{N} - \mathbb{O}|   \;\;\;\alert{?}\;\;\;  |\mathbb{N}| $}\bigskip\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   697
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   698
\normalsize
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   699
\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
   700
\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
   701
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   702
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   703
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   704
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   705
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   706
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   707
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   708
\Large
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   709
\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
   710
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   711
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   712
\normalsize
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   713
\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
   714
\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
   715
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   716
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   717
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   718
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   719
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   720
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   721
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   722
\Large
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   723
\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
   724
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   725
\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
   726
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   727
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   728
countable:  \bl{$|A| \leq |\mathbb{N}|$}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   729
uncountable:  \bl{$|A| > |\mathbb{N}|$}\pause\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   730
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   731
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   732
Does there exist such an \bl{$A$} ?
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   733
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   734
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   735
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   736
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   737
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   738
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   739
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   740
\frametitle{Halting Problem}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   741
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   742
\large
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   743
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
   744
input data \bl{$D$} whether\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   745
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   746
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   747
\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
   748
\item \bl{$H(A, D) \dn 0$} otherwise
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   749
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   750
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   751
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   752
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   753
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   754
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   755
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   756
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   757
\frametitle{Halting Problem (2)}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   758
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   759
\large
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   760
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
   761
for all programs \bl{$A$}\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   762
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   763
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   764
\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
   765
\item \bl{$C(A) \dn$ loops} otherwise
86
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   766
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   767
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   768
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   769
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   770
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   771
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   772
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   773
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   774
\frametitle{Contradiction}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   775
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   776
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   777
\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
   778
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   779
\begin{itemize}
87
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 86
diff changeset
   780
\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
   781
\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
   782
\hspace{7cm}\bl{$H(C, C)=1$} 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   783
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   784
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   785
Contradiction in both cases. So \bl{$H$} cannot exist.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   786
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   787
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   788
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   789
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   790
\end{document}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   791
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   792
%%% Local Variables:  
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   793
%%% mode: latex
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   794
%%% TeX-master: t
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   795
%%% End: 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   796