From posting-system@google.com Tue May 29 21:16:13 2001
Date: Tue, 29 May 2001 20:58:02 -0700
Reply-To: oleg@pobox.com
From: oleg@pobox.com (oleg@pobox.com)
Newsgroups: comp.lang.functional
Subject: Subtraction, division, logarithms and other opposites in Lambda calculus
References: <200105132316.QAA85122@adric.cs.nps.navy.mil>
Message-ID: <7eb8ac3e.0105291958.7b79567d@posting.google.com>
Status: OR
Peter Hancock kindly wrote in message news:...
> 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.