Negativism and division in lambda-calculus 
Author Message
 Negativism and division in lambda-calculus

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 =
...

read more »



Fri, 31 Oct 2003 07:12:25 GMT  
 Negativism and division in lambda-calculus
Wow.

I'd wondered whether there are any semi-sensible definitions of
subtraction, division, and logarithms in lambda-calculus. (I was
struck by the fact that the combinators for +, *, ^ and 0 are
combinatorially complete, and (wrt eta equality) satisfy some nice
algebraic properties that suggest looking for their "opposites".

Another idea might be to make some "Church" version of
Conway's games or surreal numbers.

Thanks for posting that!

Peter



Wed, 12 Nov 2003 09:38:07 GMT  
 Negativism and division in lambda-calculus

Quote:

>I'd wondered whether there are any semi-sensible definitions of
>subtraction, division, and logarithms in lambda-calculus. (I was
>struck by the fact that the combinators for +, *, ^ and 0 are
>combinatorially complete, and (wrt eta equality) satisfy some nice
>algebraic properties that suggest looking for their "opposites".

You can, of course, define subtraction, division etc. on
church-numerals, but they are quite cumbersome. Besides,
church-numbers aren't very efficient as they unary. You can define
binary (or higher bases) numbers in the lambda calculus to obtain
better efficiency (addition in time proportional to the number of bits
in a number etc.). This complicates the definition of the basic
arithmetical operators, though.




Fri, 14 Nov 2003 16:57:38 GMT  
 Negativism and division in lambda-calculus

    Torben> You can, of course, define subtraction, division etc. on
    Torben> church-numerals, but they are quite cumbersome. Besides,
    Torben> church-numbers aren't very efficient as they unary.

I've looked at these operations on Church ordinals(*); my experience
there is that the "real" (and fastest) operation is binary: it is
\(a,b)->a + w^b. (For finite ordinals, \(a,b)->a + 2^b, which was
essentially discovered by Archimedes, then explicitly by Cantor,
though computer scientists attribute it to Knuth!)  It is fascinating
to define the arithmetic operations by recursion on binary trees/notations.

(*) I mean the data type O = Zero | Succ O | Lim (Nat -> O),
    with +, * and ^ commuting with limits in their second argument.

My interest in subtraction, division etc isn't in the least practical!
It's just that it's natural to look for something (infinite)
satisfying the axioms of a field.  (Or even fields with exponentiation
and logarithms.)

Peter



Fri, 14 Nov 2003 17:29:09 GMT  
 Negativism and division in lambda-calculus

Quote:
> I was struck by the fact that the combinators for +, *, ^ and 0 are
> combinatorially complete, and (wrt eta equality) satisfy some nice
> algebraic properties that suggest looking for their "opposites".

It appears we can always introduce the "opposites" by cheating:

-- given a Church numeral cn, define -cn as the least fixpoint of a
   term \x.(x+x+a)
-- given two Church numerals cn and cm, define cn/cm as the least
   fixpoint of a term \x.(cm*x + (-cn) + x)
-- given a Church numeral cn, define sqrt(cn) as the least fixpoint of
   a term \x.((x*x+cn)/c2/x) (the Newton method)
-- given two Church numerals cn and cm, define log(cn,cm) (base cm)
   as the least fixpoint of a term \x.(cm^x - cn + x)

If the required fixpoint does not exist, the corresponding lambda term
will have no normal form and will thus "evaluate" to the "bottom".

As many such terms involving the Y combinator, these expressions are
not very practical. Less aspiring and more down-to-earth algorithms
seem to work better:

-- define cn - cm by counting how many times we can apply succ to cm
   so that the result will be no less than cn
-- define (quotient cn cm) by counting how many times we can
   add cm to c0 so that the result reaches or exceeds cn
-- define the discrete log of cn base cm by counting how many times we
   can multiply c1 by cm so that the result reaches or exceeds cn

These are basically the algorithms behind the previous article. They
exhibit some kind of duality to the fixpoint versions...

The latter group of algorithms depends on the ability to compare two
Church numerals, which can be easily accomplished. To see if numeral a
is greater than numeral b we apply a stopping-at-zero predecessor to a, b
times. If the result is non-zero, a is indeed larger than b. A faster
and a more memory efficient algorithm is to have numeral 'a' build a
list and then get numeral 'b' to destroy it, cell by cell. If there is
something left, 'a' is greater than 'b'.

In the notation of the Lambda calculator,

; Numeral a will be building a list
; (%cons %true (%cons %true .... (cons %false %false)))
; where there are as many %true terms as there is the cardinality of a

(X Define* %greater?
   (L a (L b
      ; Checking if anything is left of the list: if the current
      ; cell is nil
     (%car
      (b
       ; deconstructing the list. Once we hit the nil, we stop
       (L z (%if (%car z) (%cdr z) z))
       ; Building the list
       (a
        (L z (%cons %true z))
        (%cons %false %false)) ; Initial cell, the nil
)))))

Where %cons, %car and %cdr are defined as usual in the Lambda calculus:
        (X Define %true (L x (L y x)))
        (X Define %false (L x (L y y)))
        (X Define %cons (L x (L y (L p (p x y)))))
        (X Define %car (L p (p %true)))
        (X Define %cdr (L p (p %false)))

To verify:
(%greater? %c1 %c0) ;==> %true
(%greater? %c0 %c0) ;==> %false
(%greater? %c2 %c3) ;==> %false
(%greater? %c3 %c1) ;==> %true

Indeed, the calculator types %true or %false as the result of the
evaluations, which is kind of nice. Here's the comparison function
%greater? without any embellishments, as a combination of only
variables, abstractions and applications:

(L a (L b
  (((b (L z (((z (L x (L y x))) (z (L x (L y y)))) z)))
     ((a (L y (L p ((p (L x (L y x))) y))))
      (L p ((p (L x (L y y))) (L x (L y y))))))
   (L x (L y x)))))

Thank you.



Sun, 16 Nov 2003 11:58:01 GMT  
 
 [ 6 post ] 

 Relevant Pages 

1. Lambda Calculus Question

2. lambda calculus implementation

3. Introduction to lambda calculus ?

4. Lambda Calculus Problem!

5. Lambda calculus + Church numerals

6. Typed lambda calculus, recursion and halting

7. lambda calculus: delta rules

8. Need help on Lambda calculus reduction please.

9. Q: reduction strategies in lambda calculus

10. Lambda-Calculus

11. Introduction to Lambda Calculus

12. Typed Lambda calculus

 

 
Powered by phpBB® Forum Software