From 6ca26199d5b57ebc0c33d1009d8bff8be92142c1 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Fri, 25 Apr 2025 12:00:48 +0100
Subject: Describe encoding of inductive types.

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

(limited to 'sec/encoding.ltx')

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index ffc868b..a8d0269 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -101,9 +101,17 @@ Given a well-formedness derivation \(\jdgmnt{ty}{\Psi}{A}\), a type variable \(X
 that calls each accumulator within \(A\) in sequence. The definition is by
 induction on the well-formedness derivation.
 
+\subsection{Phase 2: Encoding Inductive Types}%
+\label{subsec:inductive-types}
+
+We use a modified heap encoding to encode regular types. We use a
+\(\mathsf{List}~\nat\)-indexed heap, but keep the pointers within terms as
+naturals. The idea is that the heap index describes the path taken through the
+term to reach a particular point, whilst the pointers describe the next step
+along the path.
+
 \TODO{
   \begin{itemize}
-    \item state that we encode inductive types as nat-list-indexed heaps
     \item describe that storing higher-order data makes G\"odel encodings
       impractical
     \item describe that the need for local encodings rules out Church encodings
-- 
cgit v1.2.3

