Edit detail for SandBoxDefineInteger revision 4 of 11

Why are PositiveInteger? and NonNegativeInteger? defined as SubDomains? of Integer? Here is an (imperfect) example of defining Integers from a more primitive domain rather than the other way around.

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

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

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

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

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

   Compiling OpenAxiom source code from file 
      /var/zope2/var/LatexWiki/3168118417028783659-25px001.spad using 
      Spad compiler.
   DIFF abbreviates domain Difference 
------------------------------------------------------------------------
   initializing NRLIB DIFF for Difference 
   compiling into NRLIB DIFF 
   Adding $ modemaps
   Adding T$ modemaps
   Adding T$ modemaps
****** Domain: T$ already in scope
   compiling local rep : % -> Record(neg: T$,pos: T$)
      DIFF;rep is replaced by G1392 
Time: 0 SEC.

   compiling local per : Record(neg: T$,pos: T$) -> %
      DIFF;per is replaced by G1392 
Time: 0 SEC.

   compiling exported Zero : () -> %
Time: 0 SEC.

   compiling exported + : (%,%) -> %
Time: 0 SEC.

   compiling exported - : (%,%) -> %
Time: 0 SEC.

   Adding Boolean modemaps
   compiling exported = : (%,%) -> Boolean
Time: 0.06 SEC.

   Adding OutputForm modemaps
   compiling exported coerce : % -> OutputForm
Time: 0 SEC.

   Adding Integer modemaps
   Adding NonNegativeInteger modemaps
   compiling exported coerce : NonNegativeInteger -> %
Time: 0.01 SEC.

(time taken in buildFunctor:  0)

;;;     ***       |Difference| REDEFINED

;;;     ***       |Difference| REDEFINED
Time: 0 SEC.

   Cumulative Statistics for Constructor Difference
      Time: 0.07 seconds

   finalizing NRLIB DIFF 
   Processing Difference for Browser database:
--->-->Difference((- (% % %))): Not documented!!!!
--->-->Difference(constructor): Not documented!!!!
--->-->Difference(): Missing Description
------------------------------------------------------------------------
   Difference is now explicitly exposed in frame initial 
   Difference will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/DIFF.NRLIB/code.o

Now use DIFF to define an "Integer"

axiom
i:DIFF(CardinalNumber)

axiom
i:=2

(1)

axiom
j:=i-4

(2)

axiom
k:=j+2

(3)

axiom
test(k=0)

(4)

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