From 676205e1ab81357b59543984cd940d9be9807385 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Thu, 26 Jun 2025 13:19:15 +0100 Subject: Fix 479--485. --- sec/encoding.ltx | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) (limited to 'sec') diff --git a/sec/encoding.ltx b/sec/encoding.ltx index 1db6720..da9230f 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -143,12 +143,13 @@ pointers. The idea is that the heap index describes the path taken through the term to reach a particular entry, 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 +We chose to use a heap encoding over another encoding strategy by +elimination of the other strategies. 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. Unlike the description of the heap encoding in -- cgit v1.2.3