Give the encoding for fold.

1 files changed, 19 insertions, 10 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index ac4d174..296bf73 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -140,19 +140,28 @@ index of the given child.
 
 More formally, we encode the type \(\mu X. A\) as \(\nat \times
 (\mathsf{List}~\nat \to \sub{A}{X/\nat})\), recursively encoding \(A\).
-We present the encoding of \roll*{} below and \foldkw{} in
-\cref{fig:phase-2-fold}.
-\[
-\roll*~ts~x \coloneq \tuple*{
-  1 + \mathsf{max}~(\mapkw{}~(\lambda t. t.0)~ts),
-  \lambda i. \domatch*{i}{
-    \mathsf{nil}. x;
-    \mathsf{cons}(i, j). {(\mathsf{index}~ts~i).1~j}}}
-\]
+We present the encoding of \roll*{} and \foldkw{} in
+\cref{fig:phase-2-encode}.
+
+\begin{figure}
+  \begin{align*}
+    \roll*~ts~x &\coloneq \tuple*{
+      1 + \mathsf{max}~(\mapkw~(\lambda t. t.0)~ts),
+      \lambda i. \domatch*{i}{
+        \mathsf{nil}. x;
+        \mathsf{cons}(i, j). {(\mathsf{index}~ts~i).1~j}}}
+    \\
+    \dofold{t}{x}{u} &\coloneq \dolet
+      {go}*{\doprimrec*{t.0}
+        {\arb}
+        {r}{\lambda i. \sub{u}{x/\mapkw~(\lambda n. r~(\mathsf{snoc}~i~n))~(t.1~i)}}
+      }*{go~\mathsf{nil}}
+  \end{align*}
+  \caption{Phase 2 encoding of the \roll*{} and \foldkw{} operators.}\label{fig:phase-2-encode}
+\end{figure}
 
 \TODO{
   \begin{itemize}
-    \item give the encoding of fold
     \item justify the max operator
     \item justify the head operator
     \item justify the snoc operator