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

Edit detail for SandBoxSum revision 9 of 14

 1 2 3 4 5 6 7 8 9 10 11 12 13 14 Editor: Bill Page Time: 2008/08/28 17:55:09 GMT-7 Note: CoTuple

changed:
-       selectsum(x:%) == rep(x)
-       in1(a:A):%   == per [a]
-       in2(b:B): % == per [b]
selectsum(x) == rep(x)
in1(a) == per [a]
in2(b) == per [b]

changed:
-                   rep(x) case acomp and rep(x).acomp=1$A and rep(y) case bcomp => y x=1 => y y=1 => x changed: - rep(x) case acomp and x=0 and rep(y) case bcomp => y - rep(x) case bcomp and y=0 and rep(y) case acomp => x x=0 => y y=0 => x changed: - - x == -x == changed: - rep(x) case acomp and x=0 and rep(y) case bcomp => - y - rep(x) case bcomp and y=0 and rep(y) case acomp => x x=0 => -y y=0 => x changed: - rep(x) case acomp and rep(y) case bcomp => true - false - rep(x) case acomp and rep(y) case bcomp added: The CoTuple domain constructor is intended to be the "Categorical Dual":http://en.wikipedia.org/wiki/Dual_(category_theory) of the "Tuple":/axiom--test--1/src/algebra/Array1Spad domain constructor \begin{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) --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 \end{spad} \begin{axiom} inj(1,10) inj(1,10) < inj(2,10) sup(inj(1,99), inj(2,10))$CoTuple(NNI)
\end{axiom}



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 OpenAxiom source code from file
SUM abbreviates domain Sum
------------------------------------------------------------------------
initializing NRLIB SUM for Sum
compiling into NRLIB SUM
compiling local rep : % -> Union(acomp: A,bcomp: B)
SUM;rep is replaced by G1424
Time: 0.01 SEC.
compiling local per : Union(acomp: A,bcomp: B) -> %
SUM;per is replaced by G1424
Time: 0 SEC.
importing Rep
compiling exported coerce : % -> OutputForm
Time: 0.01 SEC.
compiling exported = : (%,%) -> Boolean
Time: 0 SEC.
compiling exported selectsum : % -> Union(acomp: A,bcomp: B)
Time: 0 SEC.
compiling exported in1 : A -> %
Time: 0 SEC.
compiling exported in2 : B -> %
Time: 0 SEC.
****** Domain: A already in scope
augmenting A: (Monoid)
****** Domain: B already in scope
augmenting B: (Monoid)
compiling exported One : () -> %
Time: 0.01 SEC.
compiling exported * : (%,%) -> %
Time: 0.07 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.01 SEC.
compiling exported index : PositiveInteger -> %
Time: 0 SEC.
compiling exported random : () -> %
Time: 0 SEC.
compiling exported lookup : % -> PositiveInteger
Time: 0.01 SEC.
compiling exported hash : % -> SingleInteger
Time: 0.01 SEC.
****** Domain: A already in scope
augmenting A: (Group)
****** Domain: B already in scope
augmenting B: (Group)
compiling exported inv : % -> %
Time: 0.01 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.02 SEC.
compiling exported * : (PositiveInteger,%) -> %
Time: 0.07 SEC.
****** Domain: A already in scope
augmenting A: (AbelianGroup)
****** Domain: B already in scope
augmenting B: (AbelianGroup)
compiling exported - : % -> %
Time: 0.02 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.02 SEC.
****** Domain: A already in scope
augmenting A: (OrderedSet)
****** Domain: B already in scope
augmenting B: (OrderedSet)
compiling exported < : (%,%) -> Boolean
Time: 0.02 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)
****** Domain: A already in scope
augmenting A: (AbelianGroup)
****** Domain: B already in scope
augmenting B: (AbelianGroup)
****** Domain: A already in scope
augmenting A: (AbelianGroup)
****** Domain: B already in scope
augmenting B: (AbelianGroup)
****** Domain: A already in scope
augmenting A: (AbelianGroup)
****** Domain: B already in scope
augmenting B: (AbelianGroup)
****** 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:  2)
;;;     ***       |Sum| REDEFINED
;;;     ***       |Sum| REDEFINED
Time: 0.10 SEC.
Warnings:
[1] coerce:  acomp has no value
[2] coerce:  bcomp has no value
[3] *:  acomp has no value
[4] *:  bcomp has no value
[5] **:  acomp has no value
[6] **:  bcomp has no value
[7] lookup:  acomp has no value
[8] lookup:  bcomp has no value
[9] hash:  acomp has no value
[10] hash:  bcomp has no value
[11] inv:  acomp has no value
[12] inv:  bcomp has no value
[13] +:  acomp has no value
[14] +:  bcomp has no value
[15] -:  acomp has no value
[16] -:  bcomp has no value
[17] sup:  acomp has no value
[18] sup:  bcomp has no value
[19] <:  acomp has no value
[20] <:  bcomp has no value
Cumulative Statistics for Constructor Sum
Time: 0.42 seconds
finalizing NRLIB SUM
Processing Sum for Browser database:
-- selectsum : % -> Union(acomp: A,bcomp: B)
--->-->Sum((selectsum ((Union (: acomp A) (: bcomp B)) %))): Unexpected HT command: \spad
-- 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
-- constructor
------------------------------------------------------------------------
Sum is now explicitly exposed in frame initial
Sum will be automatically loaded when needed from
/var/zope2/var/LatexWiki/SUM.NRLIB/code.o

axiom
size()$Sum(PF 7,PF 13)  (1) Type: NonNegativeInteger? axiom size()$Sum(PF 7,Product(PF 3,PF 13))
 (2)
Type: NonNegativeInteger?
axiom
in1(10)$Sum(Integer,Integer)  (3) Type: Sum(Integer,Integer) axiom in1(10)$Sum(Integer,Integer) < in2(10)$Sum(Integer,Integer)  (4) Type: Boolean axiom sup(in1(99)$Sum(NNI,NNI), in2(10)$Sum(NNI,NNI))  (5) Type: Sum(NonNegativeInteger?,NonNegativeInteger?) 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) --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 OpenAxiom source code from file /var/zope2/var/LatexWiki/2899346089849641949-25px003.spad using Spad compiler. COT abbreviates domain CoTuple ------------------------------------------------------------------------ initializing NRLIB COT for CoTuple compiling into NRLIB COT compiling local rep : % -> Record(ind: NonNegativeInteger,elt: S) COT;rep is replaced by G1625 Time: 0 SEC. compiling local per : Record(ind: NonNegativeInteger,elt: S) -> % COT;per is replaced by G1625 Time: 0 SEC. compiling exported coerce : % -> S Time: 0.01 SEC. compiling exported inj : (NonNegativeInteger,S) -> % Time: 0 SEC. compiling exported ind : % -> NonNegativeInteger Time: 0 SEC. ****** Domain: S already in scope augmenting S: (SetCategory) compiling exported = : (%,%) -> Boolean Time: 0.01 SEC. compiling exported coerce : % -> OutputForm Time: 0.02 SEC. ****** Domain: S already in scope augmenting S: (Monoid) compiling exported One : () -> % Time: 0 SEC. compiling exported * : (%,%) -> % Time: 0.02 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.01 SEC. compiling exported + : (%,%) -> % Time: 0.01 SEC. compiling exported * : (PositiveInteger,%) -> % Time: 0 SEC. ****** Domain: S already in scope augmenting S: (AbelianGroup) compiling exported - : % -> % Time: 0 SEC. compiling exported - : (%,%) -> % Time: 0.02 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.02 SEC. ****** Domain: S already in scope augmenting S: (AbelianMonoid) ****** 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: 1) ;;; *** |CoTuple| REDEFINED ;;; *** |CoTuple| REDEFINED Time: 0.10 SEC. Cumulative Statistics for Constructor CoTuple Time: 0.23 seconds finalizing NRLIB COT Processing CoTuple for Browser database: -- 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" -- constructor --->-->CoTuple(constructor): Unexpected HT command: \indented "\\indented{1}{This domain is intended to be the categorical dual of a} Tuple (comma-delimited homogeneous sequence of values). As such it implements an \\spad{n}-ary disjoint union." ------------------------------------------------------------------------ CoTuple is now explicitly exposed in frame initial CoTuple will be automatically loaded when needed from /var/zope2/var/LatexWiki/COT.NRLIB/code.o axiom inj(1,10)  (6) Type: CoTuple? PositiveInteger? axiom inj(1,10) < inj(2,10)  (7) Type: Boolean axiom sup(inj(1,99), inj(2,10))$CoTuple(NNI)
 (8)
Type: CoTuple? NonNegativeInteger?