\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}