+++ /dev/null
-#Version 4 lists: Efficiently extracting tails#
-
-Version 3 lists and Church numerals are lovely, because they have their recursive capacity built into their very bones. However, one disadvantage
-to them is that it's relatively inefficient to extract a list's tail, or get a
-number's predecessor. To get the tail of the list `[a;b;c;d;e]`, one will
-basically be performing some operation that builds up the tail afresh: at
-different stages, one will have built up `[e]`, then `[d;e]`, then `[c;d;e]`, and
-finally `[b;c;d;e]`. With short lists, this is no problem, but with longer lists
-it takes longer and longer. And it may waste more of your computer's memory
-than you'd like. Similarly for obtaining a number's predecessor.
-
-The v1 lists and numbers on the other hand, had the tail and the predecessor
-right there as an element, easy for the taking. The problem was just that the
-v1 lists and numbers didn't have recursive capacity built into them, in the
-way the v3 implementations do.
-
-A clever approach would marry these two strategies.
-
-Version 3 makes the list `[a;b;c;d;e]` look like this:
-
- \f z. f a (f b (f c (f d (f e z))))
-
-or in other words:
-
- \f z. f a <the result of folding f and z over the tail>
-
-Instead we could make it look like this:
-
- \f z. f a <the tail itself> <the result of folding f and z over the tail>
-
-That is, now `f` is a function expecting *three* arguments: the head of the
-current list, the tail of the current list, and the result of continuing to
-fold `f` over the tail, with a given base value `z`.
-
-Call this a **version 4** list. The empty list can be the same as in v3:
-
-<pre><code>empty ≡ \f z. z</code></pre>
-
-The list constructor would be:
-
-<pre><code>make_list ≡ \h t. \f z. f h t (t f z)</code></pre>
-
-It differs from the version 3 `make_list` only in adding the extra argument
-`t` to the new, outer application of `f`.
-
-Similarly, `five` as a v3 or Church numeral looks like this:
-
- \s z. s (s (s (s (s z))))
-
-or in other words:
-
- \s z. s <the result of applying s to z (pred 5)-many times>
-
-Instead we could make it look like this:
-
- \s z. s <pred 5> <the result of applying s to z (pred 5)-many times>
-
-That is, now `s` is a function expecting *two* arguments: the predecessor of the
-current number, and the result of continuing to apply `s` to the base value `z`
-predecessor-many times.
-
-Jim had the pleasure of "inventing" these implementations himself. However,
-unsurprisingly, he wasn't the first to do so. See for example [Oleg's report
-on P-numerals](http://okmij.org/ftp/Computation/lambda-calc.html#p-numerals).
-
-