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.