Fix 138--149.

1 files changed, 9 insertions, 9 deletions

diff --git a/sec/systemt.ltx b/sec/systemt.ltx
index 7ed5870..c9f280b 100644
--- a/sec/systemt.ltx
+++ b/sec/systemt.ltx
@@ -151,19 +151,19 @@ is lacking in some regard.
 
 \subsubsection*{G\"odel Encodings}
 
-G\"odel encodings represent inductive data types as natural
-numbers. It is well-known that there are pairing functions, bijections
-from \(\mathbb{N} \times \mathbb{N}\) to \(\mathbb{N}\), that are primitive recursive. We can use
-these functions to encode inductive types as pairs of tags and
-payloads, such that every constructor has a unique tag. Writing
-\(\tuple{\cdot, \cdot}\) for a chosen pairing function, we can encode the
-binary tree constructors as
+G\"odel encodings~\cite{dialectica?} represent data types as natural
+numbers. It is well-known that there are pairing functions, invertible
+functions from \(\mathbb{N} \times \mathbb{N}\) to \(\mathbb{N}\), that are primitive
+recursive~\cite{pairing}. We can use pairing functions to encode
+inductive types as pairs of tags and payloads, such that every
+constructor has a unique tag. Writing \(\tuple{\cdot, \cdot}\) for a chosen
+pairing function, we can encode the binary tree constructors as
 \begin{align*}
   \mathsf{leaf}(n) &\coloneq \tuple{0, n} \\
   \mathsf{branch}(l, r) &\coloneq \tuple{1, \tuple{l, r}}.
 \end{align*}
-One can pattern match on G\"odel encodings by using the unpairing part of
-the bijection to split a value back into the tag and payload.
+One can pattern match on G\"odel encodings by unpairing a value to
+split it back into the tag and payload.
 
 One major limitation of G\"odel encodings is that they cannot
 represent higher-order data such as functions. The defining trait of