Edit detail for SandBoxDefineInteger revision 3 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.

This definition (which can be found in many standard texts on formal mathematics) was suggested by Ralf Hemmecke in discussions at ISSAC 2008 as an example of something simple that is not handled well by any current computer algebra system. But of course he is in no way responsible for the quality (or lack of it -:) for my particular attempt at implementing this below.

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

(1) -> <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]</spad>

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

   >> 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?

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