diff options
Diffstat (limited to 'InterimReport.tex')
| -rw-r--r-- | InterimReport.tex | 93 |
1 files changed, 58 insertions, 35 deletions
diff --git a/InterimReport.tex b/InterimReport.tex index 752288c..1c89260 100644 --- a/InterimReport.tex +++ b/InterimReport.tex @@ -36,6 +36,7 @@ \usepackage{turnstile} \usepackage{centernot} \usepackage{stmaryrd} +\usepackage{bm} %% ----------------------------------------------------------------------------- %% Utils @@ -170,7 +171,7 @@ In the languages presented I will also use different fonts for different things: Moreover, I will from time to time give examples in the Haskell programming language as defined in \citep{Haskell2010}, which I will typeset in -\texttt{typewriter} font. I assume that the reader is already familiar with +\texttt{teletype} font. I assume that the reader is already familiar with Haskell, plenty of good introductions are available \citep{LYAH,ProgInHask}. \subsection{Untyped $\lambda$-calculus} @@ -224,8 +225,21 @@ complete. As a corollary, we must be able to devise a term that reduces forever \app{(\abs{x}{\app{x}{x}})}{(\abs{x}{\app{x}{x}})} \bred \app{(\abs{x}{\app{x}{x}})}{(\abs{x}{\app{x}{x}})} \bred \dotsb \] Terms that can be reduced only a finite number of times (the non-looping ones) -are said to be \emph{normalising}, and the `final' term (where no reductions are -possible on the term or on its subterms) is called \emph{normal form}. +are said to be \emph{strongly normalising}, and the `final' term (where no +reductions are possible on the term or on its subterms) is called \emph{normal + form}. + +From now on I will omit the `strongly' in `strongly normalising', however weaker +notions of normalisation have been described. More generally, it is often +convenient not to reduce subterms indiscriminately, and have a more principled +approach to evaluation, or `evaluation strategy'. Common evaluation strategies +include `call by value' (or `strict'), where arguments of abstractions are +reduced before being applied to the abstraction; and conversely `call by name' +(or `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, and a +different notion of normalisation (`weak head normal form') if often used, where +every abstraction is a weak head normal form. \subsection{The simply typed $\lambda$-calculus} \label{sec:stlc} @@ -245,21 +259,27 @@ The syntax for types is as follows: \begin{center} \axname{syntax} - $$\tysyn ::= x \separ \tysyn \tyarr \tysyn$$ +$$ +\begin{array}{rcl} + \tysyn & ::= & \alpha \separ \tysyn \tyarr \tysyn \\ + \alpha & \in & \text{A set of base types provided by the language} +\end{array} +$$ \end{center} -I will use $\tya,\tyb,\dots$ to indicate a generic type. +I will use $\tya,\tyb,\dots$ to indicate a generic type, carrying the convention +from set theory of denoting member of sets with lowercase letters and sets +themselves with capitals. A context $\Gamma$ is a map from variables to types. I will use the notation $\Gamma; x : \tya$ to augment it and to `extract' pairs from it. 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.}: +$\tyb$. We extend the syntax and allow to decorate our abstractions with +types: \begin{center} \axname{syntax} - $$\termsyn ::= x \separ (\abs{x : \tysyn}{\termsyn}) \separ (\app{\termsyn}{\termsyn})$$ + $$\termsyn ::= x \separ (\abs{x{:}\tysyn}{\termsyn}) \separ (\app{\termsyn}{\termsyn})$$ \end{center} Now we are ready to give the typing judgements: @@ -273,7 +293,7 @@ Now we are ready to give the typing judgements: \DisplayProof & \AxiomC{$\Gamma; x : \tya \vdash \termt : \tyb$} - \UnaryInfC{$\Gamma \vdash \abs{x : \tya}{\termt} : \tya \tyarr \tyb$} + \UnaryInfC{$\Gamma \vdash \abs{x{:}\tya}{\termt} : \tya \tyarr \tyb$} \DisplayProof \end{tabular} @@ -344,10 +364,11 @@ That is, function composition. We might want extend our bare lambda calculus with a couple of terms former to make our natural deduction more pleasant to use. For example, tagged unions (\texttt{Either} in Haskell) are disjunctions, and tuples (or products) are conjunctions. We also want to be able to express -falsity ($\bot$): that can done by introducing a type inhabited by no terms. If -evidence of such a type is presented, then we can derive any type, which -expresses absurdity. Conversely, truth ($\top$) is the type with just one -trivial element ($\lcunit$). +falsity ($\bot$): that can done by introducing a type inhabited by no closed +terms. If evidence of such a type is presented (necessarily under an +abstraction), then we can derive any type, which expresses absurdity. +Conversely, truth ($\top$) is the type with just one trivial element +($\lcunit$). \newcommand{\lcinl}{\lccon{inl}\appsp} \newcommand{\lcinr}{\lccon{inr}\appsp} @@ -364,7 +385,7 @@ trivial element ($\lcunit$). \newcommand{\lcabsurd}{\lcfun{absurd}\appsp} \newcommand{\lcabsurdd}[1]{\lcfun{absurd}_{#1}\appsp} - +% TODO make parens bold with \bm \begin{center} \axname{syntax} $$ @@ -507,10 +528,11 @@ above additions, and thus would sit where $\lambda{C}$ sits in the Logic frameworks and programming languages based on type theory have a long history. Per Martin-L\"{o}f described the first version of his theory in 1971, -but then revised it since the original version was too impredicative and thus -inconsistent\footnote{In the early version $\lcsetz : \lcsetz$, see section - \ref{sec:core-tt} for an explanation on why this causes problems.}. For this -reason he gave a revised and consistent definition later \citep{Martin-Lof1984}. +but then revised it since the original version was inconsistent due to its +impredicativity\footnote{In the early version there was only one universe + $\lcsetz$ and $\lcsetz : \lcsetz$, see section \ref{sec:core-tt} for an + explanation on why this causes problems.}. For this reason he gave a revised +and consistent definition later \citep{Martin-Lof1984}. A related development is the polymorphic $\lambda$-calculus, and specifically the previously mentioned System F, which was developed independently by Girard @@ -631,11 +653,12 @@ logic. $\tyarr$ and $\times$ are at the core of the machinery of ITT: \begin{description} \item[`forall' ($\tyarr$)] is a generalisation of $\tyarr$ in the STLC and - expresses universal quantification in our logic. It is often written with a - syntax closer to logic, e.g. $\forall x : \tya. \tyb$. In the - literature this is also known as `dependent product' and shown as $\Pi$, - following the interpretation of functions as infinitary products. I will just - call it `dependent function', reserving `product' for $\exists$. + expresses universal quantification in our logic, where $A \tyarr B$ can be + expressed as $(- : A) \tyarr B$. It is often written with a syntax closer to + logic, e.g. $\forall x : \tya. \tyb$. In the literature this is also known as + `dependent product' and shown as $\Pi$, following the interpretation of + functions as infinitary products. I will just call it `dependent function', + reserving `product' for $\exists$. \item[`exists' ($\times$)] is a generalisation of $\wedge$ in the extended STLC of section \ref{sec:curry-howard}, and thus I will call it `dependent @@ -643,8 +666,8 @@ logic. $\tyarr$ and $\times$ are at the core of the machinery of ITT: logic, it represents existential quantification. Similarly to $\tyarr$, it is often written as $\exists x : \tya. \tyb$. - For added confusion, in the literature that calls $\tyarr$ $\Pi$, $\times$ is - often named `dependent sum' and shown as $\Sigma$. This is following the + For added confusion, in the literature that uses $\Pi$ for $\tyarr$, $\times$ + is often named `dependent sum' and shown as $\Sigma$. This is following the interpretation of $\exists$ as a generalised, infinitary $\vee$, where the first element of the pair is the `tag' that determines which type the second element will have. @@ -655,12 +678,12 @@ create functions that accept and return types. For this reason we define $\defeq$ as the smallest equivalence relation extending $\bredc$, where $\bredc$ is the reflexive transitive closure of $\bred$; and we treat types that are related according to $\defeq$ as the same. Another way of seeing $\defeq$ is -this: when we want to compare two types for equality, we reduce them as far as +this: when we want to compare two terms for equality, we reduce them as far as possible and then check if they are equal\footnote{Note that when comparing - terms we do it up to $\alpha$-renaming. That is, we do not consider - relabelling of variables as a difference - for example $\abs{x : A}{x} \defeq - \abs{y : A}{y}$.}. This works since not only each term has a normal form (ITT -is strongly normalising), but the normal form is also unique; or in other words + terms we do it up to $\alpha$-renaming. That is, we do not consider renaming + of bound variables as a difference - for example $\abs{x : A}{x} \defeq \abs{y + : A}{y}$.}. This works since not only each term has a normal form (ITT is +strongly normalising), but the normal form is also unique; or in other words $\bred$ is confluent (if $\termt \bredc \termm$ and $\termt \bredc \termn$, then there is a $p$ such that $\termm \bredc \termp$ and $\termn \bredc \termp$). This measure makes sure that, for instance, $\app{(\abs{x : @@ -669,13 +692,13 @@ and will be analysed better in section \ref{sec:equality}. The theory presented is \emph{stratified}. We have a hierarchy of types $\lcset{0} : \lcset{1} : \lcset{2} : \dots$, so that there is no `type of all -types', and our theory is predicative. Type-formers like $\tyarr$ and $\times$ +types', and our theory is predicative. Constructors like $\tyarr$ and $\times$ take the least upper bound $\sqcup$ of the contained types. The layers of the hierarchy are called `universes'. Theories where $\lcsetz : \lcsetz$ are inconsistent due to Girard's paradox \citep{Hurkens1995}, and thus lose their -well-behavedness. Some impredicativity sometimes has its place, either because -the theory retain good properties (normalization, consistency, etc.) anyway, -like in System F and CoC; or because we are at a stage at which we do not care. +well-behavedness. Impredicativity sometimes has its place, either because the +theory retain good properties (normalization, consistency, etc.) anyway, like in +System F and CoC; or because we are at a stage at which we do not care. \subsection{Base Types} \label{sec:base-types} |