\documentclass[report]{article}
%% Narrow margins
-\usepackage{fullpage}
+% \usepackage{fullpage}
%% Bibtex
\usepackage{natbib}
%% Links
\usepackage{hyperref}
+%% Frames
+\usepackage{framed}
+
+%% Symbols
+\usepackage[fleqn]{amsmath}
+
+%% Proof trees
+\usepackage{bussproofs}
+
%% -----------------------------------------------------------------------------
%% Commands for Agda
\usepackage[english]{babel}
\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}
\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. \\
projects / bitonic-mengthesis.git / commitdiff