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 »**