Fix 258--275.

1 files changed, 31 insertions, 26 deletions

diff --git a/sec/systemt.ltx b/sec/systemt.ltx
index f887328..dd64d07 100644
--- a/sec/systemt.ltx
+++ b/sec/systemt.ltx
@@ -323,33 +323,38 @@ different constructors within a single type.
 \label{fig:box-pointer:tree}\label{fig:box-pointer:heap}
 \end{figure}
 
-The recursive depth is essential for the fold operation. We
-iteratively construct a heap of values; the recursive depth is an
-upper bound on the number of steps it takes to converge on the
-``true'' result of the fold. For recursive depth zero, we return an
-arbitrary value at each index. As no inductive value is made from
-applying zero constructors, we have no soundness obligations. For the
-successor case, at any given index we look up the constructor and
-payload in the heap. We use the induction hypothesis to replace
-inductive components with their final values, and then apply the
-appropriate fold branch.
+The recursive depth is essential for the fold operation. We give an
+example in \cref{fig:heap-fold}. The \(results\) function constructs a
+heap of values; the recursive depth is an upper bound on the number of
+steps it takes to converge on the ``true'' result of the fold. For
+recursive depth zero, \(results\) returns an arbitrary value at each
+index. As no inductive value is made from applying zero constructors,
+we have no soundness obligations. For the successor case, at any given
+index \(results\) looks up the constructor and payload in the heap. It
+uses the induction hypothesis to replace inductive components with
+their final values, and then applies the appropriate fold branch. We
+retrieve the final value by looking up the root in \(results\).
 
-\[
-\dofoldmatch*{t}{
-  \mathsf{leaf}(n).      f(n);
-  \mathsf{branch}(x, y). g(x, y)
-} \coloneq
-\dolet
-  {\tuple{depth, root, heap}}{t}
-  {go}*{
-    \doprimrec*{depth}
-      {\arb{}}
-      {h}{\lambda i.
-        \domatch*{heap~i}{
-          \mathsf{Left}(n).     f(n);
-          \mathsf{Right}(j, k). g(h~i, h~j)}}}
-  *{go~root}
-\]
+\begin{figure}
+  \[
+  \dofoldmatch*{t}{
+    \mathsf{leaf}(n).      f(n);
+    \mathsf{branch}(x, y). g(x, y)
+  } \coloneq
+  \dolet
+    {\tuple{depth, root, heap}}{t}
+    {results}*{
+      \doprimrec*{depth}
+        {\arb{}}
+        {h}{\lambda i.
+          \domatch*{heap~i}{
+            \mathsf{Left}(n).     f(n);
+            \mathsf{Right}(j, k). g(h~i, h~j)}}}
+    *{results~root}
+  \]
+  \caption{The heap encoding of fold for binary trees.}%
+\label{fig:heap-fold}
+\end{figure}
 
 Roll is harder to encode as it involves merging several heaps into
 one. The basic idea is that the indices for the new heap have to