|
The Sum domain constructor is intended to be the
Categorical Dual
of the Product
domain constructor
fricas (1) -> <spad>
fricas )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)
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</spad>
fricas Compiling FriCAS source code from file
/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/6614319580939889182-25px001.spad
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=#:G0 (|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:=
((((#:G0 # #) (|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
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,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
== add
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
spad Compiling FriCAS source code from file
/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/2750494589739067594-25px003.spad
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 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 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: 0)
;;; *** |CoTuple| REDEFINED
;;; *** |CoTuple| REDEFINED
Time: 0 SEC.
Cumulative Statistics for Constructor CoTuple
Time: 0.01 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 22 NOV 2024 06:24:51 AM):
; wrote /var/aw/var/LatexWiki/COT.NRLIB/COT.fasl
; compilation finished in 0:00:00.028
------------------------------------------------------------------------
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)
Type: CoTuple ?(PositiveInteger ?)
fricas inj(1,10) < inj(2,10)
Type: Boolean
fricas sup(inj(1,99), inj(2,10))$CoTuple(NNI)
Type: CoTuple ?(NonNegativeInteger ?)
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,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
== add
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
spad Compiling FriCAS source code from file
/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/5742852776520408994-25px005.spad
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 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 SEC.
compiling exported * : (Integer,%) -> %
Time: 0 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: 736)
;;; *** |DirectSum| REDEFINED
;;; *** |DirectSum| REDEFINED
Time: 0 SEC.
Cumulative Statistics for Constructor DirectSum
Time: 0.02 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 22 NOV 2024 06:24:51 AM):
; wrote /var/aw/var/LatexWiki/DIRSUM.NRLIB/DIRSUM.fasl
; compilation finished in 0:00:00.032
------------------------------------------------------------------------
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)
Type: DirectSum ?(Integer)
fricas inj(0,2,10) < inj(1,2,10)
Type: Boolean
fricas sup(inj(0,2,99), inj(1,2,10))$DirectSum(NNI)
Type: DirectSum ?(NonNegativeInteger ?)
fricas a0:=inj(0,2,'a)
Type: DirectSum ?(Polynomial(Integer))
fricas len(a0)
fricas b1:=inj(1,2,'b)
Type: DirectSum ?(Polynomial(Integer))
fricas len(b1)
fricas a2:=inj(0,2,inj(0,2,'aa))
Type: DirectSum ?(Polynomial(Integer))
fricas len(a2)
fricas a3:=inj(1,2,inj(0,2,'ba))
Type: DirectSum ?(Polynomial(Integer))
fricas len(a3)
fricas b2:=inj(0,2,inj(1,2,'ab))
Type: DirectSum ?(Polynomial(Integer))
fricas len(b2)
fricas b3:=inj(1,2,inj(1,2,'bb))
Type: DirectSum ?(Polynomial(Integer))
fricas len(b3)
fricas inj(2,3,b3)
Type: DirectSum ?(Polynomial(Integer))
|