Remove invalid reference to `map`.

1 files changed, 20 insertions, 16 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index ff4bc5c..83130ea 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -141,7 +141,7 @@ index of the given child.
 \begin{figure}
   \begin{align*}
     \roll*~ts~x &\coloneq \tuple*{
-      \suc~(\mathsf{max}~(\mapkw~(\lambda t. t.0)~ts)),
+      \suc~(\mathsf{max}~(\lambda t. t.0)~ts),
       \lambda i. \domatch*{i}{
         \mathsf{nil}. x;
         \mathsf{cons}(i, j). {(\mathsf{index}~ts~i).1~j}}}
@@ -161,8 +161,8 @@ We present the encoding of \roll*{} and \foldkw{} in
 \cref{fig:phase-2-encode}. We add four new operators for working with
 lists:
 \begin{description}
-  \item[\(\mathsf{max}\)] for calculating the maximum from a list of
-    naturals;
+  \item[\(\mathsf{max}\)] for calculating the maximum from a list,
+    given a function converting values to naturals;
   \item[\(\mathsf{snoc}\)] for appending a single item to the end of a
     list;
   \item[\(\mathsf{index}\)] for retrieving an item from a list;
@@ -211,10 +211,11 @@ let balanced n f = primrec n with
     match xs with
       []      => Leaf f
     | x :: xs => snd (index [] x) xs)
-| Suc (depth, heap) => (Suc (max [depth, depth]), fun xs =>
-    match xs with
-      []      => Branch (0, 1)
-    | x :: xs => snd (index [(depth, heap), (depth, heap)] x) xs)
+| Suc (depth, heap) =>
+    (Suc (max (fun (d, h) => d) [(depth, heap), (depth, hep)]), fun xs =>
+      match xs with
+        []      => Branch (0, 1)
+      | x :: xs => snd (index [(depth, heap), (depth, heap)] x) xs)
 \end{systemt}
 \vspace{-\baselineskip}
 \end{listing}
@@ -306,11 +307,11 @@ 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 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
+We encode \(\mathsf{max}~f~t\) by primitive recursion on the length of
+the list \(t\).
+\[\doprimrec{t.0}{\zero}{x}{(x.1 - f~x.0) + f~x.0}\]
+We compute the binary 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.
@@ -338,12 +339,15 @@ of eliminators, as these all construct lists. Similarly pattern
 matching ``constructs'' the tail of a non-empty list. The only other
 operator we could possibly add as an eliminator is
 \(\mathsf{max}\). There are two main reasons we have not done
-this. Firstly, \(\mathsf{max}\) is only defined on lists of naturals,
-so we would end up with a non-uniform representation of
-lists. Secondly, the maximum is only computed for a small number of
+this. Firstly, the maximum is only computed for a small number of
 lists. In our running examples we compute the maximum only twice,
 whereas we use lists thoughout. Carrying redundant data around for an
-infrequent operation is inefficient and would complicate the encoding.
+infrequent operation is inefficient and would complicate the
+encoding. Secondly, \(\mathsf{max}\) interacts poorly with pattern
+matching. The only way to correctly calculate the maximum of the tail
+of a list is to start from scratch. Whilst for our purposes an
+overestimate is acceptable, carrying data we need to recompute is
+inefficient.
 
 After phase three, our example for \systemtinline{balanced} beta
 reduces to the following: