diff options
Diffstat (limited to 'sec/encoding.ltx')
| -rw-r--r-- | sec/encoding.ltx | 19 |
1 files changed, 13 insertions, 6 deletions
diff --git a/sec/encoding.ltx b/sec/encoding.ltx index cd59b67..fd71af8 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -153,8 +153,8 @@ write the fold operation, so we cannot use eliminator encodings. Thus the only suitable encoding strategy is a heap encoding. Unlike the description of the heap encoding in -\cref{M-subsec:heap-encoding} we do not use the same type for indices -and pointers. We use \(\mathsf{List}~\nat\) as the index type, +\cref{M-subsec:encoding-strategies} we do not use the same type for +indices and pointers. We use \(\mathsf{List}~\nat\) as the index type, representing a path through the term. We use the empty list to indicate the root of the inductive value. Otherwise, the head of the list selects which child to recurse into and its tail is the path @@ -181,16 +181,23 @@ the \roll*{} operation as we do not need to fixup the entire heap. More formally, we encode the type \(\mu X. A\) as \(\nat \times (\mathsf{List}~\nat \to \sub{A}{X/\nat})\). We present the encoding of -\roll*{} and \foldkw{} in \cref{fig:phase-2-encode}. We add three new +\roll*{} and \foldkw{} in \cref{fig:phase-2-encode}. We add two new operators for working with lists: \begin{description} \item[\(\mathsf{max}\)] for calculating the maximum from a list, - given a function converting values to naturals; - \item[\(\mathsf{snoc}\)] for appending a single item to the tail of - a list; + given a function converting values to naturals; and \item[\(\mathsf{match}\)] for pattern matching on a list as either \(\mathsf{nil}\) or \(\mathsf{cons}\) \end{description} +These operators satisfy the following equations: +\begin{align*} + \mathsf{max}~f~\mathsf{nil} &= 0 & + \domatch{\mathsf{nil}}{\mathsf{nil}. f; \mathsf{cons}~x~y. g} &= f \\ + \mathsf{max}~f~(\mathsf{cons}~t~u) &= f~t \sqcup u & + \domatch{\mathsf{cons}~t~u}{\mathsf{nil}. f; \mathsf{cons}~x~y. g} + &= \sub{g}{x/t, y/u} +\end{align*} + Computing the maximum value from a list is necessary to correctly determine the recursive depth to use when folding over an inductive value. It is also the primary reason why infinite inductive types are |