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

SandBoxFreeSum
  
last edited 11 years ago by test1

Edit detail for SandBoxFreeSum revision 1 of 3
1 2 3
Editor: Bill Page
Time: 2009/09/23 01:00:24 GMT-7
Note: new 
changed:
-
\begin{spad}
)abbrev domain FSUM FreeSum
++ Description:
++ This domain implements the free "product" of abelian monoids (groups)
++ It is the coproduct in the category of abelian monoids (groups).
++ FreeSum(A,B) is the abelian monoid (group) whose elements are
++ the reduced words in A and B, under the operation of concatenation
++ followed by reduction:
++   * Remove identity elements (of either A or B)
++   * Replace a1a2 by its sum in A and b1b2 by its sum in B
++ Ref: http://en.wikipedia.org/wiki/Free_product
FreeSum(A:AbelianMonoid,B:AbelianMonoid):AbelianMonoid with
    if A has AbelianGroup and B has AbelianGroup then AbelianGroup
    in1: A -> %
    in2: B -> %
    RetractableTo(A)
    RetractableTo(B)
    is1: % -> Boolean
    is2: % -> Boolean
    if A has Comparable and B has Comparable then Comparable
    terms: % -> List %
  == add
    Rep == List Union(A,B)
    rep(x:%):Rep == x pretend Rep
    per(x:Rep):% == x pretend %

    Zero() == per []
    coerce(x:%):OutputForm ==
      r:=rep(x)
      if empty?(r) then
        return coerce(0$InputForm)
      else if #r=1 then
        s:=first r
        if s case A then
          return coerce(s::A)
        else if s case B then
          return overbar(coerce(s::B))
      return infix(_+,[coerce(per [s]) for s in r])

    if A has Comparable and B has Comparable then
      smaller?(x:%,y:%):Boolean ==
        r1:=rep(x); r2:=rep(y)
        for s1 in r1 for s2 in r2 repeat
          if s1 case A then
            if s2 case A then
              if smaller?(s1::A, s2::A) then return true
            if s2 case B then return true
          else if s1 case B then
            if s2 case B then
              if smaller?(s1::B, s2::B) then return true
            if s2 case A then return false
        if #r1 < #r2 then return true
        return false

    (x:% = y:%):Boolean ==
      r1:=rep(x); r2:=rep(y)
      if #r1 ~= #r2 then return false
      for s1 in r1 for s2 in r2 repeat
        if s1 case A then
          if s2 case A then
            if (s1::A) ~= (s2::A) then return false
          if s2 case B then return false
        else if s1 case B then
          if s2 case B then
            if (s1::B) ~= (s2::B) then return false
          if s2 case A then return false
      return true

    in1(x:A):% == if x=0 then 0 else per [[x]]
    in2(y:B):% == if y=0 then 0 else per [[y]]
    coerce(x:A):% == in1(x)
    coerce(x:B):% == in2(x)
    is1(x:%):Boolean == first(rep x) case A
    is2(x:%):Boolean == first(rep x) case B
    retract(x:%):A == if x=0 or not is1(x) then 0 else coerce(first rep x)@A
    retract(x:%):B == if x=0 or not is2(x) then 0 else coerce(first rep x)@B
    terms(x:%):List % == [ per [s] for s in rep(x) ]

    if A has AbelianGroup and B has AbelianGroup then
      _-(x:%):% ==
        if x=0 then return 0
        return per [( _
          s case A => -(s::A); _
          s case B => -(s::B)) _
        for s in reverse rep(x)]
      (x:% - y:%):% == x + (-y)
      (n:Integer * x:%):% ==
        if x=0 then return 0
        if n>0 then return (n-1) * x + x
        if n<0 then return (n+1) * x - x
        return 0      

    (x:% + y:%):% ==
      if x=0 then return y
      if y=0 then return x
      r1:=rep(x); r2:=rep(y)
      f1:=first(r1,(#r1-1)::NonNegativeInteger); l1:=last r1
      f2:=first r2; l2:=last(r2,(#r2-1)::NonNegativeInteger)
      -- reduction
      if l1 case A and f2 case A then
        return per(f1)+in1((l1::A)+(f2::A))+per(l2)
      if l1 case B and f2 case B then
        return per(f1)+in2((l1::B)+(f2::B))+per(l2)
      return per concat(r1,r2)

    (n:NonNegativeInteger * x:%):% ==
      if x=0 then return 0
      if n>0 then return (n-1)::NonNegativeInteger * x + x
      return 0      
    (n:PositiveInteger * x:%):% ==
      if x=0 then return 0
      if n>1 then return (n-1)::PositiveInteger * x + x
      return x      
\end{spad}

\begin{axiom}
II:=FSUM(INT,INT)
i1:=in1(2)$II
i2:=in2(3)$II
i1
i2
i1=i2
test(i1=i2)
test(i2=i2)
i1+i1
i2+i2
i1+i2
i2+i1
\end{axiom}

\begin{axiom}
fs:=FreeSum(FreeAbelianMonoid Symbol,FreeAbelianMonoid Symbol)
p:=in1('p)$fs
q:=in2('q)$fs
r:=in1('r)$fs
2*(p+q+r)
(p+q)+(r+p)+(q+r)
a:FreeAbelianMonoid Symbol:='a
b:FreeAbelianMonoid Symbol:='b
a+b
p+q                                          
p+2*q                              
\end{axiom}

\begin{axiom}
gs:=FreeSum(FreeAbelianGroup Symbol,FreeAbelianGroup Symbol)
g1:=(in1('g1)$gs)
g2:=(in2('g2)$gs)
g1+g2+ -1*g1
\end{axiom}

spad
)abbrev domain FSUM FreeSum
++ Description:
++ This domain implements the free "product" of abelian monoids (groups)
++ It is the coproduct in the category of abelian monoids (groups).
++ FreeSum(A,B) is the abelian monoid (group) whose elements are
++ the reduced words in A and B, under the operation of concatenation
++ followed by reduction:
++   * Remove identity elements (of either A or B)
++   * Replace a1a2 by its sum in A and b1b2 by its sum in B
++ Ref: http://en.wikipedia.org/wiki/Free_product
FreeSum(A:AbelianMonoid,B:AbelianMonoid):AbelianMonoid with
    if A has AbelianGroup and B has AbelianGroup then AbelianGroup
    in1: A -> %
    in2: B -> %
    RetractableTo(A)
    RetractableTo(B)
    is1: % -> Boolean
    is2: % -> Boolean
    if A has Comparable and B has Comparable then Comparable
    terms: % -> List %
  == add
    Rep == List Union(A,B)
    rep(x:%):Rep == x pretend Rep
    per(x:Rep):% == x pretend %

    Zero() == per []
    coerce(x:%):OutputForm ==
      r:=rep(x)
      if empty?(r) then
        return coerce(0$InputForm)
      else if #r=1 then
        s:=first r
        if s case A then
          return coerce(s::A)
        else if s case B then
          return overbar(coerce(s::B))
      return infix(_+,[coerce(per [s]) for s in r])

    if A has Comparable and B has Comparable then
      smaller?(x:%,y:%):Boolean ==
        r1:=rep(x); r2:=rep(y)
        for s1 in r1 for s2 in r2 repeat
          if s1 case A then
            if s2 case A then
              if smaller?(s1::A, s2::A) then return true
            if s2 case B then return true
          else if s1 case B then
            if s2 case B then
              if smaller?(s1::B, s2::B) then return true
            if s2 case A then return false
        if #r1 < #r2 then return true
        return false

    (x:% = y:%):Boolean ==
      r1:=rep(x); r2:=rep(y)
      if #r1 ~= #r2 then return false
      for s1 in r1 for s2 in r2 repeat
        if s1 case A then
          if s2 case A then
            if (s1::A) ~= (s2::A) then return false
          if s2 case B then return false
        else if s1 case B then
          if s2 case B then
            if (s1::B) ~= (s2::B) then return false
          if s2 case A then return false
      return true

    in1(x:A):% == if x=0 then 0 else per [[x]]
    in2(y:B):% == if y=0 then 0 else per [[y]]
    coerce(x:A):% == in1(x)
    coerce(x:B):% == in2(x)
    is1(x:%):Boolean == first(rep x) case A
    is2(x:%):Boolean == first(rep x) case B
    retract(x:%):A == if x=0 or not is1(x) then 0 else coerce(first rep x)@A
    retract(x:%):B == if x=0 or not is2(x) then 0 else coerce(first rep x)@B
    terms(x:%):List % == [ per [s] for s in rep(x) ]

    if A has AbelianGroup and B has AbelianGroup then
      _-(x:%):% ==
        if x=0 then return 0
        return per [( _
          s case A => -(s::A); _
          s case B => -(s::B)) _
        for s in reverse rep(x)]
      (x:% - y:%):% == x + (-y)
      (n:Integer * x:%):% ==
        if x=0 then return 0
        if n>0 then return (n-1) * x + x
        if n<0 then return (n+1) * x - x
        return 0      

    (x:% + y:%):% ==
      if x=0 then return y
      if y=0 then return x
      r1:=rep(x); r2:=rep(y)
      f1:=first(r1,(#r1-1)::NonNegativeInteger); l1:=last r1
      f2:=first r2; l2:=last(r2,(#r2-1)::NonNegativeInteger)
      -- reduction
      if l1 case A and f2 case A then
        return per(f1)+in1((l1::A)+(f2::A))+per(l2)
      if l1 case B and f2 case B then
        return per(f1)+in2((l1::B)+(f2::B))+per(l2)
      return per concat(r1,r2)

    (n:NonNegativeInteger * x:%):% ==
      if x=0 then return 0
      if n>0 then return (n-1)::NonNegativeInteger * x + x
      return 0      
    (n:PositiveInteger * x:%):% ==
      if x=0 then return 0
      if n>1 then return (n-1)::PositiveInteger * x + x
      return x
spad
   Compiling FriCAS source code from file 
      /var/zope2/var/LatexWiki/8696243271036350699-25px001.spad using 
      old system compiler.
   FSUM abbreviates domain FreeSum 
------------------------------------------------------------------------
   initializing NRLIB FSUM for FreeSum 
   compiling into NRLIB FSUM 
   compiling local rep : $ -> List Union(A,B)
      FSUM;rep is replaced by x 
Time: 0.04 SEC.

   compiling local per : List Union(A,B) -> $
      FSUM;per is replaced by x 
Time: 0.004 SEC.

   compiling exported Zero : () -> $
Time: 0 SEC.

   compiling exported coerce : $ -> OutputForm
Time: 0.13 SEC.

****** Domain: A already in scope
augmenting A: (Comparable)
****** Domain: B already in scope
augmenting B: (Comparable)
   compiling exported smaller? : ($,$) -> Boolean
Time: 0.01 SEC.

   compiling exported = : ($,$) -> Boolean
Time: 0.01 SEC.

   compiling exported in1 : A -> $
Time: 0 SEC.

   compiling exported in2 : B -> $
Time: 0 SEC.

   compiling exported coerce : A -> $
Time: 0 SEC.

   compiling exported coerce : B -> $
Time: 0 SEC.

   compiling exported is1 : $ -> Boolean
Time: 0.004 SEC.

   compiling exported is2 : $ -> Boolean
Time: 0 SEC.

   compiling exported retract : $ -> A
Time: 0 SEC.

   compiling exported retract : $ -> B
Time: 0.004 SEC.

   compiling exported terms : $ -> List $
Time: 0 SEC.

****** Domain: A already in scope
augmenting A: (AbelianGroup)
****** Domain: B already in scope
augmenting B: (AbelianGroup)
   compiling exported - : $ -> $
Time: 0.004 SEC.

   compiling exported - : ($,$) -> $
Time: 0 SEC.

   compiling exported * : (Integer,$) -> $
Time: 0.01 SEC.

   compiling exported + : ($,$) -> $
Time: 0.02 SEC.

   compiling exported * : (NonNegativeInteger,$) -> $
Time: 0.004 SEC.

   compiling exported * : (PositiveInteger,$) -> $
Time: 0.004 SEC.

****** Domain: A already in scope
augmenting A: (AbelianGroup)
****** Domain: B already in scope
augmenting B: (AbelianGroup)
****** Domain: A already in scope
augmenting A: (Comparable)
****** Domain: B already in scope
augmenting B: (Comparable)
(time taken in buildFunctor:  4)

;;;     ***       |FreeSum| REDEFINED

;;;     ***       |FreeSum| REDEFINED
Time: 0.01 SEC.

   Cumulative Statistics for Constructor FreeSum
      Time: 0.25 seconds

   finalizing NRLIB FSUM 
   Processing FreeSum for Browser database:
--->-->FreeSum((in1 (% A))): Not documented!!!!
--->-->FreeSum((in2 (% B))): Not documented!!!!
--->-->FreeSum((is1 ((Boolean) %))): Not documented!!!!
--->-->FreeSum((is2 ((Boolean) %))): Not documented!!!!
--->-->FreeSum((terms ((List %) %))): Not documented!!!!
--------constructor---------
; compiling file "/var/zope2/var/LatexWiki/FSUM.NRLIB/FSUM.lsp" (written 23 SEP 2009 01:00:26 AM):
; compiling (/VERSIONCHECK 2)
; compiling (PUT (QUOTE |FSUM;rep|) ...)
; compiling (DEFUN |FSUM;rep| ...)
; compiling (PUT (QUOTE |FSUM;per|) ...)
; compiling (DEFUN |FSUM;per| ...)
; compiling (DEFUN |FSUM;Zero;$;3| ...)
; compiling (DEFUN |FSUM;coerce;$Of;4| ...)
; compiling (DEFUN |FSUM;smaller?;2$B;5| ...)
; compiling (DEFUN |FSUM;=;2$B;6| ...)
; compiling (DEFUN |FSUM;in1;A$;7| ...)
; compiling (DEFUN |FSUM;in2;B$;8| ...)
; compiling (DEFUN |FSUM;coerce;A$;9| ...)
; compiling (DEFUN |FSUM;coerce;B$;10| ...)
; compiling (DEFUN |FSUM;is1;$B;11| ...)
; compiling (DEFUN |FSUM;is2;$B;12| ...)
; compiling (DEFUN |FSUM;retract;$A;13| ...)
; compiling (DEFUN |FSUM;retract;$B;14| ...)
; compiling (DEFUN |FSUM;terms;$L;15| ...)
; compiling (DEFUN |FSUM;-;2$;16| ...)
; compiling (DEFUN |FSUM;-;3$;17| ...)
; compiling (DEFUN |FSUM;*;I2$;18| ...)
; compiling (DEFUN |FSUM;+;3$;19| ...)
; compiling (DEFUN |FSUM;*;Nni2$;20| ...)
; compiling (DEFUN |FSUM;*;Pi2$;21| ...)
; compiling (DEFUN |FreeSum| ...)
; compiling (DEFUN |FreeSum;| ...)
; compiling (MAKEPROP (QUOTE |FreeSum|) ...)

; /var/zope2/var/LatexWiki/FSUM.NRLIB/FSUM.fasl written
; compilation finished in 0:00:00.240
------------------------------------------------------------------------
   FreeSum is now explicitly exposed in frame initial 
   FreeSum will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/FSUM.NRLIB/FSUM

axiom
II:=FSUM(INT,INT)
LatexWiki Image(1)
Type: Domain
axiom
i1:=in1(2)$II
LatexWiki Image(2)
Type: FreeSum?(Integer,Integer)
axiom
i2:=in2(3)$II
LatexWiki Image(3)
Type: FreeSum?(Integer,Integer)
axiom
i1
LatexWiki Image(4)
Type: FreeSum?(Integer,Integer)
axiom
i2
LatexWiki Image(5)
Type: FreeSum?(Integer,Integer)
axiom
i1=i2
LatexWiki Image(6)
Type: Equation(FreeSum?(Integer,Integer))
axiom
test(i1=i2)
LatexWiki Image(7)
Type: Boolean
axiom
test(i2=i2)
LatexWiki Image(8)
Type: Boolean
axiom
i1+i1
LatexWiki Image(9)
Type: FreeSum?(Integer,Integer)
axiom
i2+i2
LatexWiki Image(10)
Type: FreeSum?(Integer,Integer)
axiom
i1+i2
LatexWiki Image(11)
Type: FreeSum?(Integer,Integer)
axiom
i2+i1
LatexWiki Image(12)
Type: FreeSum?(Integer,Integer)

axiom
fs:=FreeSum(FreeAbelianMonoid Symbol,FreeAbelianMonoid Symbol)
LatexWiki Image(13)
Type: Domain
axiom
p:=in1('p)$fs
LatexWiki Image(14)
Type: FreeSum?(FreeAbelianMonoid?(Symbol),FreeAbelianMonoid?(Symbol))
axiom
q:=in2('q)$fs
LatexWiki Image(15)
Type: FreeSum?(FreeAbelianMonoid?(Symbol),FreeAbelianMonoid?(Symbol))
axiom
r:=in1('r)$fs
LatexWiki Image(16)
Type: FreeSum?(FreeAbelianMonoid?(Symbol),FreeAbelianMonoid?(Symbol))
axiom
2*(p+q+r)
LatexWiki Image(17)
Type: FreeSum?(FreeAbelianMonoid?(Symbol),FreeAbelianMonoid?(Symbol))
axiom
(p+q)+(r+p)+(q+r)
LatexWiki Image(18)
Type: FreeSum?(FreeAbelianMonoid?(Symbol),FreeAbelianMonoid?(Symbol))
axiom
a:FreeAbelianMonoid Symbol:='a
LatexWiki Image(19)
Type: FreeAbelianMonoid?(Symbol)
axiom
b:FreeAbelianMonoid Symbol:='b
LatexWiki Image(20)
Type: FreeAbelianMonoid?(Symbol)
axiom
a+b
LatexWiki Image(21)
Type: FreeAbelianMonoid?(Symbol)
axiom
p+q
LatexWiki Image(22)
Type: FreeSum?(FreeAbelianMonoid?(Symbol),FreeAbelianMonoid?(Symbol))
axiom
p+2*q
LatexWiki Image(23)
Type: FreeSum?(FreeAbelianMonoid?(Symbol),FreeAbelianMonoid?(Symbol))

axiom
gs:=FreeSum(FreeAbelianGroup Symbol,FreeAbelianGroup Symbol)
LatexWiki Image(24)
Type: Domain
axiom
g1:=(in1('g1)$gs)
LatexWiki Image(25)
Type: FreeSum?(FreeAbelianGroup?(Symbol),FreeAbelianGroup?(Symbol))
axiom
g2:=(in2('g2)$gs)
LatexWiki Image(26)
Type: FreeSum?(FreeAbelianGroup?(Symbol),FreeAbelianGroup?(Symbol))
axiom
g1+g2+ -1*g1
LatexWiki Image(27)
Type: FreeSum?(FreeAbelianGroup?(Symbol),FreeAbelianGroup?(Symbol))