;; -*-mode: Outline;  -*-

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. It turns out, P-numerals were first
discovered by Michel Parigot in 1988.

   * Motivation
   * P-numerals
     ** P-numerals and lists
     ** P-numerals in the lambda-calculator written in Haskell
   * The diffs combinator: computing the symmetric difference
   * P-numerals and the list fold

     [Addenda (Dec 31, 2005)]
   * Additional properties of P-numerals
   * P-numerals and Goedel's recursor R

     [Addenda (Jan 24, 2010)]
   * P-numerals are Parigot integers
   * P-numerals from Peano induction schema

The original article was posted on a comp.lang.functional newsgroup:
     From posting-system@google.com Fri Aug 30 01:49:31 2002
     Date: Thu, 29 Aug 2002 18:49:18 -0700
     From: oleg-at-pobox.com 
     Newsgroups: comp.lang.functional
     Subject: Symmetric difference in LC, P-numerals, and fold
     Message-ID: <7eb8ac3e.0208291749.3bcd95c6@posting.google.com>

This is a literate Haskell script that defines the module LC_Pnum. The
module exports the following functions

> module LC_Pnum (
>   p0, p1, p2,       -- sample P-numerals
>   succp,            -- the successor function for P-numerals
>   c2p, p2c,         -- conversion between Church and P-numerals
>
>   diffs             -- symmetric difference function for two Church numerals
> ) where


* Motivation

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.


* P-numerals

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 and lists

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". With the normal
order of evaluation, 'up pn', 'down pn', and 'emptyp? pn' all take
the constant time. In contrast, the predecessor of a Church numeral
takes linear time (proportional to the magnitude of the numeral). One
connection between P-numerals and lists should be apparent: Operations
'cons', 'head' and the emptiness testing on lists take -- like the
corresponding operations on P-numerals -- constant time.


** P-numerals in the lambda-calculator written in Haskell

In the following, we would be using the lambda-calculator in Haskell
described in 
	http://www.mail-archive.com/haskell@haskell.org/msg10769.html
Note that x ^ t denotes (\x . t) and x # y stands for an application
of x to y. To recall, this article is also 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. 


* The diffs combinator: computing the symmetric difference

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

> 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 the unary representation of numerals.
If we used Church numerals internally when computing diffs, the
complexity would have been quadratic.


* P-numerals and the list fold

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 a 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 [])



* Additional properties of P-numerals
Let p_n be the P-numeral that corresponds to a non-negative integer n.
Let S, K, I be combinators in the SKI calculus. We observe:

	p_n p_m = I  for any n, m >= 0

 For example,
 *LC_Pnum> eval $ p1 # p2
 (\x. x)

	p_n I = p_0   for odd n
              = K p_0 for even n > 0
	      = I     for n = 0


	p_n K = K p_{n-1}, n > 0

	p_n S I I = I   for even n > 0
		  = p_0 for odd n


	add p = p (K succp), or
	add p = p (add I)


	mul p_n p_m = p_n (K (add p_m)) p_0


	mul I I = add I

The even/odd dichotomy is notable.


* P-numerals and Goedel's recursor R

Peter G. Hancock, in a private message sent in Nov 2004, observed:

P-numerals are closely related to the recursor R in Godel's T.
One form of this is:

   R b a 0 = a
   R b a (Succ n) = b n (R b a n)

 ie. R b a n = p_n b a


* Parigot integers

Paul Brauner has pointed out that P-numerals have been introduced by
Michel Parigot back in 1988, with different motivations and in a typed
setting:

Michel Parigot: Programming with proofs: A second order type theory.
LNCS 300, pp. 145-159, 1988.


* P-numerals from Peano induction schema

Paul Brauner has pointed yet another way to come to P-numerals, from
the encoding of Peano induction schema in type theory:

  N n = forall P. P 0 -> (forall m. N m -> P m -> P (S m)) -> P n

To show just the structure of the type N, we roughen the above
yielding an inductive equation

  N = forall P. P -> (N -> P -> P) -> P

The connection to Goedel recursor is becoming apparent. Paul Brauner
has pointed to his recent work on using supernatural deduction modulo
to derive recursors from inductive equations such as above:

      Lisa Allali and Paul Brauner: Inductive Types as Equations.
      http://www.loria.fr/~brauner/pdf/papers/inductives.pdf