diff options
Diffstat (limited to 'sec/systemt.ltx')
| -rw-r--r-- | sec/systemt.ltx | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/sec/systemt.ltx b/sec/systemt.ltx index 63cd7a7..b534040 100644 --- a/sec/systemt.ltx +++ b/sec/systemt.ltx @@ -4,13 +4,15 @@ \section{System T}% \label{sec:systemt} -System~T is a simply-typed lambda calculus. The types are naturals +System~T is a simply-typed lambda calculus. Its types are naturals \nat{} and functions \(A \to B\). On top of the function abstraction and application operators, we have \zero{} and \suc{} for zero and successor, as well as \primreckw{}, the primitive recursor. \Cref{fig:syst-typing} shows the typing judgements, where \(\judgement{\Gamma}[T]{t}{A}\) means that \(t\) is System~T term of type -\(A\) in context \(\Gamma\), and \cref{fig:syst-eq} the equational theory. +\(A\) in context \(\Gamma\). \Cref{fig:syst-eq} gives the equational +theory. We have beta- and eta-equality of functions and beta-reduction +of natural numbers. \begin{figure} \[ @@ -54,6 +56,7 @@ recursor. \Cref{fig:syst-typing} shows the typing judgements, where \begin{figure} \begin{align*} (\lambda x. t)~u &= \sub{t}{x/u} \\ + \lambda x. t~x &= t \qquad (x \notin t)\\ \primrec{\zero}{u}{(x.v)} &= u \\ \primrec{(\suc~t)}{u}{(x.v)} &= \sub{v}{x/\primrec{t}{u}{(x.v)}} \end{align*} |