

last edited 9 years ago by test1 
1 2 3 4 5 6 7 8 9 10 11 12 13 14  
Editor: Bill Page
Time: 2008/08/29 11:42:34 GMT7 

Note: DirectSum 
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
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 == 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) == per [a] in2(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 x=1 => y y=1 => x 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 x=0 => y y=0 => 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 x=0 => y y=0 => 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
Compiling FriCAS source code from file /var/zope2/var/LatexWiki/821944659447829011725px001.spad using old system compiler. SUM abbreviates domain Sum  initializing NRLIB SUM for Sum compiling into NRLIB SUM importing Union(acomp: A,bcomp: B) compiling exported coerce : $ > OutputForm ****** comp fails at level 4 with expression: ****** error in function coerce
(SEQ (LET #1=#:G718 (case  <<  (rep x)  >>  acomp)) (exit 1 (IF #1# (sub (coerce ((rep x) acomp)) "1") (sub (coerce ((rep x) bcomp)) "2")))) ****** level 4 ****** $x:= (rep x) $m:= $EmptyMode $f:= ((((x # #) (d #) (c #) (* #) ...)))
>> Apparent user error: acomp is an unknown mode
size()$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? in1(10)$Sum(Integer,Integer)
Sum is an unknown constructor and so is unavailable. Did you mean to use > but type something different instead? in1(10)$Sum(Integer,Integer) < in2(10)$Sum(Integer, Integer)
Sum is an unknown constructor and so is unavailable. Did you mean to use > but type something different instead? sup(in1(99)$Sum(NNI,NNI), in2(10)$Sum(NNI, NNI))
Sum is an unknown constructor and so is unavailable. Did you mean to use > but type something different instead?
The CoTuple? domain constructor is intended to be the Categorical Dual of the Tuple domain constructor
)abbrev domain COT CoTuple ++ This domain is intended to be the categorical dual of a ++ Tuple (commadelimited homogeneous sequence of values). ++ As such it implements an nary disjoint union. CoTuple(S:Type): CoercibleTo(S) with inj: (NonNegativeInteger,S) > % ++ inject(x, n) returns x as an element of the nth ++ component of the CoTuple. CoTuples are 0based ind: % > NonNegativeInteger ++ index(x) returns the component number of x in the CoTuple if S has Monoid then Monoid if S has AbelianMonoid then AbelianMonoid if S has CancellationAbelianMonoid then CancellationAbelianMonoid if S has Group then Group if S has AbelianGroup then AbelianGroup if S has OrderedAbelianMonoidSup then OrderedAbelianMonoidSup if S has SetCategory then SetCategory if S has OrderedSet then OrderedSet == add Rep == Record(ind : NonNegativeInteger, elt : S) declarations x, y: % s: S i: NonNegativeInteger p: NonNegativeInteger c: PositiveInteger d: Integer
coerce(x:%):S == rep(x).elt inj(i,s) == per [i, s] ind(x) == rep(x).ind
if S has SetCategory then x = y == (rep(x).ind = rep(y).ind) and (rep(x).elt = rep(y).elt) coerce(x : %): OutputForm == sub(coerce(rep(x).elt),coerce(rep(x).ind)) if S has Monoid then  represent unit of CoTuple(S) as 1$S of component 0 1 == per [0, 1] x * y == rep(x).ind = rep(y).ind => per [rep(x).ind, rep(x).elt * rep(y).elt] x = 1 => y y = 1 => x error "not same type" x ** p == per [rep(x).ind, rep(x).elt ** p]
if S has Group then inv(x) == per [rep(x).ind,inv(rep(x).elt)]
if S has AbelianMonoid then  represent zero of Sum(A,B) as 0$S 0 == per [0, 0] x + y == rep(x).ind = rep(y).ind => per [rep(x).ind, rep(x).elt + rep(y).elt] x = 0 => y y = 0 => x error "not same type" c * x == per [rep(x).ind, c * rep(x).elt]
if S has AbelianGroup then  x == per [rep(x).ind,rep(x).elt] (x  y):% == rep(x).ind = rep(y).ind => per [rep(x).ind, rep(x).elt  rep(y).elt] x = 0 => y y = 0 => x error "not same type"
d * x == per [rep(x).ind,d* rep(x).elt]
if S has OrderedAbelianMonoidSup then sup(x,y) == rep(x).ind = rep(y).ind => per [rep(x).ind, sup(rep(x).elt, rep(y).elt)] rep(x).ind < rep(y).ind => y x if S has OrderedSet then x < y == rep(x).ind = rep(y).ind => rep(x).elt < rep(y).elt rep(x).ind < rep(y).ind
Compiling FriCAS source code from file /var/zope2/var/LatexWiki/289934608984964194925px003.spad using old system compiler. COT abbreviates domain CoTuple  initializing NRLIB COT for CoTuple compiling into NRLIB COT compiling exported coerce : $ > S ****** comp fails at level 2 with expression: ****** error in function coerce
((rep x)  << elt >> ) ****** level 2 ****** $x:= elt $m:= $EmptyMode $f:= ((((x # #) (d #) (c #) (* #) ...)))
>> Apparent user error: cannot compile (rep x)
inj(1,10)
There are no library operations named inj Use HyperDoc Browse or issue )what op inj to learn if there is any operation containing " inj " in its name.
Cannot find a definition or applicable library operation named inj with argument type(s) PositiveInteger PositiveInteger
Perhaps you should use "@" to indicate the required return type,or "$" to specify which version of the function you need. inj(1, 10) < inj(2, 10)
There are no library operations named inj Use HyperDoc Browse or issue )what op inj to learn if there is any operation containing " inj " in its name.
Cannot find a definition or applicable library operation named inj with argument type(s) PositiveInteger PositiveInteger
Perhaps you should use "@" to indicate the required return type,or "$" to specify which version of the function you need. sup(inj(1, 99), inj(2, 10))$CoTuple(NNI)
CoTuple is an unknown constructor and so is unavailable. Did you mean to use > but type something different instead?
The DirectSum? domain constructor implements an associative (flat) DirectSum? domain that is the dual to DirectProduct?.
)abbrev domain DIRSUM DirectSum ++ This domain is intended to be the categorical dual of ++ DirectProduct (commadelimited homogeneous sequence of ++ values). As such it implements an nary disjoint union. DirectSum(S:Type): Type with coerce: S > % ++ any type is a 1ary union inj: (NonNegativeInteger,NonNegativeInteger, %) > % ++ inject(i, n, x) injects the mCoTuple element x as the ++ (m + i)th component of the (n+m)CoTuple. ind: % > NonNegativeInteger ++ index(x) returns the component number of x in the CoTuple len: % > NonNegativeInteger ++ len(x) returns the number of components if S has Monoid then Monoid if S has AbelianMonoid then AbelianMonoid if S has CancellationAbelianMonoid then CancellationAbelianMonoid if S has Group then Group if S has AbelianGroup then AbelianGroup if S has OrderedAbelianMonoidSup then OrderedAbelianMonoidSup if S has SetCategory then SetCategory if S has OrderedSet then OrderedSet == add Rep == Record(ind:NonNegativeInteger, len:NonNegativeInteger, elt:S) declarations x, y: % s: S i: NonNegativeInteger p: NonNegativeInteger c: PositiveInteger d: Integer
coerce(s:S):% == per [0,0, s] inj(i, n, x) == i < n => per [rep(x).len+i, rep(x).len+n, rep(x).elt] error "index out of bounds" ind(x) == rep(x).ind len(x) == rep(x).len
if S has SetCategory then x = y == (rep(x).ind = rep(y).ind) and (rep(x).elt = rep(y).elt) coerce(x : %): OutputForm == sub(coerce(rep(x).elt),coerce(rep(x).ind)) if S has Monoid then  represent unit of CoTuple(S) as 1$S of component 0 1 == per [0, 0, 1] x * y == rep(x).ind = rep(y).ind => per [rep(x).ind, rep(x).len, rep(x).elt * rep(y).elt] x = 1 => y y = 1 => x error "not same type" x ** p == per [rep(x).ind, rep(x).len, rep(x).elt ** p]
if S has Group then inv(x) == per [rep(x).ind,rep(x).len, inv(rep(x).elt)]
if S has AbelianMonoid then  represent zero of Sum(A,B) as 0$S 0 == per [0, 0, 0] x + y == rep(x).ind = rep(y).ind => per [rep(x).ind, rep(x).len, rep(x).elt + rep(y).elt] x = 0 => y y = 0 => x error "not same type" c * x == per [rep(x).ind, rep(x).len, c * rep(x).elt]
if S has AbelianGroup then  x == per [rep(x).ind,rep(x).len, rep(x).elt] (x  y):% == rep(x).ind = rep(y).ind => per [rep(x).ind, rep(x).len, rep(x).elt  rep(y).elt] x = 0 => y y = 0 => x error "not same type"
d * x == per [rep(x).ind,rep(x).len, d* rep(x).elt]
if S has OrderedAbelianMonoidSup then sup(x,y) == rep(x).ind = rep(y).ind => per [rep(x).ind, rep(x).len, sup(rep(x).elt, rep(y).elt)] rep(x).ind < rep(y).ind => y x if S has OrderedSet then x < y == rep(x).ind = rep(y).ind => rep(x).elt < rep(y).elt rep(x).ind < rep(y).ind
Compiling FriCAS source code from file /var/zope2/var/LatexWiki/475374031581685246125px005.spad using old system compiler. DIRSUM abbreviates domain DirectSum  initializing NRLIB DIRSUM for DirectSum compiling into NRLIB DIRSUM compiling exported coerce : S > $ ****** comp fails at level 2 with expression: ****** error in function coerce
(per  <<  (construct 0 0 s)  >> ) ****** level 2 ****** $x:= (construct (Zero) (Zero) s) $m:= $EmptyMode $f:= ((((s # #) (d #) (c #) (* #) ...)))
>> Apparent user error: not known that $ has (has S (AbelianMonoid))
inj(0,2, 10)
There are no library operations named inj Use HyperDoc Browse or issue )what op inj to learn if there is any operation containing " inj " in its name.
Cannot find a definition or applicable library operation named inj with argument type(s) NonNegativeInteger PositiveInteger PositiveInteger
Perhaps you should use "@" to indicate the required return type,or "$" to specify which version of the function you need. inj(0, 2, 10) < inj(1, 2, 10)
There are no library operations named inj Use HyperDoc Browse or issue )what op inj to learn if there is any operation containing " inj " in its name.
Cannot find a definition or applicable library operation named inj with argument type(s) NonNegativeInteger PositiveInteger PositiveInteger
Perhaps you should use "@" to indicate the required return type,or "$" to specify which version of the function you need. sup(inj(0, 2, 99), inj(1, 2, 10))$DirectSum(NNI)
DirectSum is an unknown constructor and so is unavailable. Did you mean to use > but type something different instead? a0:=inj(0,2, 'a)
There are no library operations named inj Use HyperDoc Browse or issue )what op inj to learn if there is any operation containing " inj " in its name.
Cannot find a definition or applicable library operation named inj with argument type(s) NonNegativeInteger PositiveInteger Variable(a)
Perhaps you should use "@" to indicate the required return type,or "$" to specify which version of the function you need. len(a0)
There are no library operations named len Use HyperDoc Browse or issue )what op len to learn if there is any operation containing " len " in its name.
Cannot find a definition or applicable library operation named len with argument type(s) Variable(a0)
Perhaps you should use "@" to indicate the required return type,or "$" to specify which version of the function you need. b1:=inj(1, 2, 'b)
There are no library operations named inj Use HyperDoc Browse or issue )what op inj to learn if there is any operation containing " inj " in its name.
Cannot find a definition or applicable library operation named inj with argument type(s) PositiveInteger PositiveInteger Variable(b)
Perhaps you should use "@" to indicate the required return type,or "$" to specify which version of the function you need. len(b1)
There are no library operations named len Use HyperDoc Browse or issue )what op len to learn if there is any operation containing " len " in its name.
Cannot find a definition or applicable library operation named len with argument type(s) Variable(b1)
Perhaps you should use "@" to indicate the required return type,or "$" to specify which version of the function you need. a2:=inj(0, 2, inj(0, 2, 'aa))
There are no library operations named inj Use HyperDoc Browse or issue )what op inj to learn if there is any operation containing " inj " in its name.
Cannot find a definition or applicable library operation named inj with argument type(s) NonNegativeInteger PositiveInteger Variable(aa)
Perhaps you should use "@" to indicate the required return type,or "$" to specify which version of the function you need. len(a2)
There are no library operations named len Use HyperDoc Browse or issue )what op len to learn if there is any operation containing " len " in its name.
Cannot find a definition or applicable library operation named len with argument type(s) Variable(a2)
Perhaps you should use "@" to indicate the required return type,or "$" to specify which version of the function you need. a3:=inj(1, 2, inj(0, 2, 'ba))
There are no library operations named inj Use HyperDoc Browse or issue )what op inj to learn if there is any operation containing " inj " in its name.
Cannot find a definition or applicable library operation named inj with argument type(s) NonNegativeInteger PositiveInteger Variable(ba)
Perhaps you should use "@" to indicate the required return type,or "$" to specify which version of the function you need. len(a3)
There are no library operations named len Use HyperDoc Browse or issue )what op len to learn if there is any operation containing " len " in its name.
Cannot find a definition or applicable library operation named len with argument type(s) Variable(a3)
Perhaps you should use "@" to indicate the required return type,or "$" to specify which version of the function you need. b2:=inj(0, 2, inj(1, 2, 'ab))
There are no library operations named inj Use HyperDoc Browse or issue )what op inj to learn if there is any operation containing " inj " in its name.
Cannot find a definition or applicable library operation named inj with argument type(s) PositiveInteger PositiveInteger Variable(ab)
Perhaps you should use "@" to indicate the required return type,or "$" to specify which version of the function you need. len(b2)
There are no library operations named len Use HyperDoc Browse or issue )what op len to learn if there is any operation containing " len " in its name.
Cannot find a definition or applicable library operation named len with argument type(s) Variable(b2)
Perhaps you should use "@" to indicate the required return type,or "$" to specify which version of the function you need. b3:=inj(1, 2, inj(1, 2, 'bb))
There are no library operations named inj Use HyperDoc Browse or issue )what op inj to learn if there is any operation containing " inj " in its name.
Cannot find a definition or applicable library operation named inj with argument type(s) PositiveInteger PositiveInteger Variable(bb)
Perhaps you should use "@" to indicate the required return type,or "$" to specify which version of the function you need. len(b3)
There are no library operations named len Use HyperDoc Browse or issue )what op len to learn if there is any operation containing " len " in its name.
Cannot find a definition or applicable library operation named len with argument type(s) Variable(b3)
Perhaps you should use "@" to indicate the required return type,or "$" to specify which version of the function you need. inj(2, 3, b3)
There are no library operations named inj Use HyperDoc Browse or issue )what op inj to learn if there is any operation containing " inj " in its name.
Cannot find a definition or applicable library operation named inj with argument type(s) PositiveInteger PositiveInteger Variable(b3)
Perhaps you should use "@" to indicate the required return type,or "$" to specify which version of the function you need.