From d9a0d21a21f2c597f78d2ac9f817b5ee7d3fd334 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 29 Apr 2025 14:20:42 +0100
Subject: Explain why we use a heap encoding.

---
 sec/encoding.ltx | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

(limited to 'sec/encoding.ltx')

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 6d339bd..29929d5 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -120,12 +120,16 @@ 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.
 
+We choose to use a heap encoding over another encoding strategy for the
+following reasons. Firstly, inductive types in \lang{} can contain higher-order
+data, such as our tree of functions, which prevents us from using G\"odel
+encodings. Using a local translation makes writing the encoding easier, and as
+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.
+
 \TODO{
   \begin{itemize}
-    \item describe that storing higher-order data makes G\"odel encodings
-      impractical
-    \item describe that the need for local encodings rules out Church encodings
-    \item describe that the need for fold invalidates using codata encodings
     \item explain that using nat-list indices reflects the structure of terms
     \item give the encoding of roll
     \item give the encoding of fold
-- 
cgit v1.2.3

