diff options
Diffstat (limited to 'docs')
| -rw-r--r-- | docs/background.tex | 186 |
1 files changed, 184 insertions, 2 deletions
diff --git a/docs/background.tex b/docs/background.tex index 6e93919..4c9263c 100644 --- 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} |