From 22ae2d172d3be761319a8be39813e291e11c59b6 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Thu, 26 Jun 2025 13:31:53 +0100 Subject: Fix 514--525. --- sec/encoding.ltx | 25 ++++++++++--------------- 1 file changed, 10 insertions(+), 15 deletions(-) (limited to 'sec/encoding.ltx') diff --git a/sec/encoding.ltx b/sec/encoding.ltx index fd71af8..becab5e 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -199,21 +199,16 @@ These operators satisfy the following equations: \end{align*} Computing the maximum value from a list is necessary to correctly -determine the recursive depth to use when folding over an inductive -value. It is also the primary reason why infinite inductive types are -forbidden. Take for example the inductive type \(\mu X. 1 + (\nat \to -X)\) of countable trees. To compute the recursive depth, we need to -compute the maximum of a countable sequence, which is impossible in -general. Thus we cannot encode such infinite types. - -We need the \(\mathsf{snoc}\) operation to find the indices of -inductive components within the encoding of \foldkw{}. This is true -even if we computed paths eagerly during \roll*{}; we need -\(\mathsf{snoc}\) to fixup paths there instead. - -The final operator we add at this phase is \(\mathsf{match}\) on -lists. We need this to determine whether a path is addressing the root -entry or one of its inductive components. +determine the recursive depth to use when folding over a value. It is +also the primary reason why infinite inductive types are +forbidden. Recall the inductive type \(\mu X. 1 + (\nat \to X)\) of +countable trees. To compute the recursive depth of such a tree, we +need to compute the maximum of an arbitrary countable sequence. Thus +we cannot encode such infinite types. + +We also add \(\mathsf{match}\) on lists. We need this to determine +whether a path is addressing the root entry or one of its inductive +components. We now return to our examples. After some beta reduction we recover the following value for \systemtinline{balanced}: -- cgit v1.2.3