

last edited 9 years ago by test1 
1 2 3 4 5 6 7 8 9 10 11  
Editor: test1
Time: 2013/04/26 18:59:47 GMT+0 

Note: 
changed:  Rep == Record(neg:T, pos:T) Rep ==> Record(neg:T, pos:T) rep x ==> (x@%) pretend Rep per x ==> (x@Rep) pretend %
Why are the domains PositiveInteger? and NonNegativeInteger? defined as SubDomains 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).
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) rep x ==> (x@%) pretend Rep per x ==> (x@Rep) pretend %
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] xy == 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/axiomwiki/var/LatexWiki/764699444807244438325px001.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 processing macro definition Rep ==> Record(neg: T$,pos: T$) processing macro definition rep x ==> pretend(@(x, $), Record(neg: T$, pos: T$)) processing macro definition per x ==> pretend(@(x, Record(neg: T$, pos: T$)), $) compiling exported Zero : () > $ Time: 0 SEC.
compiling exported One : () > $ Time: 0 SEC.
compiling local canonize : Record(neg: T$,pos: T$) > Record(neg: T$, pos: T$) Time: 0 SEC.
compiling exported + : ($,$) > $ Time: 0 SEC.
compiling exported  : ($,$) > $ Time: 0 SEC.
compiling exported = : ($,$) > Boolean Time: 0 SEC.
compiling exported < : ($,$) > Boolean Time: 0.01 SEC.
compiling exported > : ($,$) > Boolean Time: 0 SEC.
compiling exported coerce : $ > OutputForm Time: 0 SEC.
compiling exported coerce : NonNegativeInteger > $ Time: 0 SEC.
(time taken in buildFunctor: 0)
;;; *** Difference REDEFINED
;;; *** Difference REDEFINED Time: 0 SEC.
Warnings: [1] canonize: neg has no value [2] canonize: pos has no value [3] =: pos has no value [4] <: pos has no value [5] >: pos has no value [6] coerce: neg has no value [7] coerce: pos has no value
Cumulative Statistics for Constructor Difference Time: 0.01 seconds
finalizing NRLIB DIFF Processing Difference for Browser database: >>Difference(constructor): Not documented!!!! >>Difference(( (% % %))): Not documented!!!! >>Difference(): Missing Description ; compiling file "/var/aw/var/LatexWiki/DIFF.NRLIB/DIFF.lsp" (written 04 APR 2022 07:06:23 PM):
; /var/aw/var/LatexWiki/DIFF.NRLIB/DIFF.fasl written ; compilation finished in 0:00:00.037  Difference is now explicitly exposed in frame initial Difference will be automatically loaded when needed from /var/aw/var/LatexWiki/DIFF.NRLIB/DIFF
Now use DIFF to define an "Integer"
i:DIFF(CardinalNumber)
i:=2
(1) 
j:=i4
(2) 
k:=j+2
(3) 
test(k=0)
(4) 
i:=1234567
(5) 
j:=i7654321
(6) 
k:=j+6666666246912
(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 builtin support for such common algebraic constructions as "taking a quotient". In particular, there seems to be no general way of defining a "canonical representation".