Yesterday I posted a question about Church numeral and received lots of
answers from many friends. Thank you all.
My question is:
Suppose lambda=\
0'=\f.\x.x
1'=\f.\x.f x
2'=\f.\x.f (f x)
...
n'=\f.\x.f^n x
(0',1',2'.....n' are so called Church numerals)
How to define mult,which multiplies m' and n', and expt, which raises m'
to the power n'?
(1) A good algorithm from John Lamping:
>One way that I find useful for thinking about Church numerals is as
>iteration forms. That is, (n f x) is equivalent to:
>
>temp := x
>for i = 1 to n
> temp := f(temp)
>endfor
>return temp
>
>So if you can write a computation in terms of those kinds of iterations,
>then you can translate that to operations with Church numerals.
>
>For example, a+b can be computed by
>
>temp := a
>for i = 1 to b
> temp := temp + 1
>endfor
>return temp
>
>Now, reconizing that temp, a, and the answer are Church numerals, halfway
>translate this to the lambda calculus:
>
>lambda f. lambda x.
>temp := (a f x)
>for i = 1 to b
> temp := (f temp)
>end for
>
>Now, translate the inner loop based on b's being a Church numberal:
>
>lambda f. lambda x.
>(b f (a f x))
>
>and finally put lambdas for the free variables (which I probably should
>have done at the start:
>
>lambda a. lambda b. lambda f. lambda x. (b f (a f x))
>
Then,
mult=\m.\n.\f.\x. m (n f) x
expt=\m.\n.\f.\x. n (m f) x
But I think it goes wrong when m=zero, and <··@cs.st-andrews.ac.uk> mail
me to agree my idea.
>Yes: If ci is the ith Church numeral, c0cn = I . A special case. See
>Barendregt's book (revised edn.) p149, Ex 6.8.6
I also implement mult and exp function in ML language to test :
val zero=fn f=>( fn x=>x );
val one=fn f=>( fn x=>f(x) );
val two=fn f=>( fn x=>f(f(x)) );
val three=fn f=>( fn x=>f(f(f(x))) );
val four=fn f=>( fn x=>f(f(f(f(x)))) );
val five=fn f=>( fn x=>f(f(f(f(f(x))))) );
fun plus1(n)=fn f=>(fn x=>f(n(f)(x)));
fun plus(m,n)=fn f=>(fn x=> m f (n f x));
fun mult(m,n)=fn f=>(fn x=> m (n f) x);
fun exp(m,n)=fn f=>(fn x=> n (m f) x);
The result is:
- mult(zero,one);
val it = fn : ('a -> 'b) -> 'c -> 'c
(* when m=zero the result is not zero *)
- mult(one,zero);
val it = fn : 'a -> 'b -> 'b
(* when n=zero the result is zero *)
- mult(two,one);
val it = fn : ('a -> 'a) -> 'a -> 'a
(* the result is two *)
- exp(zero,one);
val it = fn : 'a -> 'b -> 'b
(* the result is zero *)
- exp(zero,zero);
val it = fn : 'a -> 'b -> 'b
(* the result is zero *)
- exp(one,zero);
val it = fn : ('a -> 'b) -> 'c -> 'c
(* the result is not one *)
BUT the mult and exp function do good and are very clear in lambda expression.
If we don't care the special case, they are good examples to see how
lambda calculua works.
(2) Scheme implementation on Church numerals from Mr. Taj Khattra:
( The definition below I have not tested yet, but there should be no
error. )
>;; Here's a few defns I've translated (almost) verbatim into Scheme from
>;;
>;; Gordon, M.J.C, _Programming Language Theory and its Implementation_,
>;; (Prentice Hall International series in computer science),
>;; New York, Prentice Hall, 1988.
>;;
>;; Read chaps 4 and 5 for an explanation of what's going on below.
>
>
>
>;; NOTE
>;; we use builtin false/true/if/cond, but these could be defined
>;; in the lambda-calculus as well
>
>;;
>;; NUMBERS
>;;
>
>(define zero
> (lambda (f x) x))
>
>(define one
> (lambda (f x) (f x)))
>
>(define two
> (lambda (f x) (f (f x))))
>
>;; etc etc
>
>
>;;
>;; HELPERS
>;;
>
>;; successor
>(define suc
> (lambda (n)
> (lambda (f x) (n f (f x)))))
>
>
>
>(define iszero
> (lambda (n)
> (n (lambda (x) false) true)))
>
>(define prefn
>
> (lambda (f)
> (lambda (p)
> (cons false
> (if (car p) (cdr p) (f (cdr p)))))))
>
>;; predecessor
>(define pre
> (lambda (n)
> (lambda (f x) (cdr (n (prefn f) (cons true x))))))
>
>
>;;
>;; THE MIGHTY Y
>;;
>
>(define Y
> (lambda (g)
> ((lambda (f) (g (lambda (x y) ((f f) x y))))
> (lambda (f) (g (lambda (x y) ((f f) x y)))))))
>
>
>;;
>;; ARITHMETIC FNS
>;;
>
>;; addition
>(define add
> (lambda (m n)
> (lambda (f x) (m f (n f x)))))
>
>;; multiplication
>(define mult
> (Y (lambda (f)
> (lambda (m n)
> (if (iszero m) zero (add n (f (pre m) n)))))))
>
>;; our eq function for numbers
>(define *eq*
> (Y (lambda (eq)
> (lambda (m n)
> (cond ((iszero m) (iszero n))
> ((iszero n) false)
> (t (eq (pre m) (pre n))))))))
>
> (define expt
> (Y (lambda (f)
> (lambda (m n)
> (if (iszero n) one (mult m (f m (pre n))))))))
>
>where we define (expt zero zero) = one
>
>If you want to define (expt zero zero) = zero then use
>
> (define expt
> (Y (lambda (f)
> (lambda (m n)
> (cond ((iszero m) zero)
> ((iszero n) one)
> (t (mult m (f m (pre n)))))))))
>
>
--
Dept. of CS of UNT
····@cs.unt.edu
····@sol.acs.unt.edu