Explain why we used natural-list indices.

1 files changed, 10 insertions, 1 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 29929d5..d68ff72 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -128,9 +128,18 @@ System~T does not have polymorphism, we cannot use Church encodings. We need to
 be able to 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,
+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 the tail the path with
+this root. Instead of eagerly computing paths within the heap, we
+compute new paths lazily. The only necessary value to store is the
+index of the given child.
+
 \TODO{
   \begin{itemize}
-    \item explain that using nat-list indices reflects the structure of terms
     \item give the encoding of roll
     \item give the encoding of fold
     \item justify the max operator