Notes on Church Numerals ---------------------------------------------------------------------- From: Jesse Subject: Summary on Church numeral Message-ID: Organization: Computer Science Dept .of UNT Date: Wed, 12 Aug 1992 04:43:57 GMT Lines: 231 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 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 cyen@cs.unt.edu jh33@sol.acs.unt.edu ---------------------------------------------------------------------- From: blume@news@informatik.hu-berlin.de (Matthias Blume) Subject: Re: Summary on Church numeral Message-ID: Organization: Humbolt University, Department of Computer Science Date: Wed, 12 Aug 1992 10:57:31 GMT Lines: 89 Hi, after returning from vacation I saw the Church-numeral-questions and the many responses, but I'm not happy with them. I didn't find any hint about the fact, that EVERY computable arithmetic function can be represented by a lambda-expression, operating on Church-Numerals. [Read ``->'' as ``can be represented as''] The fact, that add -> \a\b\f\x (b f (a f x)) mult -> \a\b\f\x (b (a f) x) and pow -> \a\b\f\x (b a f x) must be considered a conincidence. If you're trying to understand WHY EVERY computable function might be represented, you should have a closer look at the problem. I don't want to give a proof (this includes reasoning about confluency etc.), but I want to give you an idea, how things work: We show, that every mu-recursive function can be represented as \-expression: 1. 0 -> 0' = \f\xx 2. succ -> SUCC = \a\f\x (f (a f x)) 3. c[m,n](x1,...,xn) = xm ; c[m,n] -> \x1...\xn xm 4. h(x1,...xn) = f (g1 (x1,...,xn), ..., gm (x1,...,xn)) if f -> f' and gi -> gi', then h -> h' = \x1...\xn (f' (g1' x1 ... xn) (gm' x1 ... xm)) if(c,t,e) = e, iff c = 0 if(c,t,e) = t, otherwise if -> IF = \c\t\e (c \it e) [If the condition c is the Church-numeral 0', then (c \it) becomes \xx, which is the identity function yielding e, otherwise (c \it) becomes a constant function yielding t, no matter what argument given] pseudo-numerals: -1* -> (Z 0' 1') 0* -> (Z 0' 0') 1* -> (Z 1' 0') 2* -> (Z 2' 0') ... n* -> (Z n' 0') ... where Z = \a\b\s (IF s a b) [Z is much like cons in Lisp, 'cause it constructs something from two parts while the parts remain easily accessible (by applying the thing to 0' or 1')] S = \z (IF (z 0') 0* (Z (SUCC (z 1')) 0')) pred -> PRED = \n (n S -1* 1') [We compute the predecessor of a Church-Numeral n' by computing n-times the successor of -1; therefore we need a number representation, which includes -1; our pseudo-numerals serve for this purpose] 5. h (0, x1, ... xn) = g (x1, ..., xn) h (n', x1, ..., xn) = f (h (n, x1, ..., xn), n, x1, ..., xn) if g -> g' and f-> f', then hh = \h\n\x1...\xn (IF n (f' (h h (PRED n) x1 ... xn) (PRED n) x1 ... xn) (g' x1 ... xn)) h -> (hh hh) 6. h (x1, ..., xn) = %y g(y, x1, ..., xn) = 0 [the least y, where g(y, x1, ..., xn) gives zero] if g -> g', then hh = \h\y\x1...\xn (IF (g' y x1 ... xn) (h h (SUCC y) x1 ... xn) y) h -> (hh hh 0') [5. and 6. make use of a trick: here we apply hh to itself to obtain recursion without the need of syntactic recursion (this is what the magic Y does)] Please, don't flame at me, if I made some typo, 'cause the're so many lambdas etc. -- -- m.b Matthias Blume, blume@informatik.hu-berlin.de, Humboldt-Uni zu Berlin, FB 16 (Informatik), [Dept. of Computer Science] ---------------------------------------------------------------------- From: Mayer Goldberg Subject: church numerals ... Message-ID: <1992Aug12.201701.18392@news.cs.indiana.edu> Organization: Computer Science, Indiana University Date: Wed, 12 Aug 1992 20:16:55 -0500 Lines: 91 Here are my 2 cents worth of church numeral stuff: It would really be neat if we had a successor and a zero. If we did, we could say the following (in either LC or Scheme): Let z be our zero combinator; let s be our successor combinator: zero == z one == (s z) two == (s (s z)) etc. But unfortunately we con't have s and z in any obvious way, and so we abstract over the two, defining our numerals as follows: zero == \sz.z one == \sz.(s z) == \x.x two == \sz.(s (s z)) etc. We want a successor. If we had a successor "add1" combinator, we could have: (add1 five) -> six. and in general (add1 'n') -> 'n+1', where 'n' is our church numeral representation for n, and 'n+1' is our church numeral rep for n+1, both quasi-quoted. If we had s and z, all we'd need is one more application of s: (s ('n' s z)) or the less obvious: ('n' s (s z)) where 'n' is the rep for our n'th church numeral. But we don't have s and z and so we abstract them out, getting: 'n+1' == \sz.(s ('n' s z)) or the less obvious: 'n+1' == \sz.('n' s (s z)) By abstracting over 'n' we can define add1 as follows: add1_version1 == \nsn.(s (n s z)) or the less obvious: add1_version2 == \nsz.(n s (s z)). We'll use version1 here because it's the easiest to prove things about. A church numeral is an abstraction over the n'th composition of a function, hence for some function f: ('n' f) -> f^n (right-associated). This means that for example (three add1) is just: \x.(add1 (add1 (add1 x))) So so we clearly have: ('n' add1 'm') -> 'n+m'. Remeber that in LC and CL we auto-left-associate, and so (a b c) is really ((a b) c) ... side note ... So we get addition by abstracting over 'n' and 'm': add == \nm.(n add1 m) where add1 is just a placeholder for the text of the add1 combinator, and a simple substitution can take place, yielding a formal mess. (add five) is the procedure which adds 5 to anything ... (four (add five)) is thus: \x.(add5 (add5 (add5 (add5 x)))). If we apply it to zero we get twenty. In general: ('n' (add 'm') zero) -> 'n*m' so we abstract over 'n' and 'm' getting: mul == \nm.(n (add m) zero) (mul three) is the procedure which multiplies something by three ... (two (mul three)) is thus: \x.(mul3 (mul3 x)). If we apply this to one we get 3^2 -> 9. In general: ('m' (mul 'n')) -> 'n^m' We abstract over 'n' and 'm' and thus get exponentiation: exp == \nm.(m (mul n) one) This can go on all the way to ackerman and above. Ackermann is gotten through exponentiating the lambda expression taking the super-n-exponent and returning the super-n+1-exponent and applying it to exponentiation ... :) Another interesting point is that exponentiation on church numerals is just \nm.(m n) or if you are willing to cope with a change of order in the arguments, it's just the identity \x.x. This is so because composition and exponentiation are governed by a similar algebraic structure. Church numerals are a lot of fun! Mayer. ---------------------------------------------------------------------- From: stone@hilbert.math.grin.EDU (John David Stone) Subject: Church numerals Message-ID: <9208131348.AA08840@HILBERT.MATH.GRIN.EDU> Date: 13 Aug 92 13:48:34 GMT Lines: 114 Here's the classic approach to arithmetic with Church numerals: (define zero (lambda (x) (lambda (y) y))) (define successor (lambda (u) (lambda (x) (lambda (y) (x ((u x) y)))))) (define one (successor zero)) (define add (lambda (m) (lambda (n) (lambda (f) (lambda (x) ((m f) ((n f) x))))))) (define mult (lambda (m) (lambda (n) (lambda (f) (m (n f)))))) (define power (lambda (m) (lambda (n) (n m)))) And for direct definition of recursive functions (without Y, incidentally!): (define constant (lambda (x) (lambda (y) x))) (define ordered-pair (lambda (x) (lambda (y) (lambda (z) ((z (constant y)) x))))) The idea of the ordered-pair notation is that ((ordered-pair x) y) is a function that yields x when applied to zero and y when applied to any other Church numeral, thus giving the effect of a test for equality with zero. (define extender (lambda (y) (lambda (v) ((ordered-pair (successor (v zero))) ((y (v zero)) (v one)))))) You can think of extender as a function that takes a function y and an ordered pair v, where v's two elements are a counter and a previously generated value, and yields an ordered pair consisting of the counter incremented once and a value obtained by applying y to the old value of the counter and the previously generated value. (define recurser (lambda (x) (lambda (y) (lambda (u) (((u (extender y)) ((ordered-pair zero) x)) one))))) Recurser takes an initial value x, a transition function y, and a Church numeral u and delivers the result of applying the transition function to the initial value u times in succession. (Actually, you think of y as applying to two arguments to give its value -- the count of the number of times it's been applied previously, and the value resulting from those earlier applications.) Now recursive definitions simply fall out of applications of recurser: (define recursive-add (lambda (n) ((recurser n) (constant successor)))) (define recursive-multiply (lambda (n) ((recurser zero) (constant (recursive-add n))))) (define recursive-power (lambda (m) (lambda (n) (((recurser one) (constant (recursive-multiply m))) n)))) (define factorial ((recurser one) (lambda (x) (recursive-multiply (successor x))))) In testing these, you may find the following Scheme procedures useful: (define int->Church (lambda (n) (if (zero? n) zero (successor (int->Church (- n 1)))))) (define Church->int (lambda (numeral) ((numeral (lambda (x) (+ 1 x))) 0))) as in: (Church->int (factorial (int->Church 4))) (Church->int ((recursive-power (int->Church 5)) (int->Church 3))) which yield 24 and 125 respectively. I found the idea behind extender and recurser in Hindley and Seldin's _Introduction to Combinators and the Lambda-Calculus_, where it is ascribed to the logician P. Bernays. ------ John David Stone - Lecturer in Computer Science and Philosophy ----- -------------- Manager of the Mathematics Local-Area Network -------------- -------------- Grinnell College - Grinnell, Iowa 50112 - USA -------------- -------- stone@math.grin.edu - (515) 269-3181 - stone@grin1.bitnet --------