[bitonic-mengthesis.git] / 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}}{}

%% -----------------------------------------------------------------------------
%% Diagrams
% \usepackage{tikz}
% \usetikzlibrary{positioning}
%% \usetikzlibrary{shapes}
%% \usetikzlibrary{arrows}
%% \usepackage{tikz-cd}
%% \usepackage{pgfplots}
\usepackage[all]{xy}

%% -----------------------------------------------------------------------------
%% 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

The marriage between programming and logic has been a very fertile one.  In
particular, since the simply typed lambda calculus (STLC), a number of type
systems have been devised with increasing expressive power.

In the next sections I will give a very brief overview of STLC, and then
describe how to augment it to reach the theory I am interested in,
Inutitionistic Type Theory (ITT), also known as Martin-L\"{o}f Type Theory after
its inventor.

I will then explain why equality has been a tricky business in this theories,
and talk about the various attempts have been made.  One interesting development
has recently emerged: Observational Type theory.  I propose to explore the ways
to turn these ideas into useful practices for programming and theorem proving.

\section{Simple and not-so-simple types}

\subsection{Untyped $\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{\appspace}{\hspace{0.07cm}}
\newcommand{\app}[2]{#1\appspace#2}
\newcommand{\abs}[2]{\lambda #1. #2}
\newcommand{\termt}{\mathrm{T}}
\newcommand{\termm}{\mathrm{M}}
\newcommand{\termn}{\mathrm{N}}
\newcommand{\termp}{\mathrm{P}}
\newcommand{\separ}{\ |\ }

\begin{eqnarray*}
  \termt & ::= & x \separ (\abs{x}{\termt}) \separ (\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}{\to_{\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$.

% % 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.

\subsection{The simply typed $\lambda$-calculus}

\newcommand{\tya}{\mathrm{A}}
\newcommand{\tyb}{\mathrm{B}}
\newcommand{\tyc}{\mathrm{C}}

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

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

The syntax for types is as follows:

\newcommand{\tyarr}{\to}

\begin{equation*}
  \tya ::= x \separ \tya \tyarr \tya
\end{equation*}

The $x$ represents all the primitive types that we might want to add to our
calculus, for example $\mathbb{N}$ or $\mathsf{Bool}$.

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

Predictably, $\tya \tyarr \tyb$ is the type of a function from $\tya$ to
$\tyb$.  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{equation*}
  \termt ::= \dots \separ (\abs{x : \tya}{\termt})
\end{equation*}
Now we are ready to give the typing judgements:

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

This typing system takes the name of ``simply typed lambda calculus'' (STLC),
and enjoys a number of properties.  Two of them are expected in most type
systems: %TODO add credit to pierce
\begin{description}
  % TODO the definition of "stuck" thing is wrong
\item[Progress] A well-typed term is not stuck.  With stuck, we mean a compound
  term (not a variable or a value) that cannot be reduced further.  In the raw
  $\lambda$-calculus all we have is functions, but if we add other primitive
  types and constructors it's easy to see how things can go bad - for example
  trying to apply a boolean to something.
\item[Preservation] If a well-typed term takes a step of evaluation, then the
  resulting term is also well typed.
\end{description}

However, STLC buys us much more: every well-typed term
is normalising.  It is easy to see that we can't fill the blanks if we want to
give types to the non-normalising term shown before:
\begin{equation*}
  \app{(\abs{x : ?}{\app{x}{x}})}{(\abs{x : ?}{\app{x}{x}})}
\end{equation*}

\newcommand{\lcfix}[2]{\mathsf{fix} \appspace #1. #2}

This makes the STLC Turing incomplete.  We can recover the ability to loop by
adding a combinator that recurses:
\begin{equation*}
  \termt ::= \dots \separ  \lcfix{x : \tya}{\termt}
\end{equation*}
\begin{equation*}
  \lcfix{x : \tya}{\termt} \bred \termt[(\lcfix{x : \tya}{\termt}) / x]
\end{equation*}
\begin{center}
  \begin{prooftree}
    \AxiomC{$\Gamma,x : \tya \vdash \termt : \tya$}
    \UnaryInfC{$\Gamma \vdash \lcfix{x : \tya}{\termt} : \tya$}
  \end{prooftree}
\end{center}

However, we will keep STLC without such a facility. In the next section we shall
see why that is preferable for our needs.

\subsection{The Curry-Howard correspondence}

It turns out that the STLC can be seen a natural deduction system.  Terms are
proofs, and their types are the propositions they prove.  This remarkable fact
is known as the Curry-Howard isomorphism.

The ``arrow'' ($\to$) type corresponds to implication.  If we wished to
prove that $(\tya \tyarr \tyb) \tyarr (\tyb \tyarr \tyc) \tyarr (\tyc
\tyarr \tyc)$, all we need to do is to devise a $\lambda$-term that has the
correct type:
\begin{equation*}
  \abs{f : (\tya \tyarr \tyb)}{\abs{g : (\tyb \tyarr \tyc)}{\abs{x : \tya}{\app{g}{(\app{f}{x})}}}}
\end{equation*}
That is, function composition.  We might want extend our bare lambda calculus
with a couple of terms to make our natural deduction more pleasant to use.  For
example, tagged unions (\texttt{Either} in Haskell) are disjunctions, and tuples
are conjunctions.  We also want to be able to express falsity, and that is done
by introducing a type inhabited by no terms.  If evidence of such a type is
presented, then we can derive any type, which expresses absurdity.

\newcommand{\lcinl}{\mathsf{inl}\appspace}
\newcommand{\lcinr}{\mathsf{inr}\appspace}
\newcommand{\lccase}[3]{\mathsf{case}\appspace#1\appspace#2\appspace#3}
\newcommand{\lcfst}{\mathsf{fst}\appspace}
\newcommand{\lcsnd}{\mathsf{snd}\appspace}
\newcommand{\orint}{\vee I_{1,2}}
\newcommand{\orintl}{\vee I_{1}}
\newcommand{\orintr}{\vee I_{2}}
\newcommand{\orel}{\vee E}
\newcommand{\andint}{\wedge I}
\newcommand{\andel}{\wedge E_{1,2}}
\newcommand{\botel}{\bot E}
\newcommand{\lcabsurd}{\mathsf{absurd}\appspace}

\begin{eqnarray*}
  \termt & ::= & \dots \\
         &  |  & \lcinl \termt \separ \lcinr \termt \separ \lccase{\termt}{\termt}{\termt} \\
         &  |  & (\termt , \termt) \separ \lcfst \termt \separ \lcsnd \termt
\end{eqnarray*}
\begin{eqnarray*}
  \lccase{(\lcinl \termt)}{\termm}{\termn} & \bred & \app{\termm}{\termt} \\
  \lccase{(\lcinr \termt)}{\termm}{\termn} & \bred & \app{\termn}{\termt} \\
  \lcfst (\termt , \termm)                 & \bred & \termt \\
  \lcsnd (\termt , \termm)                 & \bred & \termm
\end{eqnarray*}
\begin{equation*}
  \tya ::= \dots \separ \tya \vee \tya \separ \tya \wedge \tya \separ \bot
\end{equation*}
\begin{center}
  \begin{prooftree}
    \AxiomC{$\Gamma \vdash \termt : \tya$}
    \RightLabel{$\orint$}
    \UnaryInfC{$\Gamma \vdash \lcinl \termt : \tya \vee \tyb$}
    \noLine
    \UnaryInfC{$\Gamma \vdash \lcinr \termt : \tyb \vee \tya$}
  \end{prooftree}
  \begin{prooftree}
    \AxiomC{$\Gamma \vdash \termt : \tya \vee \tyb$}
    \AxiomC{$\Gamma \vdash \termm : \tya \tyarr \tyc$}
    \AxiomC{$\Gamma \vdash \termn : \tyb \tyarr \tyc$}
    \RightLabel{$\orel$}
    \TrinaryInfC{$\Gamma \vdash \lccase{\termt}{\termm}{\termn} : \tyc$}
  \end{prooftree}
  \begin{prooftree}
    \AxiomC{$\Gamma \vdash \termt : \tya$}
    \AxiomC{$\Gamma \vdash \termm : \tyb$}
    \RightLabel{$\andint$}
    \BinaryInfC{$\Gamma \vdash (\tya , \tyb) : \tya \wedge \tyb$}
  \end{prooftree}
  \begin{prooftree}
    \AxiomC{$\Gamma \vdash \termt : \tya \wedge \tyb$}
    \RightLabel{$\andel$}
    \UnaryInfC{$\Gamma \vdash \lcfst \termt : \tya$}
    \noLine
    \UnaryInfC{$\Gamma \vdash \lcsnd \termt : \tyb$}
  \end{prooftree}
  \begin{prooftree}
    \AxiomC{$\Gamma \vdash \termt : \bot$}
    \RightLabel{$\botel$}
    \UnaryInfC{$\Gamma \vdash \lcabsurd \termt : \tya$}
  \end{prooftree}
\end{center}

With these rules, our STLC now looks remarkably similar in power and use to the
natural deduction we already know.  $\neg A$ can be expressed as $A \tyarr
\bot$.  However, there is an important omission: there is no term of the type $A
\vee \neg A$ (excluded middle), or equivalently $\neg \neg A \tyarr A$ (double
negation).

This has a considerable effect on our logic and it's no coincidence, since there
is no obvious computational behaviour for laws like the excluded middle.
Theories of this kind are called \emph{intuitionistic}, or \emph{constructive},
and all the systems analysed will have this characteristic since they build on
the foundation of the STLC.

\subsection{Extending the STLC}

\newcommand{\lctype}{\mathsf{Type}}
\newcommand{\lcite}[3]{\mathsf{if}\appspace#1\appspace\mathsf{then}\appspace#2\appspace\mathsf{else}\appspace#3}
\newcommand{\lcbool}{\mathsf{Bool}}

The STLC can be made more expressive in various ways.  Henk Barendregt
succinctly expressed geometrically how we can expand our type system:

\begin{equation*}
\xymatrix@!0@=1.5cm{
  & \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd]
  & & \lambda C \ar@{-}[dd]
  \\
  \lambda2 \ar@{-}[ur]\ar@{-}[rr]\ar@{-}[dd]
  & & \lambda P2 \ar@{-}[ur]\ar@{-}[dd]
  \\
  & \lambda\underline\omega \ar@{-}'[r][rr]
  & & \lambda P\underline\omega
  \\
  \lambda{\to} \ar@{-}[rr]\ar@{-}[ur]
  & & \lambda P \ar@{-}[ur]
}
\end{equation*}
Here $\lambda{\to}$, in the bottom left, is the STLC.  From there can move along
3 dimensions:
\begin{description}
\item[Terms depending on types (towards $\lambda{2}$)] In other words, we can
  quantify over types in our type signatures: $(\lambda A : \lctype. \lambda x :
  A. x) : \forall A. A \to A$.  The first and most famous instance of this idea
  has been System F.  This gives us a form of polymorphism and has been wildly
  successful, also thanks to a well known inference algorithm for a restricted
  version of System F known as Hindley-Milner.  Languages like Haskell and SML
  are based on this discipline.
\item[Types depending on types (towards $\lambda{\underline{\omega}}$)] In other
  words, we have type operators: $(\lambda A : \lctype. \lambda R : \lctype. (A \to R) \to R) : \lctype \to \lctype \to \lctype$.
\item[Types depending on terms (towards $\lambda{P}$)] Also known as ``dependent
  types'', give great expressive power: $(\lambda x :
  \lcbool. \lcite{x}{\mathbb{N}}{\mathbb{Q}}) : \lcbool \to \lctype$.
\end{description}

All the systems preserve the properties that make the STLC well behaved (some of
which I haven't mentioned yet).  The system we are going to focus on,
Intuitionistic Type Theory, has all of the above additions, and thus would sit
where $\lambda{C}$ sits in the ``$\lambda$-cube'' above.

\section{Intuitionistic Type Theory}

In this section I will describe 

\end{document}