|
|
|
last edited 12 years ago by test1 |
Edit detail for SandBoxSum revision 12 of 14
| 1 2 3 4 5 6 7 8 9 10 11 12 13 14 | ||
|
Editor: Bill Page
Time: 2008/08/29 11:42:34 GMT-7 |
||
| Note: DirectSum | ||
The Sum domain constructor is intended to be the Categorical Dual 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 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
spad
Compiling FriCAS source code from file
/var/zope2/var/LatexWiki/8219446594478290117-25px001.spad using
old system compiler.
SUM abbreviates domain Sum
------------------------------------------------------------------------
initializing NRLIB SUM for Sum
compiling into NRLIB SUM
importing Union(acomp: A,
(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 modeaxiom
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
spad
)abbrev domain COT CoTuple
++ This domain is intended to be the categorical dual of a
++ Tuple (comma-delimited homogeneous sequence of values).
++ As such it implements an n-ary disjoint union.
CoTuple(S:Type): CoercibleTo(S) with
inj: (NonNegativeInteger,
coerce(x:%):S == rep(x).elt
inj(i,
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),
if S has Group then
inv(x) == per [rep(x).ind,
if S has AbelianMonoid then
-- represent zero of Sum(A,
if S has AbelianGroup then
- x == per [rep(x).ind,
d * x == per [rep(x).ind,
if S has OrderedAbelianMonoidSup then
sup(x,
spad
Compiling FriCAS source code from file
/var/zope2/var/LatexWiki/2899346089849641949-25px003.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)axiom
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?.
spad
)abbrev domain DIRSUM DirectSum
++ This domain is intended to be the categorical dual of
++ DirectProduct (comma-delimited homogeneous sequence of
++ values). As such it implements an n-ary disjoint union.
DirectSum(S:Type): Type with
coerce: S -> %
++ any type is a 1-ary union
inj: (NonNegativeInteger,
coerce(s:S):% == per [0,
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),
if S has Group then
inv(x) == per [rep(x).ind,
if S has AbelianMonoid then
-- represent zero of Sum(A,
if S has AbelianGroup then
- x == per [rep(x).ind,
d * x == per [rep(x).ind,
if S has OrderedAbelianMonoidSup then
sup(x,
spad
Compiling FriCAS source code from file
/var/zope2/var/LatexWiki/4753740315816852461-25px005.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))axiom
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.