Edit detail for SandBoxDefineInteger revision 10 of 11

Why are the domains PositiveInteger? and NonNegativeInteger? defined as [SubDomain]?s of Integer insteadof the other way around? Here is a (still somewhat imperfect) example of one way of defining Integer from a more primitive domain (some domain without negatives and perhaps without zero, sometimes called a rig - ring without negative) although Axiom does not currently implement such a category. (Related: category RNG - ring without identity).

John Baez wrote:

Rigs are neglected in ordinary algebra texts, a deficiency that someday must be fixed. Why? First, a lot of stuff that’s true about rings is still true about rigs. Second, and much more importantly, any approach to algebra that doesn’t make room for the natural numbers is clearly defective: the natural numbers are a fundamental algebraic structure that must be reckoned with!

http://golem.ph.utexas.edu/category/2008/05/theorems_into_coffee_iii.html

(Refer also to his discussion of PROPS.)

Most CAS doesn't bother to define natural numbers via the Peano Axioms and then derive integers, for example, as an equivalence class of pairs of natural numbers so that

(a, b) ~ (c, d) iff a + d = b + c.

The question is whether a compiler could be smart enough to replace the definition via equivalence classes by an efficient representation that is, for example, used by GMP.

First let's define a constructor name Difference. Like Fraction the representation will be pairs of some suitable type and equality will be defined by an equivalence relation on this representation. Integer then can be constructed as Difference(CardinalNumber) as a kind of algebraic "quotient".

)abbrev domain DIFF Difference
Difference(T:Join(Monoid,AbelianMonoid,OrderedSet,RetractableTo(NonNegativeInteger))): Join(Monoid,AbelianMonoid, OrderedSet,RetractableTo(NonNegativeInteger)) with
    _-:(%,%) -> %
  == add
    Rep == Record(neg:T, pos:T)

    0 == per [0,0]
    1 == per [0,1]

    -- binary search for the canonical representative
    canonize(x:Rep):Rep ==
      y:= [0,0]@Rep
      while x.neg+y.pos < x.pos repeat
        n:T:=1
        while x.neg+y.pos+(nn:=n+n) <= x.pos repeat n:=nn
        y.pos:=y.pos+n
      while x.neg > x.pos+y.neg repeat
        n:T:=1
        while x.neg >= x.pos+y.neg+(nn:=n+n) repeat n:=nn
        y.neg := y.neg+n
      y

    x+y == per canonize [rep(x).neg+rep(y).neg, rep(x).pos+rep(y).pos]
    x-y == per canonize [rep(x).neg+rep(y).pos, rep(x).pos+rep(y).neg]
    x=y == rep(x).pos+rep(y).neg = rep(x).neg+rep(y).pos
    x<y == rep(x).pos+rep(y).neg < rep(x).neg+rep(y).pos
    x>y == rep(x).pos+rep(y).neg > rep(x).neg+rep(y).pos

    -- how to define this properly?
    coerce(x:%):OutputForm ==
      x<0 => -(rep(x).neg::OutputForm)
      rep(x).pos::OutputForm
    coerce(x:NonNegativeInteger):% == per [0,coerce(x)$T]

   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/3066500097849615682-25px001.spad
      using old system compiler.
   DIFF abbreviates domain Difference 
------------------------------------------------------------------------
   initializing NRLIB DIFF for Difference 
   compiling into NRLIB DIFF 
****** Domain: T$ already in scope
****** Domain: T$ already in scope
****** Domain: T$ already in scope
************* USER ERROR **********
available signatures for Rep: 
    NONE
NEED Rep: () -> ?
****** comp fails at level 1 with expression: ******
((DEF (|Rep|) (NIL) (NIL) (|Record| (|:| |neg| T$) (|:| |pos| T$))))
****** level 1  ******
$x:= (DEF (Rep) (NIL) (NIL) (Record (: neg T$) (: pos T$)))
$m:= $EmptyMode
$f:=
((((|$Information| #) (|retract| #) (|retractIfCan| #) (|coerce| #) ...)))

   >> Apparent user error:
   unspecified error

Now use DIFF to define an "Integer"

i:DIFF(CardinalNumber)

   Difference is an unknown constructor and so is unavailable. Did you 
      mean to use -> but type something different instead?
i:=2

(1)

j:=i-4

(2)

k:=j+2

(3)

test(k=0)

(4)

i:=1234567

(5)

j:=i-7654321

(6)

k:=j+6666666-246912

(7)

test(k=0)

(8)

The point of this construction is to illustrate several problems.

One such problem is that current generation of compilers in computer algebra systems such as Axiom, specifically Spad and Aldor, are not able to automatically convert this presumably mathematically correct specification to an efficient implementation, e.g. signed integers.

Another issue is why these languages do not have some built-in support for such common algebraic constructions as "taking a quotient". In particular, there seems to be no general way of defining a "canonical representation".

http://en.wikipedia.org/wiki/Mathematical_joke