From a2afd4b08dc2b7eada2f95ee95457457a3331344 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Tue, 25 Mar 2025 16:52:43 +0000 Subject: Before the big rewrite --- sec/systemt.ltx | 130 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 130 insertions(+) create mode 100644 sec/systemt.ltx (limited to 'sec/systemt.ltx') 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} -- cgit v1.2.3