From 2121ecaf46a6f0500934662686563e8692e166e6 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 29 Apr 2025 18:33:07 +0100
Subject: Provide (weak) justification for `max`.

---
 sec/encoding.ltx | 29 +++++++++++++++++++++++------
 1 file changed, 23 insertions(+), 6 deletions(-)

(limited to 'sec/encoding.ltx')

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index dc3f8c8..1063ba7 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -158,36 +158,53 @@ index of the given child.
 More formally, we encode the type \(\mu X. A\) as \(\nat \times
 (\mathsf{List}~\nat \to \sub{A}{X/\nat})\), recursively encoding \(A\).
 We present the encoding of \roll*{} and \foldkw{} in
-\cref{fig:phase-2-encode}. 
+\cref{fig:phase-2-encode}. We add three new operators for working with
+lists:
+\begin{description}
+  \item[\(\mathsf{max}\)] for calculating the maximum from a list of
+    naturals;
+  \item[\(\mathsf{snoc}\)] for appending a single item to the end of a
+    list;
+  \item[\(\mathsf{match}\)] for pattern matching on a list.
+\end{description}
+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.
 
 \TODO{
   \begin{itemize}
-    \item justify the max operator
     \item justify the head operator
     \item justify the snoc operator
     \item justify the arb operator
   \end{itemize}
 }
 
-After some beta reduction we recover the following definition for \systemtinline{balanced}:
+We now return to our examples. After some beta reduction we recover
+the following value for \systemtinline{balanced}:
 \begin{listing}[H]
 \begin{systemt}
 let balanced n f = primrec n with
   Zero              => (1, fun xs =>
     match xs with
       []      => Leaf f
-    | x :: xs => arb)
+    | x :: xs => match x with
+      _ => arb)
 | Suc (depth, heap) => (1 + max [depth, depth], fun xs =>
     match xs with
       []      => Branch (0, 1)
     | x :: xs => match x with
         0 => heap xs
-      | 1 => heap xs)
+      | 1 => heap xs
+      | _ => arb)
 \end{systemt}
 \vspace{-\baselineskip}
 \end{listing}
 
-And here is the updated definition of \systemtinline{compose}:
+And here is the updated value of \systemtinline{compose}:
 \begin{listing}[H]
 \begin{systemt}
 let compose (depth, heap) =
-- 
cgit v1.2.3