diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | thesis.bib | 7 | ||||
| -rw-r--r-- | thesis.lagda | 317 |
3 files changed, 316 insertions, 10 deletions
@@ -15,7 +15,7 @@ thesis.pdf: thesis.tex thesis.bib agda.sty agda.sty: thesis.tex thesis.tex: thesis.lagda - agda --latex --latex-dir . -i . -i ~/src/agda-lib/src/ thesis.lagda + agda --allow-unsolved-metas --latex --latex-dir . -i . -i ~/src/agda-lib/src/ thesis.lagda InterimReport.pdf: InterimReport.tex InterimReport.bib InterimReport.agda xelatex -halt-on-error $< -o $@ @@ -12,6 +12,13 @@ year = {2002} } +@inbook{Queinnec2003, + author = {Christian Queinnec}, + title = {Lisp in Small Pieces}, + publisher = {Cambridge University Press}, + year = {2003}, +} + @online{Coq, author = {{The Coq Team}}, title = {The Coq Proof Assistant}, diff --git a/thesis.lagda b/thesis.lagda index 4407487..b1539c6 100644 --- a/thesis.lagda +++ b/thesis.lagda @@ -1,7 +1,7 @@ \documentclass[report]{article} %% Narrow margins -\usepackage{fullpage} +% \usepackage{fullpage} %% Bibtex \usepackage{natbib} @@ -9,6 +9,15 @@ %% Links \usepackage{hyperref} +%% Frames +\usepackage{framed} + +%% Symbols +\usepackage[fleqn]{amsmath} + +%% Proof trees +\usepackage{bussproofs} + %% ----------------------------------------------------------------------------- %% Commands for Agda \usepackage[english]{babel} @@ -25,16 +34,64 @@ \newcommand{\mysyn}{\AgdaKeyword} \newcommand{\mytyc}{\AgdaDatatype} -\newcommand{\myind}{\AgdaInductiveConstructor} +\newcommand{\mydc}{\AgdaInductiveConstructor} \newcommand{\myfld}{\AgdaField} \newcommand{\myfun}{\AgdaFunction} -\newcommand{\myb}{\AgdaBound} +% TODO make this use AgdaBount +\newcommand{\myb}[1]{\ensuremath{#1}} \newcommand{\myfield}{\AgdaField} +\newcommand{\myind}{\AgdaIndent} +\newcommand{\mykant}{\textsc{Kant}} +\newcommand{\mysynel}[1]{\langle #1 \rangle} +\newcommand{\mytmsyn}{\mysynel{term}} +\newcommand{\mysp}{\ } +\newcommand{\myabs}[2]{\lambda #1 \mapsto #2} +\newcommand{\myappsp}{\hspace{0.07cm}} +\newcommand{\myapp}[2]{#1 \myappsp #2} +\newcommand{\mysynsep}{\ \ |\ \ } + +\FrameSep0.3cm +\newcommand{\mydesc}[3]{ + \hfill \textbf{#1} $#2$ + \vspace{-0.2cm} + \begin{framed} + #3 + \end{framed} +} + +% TODO is \mathbin the correct thing for arrow and times? + +\newcommand{\mytmt}{\myb{T}} +\newcommand{\mytmm}{\myb{M}} +\newcommand{\mytmn}{\myb{N}} +\newcommand{\myred}{\leadsto} +\newcommand{\mysub}[3]{#1[#2 \mapsto #3]} +\newcommand{\mytysyn}{\mysynel{type}} +\newcommand{\mybasetys}{K} +% TODO change this name +\newcommand{\mybasety}[1]{B_{#1}} +\newcommand{\mytya}{\myb{A}} +\newcommand{\mytyb}{\myb{B}} +\newcommand{\myarr}{\mathbin{\textcolor{AgdaDatatype}{\to}}} +\newcommand{\myprod}{\mathbin{\textcolor{AgdaDatatype}{\times}}} +\newcommand{\myctx}{\Gamma} +\newcommand{\myvalid}[1]{#1 \vdash \underline{\mathrm{valid}}} +\newcommand{\myjudd}[3]{#1 \vdash #2 : #3} +\newcommand{\myjud}[2]{\myjudd{\myctx}{#1}{#2}} +\newcommand{\myabss}[3]{\lambda #1 {:} #2 \mapsto #3} +\newcommand{\mytt}{\mydc{tt}} +\newcommand{\myunit}{\mytyc{$\top$}} +\newcommand{\mypair}[2]{(#1\mathpunct{\textcolor{AgdaInductiveConstructor}{,}} #2)} +\newcommand{\myfst}[1]{\myapp{\myfld{fst}}{#1}} +\newcommand{\mysnd}[1]{\myapp{\myfld{snd}}{#1}} +\newcommand{\myconst}{\myb{c}} +\newcommand{\myemptyctx}{\cdot} +\newcommand{\myhole}{\AgdaUnsolvedMeta} +\newcommand{\myfix}[3]{\mysyn{fix} \myappsp #1 {:} #2 \mapsto #3} %% ----------------------------------------------------------------------------- -\title{\textsc{Kant}: Implementing Observational Equality} -% TODO remove double @ if we get rid of lhs2TeX +\title{\mykant: Implementing Observational Equality} \author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}} \date{June 2013} @@ -76,29 +133,271 @@ open import Level \section{Simple and not-so-simple types} \label{sec:types} -\section{Intuitionistic Type Theory and dependent types} +\subsection{The untyped $\lambda$-calculus} + +Along with Turing's machines, the earliest attempts to formalise computation +lead to the $\lambda$-calculus \citep{Church1936}. This early programming +language encodes computation with a minimal syntax and no `data' in the +traditional sense, but just functions. Here we give a brief overview of the +language, which will give the chance to introduce concepts central to the +analysis of all the following calculi. The exposition follows the one found in +chapter 5 of \cite{Queinnec2003}. + +The syntax of $\lambda$-terms consists of three things: variables, abstractions, +and applications: + +\mydesc{syntax}{ }{ + $ + \begin{array}{r@{\ }c@{\ }l} + \mytmsyn & ::= & \myb{x} \mysynsep \myabs{\myb{x}}{\mytmsyn} \mysynsep (\myapp{\mytmsyn}{\mytmsyn}) \\ + x & \in & \text{Some enumerable set of symbols} + \end{array} + $ +} + +Through this text, I will use $\mytmt$, $\mytmm$, $\mytmn$ to indicate a generic +term, and $x$, $y$ to refer to variables. Parenthesis will be omitted in the +usual way: $\myapp{\myapp{\mytmt}{\mytmm}}{\mytmn} = +\myapp{(\myapp{\mytmt}{\mytmm})}{\mytmn}$. + +Abstractions roughly corresponds to functions, and their semantics is more +formally explained by the $\beta$-reduction rule: + +\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{ + $ + \begin{array}{l} + \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{x}{\mytmn}\text{, where} \\ + \myind{1} + \begin{array}{l@{\ }c@{\ }l} + \mysub{x}{x}{\mytmn} & = & \mytmn \\ + \mysub{y}{x}{\mytmn} & = & y\text{, with } x \neq y \\ + \mysub{\myapp{\mytmt}{\mytmm}}{x}{\mytmn} & = & (\myapp{\mysub{\mytmt}{x}{\mytmn}}{\mysub{\mytmm}{x}{\mytmn}}) \\ + \mysub{(\myabs{x}{\mytmm})}{x}{\mytmn} & = & \myabs{x}{\mytmm} \\ + \mysub{(\myabs{y}{\mytmm})}{x}{\mytmn} & = & \myabs{z}{\mysub{\mysub{\mytmm}{y}{z}}{x}{\mytmn}}, \\ + \multicolumn{3}{l}{\myind{1} \text{with $x \neq y$ and $z$ not free in $\myapp{\mytmm}{\mytmn}$}} + \end{array} + \end{array} + $ +} + +The care required during substituting variables for terms is required to avoid +name capturing. + +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): +\[ + (\myapp{\omega}{\omega}) \myred (\myapp{\omega}{\omega}) \myred \dots\text{, with $\omega = \myabs{x}{\myapp{x}{x}}$} +\] + +A \emph{redex} is a term that can be reduced. In the untyped $\lambda$-calculus +this will be the case for an application in which the first term is an +abstraction, but in general a term is reducible if it appears to the left of a +reduction rule. When a term contains no redex it's said to be in \emph{normal + form}. Given the observation above, not all terms reduce to a normal forms: +we call the ones that do \emph{normalising}, and the ones that don't +\emph{non-normalising}. + +The reduction rule presented is not syntax directed, but \emph{evaluation + strategies} can be employed to reduce term systematically. Common evaluation +strategies include \emph{call by value} (or \emph{strict}), where arguments of +abstractions are reduced before being applied to the abstraction; and conversely +\emph{call by name} (or \emph{lazy}), where we reduce only when we need to do so +to proceed---in other words when we have an application where the function is +still not a $\lambda$. In both these reduction strategies we never reduce under +an abstraction: for this reason a weaker form of normalisation is used, where +both abstractions and normal forms are said to be in \emph{weak head normal + form}. + +\subsection{The simply typed $\lambda$-calculus} + +A convenient 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 \citep{Curry1934}. The first most basic instance of this idea +takes the name of \emph{simply typed $\lambda$ calculus}. + +Our types contain a set of \emph{type variables} $\Phi$, which might correspond +to some `primitive' types; and $\myarr$, the type former for `arrow' types, the +types of functions. The language is explicitly typed: when we bring a variable +into scope with an abstraction, we explicitly declare its type. $\mytya$, +$\mytyb$ will be used to refer to a generic type. Reduction is unchanged from +the untyped $\lambda$-calculus. + +\mydesc{syntax}{ }{ + $ + \begin{array}{r@{\ }c@{\ }l} + \mytmsyn & ::= & \myb{x} \mysynsep \myabss{\myb{x}}{\mytysyn}{\mytmsyn} \mysynsep + (\myapp{\mytmsyn}{\mytmsyn}) \\ + \mytysyn & ::= & \myb{\phi} \mysynsep \mytysyn \myarr \mytysyn \mysynsep \\ + \myb{x} & \in & \text{Some enumerable set of symbols} \\ + \myb{\phi} & \in & \Phi + \end{array} + $ +} + +\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{ + \centering{ + \begin{tabular}{ccc} + \AxiomC{$\myctx(x) = A$} + \UnaryInfC{$\myjud{\myb{x}}{A}$} + \DisplayProof + & + \AxiomC{$\myjudd{\myctx;\myb{x} : A}{\mytmt}{\mytyb}$} + \UnaryInfC{$\myjud{\myabss{x}{A}{\mytmt}}{\mytyb}$} + \DisplayProof + & + \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$} + \AxiomC{$\myjud{\mytmn}{\mytya}$} + \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$} + \DisplayProof + \end{tabular} + } +} + +In the typing rules, a context $\myctx$ is used to store the types of bound +variables: $\myctx; \myb{x} : \mytya$ adds a variable to the context and +$\myctx(x)$ returns the type of the rightmost occurrence of $x$. + +This typing system takes the name of `simply typed lambda calculus' (STLC), and +enjoys a number of properties. Two of them are expected in most type systems +\citep{Pierce2002}: +\begin{description} +\item[Progress] A well-typed term is not stuck---it is either a variable, or its + constructor does not appear on the left of the $\myred$ relation (currently + only $\lambda$), 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, and preserves the previous type. +\end{description} + +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*} + \myapp{(\myabss{x}{\myhole{?}}{\myapp{x}{x}})}{(\myabss{x}{\myhole{?}}{\myapp{x}{x}})} +\end{equation*} + +This makes the STLC Turing incomplete. We can recover the ability to loop by +adding a combinator that recurses: + +% TODO make this more compact + +\mydesc{syntax}{ } { + $ \mytmsyn ::= \dotsb \mysynsep \myfix{x}{\mytysyn}{\mytmsyn} $ +} + +\mydesc{typing:}{ } { + \AxiomC{$\myjudd{\myctx; x : \mytya}{\mytmt}{\mytya}$} + \UnaryInfC{$\myjud{\myfix{x}{\mytya}{\mytmt}}{\mytya}$} + \DisplayProof +} + +\mydesc{reduction:}{ }{ + $ \myfix{x}{\mytya}{\mytmt} \myred \mysub{\mytmt}{x}{(\myfix{x}{\mytya}{\mytmt})}$ +} + +This will deprive us of normalisation, which is a particularly bad thing if we +want to use the STLC as described in the next section. + +\subsection{The Curry-Howard correspondence} + +Moreover, +we have a product (or pair, or tuple) type $\mytya \myprod \mytyb$ for each pair +of types $\mytya$ and $\mytyb$, and a function (or arrow) type $\mytya \myarr +\mytyb$ for each pair of types $\mytya$ and $\mytyb$. $\beta$-reduction is +unchanged, but we have added reduction rules for products. Products are not +essential, but they serve as a good example of a type former apart from the +arrow type. + +\mydesc{syntax}{ }{ + $ + \begin{array}{r@{\ }c@{\ }l} + \mytmsyn & ::= & \myb{x} \mysynsep \myconst \mysynsep + \myabss{\myb{x}}{\mytysyn}{\mytmsyn} \mysynsep + (\myapp{\mytmsyn}{\mytmsyn}) \\ + & | & \mytt \mysynsep \mypair{\mytmsyn}{\mytmsyn} \mysynsep + \myfst{\mytmsyn} \mysynsep \mysnd{\mytmsyn} \\ + \mytysyn & ::= & \mytysyn \myprod \mytysyn \mysynsep + \mytysyn \myarr \mytysyn \mysynsep + \mybasety{\myconst} \\ + \myb{x} & \in & \text{Some enumerable set of symbols} \\ + \myconst & \in & \text{Some set $C$ of constants} \\ + \end{array} + $ +} + +\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{ + \centering{ + \begin{tabular}{cc} + $\myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{x}{\mytmn}$ & + $ + \begin{array}{r@{\ }c@{\ }l} + \myapp{\myfst}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\ + \myapp{\mysnd}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn + \end{array} + $ + \end{tabular} + } +} + +% TODO write context rules +% \mydesc{validity:}{\myvalid{\myctx}}{ +% \centering{ +% \begin{tabular}{ccc} +% \AxiomC{} +% \UnaryInfC{$\myvalid{\myemptyctx}$} +% \DisplayProof +% & +% \AxiomC{$\mytmt : \mytya$} +% \UnaryInfC{$\myvalid{\myctx; x : \mytya +% bar & +% baz +% \end{tabular} +% } +% } + +\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{ + \centering{ + \begin{tabular}{cc} + \AxiomC{$x : A \in \myctx$} + \UnaryInfC{$\myjud{x}{A}$} + \DisplayProof + & + foo + \end{tabular} + } +} + +\section{Intuitionistic Type Theory} \label{sec:itt} \section{The struggle for equality} \label{sec:equality} -\section{A more useful language} +\section{Extending ITT} \label{sec:practical} -\section{Kant} +\section{\mykant} \label{sec:kant} \appendix \section{Notation and syntax} +Syntax, derivation rules, and reduction rules, are enclosed in frames describing +the type of relation being established and the syntactic elements appearing, +for example + +\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{ + Typing derivations here. +} + In the languages presented I will also use different fonts and colors for different things: \begin{center} \begin{tabular}{c | l} $\mytyc{Sans}$ & Type constructors. \\ - $\myind{sans}$ & Data constructors. \\ + $\mydc{sans}$ & Data constructors. \\ % $\myfld{sans}$ & Field accessors (e.g. \myfld{fst} and \myfld{snd} for products). \\ $\mysyn{roman}$ & Syntax of the language. \\ $\myfun{roman}$ & Defined values. \\ |