|
|
|
last edited 11 years ago by test1 |
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: - \begin{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) --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 \end{spad} \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 T == add --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
spad
Compiling FriCAS source code from file
/var/zope2/var/LatexWiki/5234054015459578221-25px001.spad using
old system compiler.
SUM abbreviates domain Sum
------------------------------------------------------------------------
initializing NRLIB SUM for Sum
compiling into NRLIB SUM
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) Sum is an unknown constructor and so is unavailable. Did you mean to use -> but type something different instead? size()$Sum(PF 7,Product(PF 3,PF 13)) Sum is an unknown constructor and so is unavailable. Did you mean to use -> but type something different instead?