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

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) 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
   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
Time: 0.02 SEC.
compiling exported = : ($,$) -> Boolean Time: 0 SEC.
compiling exported selectsum : $ -> Union(acomp: A,bcomp: B) SUM;selectsum;$U;3 is replaced by x Time: 0 SEC.
compiling exported in1 : A -> $ SUM;in1;A$;4 is replaced by CONS0a Time: 0 SEC.
compiling exported in2 : B -> $ SUM;in2;B$;5 is replaced by CONS1b Time: 0 SEC.
****** Domain: A already in scope augmenting A: (Monoid) ****** Domain: B already in scope augmenting B: (Monoid) compiling exported One : () -> $ Time: 0 SEC.
compiling exported * : ($,$) -> $ Time: 0.01 SEC.
compiling exported ^ : ($,NonNegativeInteger) -> $ Time: 0.01 SEC.
****** Domain: A already in scope augmenting A: (Finite) ****** Domain: B already in scope augmenting B: (Finite) compiling exported size : () -> NonNegativeInteger Time: 0 SEC.
compiling exported index : PositiveInteger -> $ Time: 0 SEC.
compiling exported random : () -> $ Time: 0 SEC.
compiling exported lookup : $ -> PositiveInteger Time: 0 SEC.
compiling exported hash : $ -> SingleInteger Time: 0 SEC.
****** Domain: A already in scope augmenting A: (Group) ****** Domain: B already in scope augmenting B: (Group) compiling exported inv : $ -> $ Time: 0 SEC.
****** Domain: A already in scope augmenting A: (AbelianMonoid) ****** Domain: B already in scope augmenting B: (AbelianMonoid) compiling exported Zero : () -> $ Time: 0 SEC.
compiling exported + : ($,$) -> $ Time: 0 SEC.
compiling exported * : (PositiveInteger,$) -> $ Time: 0.01 SEC.
****** Domain: A already in scope augmenting A: (AbelianGroup) ****** Domain: B already in scope augmenting B: (AbelianGroup) compiling exported - : $ -> $ Time: 0.01 SEC.
compiling exported - : ($,$) -> $ Time: 0.01 SEC.
compiling exported * : (Integer,$) -> $ Time: 0.01 SEC.
****** Domain: A already in scope augmenting A: (OrderedAbelianMonoidSup) ****** Domain: B already in scope augmenting B: (OrderedAbelianMonoidSup) compiling exported sup : ($,$) -> $ Time: 0.01 SEC.
****** Domain: A already in scope augmenting A: (OrderedSet) ****** Domain: B already in scope augmenting B: (OrderedSet) compiling exported < : ($,$) -> Boolean Time: 0 SEC.
****** Domain: A already in scope augmenting A: (AbelianGroup) ****** Domain: B already in scope augmenting B: (AbelianGroup) ****** Domain: A already in scope augmenting A: (Finite) ****** Domain: B already in scope augmenting B: (Finite) ****** Domain: A already in scope augmenting A: (Group) ****** Domain: B already in scope augmenting B: (Group) ****** Domain: A already in scope augmenting A: (OrderedAbelianMonoidSup) ****** Domain: B already in scope augmenting B: (OrderedAbelianMonoidSup) (time taken in buildFunctor: 10)
;;; *** |Sum| REDEFINED
;;; *** |Sum| REDEFINED Time: 0.02 SEC.
Warnings: [1] coerce: acomp has no value [2] coerce: bcomp has no value [3] in1: cannot pretend (@ (construct a) (Union (: acomp A) (: bcomp B))) of mode (Union (: acomp A) (: bcomp B)) to mode $ [4] in2: cannot pretend (@ (construct b) (Union (: acomp A) (: bcomp B))) of mode (Union (: acomp A) (: bcomp B)) to mode $ [5] One: cannot pretend (@ (construct (elt A (One))) (Union (: acomp A) (: bcomp B))) of mode (Union (: acomp A) (: bcomp B)) to mode $ [6] *: acomp has no value [7] *: cannot pretend (@ (construct (* ((pretend (@ x $) (Union (: acomp A) (: bcomp B))) acomp) ((pretend (@ y $) (Union (: acomp A) (: bcomp B))) acomp))) (Union (: acomp A) (: bcomp B))) of mode (Union (: acomp A) (: bcomp B)) to mode $ [8] *: cannot pretend (@ (construct (* ((pretend (@ x $) (Union (: acomp A) (: bcomp B))) bcomp) ((pretend (@ y $) (Union (: acomp A) (: bcomp B))) bcomp))) (Union (: acomp A) (: bcomp B))) of mode (Union (: acomp A) (: bcomp B)) to mode $ [9] ^: acomp has no value [10] ^: cannot pretend (@ (construct (^ ((pretend (@ x $) (Union (: acomp A) (: bcomp B))) acomp) p)) (Union (: acomp A) (: bcomp B))) of mode (Union (: acomp A) (: bcomp B)) to mode $ [11] ^: cannot pretend (@ (construct (^ ((pretend (@ x $) (Union (: acomp A) (: bcomp B))) bcomp) p)) (Union (: acomp A) (: bcomp B))) of mode (Union (: acomp A) (: bcomp B)) to mode $ [12] index: cannot pretend (@ (construct ((elt A index) (:: (- (:: n (Integer)) (elt B size)) (PositiveInteger)))) (Union (: acomp A) (: bcomp B))) of mode (Union (: acomp A) (: bcomp B)) to mode $ [13] index: cannot pretend (@ (construct ((elt B index) n)) (Union (: acomp A) (: bcomp B))) of mode (Union (: acomp A) (: bcomp B)) to mode $ [14] random: cannot pretend (@ (construct ((elt A random))) (Union (: acomp A) (: bcomp B))) of mode (Union (: acomp A) (: bcomp B)) to mode $ [15] random: cannot pretend (@ (construct ((elt B random))) (Union (: acomp A) (: bcomp B))) of mode (Union (: acomp A) (: bcomp B)) to mode $ [16] inv: acomp has no value [17] inv: cannot pretend (@ (construct (inv ((pretend (@ x $) (Union (: acomp A) (: bcomp B))) acomp))) (Union (: acomp A) (: bcomp B))) of mode (Union (: acomp A) (: bcomp B)) to mode $ [18] inv: cannot pretend (@ (construct (inv ((pretend (@ x $) (Union (: acomp A) (: bcomp B))) bcomp))) (Union (: acomp A) (: bcomp B))) of mode (Union (: acomp A) (: bcomp B)) to mode $ [19] Zero: cannot pretend (@ (construct (elt A (Zero))) (Union (: acomp A) (: bcomp B))) of mode (Union (: acomp A) (: bcomp B)) to mode $ [20] +: acomp has no value [21] +: cannot pretend (@ (construct (+ ((pretend (@ x $) (Union (: acomp A) (: bcomp B))) acomp) ((pretend (@ y $) (Union (: acomp A) (: bcomp B))) acomp))) (Union (: acomp A) (: bcomp B))) of mode (Union (: acomp A) (: bcomp B)) to mode $ [22] +: cannot pretend (@ (construct (+ ((pretend (@ x $) (Union (: acomp A) (: bcomp B))) bcomp) ((pretend (@ y $) (Union (: acomp A) (: bcomp B))) bcomp))) (Union (: acomp A) (: bcomp B))) of mode (Union (: acomp A) (: bcomp B)) to mode $ [23] *: cannot pretend (@ (construct (* c ((pretend (@ x $) (Union (: acomp A) (: bcomp B))) acomp))) (Union (: acomp A) (: bcomp B))) of mode (Union (: acomp A) (: bcomp B)) to mode $ [24] *: cannot pretend (@ (construct (* c ((pretend (@ x $) (Union (: acomp A) (: bcomp B))) bcomp))) (Union (: acomp A) (: bcomp B))) of mode (Union (: acomp A) (: bcomp B)) to mode $ [25] -: acomp has no value [26] -: cannot pretend (@ (construct (- ((pretend (@ x $) (Union (: acomp A) (: bcomp B))) acomp))) (Union (: acomp A) (: bcomp B))) of mode (Union (: acomp A) (: bcomp B)) to mode $ [27] -: cannot pretend (@ (construct (- ((pretend (@ x $) (Union (: acomp A) (: bcomp B))) bcomp))) (Union (: acomp A) (: bcomp B))) of mode (Union (: acomp A) (: bcomp B)) to mode $ [28] -: cannot pretend (@ (construct (- ((pretend (@ x $) (Union (: acomp A) (: bcomp B))) acomp) ((pretend (@ y $) (Union (: acomp A) (: bcomp B))) acomp))) (Union (: acomp A) (: bcomp B))) of mode (Union (: acomp A) (: bcomp B)) to mode $ [29] -: cannot pretend (@ (construct (- ((pretend (@ x $) (Union (: acomp A) (: bcomp B))) bcomp) ((pretend (@ y $) (Union (: acomp A) (: bcomp B))) bcomp))) (Union (: acomp A) (: bcomp B))) of mode (Union (: acomp A) (: bcomp B)) to mode $ [30] *: cannot pretend (@ (construct (* d ((pretend (@ x $) (Union (: acomp A) (: bcomp B))) acomp))) (Union (: acomp A) (: bcomp B))) of mode (Union (: acomp A) (: bcomp B)) to mode $ [31] *: cannot pretend (@ (construct (* d ((pretend (@ x $) (Union (: acomp A) (: bcomp B))) bcomp))) (Union (: acomp A) (: bcomp B))) of mode (Union (: acomp A) (: bcomp B)) to mode $ [32] sup: acomp has no value [33] sup: cannot pretend (@ (construct (sup ((pretend (@ x $) (Union (: acomp A) (: bcomp B))) acomp) ((pretend (@ y $) (Union (: acomp A) (: bcomp B))) acomp))) (Union (: acomp A) (: bcomp B))) of mode (Union (: acomp A) (: bcomp B)) to mode $ [34] sup: cannot pretend (@ (construct (sup ((pretend (@ x $) (Union (: acomp A) (: bcomp B))) bcomp) ((pretend (@ y $) (Union (: acomp A) (: bcomp B))) bcomp))) (Union (: acomp A) (: bcomp B))) of mode (Union (: acomp A) (: bcomp B)) to mode $ [35] <: acomp has no value [36] <: bcomp has no value
Cumulative Statistics for Constructor Sum Time: 0.11 seconds
finalizing NRLIB SUM Processing Sum for Browser database: --------constructor--------- --------(selectsum ((Union (: acomp A) (: bcomp B)) %))--------- --------(in1 (% A))--------- --->-->Sum((in1 (% A))): Improper first word in comments: makefirst "makefirst(a) \\undocumented" --------(in2 (% B))--------- --->-->Sum((in2 (% B))): Improper first word in comments: makesecond "makesecond(\\spad{b}) \\undocumented" ; compiling file "/var/aw/var/LatexWiki/SUM.NRLIB/SUM.lsp" (written 31 JUL 2013 04:46:24 PM):
; /var/aw/var/LatexWiki/SUM.NRLIB/SUM.fasl written ; compilation finished in 0:00:00.107 ------------------------------------------------------------------------ Sum is now explicitly exposed in frame initial Sum will be automatically loaded when needed from /var/aw/var/LatexWiki/SUM.NRLIB/SUM

fricas
size()$Sum(PF 7,PF 13)

\label{eq1}20(1)
fricas
size()$Sum(PF 7,Product(PF 3,PF 13))

\label{eq2}46(2)
fricas
in1(10)$Sum(Integer,Integer)

\label{eq3}{10}_{1}(3)
Type: Sum(Integer,Integer)
fricas
in1(10)$Sum(Integer,Integer) < in2(10)$Sum(Integer,Integer)

\label{eq4} \mbox{\rm true} (4)
Type: Boolean
fricas
sup(in1(99)$Sum(NNI,NNI), in2(10)$Sum(NNI,NNI))

\label{eq5}{10}_{2}(5)

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.01 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.01 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: 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 31 JUL 2013 04:46:24 PM):
; /var/aw/var/LatexWiki/COT.NRLIB/COT.fasl written ; compilation finished in 0:00:00.054 ------------------------------------------------------------------------ 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)

\label{eq6}{10}_{1}(6)
Type: CoTuple?(PositiveInteger)
fricas
inj(1,10) < inj(2,10)

\label{eq7} \mbox{\rm true} (7)
Type: Boolean
fricas
sup(inj(1,99), inj(2,10))$CoTuple(NNI)

\label{eq8}{10}_{2}(8)
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.01 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: 10)
;;; *** |DirectSum| REDEFINED
;;; *** |DirectSum| REDEFINED Time: 0.01 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 31 JUL 2013 04:46:24 PM):
; /var/aw/var/LatexWiki/DIRSUM.NRLIB/DIRSUM.fasl written ; compilation finished in 0:00:00.083 ------------------------------------------------------------------------ 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)

\label{eq9}{10}_{0}(9)
Type: DirectSum?(Integer)
fricas
inj(0,2,10) < inj(1,2,10)

\label{eq10} \mbox{\rm true} (10)
Type: Boolean
fricas
sup(inj(0,2,99), inj(1,2,10))$DirectSum(NNI)

\label{eq11}{10}_{1}(11)
Type: DirectSum?(NonNegativeInteger)
fricas
a0:=inj(0,2,'a)

\label{eq12}a_{0}(12)
Type: DirectSum?(Polynomial(Integer))
fricas
len(a0)

\label{eq13}2(13)
fricas
b1:=inj(1,2,'b)

\label{eq14}b_{1}(14)
Type: DirectSum?(Polynomial(Integer))
fricas
len(b1)

\label{eq15}2(15)
fricas
a2:=inj(0,2,inj(0,2,'aa))

\label{eq16}aa_{2}(16)
Type: DirectSum?(Polynomial(Integer))
fricas
len(a2)

\label{eq17}4(17)
fricas
a3:=inj(1,2,inj(0,2,'ba))

\label{eq18}ba_{3}(18)
Type: DirectSum?(Polynomial(Integer))
fricas
len(a3)

\label{eq19}4(19)
fricas
b2:=inj(0,2,inj(1,2,'ab))

\label{eq20}ab_{2}(20)
Type: DirectSum?(Polynomial(Integer))
fricas
len(b2)

\label{eq21}4(21)
fricas
b3:=inj(1,2,inj(1,2,'bb))

\label{eq22}bb_{3}(22)
Type: DirectSum?(Polynomial(Integer))
fricas
len(b3)

\label{eq23}4(23)
fricas
inj(2,3,b3)

\label{eq24}bb_{6}(24)
Type: DirectSum?(Polynomial(Integer))




  Subject:   Be Bold !!
  ( 13 subscribers )  
Please rate this page: