diff options
Diffstat (limited to 'sec/encoding.ltx')
| -rw-r--r-- | sec/encoding.ltx | 12 |
1 files changed, 8 insertions, 4 deletions
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 |