1 \documentclass[article, a4paper]{article}
2 \usepackage[T1]{fontenc}
5 \usepackage[normalem]{ulem}
7 \usepackage{subcaption}
9 %% -----------------------------------------------------------------------------
11 %% \usepackage[osf]{libertine}
12 %% \usepackage{helvet}
13 %% \usepackage{lmodern}
14 %% \IfFileExists{microtype.sty}{\usepackage{microtype}}{}
16 %% -----------------------------------------------------------------------------
19 %% \usetikzlibrary{positioning}
20 %% \usetikzlibrary{shapes}
21 %% \usetikzlibrary{arrows}
22 %% \usepackage{tikz-cd}
23 %% \usepackage{pgfplots}
25 %% -----------------------------------------------------------------------------
27 \usepackage{amssymb,amsmath}
29 \usepackage{turnstile}
30 \usepackage{centernot}
32 %% -----------------------------------------------------------------------------
34 \usepackage{bussproofs}
36 \usepackage[export]{adjustbox}
40 %% \setcounter{secnumdepth}{0}
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.
48 \ifdim\Gin@nat@width>\linewidth\linewidth
49 \else\Gin@nat@width\fi
53 %% -----------------------------------------------------------------------------
56 setpagesize=false, % page size defined by xetex
57 unicode=false, % unicode breaks when used with xetex
64 pdfauthor={Francesco Mazzoli <fm2209@ic.ac.uk>},
65 pdftitle={The Paths Towards Observational Equality},
70 % Make links footnotes instead of hotlinks:
71 \renewcommand{\href}[2]{#2\footnote{\url{#1}}}
73 % avoid problems with \sout in headers with hyperref:
74 \pdfstringdefDisableCommands{\renewcommand{\sout}{}}
76 \title{The Paths Towards Observational Equality}
77 \author{Francesco Mazzoli \url{<fm2209@ic.ac.uk>}}
84 \section{Functional programming}
86 \subsection{The $\lambda$-calculus}
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.
93 The syntax of $\lambda$-terms consists of just three things: variables,
94 abstractions, and applications:
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}}
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\}
110 I will omit parethesis in the usual manner. %TODO explain how
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$).
116 The ``applying'' is more formally explained with a reduction rule:
118 \newcommand{\bred}{\rightarrow_{\beta}}
121 \app{(\abs{x}{\termt})}{\termm} & \bred & \termt[\termm / x] \\
122 \termt \bred \termm & \Rightarrow & \left \{
124 \app{\termt}{\termn} \bred \app{\termm}{\termn} \\
125 \app{\termn}{\termt} \bred \app{\termn}{\termm} \\
126 \abs{x}{\termt} \bred \abs{x}{\termm}
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
136 % TODO put the trans closure
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):
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
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
149 The $\lambda$-calculus has been extensively studied in literature. Recursion in
150 particular is a central subject, and very relevant to my thesis.
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.
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
165 We wish to introduce rules of the form $\Gamma \vdash \termt : \tau$, which
166 reads ``in context $\Gamma$, term $\termt$ has type $\tau$''.
168 The syntax for types is as follows:
170 \newcommand{\tyarr}[2]{#1 \rightarrow #2}
174 & | & \tyarr{\tau}{\tau}
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.
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.}:
187 \termt & ::= & \dots \\
188 & | & (\abs{x : \tau}{\termt})
191 Now we are ready to give the typing judgements:
196 \UnaryInfC{$\Gamma, x : \tau \vdash x : \tau$}
199 \AxiomC{$\Gamma, x : \tau \vdash \termt : \sigma$}
200 \UnaryInfC{$\Gamma \vdash \abs{x : \tau}{\termt} : \tyarr{\tau}{\sigma}$}
203 \AxiomC{$\Gamma \vdash \termt : \tyarr{\tau}{\sigma}$}
204 \AxiomC{$\Gamma \vdash \termm : \tau$}
205 \BinaryInfC{$\Gamma \vdash \app{\termt}{\termm} : \sigma$}
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
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.
219 While the latter rule is clear, to understand the former property, consider the
220 lambda calculus augmented with booleans:
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}}
228 \termt & ::= & \dots \\
231 & | & \lcite{\termt}{\termm}{\termn}
234 \lcite{\lctt}{\termt}{\termm} & \bred & \termt \\
235 \lcite{\lcff}{\termt}{\termm} & \bred & \termm
238 \tau & ::= & \dots \\
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
249 \UnaryInfC{$\Gamma \vdash \lctt : \lcbool$}
253 \UnaryInfC{$\Gamma \vdash \lcff : \lcbool$}
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$}
263 Then $\Gamma \not{\vdash}\ \lctt : \tyarr{\tau}{\sigma}$ and thus
264 $(\app{\lctt}{\lcff})$ won't be table.