|
|
|
last edited 11 years ago by test1 |
Edit detail for SandBoxSum revision 3 of 14
| 1 2 3 4 5 6 7 8 9 10 11 12 13 14 | ||
|
Editor: Bill Page
Time: 2008/05/16 17:00:00 GMT-7 |
||
| Note: Sum is dual to Product | ||
changed: - -- represent unit of Sum(A,B) as use 1$A (We could use either 1$A or 1$B) -- represent unit of Sum(A,B) as 1$A (We could use either 1$A or 1$B) changed: - x * y == x case acomp and y case acomp => per construct(rep(x).acomp * rep(y).acomp)$REP x * y == x case acomp and y case acomp => per construct(rep(x).acomp * rep(y).acomp)$REP changed: - x ** p == x case acomp => per construct(rep(x).acomp ** p)$REP x ** p == x case acomp => per construct(rep(x).acomp ** p)$REP changed: - index(n) == n > size$B => per construct(index((n::Integer - size$B)::PositiveInteger)$A)$REP index(n) == n > size$B => per construct(index((n::Integer - size$B)::PositiveInteger)$A)$REP changed: - random() == random()$Boolean => per construct(random()$A)$REP random() == random()$Boolean => per construct(random()$A)$REP changed: - lookup(x) == x case acomp => lookup(x.acomp)$A + size$B::Integer lookup(x) == x case acomp => lookup(x.acomp)$A + size$B::Integer changed: - hash(x) == x case acomp => hash(x.acomp)$A + size$B::SingleInteger hash(x) == x case acomp => hash(x.acomp)$A + size$B::SingleInteger changed: - 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 Group and B has Group then inv(x) == x case acomp => per construct(inv(x.acomp))$REP per construct(inv(x.bcomp))$REP changed: - 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] -- represent zero of Sum(A,B) as 0$A (We could use either 0$A or 0$B) 0 == 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 -- zero of Sum(A,B)=0$A is zero for B x case acomp and x.acomp=1$A and y case bcomp => y error "not same type" c * x == x case acomp => per construct(c * rep(x).acomp)$REP per construct(c* rep(x).bcomp)$REP changed: - - x == [- x.acomp,-x.bcomp] - (x - y):% == [x.acomp - y.acomp,x.bcomp - y.bcomp] - d * x == [d * x.acomp,d * x.bcomp] - x == x case acomp => per(- rep(x).acomp) per(- rep(x).bcomp) (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 -- zero of Sum(A,B)=0$A is zero for B 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 error "not same type" d * x == x case acomp => per construct(d * rep(x).acomp)$REP per construct(d* rep(x).bcomp)$REP added: x case acomp and y case acomp => per construct(sup(rep(x).acomp,rep(y).acomp))$REP x case bcomp and y case bcomp => per construct(sup(rep(x).bcomp,rep(y).bcomp))$REP error "not same type" changed: - 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 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 error "not same type"
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) --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 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 and B has Group then inv(x) == x case acomp => per construct(inv(x.acomp))$REP per construct(inv(x.bcomp))$REP 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 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 -- zero of Sum(A,B)=0$A is zero for B x case acomp and x.acomp=1$A and y case bcomp => y error "not same type" c * x == x case acomp => per construct(c * rep(x).acomp)$REP per construct(c* rep(x).bcomp)$REP if A has AbelianGroup and B has AbelianGroup then - x == x case acomp => per(- rep(x).acomp) per(- rep(x).bcomp) (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 -- zero of Sum(A,B)=0$A is zero for B 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 error "not same type" d * x == x case acomp => per construct(d * rep(x).acomp)$REP per construct(d* rep(x).bcomp)$REP if A has OrderedAbelianMonoidSup and B has OrderedAbelianMonoidSup then sup(x,y) == [sup(x.acomp,y.acomp),sup(x.bcomp,y.bcomp)] x case acomp and y case acomp => per construct(sup(rep(x).acomp,rep(y).acomp))$REP x case bcomp and y case bcomp => per construct(sup(rep(x).bcomp,rep(y).bcomp))$REP error "not same type" if A has OrderedSet and B has OrderedSet then x < y == 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 error "not same type"
spad
Compiling FriCAS source code from file
/var/zope2/var/LatexWiki/4880448010643137522-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.03 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?