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

# Edit detail for SandBoxSum revision 8 of 14

 1 2 3 4 5 6 7 8 9 10 11 12 13 14 Editor: Bill Page Time: 2008/08/24 06:55:53 GMT-7 Note: output format

```changed:
-       makefirst  :   A -> %
in1  :   A -> %

changed:
-       makesecond :   B -> %
in2 :   B -> %

changed:
-       coerce(x:%):OutputForm == coerce(rep(x))\$Rep
coerce(x:%):OutputForm ==
rep(x) case acomp => sub(coerce(rep(x).acomp),"1")
sub(coerce(rep(x).bcomp),"2")

changed:
-       makefirst(a:A):%   == per [a]
-       makesecond(b:B): % == per [b]
in1(a:A):%   == per [a]
in2(b:B): % == per [b]

changed:
-makefirst(10)\$Sum(Integer,Integer)
-makefirst(10)\$Sum(Integer,Integer)<makesecond(10)\$Sum(Integer,Integer)
-sup(makefirst(99)\$Sum(NNI,NNI),makesecond(10)\$Sum(NNI,NNI))
-
in1(10)\$Sum(Integer,Integer)
in1(10)\$Sum(Integer,Integer) < in2(10)\$Sum(Integer,Integer)
sup(in1(99)\$Sum(NNI,NNI), in2(10)\$Sum(NNI,NNI))
```

The Sum domain constructor is intended to be the Categorical Dual of the Product domain constructor

```)abbrev domain SUM Sum
++ Description:
++ This domain implements direct union
Sum (A:SetCategory,B:SetCategory) : C == T
where
C == SetCategory  with
if A has Finite and B has Finite then Finite
if A has Monoid and B has Monoid then Monoid
if A has AbelianMonoid and B has AbelianMonoid then AbelianMonoid
if A has CancellationAbelianMonoid and
B has CancellationAbelianMonoid then CancellationAbelianMonoid
if A has Group  and B has Group  then  Group
if A has AbelianGroup and B has AbelianGroup then  AbelianGroup
if A has OrderedAbelianMonoidSup and B has OrderedAbelianMonoidSup
then OrderedAbelianMonoidSup
if A has OrderedSet and B has OrderedSet then  OrderedSet
selectsum     : % -> Union(acomp:A,bcomp:B)
++ selectsum(x) \undocumented
in1  :   A -> %
++ makefirst(a) \undocumented
in2 :   B -> %
++ makesecond(b) \undocumented
--representations
Rep == Union(acomp:A,bcomp:B)
import Rep
--declarations
x,y: %
i: NonNegativeInteger
p: NonNegativeInteger
a: A
b: B
c: PositiveInteger
d: Integer
--define
coerce(x:%):OutputForm ==
rep(x) case acomp => sub(coerce(rep(x).acomp),"1")
sub(coerce(rep(x).bcomp),"2")
x=y == rep(x)=rep(y)
selectsum(x:%) == rep(x)
in1(a:A):%   == per [a]
in2(b:B): % == per [b]
if A has Monoid and B has Monoid then
-- represent unit of Sum(A,B) as 1\$A (We could use either 1\$A or 1\$B)
1 == per [1\$A]
x * y ==
rep(x) case acomp and rep(y) case acomp => per [rep(x).acomp * rep(y).acomp]
rep(x) case bcomp and rep(y) case bcomp => per [rep(x).bcomp * rep(y).bcomp]
-- unit of Sum(A,B)=1\$A is unit for B
rep(x) case acomp and rep(x).acomp=1\$A and rep(y) case bcomp => y
error "not same type"
x ** p ==
rep(x) case acomp => per [rep(x).acomp ** p]
per [rep(x).bcomp ** p]
if A has Finite and B has Finite then
size == size\$A + size\$B
index(n) ==
n > size\$B => per [index((n::Integer - size\$B)::PositiveInteger)\$A]
per [index(n)\$B]
random() ==
random()\$Boolean => per [random()\$A]
per [random()\$B]
lookup(x) ==
rep(x) case acomp => (lookup(rep(x).acomp)\$A::NonNegativeInteger + size\$B)::PositiveInteger
lookup(rep(x).bcomp)\$B
hash(x) ==
rep(x) case acomp => hash(rep(x).acomp)\$A + size\$B::SingleInteger
hash(rep(x).bcomp)\$B
if A has Group and B has Group then
inv(x) ==
rep(x) case acomp => per [inv(rep(x).acomp)]
per [inv(rep(x).bcomp)]
if A has AbelianMonoid and B has AbelianMonoid then
-- represent zero of Sum(A,B) as 0\$A (We could use either 0\$A or 0\$B)
0 == per [0\$A]
x + y ==
rep(x) case acomp and rep(y) case acomp => per [rep(x).acomp + rep(y).acomp]
rep(x) case bcomp and rep(y) case bcomp => per [rep(x).bcomp + rep(y).bcomp]
-- zero of Sum(A,B)=0\$A is zero for B
rep(x) case acomp and x=0 and rep(y) case bcomp => y
rep(x) case bcomp and y=0 and rep(y) case acomp => x
error "not same type"
c * x ==
rep(x) case acomp => per [c * rep(x).acomp]
per [c* rep(x).bcomp]
if A has AbelianGroup and B has AbelianGroup then
- x ==
rep(x) case acomp => per [- rep(x).acomp]
per [- rep(x).bcomp]
(x - y):% ==
rep(x) case acomp and rep(y) case acomp => per [rep(x).acomp - rep(y).acomp]
rep(x) case bcomp and rep(y) case bcomp => per [rep(x).bcomp - rep(y).bcomp]
-- zero of Sum(A,B)=0\$A is zero for B
rep(x) case acomp and x=0 and rep(y) case bcomp => - y
rep(x) case bcomp and y=0 and rep(y) case acomp => x
error "not same type"
d * x ==
rep(x) case acomp => per [d * rep(x).acomp]
per [d* rep(x).bcomp]
if A has OrderedAbelianMonoidSup and B has OrderedAbelianMonoidSup then
sup(x,y) ==
rep(x) case acomp and rep(y) case acomp => per [sup(rep(x).acomp,rep(y).acomp)]
rep(x) case bcomp and rep(y) case bcomp => per [sup(rep(x).bcomp,rep(y).bcomp)]
rep(x) case acomp and rep(y) case bcomp => y
x
if A has OrderedSet and B has OrderedSet then
x < y ==
rep(x) case acomp and rep(y) case acomp => rep(x).acomp < rep(y).acomp
rep(x) case bcomp and rep(y) case bcomp => rep(x).bcomp < rep(y).bcomp
rep(x) case acomp and rep(y) case bcomp => true
false```
```   Compiling OpenAxiom source code from file
SUM abbreviates domain Sum
------------------------------------------------------------------------
initializing NRLIB SUM for Sum
compiling into NRLIB SUM
compiling local rep : % -> Union(acomp: A,bcomp: B)
SUM;rep is replaced by G1436
Time: 0.01 SEC.
compiling local per : Union(acomp: A,bcomp: B) -> %
SUM;per is replaced by G1436
Time: 0 SEC.
importing Rep
compiling exported coerce : % -> OutputForm
Time: 0.02 SEC.
compiling exported = : (%,%) -> Boolean
Time: 0 SEC.
compiling exported selectsum : % -> Union(acomp: A,bcomp: B)
Time: 0 SEC.
compiling exported in1 : A -> %
Time: 0 SEC.
compiling exported in2 : B -> %
Time: 0 SEC.
****** Domain: A already in scope
augmenting A: (Monoid)
****** Domain: B already in scope
augmenting B: (Monoid)
compiling exported One : () -> %
Time: 0 SEC.
compiling exported * : (%,%) -> %
Time: 0.07 SEC.
compiling exported ** : (%,NonNegativeInteger) -> %
Time: 0.01 SEC.
****** Domain: A already in scope
augmenting A: (Finite)
****** Domain: B already in scope
augmenting B: (Finite)
compiling exported size : () -> NonNegativeInteger
Time: 0 SEC.
compiling exported index : PositiveInteger -> %
Time: 0.01 SEC.
compiling exported random : () -> %
Time: 0 SEC.
compiling exported lookup : % -> PositiveInteger
Time: 0.01 SEC.
compiling exported hash : % -> SingleInteger
Time: 0 SEC.
****** Domain: A already in scope
augmenting A: (Group)
****** Domain: B already in scope
augmenting B: (Group)
compiling exported inv : % -> %
Time: 0.02 SEC.
****** Domain: A already in scope
augmenting A: (AbelianMonoid)
****** Domain: B already in scope
augmenting B: (AbelianMonoid)
compiling exported Zero : () -> %
Time: 0 SEC.
compiling exported + : (%,%) -> %
Time: 0.01 SEC.
compiling exported * : (PositiveInteger,%) -> %
Time: 0.07 SEC.
****** Domain: A already in scope
augmenting A: (AbelianGroup)
****** Domain: B already in scope
augmenting B: (AbelianGroup)
compiling exported - : % -> %
Time: 0.01 SEC.
compiling exported - : (%,%) -> %
Time: 0.01 SEC.
compiling exported * : (Integer,%) -> %
Time: 0.02 SEC.
****** Domain: A already in scope
augmenting A: (OrderedAbelianMonoidSup)
****** Domain: B already in scope
augmenting B: (OrderedAbelianMonoidSup)
compiling exported sup : (%,%) -> %
Time: 0.01 SEC.
****** Domain: A already in scope
augmenting A: (OrderedSet)
****** Domain: B already in scope
augmenting B: (OrderedSet)
compiling exported < : (%,%) -> Boolean
Time: 0.02 SEC.
****** Domain: A already in scope
augmenting A: (AbelianGroup)
****** Domain: B already in scope
augmenting B: (AbelianGroup)
****** Domain: A already in scope
augmenting A: (Finite)
****** Domain: B already in scope
augmenting B: (Finite)
****** Domain: A already in scope
augmenting A: (Group)
****** Domain: B already in scope
augmenting B: (Group)
****** Domain: A already in scope
augmenting A: (OrderedAbelianMonoidSup)
****** Domain: B already in scope
augmenting B: (OrderedAbelianMonoidSup)
****** Domain: A already in scope
augmenting A: (AbelianGroup)
****** Domain: B already in scope
augmenting B: (AbelianGroup)
****** Domain: A already in scope
augmenting A: (AbelianGroup)
****** Domain: B already in scope
augmenting B: (AbelianGroup)
****** Domain: A already in scope
augmenting A: (AbelianGroup)
****** Domain: B already in scope
augmenting B: (AbelianGroup)
****** Domain: A already in scope
augmenting A: (Group)
****** Domain: B already in scope
augmenting B: (Group)
****** Domain: A already in scope
augmenting A: (OrderedAbelianMonoidSup)
****** Domain: B already in scope
augmenting B: (OrderedAbelianMonoidSup)
(time taken in buildFunctor:  2)
;;;     ***       |Sum| REDEFINED
;;;     ***       |Sum| REDEFINED
Time: 0.09 SEC.
Warnings:
[1] coerce:  acomp has no value
[2] coerce:  bcomp has no value
[3] *:  acomp has no value
[4] *:  bcomp has no value
[5] **:  acomp has no value
[6] **:  bcomp has no value
[7] lookup:  acomp has no value
[8] lookup:  bcomp has no value
[9] hash:  acomp has no value
[10] hash:  bcomp has no value
[11] inv:  acomp has no value
[12] inv:  bcomp has no value
[13] +:  acomp has no value
[14] +:  bcomp has no value
[15] -:  acomp has no value
[16] -:  bcomp has no value
[17] sup:  acomp has no value
[18] sup:  bcomp has no value
[19] <:  acomp has no value
[20] <:  bcomp has no value
Cumulative Statistics for Constructor Sum
Time: 0.39 seconds
finalizing NRLIB SUM
Processing Sum for Browser database:
-- selectsum : % -> Union(acomp: A,bcomp: B)
--->-->Sum((selectsum ((Union (: acomp A) (: bcomp B)) %))): Unexpected HT command: \spad
-- in1 : A -> %
--->-->Sum((in1 (% A))): Improper first word in comments: makefirst
"makefirst(a) \\undocumented"
-- in2 : B -> %
--->-->Sum((in2 (% B))): Improper first word in comments: makesecond
-- constructor
------------------------------------------------------------------------
Sum is now explicitly exposed in frame initial
Sum will be automatically loaded when needed from
/var/zope2/var/LatexWiki/SUM.NRLIB/code.o```

axiom
`size()\$Sum(PF 7,PF 13)`
 (1)
Type: NonNegativeInteger?
axiom
`size()\$Sum(PF 7,Product(PF 3,PF 13))`
 (2)
Type: NonNegativeInteger?
axiom
`in1(10)\$Sum(Integer,Integer)`
 (3)
Type: Sum(Integer,Integer)
axiom
`in1(10)\$Sum(Integer,Integer) < in2(10)\$Sum(Integer,Integer)`
 (4)
Type: Boolean
axiom
`sup(in1(99)\$Sum(NNI,NNI), in2(10)\$Sum(NNI,NNI))`
 (5)
Type: Sum(NonNegativeInteger?,NonNegativeInteger?)