|
| 1 | +\chapter{Introduction} |
| 2 | + |
| 3 | +\section{Course Structure} |
| 4 | +\twosplit{ |
| 5 | + \begin{center} |
| 6 | + \begin{tikzpicture} |
| 7 | + \clip (0,0) circle (2cm) ; |
| 8 | + \node[anchor=center] at (0,-0.5) {\includegraphics[width=4.5cm]{introduction/images/azalea_raad.jpg}}; |
| 9 | + \end{tikzpicture} |
| 10 | + \centerline{\textbf{Dr Azelea Raad}} |
| 11 | + \end{center} |
| 12 | + \textbf{First Half} |
| 13 | + \begin{itemize} |
| 14 | + \item The while language |
| 15 | + \item Big \& small step semantics |
| 16 | + \item Structural induction |
| 17 | + \end{itemize} |
| 18 | +}{ |
| 19 | + \begin{center} |
| 20 | + \begin{tikzpicture} |
| 21 | + \clip (0,0) circle (2cm) ; |
| 22 | + \node[anchor=center] at (-.1,0.0) {\includegraphics[width=4.5cm]{introduction/images/herbert_wiklicky.jpg}}; |
| 23 | + \end{tikzpicture} |
| 24 | + \centerline{\textbf{Dr Herbert Wiklicky}} |
| 25 | + \end{center} |
| 26 | + \textbf{Second Half} |
| 27 | + \begin{itemize} |
| 28 | + \item Register Machines \& gadgets |
| 29 | + \item Turing Machines |
| 30 | + \item Lambda Calculus |
| 31 | + \end{itemize} |
| 32 | +} |
| 33 | + |
| 34 | +\section{Algorithms} |
| 35 | +\begin{sidenotebox}{Euclid's Algorithm} |
| 36 | + Algorithm to find the greatest common divisor published by greek mathematician Euclid in $\approx 300$ B.C. |
| 37 | + \inputminted{haskell}{introduction/code/euclid.hs} |
| 38 | +\end{sidenotebox} |
| 39 | +\begin{sidenotebox}{Sieve of Eratosthenes} |
| 40 | + Used to find the prime numbers within a limit. Done by starting from the 2, adding the number to the primes, marking all multiples as non-prime, then repeating progressing to the next non-marked number (a prime) and repeating. |
| 41 | + \\ |
| 42 | + \\ The sieve is attributed to Eratosthenes of Cyrene and was first published $\approx 200$ B.C. |
| 43 | + \inputminted{haskell}{introduction/code/eratosthenes.hs} |
| 44 | +\end{sidenotebox} |
| 45 | +\begin{sidenotebox}{Al-Khwarizmi} |
| 46 | + A persian polymath who first presented systematic solutions to linear and quadratic equations (by completing the square). |
| 47 | + He pioneered the treatment of algebra as an independent discipline within mathematics and introduced foundational methods such as the notion of balancing \& reducing equal equations (e.g subtract/cancel the same algebraic term from both sides of an equation) |
| 48 | + \\ |
| 49 | + \\ His book title \RL{الجبر} \textit{"al-jabr"} resulted in the word \textit{algebra} and subsequently algorithm. |
| 50 | +\end{sidenotebox} |
| 51 | + |
| 52 | +Algorithms predate the computer, and have been studied in a mathematical/logical context for centuries. |
| 53 | +\begin{itemize} |
| 54 | + \item Very early attempts such as the Antikythera Mechanism (an analogue calculator for determining the positions of ) |
| 55 | + \item Simple configurable machines (e.g automatic looms, pianola, census tabulating machines) invented in the 1800s. |
| 56 | + \item Basic calculation devices such as Charles \textit{Babbage's Difference Engine} further generalised the idea of a calculating machine with a sequence of operations, and rudimentary memory store. |
| 57 | + \item Babbage's Analytical Engine is generally considered the world's first digital computer design, but was not fully implemented due to the limits of precision engineering at the time. |
| 58 | + \item English mathematician Ada Lovelace writes the first ever computer program (to calculate bernoulli numbers) on Babbage's analytical engine. |
| 59 | +\end{itemize} |
| 60 | + |
| 61 | +\begin{sidenotebox}{Note G} |
| 62 | + While translating a french transcript of a lecture given by Charles Babbage at the University of Turin on his analytical engine, Ada Lovelace added several notes (A-G), with the last including a description of an algorithm to compute the \href{https://en.wikipedia.org/wiki/Bernoulli_number}{Bernoulli numbers}. |
| 63 | + \begin{center} |
| 64 | + \includegraphics[width=.8\textwidth]{introduction/images/note_G.jpg} |
| 65 | + \end{center} |
| 66 | +\end{sidenotebox} |
| 67 | + |
| 68 | +\begin{sidenotebox}{Babbage's Machines} |
| 69 | + The \textit{Difference Engine} was used as the basis for designing the fully programmable \textit{Analytical Engine}. |
| 70 | + \begin{itemize} |
| 71 | + \item Held back by lack of funds, limitations of precision machining at the time. |
| 72 | + \item Contains an ALU for arithmetic operations, supports conditional branches and has a memory |
| 73 | + \item Part of the machine (including a printing mechanism) are on display at the science museum. |
| 74 | + \end{itemize} |
| 75 | +\end{sidenotebox} |
| 76 | + |
| 77 | +\section{Decision Problems} |
| 78 | +\begin{definitionbox}{Formulas} |
| 79 | + Well formed logical statements that are a sequence of symbols form a given formal language. e.g $(p \lor q) \land i$ is a formula, but $) \lor \land j i$ is not. |
| 80 | +\end{definitionbox} |
| 81 | +Given: |
| 82 | +\begin{itemize} |
| 83 | + \item A set $S$ of finite data structures of some kind (e.g formulae in first order logic). |
| 84 | + \item A property $P$ of elements of $S$ (e.g the porperty of a formula that it has a proof). |
| 85 | +\end{itemize} |
| 86 | +The associated decision procedure is: |
| 87 | +\\ |
| 88 | +\\ Find an algorithm such that for any $s \in S$, if $s$ has property $P$ the algorithm terminates with $1$, otherwise with $0$. |
| 89 | + |
| 90 | +\subsection{Hilbert's Entscheidungsproblem} |
| 91 | +\begin{quote} |
| 92 | + \textit{Is there an algorithm which can take any statement in first-order logic, and determine in a finite number of steps if the statement is provable?} |
| 93 | +\end{quote} |
| 94 | +\begin{definitionbox}{First Order Logic/Predicate Logic} |
| 95 | + An extension of propositional logic that includes quanifiers ($\forall, \exists$), equality, function symbols (e.g $\times, \div, +, -$) and structured formulas (predicate functions). |
| 96 | +\end{definitionbox} |
| 97 | + |
| 98 | +\noindent This problem was originally presented in a more ambiguous form, using a logic system more powerful than first-order logic. |
| 99 | +\\ |
| 100 | +\\ '\textit{Entscheidungsproblem}' means 'decision problem' |
| 101 | +\\ |
| 102 | +\\ Many tried to solve the problem, without success. One strategy was to try and disprove that such an algorithm can exist. |
| 103 | +In order to answer this question properly a formal definition of algorithm was required. |
| 104 | +\section{Algorithms} |
| 105 | +\subsection{Algorithms Informally} |
| 106 | +Common features of Algorithms: |
| 107 | +\begin{center} |
| 108 | + \begin{tabular}{l p{.8\textwidth}} |
| 109 | + \textbf{Finite} & Description of the procedure in terms of elementary operations. \\ |
| 110 | + \textbf{Deterministic} & If there is a next step, it is uniquely determined - that is on the same data, the same steps will be made. \\ |
| 111 | + \textbf{Terminate?} & Procedure may not terminate on some input data, however we can recognize when it terminates and what the result is. \\ |
| 112 | + \end{tabular} |
| 113 | +\end{center} |
| 114 | +\noindent |
| 115 | +In 1935/35, Alan Turing (Cambridge) and Church (Princeton) independently gave negative soltuions to Hilberts Entscheidungsproblem (showed such an algorithm could not exist). |
| 116 | +\begin{enumerate} |
| 117 | + \item They gave concrete/precise definitions of what algorithms are (Turing Machines \& Lambda Calculus). |
| 118 | + \item They regarded algorithms as data, on which other algorithms could act. |
| 119 | + \item They reduced the problem to the \textit{Halting problem}. |
| 120 | +\end{enumerate} |
| 121 | +This work led to the Church-Turing Thesis, that shows everything computable is computed by a Turing Machine. Church's Thesis extended this to show that General Recurisve Functions were the same type as those expressed by lambda calculus, and Turning showed that lambda calculus and the turning machine were equivalent. |
| 122 | + |
| 123 | +\subsubsection{Algorithms Formalised} |
| 124 | +Any formal definition of an algorithm should be: |
| 125 | +\begin{center} |
| 126 | + \begin{tabular}{l p{.8\textwidth}} |
| 127 | + \textbf{Precise} & No ambiguities, no implicit assumptions, Should be phrased mathematically. \\ |
| 128 | + \textbf{Simple} & No unnecessary details, only the few axioms required. Makes it easier to reason about. \\ |
| 129 | + \textbf{General} & So all algorithms and types of algorithms are covered. \\ |
| 130 | + \end{tabular} |
| 131 | +\end{center} |
| 132 | + |
| 133 | +\subsection{The Halting Problem} |
| 134 | +The \textit{Halting problem} is a \textit{decision problem} with: |
| 135 | +\begin{itemize} |
| 136 | + \item The set of all pairs $(A,D)$ such that $A$ is an algorithm, and $D$ is some input datum on which the algorithm operates. |
| 137 | + \item The property $A(D)\downarrow$ holds for $(A,D) \in S$ if algorithm $A$ when applied to $D$ eventually produces a result (halts). |
| 138 | +\end{itemize} |
| 139 | +Turning and Church showed that there is no algorithm such that: |
| 140 | +\[\forall (A,D) \in S \begin{bmatrix} |
| 141 | + H (A,D) & = & 1 & A(D)\downarrow \\ |
| 142 | + & & 0 & otherwise |
| 143 | + \end{bmatrix}\] |
| 144 | +The final step for Turing/Church's proof was to construct an algorithm encoding instances $(A,D)$ of the halting problem as statements such that: |
| 145 | +\[\Phi_{A,D} \ is \ provable \leftrightarrow A(D)\downarrow\] |
| 146 | + |
| 147 | +\subsection{Algorithms as Functions} |
| 148 | +It is possible to give a mathematical description of a computable function as a special function between special sets. |
| 149 | +\\ |
| 150 | +\\ In the 1960s Strachey \& Scott (Oxford) introduced \textit{denotational semantics}, which describes the meaning (denotation) |
| 151 | +of an algorithm as a function that maps input to output. |
| 152 | +\begin{definitionbox}{Domains} |
| 153 | + Domains are special kinds of partially ordered sets. Partial orders meaning there is an order of elements in the set, but not every element is comparable. |
| 154 | + \\ |
| 155 | + \\ Partial orders are reflexive, transitive and anti-symmetric. You can easily represent them on a Hasse Diagram. |
| 156 | + \begin{center} |
| 157 | + \includegraphics[width=.3\textwidth]{introduction/images/hasse_diagram.drawio.png} |
| 158 | + \end{center} |
| 159 | +\end{definitionbox} |
| 160 | +\noindent |
| 161 | +Scott solved the most difficult part, considering recursively defined algorithms as continuous functions between domains. |
| 162 | + |
| 163 | +\subsection{Haskell Programs} |
| 164 | +Example using a basic implementation of power. |
| 165 | +\inputminted{haskell}{introduction/code/power.hs} |
| 166 | + |
| 167 | +\newcommand{\step}[1]{$\leadsto$ \ #1\\} |
| 168 | + |
| 169 | +\begin{minipage}{.5\textwidth} |
| 170 | + \textbf{O(n)} \\ |
| 171 | + power 7 5 \\ |
| 172 | + \step{7 * (power 7 4)} |
| 173 | + \step{7 * ( 7 * (power 7 3))} |
| 174 | + \step{7 * ( 7 * (7 * (power 7 2)))} |
| 175 | + \step{7 * ( 7 * (7 * (7 * (power 7 1))))} |
| 176 | + \step{7 * ( 7 * (7 * (7 * (7 * (power 7 0)))))} |
| 177 | + \step{7 * ( 7 * (7 * (7 * (7 * 1))))} |
| 178 | + \step{16807} |
| 179 | +\end{minipage} \begin{minipage}{.5\textwidth} |
| 180 | + \textbf{O(log(n)) steps} \\ |
| 181 | + power' 7 5 \\ |
| 182 | + \step{7 * (power' 7 2)\^2} |
| 183 | + \step{7 * ((power' 7 1)\^2)\^2} |
| 184 | + \step{7 * ((7 * (power' 7 0)\^2)\^2)\^2} |
| 185 | + \step{7 * ((7 * (1)\^2)\^2)\^2} |
| 186 | + \step{16807} |
| 187 | +\end{minipage} |
| 188 | + |
| 189 | +These two functions are equivalent in result however operate differently (one much faster than the other). |
| 190 | + |
| 191 | +\section{Program Semantics} |
| 192 | +\begin{definitionbox}{Denotational Semantics} |
| 193 | + \begin{itemize} |
| 194 | + \item A program's meaning is described computationally using denotations (mathematical objects) |
| 195 | + \item A denotation of a program phrase is built from its sub-phrases. |
| 196 | + \end{itemize} |
| 197 | +\end{definitionbox} |
| 198 | +\begin{definitionbox}{Operational Semantics} |
| 199 | + Program's meaning is given in terms of the steps taken to make it run. |
| 200 | +\end{definitionbox} |
| 201 | + |
| 202 | +\noindent There are also \textit{axiomatic semantics} and \textit{declarative semantics} but we will not cover them here. |
0 commit comments