<div>On Thu, Sep 20, 2012 at 3:15 PM,<span dir="ltr">&lt;<a href="mailto:oleg@okmij.org" target="_blank">oleg@okmij.org</a>&gt;</span> wrote:</div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">

Incidentally, there is more than one way to build a predecessor of Church numerals. Kleene&#39;s solution is not the only one. </blockquote><div><br></div><div>Wouldn&#39;t you say then that &quot;Church encoding&quot; is still the more appropriate reference given that Boehm-Berarducci&#39;s algorithm is rarely used? And also that on discovering Church numerals in the untyped setting, one easily sees how to get it to work in Haskell? Even when one has no inkling of the larger picture of the embedding into System F?</div>

<div><br></div><div>When I need to encode pattern matching it&#39;s goodbye Church and hello Scott. Aside from your projects, where else is the B-B procedure used?</div><div><br></div><div><br clear="all">-- Kim-Ee<br>
<br><br><div class="gmail_quote">On Thu, Sep 20, 2012 at 3:15 PM,  <span dir="ltr">&lt;<a href="mailto:oleg@okmij.org" target="_blank">oleg@okmij.org</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

<div class="im"><br>
Dan Doel wrote:<br>
&gt; &gt;&gt; P.S. It is actually possible to write zip function using Boehm-Berarducci<br>
&gt; &gt;&gt; encoding:<br>
</div>&gt; &gt;&gt;         <a href="http://okmij.org/ftp/Algorithms.html#zip-folds" target="_blank">http://okmij.org/ftp/Algorithms.html#zip-folds</a><br>
<div class="im">&gt;<br>
&gt; If you do, you might want to consider not using the above method, as I<br>
&gt; seem to recall it doing an undesirable amount of extra work (repeated<br>
&gt; O(n) tail).<br>
</div>It is correct. The Boehm-Berarducci web page discusses at some extent<br>
the general inefficiency of the encoding, the need for repeated<br>
reflections and reifications for some (but not all) operations. That<br>
is why arithmetic on Church numerals is generally a bad idea.<br>
<br>
A much better encoding of numerals is what I call P-numerals<br>
        <a href="http://okmij.org/ftp/Computation/lambda-calc.html#p-numerals" target="_blank">http://okmij.org/ftp/Computation/lambda-calc.html#p-numerals</a><br>
It turns out, I have re-discovered them after Michel Parigot (so my<br>
name P-numerals is actually meaningful). Not only they are faster; one<br>
can _syntactically_ prove that PRED . SUCC is the identity.<br>
<br>
The general idea of course is Goedel&#39;s recursor R.<br>
<br>
   R b a 0 = a<br>
   R b a (Succ n) = b n (R b a n)<br>
<br>
which easily generalizes to lists. The enclosed code shows the list<br>
encoding that has constant-time cons, head, tail and trivially<br>
expressible fold and zip.<br>
<div class="im"><br>
<br>
Kim-Ee Yeoh wrote:<br>
&gt; So properly speaking, tail and pred for Church-encoded lists and nats<br>
&gt; are trial-and-error affairs. But the point is they need not be if we<br>
&gt; use B-B encoding, which looks _exactly_ the same, except one gets a<br>
&gt; citation link to a systematic procedure.<br>
&gt;<br>
&gt; So it looks like you&#39;re trying to set the record straight on who actually<br>
&gt; did what.<br>
<br>
</div>Exactly. Incidentally, there is more than one way to build a<br>
predecessor of Church numerals. Kleene&#39;s solution is not the only<br>
one. Many years ago I was thinking on this problem and designed a<br>
different predecessor:<br>
<br>
excerpted from <a href="http://okmij.org/ftp/Haskell/LC_neg.lhs" target="_blank">http://okmij.org/ftp/Haskell/LC_neg.lhs</a><br>
<br>
<br>
    One ad hoc way of defining a predecessor of a positive numeral<br>
                    predp cn+1 ==&gt; cn<br>
    is to represent &quot;predp cn&quot; as &quot;cn f v&quot;<br>
    where f and v are so chosen that (f z) acts as<br>
            if z == v then c0 else (succ z)<br>
    We know that z can be either a numeral cn or a special value v. All<br>
    Church numerals have a property that (cn combI) is combI: the identity<br>
    combinator is a fixpoint of every numeral. Therefore, ((cn combI) (succ<br>
    cn)) reduces to (succ cn). We only need to choose the value v in such<br>
    a way that ((v I) (succ v)) yields c0.<br>
<br>
    &gt; predp = eval $<br>
    &gt;   c ^ c<br>
    &gt;        # (z ^ (z # combI # (succ # z)))       -- function f(z)<br>
    &gt;        # (a ^ x ^ c0)                         -- value v<br>
<br>
<br>
{-# LANGUAGE Rank2Types #-}<br>
<br>
-- List represented with R<br>
<br>
newtype R x = R{unR :: forall w.<br>
  -- b<br>
  (x -&gt; R x -&gt; w -&gt; w)<br>
  -- a<br>
  -&gt; w<br>
  -- result<br>
  -&gt; w}<br>
<br>
nil :: R x<br>
nil = R (\b a -&gt; a)<br>
<br>
-- constant type<br>
cons :: x -&gt; R x -&gt; R x<br>
cons x r = R(\b a -&gt; b x r (unR r b a))<br>
<br>
-- constant time<br>
rhead :: R x -&gt; x<br>
rhead (R fr) = fr (\x _ _ -&gt; x) (error &quot;head of the empty list&quot;)<br>
<br>
-- constant time<br>
rtail :: R x -&gt; R x<br>
rtail (R fr) = fr (\_ r _ -&gt; r) (error &quot;tail of the empty list&quot;)<br>
<br>
-- fold<br>
rfold :: (x -&gt; w -&gt; w) -&gt; w -&gt; R x -&gt; w<br>
rfold f z (R fr) = fr (\x _ w -&gt; f x w) z<br>
<br>
-- zip is expressed via fold<br>
rzipWith :: (x -&gt; y -&gt; z) -&gt; R x -&gt; R y -&gt; R z<br>
rzipWith f r1 r2 =  rfold f&#39; z r1 r2<br>
 where f&#39; x tD = \r2 -&gt; cons (f x (rhead r2)) (tD (rtail r2))<br>
       z       = \_  -&gt; nil<br>
<br>
-- tests<br>
<br>
toR :: [a] -&gt; R a<br>
toR = foldr cons nil<br>
<br>
toL :: R a -&gt; [a]<br>
toL = rfold (:) []<br>
<br>
<br>
l1 = toR [1..10]<br>
l2 = toR &quot;abcde&quot;<br>
<br>
<br>
t1 = toL $ rtail l2<br>
-- &quot;bcde&quot;<br>
<br>
t2 = toL $ rzipWith (,) l2 l1<br>
-- [(&#39;a&#39;,1),(&#39;b&#39;,2),(&#39;c&#39;,3),(&#39;d&#39;,4),(&#39;e&#39;,5)]<br>
<br>
<br>
</blockquote></div><br></div>