path: root/docs/background.tex

\documentclass[article, a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{fixltx2e}
\usepackage{enumitem}
\usepackage[normalem]{ulem}
\usepackage{graphicx}
\usepackage{subcaption}

%% -----------------------------------------------------------------------------
%% Fonts
%% \usepackage[osf]{libertine}
%% \usepackage{helvet}
%% \usepackage{lmodern}
%% \IfFileExists{microtype.sty}{\usepackage{microtype}}{}

%% -----------------------------------------------------------------------------
%% TikZ stuff
%% \usepackage{tikz}
%% \usetikzlibrary{positioning}
%% \usetikzlibrary{shapes}
%% \usetikzlibrary{arrows}
%% \usepackage{tikz-cd}
%% \usepackage{pgfplots}

%% -----------------------------------------------------------------------------
%% Symbols
\usepackage{amssymb,amsmath}
\usepackage{wasysym}
\usepackage{turnstile}
\usepackage{centernot}

%% -----------------------------------------------------------------------------
%% Utils
\usepackage{bussproofs}
\usepackage{umoline}
\usepackage[export]{adjustbox}
\usepackage{multicol}

%% Numbering depth
%% \setcounter{secnumdepth}{0}

%% -----------------------------------------------------------------------------
% We will generate all images so they have a width \maxwidth. This means
% that they will get their normal width if they fit onto the page, but
% are scaled down if they would overflow the margins.
\makeatletter
\def\maxwidth{
  \ifdim\Gin@nat@width>\linewidth\linewidth
  \else\Gin@nat@width\fi
}
\makeatother

%% -----------------------------------------------------------------------------
%% Links
\usepackage[
  setpagesize=false, % page size defined by xetex
  unicode=false, % unicode breaks when used with xetex
  xetex
]{hyperref}

\hypersetup{
  breaklinks=true,
  bookmarks=true,
  pdfauthor={Francesco Mazzoli <fm2209@ic.ac.uk>},
  pdftitle={The Paths Towards Observational Equality},
  colorlinks=false,
  pdfborder={0 0 0}
}

% Make links footnotes instead of hotlinks:
\renewcommand{\href}[2]{#2\footnote{\url{#1}}}

% avoid problems with \sout in headers with hyperref:
\pdfstringdefDisableCommands{\renewcommand{\sout}{}}

\title{The Paths Towards Observational Equality}
\author{Francesco Mazzoli \url{<fm2209@ic.ac.uk>}}
\date{December 2012}

\begin{document}

\maketitle

\section{Functional programming}

\subsection{The $\lambda$-calculus}

Along with Turing's machines, the earliest attempts to formalise computation
lead to the $\lambda$-calculus.  This early programming language encodes
computation with a minimal sintax and most notably no ``data'' in the
traditional sense, but just functions.

The syntax of $\lambda$-terms consists of just three things: variables,
abstractions, and applications:

\newcommand{\app}[2]{#1\hspace{0.07cm}#2}
\newcommand{\abs}[2]{\lambda #1. #2}
\newcommand{\termt}{\mathrm{T}}
\newcommand{\termm}{\mathrm{M}}
\newcommand{\termn}{\mathrm{N}}
\newcommand{\termp}{\mathrm{P}}

\begin{eqnarray*}
  \termt & ::= & x \\
         &  |  & (\abs{x}{\termt}) \\
         &  |  & (\app{\termt}{\termt}) \\
  x & \in & \text{Some enumerable set of symbols, e.g.}\ \{x, y, z, \dots , x_1, x_2, \dots\}
\end{eqnarray*}

I will omit parethesis in the usual manner. %TODO explain how

Intuitively, abstractions ($\abs{x}{\termt}$) introduce functions with a named
parameter ($x$), and applications ($\app{\termt}{\termm}$) apply a function
($\termt$) to an argument ($\termm$).

The ``applying'' is more formally explained with a reduction rule:

\newcommand{\bred}{\rightarrow_{\beta}}

\begin{eqnarray*}
  \app{(\abs{x}{\termt})}{\termm} & \bred & \termt[\termm / x] \\
  \termt \bred \termm & \Rightarrow & \left \{
    \begin{array}{l}
      \app{\termt}{\termn} \bred \app{\termm}{\termn} \\
      \app{\termn}{\termt} \bred \app{\termn}{\termm} \\
      \abs{x}{\termt}      \bred \abs{x}{\termm}
    \end{array}
    \right.
\end{eqnarray*}

Where $\termt[\termm / x]$ expresses the operation that substitutes all
occurrences of $x$ with $\termm$ in $\termt$.  For simplicity, we assume that
all variables in a term are distinct.  This reduction practice takes the name of
$\beta$-reduction.

% TODO put the trans closure

These few elements are of remarkable expressiveness, and in fact Turing
complete.  As a corollary, we must be able to devise a term that reduces forever
(``loops'' in imperative terms):
\begin{equation*}
  \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
\end{equation*}
Terms that can be reduced only a finite number of times (the non-looping ones)
are said to be \emph{normalising}, and the ``final'' term is called \emph{normal
  form}.  These concepts (reduction and normal forms) will run through all the
material analysed.

The $\lambda$-calculus has been extensively studied in literature.  Recursion in
particular is a central subject, and very relevant to my thesis.

\subsection{Types}

While the $\lambda$-calculus is theoretically complete, in its raw form is quite
unwieldy.  We cannot produce any data apart from $\lambda$-terms themselves, and
as mentioned we cannot guarantee that terms will eventually produce something
definitive.  Note that the latter property is often a necessary price: after
all, if we can guarantee termination, then the language is not Turing complete,
due to the halting problem.

One way to discipline $\lambda$-terms is to assign \emph{types} to them, and
then check that the terms that we are forming ``makes sense'' given our typing
rules.

We wish to introduce rules of the form $\Gamma \vdash \termt : \tau$, which
reads ``in context $\Gamma$, term $\termt$ has type $\tau$''.

The syntax for types is as follows:

\newcommand{\tyarr}[2]{#1 \rightarrow #2}

\begin{eqnarray*}
  \tau & ::= & x \\
       &  |  & \tyarr{\tau}{\tau}
\end{eqnarray*}

A context $\Gamma$ is a map from variables to types.  We use the notation
$\Gamma, x : \tau$ to augment it.  Note that, being a map, no variable can
appear twice as a subject in a context.

Predictably, $\tyarr{\tau}{\sigma}$ is the type of a function from $\tau$ to
$\sigma$.  We need to be able to decorate our abstractions with
types\footnote{Actually, we don't need to: computers can infer the right type
  easily, but that is another story.}:

\begin{eqnarray*}
  \termt & ::= & \dots \\
               &  |  & (\abs{x : \tau}{\termt})
\end{eqnarray*}

Now we are ready to give the typing judgements:

\begin{center}
  \begin{prooftree}
    \AxiomC{}
    \UnaryInfC{$\Gamma, x : \tau \vdash x : \tau$}
  \end{prooftree}
  \begin{prooftree}
    \AxiomC{$\Gamma, x : \tau \vdash \termt : \sigma$}
    \UnaryInfC{$\Gamma \vdash \abs{x : \tau}{\termt} : \tyarr{\tau}{\sigma}$}
  \end{prooftree}
  \begin{prooftree}
    \AxiomC{$\Gamma \vdash \termt : \tyarr{\tau}{\sigma}$}
    \AxiomC{$\Gamma \vdash \termm : \tau$}
    \BinaryInfC{$\Gamma \vdash \app{\termt}{\termm} : \sigma$}
  \end{prooftree}
\end{center}

This typing system takes the name of ``simply typed lambda calculus'' (STLC),
and enjoys a number of properties.  In general, a well behaved type system has
to preserve two properties: %TODO add credit to pierce
\begin{description}
  \item[Progress] A well-typed term is not stuck (either it is a value or
    it can take a step according to the evaluation rules).
  \item[Preservation] If a well-typed term takes a step of evaluation, then
    the resulting term is also well typed.
\end{description}

While the latter rule is clear, to understand the former property, consider the
lambda calculus augmented with booleans:

\newcommand{\lctt}{\mathsf{true}}
\newcommand{\lcff}{\mathsf{false}}
\newcommand{\lcite}[3]{\mathsf{if}\ #1\ \mathsf{then}\ #2\ \mathsf{else}\ #2}
\newcommand{\lcbool}{\mathsf{Bool}}

\begin{eqnarray*}
  \termt & ::= & \dots \\
         &  |  & \lctt \\
         &  |  & \lcff \\
         &  |  & \lcite{\termt}{\termm}{\termn}
\end{eqnarray*}
\begin{eqnarray*}
  \lcite{\lctt}{\termt}{\termm} & \bred & \termt \\
  \lcite{\lcff}{\termt}{\termm} & \bred & \termm
\end{eqnarray*}
\begin{eqnarray*}
  \tau & ::= & \dots \\
       &  |  & \lcbool
\end{eqnarray*}

Terms like $(\app{\lctt}{\lcff})$ are what we call ``stuck'': no reduction rule
applies to it.  We the help of the type system, we can check that this does not
happen:

\begin{center}
  \begin{prooftree}
    \AxiomC{}
    \UnaryInfC{$\Gamma \vdash \lctt : \lcbool$}
  \end{prooftree}
  \begin{prooftree}
    \AxiomC{}
    \UnaryInfC{$\Gamma \vdash \lcff : \lcbool$}
  \end{prooftree}
  \begin{prooftree}
    \AxiomC{$\Gamma \vdash \termt : \lcbool$}
    \AxiomC{$\Gamma \vdash \termm : \tau$}
    \AxiomC{$\Gamma \vdash \termn : \tau$}
    \TrinaryInfC{$\Gamma \vdash \lcite{\termt}{\termm}{\termn} : \tau$}
  \end{prooftree}
\end{center}

Then $\Gamma \not{\vdash}\ \lctt : \tyarr{\tau}{\sigma}$ and thus
$(\app{\lctt}{\lcff})$ won't be table.

\end{document}