diff options
| -rw-r--r-- | sec/encoding.ltx | 19 |
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} } |