From d8c0da7f27a1b89e005feddb83763cb453a9ac2a Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Tue, 24 Jun 2025 18:39:42 +0100 Subject: Note eliminator encoding works for lists. --- sec/systemt.ltx | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'sec') diff --git a/sec/systemt.ltx b/sec/systemt.ltx index 8b24706..75461f9 100644 --- a/sec/systemt.ltx +++ b/sec/systemt.ltx @@ -295,6 +295,11 @@ our sum and depth example, we have no way of knowing whether the value representing a tree came from a leaf or branch as we deliberately forget this information. +A notable exception to this general trend is lists. We can encode a +list as a pair of its length and its index function, returning the +element at a given position. From these two eliminators, we can +reconstruct both folds and pattern matching. + \subsubsection*{Heap Encodings} This encoding strategy is a crude approximation of a heap of memory. Given an -- cgit v1.2.3