Fix 449--463.

1 files changed, 23 insertions, 22 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 9b905bc..2b9b7a8 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -72,30 +72,31 @@ operator satisfies the following equation:
 \dofold{\roll*~t~u}{x}{v} \coloneq \sub{v}{x/\mapkw{}~(\lambda i. \dofold{\mathsf{index}~t~i}{x}{v})~u}
 \]
 
-To encode \roll{} into \roll*{} we require a function that traverses a
-value of type \(\sub{A}{X/\mu X. A}\) and collects all inductive
-components into a single list.  We can extend a list with a single
-value and return the index of that value with the function
-\(\mathsf{extend} : A \to \mathsf{List}~A \to \mathsf{List}~A \times \nat\)
-defined by \(\mathsf{extend}~a~t = \tuple{\mathsf{cons}~a~t,
-  \mathsf{length}~t}\). By using the \mapkw{} pseudo-operator we can
-replace all inductive components in a vessel \(\sub{A}{X/\mu X. A}\)
-with accumulator functions \(\sub{A}{X/\mathsf{List}~(\mu X. A) \to
-  \mathsf{List}~(\mu X. A) \times \nat}\). The non-trivial step is
-``distributing'' the accumulator with the substitution to obtain a
-value of type \(\mathsf{List}~(\mu X. A) \to \mathsf{List}~(\mu X. A) \times
-\sub{A}{X/\nat}\). We can apply this function to the empty list to
-obtain the arguments for \roll*{}.
-
-Given a well-formedness derivation \(\jdgmnt{ty}{\Psi}{A}\), a type
-variable \(X \in \Psi\), a type environment \(\alpha\) and a type \(S\), we
-define a term \(\mathsf{distrib}\) of type
+To transform an argument for \roll{} \(x\) into the arguments for
+\roll*{}, we take the projections of the term
 \[
-\suball{A}{\sub{\alpha}{X/S \to S \times \alpha(X)}} \to S \to S \times \suball{A}{\alpha}
+  \mathsf{distrib}^{\nat}_{\Lambda X. A}~(
+    \maptm{X}{A}~(
+      \lambda y, acc. \tuple{\mathsf{snoc}~acc~y, \mathsf{length}~acc}
+    )~x
+  )~\mathsf{nil}
 \]
-that calls each accumulator within \(A\) in sequence.  The definition
-is by induction on the well-formedness derivation of \(A\). The
-details of the definition are in \cref{M-sec:distrib}.
+The \mapkw{} replaces each inductive component \(\mu X. A\) with an
+accumulator \(\mathsf{List}~(\mu X. A) \to \mathsf{List}~(\mu X. A) \times
+\nat\), which extends a list with the component and records the
+component's index in the list. We then ``distribute'' the accumulator
+over the vessel using the \(\mathsf{distrib}\) meta-operator. We finally
+give the empty list as the initial accumulator.
+
+Given a
+well-formedness derivation \(\jdgmnt{ty}{\Psi}{A}\), a type variable \(X
+\in \Psi\), a type environment \(\alpha\) and a type \(S\),
+\(\mathsf{distrib}^{\alpha, S}_{\Lambda X. A}\) has type
+\[
+\suball{A}{\sub{\alpha}{X/S \to S \times \alpha(X)}} \to S \to S \times \suball{A}{\alpha}.
+\]
+\(\mathsf{distrib}\) calls each accumulator of type in the vessel in
+sequence. We give the details in \cref{M-sec:distrib}.
 
 We require a few operations on lists to compute this transformation:
 \begin{description}