lambda-calculus stuff

diff --git a/docs/background.tex b/docs/background.tex
index 6e939197a8bcf82ee3dad1f5488a4d06afc8df48..4c9263c1f252ccd85ddcfd0a4d1255676ba5d422 100644 (file)
--- a/docs/background.tex
+++ b/docs/background.tex
@@ -62,7 +62,7 @@
   breaklinks=true,
   bookmarks=true,
   pdfauthor={Francesco Mazzoli <fm2209@ic.ac.uk>},
-  pdftitle={The Path Towards Observational Equality},
+  pdftitle={The Paths Towards Observational Equality},
   colorlinks=false,
   pdfborder={0 0 0}
 }
@@ -73,7 +73,7 @@
 % avoid problems with \sout in headers with hyperref:
 \pdfstringdefDisableCommands{\renewcommand{\sout}{}}
 
-\title{The Path Towards Observational Equality}
+\title{The Paths Towards Observational Equality}
 \author{Francesco Mazzoli \url{<fm2209@ic.ac.uk>}}
 \date{December 2012}
 
@@ -81,4 +81,186 @@
 
 \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}