axiom-source 20170501-3 / usr / share / axiom-20170501 / src / algebra / TSETCAT.spad

)abbrev category TSETCAT TriangularSetCategory
++ Author: Marc Moreno Maza (marc@nag.co.uk)
++ Date Created: 04/26/1994
++ Date Last Updated: 12/15/1998
++ References :
++ SALSA Solvers for Algebraic Systems and Applications
++ Kalk91 Three contributions to elimination theory
++ Kalk98 Algorithmic properties of polynomial rings
++ Aubr96 Triangular Sets for Solving Polynomial Systems: 
++ Aubr99 On the Theories of Triangular Sets
++ Aubr99a Triangular Sets for Solving Polynomial Systems: 
++ Laza91 A new method for solving algebraic systems of positive dimension
++ Maza95 Polynomial Gcd Computations over Towers of Algebraic Extensions
++ Maza97 Calculs de pgcd au-dessus des tours d'extensions simples et 
++        resolution des systemes d'equations algebriques
++ Maza98 A new algorithm for computing triangular decomposition of 
++        algebraic varieties
++ Maza00 On Triangular Decompositions of Algebraic Varieties
++ Description:
++ The category of triangular sets of multivariate polynomials
++ with coefficients in an integral domain.
++ Let \axiom{R} be an integral domain and \axiom{V} a finite ordered set of 
++ variables, say \axiom{X1 < X2 < ... < Xn}.  
++ A set \axiom{S} of polynomials in \axiom{R[X1,X2,...,Xn]} is triangular
++ if no elements of \axiom{S} lies in \axiom{R}, and if two distinct 
++ elements of \axiom{S} have distinct main variables. 
++ Note that the empty set is a triangular set. A triangular set is not
++ necessarily a (lexicographical) Groebner basis and the notion of 
++ reduction related to triangular sets is based on the recursive view
++ of polynomials. We recall this notion here and refer to [1] for more 
++ details.
++ A polynomial \axiom{P} is reduced w.r.t a non-constant polynomial 
++ \axiom{Q} if the degree of \axiom{P} in the main variable of \axiom{Q} 
++ is less than the main degree of \axiom{Q}.
++ A polynomial \axiom{P} is reduced w.r.t a triangular set \axiom{T}
++ if it is reduced w.r.t. every polynomial of \axiom{T}. 

TriangularSetCategory(R,E,V,P) : Category == SIG where
  R : IntegralDomain
  E : OrderedAbelianMonoidSup
  V : OrderedSet
  P : RecursivePolynomialCategory(R,E,V)

  SIG ==> PolynomialSetCategory(R,E,V,P) with 

    finiteAggregate

    shallowlyMutable

    infRittWu? : ($,$) -> Boolean
      ++ \axiom{infRittWu?(ts1,ts2)} returns true iff \axiom{ts2} has 
      ++ higher rank than \axiom{ts1} in Wu Wen Tsun sense.

    basicSet : (List P,((P,P)->Boolean)) -> _
     Union(Record(bas:$,top:List P),"failed")
      ++ \axiom{basicSet(ps,redOp?)} returns \axiom{[bs,ts]} where
      ++ \axiom{concat(bs,ts)} is \axiom{ps} and \axiom{bs}
      ++ is a basic set in Wu Wen Tsun sense of \axiom{ps} w.r.t 
      ++ the reduction-test \axiom{redOp?}, if no non-zero constant 
      ++ polynomial lie in \axiom{ps}, otherwise \axiom{"failed"} is returned.

    basicSet : (List P,(P->Boolean),((P,P)->Boolean)) -> _
     Union(Record(bas:$,top:List P),"failed")
      ++ \axiom{basicSet(ps,pred?,redOp?)} returns the same as 
      ++ \axiom{basicSet(qs,redOp?)}
      ++ where \axiom{qs} consists of the polynomials of \axiom{ps}
      ++ satisfying property \axiom{pred?}.

    initials : $ -> List P
      ++ \axiom{initials(ts)} returns the list of the non-constant initials
      ++ of the members of \axiom{ts}.

    degree : $ -> NonNegativeInteger
      ++ \axiom{degree(ts)} returns the product of main degrees of the 
      ++ members of \axiom{ts}.

    quasiComponent : $ -> Record(close:List P,open:List P)
      ++ \axiom{quasiComponent(ts)} returns \axiom{[lp,lq]} where \axiom{lp} 
      ++ is the list of the members of \axiom{ts} and \axiom{lq}is 
      ++ \axiom{initials(ts)}.

    normalized? : (P,$) -> Boolean
      ++ \axiom{normalized?(p,ts)} returns true iff \axiom{p} and all 
      ++ its iterated initials have degree zero w.r.t. the main variables 
      ++ of the polynomials of \axiom{ts}

    normalized? : $  -> Boolean
      ++ \axiom{normalized?(ts)} returns true iff for every axiom{p} in 
      ++ \axiom{ts} we have \axiom{normalized?(p,us)} where \axiom{us} 
      ++ is \axiom{collectUnder(ts,mvar(p))}.

    reduced? : (P,$,((P,P) -> Boolean)) -> Boolean
      ++ \axiom{reduced?(p,ts,redOp?)} returns true iff \axiom{p} is reduced 
      ++ w.r.t.in the sense of the operation \axiom{redOp?}, that is if for 
      ++ every \axiom{t} in \axiom{ts} \axiom{redOp?(p,t)} holds.

    stronglyReduced? : (P,$) -> Boolean
      ++ \axiom{stronglyReduced?(p,ts)} returns true iff \axiom{p} 
      ++ is reduced w.r.t. \axiom{ts}.

    headReduced? : (P,$) -> Boolean
      ++ \axiom{headReduced?(p,ts)} returns true iff the head of \axiom{p} is 
      ++ reduced w.r.t. \axiom{ts}.

    initiallyReduced? : (P,$) -> Boolean
      ++ \axiom{initiallyReduced?(p,ts)} returns true iff \axiom{p} and all 
      ++ its iterated initials are reduced w.r.t. to the elements of 
      ++ \axiom{ts} with the same main variable.

    autoReduced? : ($,((P,List(P)) -> Boolean)) -> Boolean
      ++ \axiom{autoReduced?(ts,redOp?)} returns true iff every element of 
      ++ \axiom{ts} is reduced w.r.t to every other in the sense of 
      ++ \axiom{redOp?}

    stronglyReduced? : $ -> Boolean
      ++ \axiom{stronglyReduced?(ts)} returns true iff every element of 
      ++ \axiom{ts} is reduced w.r.t to any other element of \axiom{ts}.

    headReduced? : $ -> Boolean
      ++ headReduced?(ts) returns true iff the head of every element of 
      ++ \axiom{ts} is reduced w.r.t to any other element of \axiom{ts}.

    initiallyReduced? : $ -> Boolean
      ++ initiallyReduced?(ts) returns true iff for every element \axiom{p} 
      ++ of \axiom{ts}. \axiom{p} and all its iterated initials are reduced 
      ++ w.r.t. to the other elements of \axiom{ts} with the same main 
      ++ variable.

    reduce : (P,$,((P,P) -> P),((P,P) -> Boolean) ) -> P
      ++ \axiom{reduce(p,ts,redOp,redOp?)} returns a polynomial \axiom{r}  
      ++ such that \axiom{redOp?(r,p)} holds for every \axiom{p} of 
      ++ \axiom{ts} and there exists some product \axiom{h} of the initials 
      ++ of the members of \axiom{ts} such that \axiom{h*p - r} lies in the 
      ++ ideal generated by \axiom{ts}. The operation \axiom{redOp} must 
      ++ satisfy the following conditions. For every \axiom{p} and \axiom{q} 
      ++ we have  \axiom{redOp?(redOp(p,q),q)} and there exists an integer 
      ++ \axiom{e} and a polynomial \axiom{f} such that 
      ++ \axiom{init(q)^e*p = f*q + redOp(p,q)}. 

    rewriteSetWithReduction : (List P,$,((P,P) -> P),((P,P) -> Boolean) ) ->
     List P
      ++ \axiom{rewriteSetWithReduction(lp,ts,redOp,redOp?)} returns a list 
      ++ \axiom{lq} of polynomials such that 
      ++ \axiom{[reduce(p,ts,redOp,redOp?) for p in lp]} and \axiom{lp} 
      ++ have the same zeros inside the regular zero set of \axiom{ts}. 
      ++ Moreover, for every polynomial \axiom{q} in \axiom{lq} and every 
      ++ polynomial \axiom{t} in \axiom{ts}
      ++ \axiom{redOp?(q,t)} holds and there exists a polynomial \axiom{p}
      ++ in the ideal generated by \axiom{lp} and a product \axiom{h} of 
      ++ \axiom{initials(ts)} such that \axiom{h*p - r} lies in the ideal 
      ++ generated by \axiom{ts}. 
      ++ The operation \axiom{redOp} must satisfy the following conditions.
      ++ For every \axiom{p} and \axiom{q} we have 
      ++ \axiom{redOp?(redOp(p,q),q)}
      ++ and there exists an integer \axiom{e} and a polynomial \axiom{f}
      ++ such that \axiom{init(q)^e*p = f*q + redOp(p,q)}.

    stronglyReduce : (P,$) -> P
      ++ \axiom{stronglyReduce(p,ts)} returns a polynomial \axiom{r} such that
      ++ \axiom{stronglyReduced?(r,ts)} holds and there exists some product 
      ++ \axiom{h} of \axiom{initials(ts)}
      ++ such that \axiom{h*p - r} lies in the ideal generated by \axiom{ts}.

    headReduce : (P,$) -> P
      ++ \axiom{headReduce(p,ts)} returns a polynomial \axiom{r}  such that 
      ++ \axiom{headReduce?(r,ts)} holds and there exists some product 
      ++ \axiom{h} of \axiom{initials(ts)} such that \axiom{h*p - r} lies 
      ++ in the ideal generated by \axiom{ts}.

    initiallyReduce : (P,$) -> P
      ++ \axiom{initiallyReduce(p,ts)} returns a polynomial \axiom{r}  
      ++ such that  \axiom{initiallyReduced?(r,ts)}
      ++ holds and there exists some product \axiom{h} of \axiom{initials(ts)}
      ++ such that \axiom{h*p - r} lies in the ideal generated by \axiom{ts}.

    removeZero : (P, $) -> P
      ++ \axiom{removeZero(p,ts)} returns \axiom{0} if \axiom{p} reduces
      ++ to \axiom{0} by pseudo-division w.r.t \axiom{ts} otherwise
      ++ returns a polynomial \axiom{q} computed from \axiom{p}
      ++ by removing any coefficient in \axiom{p} reducing to \axiom{0}.

    collectQuasiMonic : $ -> $
      ++ \axiom{collectQuasiMonic(ts)} returns the subset of \axiom{ts}
      ++ consisting of the polynomials with initial in \axiom{R}.

    reduceByQuasiMonic : (P, $) -> P
      ++ \axiom{reduceByQuasiMonic(p,ts)} returns the same as
      ++ \axiom{remainder(p,collectQuasiMonic(ts)).polnum}.

    zeroSetSplit : List P -> List $
      ++ \axiom{zeroSetSplit(lp)} returns a list \axiom{lts} of triangular 
      ++ sets such that the zero set of \axiom{lp} is the union of the 
      ++ closures of the regular zero sets  of the members of \axiom{lts}.

    zeroSetSplitIntoTriangularSystems : List P -> _
     List Record(close:$,open:List P)
      ++ \axiom{zeroSetSplitIntoTriangularSystems(lp)} returns a list of 
      ++ triangular systems \axiom{[[ts1,qs1],...,[tsn,qsn]]} such that the 
      ++ zero set of \axiom{lp} is the union of the closures of the 
      ++ \axiom{W_i} where \axiom{W_i} consists of the zeros of \axiom{ts} 
      ++ which do not cancel any polynomial in \axiom{qsi}.

    first : $ -> Union(P,"failed")
      ++ \axiom{first(ts)} returns the polynomial of \axiom{ts} with 
      ++ greatest main variable if \axiom{ts} is not empty, otherwise 
      ++ returns \axiom{"failed"}.

    last : $ -> Union(P,"failed")
      ++ \axiom{last(ts)} returns the polynomial of \axiom{ts} with 
      ++ smallest main variable if \axiom{ts} is not empty, otherwise 
      ++ returns \axiom{"failed"}.

    rest : $ -> Union($,"failed")
      ++ \axiom{rest(ts)} returns the polynomials of \axiom{ts} with smaller 
      ++ main variable than \axiom{mvar(ts)} if \axiom{ts} is not empty, 
      ++ otherwise returns "failed"

    algebraicVariables : $ -> List(V)
      ++ \axiom{algebraicVariables(ts)} returns the decreasingly sorted 
      ++ list of the main variables of the polynomials of \axiom{ts}.

    algebraic? : (V,$) -> Boolean
      ++ \axiom{algebraic?(v,ts)} returns true iff \axiom{v} is the 
      ++ main variable of some polynomial in \axiom{ts}.

    select : ($,V) -> Union(P,"failed")
      ++ \axiom{select(ts,v)} returns the polynomial of \axiom{ts} with 
      ++ \axiom{v} as main variable, if any.

    extendIfCan : ($,P) -> Union($,"failed")
      ++ \axiom{extendIfCan(ts,p)} returns a triangular set which encodes 
      ++ the simple extension by \axiom{p} of the extension of the base 
      ++ field defined by \axiom{ts}, according
      ++ to the properties of triangular sets of the current domain.
      ++ If the required properties do not hold then "failed" is returned.
      ++ This operation encodes in some sense the properties of the
      ++ triangular sets of the current category. Is is used to implement
      ++ the \axiom{construct} operation to guarantee that every triangular
      ++ set build from a list of polynomials has the required properties.

    extend : ($,P) -> $
      ++ \axiom{extend(ts,p)} returns a triangular set which encodes the 
      ++ simple extension by \axiom{p} of the extension of the base field 
      ++ defined by \axiom{ts}, according to the properties of triangular 
      ++ sets of the current category. If the required properties do not 
      ++ hold an error is returned.

    if V has Finite then

      coHeight : $ -> NonNegativeInteger
        ++ \axiom{coHeight(ts)} returns \axiom{size()\$V} minus \axiom{\#ts}.

   add
     
     GPS ==> GeneralPolynomialSet(R,E,V,P)
     B ==> Boolean
     RBT ==> Record(bas:$,top:List P)

     ts:$ = us:$ ==
       empty?(ts)$$ => empty?(us)$$
       empty?(us)$$ => false
       first(ts)::P =$P first(us)::P => rest(ts)::$ =$$ rest(us)::$
       false

     infRittWu?(ts,us) ==
       empty?(us)$$ => not empty?(ts)$$
       empty?(ts)$$ => false
       p : P := (last(ts))::P
       q : P := (last(us))::P
       infRittWu?(p,q)$P => true
       supRittWu?(p,q)$P => false
       v : V := mvar(p)
       infRittWu?(collectUpper(ts,v),collectUpper(us,v))$$

     reduced?(p,ts,redOp?) ==
       lp : List P := members(ts)
       while (not empty? lp) and (redOp?(p,first(lp))) repeat
         lp := rest lp
       empty? lp 

     basicSet(ps,redOp?) ==
       ps := remove(zero?,ps)
       any?(ground?,ps) => "failed"::Union(RBT,"failed")
       ps := sort(infRittWu?,ps)
       p,b : P
       bs := empty()$$
       ts : List P := []
       while not empty? ps repeat
         b := first(ps)
         bs := extend(bs,b)$$
         ps := rest ps
         while (not empty? ps) and _
               (not reduced?((p := first(ps)),bs,redOp?)) repeat
           ts := cons(p,ts)
           ps := rest ps
       ([bs,ts]$RBT)::Union(RBT,"failed")

     basicSet(ps,pred?,redOp?) ==
       ps := remove(zero?,ps)
       any?(ground?,ps) => "failed"::Union(RBT,"failed")
       gps : List P := []
       bps : List P := []
       while not empty? ps repeat
         p := first ps
         ps := rest ps  
         if pred?(p)
           then
             gps := cons(p,gps)
           else
             bps := cons(p,bps)
       gps := sort(infRittWu?,gps)
       p,b : P
       bs := empty()$$
       ts : List P := []
       while not empty? gps repeat
         b := first(gps)
         bs := extend(bs,b)$$
         gps := rest gps
         while (not empty? gps) and _
               (not reduced?((p := first(gps)),bs,redOp?)) repeat
           ts := cons(p,ts)
           gps := rest gps
       ts := sort(infRittWu?,concat(ts,bps))
       ([bs,ts]$RBT)::Union(RBT,"failed")

     initials ts ==
       lip : List P := []
       empty? ts => lip
       lp := members(ts)
       while not empty? lp repeat
          p := first(lp)
          if not ground?((ip := init(p)))
            then
              lip := cons(primPartElseUnitCanonical(ip),lip)
          lp := rest lp
       removeDuplicates lip

     degree ts ==
       empty? ts => 0$NonNegativeInteger
       lp := members ts
       d : NonNegativeInteger := mdeg(first lp)
       while not empty? (lp := rest lp) repeat
         d := d * mdeg(first lp)
       d

     quasiComponent ts == 
       [members(ts),initials(ts)]

     normalized?(p,ts) ==
       normalized?(p,members(ts))$P

     stronglyReduced? (p,ts) ==
       reduced?(p,members(ts))$P

     headReduced? (p,ts) ==
       stronglyReduced?(head(p),ts)

     initiallyReduced? (p,ts) ==
       lp : List (P) := members(ts)
       red : Boolean := true
       while (not empty? lp) and (not ground?(p)$P) and red repeat
         while (not empty? lp) and (mvar(first(lp)) > mvar(p)) repeat 
           lp := rest lp
         if (not empty? lp) 
           then
             if  (mvar(first(lp)) = mvar(p))
               then
                 if reduced?(p,first(lp))
                   then
                     lp := rest lp
                     p := init(p)
                   else
                     red := false
               else
                 p := init(p)
       red

     reduce(p,ts,redOp,redOp?) ==
       (empty? ts) or (ground? p) => p
       ts0 := ts
       while (not empty? ts) and (not ground? p) repeat
          reductor := (first ts)::P
          ts := (rest ts)::$
          if not redOp?(p,reductor) 
            then 
              p := redOp(p,reductor)
              ts := ts0
       p

     rewriteSetWithReduction(lp,ts,redOp,redOp?) ==
       trivialIdeal? ts => lp
       lp := remove(zero?,lp)
       empty? lp => lp
       any?(ground?,lp) => [1$P]
       rs : List P := []
       while not empty? lp repeat
         p := first lp
         lp := rest lp
         p := primPartElseUnitCanonical reduce(p,ts,redOp,redOp?)
         if not zero? p
           then 
             if ground? p
               then
                 lp := []
                 rs := [1$P]
               else
                 rs := cons(p,rs)
       removeDuplicates rs

     stronglyReduce(p,ts) ==
       reduce (p,ts,lazyPrem,reduced?)

     headReduce(p,ts) ==
       reduce (p,ts,headReduce,headReduced?)

     initiallyReduce(p,ts) ==
       reduce (p,ts,initiallyReduce,initiallyReduced?)

     removeZero(p,ts) ==
       (ground? p) or (empty? ts) => p
       v := mvar(p)
       ts_v_- := collectUnder(ts,v)
       if algebraic?(v,ts) 
         then
           q := lazyPrem(p,select(ts,v)::P)
           zero? q => return q
           zero? removeZero(q,ts_v_-) => return 0
       empty? ts_v_- => p
       q: P := 0
       while positive? degree(p,v) repeat
          q := removeZero(init(p),ts_v_-) * mainMonomial(p) + q
          p := tail(p)
       q + removeZero(p,ts_v_-)

     reduceByQuasiMonic(p, ts) ==
       (ground? p) or (empty? ts) => p
       remainder(p,collectQuasiMonic(ts)).polnum

     autoReduced?(ts : $,redOp? : ((P,List(P)) -> Boolean)) ==        
       empty? ts => true
       lp : List (P) := members(ts)
       p : P := first(lp)
       lp := rest lp
       while (not empty? lp) and redOp?(p,lp) repeat
          p := first lp
          lp := rest lp
       empty? lp

     stronglyReduced? ts ==
       autoReduced? (ts, reduced?)

     normalized? ts ==
       autoReduced? (ts,normalized?)

     headReduced? ts ==
       autoReduced? (ts,headReduced?)

     initiallyReduced?  ts ==
       autoReduced? (ts,initiallyReduced?)
         
     mvar ts ==
       empty? ts => error"Error from TSETCAT in mvar : #1 is empty"
       mvar((first(ts))::P)$P

     first ts ==
       empty? ts => "failed"::Union(P,"failed")
       lp : List(P) := sort(supRittWu?,members(ts))$(List P)
       first(lp)::Union(P,"failed")

     last ts ==
       empty? ts => "failed"::Union(P,"failed")
       lp : List(P) := sort(infRittWu?,members(ts))$(List P)
       first(lp)::Union(P,"failed")

     rest ts ==
       empty? ts => "failed"::Union($,"failed")
       lp : List(P) := sort(supRittWu?,members(ts))$(List P)
       construct(rest(lp))::Union($,"failed")

     coerce (ts:$) : List(P) == 
       sort(supRittWu?,members(ts))$(List P)

     algebraicVariables ts ==
       [mvar(p) for p in members(ts)]

     algebraic? (v,ts) ==
       member?(v,algebraicVariables(ts))

     select  (ts,v) ==
       lp : List (P) := sort(supRittWu?,members(ts))$(List P)
       while (not empty? lp) and (not (v = mvar(first lp))) repeat
         lp := rest lp
       empty? lp => "failed"::Union(P,"failed")
       (first lp)::Union(P,"failed")

     collectQuasiMonic ts ==
       lp: List(P) := members(ts)
       newlp: List(P) := []
       while (not empty? lp) repeat
         if ground? init(first(lp)) then newlp := cons(first(lp),newlp)
         lp := rest lp
       construct(newlp)

     collectUnder (ts,v) ==
       lp : List (P) := sort(supRittWu?,members(ts))$(List P)
       while (not empty? lp) and (not (v > mvar(first lp))) repeat
         lp := rest lp       
       construct(lp)

     collectUpper  (ts,v) ==
       lp1 : List(P) := sort(supRittWu?,members(ts))$(List P)
       lp2 : List(P) := []
       while (not empty? lp1) and  (mvar(first lp1) > v) repeat
         lp2 := cons(first(lp1),lp2)
         lp1 := rest lp1
       construct(reverse lp2)

     construct(lp:List(P)) ==
       rif := retractIfCan(lp)@Union($,"failed")
       not (rif case $) => error"in construct : LP -> $ from TSETCAT : bad arg"
       rif::$

     retractIfCan(lp:List(P)) ==
       empty? lp => (empty()$$)::Union($,"failed")
       lp := sort(supRittWu?,lp)
       rif := retractIfCan(rest(lp))@Union($,"failed")
       not (rif case $) => _
        error "in retractIfCan : LP -> ... from TSETCAT : bad arg"
       extendIfCan(rif::$,first(lp))@Union($,"failed")

     extend(ts:$,p:P):$ ==
       eif := extendIfCan(ts,p)@Union($,"failed")
       not (eif case $) => error"in extend : ($,P) -> $ from TSETCAT : bad ars"
       eif::$

     if V has Finite then
        
       coHeight ts ==
         n := size()$V
         m := #(members ts)
         subtractIfCan(n,m)$NonNegativeInteger::NonNegativeInteger