|
|
|
last edited 12 years ago by test1 |
Edit detail for SandBoxSum revision 5 of 14
| 1 2 3 4 5 6 7 8 9 10 11 12 13 14 | ||
|
Editor: Bill Page
Time: 2008/05/16 19:36:50 GMT-7 |
||
| Note: Sum is dual to Product | ||
added: c: PositiveInteger changed: - x case acomp => lookup(x.acomp)$A + size$B::Integer - lookup(x.bcomp)$B rep(x) case acomp => (lookup(rep(x).acomp)$A::NonNegativeInteger + size$B)::PositiveInteger lookup(rep(x).bcomp)$B changed: - x case acomp => hash(x.acomp)$A + size$B::SingleInteger - hash(x.bcomp)$B rep(x) case acomp => hash(rep(x).acomp)$A + size$B::SingleInteger hash(rep(x).bcomp)$B changed: - x case acomp => per [inv(x.acomp)] - per [inv(x.bcomp)] rep(x) case acomp => per [inv(rep(x).acomp)] per [inv(rep(x).bcomp)] changed: - 0 == per [1$A] 0 == per [0$A] changed: - rep(x) case acomp and rep(x).acomp=1$A and rep(y) case bcomp => y 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 changed: - x case acomp => per [c * rep(x).acomp] rep(x) case acomp => per [c * rep(x).acomp] changed: - x case acomp => per(- rep(x).acomp) - per(- rep(x).bcomp) rep(x) case acomp => per [- rep(x).acomp] per [- rep(x).bcomp] changed: - x case acomp and y case acomp => per [rep(x).acomp - rep(y).acomp] - x case bcomp and y case bcomp => per [rep(x).bcomp - rep(y).bcomp] 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] changed: - x case acomp and x.acomp=0$A and y case bcomp => - y - x case acomp and y.bcomp=0$A and y case bcomp => y 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 changed: - x case acomp => per [d * rep(x).acomp] rep(x) case acomp => per [d * rep(x).acomp] changed: - sup(x,y) == [sup(x.acomp,y.acomp),sup(x.bcomp,y.bcomp)] - x case acomp and y case acomp => per [sup(rep(x).acomp,rep(y).acomp)] - x case bcomp and y case bcomp => per [sup(rep(x).bcomp,rep(y).bcomp)] 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)] changed: - x case acomp and y case acomp => rep(x).acomp < rep(y).acomp - x case bcomp and y case bcomp => rep(x).bcomp < rep(y).bcomp 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
The Sum domain constructor is intended to be the CategoricalDual? of the Product domain constructor
spad)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 makefirst : A -> % ++ makefirst(a) \undocumented makesecond : B -> % ++ makesecond(b) \undocumented T == add --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 == coerce(rep(x))$Rep x=y == rep(x)=rep(y) selectsum(x:%) == rep(x) makefirst(a) == per [a] makesecond(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)] error "not same type" 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 error "not same type"
spad
Compiling OpenAxiom source code from file
/var/zope2/var/LatexWiki/8961560744568257601-25px001.spad using
Spad compiler.
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 G1431
Time: 0.01 SEC.
compiling local per : Union(acomp: A,bcomp: B) -> %
SUM;per is replaced by G1431
Time: 0 SEC.
importing Rep
compiling exported coerce : % -> OutputForm
Time: 0 SEC.
compiling exported = : (%,%) -> Boolean
Time: 0.01 SEC.
compiling exported selectsum : % -> Union(acomp: A,bcomp: B)
Time: 0 SEC.
compiling exported makefirst : A -> %
Time: 0 SEC.
compiling exported makesecond : 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.01 SEC.
compiling exported * : (%,%) -> %
Time: 0.08 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 SEC.
compiling exported hash : % -> SingleInteger
Time: 0.01 SEC.
****** Domain: A already in scope
augmenting A: (Group)
****** Domain: B already in scope
augmenting B: (Group)
compiling exported inv : % -> %
Time: 0.01 SEC.
****** Domain: A already in scope
augmenting A: (AbelianMonoid)
****** Domain: B already in scope
augmenting B: (AbelianMonoid)
compiling exported Zero : () -> %
Time: 0.01 SEC.
compiling exported + : (%,%) -> %
Time: 0.02 SEC.
compiling exported * : (PositiveInteger,%) -> %
Time: 0.08 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.02 SEC.
compiling exported * : (Integer,%) -> %
Time: 0.01 SEC.
****** Domain: A already in scope
augmenting A: (OrderedAbelianMonoidSup)
****** Domain: B already in scope
augmenting B: (OrderedAbelianMonoidSup)
compiling exported sup : (%,%) -> %
Time: 0.02 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.11 SEC.
Warnings:
[1] *: acomp has no value
[2] *: bcomp has no value
[3] **: acomp has no value
[4] **: bcomp has no value
[5] lookup: acomp has no value
[6] lookup: bcomp has no value
[7] hash: acomp has no value
[8] hash: bcomp has no value
[9] inv: acomp has no value
[10] inv: bcomp has no value
[11] +: acomp has no value
[12] +: bcomp has no value
[13] -: acomp has no value
[14] -: bcomp has no value
[15] sup: acomp has no value
[16] sup: bcomp has no value
[17] <: acomp has no value
[18] <: bcomp has no value
Cumulative Statistics for Constructor Sum
Time: 0.45 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
"\\spad{selectsum(x)} \\undocumented"
-- makefirst : A -> %
--->-->Sum((makefirst (% A))): Unexpected HT command: \spad
"\\spad{makefirst(a)} \\undocumented"
-- makesecond : B -> %
--->-->Sum((makesecond (% B))): Unexpected HT command: \spad
"\\spad{makesecond(b)} \\undocumented"
-- constructor
------------------------------------------------------------------------
Sum is now explicitly exposed in frame initial
Sum will be automatically loaded when needed from
/var/zope2/var/LatexWiki/SUM.NRLIB/code.oaxiomsize()$Sum(PF 7,PF 13)
 | (1) |
Type: NonNegativeInteger?
axiomsize()$Sum(PF 7,Product(PF 3,PF 13))
 | (2) |
Type: NonNegativeInteger?