--- /dev/null
+
+@inbook{Thompson1991,
+ author = {Thompson, Simon},
+ title = {Type Theory and Functional Programming},
+ publisher = {Addison-Wesley},
+ year = {1991}
+}
+
+@inbook{Pierce2002,
+ author = {Pierce, Benjamin C.},
+ title = {Types and Programming Languages},
+ publisher = {The MIT Press},
+ year = {2002}
+}
+
+
+@article{Altenkirch2010,
+author = {Altenkirch, Thorsten and Danielsson, N and L\"{o}h, A and Oury, Nicolas},
+file = {:home/bitonic/docs/papers/PiSigma.pdf:pdf},
+journal = {Functional and Logic \ldots},
+number = {Sheard 2005},
+title = {{$\Pi$$\Sigma$: dependent types without the sugar}},
+url = {http://www.springerlink.com/index/91W712G2806R575H.pdf},
+year = {2010}
+}
+@article{Altenkirch2007,
+address = {New York, New York, USA},
+author = {Altenkirch, Thorsten and McBride, Conor and Swierstra, Wouter},
+doi = {10.1145/1292597.1292608},
+file = {:home/bitonic/docs/papers/OTT2.pdf:pdf},
+isbn = {9781595936776},
+journal = {Proceedings of the 2007 workshop on Programming languages meets program verification - PLPV '07},
+keywords = {case analysis relies on,datatypes are indexed in,equality,of any language where,ole in the programs,play a crucial internal,rˆ,solving,some way,type theory},
+pages = {57},
+publisher = {ACM Press},
+title = {{Observational equality, now!}},
+url = {http://portal.acm.org/citation.cfm?doid=1292597.1292608},
+year = {2007}
+}
+@article{Barendregt1991,
+author = {Barendregt, Henk},
+file = {:home/bitonic/docs/papers/lambda-cube.pdf:pdf},
+journal = {Journal of functional programming},
+title = {{Introduction to generalized type systems}},
+url = {http://www.diku.dk/hjemmesider/ansatte/henglein/papers/barendregt1991.pdf},
+year = {1991}
+}
+@article{Brady2012,
+author = {Brady, Edwin},
+file = {:home/bitonic/docs/papers/idris-implementation.pdf:pdf},
+journal = {Unpublished draft},
+number = {November},
+title = {{Implementing General Purpose Dependently Typed Programming Languages}},
+url = {http://www.cs.st-andrews.ac.uk/~eb/drafts/impldtp.pdf},
+year = {2012}
+}
+@article{Chapman2010,
+address = {New York, New York, USA},
+author = {Chapman, James and Dagand, Pierre-\'{E}variste and McBride, Conor and Morris, Peter},
+doi = {10.1145/1863543.1863547},
+file = {:home/bitonic/docs/papers/conor-levitation.pdf:pdf},
+isbn = {9781605587943},
+journal = {Proceedings of the 15th ACM SIGPLAN international conference on Functional programming - ICFP '10},
+pages = {3},
+publisher = {ACM Press},
+title = {{The gentle art of levitation}},
+url = {http://portal.acm.org/citation.cfm?doid=1863543.1863547},
+year = {2010}
+}
+@article{Church1936,
+author = {Church, Alonzo},
+file = {:home/bitonic/docs/papers/church-lc.pdf:pdf},
+journal = {American journal of mathematics},
+number = {2},
+pages = {345--363},
+title = {{An unsolvable problem of elementary number theory}},
+url = {http://www.ams.org/leavingmsn?url=http://dx.doi.org/10.2307/2371045},
+volume = {58},
+year = {1936}
+}
+@article{Church1940,
+author = {Church, Alonzo},
+file = {:home/bitonic/docs/papers/church-stlc.pdf:pdf},
+journal = {J. Symb. Log.},
+number = {2},
+pages = {56--68},
+title = {{A formulation of the simple theory of types}},
+url = {http://www.ams.org/leavingmsn?url=http://dx.doi.org/10.2307/2266170},
+volume = {5},
+year = {1940}
+}
+@article{Coquand1986,
+author = {Coquand, Thierry and Huet, Gerard},
+file = {:home/bitonic/docs/papers/coc.pdf:pdf},
+title = {{The calculus of constructions}},
+url = {http://hal.inria.fr/docs/00/07/60/24/PDF/RR-0530.pdf},
+year = {1986}
+}
+@article{Curry1934,
+author = {Curry, Haskell B.},
+file = {:home/bitonic/docs/papers/curry-stlc.pdf:pdf},
+journal = {Proceedings of the National Academy of Sciences of \ldots},
+number = {1930},
+pages = {584--590},
+title = {{Functionality in combinatory logic}},
+url = {http://www.ncbi.nlm.nih.gov/pmc/articles/pmc1076489/},
+volume = {511},
+year = {1934}
+}
+@article{Hurkens1995,
+author = {Hurkens, Antonius J.C.},
+file = {:home/bitonic/docs/papers/hurkens-paradox.pdf:pdf},
+journal = {Typed Lambda Calculi and Applications},
+title = {{A simplification of Girard's paradox}},
+url = {http://www.springerlink.com/index/W718604JN467672H.pdf},
+year = {1995}
+}
+@book{Martin-Lof1984,
+author = {Martin-L\"{o}f, Per},
+file = {:home/bitonic/docs/papers/martin-lof-tt.pdf:pdf},
+isbn = {8870881059},
+publisher = {Bibliopolis},
+title = {{Intuitionistic type theory}},
+year = {1984}
+}
+@article{McBride2004,
+author = {McBride, Conor},
+doi = {10.1017/S0956796803004829},
+file = {:home/bitonic/docs/papers/view-from-the-left.ps.gz:gz},
+journal = {Journal of Functional Programming},
+month = jan,
+number = {1},
+pages = {69--111},
+title = {{The View from The Left}},
+url = {http://strictlypositive.org/view.ps.gz},
+volume = {14},
+year = {2004}
+}
+@phdthesis{Norell2007,
+author = {Norell, Ulf},
+file = {:home/bitonic/docs/papers/ulf-thesis.pdf:pdf},
+isbn = {9789172919969},
+school = {Chalmers University of Technology and G\"{o}teborg University},
+title = {{Towards a practical programming language based on dependent type theory}},
+url = {http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf},
+year = {2007}
+}
+@article{Oury2008,
+address = {New York, New York, USA},
+author = {Oury, Nicolas and Swierstra, Wouter},
+doi = {10.1145/1411204.1411213},
+file = {:home/bitonic/docs/papers/powerofpi.pdf:pdf},
+isbn = {9781595939197},
+journal = {Proceeding of the 13th ACM SIGPLAN international conference on Functional programming - ICFP '08},
+pages = {39},
+publisher = {ACM Press},
+title = {{The power of Pi}},
+url = {http://portal.acm.org/citation.cfm?doid=1411204.1411213},
+year = {2008}
+}
+@article{Pierce2000,
+author = {Pierce, Benjamin C. and Turner, David N.},
+doi = {10.1145/345099.345100},
+file = {:home/bitonic/docs/papers/local-type-inference.pdf:pdf},
+issn = {01640925},
+journal = {ACM Transactions on Programming Languages and Systems},
+month = jan,
+number = {1},
+pages = {1--44},
+title = {{Local type inference}},
+url = {http://portal.acm.org/citation.cfm?doid=345099.345100},
+volume = {22},
+year = {2000}
+}
+@article{Pollack1990,
+author = {Pollack, Robert},
+file = {:home/bitonic/docs/papers/implicit-syntax.ps:ps},
+journal = {Informal Proceedings of First Workshop on Logical Frameworks},
+title = {{Implicit syntax}},
+url = {http://reference.kfupm.edu.sa/content/i/m/implicit\_syntax\_\_1183660.pdf},
+year = {1992}
+}
+@article{Reynolds1994,
+author = {Reynolds, John C.},
+file = {:home/bitonic/docs/papers/reynolds-polymorphic-lc.ps:ps},
+journal = {Logical Foundations of Functional Programming},
+title = {{An introduction to the polymorphic lambda calculus}},
+url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.7.9916\&rep=rep1\&type=pdf},
+year = {1994}
+}
+@article{Sulzmann2007,
+address = {New York, New York, USA},
+author = {Sulzmann, Martin and Chakravarty, Manuel M. T. and Jones, Simon Peyton and Donnelly, Kevin},
+doi = {10.1145/1190315.1190324},
+file = {:home/bitonic/docs/papers/systemf-coercions.pdf:pdf},
+isbn = {159593393X},
+journal = {Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation - TLDI '07},
+pages = {53},
+publisher = {ACM Press},
+title = {{System F with type equality coercions}},
+url = {http://portal.acm.org/citation.cfm?doid=1190315.1190324},
+year = {2007}
+}
+@article{Vytiniotis2011,
+author = {Vytiniotis, Dimitrios and Jones, Simon Peyton and Schrijvers, Tom and Sulzmann, Martin},
+file = {:home/bitonic/docs/papers/outsidein.pdf:pdf},
+journal = {Journal of Functional Programming},
+number = {4-5},
+pages = {333--412},
+title = {{OutsideIn (X) Modular type inference with local assumptions}},
+url = {http://journals.cambridge.org/production/action/cjoGetFulltext?fulltextid=8274818},
+volume = {21},
+year = {2011}
+}
+@article{Yorgey2012,
+address = {New York, New York, USA},
+author = {Yorgey, Brent a. and Weirich, Stephanie and Cretin, Julien and {Peyton Jones}, Simon and Vytiniotis, Dimitrios and Magalh\~{a}es, Jos\'{e} Pedro},
+doi = {10.1145/2103786.2103795},
+file = {:home/bitonic/docs/papers/haskell-promotion.pdf:pdf},
+isbn = {9781450311205},
+journal = {Proceedings of the 8th ACM SIGPLAN workshop on Types in language design and implementation - TLDI '12},
+pages = {53},
+publisher = {ACM Press},
+title = {{Giving Haskell a promotion}},
+url = {http://dl.acm.org/citation.cfm?doid=2103786.2103795},
+year = {2012}
+}
\usepackage[export]{adjustbox}
\usepackage{multicol}
+%% -----------------------------------------------------------------------------
+%% Bibtex
+\usepackage{natbib}
+
%% Numbering depth
%% \setcounter{secnumdepth}{0}
}
% Make links footnotes instead of hotlinks:
-\renewcommand{\href}[2]{#2\footnote{\url{#1}}}
+% \renewcommand{\href}[2]{#2\footnote{\url{#1}}}
% avoid problems with \sout in headers with hyperref:
\pdfstringdefDisableCommands{\renewcommand{\sout}{}}
\title{The Paths Towards Observational Equality}
-\author{Francesco Mazzoli \url{<fm2209@ic.ac.uk>}}
+\author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}
\date{December 2012}
\begin{document}
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.
+its inventor. The exposition is quite dense since there is a lot of material to
+cover, for a more complete treatment of the material the reader can refer to
+\citep{Thompson1991, Pierce2002}.
-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.
+I will then explain why equality has been a tricky business in these theories,
+and talk about the various attempts have been made to make the situation better.
+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
-computation with a minimal sintax and most notably no ``data'' in the
-traditional sense, but just functions.
+lead to the $\lambda$-calculus \citep{Church1936}. This early programming
+language encodes computation with a minimal sintax and most notably no ``data''
+in the traditional sense, but just functions.
The syntax of $\lambda$-terms consists of just three things: variables,
abstractions, and applications:
\newcommand{\tyc}{C}
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.
+then check that the terms that we are forming make sense given our typing rules
+\citep{Curry1934}.
We wish to introduce rules of the form $\Gamma \vdash \termt : \tya$, which
reads ``in context $\Gamma$, term $\termt$ has type $\tya$''.
\newcommand{\lcunit}{\mathsf{()}}
-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 correspondence, or isomorphism.
+It turns out that the STLC can be seen a natural deduction system for
+propositional logic. Terms are proofs, and their types are the propositions
+they prove. This remarkable fact is known as the Curry-Howard correspondence,
+or isomorphism.
The ``arrow'' ($\to$) type corresponds to implication. If we wished to
prove that $(\tya \tyarr \tyb) \tyarr (\tyb \tyarr \tyc) \tyarr (\tya
\section{Intuitionistic Type Theory}
-Intuitionistic Type Theory (ITT) is a very expressive system first described by
-Per Martin-L\"{o}f at the end of the 70s. It extends the STLC giving it all the
-properties described above, while retaining good computational properties. Here
-we will present a core type theory and illustrate its components and properties
-one by one, and then describe the various additions that make it useful as a
-programming language and as a theorem prover.
-
\newcommand{\lcset}[1]{\mathsf{Type}_{#1}}
\newcommand{\lcsetz}{\mathsf{Type}}
\newcommand{\defeq}{\equiv}
+\subsection{A Bit of History}
+
+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}.
+
+A related development is the one of the polymorphic $\lambda$-calculus, and
+specifically the previously mentioned System F, which was invented independently
+by Girard and Reynolds. An can be found in \citep{Reynolds1994}. The
+surprising fact is that while System F is impredicative it is still consistent
+and strongly normalising. Coquand and Huet further extended this line of work
+with the Calculus of Constructions (CoC) \citep{Coquand1986}.
+
+\subsection{A Core Type Theory}
+\label{sec:core-tt}
+
+The calculus I present follows the exposition in \citep{Thompson1991}, and as
+said previously is quite close to the original formulation of predicative ITT as
+found in \citep{Martin-Lof1984}.
+
\begin{center}
\axname{syntax}
\begin{eqnarray*}
the separation between types and terms is gone. All we have is terms, that
include both values (terms of type $\lcset{0}$) and types (terms of type
$\lcset{n}$, with $n > 0$). This change is reflected in the typing rules.
-While in the STLC terms and types are kept well separated (terms never go
-``right of the colon''), in ITT types can freely depend on terms.
+While in the STLC values and types are kept well separated (values never go
+``right of the colon''), in ITT types can freely depend on values.
This relation is expressed in the typing rules for $\forall$ and $\exists$: if a
function has type $\lcforall{x}{\tya}{\tyb}$, $\tyb$ can depend on $x$.
$\forall$ and $\exists$ are at the core of the machinery of ITT:
\begin{description}
-\item[$\forall$] is a generalisation of $\tyarr$ in the STLC and expresses
- universal quantification in our logic. In the literature this is also known
- as ``dependent product'' and shown as $\Pi$, following an interpretation of
- functions as infinitary products. We will just call it ``dependent function'',
- reserving ``product'' for $\exists$.
-
-\item[$\exists$] is a generalisation of $\wedge$ in the extended STLC of section
- \ref{sec:curry-howard}, and thus we will call it ``dependent product''. In
- our logic, it represents existential quantification.
-
- For added confusion, in the literature that calls $\forall$ $\Pi$ $\exists$ is
- often named ``dependent sum'' and shown as $\Sigma$. This is following the
- interpretation of $\exists$ as a generalised $\vee$, where the first element
- of the pair is the ``tag'' that decides which type the second element will
- have.
+\item[``forall'' ($\forall$)] is a generalisation of $\tyarr$ in the STLC and
+ expresses universal quantification in our logic. In the literature this is
+ also known as ``dependent product'' and shown as $\Pi$, following the
+ interpretation of functions as infinitary products. We will just call it
+ ``dependent function'', reserving ``product'' for $\exists$.
+
+\item[``exists'' ($\exists$)] is a generalisation of $\wedge$ in the extended
+ STLC of section \ref{sec:curry-howard}, and thus we will call it ``dependent
+ product''. Like $\wedge$, it is formed by providing a pair of things. In our
+ logic, it represents existential quantification.
+
+ For added confusion, in the literature that calls $\forall$ $\Pi$, $\exists$
+ 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 decides which type the second
+ element will have.
\end{description}
Another thing to notice is that types are very ``first class'': we are free to
create functions that accept and return types. For this reason we $\defeq$ as
-the smallest
-
-\begin{thebibliography}{9}
-
-\bibitem{levitation}
- James Chapman, Pierre-Evariste Dagand, Conor McBride, and Peter Morris.
- \emph{The gentle art of levitation}.
- SIGPLAN Not., 45:3–14, September 2010.
-
-\bibitem{outsidein}
- Dimitrios Vytiniotis, Simon Peyton Jones, Tom Schrijvers, and Martin
- Sulzmann.
- \emph{OutsideIn(X): Modular Type inference with local assumptions}.
- Journal of Functional Programming, 21, 2011.
-
-\bibitem{haskell-promotion}
- Brent A. Yorgey, Stephanie Weirich, Julien Cretin, Simon Peyton Jones,
- Dimitrios Vytiniotis, and Jos\'{e} Pedro Magalh\~{a}es.
- \emph{Giving Haskell a promotion}.
- In Proceedings of the 8th ACM SIGPLAN Workshop on Types in Language Design and
- Implementation, TLDI ’12, pages 53–66, New York, NY, USA, 2012. ACM. doi:
- 10.1145/2103786.2103795.
-
-\bibitem{idris}
- Edwin Brady.
- \emph{Implementing General Purpose Dependently Typed Programming Languages}.
- Unpublished draft.
-
-\bibitem{bidirectional}
- Benjamin C. Pierce and David N. Turner.
- \emph{Local type inference}.
- ACM Transactions on Programming Languages and Systems, 22(1):1–44, January
- 2000. ISSN 0164-0925. doi: 10.1145/345099.345100.
-
-\end{thebibliography}
+the smallest equivalence relation extending $\bredc$, where $\bredc$ is the
+reflexive transitive closure of $\bred$; and we treat types that are equal
+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 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 $\bred$ is confluent (if
+$\termt \bredc \termm$ and $\termt \bredc \termn$, then $\termm \bredc \termp$
+and $\termn \bredc \termp$). This measure makes sure that, for instance,
+$\app{(\abs{x : \lctype}{x})}{\lcbool} \defeq \lcbool$. The theme of equality
+is central and will be analysed better later.
+
+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. The layers of the hierarchy are called
+``universes''. $\lcsetz : \lcsetz$ ITT is inconsistent due to Girard's paradox
+\citep{Hurkens1995}, and thus loses its 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 - we will see instances of the last
+motivation later. Moreover, universes can be inferred mechanically
+\citep{Pollack1990}. It is also convenient to have a \emph{cumulative} theory,
+where $\lcset{n} : \lcset{m}$ iff $n < m$. We eschew these measures to keep the
+presentation simple.
+
+Lastly, the theory I present is fully explicit in the sense that the user has to
+specify every type when forming abstractions, products, etc. This can be a
+great burden if one wants to use the theory directly. Complete inference is
+undecidable (which is hardly surprising considering the role that types play)
+but partial inference (also called ``bidirectional type checking'' in this
+context) in the style of \citep{Pierce2000} will have to be deployed in a
+practical system. When showing examples obvious types will be omitted.
+
+Note that the Curry-Howard correspondence runs through ITT as it did with the
+STLC with the difference that ITT corresponds to an higher order propositional
+logic.
+
+\subsection{Base Types}
+
+While the ITT presented is a fairly complete logic, it is not that useful for
+programming. If we wish to make it better, we can add some base types to
+represent the data structures we know and love, such as numbers, lists, and
+trees.
+
+\newcommand{\lctrue}{\mathsf{true}}
+\newcommand{\lcfalse}{\mathsf{false}}
+
+\begin{center}
+ \axname{syntax}
+ \begin{eqnarray*}
+ \termsyn & ::= & ... \\
+ & | & \lcbool \separ \lctrue \separ \lcfalse
+ \end{eqnarray*}
+
+ \axdesc{typing}{\Gamma \vdash \termsyn : \termsyn}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c c c}
+ \AxiomC{}
+ \RightLabel{var}
+ \UnaryInfC{$\Gamma;x : \tya \vdash x : \tya$}
+ \DisplayProof
+ &
+ \AxiomC{$\Gamma \vdash \termt : \bot$}
+ \RightLabel{$\bot E$}
+ \UnaryInfC{$\Gamma \vdash \lcabsurd \termt : A$}
+ \DisplayProof
+ &
+ \AxiomC{$\Gamma \vdash \termt : \tya$}
+ \AxiomC{$\tya \defeq \tyb$}
+ \RightLabel{$\defeq$ type}
+ \BinaryInfC{$\Gamma \vdash \termt : \tyb$}
+ \DisplayProof
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c c}
+ \AxiomC{$\Gamma;x : \tya \vdash \termt : \tya$}
+ \RightLabel{$\forall I$}
+ \UnaryInfC{$\Gamma \vdash \abs{x : \tya}{\termt} : \lcforall{x}{\tya}{\tyb}$}
+ \DisplayProof
+ &
+ \AxiomC{$\Gamma \vdash \termt : \lcforall{x}{\tya}{\tyb}$}
+ \AxiomC{$\Gamma \vdash \termm : \tya$}
+ \RightLabel{$\forall E$}
+ \BinaryInfC{$\Gamma \vdash \app{\termt}{\termm} : \tyb[\termm / x]$}
+ \DisplayProof
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c c}
+ \AxiomC{$\Gamma \vdash \termt : \tya$}
+ \AxiomC{$\Gamma \vdash \termm : \tyb[\termt / x]$}
+ \RightLabel{$\exists I$}
+ \BinaryInfC{$\Gamma \vdash (\termt, \termm) : \lcexists{x}{\tya}{\tyb}$}
+ \DisplayProof
+ &
+ \AxiomC{$\Gamma \vdash \termt: \lcexists{x}{\tya}{\tyb}$}
+ \RightLabel{$\exists E_{1,2}$}
+ \UnaryInfC{$\hspace{0.7cm} \Gamma \vdash \lcfst \termt : \tya \hspace{0.7cm}$}
+ \noLine
+ \UnaryInfC{$\Gamma \vdash \lcsnd \termt : \tyb[\lcfst \termt / x]$}
+ \DisplayProof
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c c}
+ \AxiomC{}
+ \RightLabel{type}
+ \UnaryInfC{$\Gamma \vdash \lcset{n} : \lcset{n + 1}$}
+ \DisplayProof
+ &
+ \AxiomC{$\Gamma \vdash \tya : \lcset{n}$}
+ \AxiomC{$\Gamma; x : \tya \vdash \tyb : \lcset{m}$}
+ \RightLabel{$\forall, \exists$ type}
+ \BinaryInfC{$\Gamma \vdash \lcforall{x}{\tya}{\tyb} : \lcset{n \sqcup m}$}
+ \noLine
+ \UnaryInfC{$\Gamma \vdash \lcexists{x}{\tya}{\tyb} : \lcset{n \sqcup m}$}
+ \DisplayProof
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \axdesc{reduction}{\termsyn \bred \termsyn}
+ \begin{eqnarray*}
+ \app{(\abs{x}{\termt})}{\termm} & \bred & \termt[\termm / x] \\
+ \lcfst (\termt, \termm) & \bred & \termt \\
+ \lcsnd (\termt, \termm) & \bred & \termm
+ \end{eqnarray*}
+\end{center}
+
+
+\bibliographystyle{authordate1}
+\bibliography{background}
\end{document}
projects / bitonic-mengthesis.git / commitdiff