;; -*-mode: Outline;  -*-

  Subtraction, division, and negative numbers in lambda-calculus

This file introduces a representation for negative and positive
_integers_ in lambda-calculus. We define all four arithmetic
operations on integers as well as an ordered comparison of two
integers.  We also show two approaches of defining a predecessor of a
Church numeral. Curiously, none of the arithmetic operations involve
the Y combinator; even the division gets by without Y.

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.

     * Predecessor functions
     * Comparison of two Church numerals, a and b
     * Negative numbers and -1
        ** Introduction to negative integers
        ** Function c_to_i
        ** Function abs
     * Testing if an integer is positive or negative
        ** sign_case
        ** negativep, c_negate, i_negate
     * Integer successor
     * Integer addition
     * Integer Subtraction
     * Integer Multiplication
     * Integer Division
     * Running all validation tests

$Id: LC_neg.lhs,v 2.0 2003/01/01 23:55:25 oleg Exp oleg $

This is a literate Haskell code. We should first declare a module and
import the evaluator and the definitions for booleans, basic
combinators, Church numerals, addition, multiplication and
exponentiation.

> module LC_neg where
>
> import Lambda_calc
> import LC_basic
> import Prelude hiding ((^),and,or,not,succ,abs)
> import qualified Prelude (and)

------------------------------------------------------------------------

* Predecessor functions

A Church numeral 'cn' is an iterator. A natural number is represented
by the count of applying a function. A successor therefore is trivial:
it performs one more application, on the result of 'cn'. This line of
reasoning makes the definition of a predecessor hard: given cn, we
need to _unapply_ a function.

One ad hoc way of defining a predecessor of a positive numeral
		predp cn+1 ==> cn
is to represent "predp cn" as "cn f v"
where f and v are so chosen that (f z) acts 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 combI) is combI: the identity
combinator is a fixpoint of every numeral. Therefore, ((cn combI) (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.

> predp = eval $
>   c ^ c 
>	 # (z ^ (z # combI # (succ # z)))	-- function f(z)
>	 # (a ^ x ^ c0)			        -- value v

LC_neg> eval $ predp # c1 ;--> c0
LC_neg> eval $ predp # c3 ;--> c2

> test_predp 
>   = Prelude.and [ expectd (eval$ predp # c1) c0
>                 , expectd (eval$ predp # c3) c2
>                 ]


We can also define a predecessor in a more explicit variation of the
above approach. Recall that "predp cn f x" is to apply f to x (n-1)
times. Also recall that "cn g u" applies 'g' to 'u' (n) times. If the
function g can tell the first application from the others, we can
indeed apply f to x (n-1) times.  To this end, we choose the value 'u'
to be a pair, whose first element is a flag. Initially, the flag is
set to 'true'. The application (g u) returns a pair whose flag is set
to false. By this flag, the function 'g' can tell if it was applied to
'u' earlier.

pred1p = m^ f^ x^
  cdr # (m # (u^ lif # (car#u)
	       # (cons#false#x)
	       # (cons#false#(f#(cdr#u))) )
	   # (cons#true#false))


In the definition of pred1p above, the value 'u' should be more
properly set as (cons true term-M) rather than (cons true false). The
result of applying pred1p to any non-zero Church numeral does not
depend on the choice of term-M. It is only when pred1p is applied to
c0 that the meaning of term-M is revealed:
	(pred1p # c0) ;==> f^ x^ term-M

Therefore, term-M must be (-1 f x)!


* Comparison of two Church numerals, a and b

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

Numeral 'a' will be building a list
	(cons true (cons true .... (cons false false)))
where the number of true terms is equal to the cardinality of 'a'

> greaterp = eval $
>   a ^ 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
>        # (z ^ lif # (car # z) # (cdr # z) # z)
>        -- Building the list
>        # (a
>	   # (z ^ (cons # true # z))
>	   # (cons # false # false)) -- Initial cell, the nil
>      ))

LC_neg> eval $ greaterp # c1 # c0 --> true
LC_neg> eval $ greaterp # c0 # c0 --> false
LC_neg> eval $ greaterp # c2 # c3 --> false
LC_neg> eval $ greaterp # c3 # c1 --> true

> test_greaterp 
>   = Prelude.and [ expectd (eval$ greaterp # c1 # c0) true
>                 , expectd (eval$ greaterp # c0 # c0) false
>                 , expectd (eval$ greaterp # c2 # c3) false
>                 , expectd (eval$ greaterp # c3 # c1) true
>                 ]

------------------------------------------------------------------------
		
* Negative numbers and -1

** Introduction to negative integers

Note that none of operations below make any use of a fixpoint combinator.

We define integer numbers as a sign-bit abstraction over natural
numbers, Church numerals c_n:

Non-negative integers i_n are defined as
	sign_bit ^ c_n 
Negative integers i_minus_n are defined as
	sign_bit ^ f ^ x ^ sign_bit # (c_n # f # x)

A non-negative integer disregards the sign term; negative integers
apply the sign term to the result of a numeral

> sign = make_var "sign_bit"
> i = make_var "i"
> i0  = eval$ sign ^ c0		-- A zero integer
> i1  = eval$ sign ^ c1		-- integer +1
> im1 = eval$ sign ^ f ^ x ^ sign # (f # x) -- integer -1

** Function c_to_i

> -- c_to_i: N->Z
> -- Convert a natural number to an integer
> c_to_i = eval$ c ^ (sign ^ c)

** Function abs

Function abs:: Z -> N returns the magnitude of an integer Z. The result
is a natural number (Church numeral). We define abs by applying an
integer to an identity combinator. The combinator combI becomes the
sign "bit". In that case, it makes no difference if the body of an
integer has the form (sign ^ cn) or just 'cn':

> abs = eval$ i ^ i # combI

> -- Validation tests
> test_abs 
>   = Prelude.and [ expectd (eval$ abs # i0)  c0
>                 , expectd (eval$ abs # i1)  c1
>                 , expectd (eval$ abs # im1) c1
>                 ]


* Testing if an integer is positive or negative

** sign_case

Function sign_case:: Z -> on-positive -> on-zero -> on-negative -> term
is to be applied to an integer and three terms. The application
reduces to one of the terms, depending on the sign of the integer.

To implement the sign-branching, we apply the integer to three
suitably-chosen terms.

> sign_case = i ^ on_positive ^ on_zero ^ on_negative ^
>    i # (d ^ on_negative) # (d ^ on_positive) # on_zero
>  where [d,on_positive,on_zero,on_negative] = 
>         map make_var ["dummy","on_positive","on_zero","on_negative"]

** negativep, c_negate, i_negate

We can now easily define a negativity predicate and functions to
negate a number

> -- negativep:: Z -> Bool
> negativep = eval$ i ^ sign_case # i # false # false # true

> -- Validation tests
> test_negativep
>    = Prelude.and [ expectd (eval$ negativep # i0)  false 
>                  , expectd (eval$ negativep # i1)  false
>                  , expectd (eval$ negativep # im1) true
>                  ]

> -- c_negate:: N -> Z
> -- Turn a non-zero Church numeral into a negative integer
> c_negate = eval$ c^ sign^ f^ x^ sign # (c # f # x)

> -- i_negate:: Z -> Z
> -- Negate an integer
> -- The lazy semantics inherent in the normal order really helps us here
> i_negate = eval$ i^ sign_case #i # (c_negate#(abs#i)) # i0 # (c_to_i#(abs#i))


* Integer successor

The successor of an integer number a:

> i_succ = eval$ a^
>      sign_case # a
>      -- if the number 'a' is positive
>      # (c_to_i#(succ#(abs#a)))
>      -- if the number 'a' is zero
>      # i1
>      -- if the number 'a' is negative
>      # (i_negate # (c_to_i # (predp#(abs#a))))


> -- Validation tests
> test_isucc
>   = Prelude.and [ expectd (eval$ i_succ # i0)  i1 
>                 , expectd (eval$ i_succ # i1)  (sign^f^x^f#(f#x))
>                 , expectd (eval$ i_succ # i1)  (sign^c2)
>                 , expectd (eval$ i_succ # im1) i0
>                 , expectd (eval$ i_succ # (c_negate#c2)) im1
>                 ]


* Integer addition

Addition of two integer numbers, a and b

> i_add = eval$ a^ b^
>   sign_case # a
>     -- a > 0
>     # (sign_case # b
>         -- b > 0
>	  # (c_to_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)))
>       )


> -- Validation tests
> test_iadd
>   = Prelude.and [ expectd (eval$ i_add # i0 # i0)   i0
>                 , expectd (eval$ i_add # i0 # i1)   i1
>                 , expectd (eval$ i_add # i1 # i0)   i1
>                 , expectd (eval$ i_add # i1 # im1)  i0
>                 , expectd (eval$ i_add # (c_negate#c2) # im1) 
>                                              (sign^f^x^sign#(f#(f#(f#x))))
>                 , expectd (eval$ i_add # (c_negate#c2) # i1) im1
>                 , expectd (eval$ i_add # (c_to_i#c2) # im1) i1
>                 , expectd (eval$ i_add # (c_to_i#c2) # i1) (sign^c3)
>                 ]

* Integer Subtraction

a + b = a + (- b)

> i_sub = eval$ a^ b^ (i_add # a # (i_negate # b))

> -- Validation tests
> test_isub
>   = Prelude.and [ expectd (eval$ i_sub # i1 # i1)     i0
>                 , expectd (eval$ i_sub # i0 # i0)     i0
>                 , expectd (eval$ i_sub # im1 # im1)   i0
>                 , expectd (eval$ i_sub # (c_to_i#c2) # i1) i1
>                 , expectd (eval$ i_sub # i1 # (c_to_i#c2)) im1
>                 , expectd (eval$ i_sub # im1 # i0)  im1
>                 , expectd (eval$ i_sub # i0 # im1)  i1
>                 , expectd (eval$ i_sub # i1 # i0)   i1
>                 , expectd (eval$ i_sub # i0 # i1)   im1
>                 , expectd (eval$ i_sub # (c_to_i#c2) # (c_to_i#c3)) im1
>                 , expectd (eval$ i_sub # (c_to_i#c3) # (c_to_i#c2)) i1
>                 , expectd (eval$ i_sub # (c_negate#c2) # i1) 
>                                              (sign^f^x^sign#(f#(f#(f#x))))
>                 , expectd (eval$ i_sub # i1 # (c_negate#c2)) (sign^c3)
>                 , expectd (eval$ i_sub # im1 # (c_negate#c2)) i1
>                 , expectd (eval$ i_sub # (c_negate#c2) # im1) im1
>                 ]


* Integer Multiplication

We multiply the absolute values of the multiplicands and then adjust
the sign.

> i_mul = eval$ a^ b^
>   (  -- The sign-adjustment combinator
>    x^ sign_case # a
>      -- a > 0
>      # (sign_case # b # (c_to_i#x) # i0 # (c_negate#x))
>      -- a = 0
>      # i0
>      -- a < 0
>      # (sign_case # b # (c_negate#x) # i0 # (c_to_i#x))
>   )
>   # (mul # (abs#a) # (abs#b))


> -- Validation tests
> test_imul
>   = Prelude.and [ expectd (eval$ i_mul # i0 # i1)   i0
>                 , expectd (eval$ i_mul # i0 # im1)  i0
>                 , expectd (eval$ i_mul # i0 # i0)   i0
>                 , expectd (eval$ i_mul # im1# i0)   i0
>                 , expectd (eval$ i_mul # i1 # im1)  im1
>                 -- 2*3 => 6
>                 , expectd (eval$ i_mul # (c_to_i#c2) # (c_to_i#c3)) 
>                                      (eval$ (c_to_i#(add#c2#(add#c2#c2))))
>                 , expectd (eval$ i_mul # (c_negate#c2) # i1) 
>                                      (eval$ (c_negate#c2))
>                 , expectd (eval$ i_mul # i1 # (c_negate#c2)) 
>                                      (eval$ (c_negate#c2))
>                 , expectd (eval$ i_mul # (c_negate#c2) # im1) 
>                                      (eval$ (c_to_i#c2))
>                 ]


* Integer Division

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 latter 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,
type-arithmetics.html.  However the algorithm 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))

> i_div = eval$ a^ b^
>   (  -- The sign-adjustment combinator
>    x^ sign_case # a
>      -- a > 0
>      # (sign_case # b # (c_to_i#x) # true # (c_negate#x))
>      -- a = 0
>      # i0
>      -- a < 0
>      # (sign_case # b # (c_negate#x) # true # (c_to_i#x))
>   ) #
>   -- now divide x by y, where x and y are two positive integers
>  ((x^ y^
>     cdr # (cdr #
>      (x		            -- the dividend drives the iteration
>       # combI # (div_iter#y) # (cons3 # x # false # c0))))
>   # (c_to_i # (abs#a)) # (c_to_i # (abs#b)))
>    where
>      -- make a triple
>      cons3 = a^b^c^ (cons# a # (cons# b # c))
>      -- (uncurry3 f) = \(a,b,c) -> f a b c
>      uncurry3 = f^x^ (f # (car#x) # (car#(cdr#x)) # (cdr#(cdr#x)))
>      div_iter = y^u^ 
>       uncurry3 # 
>          (current^ flag^ accum^
>	      (lif # flag # u  -- we're done
>		#((diff^		 -- which is, current - y
>		   sign_case # diff
>		    -- diff > 0
>		    # (cons3# diff # false # (succ#accum))
>		    -- diff = 0
>		    # (cons3# diff # true  # (succ#accum))
>		    -- diff < 0
>		    # (cons3# diff # true  # accum))
>		# (i_sub#current#y))))
>         # u
>      [u,current,flag,accum,diff] 
>            = map make_var ["u","current","flag","accum","diff"]


This is honestly a lambda-term. To see that for yourself, type 'show_term
i_div 2000' at the Hugs or GHCi prompt.

Note that division by zero is undefined, which gives us freedom to
return any result of (i_div#x#i0). We chose to return 'true'


> -- Validation tests
> test_idiv
>   = Prelude.and [ expectd (eval$ i_div # i1 # i1)   i1
>                 , expectd (eval$ i_div # i0 # (c_to_i#c2))  i0
>                 , expectd (eval$ i_div # (c_to_i#c2) # i1) (sign^c2)
>                 , expectd (eval$ i_div # (c_to_i#c2) # im1)
>                                       (eval$ (c_negate#c2))
>                 -- 5 / 2 => 2
>--                 , expectd (eval$ i_div # (c_to_i#(succ#(add#c2#c2))) 
>--                                         # (c_to_i#c2))  (sign^c2)
>                 -- 5 / 2 => 2
>--                 , expectd (eval$ i_div # (c_to_i#(add#c2#c2)) 
>--                                         # (c_to_i#c2))  (sign^c2)
>                 -- -3 /  2 => -1
>--                 , expectd (eval$ i_div # (c_negate#c3) # (c_to_i#c2)) im1
>                 -- -3 / -2 => -1
>--                 , expectd (eval$ i_div # (c_negate#c3) # (c_negate#c2)) i1
>                 -- 2 /3 => 0
>                 , expectd (eval$ i_div # (c_negate#c2) # (c_negate#c3)) i0
>                 ]

Some of the division tests are filtered out because they really take
a lot of time and memory.

* Running all validation tests

> all_tests = Prelude.and 
>               [ test_predp, test_greaterp, test_abs
>                ,test_negativep, test_isucc, test_iadd, test_isub
>                ,test_imul, test_idiv
>               ]