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}
26 %% -----------------------------------------------------------------------------
28 \usepackage{amssymb,amsmath}
30 \usepackage{turnstile}
31 \usepackage{centernot}
33 %% -----------------------------------------------------------------------------
35 \usepackage{bussproofs}
37 \usepackage[export]{adjustbox}
41 %% \setcounter{secnumdepth}{0}
43 %% -----------------------------------------------------------------------------
44 % We will generate all images so they have a width \maxwidth. This means
45 % that they will get their normal width if they fit onto the page, but
46 % are scaled down if they would overflow the margins.
49 \ifdim\Gin@nat@width>\linewidth\linewidth
50 \else\Gin@nat@width\fi
54 %% -----------------------------------------------------------------------------
57 setpagesize=false, % page size defined by xetex
58 unicode=false, % unicode breaks when used with xetex
65 pdfauthor={Francesco Mazzoli <fm2209@ic.ac.uk>},
66 pdftitle={The Paths Towards Observational Equality},
71 % Make links footnotes instead of hotlinks:
72 \renewcommand{\href}[2]{#2\footnote{\url{#1}}}
74 % avoid problems with \sout in headers with hyperref:
75 \pdfstringdefDisableCommands{\renewcommand{\sout}{}}
77 \title{The Paths Towards Observational Equality}
78 \author{Francesco Mazzoli \url{<fm2209@ic.ac.uk>}}
85 The marriage between programming and logic has been a very fertile one. In
86 particular, since the simply typed lambda calculus (STLC), a number of type
87 systems have been devised with increasing expressive power.
89 In the next sections I will give a very brief overview of STLC, and then
90 describe how to augment it to reach the theory I am interested in,
91 Inutitionistic Type Theory (ITT), also known as Martin-L\"{o}f Type Theory after
94 I will then explain why equality has been a tricky business in this theories,
95 and talk about the various attempts have been made. One interesting development
96 has recently emerged: Observational Type theory. I propose to explore the ways
97 to turn these ideas into useful practices for programming and theorem proving.
99 \section{Simple and not-so-simple types}
101 \subsection{Untyped $\lambda$-calculus}
103 Along with Turing's machines, the earliest attempts to formalise computation
104 lead to the $\lambda$-calculus. This early programming language encodes
105 computation with a minimal sintax and most notably no ``data'' in the
106 traditional sense, but just functions.
108 The syntax of $\lambda$-terms consists of just three things: variables,
109 abstractions, and applications:
111 \newcommand{\appspace}{\hspace{0.07cm}}
112 \newcommand{\app}[2]{#1\appspace#2}
113 \newcommand{\abs}[2]{\lambda #1. #2}
114 \newcommand{\termt}{\mathrm{T}}
115 \newcommand{\termm}{\mathrm{M}}
116 \newcommand{\termn}{\mathrm{N}}
117 \newcommand{\termp}{\mathrm{P}}
118 \newcommand{\separ}{\ |\ }
121 \termt & ::= & x \separ (\abs{x}{\termt}) \separ (\app{\termt}{\termt}) \\
122 x & \in & \text{Some enumerable set of symbols, e.g.}\ \{x, y, z, \dots , x_1, x_2, \dots\}
125 % I will omit parethesis in the usual manner. %TODO explain how
127 Intuitively, abstractions ($\abs{x}{\termt}$) introduce functions with a named
128 parameter ($x$), and applications ($\app{\termt}{\termm}$) apply a function
129 ($\termt$) to an argument ($\termm$).
131 The ``applying'' is more formally explained with a reduction rule:
133 \newcommand{\bred}{\to_{\beta}}
136 \app{(\abs{x}{\termt})}{\termm} & \bred & \termt[\termm / x] \\
137 \termt \bred \termm & \Rightarrow & \left \{
139 \app{\termt}{\termn} \bred \app{\termm}{\termn} \\
140 \app{\termn}{\termt} \bred \app{\termn}{\termm} \\
141 \abs{x}{\termt} \bred \abs{x}{\termm}
146 Where $\termt[\termm / x]$ expresses the operation that substitutes all
147 occurrences of $x$ with $\termm$ in $\termt$.
149 % % TODO put the trans closure
151 These few elements are of remarkable expressiveness, and in fact Turing
152 complete. As a corollary, we must be able to devise a term that reduces forever
153 (``loops'' in imperative terms):
155 \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
157 Terms that can be reduced only a finite number of times (the non-looping ones)
158 are said to be \emph{normalising}, and the ``final'' term is called \emph{normal
159 form}. These concepts (reduction and normal forms) will run through all the
162 \subsection{The simply typed $\lambda$-calculus}
164 \newcommand{\tya}{\mathrm{A}}
165 \newcommand{\tyb}{\mathrm{B}}
166 \newcommand{\tyc}{\mathrm{C}}
168 One way to ``discipline'' $\lambda$-terms is to assign \emph{types} to them, and
169 then check that the terms that we are forming make sense given our typing rules.
171 We wish to introduce rules of the form $\Gamma \vdash \termt : \tya$, which
172 reads ``in context $\Gamma$, term $\termt$ has type $\tya$''.
174 The syntax for types is as follows:
176 \newcommand{\tyarr}{\to}
179 \tya ::= x \separ \tya \tyarr \tya
182 The $x$ represents all the primitive types that we might want to add to our
183 calculus, for example $\mathbb{N}$ or $\mathsf{Bool}$.
185 A context $\Gamma$ is a map from variables to types. We use the notation
186 $\Gamma, x : \tya$ to augment it. Note that, being a map, no variable can
187 appear twice as a subject in a context.
189 Predictably, $\tya \tyarr \tyb$ is the type of a function from $\tya$ to
190 $\tyb$. We need to be able to decorate our abstractions with
191 types\footnote{Actually, we don't need to: computers can infer the right type
192 easily, but that is another story.}:
194 \termt ::= \dots \separ (\abs{x : \tya}{\termt})
197 Now we are ready to give the typing judgements:
202 \UnaryInfC{$\Gamma, x : \tya \vdash x : \tya$}
205 \AxiomC{$\Gamma, x : \tya \vdash \termt : \tyb$}
206 \UnaryInfC{$\Gamma \vdash \abs{x : \tya}{\termt} : \tya \tyarr \tyb$}
209 \AxiomC{$\Gamma \vdash \termt : \tya \tyarr \tyb$}
210 \AxiomC{$\Gamma \vdash \termm : \tya$}
211 \BinaryInfC{$\Gamma \vdash \app{\termt}{\termm} : \tyb$}
215 This typing system takes the name of ``simply typed lambda calculus'' (STLC),
216 and enjoys a number of properties. Two of them are expected in most type
217 systems: %TODO add credit to pierce
219 \item[Progress] A well-typed term is not stuck. With stuck, we mean a compound
220 term (not a variable or a value) that cannot be reduced further. In the raw
221 $\lambda$-calculus all we have is functions, but if we add other primitive
222 types and constructors it's easy to see how things can go bad - for example
223 trying to apply a boolean to something.
224 \item[Preservation] If a well-typed term takes a step of evaluation, then the
225 resulting term is also well typed.
228 However, STLC buys us much more: every well-typed term
229 is normalising. It is easy to see that we can't fill the blanks if we want to
230 give types to the non-normalising term shown before:
232 \app{(\abs{x : ?}{\app{x}{x}})}{(\abs{x : ?}{\app{x}{x}})}
235 \newcommand{\lcfix}[2]{\mathsf{fix} \appspace #1. #2}
237 This makes the STLC Turing incomplete. We can recover the ability to loop by
238 adding a combinator that recurses:
240 \termt ::= \dots \separ \lcfix{x : \tya}{\termt}
243 \lcfix{x : \tya}{\termt} \bred \termt[(\lcfix{x : \tya}{\termt}) / x]
247 \AxiomC{$\Gamma,x : \tya \vdash \termt : \tya$}
248 \UnaryInfC{$\Gamma \vdash \lcfix{x : \tya}{\termt} : \tya$}
252 However, we will keep STLC without such a facility. In the next section we shall
253 see why that is preferable for our needs.
255 \subsection{The Curry-Howard correspondence}
257 It turns out that the STLC can be seen a natural deduction system. Terms are
258 proofs, and their types are the propositions they prove. This remarkable fact
259 is known as the Curry-Howard isomorphism.
261 The ``arrow'' ($\to$) type corresponds to implication. If we wished to
262 prove that $(\tya \tyarr \tyb) \tyarr (\tyb \tyarr \tyc) \tyarr (\tyc
263 \tyarr \tyc)$, all we need to do is to devise a $\lambda$-term that has the
266 \abs{f : (\tya \tyarr \tyb)}{\abs{g : (\tyb \tyarr \tyc)}{\abs{x : \tya}{\app{g}{(\app{f}{x})}}}}
268 That is, function composition. We might want extend our bare lambda calculus
269 with a couple of terms to make our natural deduction more pleasant to use. For
270 example, tagged unions (\texttt{Either} in Haskell) are disjunctions, and tuples
271 are conjunctions. We also want to be able to express falsity, and that is done
272 by introduced a type ``inhabited'' by no terms. If evidence of such a type is
273 presented, then we can derive any type, which expresses absurdity.
275 \newcommand{\lcinl}{\mathsf{inl}\appspace}
276 \newcommand{\lcinr}{\mathsf{inr}\appspace}
277 \newcommand{\lccase}[3]{\mathsf{case}\appspace#1\appspace#2\appspace#3}
278 \newcommand{\lcfst}{\mathsf{fst}\appspace}
279 \newcommand{\lcsnd}{\mathsf{snd}\appspace}
280 \newcommand{\orint}{\vee I_{1,2}}
281 \newcommand{\orintl}{\vee I_{1}}
282 \newcommand{\orintr}{\vee I_{2}}
283 \newcommand{\orel}{\vee E}
284 \newcommand{\andint}{\wedge I}
285 \newcommand{\andel}{\wedge E_{1,2}}
286 \newcommand{\botel}{\bot E}
287 \newcommand{\lcabsurd}{\mathsf{absurd}\appspace}
290 \termt & ::= & \dots \\
291 & | & \lcinl \termt \separ \lcinr \termt \separ \lccase{\termt}{\termt}{\termt} \\
292 & | & (\termt , \termt) \separ \lcfst \termt \separ \lcsnd \termt
295 \lccase{(\lcinl \termt)}{\termm}{\termn} & \bred & \app{\termm}{\termt} \\
296 \lccase{(\lcinr \termt)}{\termm}{\termn} & \bred & \app{\termn}{\termt} \\
297 \lcfst (\termt , \termm) & \bred & \termt \\
298 \lcsnd (\termt , \termm) & \bred & \termm
301 \tya ::= \dots \separ \tya \vee \tya \separ \tya \wedge \tya \separ \bot
305 \AxiomC{$\Gamma \vdash \termt : \tya$}
306 \RightLabel{$\orint$}
307 \UnaryInfC{$\Gamma \vdash \lcinl \termt : \tya \vee \tyb$}
309 \UnaryInfC{$\Gamma \vdash \lcinr \termt : \tyb \vee \tya$}
312 \AxiomC{$\Gamma \vdash \termt : \tya \vee \tyb$}
313 \AxiomC{$\Gamma \vdash \termm : \tya \tyarr \tyc$}
314 \AxiomC{$\Gamma \vdash \termn : \tyb \tyarr \tyc$}
316 \TrinaryInfC{$\Gamma \vdash \lccase{\termt}{\termm}{\termn} : \tyc$}
319 \AxiomC{$\Gamma \vdash \termt : \tya$}
320 \AxiomC{$\Gamma \vdash \termm : \tyb$}
321 \RightLabel{$\andint$}
322 \BinaryInfC{$\Gamma \vdash (\tya , \tyb) : \tya \wedge \tyb$}
325 \AxiomC{$\Gamma \vdash \termt : \tya \wedge \tyb$}
326 \RightLabel{$\andel$}
327 \UnaryInfC{$\Gamma \vdash \lcfst \termt : \tya$}
329 \UnaryInfC{$\Gamma \vdash \lcsnd \termt : \tyb$}
332 \AxiomC{$\Gamma \vdash \termt : \bot$}
333 \RightLabel{$\botel$}
334 \UnaryInfC{$\Gamma \vdash \lcabsurd \termt : \tya$}
338 With these rules, our STLC now looks remarkably similar in power and use to the
339 natural deduction we already know. $\neg A$ can be expressed as $A \tyarr
340 \bot$. However, there is an important omission: there is no term of the type $A
341 \vee \neg A$ (excluded middle), or equivalently $\neg \neg A \tyarr A$ (double
344 This has a considerable effect on our logic and it's no coincidence, since there
345 is no obvious computational behaviour for laws like the excluded middle.
346 Theories of this kind are called \emph{intuitionistic}, or \emph{constructive},
347 and all the systems analysed will have this characteristic since they build on
348 the foundation of the STLC.
350 \subsection{Extending the STLC}
352 The STLC can be made more expressive in various ways. Henk Barendregt
353 succinctly expressed geometrically in what ``direction'' we can expand our type
357 & \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd]
358 & & \lambda C \ar@{-}[dd]
360 \lambda2 \ar@{-}[ur]\ar@{-}[rr]\ar@{-}[dd]
361 & & \lambda P2 \ar@{-}[ur]\ar@{-}[dd]
363 & \lambda\underline\omega \ar@{-}'[r][rr]
364 & & \lambda P\underline\omega
366 \lambda{\to} \ar@{-}[rr]\ar@{-}[ur]
367 & & \lambda P \ar@{-}[ur]