From 300515a538313b09c082adf79495cfe053d3b8e3 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 29 Apr 2025 17:50:45 +0100
Subject: Give the encoding for fold.

---
 sec/encoding.ltx | 29 +++++++++++++++++++----------
 1 file changed, 19 insertions(+), 10 deletions(-)

(limited to 'sec')

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
-- 
cgit v1.2.3