login  home  contents  what's new  discussion  bug reports     help  links  subscribe  changes  refresh  edit

Edit detail for SandBoxDefineInteger revision 2 of 11

1 2 3 4 5 6 7 8 9 10 11
Editor: Bill Page
Time: 2008/07/21 07:02:04 GMT-7
Note: new

changed:
-Difference(T:AbelianMonoid): AbelianMonoid with
Difference(T:Join(AbelianMonoid,RetractableTo(NonNegativeInteger))): Join(AbelianMonoid, RetractableTo(NonNegativeInteger)) with

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

added:
    coerce(x:NonNegativeInteger):% == per [0,coerce(x)$T]

added:

Now use DIFF to define an "Integer"
\begin{axiom}
i:DIFF(CardinalNumber)
i:=2
i-4
\end{axiom}

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 was suggested by Ralf Hemmecke in discussions at ISSAC 2008.

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

The point of this construction is to illustrate several problems. One is to ask why the current generation of compilers in computer algebra systems such as Axiom, e.g. Spad and Aldor, are not able to automatically convert this mathematically correct specification to an efficient implementation. 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".

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 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.05 SEC.
Adding OutputForm modemaps compiling exported coerce : % -> OutputForm Time: 0.01 SEC.
Adding Integer modemaps Adding NonNegativeInteger modemaps compiling exported coerce : NonNegativeInteger -> % Time: 0 SEC.
(time taken in buildFunctor: 0)
;;; *** |Difference| REDEFINED
;;; *** |Difference| REDEFINED Time: 0.01 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)
Type: Void
axiom
i:=2
LatexWiki Image(1)
Type: Difference CardinalNumber?
axiom
i-4
LatexWiki Image(2)
Type: Difference CardinalNumber?