From d9a0d21a21f2c597f78d2ac9f817b5ee7d3fd334 Mon Sep 17 00:00:00 2001 From: Chloe Brown 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