diff options
Diffstat (limited to 'sec/encoding.ltx')
| -rw-r--r-- | sec/encoding.ltx | 23 |
1 files changed, 14 insertions, 9 deletions
diff --git a/sec/encoding.ltx b/sec/encoding.ltx index 9f13f1c..23a8784 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -73,17 +73,22 @@ operator satisfies the following equation: \] We require a few operations on lists to compute this transformation: -\(\mathsf{nil}\) representing the empty list; \(\mathsf{cons}\) for -adding an element to the head of a list; \(\mathsf{length}\) to -compute a list's length; and \(\mathsf{index}\) to retrieve a value -from a list by position. We give the four equations these operators -satisfy below. Note that whilst this encoding phase does not strictly -require \(\mathsf{index}\), it is both necessary to describe the -equational theory and will be used in the next phase. +\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{index}~(\mathsf{cons}~t~u)~\zero &= t \\ -\mathsf{length}~(\mathsf{cons}~t~u) &= \suc~(\mathsf{length}~u) & +\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*} |