Give the encoding of `max`.

1 files changed, 23 insertions, 10 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index a0995c5..16b8fd4 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -257,11 +257,18 @@ arbitrary value.
 
 We encode \(\mathsf{cons}~t~u\), adding element \(t\) to the head of
 the list \(u\), by
-\[\tuple{\suc~u.0, \lambda x.\domatch{x}{\zero. t; \suc~x. {u.1}~x}}\]
+\[
+\tuple{
+  \suc~u.0,
+  \lambda x.\mathsf{if}~x = 0~
+    \mathsf{then}~t~
+    \mathsf{else}~u.0~(\mathsf{pred}~x)}
+\]
 The length of our new list is one larger that
-the tail. To lookup a value, we first pattern match on the
-index. Index zero represents the head, which we return
-directly. Otherwise we lookup the index in the tail.
+the tail. To lookup a value, we first test whether the index is
+zero. If it is, we return the new head directly. Otherwise, we
+decrement the index and lookup its value in the tail. The encoding of
+\(\mathsf{if}\) and equality is standard~\cref{if+equals}.
 
 The encoding of \(\mathsf{snoc}~t~u\), adding element \(u\) to the
 tail of the list \(t\), is encoded similarly:
@@ -274,13 +281,20 @@ tail of the list \(t\), is encoded similarly:
 The new list is also one item longer that the old list. When looking
 up an item, we first check if the index is the last in the list. If it
 is, we return the element we are adding to the tail. Otherwise, we
-lookup the index in the old list. We will desugar this comparison in
-the final phase of the encoding.
+lookup the index in the old list.
+
+We encode the \(\mathsf{max}\) operator by primitive recursion on the
+length of the list \(t\).
+\[\doprimrec{t.0}{\zero}{x}{(x.1 - x.0) + x.0}\]
+We compute the maximum by performing a truncated subtraction followed
+by an addition. These both have standard
+encodings~\cref{add+sub}. Note that we use the recursive value on the
+left of the subtraction so that a naive partial evaluator can reduce
+the maximum of a singleton list to a single value.
 
 \TODO{
   \begin{itemize}
     \item explain why a list is a pair of length and index function
-    \item give the encoding of max
     \item give the encoding of head
   \end{itemize}
 }
@@ -294,7 +308,7 @@ let balanced n f = primrec n with
     match length with
       Zero  => Leaf f
     | Suc l => snd arb (l, fun i => idxs (Suc i)))
-| Suc (depth, heap) => (Suc (max depth depth), fun (length, idxs) =>
+| Suc (depth, heap) => (Suc ((depth - depth) + depth), fun (length, idxs) =>
     match length with
       Zero  => Branch (0, 1)
     | Suc l =>
@@ -303,7 +317,7 @@ let balanced n f = primrec n with
         | Suc x => match x with
             Zero  => (depth, heap)
           | Suc x => arb
-        in snd (dh (l, fun i => idxs (Suc i))))
+        in snd dh (l, fun i => idxs (Suc i)))
 \end{systemt}
 \end{listing}
 
@@ -371,7 +385,6 @@ let compose (depth, heap) =
     \item define desugaring of case
     \item define desugaring of map
     \item define desugaring of let
-    \item define desugaring of if-let
   \end{itemize}
 }