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

# Edit detail for Cartesian Product revision 1 of 4

 1 2 3 4 Editor: Time: 2008/05/18 20:25:01 GMT-7 Note: missing operations from Finite

changed:
-
++ This domain implements cartesian product

\begin{axiom}
)show Product
\end{axiom}

)abbrev domain PRODUCT Product
Product (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

makeprod     : (A,B) -> %
++ makeprod(a,b) \undocumented
selectfirst  :   %   -> A
++ selectfirst(x) \undocumented
selectsecond :   %   -> B
++ selectsecond(x) \undocumented

--representations
Rep := Record(acomp:A,bcomp:B)

--declarations
x,y: %
i: NonNegativeInteger
p: NonNegativeInteger
a: A
b: B
d: Integer

--define
coerce(x):OutputForm == paren [(x.acomp)::OutputForm,
(x.bcomp)::OutputForm]
x=y ==
x.acomp = y.acomp => x.bcomp = y.bcomp
false
makeprod(a:A,b:B) :%   == [a,b]

selectfirst(x:%) : A   == x.acomp

selectsecond (x:%) : B == x.bcomp

if A has Monoid and B has Monoid then
1 == [1$A,1$B]
x * y == [x.acomp * y.acomp,x.bcomp * y.bcomp]
x ** p == [x.acomp ** p ,x.bcomp ** p]

if A has Finite and B has Finite then
size == size$A * size$B
index(n) == [index((((n::Integer-1) quo size$B )+1)::PositiveInteger)$A,
index((((n::Integer-1) rem size$B )+1)::PositiveInteger)$B]
random() == [random()$A,random()$B]
lookup(x) == ((lookup(x.acomp)$A::Integer-1) * size$B::Integer +
lookup(x.bcomp)$B::Integer)::PositiveInteger hash(x) == hash(x.acomp)$A * size$B::SingleInteger + hash(x.bcomp)$B

if A has Group and B has Group then
inv(x) == [inv(x.acomp),inv(x.bcomp)]

if A has AbelianMonoid and B has AbelianMonoid then
0 == [0$A,0$B]

x + y == [x.acomp + y.acomp,x.bcomp + y.bcomp]

c:NonNegativeInteger * x == [c * x.acomp,c*x.bcomp]

if A has CancellationAbelianMonoid and
B has CancellationAbelianMonoid then
subtractIfCan(x, y) : Union(%,"failed") ==
(na:= subtractIfCan(x.acomp, y.acomp)) case "failed" => "failed"
(nb:= subtractIfCan(x.bcomp, y.bcomp)) case "failed" => "failed"
[na::A,nb::B]

if A has AbelianGroup and B has AbelianGroup then
- x == [- x.acomp,-x.bcomp]
(x - y):% == [x.acomp - y.acomp,x.bcomp - y.bcomp]
d * x == [d * x.acomp,d * x.bcomp]

if A has OrderedAbelianMonoidSup and B has OrderedAbelianMonoidSup then
sup(x,y) == [sup(x.acomp,y.acomp),sup(x.bcomp,y.bcomp)]

if A has OrderedSet and B has OrderedSet then
x < y ==
xa:= x.acomp ; ya:= y.acomp
xa < ya => true
xb:= x.bcomp ; yb:= y.bcomp
xa = ya => (xb < yb)
false

--     coerce(x:%):Symbol ==
--      PrintableForm()
--      formList([x.acomp::Expression,x.bcomp::Expression])$PrintableForm \end{spad} \begin{axiom} X:=Product(IntegerMod 3,Set PF 3) size()$X
[index(i)$X for i in 1..size()$X::PositiveInteger]
reduce(_and,[(lookup(index(i)$X)=i)::Boolean for i in 1..size()$X::PositiveInteger])
lookup(makeprod(2,)$X) [random()$X for i in 1..5]
\end{axiom}


++ This domain implements cartesian product

axiom)show Product
Product(A: SetCategory,B: SetCategory)  is a domain constructor
Abbreviation for Product is PRODUCT
This constructor is not exposed in this frame.
Issue )edit /usr/local/lib/axiom/target/x86_64-unknown-linux/../../src/algebra/PRODUCT.spad to see algebra source code for PRODUCT
------------------------------- Operations --------------------------------
?=? : (%,%) -> Boolean                coerce : % -> OutputForm
hash : % -> SingleInteger             latex : % -> String
makeprod : (A,B) -> %                 selectfirst : % -> A
selectsecond : % -> B                 ?~=? : (%,%) -> Boolean
?*? : (%,%) -> % if A has GROUP and B has GROUP or A has MONOID and B has MONOID
?*? : (PositiveInteger,%) -> % if A has ABELGRP and B has ABELGRP or A has ABELMON and B has ABELMON or A has CABMON and B has CABMON or A has OAMONS and B has OAMONS
?*? : (NonNegativeInteger,%) -> % if A has ABELGRP and B has ABELGRP or A has ABELMON and B has ABELMON or A has CABMON and B has CABMON or A has OAMONS and B has OAMONS
?*? : (Integer,%) -> % if A has ABELGRP and B has ABELGRP
?**? : (%,PositiveInteger) -> % if A has GROUP and B has GROUP or A has MONOID and B has MONOID
?**? : (%,NonNegativeInteger) -> % if A has GROUP and B has GROUP or A has MONOID and B has MONOID
?**? : (%,Integer) -> % if A has GROUP and B has GROUP
?+? : (%,%) -> % if A has ABELGRP and B has ABELGRP or A has ABELMON and B has ABELMON or A has CABMON and B has CABMON or A has OAMONS and B has OAMONS
-? : % -> % if A has ABELGRP and B has ABELGRP
?-? : (%,%) -> % if A has ABELGRP and B has ABELGRP
?/? : (%,%) -> % if A has GROUP and B has GROUP
?<? : (%,%) -> Boolean if A has OAMONS and B has OAMONS or A has ORDSET and B has ORDSET
?<=? : (%,%) -> Boolean if A has OAMONS and B has OAMONS or A has ORDSET and B has ORDSET
?>? : (%,%) -> Boolean if A has OAMONS and B has OAMONS or A has ORDSET and B has ORDSET
?>=? : (%,%) -> Boolean if A has OAMONS and B has OAMONS or A has ORDSET and B has ORDSET
1 : () -> % if A has GROUP and B has GROUP or A has MONOID and B has MONOID
0 : () -> % if A has ABELGRP and B has ABELGRP or A has ABELMON and B has ABELMON or A has CABMON and B has CABMON or A has OAMONS and B has OAMONS
?^? : (%,PositiveInteger) -> % if A has GROUP and B has GROUP or A has MONOID and B has MONOID
?^? : (%,NonNegativeInteger) -> % if A has GROUP and B has GROUP or A has MONOID and B has MONOID
?^? : (%,Integer) -> % if A has GROUP and B has GROUP
commutator : (%,%) -> % if A has GROUP and B has GROUP
conjugate : (%,%) -> % if A has GROUP and B has GROUP
enumerate : () -> List % if A has FINITE and B has FINITE
index : PositiveInteger -> % if A has FINITE and B has FINITE
inv : % -> % if A has GROUP and B has GROUP
lookup : % -> PositiveInteger if A has FINITE and B has FINITE
max : (%,%) -> % if A has OAMONS and B has OAMONS or A has ORDSET and B has ORDSET
min : (%,%) -> % if A has OAMONS and B has OAMONS or A has ORDSET and B has ORDSET
one? : % -> Boolean if A has GROUP and B has GROUP or A has MONOID and B has MONOID
random : () -> % if A has FINITE and B has FINITE
recip : % -> Union(%,"failed") if A has GROUP and B has GROUP or A has MONOID and B has MONOID
sample : () -> % if A has ABELGRP and B has ABELGRP or A has ABELMON and B has ABELMON or A has CABMON and B has CABMON or A has GROUP and B has GROUP or A has MONOID and B has MONOID or A has OAMONS and B has OAMONS
size : () -> NonNegativeInteger if A has FINITE and B has FINITE
subtractIfCan : (%,%) -> Union(%,"failed") if A has ABELGRP and B has ABELGRP or A has CABMON and B has CABMON or A has OAMONS and B has OAMONS
sup : (%,%) -> % if A has OAMONS and B has OAMONS
zero? : % -> Boolean if A has ABELGRP and B has ABELGRP or A has ABELMON and B has ABELMON or A has CABMON and B has CABMON or A has OAMONS and B has OAMONS

spad)abbrev domain PRODUCT Product
Product (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
makeprod     : (A,B) -> %
++ makeprod(a,b) \undocumented
selectfirst  :   %   -> A
++ selectfirst(x) \undocumented
selectsecond :   %   -> B
++ selectsecond(x) \undocumented
--representations
Rep := Record(acomp:A,bcomp:B)
--declarations
x,y: %
i: NonNegativeInteger
p: NonNegativeInteger
a: A
b: B
d: Integer
--define
coerce(x):OutputForm == paren [(x.acomp)::OutputForm,
(x.bcomp)::OutputForm]
x=y ==
x.acomp = y.acomp => x.bcomp = y.bcomp
false
makeprod(a:A,b:B) :%   == [a,b]
selectfirst(x:%) : A   == x.acomp
selectsecond (x:%) : B == x.bcomp
if A has Monoid and B has Monoid then
1 == [1$A,1$B]
x * y == [x.acomp * y.acomp,x.bcomp * y.bcomp]
x ** p == [x.acomp ** p ,x.bcomp ** p]
if A has Finite and B has Finite then
size == size$A * size$B
index(n) == [index((((n::Integer-1) quo size$B )+1)::PositiveInteger)$A,
index((((n::Integer-1) rem size$B )+1)::PositiveInteger)$B]
random() == [random()$A,random()$B]
lookup(x) == ((lookup(x.acomp)$A::Integer-1) * size$B::Integer +
lookup(x.bcomp)$B::Integer)::PositiveInteger hash(x) == hash(x.acomp)$A * size$B::SingleInteger + hash(x.bcomp)$B
if A has Group and B has Group then
inv(x) == [inv(x.acomp),inv(x.bcomp)]
if A has AbelianMonoid and B has AbelianMonoid then
0 == [0$A,0$B]
x + y == [x.acomp + y.acomp,x.bcomp + y.bcomp]
c:NonNegativeInteger * x == [c * x.acomp,c*x.bcomp]
if A has CancellationAbelianMonoid and
B has CancellationAbelianMonoid then
subtractIfCan(x, y) : Union(%,"failed") ==
(na:= subtractIfCan(x.acomp, y.acomp)) case "failed" => "failed"
(nb:= subtractIfCan(x.bcomp, y.bcomp)) case "failed" => "failed"
[na::A,nb::B]
if A has AbelianGroup and B has AbelianGroup then
- x == [- x.acomp,-x.bcomp]
(x - y):% == [x.acomp - y.acomp,x.bcomp - y.bcomp]
d * x == [d * x.acomp,d * x.bcomp]
if A has OrderedAbelianMonoidSup and B has OrderedAbelianMonoidSup then
sup(x,y) == [sup(x.acomp,y.acomp),sup(x.bcomp,y.bcomp)]
if A has OrderedSet and B has OrderedSet then
x < y ==
xa:= x.acomp ; ya:= y.acomp
xa < ya => true
xb:= x.bcomp ; yb:= y.bcomp
xa = ya => (xb < yb)
false
--     coerce(x:%):Symbol ==
--      PrintableForm()
--      formList([x.acomp::Expression,x.bcomp::Expression])$PrintableForm spad  Compiling FriCAS source code from file /var/zope2/var/LatexWiki/8594176356433254296-25px002.spad using old system compiler. PRODUCT abbreviates domain Product ------------------------------------------------------------------------ initializing NRLIB PRODUCT for Product compiling into NRLIB PRODUCT compiling exported coerce :$ -> OutputForm
Time: 0.03 SEC.
compiling exported = : ($,$) -> Boolean
Time: 0 SEC.
compiling exported makeprod : (A,B) -> $PRODUCT;makeprod;AB$;3 is replaced by CONS
Time: 0 SEC.
compiling exported selectfirst : $-> A PRODUCT;selectfirst;$A;4 is replaced by QCAR
Time: 0 SEC.
compiling exported selectsecond : $-> B PRODUCT;selectsecond;$B;5 is replaced by QCDR
Time: 0.01 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 SEC.
compiling exported ** : ($,NonNegativeInteger) ->$
Time: 0 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.07 SEC. compiling exported random : () ->$
Time: 0 SEC.
compiling exported lookup : $-> PositiveInteger Time: 0.03 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.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.01 SEC.
compiling exported * : (NonNegativeInteger,$) ->$
Time: 0 SEC.
****** Domain: A already in scope
augmenting A: (CancellationAbelianMonoid)
****** Domain: B already in scope
augmenting B: (CancellationAbelianMonoid)
compiling exported subtractIfCan : ($,$) -> Union($,failed) Time: 0.01 SEC. ****** Domain: A already in scope augmenting A: (AbelianGroup) ****** Domain: B already in scope augmenting B: (AbelianGroup) compiling exported - :$ -> $Time: 0 SEC. compiling exported - : ($,$) ->$
Time: 0.01 SEC.
compiling exported * : (Integer,$) ->$
Time: 0 SEC.
****** Domain: A already in scope
augmenting A: (OrderedAbelianMonoidSup)
****** Domain: B already in scope
augmenting B: (OrderedAbelianMonoidSup)
compiling exported sup : ($,$) -> $Time: 0 SEC. ****** Domain: A already in scope augmenting A: (OrderedSet) ****** Domain: B already in scope augmenting B: (OrderedSet) compiling exported < : ($,$) -> Boolean Time: 0.06 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) ;;; *** |Product| REDEFINED ;;; *** |Product| REDEFINED Time: 0.05 SEC. Cumulative Statistics for Constructor Product Time: 0.29 seconds finalizing NRLIB PRODUCT Processing Product for Browser database: --------(makeprod (% A B))--------- --------(selectfirst (A %))--------- --------(selectsecond (B %))--------- --->/usr/local/lib/axiom/target/x86_64-unknown-linux/../../src/algebra/PRODUCT.spad-->Product(constructor): Not documented!!!! --->/usr/local/lib/axiom/target/x86_64-unknown-linux/../../src/algebra/PRODUCT.spad-->Product(): Missing Description ; (DEFUN |Product;| ...) is being compiled. ;; The variable IDENTITY is undefined. ;; The compiler will assume this variable is a global. ------------------------------------------------------------------------ Product is now explicitly exposed in frame initial Product will be automatically loaded when needed from /var/zope2/var/LatexWiki/PRODUCT.NRLIB/code axiomX:=Product(IntegerMod 3,Set PF 3) (1) Type: Domain axiomsize()$X (2)
Type: NonNegativeInteger?
axiom[index(i)$X for i in 1..size()$X::PositiveInteger]
axiom
Compiling function G1544 with type NonNegativeInteger -> Boolean (3)
Type: List Product(IntegerMod? 3,Set PrimeField? 3)
axiomreduce(_and,[(lookup(index(i)$X)=i)::Boolean for i in 1..size()$X::PositiveInteger]) (4)
Type: Boolean
axiomlookup(makeprod(2,)$X) (5) Type: PositiveInteger? axiom[random()$X for i in 1..5] (6)
Type: List Product(IntegerMod? 3,Set PrimeField? 3)