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

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)
rep x ==> (x@%) pretend Rep
per x ==> (x@Rep) pretend %
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
using old system compiler.
SUM abbreviates domain Sum
------------------------------------------------------------------------
initializing NRLIB SUM for Sum
compiling into NRLIB SUM
processing macro definition Rep ==> Union(acomp: A,bcomp: B)
processing macro definition rep x ==> pretend(@(x,$),Union(acomp: A,bcomp: B)) processing macro definition per x ==> pretend(@(x,Union(acomp: A,bcomp: B)),$)
importing Union(acomp: A,bcomp: B)
compiling exported coerce : $-> OutputForm ****** comp fails at level 5 with expression: ****** error in function coerce (SEQ (|:=| (|:| #1=#:G670 (|Boolean|)) (|case| (|pretend| (@ |x|$) (|Union| (|:| |acomp| A) (|:| |bcomp| B)))
|acomp|))
(|exit| 1
(IF #1#
(|sub|
(|coerce|
((|pretend| (@ |x| $) (|Union| (|:| |acomp| A) (|:| |bcomp| B))) |acomp|)) | << 1 >> |) (|sub| (|coerce| ((|pretend| (@ |x|$) (|Union| (|:| |acomp| A) (|:| |bcomp| B)))
|bcomp|))
"2"))))
****** level 5  ******
$x:= 1$m:= (OutputForm)
$f:= ((((#:G670 # #) (|x| # #) (|d| #) (|c| #) ...))) >> Apparent user error: Cannot coerce 1 of mode 1 to mode (OutputForm) fricas 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?

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)
rep x ==> (x@%) pretend Rep
per x ==> (x@Rep) pretend %
--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
using old system compiler.
COT abbreviates domain CoTuple
------------------------------------------------------------------------
initializing NRLIB COT for CoTuple
compiling into NRLIB COT
processing macro definition Rep ==> Record(ind: NonNegativeInteger,elt: S)
processing macro definition rep x ==> pretend(@(x,$),Record(ind: NonNegativeInteger,elt: S)) processing macro definition per x ==> pretend(@(x,Record(ind: NonNegativeInteger,elt: S)),$)
compiling exported coerce : $-> S COT;coerce;$S;1 is replaced by QCDR
Time: 0.01 SEC.
compiling exported inj : (NonNegativeInteger,S) -> $COT;inj;NniS$;2 is replaced by CONS
Time: 0 SEC.
compiling exported ind : $-> NonNegativeInteger COT;ind;$Nni;3 is replaced by QCAR
Time: 0 SEC.
****** Domain: S already in scope
augmenting S: (SetCategory)
compiling exported = : ($,$) -> Boolean
Time: 0 SEC.
compiling exported coerce : $-> OutputForm Time: 0 SEC. ****** Domain: S already in scope augmenting S: (Monoid) compiling exported One : () ->$
Time: 0 SEC.
compiling exported * : ($,$) -> $Time: 0 SEC. compiling exported ^ : ($,NonNegativeInteger) -> $Time: 0 SEC. ****** Domain: S already in scope augmenting S: (Group) compiling exported inv :$ -> $Time: 0 SEC. ****** Domain: S already in scope augmenting S: (AbelianMonoid) compiling exported Zero : () ->$
Time: 0 SEC.
compiling exported + : ($,$) -> $Time: 0 SEC. compiling exported * : (PositiveInteger,$) -> $Time: 0 SEC. ****** Domain: S already in scope augmenting S: (AbelianGroup) compiling exported - :$ -> $Time: 0 SEC. compiling exported - : ($,$) ->$
Time: 0 SEC.
compiling exported * : (Integer,$) ->$
Time: 0 SEC.
****** Domain: S already in scope
augmenting S: (OrderedAbelianMonoidSup)
compiling exported sup : ($,$) -> $Time: 0.01 SEC. ****** Domain: S already in scope augmenting S: (OrderedSet) compiling exported < : ($,$) -> Boolean Time: 0 SEC. ****** Domain: S already in scope augmenting S: (AbelianGroup) ****** Domain: S already in scope augmenting S: (AbelianMonoid) ****** Domain: S already in scope augmenting S: (CancellationAbelianMonoid) ****** Domain: S already in scope augmenting S: (Group) ****** Domain: S already in scope augmenting S: (Monoid) ****** Domain: S already in scope augmenting S: (OrderedAbelianMonoidSup) ****** Domain: S already in scope augmenting S: (OrderedSet) ****** Domain: S already in scope augmenting S: (SetCategory) (time taken in buildFunctor: 10) ;;; *** |CoTuple| REDEFINED ;;; *** |CoTuple| REDEFINED Time: 0.01 SEC. Cumulative Statistics for Constructor CoTuple Time: 0.03 seconds finalizing NRLIB COT Processing CoTuple for Browser database: --------constructor--------- --------(inj (% (NonNegativeInteger) S))--------- --->-->CoTuple((inj (% (NonNegativeInteger) S))): Improper first word in comments: inject "inject(\\spad{x},{}\\spad{n}) returns \\spad{x} as an element of the \\spad{n}-th component of the CoTuple. CoTuples are 0-based" --------(ind ((NonNegativeInteger) %))--------- --->-->CoTuple((ind ((NonNegativeInteger) %))): Improper first word in comments: index "index(\\spad{x}) returns the component number of \\spad{x} in the CoTuple" ; compiling file "/var/aw/var/LatexWiki/COT.NRLIB/COT.lsp" (written 04 APR 2022 06:58:01 PM): ; /var/aw/var/LatexWiki/COT.NRLIB/COT.fasl written ; compilation finished in 0:00:00.052 ------------------------------------------------------------------------ CoTuple is now explicitly exposed in frame initial CoTuple will be automatically loaded when needed from /var/aw/var/LatexWiki/COT.NRLIB/COT fricas inj(1,10)  (1) Type: CoTuple?(PositiveInteger?) fricas inj(1,10) < inj(2,10)  (2) Type: Boolean fricas sup(inj(1,99), inj(2,10))$CoTuple(NNI)
 (3)
Type: CoTuple?(NonNegativeInteger?)

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)
rep x ==> (x@%) pretend Rep
per x ==> (x@Rep) pretend %
--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
using old system compiler.
DIRSUM abbreviates domain DirectSum
------------------------------------------------------------------------
initializing NRLIB DIRSUM for DirectSum
compiling into NRLIB DIRSUM
processing macro definition Rep ==> Record(ind: NonNegativeInteger,len: NonNegativeInteger,elt: S)
processing macro definition rep x ==> pretend(@(x,$),Record(ind: NonNegativeInteger,len: NonNegativeInteger,elt: S)) processing macro definition per x ==> pretend(@(x,Record(ind: NonNegativeInteger,len: NonNegativeInteger,elt: S)),$)
compiling exported coerce : S -> $DIRSUM;coerce;S$;1 is replaced by VECTOR00s
Time: 0 SEC.
compiling exported inj : (NonNegativeInteger,NonNegativeInteger,$) ->$
Time: 0.01 SEC.
compiling exported ind : $-> NonNegativeInteger DIRSUM;ind;$Nni;3 is replaced by QVELTx0
Time: 0 SEC.
compiling exported len : $-> NonNegativeInteger DIRSUM;len;$Nni;4 is replaced by QVELTx1
Time: 0 SEC.
****** Domain: S already in scope
augmenting S: (SetCategory)
compiling exported = : ($,$) -> Boolean
Time: 0 SEC.
compiling exported coerce : $-> OutputForm Time: 0 SEC. ****** Domain: S already in scope augmenting S: (Monoid) compiling exported One : () ->$
Time: 0 SEC.
compiling exported * : ($,$) -> $Time: 0 SEC. compiling exported ^ : ($,NonNegativeInteger) -> $Time: 0 SEC. ****** Domain: S already in scope augmenting S: (Group) compiling exported inv :$ -> $Time: 0 SEC. ****** Domain: S already in scope augmenting S: (AbelianMonoid) compiling exported Zero : () ->$
Time: 0 SEC.
compiling exported + : ($,$) -> $Time: 0 SEC. compiling exported * : (PositiveInteger,$) -> $Time: 0 SEC. ****** Domain: S already in scope augmenting S: (AbelianGroup) compiling exported - :$ -> $Time: 0 SEC. compiling exported - : ($,$) ->$
Time: 0.01 SEC.
compiling exported * : (Integer,$) ->$
Time: 0.01 SEC.
****** Domain: S already in scope
augmenting S: (OrderedAbelianMonoidSup)
compiling exported sup : ($,$) -> $Time: 0 SEC. ****** Domain: S already in scope augmenting S: (OrderedSet) compiling exported < : ($,$) -> Boolean Time: 0 SEC. ****** Domain: S already in scope augmenting S: (AbelianGroup) ****** Domain: S already in scope augmenting S: (AbelianMonoid) ****** Domain: S already in scope augmenting S: (CancellationAbelianMonoid) ****** Domain: S already in scope augmenting S: (Group) ****** Domain: S already in scope augmenting S: (Monoid) ****** Domain: S already in scope augmenting S: (OrderedAbelianMonoidSup) ****** Domain: S already in scope augmenting S: (OrderedSet) ****** Domain: S already in scope augmenting S: (SetCategory) (time taken in buildFunctor: 10) ;;; *** |DirectSum| REDEFINED ;;; *** |DirectSum| REDEFINED Time: 0.01 SEC. Cumulative Statistics for Constructor DirectSum Time: 0.04 seconds finalizing NRLIB DIRSUM Processing DirectSum for Browser database: --------constructor--------- --------(coerce (% S))--------- --->-->DirectSum((coerce (% S))): Improper first word in comments: any "any type is a 1-ary union" --------(inj (% (NonNegativeInteger) (NonNegativeInteger) %))--------- --->-->DirectSum((inj (% (NonNegativeInteger) (NonNegativeInteger) %))): Improper first word in comments: inject "inject(\\spad{i},{}\\spad{n},{}\\spad{x}) injects the \\spad{m}-CoTuple element \\spad{x} as the (\\spad{m} + \\spad{i})\\spad{-}th component of the (\\spad{n+m})-CoTuple." --------(ind ((NonNegativeInteger) %))--------- --->-->DirectSum((ind ((NonNegativeInteger) %))): Improper first word in comments: index "index(\\spad{x}) returns the component number of \\spad{x} in the CoTuple" --------(len ((NonNegativeInteger) %))--------- ; compiling file "/var/aw/var/LatexWiki/DIRSUM.NRLIB/DIRSUM.lsp" (written 04 APR 2022 06:58:01 PM): ; /var/aw/var/LatexWiki/DIRSUM.NRLIB/DIRSUM.fasl written ; compilation finished in 0:00:00.067 ------------------------------------------------------------------------ DirectSum is now explicitly exposed in frame initial DirectSum will be automatically loaded when needed from /var/aw/var/LatexWiki/DIRSUM.NRLIB/DIRSUM fricas inj(0,2,10)  (4) Type: DirectSum?(Integer) fricas inj(0,2,10) < inj(1,2,10)  (5) Type: Boolean fricas sup(inj(0,2,99), inj(1,2,10))$DirectSum(NNI)
 (6)
Type: DirectSum?(NonNegativeInteger?)
fricas
a0:=inj(0,2,'a)
 (7)
Type: DirectSum?(Polynomial(Integer))
fricas
len(a0)
 (8)
Type: PositiveInteger?
fricas
b1:=inj(1,2,'b)
 (9)
Type: DirectSum?(Polynomial(Integer))
fricas
len(b1)
 (10)
Type: PositiveInteger?
fricas
a2:=inj(0,2,inj(0,2,'aa))
 (11)
Type: DirectSum?(Polynomial(Integer))
fricas
len(a2)
 (12)
Type: PositiveInteger?
fricas
a3:=inj(1,2,inj(0,2,'ba))
 (13)
Type: DirectSum?(Polynomial(Integer))
fricas
len(a3)
 (14)
Type: PositiveInteger?
fricas
b2:=inj(0,2,inj(1,2,'ab))
 (15)
Type: DirectSum?(Polynomial(Integer))
fricas
len(b2)
 (16)
Type: PositiveInteger?
fricas
b3:=inj(1,2,inj(1,2,'bb))
 (17)
Type: DirectSum?(Polynomial(Integer))
fricas
len(b3)
 (18)
Type: PositiveInteger?
fricas
inj(2,3,b3)
 (19)
Type: DirectSum?(Polynomial(Integer))

 Subject:   Be Bold !! ( 15 subscribers )