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