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

# 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

```)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
--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
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```

axiom
```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 (comma-delimited homogeneous sequence of values).
++ As such it implements an n-ary disjoint union.
CoTuple(S:Type): CoercibleTo(S) with
inj: (NonNegativeInteger,S) -> %
++ inject(x,n) returns x as an element of the n-th
++ component of the CoTuple. CoTuples are 0-based
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
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
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?.

```)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,NonNegativeInteger,%) -> %
++ inject(i,n,x) injects the m-CoTuple 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
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
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.```