Fix 155--174.

1 files changed, 31 insertions, 27 deletions

diff --git a/sec/systemt.ltx b/sec/systemt.ltx
index 3abcdef..1295654 100644
--- a/sec/systemt.ltx
+++ b/sec/systemt.ltx
@@ -168,37 +168,41 @@ split it back into the tag and payload.
 A major limitation of G\"odel encodings is that they cannot represent
 higher-order data such as functions. G\"odel encodings by definition
 encode data as natural numbers. We cannot encode arbitrary functions
-as naturals, even in simple models such as \mathsf{Set}. If we
+as naturals, even in simple models such as \(\mathsf{Set}\). If we
 restrict ourselves to representable functions, \textcite{bauer} proves
 we cannot recover a function from its syntax.
 
 Another difficulty with G\"odel encodings is implementing the fold
-operation.  We require our chosen pairing function to be monotonic so
-that an inductive value is ``large enough'' to iterate over.  To fold
-a target into the motive type \(A\), we use primitive recursion to
-construct a function from encodings into \(A\).  The intent is that
-the \((n+1)\)-th stage of recursion will correctly fold a target with
-encoding \(n\). There are no expectations for the base case for the
-recursion, so we can use an arbitrary value. For the successor case,
-we use pattern matching to deconstruct the function input into its tag
-and payload. We can use the induction hypothesis to fold over
-inductive components in the payload. Using the induction hypothesis
-gives a correct value, as a monotonic pairing function ensures each
-inductive component is smaller than the function input we are
-currently working on. We then apply the appropriate branch for the
-constructor we have. Below is the fold over binary trees.
-\[
-  \dofoldmatch*[t]{t}{
-    \mathsf{leaf}(n). f(n);
-    \mathsf{branch}(x, y). g(x, y)
-  } \coloneq
-  \dolet{go}*{
-    \doprimrec*{t}{\arb}{h}{
-      \lambda i. \domatch*{i}{
-        \mathsf{leaf}(n). f(n);
-        \mathsf{branch}(l, r). g(h(l), h(r))}}
-  }*{go~t}
-\]
+operation. We need our chosen pairing function to be increasing so
+that values are ``large enough'' to iterate
+over. \Cref{fig:godel-fold} shows how to encode fold over binary
+trees. We use primitive recursion to construct the function \(go\). At
+the \(n\)th recursive step, \(go\) will correctly fold any value
+strictly less than \(n\). For the base case, any result is vacuously
+correct, so \(go\) returns an arbitrary value. To construct the next
+iteration of \(go\), we pattern match on the input value. As our
+chosen pairing function is increasing, we can pass any inductive
+components to the previous iteration of \(go\). We then apply the
+appropriate branch for the constructor we have. As the target \(t\) is
+less than \(\suc~t\), we can pass the target to \(go\) to compute the
+fold.
+
+\begin{figure}
+  \[
+    \dofoldmatch*[t]{t}{
+      \mathsf{leaf}(n). f(n);
+      \mathsf{branch}(x, y). g(x, y)
+    } \coloneq
+    \dolet{go}*{
+      \doprimrec*{\suc~t}{\arb}{h}{
+        \lambda i. \domatch*{i}{
+          \mathsf{leaf}(n). f(n);
+          \mathsf{branch}(l, r). g(h(l), h(r))}}
+    }*{go~t}
+  \]
+  \caption{The G\"odel encoding of \foldkw{} for binary
+    trees.}\label{fig:godel-fold}
+\end{figure}
 
 \subsubsection*{Church Encodings}