The Bluff combinator

This file gives a solution to a Bluff combinator problem in pure
untyped lambda-calculus. The problem is due to Mayer Goldberg and is
about ten years old:

Let c_i denote a Church numeral for the number i. Design two terms
'beq' and 'bluff' so that the following reductions hold:

beq c_i c_j     ==> \x\y.x (that is, boolean 'true')
		    iff i == j
	        ==> \x\y.y (that is, boolean 'false') otherwise

beq bluff c_i   ==> \x\y.x (that is, boolean 'true') for all i
beq c_i bluff   ==> \x\y.x (that is, boolean 'true') for all i
beq bluff bluff ==> \x\y.y (that is, boolean 'false')


In the following, we will write 'true' for the combinator \x\y.x and
'false' for the combinator \x\y.y . 

It appears that the gist of the problem is discriminating _a_ Church
numeral from some other term. We turn for help to the following
equivalence, which is valid for all Church numerals:
	c_i (\x.false) false <==> false for all i
Therefore, to tell a Church numeral from a bluff combinator, we need
to design 'bluff' so that
	bluff (\x.false) false ==> true
The simplest such term is
	bluff ::= \f\x.true
This term indeed looks like it is bluffing: it says 'true' no matter
what it is applied to.

Let us see how this works. We will be using a lambda-calculator
written in Haskell:
	http://pobox.com/~oleg/ftp/Haskell/Lambda_calc.lhs
We assume that the above file is downloaded into the current
directory, under the name Lambda_calc.lhs . We also need the
definitions of basic lambda-calculus terms:
	http://pobox.com/~oleg/ftp/Haskell/LC_basic.lhs
In addition, we need a file
	http://pobox.com/~oleg/ftp/Haskell/LC_Pnum.lhs
that defines a symmetric difference of two Church numerals. We need
the latter for a term that compares two Church numerals for equality.
The symmetric difference function and the equality predicate run in
_linear_ time, with respect to the magnitude of the largest numeral in
question. This linearity property is the consequence of using
P-numerals internally. The latter permit zero checking, successor and
_predecessor_ operations in constant time (given the normal order of
evaluation).

This message is a literate Haskell script. It could be executed by
loading it into Hugs (again, providing that the current directory
contains files Lambda_calc.lhs, LC_basic.lhs, and LC_Pnum.lhs).

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
> import LC_Pnum(diffs)  -- import symmetric difference term

Note that x ^ t denotes (\x . t) and x # y stands for an application
of x to y. As we said earlier, true stands for \x\y.x and false stands
for \x\y.y. We can see that by asking the calculator (Hugs, actually)
to show these terms:

	Main> print true
	(\x. (\y. x)) 
	Main> print false
	(\x. (\y. y)) 
	Main> print lif  -- 'if' in lambda-calculus
	(\p. (\x. (\y. p x y)))

Let us first define variables with mnemonic names

> [ci,cj] =
>    map make_var ["ci","cj"]

The symmetric difference of two Church numerals is defined in the
module LC_Pnum.  We can use the difference combinator to derive the
equality predicate for two Church numerals:

> ceq = ci ^ cj ^ zerop # (diffs # ci # cj)

Let us test the equality predicate:
	Main> eval $ ceq # c0 # c0
	(\x. (\y. x))  -- which is true
	Main> eval $ ceq # c0 # c1
	(\x. (\y. y))  -- which is false
	Main> eval $ ceq # c1 # c0
	(\x. (\y. y))  -- which is false again
	Main> eval $ ceq # c2 # c2
	(\x. (\y. x))  -- which is true

Now we can define the bluff combinator:

> bluff = f ^ x ^ true

and the beq combinator:

> beq = a ^ b ^ 
>        lif # (bluffp # a)
>           -- a is the bluff combinator
>         # (not # (bluffp # b)) -- false if b is bluff, true otherwise
>          -- a is not bluffing: it's truly a Church numeral
>         # (lif # (bluffp # b)
>            # true                -- 'b' is a bluff, but 'a' isn't
>            # (ceq # a # b)       -- both a and b are Church numerals
>        )
>  where
>    bluffp = c ^ (c # (x ^ false) # false)

To assure the reader that the above is a term in pure lambda-calculus, we
will print it out: 
	Main> putStr $ show_term beq 100

(\a. (\b. (\p. (\x. (\y. p x y))) ((\c. c (\x. (\x. (\y. y)))
(\x. (\y. y))) a) ((\p. p (\x. (\y. y)) (\x. (\y. x))) ((\c. c
(\x. (\x. (\y. y))) (\x. (\y. y))) b)) ((\p. (\x. (\y. p x y)))
((\c. c (\x. (\x. (\y. y))) (\x. (\y. y))) b) (\x.  (\y. x))
((\ci. (\cj. (\c. c ((\p. (\q. p q (\x. (\y. y)))) (\x. (\y. y))) (\x.
(\y. x))) ((\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))))) ci cj))) a
b))))

The argument 100 of show_term is the maximal depth of the term to print.

We can now test that the 'beq' and 'bluff' combinator solve the problem:

	Main> eval $ beq # c0 # c0
	(\x. (\y. x)) -- which is true
	Main> eval $ beq # c0 # c1
	(\x. (\y. y)) -- which is false
	Main> eval $ beq # c1 # c1
	(\x. (\y. x)) -- which is true
	Main> eval $ beq # c1 # bluff
	(\x. (\y. x)) -- which is true
	Main> eval $ beq # c0 # bluff
	(\x. (\y. x)) -- which is true
	Main> eval $ beq # bluff # c1
	(\x. (\y. x)) -- which is true
	Main> eval $ beq # bluff # bluff
	(\x. (\y. y)) -- which is false