open-axiom-source 1.4.1+svn~2626-2ubuntu2 / usr / lib / open-axiom / src / algebra / wtpol.spad

--Copyright (c) 1991-2002, The Numerical ALgorithms Group Ltd.
--All rights reserved.
--
--Redistribution and use in source and binary forms, with or without
--modification, are permitted provided that the following conditions are
--met:
--
--    - Redistributions of source code must retain the above copyright
--      notice, this list of conditions and the following disclaimer.
--
--    - Redistributions in binary form must reproduce the above copyright
--      notice, this list of conditions and the following disclaimer in
--      the documentation and/or other materials provided with the
--      distribution.
--
--    - Neither the name of The Numerical ALgorithms Group Ltd. nor the
--      names of its contributors may be used to endorse or promote products
--      derived from this software without specific prior written permission.
--
--THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
--IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
--TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
--PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
--OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
--EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
--PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
--PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
--LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
--NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
--SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

import Ring
import OrderedSet
import OrderedAbelianMonoidSup
import PolynomialCategory
import List
import NonNegativeInteger
)abbrev domain WP WeightedPolynomials
++ Author: James Davenport
++ Date Created:  17 April 1992
++ Date Last Updated: 12 July 1992
++ Basic Functions: Ring, changeWeightLevel
++ Related Constructors: PolynomialRing
++ Also See: OrdinaryWeightedPolynomials
++ AMS Classifications:
++ Keywords:
++ References:
++ Description:
++ This domain represents truncated weighted polynomials over a general
++ (not necessarily commutative) polynomial type. The variables must be
++ specified, as must the weights.
++ The representation is sparse
++ in the sense that only non-zero terms are represented.

WeightedPolynomials(R:Ring,VarSet: OrderedSet, E:OrderedAbelianMonoidSup,
                           P:PolynomialCategory(R,E,VarSet),
                             vl:List VarSet, wl:List NonNegativeInteger,
                              wtlevel:NonNegativeInteger):
       Join(Ring, HomotopicTo P) with
         if R has CommutativeRing then Algebra(R)
         if R has Field then "/": ($,$) -> Union($,"failed")
	         ++ x/y division (only works if minimum weight
	         ++ of divisor is zero, and if R is a Field)
         changeWeightLevel: NonNegativeInteger -> Void
        	 ++ changeWeightLevel(n) changes the weight level to the new value given:
	         ++ NB: previously calculated terms are not affected
    ==
  add
   --representations
   Rep  := PolynomialRing(P,NonNegativeInteger)
   p:P
   w,x1,x2:$
   n:NonNegativeInteger
   z:Integer
   changeWeightLevel(n) ==
        wtlevel:=n
   lookupList:List Record(var:VarSet, weight:NonNegativeInteger)
   if #vl ~= #wl then error "incompatible length lists in WeightedPolynomial"
   lookupList:=[[v,n] for v in vl for n in wl]
   -- local operation
   innercoerce: (P,Integer) -> $
   lookup:VarSet -> NonNegativeInteger
   lookup v ==
      l:=lookupList
      while l ~= [] repeat
        v = l.first.var => return l.first.weight
        l:=l.rest
      0
   innercoerce(p,z) ==
      negative? z => 0
      zero? p => 0
      mv:= mainVariable p
      mv case "failed" => monomial(p,0)
      n:=lookup(mv)
      up:=univariate(p,mv)
      ans:$
      ans:=0
      while not zero? up  repeat
        d:=degree up
        f:=n*d
        lcup:=leadingCoefficient up
        up:=up-leadingMonomial up
        mon:=monomial(1,mv,d)
        f<=z =>
            tmp:= innercoerce(lcup,z-f)
            while not zero? tmp repeat
              ans:=ans+ monomial(mon*leadingCoefficient(tmp),degree(tmp)+f)
              tmp:=reductum tmp
      ans
   coerce(p):$ == innercoerce(p,wtlevel)
   coerce(w):P ==  "+"/[c for c in coefficients w]
   coerce(p:$):OutputForm ==
     zero? p => (0$Integer)::OutputForm
     degree p = 0 => leadingCoefficient(p):: OutputForm
     reduce("+",(reverse [paren(c::OutputForm) for c in coefficients p])
                 ::List OutputForm)
   0 == 0$Rep
   1 == 1$Rep
   x1 = x2 ==
      -- Note that we must strip out any terms greater than wtlevel
      while degree x1 > wtlevel repeat
            x1 := reductum x1
      while degree x2 > wtlevel repeat
            x2 := reductum x2
      x1 =$Rep x2
   x1 + x2 == x1 +$Rep x2
   -x1 == -(x1::Rep)
   x1 * x2 ==
     -- Note that this is probably an extremely inefficient definition
     w:=x1 *$Rep x2
     while degree(w) > wtlevel repeat
           w:=reductum w
     w

import Ring
import Field
import CommutativeRing
import Algebra
import Polynomial
import Void
import List
import NonNegativeInteger
)abbrev domain OWP OrdinaryWeightedPolynomials
++ Author: James Davenport
++ Date Created:  17 April 1992
++ Date Last Updated: 12 July 1992
++ Basic Functions: Ring, changeWeightLevel
++ Related Constructors: WeightedPolynomials
++ Also See: PolynomialRing
++ AMS classifications:
++ Keywords:
++ References:
++ Description:
++ This domain represents truncated weighted polynomials over the
++ "Polynomial" type. The variables must be
++ specified, as must the weights.
++ The representation is sparse
++ in the sense that only non-zero terms are represented.

OrdinaryWeightedPolynomials(R:Ring,
                             vl:List Symbol, wl:List NonNegativeInteger,
                              wtlevel:NonNegativeInteger):
       Join(Ring, HomotopicTo Polynomial R) with
         if R has CommutativeRing then Algebra(R)
         if R has Field then /: ($,$) -> Union($,"failed")
	         ++ x/y division (only works if minimum weight
       		 ++ of divisor is zero, and if R is a Field)
         changeWeightLevel: NonNegativeInteger -> Void
	         ++ changeWeightLevel(n) This changes the weight level to the new value given:
         	 ++ NB: previously calculated terms are not affected
    == WeightedPolynomials(R,Symbol,IndexedExponents(Symbol),
                           Polynomial(R),
                            vl,wl,wtlevel)