From c80dbda045f6951f43868a065f7dbf35d6949622 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 29 Apr 2025 17:16:57 +0100
Subject: Give the encoding of roll.

---
 sec/encoding.ltx | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

(limited to 'sec')

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 4afc43f..ac4d174 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -138,9 +138,20 @@ this root. Instead of eagerly computing paths within the heap, we
 compute new paths lazily. The only necessary value to store is the
 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}}}
+\]
+
 \TODO{
   \begin{itemize}
-    \item give the encoding of roll
     \item give the encoding of fold
     \item justify the max operator
     \item justify the head operator
-- 
cgit v1.2.3