diff options
| -rw-r--r-- | sec/encoding.ltx | 40 |
1 files changed, 20 insertions, 20 deletions
diff --git a/sec/encoding.ltx b/sec/encoding.ltx index 23a8784..9b905bc 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -72,26 +72,6 @@ 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} \] -We require a few operations on lists to compute this transformation: -\begin{description} - \item[\(\mathsf{nil}\)] the empty list; - \item[\(\mathsf{cons}\)] adds an element to the head of a list; - \item[\(\mathsf{snoc}\)] adds an element to the tail of a list; - \item[\(\mathsf{length}\)] computes the number of elements in a - list; and - \item[\(\mathsf{index}\)] retrieves a value from a list by position. -\end{description} - -We give the equations these operators satisfy below. -\begin{align*} -\mathsf{snoc}~\mathsf{nil}~v &= \mathsf{cons}~v~\mathsf{nil} & -\mathsf{snoc}~(\mathsf{cons}~t~u)~v &= \mathsf{cons}~t~(\mathsf{snoc}~u~v) \\ -\mathsf{length}~\mathsf{nil} &= \zero & -\mathsf{length}~(\mathsf{cons}~t~u) &= \suc~(\mathsf{length}~u) \\ -\mathsf{index}~(\mathsf{cons}~t~u)~\zero &= t & -\mathsf{index}~(\mathsf{cons}~t~u)~(\suc~n) &= \mathsf{index}~u~n -\end{align*} - 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 @@ -117,6 +97,26 @@ 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}. +We require a few operations on lists to compute this transformation: +\begin{description} + \item[\(\mathsf{nil}\)] the empty list; + \item[\(\mathsf{cons}\)] adds an element to the head of a list; + \item[\(\mathsf{snoc}\)] adds an element to the tail of a list; + \item[\(\mathsf{length}\)] computes the number of elements in a + list; and + \item[\(\mathsf{index}\)] retrieves a value from a list by position. +\end{description} + +We give the equations these operators satisfy below. +\begin{align*} +\mathsf{snoc}~\mathsf{nil}~v &= \mathsf{cons}~v~\mathsf{nil} & +\mathsf{snoc}~(\mathsf{cons}~t~u)~v &= \mathsf{cons}~t~(\mathsf{snoc}~u~v) \\ +\mathsf{length}~\mathsf{nil} &= \zero & +\mathsf{length}~(\mathsf{cons}~t~u) &= \suc~(\mathsf{length}~u) \\ +\mathsf{index}~(\mathsf{cons}~t~u)~\zero &= t & +\mathsf{index}~(\mathsf{cons}~t~u)~(\suc~n) &= \mathsf{index}~u~n +\end{align*} + At the end of this phase, the \systemtinline{compose} example is unchanged. The \systemtinline{balanced} example reduces to the below code. Notice how the \suc{} branch uses the same variable |