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