From ebdbf9eb5db4bdad3a07b58163efa1fa00dfbc39 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Thu, 26 Jun 2025 13:34:44 +0100 Subject: Fix 525--538. --- sec/encoding.ltx | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/sec/encoding.ltx b/sec/encoding.ltx index becab5e..f2ace28 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -210,20 +210,22 @@ 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}: +We now return to our examples. After simplifying using the equational +theory we recover +the below value for \systemtinline{balanced}. In each branch we +increase the recursive depth by one and create a new heap. \begin{listing}[H] \begin{systemt} let balanced n f = primrec n with - Zero => (Suc (max (fun (d, h) => d) []), fun xs => + Zero => (Suc Zero, fun xs => match xs with [] => Leaf f | x :: xs => snd (index [] x) xs) | Suc (depth, heap) => - (Suc (max (fun (d, h) => d) [(depth, heap), (depth, hep)]), fun xs => + (Suc depth, fun xs => match xs with - [] => Branch (0, 1) - | x :: xs => snd (index [(depth, heap), (depth, heap)] x) xs) + [] => Branch (0, 0) + | x :: xs => snd (index [(depth, heap)] x) xs) \end{systemt} \vspace{-\baselineskip} \end{listing} -- cgit v1.2.3