;; -*-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
[Addenda (Mar 21, 2011)]
* Proving PRED . SUCC is the identity, syntactically
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,n,m] =
> map make_var ["pn","cn","ck","cl","seed","n","m"]
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
* Proving PRED . SUCC is the identity, syntactically
P-numerals have a remarkable property of letting us prove that
the predecessor is the left inverse of the successor _for all_
integers. The proof is within the lambda-calculus itself, without
resorting to metatheory and the induction principle. In other words,
in stark contrast to Church numerals, for P-numerals
the composition pred . succ normalizes to the identity function.
We have defined the successor on P-numerals, called succp, earlier
in this file. We define the predecessor simply as
> combK = x ^ y ^ x -- the K combinator
> predp = n ^ n # combK # combI
(one can use anything in place of combI. More properly, one should use -1).
As a spot-check:
*LC_Pnum> eval p1 -- The P-numeral 1
(\f. f (\f. (\x. x)))
*LC_Pnum> eval (succp # p1)
(\f. (\x. f (\f. f (\f. (\x. x))) (f (\f. (\x. x)) x)))
Checking that (succp # p1) is beta-eta-equivalent to p2:
*LC_Pnum> eval (succp # p1) == eval p2
True
Decrementing (succp # p1):
*LC_Pnum> eval (predp # (succp # p1))
(\f. f (\f. (\x. x)))
Checking that (predp # (succp # p1)) is beta-eta-equivalent to p1
*LC_Pnum> eval (predp # (succp # p1)) == eval p1
True
We now define the composition of predp and succp
> predsucc = n ^ predp # (succp # n)
and normalize it
*LC_Pnum> eval predsucc
(\n. n)
Thus (predp . succp) indeed normalizes to the identity function.