%% \IfFileExists{microtype.sty}{\usepackage{microtype}}{}
%% -----------------------------------------------------------------------------
-%% TikZ stuff
-%% \usepackage{tikz}
-%% \usetikzlibrary{positioning}
+%% Diagrams
+% \usepackage{tikz}
+% \usetikzlibrary{positioning}
%% \usetikzlibrary{shapes}
%% \usetikzlibrary{arrows}
%% \usepackage{tikz-cd}
%% \usepackage{pgfplots}
+\usepackage[all]{xy}
%% -----------------------------------------------------------------------------
%% Symbols
\maketitle
-\section{Functional programming}
+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.
-\subsection{The $\lambda$-calculus}
+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
The syntax of $\lambda$-terms consists of just three things: variables,
abstractions, and applications:
-\newcommand{\app}[2]{#1\hspace{0.07cm}#2}
+\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 \\
- & | & (\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\}
+ \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
+% 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
The ``applying'' is more formally explained with a reduction rule:
-\newcommand{\bred}{\rightarrow_{\beta}}
+\newcommand{\bred}{\to_{\beta}}
\begin{eqnarray*}
\app{(\abs{x}{\termt})}{\termm} & \bred & \termt[\termm / x] \\
\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.
+occurrences of $x$ with $\termm$ in $\termt$.
-% TODO put the trans closure
+% % 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
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{The simply typed $\lambda$-calculus}
-\subsection{Types}
+\newcommand{\tya}{\mathrm{A}}
+\newcommand{\tyb}{\mathrm{B}}
+\newcommand{\tyc}{\mathrm{C}}
-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 make sense given our typing rules.
-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$''.
+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}[2]{#1 \rightarrow #2}
+\newcommand{\tyarr}{\to}
-\begin{eqnarray*}
- \tau & ::= & x \\
- & | & \tyarr{\tau}{\tau}
-\end{eqnarray*}
+\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 : \tau$ to augment it. Note that, being a map, no variable can
+$\Gamma, x : \tya$ 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
+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{eqnarray*}
- \termt & ::= & \dots \\
- & | & (\abs{x : \tau}{\termt})
-\end{eqnarray*}
+\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 : \tau \vdash x : \tau$}
+ \UnaryInfC{$\Gamma, x : \tya \vdash x : \tya$}
\end{prooftree}
\begin{prooftree}
- \AxiomC{$\Gamma, x : \tau \vdash \termt : \sigma$}
- \UnaryInfC{$\Gamma \vdash \abs{x : \tau}{\termt} : \tyarr{\tau}{\sigma}$}
+ \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 : \tyarr{\tau}{\sigma}$}
- \AxiomC{$\Gamma \vdash \termm : \tau$}
- \BinaryInfC{$\Gamma \vdash \app{\termt}{\termm} : \sigma$}
+ \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. In general, a well behaved type system has
-to preserve two properties: %TODO add credit to pierce
+and enjoys a number of properties. Two of them are expected in most type
+systems: %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.
+\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}
-While the latter rule is clear, to understand the former property, consider the
-lambda calculus augmented with booleans:
+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{\lctt}{\mathsf{true}}
-\newcommand{\lcff}{\mathsf{false}}
-\newcommand{\lcite}[3]{\mathsf{if}\ #1\ \mathsf{then}\ #2\ \mathsf{else}\ #2}
-\newcommand{\lcbool}{\mathsf{Bool}}
+\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 introduced 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 \\
- & | & \lctt \\
- & | & \lcff \\
- & | & \lcite{\termt}{\termm}{\termn}
-\end{eqnarray*}
-\begin{eqnarray*}
- \lcite{\lctt}{\termt}{\termm} & \bred & \termt \\
- \lcite{\lcff}{\termt}{\termm} & \bred & \termm
+ & | & \lcinl \termt \separ \lcinr \termt \separ \lccase{\termt}{\termt}{\termt} \\
+ & | & (\termt , \termt) \separ \lcfst \termt \separ \lcsnd \termt
\end{eqnarray*}
\begin{eqnarray*}
- \tau & ::= & \dots \\
- & | & \lcbool
+ \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*}
-
-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{equation*}
+ \tya ::= \dots \separ \tya \vee \tya \separ \tya \wedge \tya \separ \bot
+\end{equation*}
\begin{center}
\begin{prooftree}
- \AxiomC{}
- \UnaryInfC{$\Gamma \vdash \lctt : \lcbool$}
+ \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{}
- \UnaryInfC{$\Gamma \vdash \lcff : \lcbool$}
+ \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 : \lcbool$}
- \AxiomC{$\Gamma \vdash \termm : \tau$}
- \AxiomC{$\Gamma \vdash \termn : \tau$}
- \TrinaryInfC{$\Gamma \vdash \lcite{\termt}{\termm}{\termn} : \tau$}
+ \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}
-Then $\Gamma \not{\vdash}\ \lctt : \tyarr{\tau}{\sigma}$ and thus
-$(\app{\lctt}{\lcff})$ won't be table.
+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}
+
+The STLC can be made more expressive in various ways. Henk Barendregt
+succinctly expressed geometrically in what ``direction'' we can expand our type
+system:
+
+\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{document}
projects / bitonic-mengthesis.git / commitdiff