docs/background.tex

   1 \documentclass[article, a4paper]{article}
   2 \usepackage[T1]{fontenc}
   3 \usepackage{fixltx2e}
   4 \usepackage{enumitem}
   5 \usepackage[normalem]{ulem}
   6 \usepackage{graphicx}
   7 \usepackage{subcaption}
   8
   9 %% -----------------------------------------------------------------------------
  10 %% Fonts
  11 %% \usepackage[osf]{libertine}
  12 %% \usepackage{helvet}
  13 %% \usepackage{lmodern}
  14 %% \IfFileExists{microtype.sty}{\usepackage{microtype}}{}
  15
  16 %% -----------------------------------------------------------------------------
  17 %% TikZ stuff
  18 %% \usepackage{tikz}
  19 %% \usetikzlibrary{positioning}
  20 %% \usetikzlibrary{shapes}
  21 %% \usetikzlibrary{arrows}
  22 %% \usepackage{tikz-cd}
  23 %% \usepackage{pgfplots}
  24
  25 %% -----------------------------------------------------------------------------
  26 %% Symbols
  27 \usepackage{amssymb,amsmath}
  28 \usepackage{wasysym}
  29 \usepackage{turnstile}
  30 \usepackage{centernot}
  31
  32 %% -----------------------------------------------------------------------------
  33 %% Utils
  34 \usepackage{bussproofs}
  35 \usepackage{umoline}
  36 \usepackage[export]{adjustbox}
  37 \usepackage{multicol}
  38
  39 %% Numbering depth
  40 %% \setcounter{secnumdepth}{0}
  41
  42 %% -----------------------------------------------------------------------------
  43 % We will generate all images so they have a width \maxwidth. This means
  44 % that they will get their normal width if they fit onto the page, but
  45 % are scaled down if they would overflow the margins.
  46 \makeatletter
  47 \def\maxwidth{
  48   \ifdim\Gin@nat@width>\linewidth\linewidth
  49   \else\Gin@nat@width\fi
  50 }
  51 \makeatother
  52
  53 %% -----------------------------------------------------------------------------
  54 %% Links
  55 \usepackage[
  56   setpagesize=false, % page size defined by xetex
  57   unicode=false, % unicode breaks when used with xetex
  58   xetex
  59 ]{hyperref}
  60
  61 \hypersetup{
  62   breaklinks=true,
  63   bookmarks=true,
  64   pdfauthor={Francesco Mazzoli <fm2209@ic.ac.uk>},
  65   pdftitle={The Paths Towards Observational Equality},
  66   colorlinks=false,
  67   pdfborder={0 0 0}
  68 }
  69
  70 % Make links footnotes instead of hotlinks:
  71 \renewcommand{\href}[2]{#2\footnote{\url{#1}}}
  72
  73 % avoid problems with \sout in headers with hyperref:
  74 \pdfstringdefDisableCommands{\renewcommand{\sout}{}}
  75
  76 \title{The Paths Towards Observational Equality}
  77 \author{Francesco Mazzoli \url{<fm2209@ic.ac.uk>}}
  78 \date{December 2012}
  79
  80 \begin{document}
  81
  82 \maketitle
  83
  84 \section{Functional programming}
  85
  86 \subsection{The $\lambda$-calculus}
  87
  88 Along with Turing's machines, the earliest attempts to formalise computation
  89 lead to the $\lambda$-calculus.  This early programming language encodes
  90 computation with a minimal sintax and most notably no ``data'' in the
  91 traditional sense, but just functions.
  92
  93 The syntax of $\lambda$-terms consists of just three things: variables,
  94 abstractions, and applications:
  95
  96 \newcommand{\app}[2]{#1\hspace{0.07cm}#2}
  97 \newcommand{\abs}[2]{\lambda #1. #2}
  98 \newcommand{\termt}{\mathrm{T}}
  99 \newcommand{\termm}{\mathrm{M}}
 100 \newcommand{\termn}{\mathrm{N}}
 101 \newcommand{\termp}{\mathrm{P}}
 102
 103 \begin{eqnarray*}
 104   \termt & ::= & x \\
 105          &  |  & (\abs{x}{\termt}) \\
 106          &  |  & (\app{\termt}{\termt}) \\
 107   x & \in & \text{Some enumerable set of symbols, e.g.}\ \{x, y, z, \dots , x_1, x_2, \dots\}
 108 \end{eqnarray*}
 109
 110 I will omit parethesis in the usual manner. %TODO explain how
 111
 112 Intuitively, abstractions ($\abs{x}{\termt}$) introduce functions with a named
 113 parameter ($x$), and applications ($\app{\termt}{\termm}$) apply a function
 114 ($\termt$) to an argument ($\termm$).
 115
 116 The ``applying'' is more formally explained with a reduction rule:
 117
 118 \newcommand{\bred}{\rightarrow_{\beta}}
 119
 120 \begin{eqnarray*}
 121   \app{(\abs{x}{\termt})}{\termm} & \bred & \termt[\termm / x] \\
 122   \termt \bred \termm & \Rightarrow & \left \{
 123     \begin{array}{l}
 124       \app{\termt}{\termn} \bred \app{\termm}{\termn} \\
 125       \app{\termn}{\termt} \bred \app{\termn}{\termm} \\
 126       \abs{x}{\termt}      \bred \abs{x}{\termm}
 127     \end{array}
 128     \right.
 129 \end{eqnarray*}
 130
 131 Where $\termt[\termm / x]$ expresses the operation that substitutes all
 132 occurrences of $x$ with $\termm$ in $\termt$.  For simplicity, we assume that
 133 all variables in a term are distinct.  This reduction practice takes the name of
 134 $\beta$-reduction.
 135
 136 % TODO put the trans closure
 137
 138 These few elements are of remarkable expressiveness, and in fact Turing
 139 complete.  As a corollary, we must be able to devise a term that reduces forever
 140 (``loops'' in imperative terms):
 141 \begin{equation*}
 142   \app{(\abs{x}{\app{x}{x}})}{(\abs{x}{\app{x}{x}})} \bred \app{(\abs{x}{\app{x}{x}})}{(\abs{x}{\app{x}{x}})} \bred \dots
 143 \end{equation*}
 144 Terms that can be reduced only a finite number of times (the non-looping ones)
 145 are said to be \emph{normalising}, and the ``final'' term is called \emph{normal
 146   form}.  These concepts (reduction and normal forms) will run through all the
 147 material analysed.
 148
 149 The $\lambda$-calculus has been extensively studied in literature.  Recursion in
 150 particular is a central subject, and very relevant to my thesis.
 151
 152 \subsection{Types}
 153
 154 While the $\lambda$-calculus is theoretically complete, in its raw form is quite
 155 unwieldy.  We cannot produce any data apart from $\lambda$-terms themselves, and
 156 as mentioned we cannot guarantee that terms will eventually produce something
 157 definitive.  Note that the latter property is often a necessary price: after
 158 all, if we can guarantee termination, then the language is not Turing complete,
 159 due to the halting problem.
 160
 161 One way to discipline $\lambda$-terms is to assign \emph{types} to them, and
 162 then check that the terms that we are forming ``makes sense'' given our typing
 163 rules.
 164
 165 We wish to introduce rules of the form $\Gamma \vdash \termt : \tau$, which
 166 reads ``in context $\Gamma$, term $\termt$ has type $\tau$''.
 167
 168 The syntax for types is as follows:
 169
 170 \newcommand{\tyarr}[2]{#1 \rightarrow #2}
 171
 172 \begin{eqnarray*}
 173   \tau & ::= & x \\
 174        &  |  & \tyarr{\tau}{\tau}
 175 \end{eqnarray*}
 176
 177 A context $\Gamma$ is a map from variables to types.  We use the notation
 178 $\Gamma, x : \tau$ to augment it.  Note that, being a map, no variable can
 179 appear twice as a subject in a context.
 180
 181 Predictably, $\tyarr{\tau}{\sigma}$ is the type of a function from $\tau$ to
 182 $\sigma$.  We need to be able to decorate our abstractions with
 183 types\footnote{Actually, we don't need to: computers can infer the right type
 184   easily, but that is another story.}:
 185
 186 \begin{eqnarray*}
 187   \termt & ::= & \dots \\
 188                &  |  & (\abs{x : \tau}{\termt})
 189 \end{eqnarray*}
 190
 191 Now we are ready to give the typing judgements:
 192
 193 \begin{center}
 194   \begin{prooftree}
 195     \AxiomC{}
 196     \UnaryInfC{$\Gamma, x : \tau \vdash x : \tau$}
 197   \end{prooftree}
 198   \begin{prooftree}
 199     \AxiomC{$\Gamma, x : \tau \vdash \termt : \sigma$}
 200     \UnaryInfC{$\Gamma \vdash \abs{x : \tau}{\termt} : \tyarr{\tau}{\sigma}$}
 201   \end{prooftree}
 202   \begin{prooftree}
 203     \AxiomC{$\Gamma \vdash \termt : \tyarr{\tau}{\sigma}$}
 204     \AxiomC{$\Gamma \vdash \termm : \tau$}
 205     \BinaryInfC{$\Gamma \vdash \app{\termt}{\termm} : \sigma$}
 206   \end{prooftree}
 207 \end{center}
 208
 209 This typing system takes the name of ``simply typed lambda calculus'' (STLC),
 210 and enjoys a number of properties.  In general, a well behaved type system has
 211 to preserve two properties: %TODO add credit to pierce
 212 \begin{description}
 213   \item[Progress] A well-typed term is not stuck (either it is a value or
 214     it can take a step according to the evaluation rules).
 215   \item[Preservation] If a well-typed term takes a step of evaluation, then
 216     the resulting term is also well typed.
 217 \end{description}
 218
 219 While the latter rule is clear, to understand the former property, consider the
 220 lambda calculus augmented with booleans:
 221
 222 \newcommand{\lctt}{\mathsf{true}}
 223 \newcommand{\lcff}{\mathsf{false}}
 224 \newcommand{\lcite}[3]{\mathsf{if}\ #1\ \mathsf{then}\ #2\ \mathsf{else}\ #2}
 225 \newcommand{\lcbool}{\mathsf{Bool}}
 226
 227 \begin{eqnarray*}
 228   \termt & ::= & \dots \\
 229          &  |  & \lctt \\
 230          &  |  & \lcff \\
 231          &  |  & \lcite{\termt}{\termm}{\termn}
 232 \end{eqnarray*}
 233 \begin{eqnarray*}
 234   \lcite{\lctt}{\termt}{\termm} & \bred & \termt \\
 235   \lcite{\lcff}{\termt}{\termm} & \bred & \termm
 236 \end{eqnarray*}
 237 \begin{eqnarray*}
 238   \tau & ::= & \dots \\
 239        &  |  & \lcbool
 240 \end{eqnarray*}
 241
 242 Terms like $(\app{\lctt}{\lcff})$ are what we call ``stuck'': no reduction rule
 243 applies to it.  We the help of the type system, we can check that this does not
 244 happen:
 245
 246 \begin{center}
 247   \begin{prooftree}
 248     \AxiomC{}
 249     \UnaryInfC{$\Gamma \vdash \lctt : \lcbool$}
 250   \end{prooftree}
 251   \begin{prooftree}
 252     \AxiomC{}
 253     \UnaryInfC{$\Gamma \vdash \lcff : \lcbool$}
 254   \end{prooftree}
 255   \begin{prooftree}
 256     \AxiomC{$\Gamma \vdash \termt : \lcbool$}
 257     \AxiomC{$\Gamma \vdash \termm : \tau$}
 258     \AxiomC{$\Gamma \vdash \termn : \tau$}
 259     \TrinaryInfC{$\Gamma \vdash \lcite{\termt}{\termm}{\termn} : \tau$}
 260   \end{prooftree}
 261 \end{center}
 262
 263 Then $\Gamma \not{\vdash}\ \lctt : \tyarr{\tau}{\sigma}$ and thus
 264 $(\app{\lctt}{\lcff})$ won't be table.
 265
 266 \end{document}