diff options
Diffstat (limited to 'sec/encoding.ltx')
| -rw-r--r-- | sec/encoding.ltx | 14 |
1 files 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} |