Symmetric difference in LC, P-numerals, and fold

[ol...@pobox.com]

This article derives a term in the pure untyped lambda-calculus that
_efficiently_ computes a symmetric difference of two Church
numerals. We introduce other numerals, so called P-numerals, which are
more convenient for arithmetics. We show the connection between the
P-numerals and the list fold.

Let cn denote a Church numeral corresponding to the natural number
n. In particular, c0 = (\f x. x) and c1 = (\f x. f x). Our goal is to
derive a term diffs, so that (diffs ck cl) reduces to a Church numeral
that corresponds to a number abs(k-l). We can easily visualize the
algorithm of computing the diffs as follows. Let us imagine a data
structure 'list'. This data structure is realized by a constant 'nil'
(which signifies the empty list) and an operation 'up' that adds a
link to the existing list. We also need an operation empty? to check
if the list is empty and an operation 'down', which removes the link
from a non-empty list and returns the shortened list. We can easily
convert a Church numeral ck to a list of 'k' links: we iterate the
'up' function 'k' times on the empty list. To compute (diffs ck cl)
we convert cl to a list of length l, and then apply a down-or-up
operation k times to the list. The down-or-up operation removes a link
from a list. If, however, it encounters an empty list, it "changes the
direction" and starts adding links. Obviously, the result is the list
whose length is abs(k-l). At the last step, we convert the list back
to the corresponding numeral.

To realize the above algorithm more conveniently, let us introduce
P-numerals, which are another representation of naturals in
Lambda-calculus. We shall see shortly where the name comes
from. Recall that the Church numerals are defined as

c0 f x --> x
c1 f x --> f (c0 f x) --> f x
c2 f x --> f (c1 f x) --> f (f x)
succ cn f x --> f (cn f x)

We define P-numerals as follows:

p0 f x --> x { the same as c0 }
p1 f x --> f p0 (p0 f x) --> f p0 x
p2 f x --> f p1 (p1 f x) --> f p1 (f p0 x)
succp pn f x --> f pn (pn f x)

The conversion from Church numerals to P-numerals is trivial:
c2p cn = cn succp p0
The reverse conversion is trivial as well
p2c pn = pn (\p seed. succ seed) c0

P-numerals represent the "list" we have mentioned earlier. Indeed,
'nil' is realized as p0, the 'up' operation is succp, the emptiness
testing is implemented as
emptyp? pn = pn (\p seed . false) true
and the 'down' operation is "pn (\p seed . p) p0"

In the following, we would be using the lambda-calculator in Haskell
described in
http://www.mail-archive.com/has...@haskell.org/msg10769.html
Note that x ^ t denotes (\x . t) and x # y stands
for an application of x to y. The following is the literate Haskell code:

First, we load the calculator and the definitions of common lambda terms
(such as true, false, lif, and cons), as well as the definitions of the
Church numerals (constants c0, c1, c2 and c3 and the term succ).

> import Prelude hiding ((^),succ,not,or,and)
> import Lambda_calc
> import LC_basic

We need to make a few variables with mnemonic names:

> [pn,cn,ck,cl,seed] =
> map make_var ["pn","cn","ck","cl","seed"]

Now we can define P-numerals

> p0 = c0
> succp = pn ^ f ^ x ^ f # pn # (pn # f # x)
> p1 = succp # p0
> p2 = succp # p1

and the conversion functions

> c2p = cn ^ cn # succp # p0
> p2c = pn ^ pn # (pn ^ seed ^ succ # seed) # c0

We can test what we've got: "print c2" prints
(\f. (\x. f (f x)))
and "print $ eval $ c2p # c2" prints the p2-numeral
(\f. (\x. f (\f. f (\f. (\x. x))) (f (\f. (\x. x)) x)))
which we can convert back to the Church form
print $ eval $ p2c # (c2p # c2)
(\f. (\x. f (f x)))
Note that "print $ eval $ c2p # p2c" prints "(\f. f)", the identity
function.

Now we can define the diffs term, by literally following the algorithm
outlined above

> diffs = ck ^ cl ^ toc # (ck # up_or_down # (cons # false # (c2p # cl)))
> where
> -- make variables
> [arg,ud_flag,prev,dummy] =
> map make_var ["arg","ud_flag","prev","_"]
> -- curry the argument
> up_or_down = arg ^ up_or_down' # (car # arg) # (cdr # arg)
> -- if ud_flag is 'true', we build on the pn
> -- if ud_flag is false, we shorten pn, unless it is already p0
> -- in the latter case, we switch the flag
> -- we return a pair (new_flag,new_pn)
> up_or_down' = ud_flag ^ pn ^
> lif # ud_flag
> -- the flag was true: build
> # (cons # true # (succp # pn))
> -- the flag was false: we're going down
> # (pn
> -- pn was > p0: shorten
> # (prev ^ dummy ^ cons # ud_flag # prev)
> -- pn was p0: we will be going up
> # (cons # true # (succp # p0)))
> -- Convert the resulting (flag,pn) to the Church numeral
> toc = arg ^ (p2c # (cdr # arg))

diffs is the genuine Lambda term. We can ask the calculator to print it
out (literally by _printing_ it):

(\ck. (\cl. (\arg. (\pn. pn (\pn. (\seed. (\c. (\f. (\x. f (c f x))))
seed)) (\f. (\x. x))) ((\p. p (\x. (\y. y))) arg)) (ck
(\arg. (\ud_flag. (\pn. (\p. (\x. (\y. p x y))) ud_flag
((\x. (\y. (\p. p x y))) (\x. (\y. x)) ((\pn. (\f. (\x. f pn (pn f
x)))) pn)) (pn (\prev. (\_. (\x. (\y. (\p. p x y))) ud_flag prev))
((\x. (\y. (\p. p x y))) (\x. (\y. x)) ((\pn. (\f. (\x. f pn (pn f
x)))) (\f. (\x. x))))))) ((\p. p (\x. (\y. x))) arg) ((\p. p
(\x. (\y. y))) arg)) ((\x. (\y. (\p. p x y))) (\x. (\y. y))
((\cn. cn (\pn. (\f. (\x. f pn (pn f x)))) (\f. (\x. x))) cl)))))

I submit the "Haskell" format for the term was more comprehensible.

Here are a few tests:
Main> eval $ diffs # c1 # c0
(\f. f) -- which is c1
Main> eval $ diffs # c0 # c1
(\f. f) -- the same
Main> eval $ diffs # c3 # c1
(\f. (\x. f (f x))) -- which is c2
Main> eval $ diffs # c1 # c3
(\f. (\x. f (f x))) -- the same
Main> eval $ diffs # c3 # c3
(\f. (\x. x)) -- or c0

If we assume the normal or a similar lazy order of evaluation,
computing of an application of up_or_down takes only constant
time. Therefore, the overall complexity of 'diffs' is Theta(k+l), which
is the best one can hope for with unary representation of numerals.
If we used Church numerals internally when computing diffs, the
complexity would have been quadratic.

Let us relate the P-numerals and the list fold. We can choose the
following format for the unary representation of numbers in Haskell:

0 -- []
1 -- [[]]
2 -- [[[]],[]]
3 -- [[[[]],[]],[[]],[]]

This representation has the remarkable property that for all i>j,
repr(j) is the proper suffix of repr(i). This is of course a Peano
representation of integers. An integer n is represented by a list of
n links long, which we will call peano(n). The right fold operation
over such lists will have the following property:

foldr f z peano(0) --> z
foldr f z peano(n) --> f peano(n-1) (foldr f z peano(n-1))

Comparing these equations with the definition of P-numerals above, we
see that
pn = \f z -> foldr f z peano(n)

which explains the name for P-numerals. We should also note that
P-numerals are indeed related to lists. We represent a list by a fold
combinator over it! This realization is in the spirit of
Lambda-calculus of representing data structures by functions.

Dealing with data structures such as [[[[]],[]],[[]],[]] is inconvenient
for many reasons. Therefore, we switch to a different format

0 -- []
1 -- [[]]
2 -- [[],[]]
3 -- [[],[],[]]

This format also has the same property that for i>j, repr(j) is a
proper suffix of repr(i). We can define the following fold operator:

> mfoldr f z [] = z
> mfoldr f z (_:p) = f p (mfoldr f z p)

This mfoldr is equivalent to the foldr over the original Peano
representation. We can write P-numerals as

pn = \f z -> mfoldr f z (take n $ repeat [])

and the regular Church numerals as

cn = \f z -> mfoldr (\_ seed -> f seed) z (take n $ repeat [])