Before the big rewrite

1 files changed, 130 insertions, 0 deletions

diff --git a/sec/systemt.ltx b/sec/systemt.ltx
new file mode 100644
index 0000000..12b1ed2
--- /dev/null
+++ b/sec/systemt.ltx
@@ -0,0 +1,130 @@
+\documentclass[../main.tex]{subfiles}
+
+\begin{document}
+\section{System T}%
+\label{sec:systemt}
+
+G\"odel's System~T extends the simply-typed lambda calculus by adding natural
+numbers and the primitiver recursor. The type formers are \(\nat\) for natural
+numbers and arrows \(A \to B\) for functions.
+
+\Cref{fig:systemt-type} shows the typing rules for System~T terms. On top of the
+usual abstraction and application rules, we can construct unary natural numbers
+using the operators \(\zero\) and \(\suc\). Natural numbers are eliminated using
+the primitive recursor \primreckw. Given a base case, update function and target
+\(n\), the primitive recursor applies the update function to the target \(n\)
+times. We will abuse notation and treat the \(\suc\) and \primreckw operators as
+functions.
+
+\begin{figure}
+  \[
+  \begin{array}{ccc}
+    \begin{prooftree}
+      \hypo{
+        x : A \in \Gamma
+        \vphantom{\judgement[T]{}{}{}} %% Spooky formatting phantom
+      }
+      \infer1{\judgement[T]{\Gamma}{x}{A}}
+    \end{prooftree}
+    &
+    \begin{prooftree}
+      \hypo{\judgement[T]{\Gamma, x \colon A}{t}{B}}
+      \infer1{\judgement[T]{\Gamma}{\lambda x.~t}{A \to B}}
+    \end{prooftree}
+    &
+    \begin{prooftree}
+      \hypo{\judgement[T]{\Gamma}{f}{A \to B}}
+      \hypo{\judgement[T]{\Gamma}{t}{A}}
+      \infer2{\judgement[T]{\Gamma}{f~t}{B}}
+    \end{prooftree}
+    \\
+    \\
+    \begin{prooftree}
+      \hypo{\vphantom{\judgement[T]{}{}{}}} %% Spooky formatting phantom
+      \infer1{\judgement[T]{\Gamma}{\zero}{\nat}}
+    \end{prooftree}
+    &
+    \begin{prooftree}
+      \hypo{\judgement[T]{\Gamma}{t}{\nat}}
+      \infer1{\judgement[T]{\Gamma}{\suc~t}{\nat}}
+    \end{prooftree}
+    &
+    \begin{prooftree}
+      \hypo{\judgement[T]{\Gamma}{z}{A}}
+      \hypo{\judgement[T]{\Gamma}{s}{A \to A}}
+      \hypo{\judgement[T]{\Gamma}{t}{\nat}}
+      \infer3{\judgement[T]{\Gamma}{\primrec{z}{s}{t}}{A}}
+    \end{prooftree}
+  \end{array}
+  \]
+  \caption{Typing judgements for System~T}%
+  \label{fig:systemt-type}
+\end{figure}
+
+The equational theory is defined in \cref{fig:systemt-eq}. We have the standard
+\(\beta\)-reduction for functions. When we apply the primitve recursor to target
+zero, we get the base case. When the recursor is applied to target \(\suc~t\),
+we apply the update function to the result of applying \primreckw{} recursively.
+An alternative theory would instead apply the update function directly to the
+base case instead of to the overall result of the recursion.  Whilst this has
+little impact for System~T (and operationally corresponds to tail recursion) the
+alternative rule does not generalise to the more complex recursive types found
+in \lang{}.
+
+\begin{figure}
+  \begin{align*}
+    (\lambda x.~t)~u &= \sub{t}{x/u} &
+    \primrec{z}{s}{\zero} &= z &
+    \primrec{z}{s}{(\suc~t)} &= s~(\primrec{z}{x}{s}{t})
+  \end{align*}
+  \caption{Equational theory for System~T. \TODO{add eta for unions}}%
+  \label{fig:systemt-eq}
+\end{figure}
+
+The primitive recursor is named as such because it generalises the first-order
+primitive recursive functions. For example, we can define addition as
+\[
+k + n = \primrec{n}{\suc}{k}.
+\]
+Despite its name, the primitive recursor can compute more than the primitive
+recursive functions. By exploiting the higher-order nature of System~T, one can
+define the Ackermann-P\'eter function~\cite{semantic-domain} as
+\[
+\lambda k, m.~\primrec{\suc}{(\lambda f.~\primrec{(\lambda n.~n)}{(\lambda g, n.~f~(g~n))})}{k}~m.
+\]
+
+Any countable set can be encoded by natural numbers. For inductively defined
+sets, such as lists or abstract syntax trees for programs, one can use a G\"odel
+encoding to represent values as natural numbers. This depends on a pairing
+function \(\pairingkw : \nat \to \nat \to \nat\) that is a (curried)
+bijection \(\nat \times \nat \to
+\nat\)~\cites{DiscoverEd:book/oc/Cantor52}{szudzik}. As some examples, we can
+encode lists of natural numbers as
+\begin{align*}
+  \encode{\epsilon} &\coloneq \pairing{0}{0} &
+  \encode{n, l} &\coloneq \pairing{1}{(\pairing{n}{\encode{l}})} \\
+  \shortintertext{and System~T terms (using deBruijn indices) as}
+  \encode{x_i}               &\coloneq \pairing{0}{i} &
+  \encode{\zero}             &\coloneq \pairing{3}{0} \\
+  \encode{\lambda~t}         &\coloneq \pairing{1}{\encode{t}} &
+  \encode{\suc~t}            &\coloneq \pairing{4}{\encode{t}} \\
+  \encode{t~u}               &\coloneq \pairing{2}{(\pairing{\encode{t}}{\encode{u}})} &
+  \encode{\primrec{z}{s}{t}} &\coloneq
+    \pairing{5}{(\pairing{\encode{z}}{(\pairing{\encode{s}}{\encode{t}})})}.
+\end{align*}
+In general, each constructor has a unique tag and this is paired with an
+encoding for each subterm. We can analyse an encoded term by reverting the
+pairing function and inspecting the tag. For an invalid tag (for our encoding of
+lists this is anything greater than 2) we can return an arbitrary value.
+Performing recursion on G\"odel encodings is difficult, particularly for values
+with more than one recursive argument.
+
+An alternative encoding strategy uses functions to encode data. One example we
+have already given is our encoding of binary trees, from the introduction.
+Another functional encoding is to represent lists as functions \(\nat \to
+\nat\). Giving the function \zero{} will return the length of the list, and the
+values are 1-indexed. This strategy doesn't require a pairing function, but
+values no longer have a unique representation. For example, the functions
+\(\lambda n.~n + n\) and \(\lambda n. \zero\) both represent the empty list.
+
+\end{document}