From 3821ab2a1c2d838f94b5c04a1557acc4ee7bcbfc Mon Sep 17 00:00:00 2001 From: Francesco Mazzoli Date: Mon, 17 Dec 2012 16:21:57 +0000 Subject: [PATCH] more background --- docs/background.tex | 276 ++++++++++++++++++++++++++++++-------------- 1 file changed, 190 insertions(+), 86 deletions(-) diff --git a/docs/background.tex b/docs/background.tex index 4c9263c..6e40d44 100644 --- a/docs/background.tex +++ b/docs/background.tex @@ -14,13 +14,14 @@ %% \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 @@ -81,9 +82,23 @@ \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 @@ -93,21 +108,21 @@ 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{\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 @@ -115,7 +130,7 @@ 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] \\ @@ -129,11 +144,9 @@ The ``applying'' is more formally explained with a reduction rule: \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 @@ -146,121 +159,212 @@ 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{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} -- 2.30.2