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

# Edit detail for SandBoxSum revision 1 of 14

 1 2 3 4 5 6 7 8 9 10 11 12 13 14 Editor: Bill Page Time: 2008/05/16 15:11:13 GMT-7 Note: Sum is dual to Product

changed:
-
)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

--representations
Rep := Union(acomp:A,bcomp:B)

--declarations
x,y: %
i: NonNegativeInteger
p: NonNegativeInteger
a: A
b: B
d: Integer

--define
coerce(x):OutputForm ==
x case acomp => (x.acomp)::OutputForm
(x.bcomp)::OutputForm
x=y == rep(x)= rep(y)
selectsum(x:%) == rep(x)
makefirst(a:A) : %   == per construct(a)$REP makesecond (b:B) : % == per construct(b)$REP

if A has Monoid and B has Monoid then
-- represent unit of Sum(A,B) as use 1$A (We could use either 1$A or 1$B) 1 == per construct(1$A)$REP x * y == x case acomp and y case acomp => per construct(rep(x).acomp * rep(y).acomp)$REP
x case bcomp and y case bcomp => per construct(rep(x).bcomp * rep(y).bcomp)$REP -- unit of Sum(A,B)=1$A is unit for B
x case acomp and x.acomp=1$A and y case bcomp => y error "not same type" x ** p == x case acomp => per construct(rep(x).acomp ** p)$REP
per construct(rep(x).bcomp ** p)$REP if A has Finite and B has Finite then size == size$A + size$B index(n) == n > size$B => per construct(index((n::Integer - size$B)::PositiveInteger)$A)$REP per construct(index(n)$B)$REP random() == random()$Boolean => per construct(random()$A)$REP
per construct(random()$B)REP lookup(x) == x case acomp => lookup(x.acomp)$A + size$B::Integer lookup(x.bcomp)$B
hash(x) == x case acomp => hash(x.acomp)$A + size$B::SingleInteger
hash(x.bcomp)$B if A has Group then inv(x) == x case acomp => per construct(inv(x.acomp))$REP
if B has Group then
inv(x) == x case bcomp => per construct(inv(x.bcomp))$REP if A has AbelianMonoid and B has AbelianMonoid then 0 == [0$A,0$B] x + y == [x.acomp + y.acomp,x.bcomp + y.bcomp] c:NonNegativeInteger * x == [c * x.acomp,c*x.bcomp] if A has CancellationAbelianMonoid and B has CancellationAbelianMonoid then subtractIfCan(x, y) : Union(%,"failed") == (na:= subtractIfCan(x.acomp, y.acomp)) case "failed" => "failed" (nb:= subtractIfCan(x.bcomp, y.bcomp)) case "failed" => "failed" [na::A,nb::B] if A has AbelianGroup and B has AbelianGroup then - x == [- x.acomp,-x.bcomp] (x - y):% == [x.acomp - y.acomp,x.bcomp - y.bcomp] d * x == [d * x.acomp,d * x.bcomp] if A has OrderedAbelianMonoidSup and B has OrderedAbelianMonoidSup then sup(x,y) == [sup(x.acomp,y.acomp),sup(x.bcomp,y.bcomp)] if A has OrderedSet and B has OrderedSet then x < y == xa:= x.acomp ; ya:= y.acomp xa < ya => true xb:= x.bcomp ; yb:= y.bcomp xa = ya => (xb < yb) false -- coerce(x:%):Symbol == -- PrintableForm() -- formList([x.acomp::Expression,x.bcomp::Expression])$PrintableForm

\begin{axiom}
size()$Sum(PF 7,PF 13) size()$Sum(PF 7,Product(PF 3,PF 13))
\end{axiom}


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
--representations
Rep := Union(acomp:A,bcomp:B)
--declarations
x,y: %
i: NonNegativeInteger
p: NonNegativeInteger
a: A
b: B
d: Integer
--define
coerce(x):OutputForm ==
x case acomp => (x.acomp)::OutputForm
(x.bcomp)::OutputForm
x=y == rep(x)= rep(y)
selectsum(x:%) == rep(x)
makefirst(a:A) : %   == per construct(a)$REP makesecond (b:B) : % == per construct(b)$REP
if A has Monoid and B has Monoid then
-- represent unit of Sum(A,B) as use 1$A (We could use either 1$A or 1$B) 1 == per construct(1$A)$REP x * y == x case acomp and y case acomp => per construct(rep(x).acomp * rep(y).acomp)$REP
x case bcomp and y case bcomp => per construct(rep(x).bcomp * rep(y).bcomp)$REP -- unit of Sum(A,B)=1$A is unit for B
x case acomp and x.acomp=1$A and y case bcomp => y error "not same type" x ** p == x case acomp => per construct(rep(x).acomp ** p)$REP
per construct(rep(x).bcomp ** p)$REP if A has Finite and B has Finite then size == size$A + size$B index(n) == n > size$B => per construct(index((n::Integer - size$B)::PositiveInteger)$A)$REP per construct(index(n)$B)$REP random() == random()$Boolean => per construct(random()$A)$REP
per construct(random()$B)REP lookup(x) == x case acomp => lookup(x.acomp)$A + size$B::Integer lookup(x.bcomp)$B
hash(x) == x case acomp => hash(x.acomp)$A + size$B::SingleInteger
hash(x.bcomp)$B if A has Group then inv(x) == x case acomp => per construct(inv(x.acomp))$REP
if B has Group then
inv(x) == x case bcomp => per construct(inv(x.bcomp))$REP if A has AbelianMonoid and B has AbelianMonoid then 0 == [0$A,0$B] x + y == [x.acomp + y.acomp,x.bcomp + y.bcomp] c:NonNegativeInteger * x == [c * x.acomp,c*x.bcomp] if A has CancellationAbelianMonoid and B has CancellationAbelianMonoid then subtractIfCan(x, y) : Union(%,"failed") == (na:= subtractIfCan(x.acomp, y.acomp)) case "failed" => "failed" (nb:= subtractIfCan(x.bcomp, y.bcomp)) case "failed" => "failed" [na::A,nb::B] if A has AbelianGroup and B has AbelianGroup then - x == [- x.acomp,-x.bcomp] (x - y):% == [x.acomp - y.acomp,x.bcomp - y.bcomp] d * x == [d * x.acomp,d * x.bcomp] if A has OrderedAbelianMonoidSup and B has OrderedAbelianMonoidSup then sup(x,y) == [sup(x.acomp,y.acomp),sup(x.bcomp,y.bcomp)] if A has OrderedSet and B has OrderedSet then x < y == xa:= x.acomp ; ya:= y.acomp xa < ya => true xb:= x.bcomp ; yb:= y.bcomp xa = ya => (xb < yb) false -- coerce(x:%):Symbol == -- PrintableForm() -- formList([x.acomp::Expression,x.bcomp::Expression])$PrintableForm
   Compiling FriCAS source code from file
compiling exported coerce : $-> OutputForm Time: 0.01 SEC. compiling exported = : ($,$) -> Boolean ****** comp fails at level 2 with expression: ****** error in function = (= | << | (|rep| |x|) | >> | (|rep| |y|)) ****** level 2 ******$x:= (rep x)
$m:=$EmptyMode
$f:= ((((|y| # #) (|x| # #) (|d| #) (|b| #) ...))) >> Apparent user error: cannot compile (rep x) axiomsize()$Sum(PF 7,PF 13)
use -> but type something different instead?