Give the encoding of `match`.

1 files changed, 17 insertions, 2 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index b90c5b9..43acd65 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -260,7 +260,7 @@ the list \(u\), by
 \[
 \tuple{
   \suc~u.0,
-  \lambda x.\mathsf{if}~x = 0~
+  \lambda x.\mathsf{if}~x = \zero~
     \mathsf{then}~t~
     \mathsf{else}~u.0~(\mathsf{pred}~x)}
 \]
@@ -292,10 +292,25 @@ 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.
 
+The final operator to encode is pattern matching. We achieve this by
+inspecting the length of the list to match.
+\begin{multline*}
+\domatch{t}{
+  \mathsf{nil}. f;
+  \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)}
+}
+\end{multline*}
+The tricky part of this definition is computing the head and tail of a
+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 too.
+
 \TODO{
   \begin{itemize}
     \item explain why a list is a pair of length and index function
-    \item give the encoding of head
   \end{itemize}
 }