diff options
Diffstat (limited to 'sec/systemt.ltx')
| -rw-r--r-- | sec/systemt.ltx | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/sec/systemt.ltx b/sec/systemt.ltx index 75461f9..c43223e 100644 --- a/sec/systemt.ltx +++ b/sec/systemt.ltx @@ -302,10 +302,11 @@ reconstruct both folds and pattern matching. \subsubsection*{Heap Encodings} -This encoding strategy is a crude approximation of a heap of memory. Given an -indexing type \(I\), an inductive type is a triple of a \emph{recursive depth}, -a \emph{root index}, and an \(I\)-indexed \emph{heap} of values. Instead of -storing recursive values ``in-line'', one stores an index to its place in the heap. +This encoding strategy is a crude approximation of a heap of +memory~\cite{heap}. Given an indexing type \(I\), an inductive type is +a triple of a \emph{recursive depth}, a \emph{root index}, and an +\(I\)-indexed \emph{heap} of values. Instead of storing recursive +values ``in-line'', one stores an index to its place in the heap. Consider the binary tree \(\mathsf{branch}(\mathsf{branch}(\mathsf{leaf}(1), \mathsf{leaf}(2)), |