Fix 608--619.

1 files changed, 10 insertions, 17 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 19f2a73..c5a311b 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -327,7 +327,7 @@ inspecting the length of the list to match.
 \begin{multline*}
 \domatch{t}{
   \mathsf{nil}. f;
-  \mathsf{cons}(x, y). g
+  \mathsf{cons}~x~y. g
 } \coloneq \\
 \mathsf{if}~t.0 = \zero~\mathsf{then}~f~\mathsf{else}~\sub{g}{
   x/t.1~\zero, y/\tuple{\mathsf{pred}~t.0, \lambda i.~t.1~(\suc~i)}
@@ -338,22 +338,15 @@ non-empty list. We retreive the head by calling the index function
 with index zero. The tail is one shorter that the initial list, and
 the index function is shifted by one.
 
-We have shown that \(\mathsf{length}\) and \(\mathsf{index}\) are
-sufficient to produce an eliminator encoding for lists. We cannot add
-\(\mathsf{nil}\), \(\mathsf{cons}\) nor \(\mathsf{snoc}\) to the set
-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, 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. 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.
+Our eliminator encoding could also include \(\mathsf{max}\). We avoid
+this for two reasons. Firstly, we can compute the maximum using the
+length and indexing functions, so adding an explicit eliminator is
+redundant information. Secondly, most lists do not need to know their
+maximum. We only need the maximum of lists passed to \roll*{}. Most
+lists we create are indices for \foldkw{}, where there is no reason to
+compute the maximum. Even when we do need to compute the maximum, most
+lists passed to \roll*{} have a static length making the
+\(\mathsf{max}\) operator easy to partially evaluate.
 
 After phase three, our example for \systemtinline{balanced} beta
 reduces to the following: