From oleg@pobox.com Sun May 13 16:17:00 2001 Newsgroups: comp.lang.functional Date-Sent: Sun, 13 May 2001 16:16:58 -0700 (PDT) Date: Sun, 13 May 2001 23:12:25 +0000 (UTC) From: oleg@pobox.com Message-Id: <200105132316.QAA85122@adric.cs.nps.navy.mil> To: comp.lang.functional@mailgate.org Subject: Negativism and division in lambda-calculus Summary: Subtraction, division, and negative numbers in lambda-calculus Keywords: lambda calculus, arithmetics, negative numbers, division Reply-to: oleg@pobox.com Status: OR This article will demonstrate basic arithmetic operations -- comparison, addition, subtraction, multiplication, and division -- on non-negative and negative integer numbers. Both the integers and the operations on them are represented as terms in the pure untyped lambda-calculus. The only building blocks are identifiers, abstractions and applications. No constants or delta-rules are used. Reductions follow only the familiar beta-substitution and eta-rules. All examples run on a lambda-calculator, which you can use as a regular calculator. Granted, a pocket TI is more practical, especially for big numbers. On the other hand, the lambda-calculator is more artful and insightful. Negative numbers in lambda-calculus seem perplexing. A natural number n has a remarkably intuitive representation: an iterator cn that applies a function n times. The next natural number, (succ cn), applies the function one more time. A predecessor of cn then applies a function one less time. How to _unapply_ a function however? And what is the meaning of the predecessor of zero? This article will demonstrate two ad hoc and two systematic ways of implementing a predecessor. The systematic approaches introduce negative numbers. One of the techniques is more theoretical; the other leads to rather practical operations on arbitrary integers. That approach permits a straightforward definition of subtraction and division of two numerals. Curiously, none of the arithmetic operations involve the Y combinator; even the division gets by without Y. All the examples below are given in the notation of a practical lambda-calculator [1]. It is a normal-order interpreter for the untyped lambda-calculus. The interpret permits "shortcuts" of terms. The shortcuts are not first class and do not alter the semantics of the lambda-calculus. Yet they make complex terms easier to define and apply. We start by defining the successor and a few Church numerals (X Define %I (L x x)) ; The I combinator (X Define %c0 (L f (L x x))) (X Define %succ (L c (L f (L x (f (c f x)))))) (X Define* %c1 (%succ %c0)) (X Define* %c2 (%succ %c1)) these and other well-known terms can be found in [2]. The Define command introduces a new shortcut. A '*' is a mark of strictness: Define* first reduces its second argument to the normal form before associating it with a shortcut. This saves reductions in further applications. We can always see a term behind a shorthand. For example, (X expand-shortcuts %c2) prints (L f (L x (f (f x)))), the expected result. We will search for a predecessor of a positive numeral cn as an application of cn itself to a particularly chosen function f and a value v: (predp cn) ==defined-as== cn f v We define f so that (f z) will effectively act as if z == v then c0 else (succ z) We know that z can be either a numeral cn or a special value v. All Church numerals have a property that (cn I) is I: the identity combinator is a fixpoint of every numeral. Therefore, ((cn I) (succ cn)) reduces to (succ cn). We only need to choose the value v in such a way that ((v I) (succ v)) yields c0. Here's the complete solution: (X Define* %predp (L c (c (L z (z %I (%succ z))) ; function f(z) (L a (L x %c0))))) ; value v To see if this definition of the predecessor really works, we ask the calculator to evaluate (%predp %c1) ;==> %c0 (%predp %c3) ;==> (L f (L x (f (f x)))) The answers are the Church numerals c0 and c2 correspondingly. We can see that for ourselves; Furthermore, we can ask the calculator if two terms are equivalent, that is, if they have the same normal form (modulo alpha conversion): (X equal?* (%predp %c1) %c0) (X equal?* (%predp %c3) %c2) Both commands print the expected value #t. File lambda-arithm-neg.scm [3] considers another ad-hoc way of defining a predecessor, and the first systematic way. The latter starts by introducing -1 as a fixed point of a term (L b (%succ (%add b b))). Indeed, the equation b + b + 1 = b has the solution -1. We skip these approaches for brevity and turn instead to a practical way of defining integer numbers and the complete set of operations on them. Recall that a Church numeral cn has a type N, in Haskell terms, type N a = (a->a)->a->a We define an Integer number 'in' as a value of type Z: type Z a = Sign a -> N a type Sign a = a->a The integer 'in' is an abstraction over natural numbers: in sign ==> cn, for non-negative integers in sign ==> sign . cn, for negative integers Thus 'in' is a sign-bit abstraction over natural numbers. (X Define* %i0 (L sign %c0)) ; A zero integer (X Define* %i1 (L sign %c1)) ; An integer +1 (X Define* %i-1 (L sign (L f (L x (sign (f x)))))) ; -1 We introduce (X Define* %c->i (L c (L sign c))) ; N a -> Z a (X Define* %abs (L i (i %I))) ; Z a -> N a The latter definition relies on the fact that passing the identity as a sign-term effectively gets rid of the sign. A more complex function is a sign-case. It takes an integer and three terms and returns one of them depending on the sign of the number. (X Define* %sign-case (L i (L on-positive (L on-zero (L on-negative (i (L _ on-negative) (L _ on-positive) on-zero)))))) The branching is an application of the integer to three suitably-chosen terms. The underscore symbol '_' in the above term is a regular, undistinguished identifier. We can now introduce the first inequality predicate, negative? (X Define* %negative? (L i (%sign-case i %false %false %true))) and the negation functions: ; Given a non-zero natural number, turn it into a negative integer (X Define* %c-negate (L m (L sign (L f (L x (sign (m f x))))))) ; Z a -> Z a (X Define* %i-negate (L i (%sign-case i (%c-negate (%abs i)) %i0 (%c->i (%abs i))))) Incidentally, Haskell can't type the above function, unfortunately. An attempt to do so in Hugs however gives a rather spectacular error message. We are now equipped to define arithmetic functions on integers. We start with an incrementor: ; Z a -> Z a ; The successor of an integer number a (X Define* %i-succ (L a (%sign-case a ; if the number is positive (%c->i (%succ (%abs a))) ; if the number is zero %i1 ; if the number is negative (%i-negate (%c->i (%predp (%abs a))))))) and an addition function ; Z a -> Z a -> Z a ; Addition of two integer numbers, a and b (X Define* %i-add (L a (L b (%sign-case a ; a > 0 (%sign-case b ; b > 0 (%c->i (%add (%abs a) (%abs b))) ; b = 0 a ; b < 0: increment b a times ((%abs a) %i-succ b) ) ; a = 0 b ; a < 0 (%sign-case b ; b > 0: increment a b times ((%abs b) %i-succ a) ; b = 0 a ; b < 0 (%c-negate (%add (%abs a) (%abs b)))) )))) For example, to add -2 to +1, we write evaluate (%i-add (%c-negate %c2) %i1) and obtain (L sign (L f (L x (sign (f x))))), which is %i-1. Skeptics may claim that the above definition looks like Scheme and has little to do with the pure lambda calculus. To answer we will ask the calculator to reveal the normal form behind the %i-add term. (X expand-shortcuts %i-add) yields: (L a (L b (((a (L _ (((b (L _ (L sign (L f (L x (sign (((a (L x x)) f) (((b (L x x)) f) x)))))))) (L _ (((b (L x x)) (L a (((a (L _ (((((a (L x x)) (L z ((z (L x x)) (L f (L x (f ((z f) x))))))) (L g73 (L x (L f (L x x))))) (L _ (L sign (L f (L x (sign (((((a (L x x)) (L z ((z (L x x)) (L f (L x (f ((z f) x))))))) (L g74 (L x (L f (L x x))))) f) x))))))) (L sign (L f (L x x)))))) (L _ (L sign (L f (L x (f (((a (L x x)) f) x))))))) (L sign (L f f))))) a))) a))) (L _ (((b (L _ (((a (L x x)) (L a (((a (L _ (((((a (L x x)) (L z ((z (L x x)) (L f (L x (f ((z f) x))))))) (L g73 (L x (L f (L x x))))) (L _ (L sign (L f (L x (sign (((((a (L x x)) (L z ((z (L x x)) (L f (L x (f ((z f) x))))))) (L g74 (L x (L f (L x x))))) f) x))))))) (L sign (L f (L x x)))))) (L _ (L sign (L f (L x (f (((a (L x x)) f) x))))))) (L sign (L f f))))) b))) (L _ (L sign (L f (L x (((a (L x x)) f) (((b (L x x)) f) x))))))) a))) b))) As you see, this is a genuine lambda term, composed of only identifiers, abstractions and applications. It makes for a good T-shirt or a wallpaper pattern. It may be useful to meditate against before going to sleep. Subtraction of two integers is rather trivial: (X Define* %i-sub (L a (L b (%i-add a (%i-negate b))))) Multiplication of two integers isn't too complex either: (X Define* %i-mul (L a (L b ( ; determine the sign of the result (%sign-case a ; a > 0 (%sign-case b (L x (L n x)) (L _ %i0) (L x (%c-negate x))) ; a = 0 (L _ %i0) ; a < 0 (%sign-case b (L x (%c-negate x)) (L _ %i0) (L x (L n x)))) (%mul (%abs a) (%abs b)))))) To multiply -2 by +3, you evaluate (%i-mul (%c-negate %c2) (%i-add %i1 (%i-add %i1 %i1))) and obtain (L sign (L f (L x (sign (f (f (f (f (f (f x)))))))))) which is -6. Division is slightly more involved. As in the case of multiplication, we analyze the signs of the operands, determine the sign of the result and then do division of two positive numbers. The algorithm is classical: keep subtracting the divisor from the dividend until the result becomes less than the divisor. Count the number of subtractions performed. The final count is the quotient. In Haskell terms, mydiv dividend divisor = if dividend < divisor then 0 else 1 + (mydiv (dividend - divisor) divisor) This algorithm is behind the arithmetics of types [4]. However it relies on recursion, which we would like to avoid. It is easy to see that, given positive divisor and dividend, we need to do at most dividend subtractions. We can do exactly dividend iterations if we keep a flag that tells us that we have done enough subtractions already. To be slightly more formal: mydiv dividend divisor = let div_iter (current, flag, accumulator) = if flag || (current < divisor) then (current, True, accumulator) -- enough subtractions else (current-divisor, False, 1+accumulator) -- continue in case ntimes dividend div_iter (dividend,False,0) of (_,_,accum) -> accum where ntimes n = -- Church Numeral n case n of 0 -> (\f seed -> seed) n -> (\f seed -> ntimes (n-1) f (f seed)) The lambda-term that performs division of two arbitrary integer numbers is as follows: (X Define* %i-div (L a (L b ( ; determine the sign of the result (%sign-case a ; a > 0 (%sign-case b (L x (%c->i x)) (L _ %true) (L x (%c-negate x))) ; a = 0 (L _ %i0) ; a < 0 (%sign-case b (L x (%c-negate x)) (L _ %true) (L x (%c->i x)))) ; now divide x by y, where x and y are two positive integers ((L x (L y (%cdr (%cdr (x ; the dividend drives the iteration %I (L u ((L current (L flag (L accum (%if flag u ; we're done ((L diff ; current - y (%sign-case diff ; diff > 0 (%cons diff (%cons %false (%succ accum))) ; diff = 0 (%cons diff (%cons %true (%succ accum))) ; diff < 0 (%cons diff (%cons %true accum)))) (%i-sub current y)))))) (%car u) (%car (%cdr u)) (%cdr (%cdr u)))) (%cons x (%cons %false %c0))))))) (%c->i (%abs a)) (%c->i (%abs b))))))) Pairs and pair-selectors -- %cons, %car, %cdr -- have the usual definitions [2]. We had to decide what to make of a division by zero. We could set it to be anything we want -- or nothing at all (no normal form). We chose however to make x/0 return true. For one thing, true is not a numeral; for another, true is the opposite of false. In lambda calculus, as in C and Perl, false and 0 are synonymous. A few examples of division: ; 2/3 => (L sign %c0), i.e., integer 0 (%i-div (%c->i %c2) (%c->i %c3)) ; -3/-2 ==> (L sign (L f f)), i.e, +1 (%i-div (%i-add %i-1 (%i-add %i-1 %i-1)) (%i-add %i-1 %i-1)) ; 5/2 ==> (L sign (L f (L x (f (f x))))), i.e, 2 (%i-div (%i-succ (%i-mul (%i-add %i1 %i1) (%i-add %i1 %i1))) (%i-add %i1 %i1)) They require a great number of reductions. Markedly unlike the real life, breaking terms in lambda-calculus is far harder than building them. We have shown how to implement the four operations of arithmetics on integer numbers -- using only beta and eta reductions of terms composed exclusively of variables, abstractions and applications. You can really do your taxes in lambda calculus. The IRS however would be no keener seeing a lambda-term representing the amount you owe than getting that amount in pennies. A forthcoming article will discuss an inductive combinator (aka fold), the Ackerman function and the implementation of a factorial function without a fixpoint combinator. I'd like to finish the article with another beautiful wall-paper pattern: an unadorned lambda-term that implements division of two integers. It is the result of executing "(X expand-shortcuts %i-div)". The rules of netiquette however prevent me from doing this: the term is a tad long. I include therefore only the reference to the term: http://pobox.com/~oleg/ftp/Computation/lambda-arithm-div-term.scm You can put the pattern on a wallpaper or a T-shirt. The latter can demonstrate that division is merely a rearrangement of pieces of cloth connected by strings (you have to appropriately shred the T-shirt, of course). The rules of rearrangement (beta and eta) are simple enough; one can probably teach a bird to do that. References [1] A practical Lambda-calculator http://pobox.com/~oleg/ftp/Scheme/index.html#lambda-calc [2] Basic lambda terms http://pobox.com/~oleg/ftp/Scheme/lambda-arithm-basic.scm [3] Negative numbers and four arithmetic operations on integers http://pobox.com/~oleg/ftp/Computation/lambda-arithm-neg.scm [4] Type Arithmetics. Computation based on the theory of types http://pobox.com/~oleg/ftp/Computation/type-arithmetics.html