Give the encoding of roll.

1 files changed, 12 insertions, 1 deletions

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