From 4effb07fd8c301eb1f98df7774da5900ffc21a31 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 29 Apr 2025 14:49:07 +0100
Subject: Explain why we used natural-list indices.

---
 sec/encoding.ltx | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'sec/encoding.ltx')

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
-- 
cgit v1.2.3

