\documentclass{article}
\usepackage{axiom}
\begin{document}
\title{\$SPAD/src/algebra triset.spad}
\author{Marc Moreno Maza}
\maketitle
\begin{abstract}
\end{abstract}
\eject
\tableofcontents
\eject
\section{category TSETCAT TriangularSetCategory}
<<category TSETCAT TriangularSetCategory>>=
)abbrev category TSETCAT TriangularSetCategory
++ Author: Marc Moreno Maza (marc@nag.co.uk)
++ Date Created: 04/26/1994
++ Date Last Updated: 12/15/1998
++ Basic Functions:
++ Related Constructors:
++ Also See:
++ AMS Classifications:
++ Keywords: polynomial, multivariate, ordered variables set
++ 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}. \newline
++ References :
++ [1] P. AUBRY, D. LAZARD and M. MORENO MAZA "On the Theories
++ of Triangular Sets" Journal of Symbol. Comp. (to appear)
++ Version: 4.
TriangularSetCategory(R:IntegralDomain,E:OrderedAbelianMonoidSup,_
V:OrderedSet,P:RecursivePolynomialCategory(R,E,V)):
Category ==
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
@
\section{TSETCAT.lsp BOOTSTRAP}
{\bf TSETCAT} depends on a chain of
files. We need to break this cycle to build the algebra. So we keep a
cached copy of the translated {\bf TSETCAT} category which we can write
into the {\bf MID} directory. We compile the lisp code and copy the
{\bf TSETCAT.o} file to the {\bf OUT} directory. This is eventually
forcibly replaced by a recompiled version.
Note that this code is not included in the generated catdef.spad file.
<<TSETCAT.lsp BOOTSTRAP>>=
(/VERSIONCHECK 2)
(DEFPARAMETER |TriangularSetCategory;CAT| 'NIL)
(DEFPARAMETER |TriangularSetCategory;AL| 'NIL)
(DEFUN |TriangularSetCategory| (&REST #0=#:G1439 &AUX #1=#:G1437)
(DSETQ #1# #0#)
(LET (#2=#:G1438)
(COND
((SETQ #2#
(|assoc| (|devaluateList| #1#) |TriangularSetCategory;AL|))
(CDR #2#))
(T (SETQ |TriangularSetCategory;AL|
(|cons5| (CONS (|devaluateList| #1#)
(SETQ #2#
(APPLY #'|TriangularSetCategory;|
#1#)))
|TriangularSetCategory;AL|))
#2#))))
(DEFUN |TriangularSetCategory;| (|t#1| |t#2| |t#3| |t#4|)
(PROG (#0=#:G1436)
(RETURN
(PROG1 (LETT #0#
(|sublisV|
(PAIR '(|t#1| |t#2| |t#3| |t#4|)
(LIST (|devaluate| |t#1|)
(|devaluate| |t#2|)
(|devaluate| |t#3|)
(|devaluate| |t#4|)))
(COND
(|TriangularSetCategory;CAT|)
('T
(LETT |TriangularSetCategory;CAT|
(|Join| (|PolynomialSetCategory| '|t#1|
'|t#2| '|t#3| '|t#4|)
(|mkCategory| '|domain|
'(((|infRittWu?|
((|Boolean|) $ $))
T)
((|basicSet|
((|Union|
(|Record| (|:| |bas| $)
(|:| |top|
(|List| |t#4|)))
"failed")
(|List| |t#4|)
(|Mapping| (|Boolean|)
|t#4| |t#4|)))
T)
((|basicSet|
((|Union|
(|Record| (|:| |bas| $)
(|:| |top|
(|List| |t#4|)))
"failed")
(|List| |t#4|)
(|Mapping| (|Boolean|)
|t#4|)
(|Mapping| (|Boolean|)
|t#4| |t#4|)))
T)
((|initials|
((|List| |t#4|) $))
T)
((|degree|
((|NonNegativeInteger|) $))
T)
((|quasiComponent|
((|Record|
(|:| |close|
(|List| |t#4|))
(|:| |open|
(|List| |t#4|)))
$))
T)
((|normalized?|
((|Boolean|) |t#4| $))
T)
((|normalized?|
((|Boolean|) $))
T)
((|reduced?|
((|Boolean|) |t#4| $
(|Mapping| (|Boolean|)
|t#4| |t#4|)))
T)
((|stronglyReduced?|
((|Boolean|) |t#4| $))
T)
((|headReduced?|
((|Boolean|) |t#4| $))
T)
((|initiallyReduced?|
((|Boolean|) |t#4| $))
T)
((|autoReduced?|
((|Boolean|) $
(|Mapping| (|Boolean|)
|t#4| (|List| |t#4|))))
T)
((|stronglyReduced?|
((|Boolean|) $))
T)
((|headReduced?|
((|Boolean|) $))
T)
((|initiallyReduced?|
((|Boolean|) $))
T)
((|reduce|
(|t#4| |t#4| $
(|Mapping| |t#4| |t#4|
|t#4|)
(|Mapping| (|Boolean|)
|t#4| |t#4|)))
T)
((|rewriteSetWithReduction|
((|List| |t#4|)
(|List| |t#4|) $
(|Mapping| |t#4| |t#4|
|t#4|)
(|Mapping| (|Boolean|)
|t#4| |t#4|)))
T)
((|stronglyReduce|
(|t#4| |t#4| $))
T)
((|headReduce|
(|t#4| |t#4| $))
T)
((|initiallyReduce|
(|t#4| |t#4| $))
T)
((|removeZero|
(|t#4| |t#4| $))
T)
((|collectQuasiMonic| ($ $))
T)
((|reduceByQuasiMonic|
(|t#4| |t#4| $))
T)
((|zeroSetSplit|
((|List| $)
(|List| |t#4|)))
T)
((|zeroSetSplitIntoTriangularSystems|
((|List|
(|Record|
(|:| |close| $)
(|:| |open|
(|List| |t#4|))))
(|List| |t#4|)))
T)
((|first|
((|Union| |t#4| "failed")
$))
T)
((|last|
((|Union| |t#4| "failed")
$))
T)
((|rest|
((|Union| $ "failed") $))
T)
((|algebraicVariables|
((|List| |t#3|) $))
T)
((|algebraic?|
((|Boolean|) |t#3| $))
T)
((|select|
((|Union| |t#4| "failed")
$ |t#3|))
T)
((|extendIfCan|
((|Union| $ "failed") $
|t#4|))
T)
((|extend| ($ $ |t#4|)) T)
((|coHeight|
((|NonNegativeInteger|) $))
(|has| |t#3| (|Finite|))))
'((|finiteAggregate| T)
(|shallowlyMutable| T))
'((|NonNegativeInteger|)
(|Boolean|) (|List| |t#3|)
(|List|
(|Record| (|:| |close| $)
(|:| |open|
(|List| |t#4|))))
(|List| |t#4|) (|List| $))
NIL))
. #1=(|TriangularSetCategory|))))) . #1#)
(SETELT #0# 0
(LIST '|TriangularSetCategory| (|devaluate| |t#1|)
(|devaluate| |t#2|) (|devaluate| |t#3|)
(|devaluate| |t#4|)))))))
@
\section{TSETCAT-.lsp BOOTSTRAP}
{\bf TSETCAT-} depends on a chain of files.
We need to break this cycle to build
the algebra. So we keep a cached copy of the translated {\bf TSETCAT-}
category which we can write into the {\bf MID} directory. We compile
the lisp code and copy the {\bf TSETCAT-.o} file to the {\bf OUT} directory.
This is eventually forcibly replaced by a recompiled version.
Note that this code is not included in the generated catdef.spad file.
<<TSETCAT-.lsp BOOTSTRAP>>=
(/VERSIONCHECK 2)
(DEFUN |TSETCAT-;=;2SB;1| (|ts| |us| $)
(PROG (#0=#:G1451 #1=#:G1457)
(RETURN
(COND
((SPADCALL |ts| (|getShellEntry| $ 12))
(SPADCALL |us| (|getShellEntry| $ 12)))
((OR (SPADCALL |us| (|getShellEntry| $ 12))
(NULL (SPADCALL
(PROG2 (LETT #0#
(SPADCALL |ts|
(|getShellEntry| $ 14))
|TSETCAT-;=;2SB;1|)
(QCDR #0#)
(|check-union| (QEQCAR #0# 0)
(|getShellEntry| $ 10) #0#))
(PROG2 (LETT #0#
(SPADCALL |us|
(|getShellEntry| $ 14))
|TSETCAT-;=;2SB;1|)
(QCDR #0#)
(|check-union| (QEQCAR #0# 0)
(|getShellEntry| $ 10) #0#))
(|getShellEntry| $ 15))))
'NIL)
('T
(SPADCALL
(PROG2 (LETT #1# (SPADCALL |ts| (|getShellEntry| $ 17))
|TSETCAT-;=;2SB;1|)
(QCDR #1#)
(|check-union| (QEQCAR #1# 0) (|getShellEntry| $ 6) #1#))
(PROG2 (LETT #1# (SPADCALL |us| (|getShellEntry| $ 17))
|TSETCAT-;=;2SB;1|)
(QCDR #1#)
(|check-union| (QEQCAR #1# 0) (|getShellEntry| $ 6) #1#))
(|getShellEntry| $ 18)))))))
(DEFUN |TSETCAT-;infRittWu?;2SB;2| (|ts| |us| $)
(PROG (|p| #0=#:G1464 |q| |v|)
(RETURN
(SEQ (COND
((SPADCALL |us| (|getShellEntry| $ 12))
(SPADCALL (SPADCALL |ts| (|getShellEntry| $ 12))
(|getShellEntry| $ 20)))
((SPADCALL |ts| (|getShellEntry| $ 12)) 'NIL)
('T
(SEQ (LETT |p|
(PROG2 (LETT #0#
(SPADCALL |ts|
(|getShellEntry| $ 21))
|TSETCAT-;infRittWu?;2SB;2|)
(QCDR #0#)
(|check-union| (QEQCAR #0# 0)
(|getShellEntry| $ 10) #0#))
|TSETCAT-;infRittWu?;2SB;2|)
(LETT |q|
(PROG2 (LETT #0#
(SPADCALL |us|
(|getShellEntry| $ 21))
|TSETCAT-;infRittWu?;2SB;2|)
(QCDR #0#)
(|check-union| (QEQCAR #0# 0)
(|getShellEntry| $ 10) #0#))
|TSETCAT-;infRittWu?;2SB;2|)
(EXIT (COND
((SPADCALL |p| |q| (|getShellEntry| $ 22))
'T)
((SPADCALL |p| |q| (|getShellEntry| $ 23))
'NIL)
('T
(SEQ (LETT |v|
(SPADCALL |p|
(|getShellEntry| $ 24))
|TSETCAT-;infRittWu?;2SB;2|)
(EXIT (SPADCALL
(SPADCALL |ts| |v|
(|getShellEntry| $ 25))
(SPADCALL |us| |v|
(|getShellEntry| $ 25))
(|getShellEntry| $ 26))))))))))))))
(DEFUN |TSETCAT-;reduced?;PSMB;3| (|p| |ts| |redOp?| $)
(PROG (|lp|)
(RETURN
(SEQ (LETT |lp| (SPADCALL |ts| (|getShellEntry| $ 29))
|TSETCAT-;reduced?;PSMB;3|)
(SEQ G190
(COND
((NULL (COND
((NULL |lp|) 'NIL)
('T
(SPADCALL |p| (|SPADfirst| |lp|) |redOp?|))))
(GO G191)))
(SEQ (EXIT (LETT |lp| (CDR |lp|)
|TSETCAT-;reduced?;PSMB;3|)))
NIL (GO G190) G191 (EXIT NIL))
(EXIT (NULL |lp|))))))
(DEFUN |TSETCAT-;basicSet;LMU;4| (|ps| |redOp?| $)
(PROG (|b| |bs| |p| |ts|)
(RETURN
(SEQ (LETT |ps| (SPADCALL (ELT $ 32) |ps| (|getShellEntry| $ 34))
|TSETCAT-;basicSet;LMU;4|)
(EXIT (COND
((SPADCALL (ELT $ 35) |ps| (|getShellEntry| $ 36))
(CONS 1 "failed"))
('T
(SEQ (LETT |ps|
(SPADCALL (ELT $ 22) |ps|
(|getShellEntry| $ 37))
|TSETCAT-;basicSet;LMU;4|)
(LETT |bs| (SPADCALL (|getShellEntry| $ 38))
|TSETCAT-;basicSet;LMU;4|)
(LETT |ts| NIL |TSETCAT-;basicSet;LMU;4|)
(SEQ G190
(COND
((NULL (SPADCALL (NULL |ps|)
(|getShellEntry| $ 20)))
(GO G191)))
(SEQ (LETT |b| (|SPADfirst| |ps|)
|TSETCAT-;basicSet;LMU;4|)
(LETT |bs|
(SPADCALL |bs| |b|
(|getShellEntry| $ 39))
|TSETCAT-;basicSet;LMU;4|)
(LETT |ps| (CDR |ps|)
|TSETCAT-;basicSet;LMU;4|)
(EXIT
(SEQ G190
(COND
((NULL
(COND
((NULL |ps|) 'NIL)
('T
(SPADCALL
(SPADCALL
(LETT |p|
(|SPADfirst| |ps|)
|TSETCAT-;basicSet;LMU;4|)
|bs| |redOp?|
(|getShellEntry| $ 40))
(|getShellEntry| $ 20)))))
(GO G191)))
(SEQ
(LETT |ts| (CONS |p| |ts|)
|TSETCAT-;basicSet;LMU;4|)
(EXIT
(LETT |ps| (CDR |ps|)
|TSETCAT-;basicSet;LMU;4|)))
NIL (GO G190) G191 (EXIT NIL))))
NIL (GO G190) G191 (EXIT NIL))
(EXIT (CONS 0 (CONS |bs| |ts|)))))))))))
(DEFUN |TSETCAT-;basicSet;LMMU;5| (|ps| |pred?| |redOp?| $)
(PROG (|bps| |b| |bs| |p| |gps| |ts|)
(RETURN
(SEQ (LETT |ps| (SPADCALL (ELT $ 32) |ps| (|getShellEntry| $ 34))
|TSETCAT-;basicSet;LMMU;5|)
(EXIT (COND
((SPADCALL (ELT $ 35) |ps| (|getShellEntry| $ 36))
(CONS 1 "failed"))
('T
(SEQ (LETT |gps| NIL |TSETCAT-;basicSet;LMMU;5|)
(LETT |bps| NIL |TSETCAT-;basicSet;LMMU;5|)
(SEQ G190
(COND
((NULL (SPADCALL (NULL |ps|)
(|getShellEntry| $ 20)))
(GO G191)))
(SEQ (LETT |p| (|SPADfirst| |ps|)
|TSETCAT-;basicSet;LMMU;5|)
(LETT |ps| (CDR |ps|)
|TSETCAT-;basicSet;LMMU;5|)
(EXIT
(COND
((SPADCALL |p| |pred?|)
(LETT |gps| (CONS |p| |gps|)
|TSETCAT-;basicSet;LMMU;5|))
('T
(LETT |bps| (CONS |p| |bps|)
|TSETCAT-;basicSet;LMMU;5|)))))
NIL (GO G190) G191 (EXIT NIL))
(LETT |gps|
(SPADCALL (ELT $ 22) |gps|
(|getShellEntry| $ 37))
|TSETCAT-;basicSet;LMMU;5|)
(LETT |bs| (SPADCALL (|getShellEntry| $ 38))
|TSETCAT-;basicSet;LMMU;5|)
(LETT |ts| NIL |TSETCAT-;basicSet;LMMU;5|)
(SEQ G190
(COND
((NULL (SPADCALL (NULL |gps|)
(|getShellEntry| $ 20)))
(GO G191)))
(SEQ (LETT |b| (|SPADfirst| |gps|)
|TSETCAT-;basicSet;LMMU;5|)
(LETT |bs|
(SPADCALL |bs| |b|
(|getShellEntry| $ 39))
|TSETCAT-;basicSet;LMMU;5|)
(LETT |gps| (CDR |gps|)
|TSETCAT-;basicSet;LMMU;5|)
(EXIT
(SEQ G190
(COND
((NULL
(COND
((NULL |gps|) 'NIL)
('T
(SPADCALL
(SPADCALL
(LETT |p|
(|SPADfirst| |gps|)
|TSETCAT-;basicSet;LMMU;5|)
|bs| |redOp?|
(|getShellEntry| $ 40))
(|getShellEntry| $ 20)))))
(GO G191)))
(SEQ
(LETT |ts| (CONS |p| |ts|)
|TSETCAT-;basicSet;LMMU;5|)
(EXIT
(LETT |gps| (CDR |gps|)
|TSETCAT-;basicSet;LMMU;5|)))
NIL (GO G190) G191 (EXIT NIL))))
NIL (GO G190) G191 (EXIT NIL))
(LETT |ts|
(SPADCALL (ELT $ 22)
(SPADCALL |ts| |bps|
(|getShellEntry| $ 44))
(|getShellEntry| $ 37))
|TSETCAT-;basicSet;LMMU;5|)
(EXIT (CONS 0 (CONS |bs| |ts|)))))))))))
(DEFUN |TSETCAT-;initials;SL;6| (|ts| $)
(PROG (|p| |ip| |lip| |lp|)
(RETURN
(SEQ (LETT |lip| NIL |TSETCAT-;initials;SL;6|)
(EXIT (COND
((SPADCALL |ts| (|getShellEntry| $ 12)) |lip|)
('T
(SEQ (LETT |lp|
(SPADCALL |ts| (|getShellEntry| $ 29))
|TSETCAT-;initials;SL;6|)
(SEQ G190
(COND
((NULL (SPADCALL (NULL |lp|)
(|getShellEntry| $ 20)))
(GO G191)))
(SEQ (LETT |p| (|SPADfirst| |lp|)
|TSETCAT-;initials;SL;6|)
(COND
((NULL
(SPADCALL
(LETT |ip|
(SPADCALL |p|
(|getShellEntry| $ 46))
|TSETCAT-;initials;SL;6|)
(|getShellEntry| $ 35)))
(LETT |lip|
(CONS
(SPADCALL |ip|
(|getShellEntry| $ 47))
|lip|)
|TSETCAT-;initials;SL;6|)))
(EXIT
(LETT |lp| (CDR |lp|)
|TSETCAT-;initials;SL;6|)))
NIL (GO G190) G191 (EXIT NIL))
(EXIT (SPADCALL |lip| (|getShellEntry| $ 48)))))))))))
(DEFUN |TSETCAT-;degree;SNni;7| (|ts| $)
(PROG (|lp| |d|)
(RETURN
(SEQ (COND
((SPADCALL |ts| (|getShellEntry| $ 12)) 0)
('T
(SEQ (LETT |lp| (SPADCALL |ts| (|getShellEntry| $ 29))
|TSETCAT-;degree;SNni;7|)
(LETT |d|
(SPADCALL (|SPADfirst| |lp|)
(|getShellEntry| $ 51))
|TSETCAT-;degree;SNni;7|)
(SEQ G190
(COND
((NULL (SPADCALL
(NULL
(LETT |lp| (CDR |lp|)
|TSETCAT-;degree;SNni;7|))
(|getShellEntry| $ 20)))
(GO G191)))
(SEQ (EXIT (LETT |d|
(* |d|
(SPADCALL (|SPADfirst| |lp|)
(|getShellEntry| $ 51)))
|TSETCAT-;degree;SNni;7|)))
NIL (GO G190) G191 (EXIT NIL))
(EXIT |d|))))))))
(DEFUN |TSETCAT-;quasiComponent;SR;8| (|ts| $)
(CONS (SPADCALL |ts| (|getShellEntry| $ 29))
(SPADCALL |ts| (|getShellEntry| $ 53))))
(DEFUN |TSETCAT-;normalized?;PSB;9| (|p| |ts| $)
(SPADCALL |p| (SPADCALL |ts| (|getShellEntry| $ 29))
(|getShellEntry| $ 57)))
(DEFUN |TSETCAT-;stronglyReduced?;PSB;10| (|p| |ts| $)
(SPADCALL |p| (SPADCALL |ts| (|getShellEntry| $ 29))
(|getShellEntry| $ 59)))
(DEFUN |TSETCAT-;headReduced?;PSB;11| (|p| |ts| $)
(SPADCALL (SPADCALL |p| (|getShellEntry| $ 61)) |ts|
(|getShellEntry| $ 62)))
(DEFUN |TSETCAT-;initiallyReduced?;PSB;12| (|p| |ts| $)
(PROG (|lp| |red|)
(RETURN
(SEQ (LETT |lp| (SPADCALL |ts| (|getShellEntry| $ 29))
|TSETCAT-;initiallyReduced?;PSB;12|)
(LETT |red| 'T |TSETCAT-;initiallyReduced?;PSB;12|)
(SEQ G190
(COND
((NULL (COND
((OR (NULL |lp|)
(SPADCALL |p| (|getShellEntry| $ 35)))
'NIL)
('T |red|)))
(GO G191)))
(SEQ (SEQ G190
(COND
((NULL (COND
((NULL |lp|) 'NIL)
('T
(SPADCALL
(SPADCALL |p|
(|getShellEntry| $ 24))
(SPADCALL (|SPADfirst| |lp|)
(|getShellEntry| $ 24))
(|getShellEntry| $ 64)))))
(GO G191)))
(SEQ (EXIT (LETT |lp| (CDR |lp|)
|TSETCAT-;initiallyReduced?;PSB;12|)))
NIL (GO G190) G191 (EXIT NIL))
(EXIT (COND
((NULL (NULL |lp|))
(COND
((SPADCALL
(SPADCALL (|SPADfirst| |lp|)
(|getShellEntry| $ 24))
(SPADCALL |p|
(|getShellEntry| $ 24))
(|getShellEntry| $ 65))
(COND
((SPADCALL |p| (|SPADfirst| |lp|)
(|getShellEntry| $ 66))
(SEQ
(LETT |lp| (CDR |lp|)
|TSETCAT-;initiallyReduced?;PSB;12|)
(EXIT
(LETT |p|
(SPADCALL |p|
(|getShellEntry| $ 46))
|TSETCAT-;initiallyReduced?;PSB;12|))))
('T
(LETT |red| 'NIL
|TSETCAT-;initiallyReduced?;PSB;12|))))
('T
(LETT |p|
(SPADCALL |p|
(|getShellEntry| $ 46))
|TSETCAT-;initiallyReduced?;PSB;12|)))))))
NIL (GO G190) G191 (EXIT NIL))
(EXIT |red|)))))
(DEFUN |TSETCAT-;reduce;PSMMP;13| (|p| |ts| |redOp| |redOp?| $)
(PROG (|ts0| #0=#:G1539 |reductor| #1=#:G1542)
(RETURN
(SEQ (COND
((OR (SPADCALL |ts| (|getShellEntry| $ 12))
(SPADCALL |p| (|getShellEntry| $ 35)))
|p|)
('T
(SEQ (LETT |ts0| |ts| |TSETCAT-;reduce;PSMMP;13|)
(SEQ G190
(COND
((NULL (COND
((SPADCALL |ts|
(|getShellEntry| $ 12))
'NIL)
('T
(SPADCALL
(SPADCALL |p|
(|getShellEntry| $ 35))
(|getShellEntry| $ 20)))))
(GO G191)))
(SEQ (LETT |reductor|
(PROG2
(LETT #0#
(SPADCALL |ts|
(|getShellEntry| $ 14))
|TSETCAT-;reduce;PSMMP;13|)
(QCDR #0#)
(|check-union| (QEQCAR #0# 0)
(|getShellEntry| $ 10) #0#))
|TSETCAT-;reduce;PSMMP;13|)
(LETT |ts|
(PROG2
(LETT #1#
(SPADCALL |ts|
(|getShellEntry| $ 17))
|TSETCAT-;reduce;PSMMP;13|)
(QCDR #1#)
(|check-union| (QEQCAR #1# 0)
(|getShellEntry| $ 6) #1#))
|TSETCAT-;reduce;PSMMP;13|)
(EXIT (COND
((NULL
(SPADCALL |p| |reductor|
|redOp?|))
(SEQ
(LETT |p|
(SPADCALL |p| |reductor|
|redOp|)
|TSETCAT-;reduce;PSMMP;13|)
(EXIT
(LETT |ts| |ts0|
|TSETCAT-;reduce;PSMMP;13|)))))))
NIL (GO G190) G191 (EXIT NIL))
(EXIT |p|))))))))
(DEFUN |TSETCAT-;rewriteSetWithReduction;LSMML;14|
(|lp| |ts| |redOp| |redOp?| $)
(PROG (|p| |rs|)
(RETURN
(SEQ (COND
((SPADCALL |ts| (|getShellEntry| $ 70)) |lp|)
('T
(SEQ (LETT |lp|
(SPADCALL (ELT $ 32) |lp|
(|getShellEntry| $ 34))
|TSETCAT-;rewriteSetWithReduction;LSMML;14|)
(EXIT (COND
((NULL |lp|) |lp|)
((SPADCALL (ELT $ 35) |lp|
(|getShellEntry| $ 36))
(LIST (|spadConstant| $ 71)))
('T
(SEQ (LETT |rs| NIL
|TSETCAT-;rewriteSetWithReduction;LSMML;14|)
(SEQ G190
(COND
((NULL
(SPADCALL (NULL |lp|)
(|getShellEntry| $ 20)))
(GO G191)))
(SEQ
(LETT |p| (|SPADfirst| |lp|)
|TSETCAT-;rewriteSetWithReduction;LSMML;14|)
(LETT |lp| (CDR |lp|)
|TSETCAT-;rewriteSetWithReduction;LSMML;14|)
(LETT |p|
(SPADCALL
(SPADCALL |p| |ts| |redOp|
|redOp?|
(|getShellEntry| $ 72))
(|getShellEntry| $ 47))
|TSETCAT-;rewriteSetWithReduction;LSMML;14|)
(EXIT
(COND
((NULL
(SPADCALL |p|
(|getShellEntry| $ 32)))
(COND
((SPADCALL |p|
(|getShellEntry| $ 35))
(SEQ
(LETT |lp| NIL
|TSETCAT-;rewriteSetWithReduction;LSMML;14|)
(EXIT
(LETT |rs|
(LIST
(|spadConstant| $ 71))
|TSETCAT-;rewriteSetWithReduction;LSMML;14|))))
('T
(LETT |rs|
(CONS |p| |rs|)
|TSETCAT-;rewriteSetWithReduction;LSMML;14|)))))))
NIL (GO G190) G191 (EXIT NIL))
(EXIT (SPADCALL |rs|
(|getShellEntry| $ 48))))))))))))))
(DEFUN |TSETCAT-;stronglyReduce;PSP;15| (|p| |ts| $)
(SPADCALL |p| |ts| (ELT $ 74) (ELT $ 66) (|getShellEntry| $ 72)))
(DEFUN |TSETCAT-;headReduce;PSP;16| (|p| |ts| $)
(SPADCALL |p| |ts| (ELT $ 76) (ELT $ 77) (|getShellEntry| $ 72)))
(DEFUN |TSETCAT-;initiallyReduce;PSP;17| (|p| |ts| $)
(SPADCALL |p| |ts| (ELT $ 79) (ELT $ 80) (|getShellEntry| $ 72)))
(DEFUN |TSETCAT-;removeZero;PSP;18| (|p| |ts| $)
(PROG (|v| |tsv-| #0=#:G1565 #1=#:G1574 |q|)
(RETURN
(SEQ (EXIT (COND
((OR (SPADCALL |p| (|getShellEntry| $ 35))
(SPADCALL |ts| (|getShellEntry| $ 12)))
|p|)
('T
(SEQ (LETT |v|
(SPADCALL |p| (|getShellEntry| $ 24))
|TSETCAT-;removeZero;PSP;18|)
(LETT |tsv-|
(SPADCALL |ts| |v|
(|getShellEntry| $ 82))
|TSETCAT-;removeZero;PSP;18|)
(COND
((SPADCALL |v| |ts| (|getShellEntry| $ 83))
(SEQ (LETT |q|
(SPADCALL |p|
(PROG2
(LETT #0#
(SPADCALL |ts| |v|
(|getShellEntry| $ 84))
|TSETCAT-;removeZero;PSP;18|)
(QCDR #0#)
(|check-union| (QEQCAR #0# 0)
(|getShellEntry| $ 10) #0#))
(|getShellEntry| $ 74))
|TSETCAT-;removeZero;PSP;18|)
(EXIT (COND
((SPADCALL |q|
(|getShellEntry| $ 32))
(PROGN
(LETT #1# |q|
|TSETCAT-;removeZero;PSP;18|)
(GO #1#)))
((SPADCALL
(SPADCALL |q| |tsv-|
(|getShellEntry| $ 85))
(|getShellEntry| $ 32))
(PROGN
(LETT #1#
(|spadConstant| $ 86)
|TSETCAT-;removeZero;PSP;18|)
(GO #1#))))))))
(EXIT (COND
((SPADCALL |tsv-|
(|getShellEntry| $ 12))
|p|)
('T
(SEQ (LETT |q| (|spadConstant| $ 86)
|TSETCAT-;removeZero;PSP;18|)
(SEQ G190
(COND
((NULL
(SPADCALL
(SPADCALL |p| |v|
(|getShellEntry| $ 87))
(|getShellEntry| $ 89)))
(GO G191)))
(SEQ
(LETT |q|
(SPADCALL
(SPADCALL
(SPADCALL
(SPADCALL |p|
(|getShellEntry| $ 46))
|tsv-|
(|getShellEntry| $ 85))
(SPADCALL |p|
(|getShellEntry| $ 90))
(|getShellEntry| $ 91))
|q| (|getShellEntry| $ 92))
|TSETCAT-;removeZero;PSP;18|)
(EXIT
(LETT |p|
(SPADCALL |p|
(|getShellEntry| $ 93))
|TSETCAT-;removeZero;PSP;18|)))
NIL (GO G190) G191 (EXIT NIL))
(EXIT
(SPADCALL |q|
(SPADCALL |p| |tsv-|
(|getShellEntry| $ 85))
(|getShellEntry| $ 92)))))))))))
#1# (EXIT #1#)))))
(DEFUN |TSETCAT-;reduceByQuasiMonic;PSP;19| (|p| |ts| $)
(COND
((OR (SPADCALL |p| (|getShellEntry| $ 35))
(SPADCALL |ts| (|getShellEntry| $ 12)))
|p|)
('T
(QVELT (SPADCALL |p| (SPADCALL |ts| (|getShellEntry| $ 95))
(|getShellEntry| $ 97))
1))))
(DEFUN |TSETCAT-;autoReduced?;SMB;20| (|ts| |redOp?| $)
(PROG (|p| |lp|)
(RETURN
(SEQ (COND
((SPADCALL |ts| (|getShellEntry| $ 12)) 'T)
('T
(SEQ (LETT |lp| (SPADCALL |ts| (|getShellEntry| $ 29))
|TSETCAT-;autoReduced?;SMB;20|)
(LETT |p| (|SPADfirst| |lp|)
|TSETCAT-;autoReduced?;SMB;20|)
(LETT |lp| (CDR |lp|)
|TSETCAT-;autoReduced?;SMB;20|)
(SEQ G190
(COND
((NULL (COND
((NULL |lp|) 'NIL)
('T (SPADCALL |p| |lp| |redOp?|))))
(GO G191)))
(SEQ (LETT |p| (|SPADfirst| |lp|)
|TSETCAT-;autoReduced?;SMB;20|)
(EXIT (LETT |lp| (CDR |lp|)
|TSETCAT-;autoReduced?;SMB;20|)))
NIL (GO G190) G191 (EXIT NIL))
(EXIT (NULL |lp|)))))))))
(DEFUN |TSETCAT-;stronglyReduced?;SB;21| (|ts| $)
(SPADCALL |ts| (ELT $ 59) (|getShellEntry| $ 101)))
(DEFUN |TSETCAT-;normalized?;SB;22| (|ts| $)
(SPADCALL |ts| (ELT $ 57) (|getShellEntry| $ 101)))
(DEFUN |TSETCAT-;headReduced?;SB;23| (|ts| $)
(SPADCALL |ts| (ELT $ 104) (|getShellEntry| $ 101)))
(DEFUN |TSETCAT-;initiallyReduced?;SB;24| (|ts| $)
(SPADCALL |ts| (ELT $ 106) (|getShellEntry| $ 101)))
(DEFUN |TSETCAT-;mvar;SV;25| (|ts| $)
(PROG (#0=#:G1593)
(RETURN
(COND
((SPADCALL |ts| (|getShellEntry| $ 12))
(|error| "Error from TSETCAT in mvar : #1 is empty"))
('T
(SPADCALL
(PROG2 (LETT #0# (SPADCALL |ts| (|getShellEntry| $ 14))
|TSETCAT-;mvar;SV;25|)
(QCDR #0#)
(|check-union| (QEQCAR #0# 0) (|getShellEntry| $ 10)
#0#))
(|getShellEntry| $ 24)))))))
(DEFUN |TSETCAT-;first;SU;26| (|ts| $)
(PROG (|lp|)
(RETURN
(SEQ (COND
((SPADCALL |ts| (|getShellEntry| $ 12)) (CONS 1 "failed"))
('T
(SEQ (LETT |lp|
(SPADCALL (ELT $ 23)
(SPADCALL |ts| (|getShellEntry| $ 29))
(|getShellEntry| $ 37))
|TSETCAT-;first;SU;26|)
(EXIT (CONS 0 (|SPADfirst| |lp|))))))))))
(DEFUN |TSETCAT-;last;SU;27| (|ts| $)
(PROG (|lp|)
(RETURN
(SEQ (COND
((SPADCALL |ts| (|getShellEntry| $ 12)) (CONS 1 "failed"))
('T
(SEQ (LETT |lp|
(SPADCALL (ELT $ 22)
(SPADCALL |ts| (|getShellEntry| $ 29))
(|getShellEntry| $ 37))
|TSETCAT-;last;SU;27|)
(EXIT (CONS 0 (|SPADfirst| |lp|))))))))))
(DEFUN |TSETCAT-;rest;SU;28| (|ts| $)
(PROG (|lp|)
(RETURN
(SEQ (COND
((SPADCALL |ts| (|getShellEntry| $ 12)) (CONS 1 "failed"))
('T
(SEQ (LETT |lp|
(SPADCALL (ELT $ 23)
(SPADCALL |ts| (|getShellEntry| $ 29))
(|getShellEntry| $ 37))
|TSETCAT-;rest;SU;28|)
(EXIT (CONS 0
(SPADCALL (CDR |lp|)
(|getShellEntry| $ 111)))))))))))
(DEFUN |TSETCAT-;coerce;SL;29| (|ts| $)
(SPADCALL (ELT $ 23) (SPADCALL |ts| (|getShellEntry| $ 29))
(|getShellEntry| $ 37)))
(DEFUN |TSETCAT-;algebraicVariables;SL;30| (|ts| $)
(PROG (#0=#:G1618 |p| #1=#:G1619)
(RETURN
(SEQ (PROGN
(LETT #0# NIL |TSETCAT-;algebraicVariables;SL;30|)
(SEQ (LETT |p| NIL |TSETCAT-;algebraicVariables;SL;30|)
(LETT #1# (SPADCALL |ts| (|getShellEntry| $ 29))
|TSETCAT-;algebraicVariables;SL;30|)
G190
(COND
((OR (ATOM #1#)
(PROGN
(LETT |p| (CAR #1#)
|TSETCAT-;algebraicVariables;SL;30|)
NIL))
(GO G191)))
(SEQ (EXIT (LETT #0#
(CONS
(SPADCALL |p|
(|getShellEntry| $ 24))
#0#)
|TSETCAT-;algebraicVariables;SL;30|)))
(LETT #1# (CDR #1#)
|TSETCAT-;algebraicVariables;SL;30|)
(GO G190) G191 (EXIT (NREVERSE0 #0#))))))))
(DEFUN |TSETCAT-;algebraic?;VSB;31| (|v| |ts| $)
(SPADCALL |v| (SPADCALL |ts| (|getShellEntry| $ 116))
(|getShellEntry| $ 117)))
(DEFUN |TSETCAT-;select;SVU;32| (|ts| |v| $)
(PROG (|lp|)
(RETURN
(SEQ (LETT |lp|
(SPADCALL (ELT $ 23)
(SPADCALL |ts| (|getShellEntry| $ 29))
(|getShellEntry| $ 37))
|TSETCAT-;select;SVU;32|)
(SEQ G190
(COND
((NULL (COND
((NULL |lp|) 'NIL)
('T
(SPADCALL
(SPADCALL |v|
(SPADCALL (|SPADfirst| |lp|)
(|getShellEntry| $ 24))
(|getShellEntry| $ 65))
(|getShellEntry| $ 20)))))
(GO G191)))
(SEQ (EXIT (LETT |lp| (CDR |lp|)
|TSETCAT-;select;SVU;32|)))
NIL (GO G190) G191 (EXIT NIL))
(EXIT (COND
((NULL |lp|) (CONS 1 "failed"))
('T (CONS 0 (|SPADfirst| |lp|)))))))))
(DEFUN |TSETCAT-;collectQuasiMonic;2S;33| (|ts| $)
(PROG (|newlp| |lp|)
(RETURN
(SEQ (LETT |lp| (SPADCALL |ts| (|getShellEntry| $ 29))
|TSETCAT-;collectQuasiMonic;2S;33|)
(LETT |newlp| NIL |TSETCAT-;collectQuasiMonic;2S;33|)
(SEQ G190
(COND
((NULL (SPADCALL (NULL |lp|) (|getShellEntry| $ 20)))
(GO G191)))
(SEQ (COND
((SPADCALL
(SPADCALL (|SPADfirst| |lp|)
(|getShellEntry| $ 46))
(|getShellEntry| $ 35))
(LETT |newlp| (CONS (|SPADfirst| |lp|) |newlp|)
|TSETCAT-;collectQuasiMonic;2S;33|)))
(EXIT (LETT |lp| (CDR |lp|)
|TSETCAT-;collectQuasiMonic;2S;33|)))
NIL (GO G190) G191 (EXIT NIL))
(EXIT (SPADCALL |newlp| (|getShellEntry| $ 111)))))))
(DEFUN |TSETCAT-;collectUnder;SVS;34| (|ts| |v| $)
(PROG (|lp|)
(RETURN
(SEQ (LETT |lp|
(SPADCALL (ELT $ 23)
(SPADCALL |ts| (|getShellEntry| $ 29))
(|getShellEntry| $ 37))
|TSETCAT-;collectUnder;SVS;34|)
(SEQ G190
(COND
((NULL (COND
((NULL |lp|) 'NIL)
('T
(SPADCALL
(SPADCALL
(SPADCALL (|SPADfirst| |lp|)
(|getShellEntry| $ 24))
|v| (|getShellEntry| $ 64))
(|getShellEntry| $ 20)))))
(GO G191)))
(SEQ (EXIT (LETT |lp| (CDR |lp|)
|TSETCAT-;collectUnder;SVS;34|)))
NIL (GO G190) G191 (EXIT NIL))
(EXIT (SPADCALL |lp| (|getShellEntry| $ 111)))))))
(DEFUN |TSETCAT-;collectUpper;SVS;35| (|ts| |v| $)
(PROG (|lp2| |lp1|)
(RETURN
(SEQ (LETT |lp1|
(SPADCALL (ELT $ 23)
(SPADCALL |ts| (|getShellEntry| $ 29))
(|getShellEntry| $ 37))
|TSETCAT-;collectUpper;SVS;35|)
(LETT |lp2| NIL |TSETCAT-;collectUpper;SVS;35|)
(SEQ G190
(COND
((NULL (COND
((NULL |lp1|) 'NIL)
('T
(SPADCALL |v|
(SPADCALL (|SPADfirst| |lp1|)
(|getShellEntry| $ 24))
(|getShellEntry| $ 64)))))
(GO G191)))
(SEQ (LETT |lp2| (CONS (|SPADfirst| |lp1|) |lp2|)
|TSETCAT-;collectUpper;SVS;35|)
(EXIT (LETT |lp1| (CDR |lp1|)
|TSETCAT-;collectUpper;SVS;35|)))
NIL (GO G190) G191 (EXIT NIL))
(EXIT (SPADCALL (REVERSE |lp2|) (|getShellEntry| $ 111)))))))
(DEFUN |TSETCAT-;construct;LS;36| (|lp| $)
(PROG (|rif|)
(RETURN
(SEQ (LETT |rif| (SPADCALL |lp| (|getShellEntry| $ 123))
|TSETCAT-;construct;LS;36|)
(EXIT (COND
((QEQCAR |rif| 0) (QCDR |rif|))
('T
(|error| "in construct : LP -> $ from TSETCAT : bad arg"))))))))
(DEFUN |TSETCAT-;retractIfCan;LU;37| (|lp| $)
(PROG (|rif|)
(RETURN
(SEQ (COND
((NULL |lp|) (CONS 0 (SPADCALL (|getShellEntry| $ 38))))
('T
(SEQ (LETT |lp|
(SPADCALL (ELT $ 23) |lp|
(|getShellEntry| $ 37))
|TSETCAT-;retractIfCan;LU;37|)
(LETT |rif|
(SPADCALL (CDR |lp|) (|getShellEntry| $ 123))
|TSETCAT-;retractIfCan;LU;37|)
(EXIT (COND
((QEQCAR |rif| 0)
(SPADCALL (QCDR |rif|) (|SPADfirst| |lp|)
(|getShellEntry| $ 125)))
('T
(|error| "in retractIfCan : LP -> ... from TSETCAT : bad arg")))))))))))
(DEFUN |TSETCAT-;extend;SPS;38| (|ts| |p| $)
(PROG (|eif|)
(RETURN
(SEQ (LETT |eif| (SPADCALL |ts| |p| (|getShellEntry| $ 125))
|TSETCAT-;extend;SPS;38|)
(EXIT (COND
((QEQCAR |eif| 0) (QCDR |eif|))
('T
(|error| "in extend : ($,P) -> $ from TSETCAT : bad ars"))))))))
(DEFUN |TSETCAT-;coHeight;SNni;39| (|ts| $)
(PROG (|n| |m| #0=#:G1659)
(RETURN
(SEQ (LETT |n| (SPADCALL (|getShellEntry| $ 128))
|TSETCAT-;coHeight;SNni;39|)
(LETT |m| (LENGTH (SPADCALL |ts| (|getShellEntry| $ 29)))
|TSETCAT-;coHeight;SNni;39|)
(EXIT (PROG2 (LETT #0#
(SPADCALL |n| |m|
(|getShellEntry| $ 129))
|TSETCAT-;coHeight;SNni;39|)
(QCDR #0#)
(|check-union| (QEQCAR #0# 0) (|NonNegativeInteger|)
#0#)))))))
(DEFUN |TriangularSetCategory&| (|#1| |#2| |#3| |#4| |#5|)
(PROG (|dv$1| |dv$2| |dv$3| |dv$4| |dv$5| |dv$| $ |pv$|)
(RETURN
(PROGN
(LETT |dv$1| (|devaluate| |#1|)
. #0=(|TriangularSetCategory&|))
(LETT |dv$2| (|devaluate| |#2|) . #0#)
(LETT |dv$3| (|devaluate| |#3|) . #0#)
(LETT |dv$4| (|devaluate| |#4|) . #0#)
(LETT |dv$5| (|devaluate| |#5|) . #0#)
(LETT |dv$|
(LIST '|TriangularSetCategory&| |dv$1| |dv$2| |dv$3|
|dv$4| |dv$5|) . #0#)
(LETT $ (|newShell| 132) . #0#)
(|setShellEntry| $ 0 |dv$|)
(|setShellEntry| $ 3
(LETT |pv$|
(|buildPredVector| 0 0
(LIST (|HasCategory| |#4| '(|Finite|)))) . #0#))
(|stuffDomainSlots| $)
(|setShellEntry| $ 6 |#1|)
(|setShellEntry| $ 7 |#2|)
(|setShellEntry| $ 8 |#3|)
(|setShellEntry| $ 9 |#4|)
(|setShellEntry| $ 10 |#5|)
(COND
((|testBitVector| |pv$| 1)
(|setShellEntry| $ 130
(CONS (|dispatchFunction| |TSETCAT-;coHeight;SNni;39|)
$))))
$))))
(MAKEPROP '|TriangularSetCategory&| '|infovec|
(LIST '#(NIL NIL NIL NIL NIL NIL (|local| |#1|) (|local| |#2|)
(|local| |#3|) (|local| |#4|) (|local| |#5|) (|Boolean|)
(0 . |empty?|) (|Union| 10 '"failed") (5 . |first|)
(10 . =) (|Union| $ '"failed") (16 . |rest|) (21 . =)
|TSETCAT-;=;2SB;1| (27 . |not|) (32 . |last|)
(37 . |infRittWu?|) (43 . |supRittWu?|) (49 . |mvar|)
(54 . |collectUpper|) (60 . |infRittWu?|)
|TSETCAT-;infRittWu?;2SB;2| (|List| 10) (66 . |members|)
(|Mapping| 11 10 10) |TSETCAT-;reduced?;PSMB;3|
(71 . |zero?|) (|Mapping| 11 10) (76 . |remove|)
(82 . |ground?|) (87 . |any?|) (93 . |sort|)
(99 . |empty|) (103 . |extend|) (109 . |reduced?|)
(|Record| (|:| |bas| $) (|:| |top| 28))
(|Union| 41 '"failed") |TSETCAT-;basicSet;LMU;4|
(116 . |concat|) |TSETCAT-;basicSet;LMMU;5| (122 . |init|)
(127 . |primPartElseUnitCanonical|)
(132 . |removeDuplicates|) |TSETCAT-;initials;SL;6|
(|NonNegativeInteger|) (137 . |mdeg|)
|TSETCAT-;degree;SNni;7| (142 . |initials|)
(|Record| (|:| |close| 28) (|:| |open| 28))
|TSETCAT-;quasiComponent;SR;8| (|List| $)
(147 . |normalized?|) |TSETCAT-;normalized?;PSB;9|
(153 . |reduced?|) |TSETCAT-;stronglyReduced?;PSB;10|
(159 . |head|) (164 . |stronglyReduced?|)
|TSETCAT-;headReduced?;PSB;11| (170 . <) (176 . =)
(182 . |reduced?|) |TSETCAT-;initiallyReduced?;PSB;12|
(|Mapping| 10 10 10) |TSETCAT-;reduce;PSMMP;13|
(188 . |trivialIdeal?|) (193 . |One|) (197 . |reduce|)
|TSETCAT-;rewriteSetWithReduction;LSMML;14|
(205 . |lazyPrem|) |TSETCAT-;stronglyReduce;PSP;15|
(211 . |headReduce|) (217 . |headReduced?|)
|TSETCAT-;headReduce;PSP;16| (223 . |initiallyReduce|)
(229 . |initiallyReduced?|)
|TSETCAT-;initiallyReduce;PSP;17| (235 . |collectUnder|)
(241 . |algebraic?|) (247 . |select|) (253 . |removeZero|)
(259 . |Zero|) (263 . |degree|) (|Integer|)
(269 . |positive?|) (274 . |mainMonomial|) (279 . *)
(285 . +) (291 . |tail|) |TSETCAT-;removeZero;PSP;18|
(296 . |collectQuasiMonic|)
(|Record| (|:| |rnum| 7) (|:| |polnum| 10) (|:| |den| 7))
(301 . |remainder|) |TSETCAT-;reduceByQuasiMonic;PSP;19|
(|Mapping| 11 10 28) |TSETCAT-;autoReduced?;SMB;20|
(307 . |autoReduced?|) |TSETCAT-;stronglyReduced?;SB;21|
|TSETCAT-;normalized?;SB;22| (313 . |headReduced?|)
|TSETCAT-;headReduced?;SB;23| (319 . |initiallyReduced?|)
|TSETCAT-;initiallyReduced?;SB;24| |TSETCAT-;mvar;SV;25|
|TSETCAT-;first;SU;26| |TSETCAT-;last;SU;27|
(325 . |construct|) |TSETCAT-;rest;SU;28|
|TSETCAT-;coerce;SL;29| (|List| 9)
|TSETCAT-;algebraicVariables;SL;30|
(330 . |algebraicVariables|) (335 . |member?|)
|TSETCAT-;algebraic?;VSB;31| |TSETCAT-;select;SVU;32|
|TSETCAT-;collectQuasiMonic;2S;33|
|TSETCAT-;collectUnder;SVS;34|
|TSETCAT-;collectUpper;SVS;35| (341 . |retractIfCan|)
|TSETCAT-;construct;LS;36| (346 . |extendIfCan|)
|TSETCAT-;retractIfCan;LU;37| |TSETCAT-;extend;SPS;38|
(352 . |size|) (356 . |subtractIfCan|) (362 . |coHeight|)
(|OutputForm|))
'#(|stronglyReduced?| 367 |stronglyReduce| 378 |select| 384
|rewriteSetWithReduction| 390 |retractIfCan| 398 |rest|
403 |removeZero| 408 |reduced?| 414 |reduceByQuasiMonic|
421 |reduce| 427 |quasiComponent| 435 |normalized?| 440
|mvar| 451 |last| 456 |initials| 461 |initiallyReduced?|
466 |initiallyReduce| 477 |infRittWu?| 483 |headReduced?|
489 |headReduce| 500 |first| 506 |extend| 511 |degree| 517
|construct| 522 |collectUpper| 527 |collectUnder| 533
|collectQuasiMonic| 539 |coerce| 544 |coHeight| 549
|basicSet| 554 |autoReduced?| 567 |algebraicVariables| 573
|algebraic?| 578 = 584)
'NIL
(CONS (|makeByteWordVec2| 1 'NIL)
(CONS '#()
(CONS '#()
(|makeByteWordVec2| 130
'(1 6 11 0 12 1 6 13 0 14 2 10 11 0 0
15 1 6 16 0 17 2 6 11 0 0 18 1 11 0 0
20 1 6 13 0 21 2 10 11 0 0 22 2 10 11
0 0 23 1 10 9 0 24 2 6 0 0 9 25 2 6
11 0 0 26 1 6 28 0 29 1 10 11 0 32 2
28 0 33 0 34 1 10 11 0 35 2 28 11 33
0 36 2 28 0 30 0 37 0 6 0 38 2 6 0 0
10 39 3 6 11 10 0 30 40 2 28 0 0 0 44
1 10 0 0 46 1 10 0 0 47 1 28 0 0 48 1
10 50 0 51 1 6 28 0 53 2 10 11 0 56
57 2 10 11 0 56 59 1 10 0 0 61 2 6 11
10 0 62 2 9 11 0 0 64 2 9 11 0 0 65 2
10 11 0 0 66 1 6 11 0 70 0 10 0 71 4
6 10 10 0 68 30 72 2 10 0 0 0 74 2 10
0 0 0 76 2 10 11 0 0 77 2 10 0 0 0 79
2 10 11 0 0 80 2 6 0 0 9 82 2 6 11 9
0 83 2 6 13 0 9 84 2 6 10 10 0 85 0
10 0 86 2 10 50 0 9 87 1 88 11 0 89 1
10 0 0 90 2 10 0 0 0 91 2 10 0 0 0 92
1 10 0 0 93 1 6 0 0 95 2 6 96 10 0 97
2 6 11 0 99 101 2 10 11 0 56 104 2 10
11 0 56 106 1 6 0 28 111 1 6 114 0
116 2 114 11 9 0 117 1 6 16 28 123 2
6 16 0 10 125 0 9 50 128 2 50 16 0 0
129 1 0 50 0 130 1 0 11 0 102 2 0 11
10 0 60 2 0 10 10 0 75 2 0 13 0 9 119
4 0 28 28 0 68 30 73 1 0 16 28 126 1
0 16 0 112 2 0 10 10 0 94 3 0 11 10 0
30 31 2 0 10 10 0 98 4 0 10 10 0 68
30 69 1 0 54 0 55 1 0 11 0 103 2 0 11
10 0 58 1 0 9 0 108 1 0 13 0 110 1 0
28 0 49 1 0 11 0 107 2 0 11 10 0 67 2
0 10 10 0 81 2 0 11 0 0 27 1 0 11 0
105 2 0 11 10 0 63 2 0 10 10 0 78 1 0
13 0 109 2 0 0 0 10 127 1 0 50 0 52 1
0 0 28 124 2 0 0 0 9 122 2 0 0 0 9
121 1 0 0 0 120 1 0 28 0 113 1 0 50 0
130 3 0 42 28 33 30 45 2 0 42 28 30
43 2 0 11 0 99 100 1 0 114 0 115 2 0
11 9 0 118 2 0 11 0 0 19)))))
'|lookupComplete|))
@
\section{domain GTSET GeneralTriangularSet}
<<domain GTSET GeneralTriangularSet>>=
)abbrev domain GTSET GeneralTriangularSet
++ Author: Marc Moreno Maza (marc@nag.co.uk)
++ Date Created: 10/06/1995
++ Date Last Updated: 06/12/1996
++ Basic Functions:
++ Related Constructors:
++ Also See:
++ AMS Classifications:
++ Keywords:
++ Description:
++ A domain constructor of the category \axiomType{TriangularSetCategory}.
++ The only requirement for a list of polynomials to be a member of such
++ a domain is the following: no polynomial is constant and two distinct
++ polynomials have distinct main variables. Such a triangular set may
++ not be auto-reduced or consistent. Triangular sets are stored
++ as sorted lists w.r.t. the main variables of their members but they
++ are displayed in reverse order.\newline
++ References :
++ [1] P. AUBRY, D. LAZARD and M. MORENO MAZA "On the Theories
++ of Triangular Sets" Journal of Symbol. Comp. (to appear)
++ Version: 1
GeneralTriangularSet(R,E,V,P) : Exports == Implementation where
R : IntegralDomain
E : OrderedAbelianMonoidSup
V : OrderedSet
P : RecursivePolynomialCategory(R,E,V)
N ==> NonNegativeInteger
Z ==> Integer
B ==> Boolean
LP ==> List P
PtoP ==> P -> P
Exports == TriangularSetCategory(R,E,V,P)
Implementation == add
Rep ==> LP
rep(s:$):Rep == s pretend Rep
per(l:Rep):$ == l pretend $
copy ts ==
per(copy(rep(ts))$LP)
empty() ==
per([])
empty?(ts:$) ==
empty?(rep(ts))
parts ts ==
rep(ts)
members ts ==
rep(ts)
map (f : PtoP, ts : $) : $ ==
construct(map(f,rep(ts))$LP)$$
map! (f : PtoP, ts : $) : $ ==
construct(map!(f,rep(ts))$LP)$$
member? (p,ts) ==
member?(p,rep(ts))$LP
unitIdealIfCan() ==
"failed"::Union($,"failed")
roughUnitIdeal? ts ==
false
-- the following assume that rep(ts) is decreasingly sorted
-- w.r.t. the main variavles of the polynomials in rep(ts)
coerce(ts:$) : OutputForm ==
lp : List(P) := reverse(rep(ts))
brace([p::OutputForm for p in lp]$List(OutputForm))$OutputForm
mvar ts ==
empty? ts => error"failed in mvar : $ -> V from GTSET"
mvar(first(rep(ts)))$P
first ts ==
empty? ts => "failed"::Union(P,"failed")
first(rep(ts))::Union(P,"failed")
last ts ==
empty? ts => "failed"::Union(P,"failed")
last(rep(ts))::Union(P,"failed")
rest ts ==
empty? ts => "failed"::Union($,"failed")
per(rest(rep(ts)))::Union($,"failed")
coerce(ts:$) : (List P) ==
rep(ts)
collectUpper (ts,v) ==
empty? ts => ts
lp := rep(ts)
newlp : Rep := []
while (not empty? lp) and (mvar(first(lp)) > v) repeat
newlp := cons(first(lp),newlp)
lp := rest lp
per(reverse(newlp))
collectUnder (ts,v) ==
empty? ts => ts
lp := rep(ts)
while (not empty? lp) and (mvar(first(lp)) >= v) repeat
lp := rest lp
per(lp)
-- for another domain of TSETCAT build on this domain GTSET
-- the following operations must be redefined
extendIfCan(ts:$,p:P) ==
ground? p => "failed"::Union($,"failed")
empty? ts => (per([unitCanonical(p)]$LP))::Union($,"failed")
not (mvar(ts) < mvar(p)) => "failed"::Union($,"failed")
(per(cons(p,rep(ts))))::Union($,"failed")
@
\section{package PSETPK PolynomialSetUtilitiesPackage}
<<package PSETPK PolynomialSetUtilitiesPackage>>=
)abbrev package PSETPK PolynomialSetUtilitiesPackage
++ Author: Marc Moreno Maza (marc@nag.co.uk)
++ Date Created: 12/01/1995
++ Date Last Updated: 12/15/1998
++ SPARC Version
++ Basic Operations:
++ Related Domains:
++ Also See:
++ AMS Classifications:
++ Keywords:
++ Examples:
++ References:
++ Description:
++ This package provides modest routines for polynomial system solving.
++ The aim of many of the operations of this package is to remove certain
++ factors in some polynomials in order to avoid unnecessary computations
++ in algorithms involving splitting techniques by partial factorization.
++ Version: 3
PolynomialSetUtilitiesPackage (R,E,V,P) : Exports == Implementation where
R : IntegralDomain
E : OrderedAbelianMonoidSup
V : OrderedSet
P : RecursivePolynomialCategory(R,E,V)
N ==> NonNegativeInteger
Z ==> Integer
B ==> Boolean
LP ==> List P
FP ==> Factored P
T ==> GeneralTriangularSet(R,E,V,P)
RRZ ==> Record(factor: P,exponent: Integer)
RBT ==> Record(bas:T,top:LP)
RUL ==> Record(chs:Union(T,"failed"),rfs:LP)
GPS ==> GeneralPolynomialSet(R,E,V,P)
pf ==> MultivariateFactorize(V, E, R, P)
Exports == with
removeRedundantFactors: LP -> LP
++ \axiom{removeRedundantFactors(lp)} returns \axiom{lq} such that if
++ \axiom{lp = [p1,...,pn]} and \axiom{lq = [q1,...,qm]}
++ then the product \axiom{p1*p2*...*pn} vanishes iff the product \axiom{q1*q2*...*qm} vanishes,
++ and the product of degrees of the \axiom{qi} is not greater than
++ the one of the \axiom{pj}, and no polynomial in \axiom{lq}
++ divides another polynomial in \axiom{lq}. In particular,
++ polynomials lying in the base ring \axiom{R} are removed.
++ Moreover, \axiom{lq} is sorted w.r.t \axiom{infRittWu?}.
++ Furthermore, if R is gcd-domain, the polynomials in \axiom{lq} are
++ pairwise without common non trivial factor.
removeRedundantFactors: (P,P) -> LP
++ \axiom{removeRedundantFactors(p,q)} returns the same as
++ \axiom{removeRedundantFactors([p,q])}
removeSquaresIfCan : LP -> LP
++ \axiom{removeSquaresIfCan(lp)} returns
++ \axiom{removeDuplicates [squareFreePart(p)$P for p in lp]}
++ if \axiom{R} is gcd-domain else returns \axiom{lp}.
unprotectedRemoveRedundantFactors: (P,P) -> LP
++ \axiom{unprotectedRemoveRedundantFactors(p,q)} returns the same as
++ \axiom{removeRedundantFactors(p,q)} but does assume that neither
++ \axiom{p} nor \axiom{q} lie in the base ring \axiom{R} and assumes that
++ \axiom{infRittWu?(p,q)} holds. Moreover, if \axiom{R} is gcd-domain,
++ then \axiom{p} and \axiom{q} are assumed to be square free.
removeRedundantFactors: (LP,P) -> LP
++ \axiom{removeRedundantFactors(lp,q)} returns the same as
++ \axiom{removeRedundantFactors(cons(q,lp))} assuming
++ that \axiom{removeRedundantFactors(lp)} returns \axiom{lp}
++ up to replacing some polynomial \axiom{pj} in \axiom{lp}
++ by some some polynomial \axiom{qj} associated to \axiom{pj}.
removeRedundantFactors : (LP,LP) -> LP
++ \axiom{removeRedundantFactors(lp,lq)} returns the same as
++ \axiom{removeRedundantFactors(concat(lp,lq))} assuming
++ that \axiom{removeRedundantFactors(lp)} returns \axiom{lp}
++ up to replacing some polynomial \axiom{pj} in \axiom{lp}
++ by some polynomial \axiom{qj} associated to \axiom{pj}.
removeRedundantFactors : (LP,LP,(LP -> LP)) -> LP
++ \axiom{removeRedundantFactors(lp,lq,remOp)} returns the same as
++ \axiom{concat(remOp(removeRoughlyRedundantFactorsInPols(lp,lq)),lq)}
++ assuming that \axiom{remOp(lq)} returns \axiom{lq} up to similarity.
certainlySubVariety? : (LP,LP) -> B
++ \axiom{certainlySubVariety?(newlp,lp)} returns true iff for every \axiom{p}
++ in \axiom{lp} the remainder of \axiom{p} by \axiom{newlp} using the division algorithm
++ of Groebner techniques is zero.
possiblyNewVariety? : (LP, List LP) -> B
++ \axiom{possiblyNewVariety?(newlp,llp)} returns true iff for every \axiom{lp}
++ in \axiom{llp} certainlySubVariety?(newlp,lp) does not hold.
probablyZeroDim?: LP -> B
++ \axiom{probablyZeroDim?(lp)} returns true iff the number of polynomials
++ in \axiom{lp} is not smaller than the number of variables occurring
++ in these polynomials.
selectPolynomials : ((P -> B),LP) -> Record(goodPols:LP,badPols:LP)
++ \axiom{selectPolynomials(pred?,ps)} returns \axiom{gps,bps} where
++ \axiom{gps} is a list of the polynomial \axiom{p} in \axiom{ps}
++ such that \axiom{pred?(p)} holds and \axiom{bps} are the other ones.
selectOrPolynomials : (List (P -> B),LP) -> Record(goodPols:LP,badPols:LP)
++ \axiom{selectOrPolynomials(lpred?,ps)} returns \axiom{gps,bps} where
++ \axiom{gps} is a list of the polynomial \axiom{p} in \axiom{ps}
++ such that \axiom{pred?(p)} holds for some \axiom{pred?} in \axiom{lpred?}
++ and \axiom{bps} are the other ones.
selectAndPolynomials : (List (P -> B),LP) -> Record(goodPols:LP,badPols:LP)
++ \axiom{selectAndPolynomials(lpred?,ps)} returns \axiom{gps,bps} where
++ \axiom{gps} is a list of the polynomial \axiom{p} in \axiom{ps}
++ such that \axiom{pred?(p)} holds for every \axiom{pred?} in \axiom{lpred?}
++ and \axiom{bps} are the other ones.
quasiMonicPolynomials : LP -> Record(goodPols:LP,badPols:LP)
++ \axiom{quasiMonicPolynomials(lp)} returns \axiom{qmps,nqmps} where
++ \axiom{qmps} is a list of the quasi-monic polynomials in \axiom{lp}
++ and \axiom{nqmps} are the other ones.
univariate? : P -> B
++ \axiom{univariate?(p)} returns true iff \axiom{p} involves one and
++ only one variable.
univariatePolynomials : LP -> Record(goodPols:LP,badPols:LP)
++ \axiom{univariatePolynomials(lp)} returns \axiom{ups,nups} where
++ \axiom{ups} is a list of the univariate polynomials,
++ and \axiom{nups} are the other ones.
linear? : P -> B
++ \axiom{linear?(p)} returns true iff \axiom{p} does not lie
++ in the base ring \axiom{R} and has main degree \axiom{1}.
linearPolynomials : LP -> Record(goodPols:LP,badPols:LP)
++ \axiom{linearPolynomials(lp)} returns \axiom{lps,nlps} where
++ \axiom{lps} is a list of the linear polynomials in lp,
++ and \axiom{nlps} are the other ones.
bivariate? : P -> B
++ \axiom{bivariate?(p)} returns true iff \axiom{p} involves two and
++ only two variables.
bivariatePolynomials : LP -> Record(goodPols:LP,badPols:LP)
++ \axiom{bivariatePolynomials(lp)} returns \axiom{bps,nbps} where
++ \axiom{bps} is a list of the bivariate polynomials,
++ and \axiom{nbps} are the other ones.
removeRoughlyRedundantFactorsInPols : (LP, LP) -> LP
++ \axiom{removeRoughlyRedundantFactorsInPols(lp,lf)} returns
++ \axiom{newlp}where \axiom{newlp} is obtained from \axiom{lp}
++ by removing in every polynomial \axiom{p} of \axiom{lp}
++ any occurence of a polynomial \axiom{f} in \axiom{lf}.
++ This may involve a lot of exact-quotients computations.
removeRoughlyRedundantFactorsInPols : (LP, LP,B) -> LP
++ \axiom{removeRoughlyRedundantFactorsInPols(lp,lf,opt)} returns
++ the same as \axiom{removeRoughlyRedundantFactorsInPols(lp,lf)}
++ if \axiom{opt} is \axiom{false} and if the previous operation
++ does not return any non null and constant polynomial,
++ else return \axiom{[1]}.
removeRoughlyRedundantFactorsInPol : (P,LP) -> P
++ \axiom{removeRoughlyRedundantFactorsInPol(p,lf)} returns the same as
++ removeRoughlyRedundantFactorsInPols([p],lf,true)
interReduce: LP -> LP
++ \axiom{interReduce(lp)} returns \axiom{lq} such that \axiom{lp}
++ and \axiom{lq} generate the same ideal and no polynomial
++ in \axiom{lq} is reducuble by the others in the sense
++ of Groebner bases. Since no assumptions are required
++ the result may depend on the ordering the reductions are
++ performed.
roughBasicSet: LP -> Union(Record(bas:T,top:LP),"failed")
++ \axiom{roughBasicSet(lp)} returns the smallest (with Ritt-Wu
++ ordering) triangular set contained in \axiom{lp}.
crushedSet: LP -> LP
++ \axiom{crushedSet(lp)} returns \axiom{lq} such that \axiom{lp} and
++ and \axiom{lq} generate the same ideal and no rough basic
++ sets reduce (in the sense of Groebner bases) the other
++ polynomials in \axiom{lq}.
rewriteSetByReducingWithParticularGenerators : (LP,(P->B),((P,P)->B),((P,P)->P)) -> LP
++ \axiom{rewriteSetByReducingWithParticularGenerators(lp,pred?,redOp?,redOp)}
++ returns \axiom{lq} where \axiom{lq} is computed by the following
++ algorithm. Chose a basic set w.r.t. the reduction-test \axiom{redOp?}
++ among the polynomials satisfying property \axiom{pred?},
++ if it is empty then leave, else reduce the other polynomials by
++ this basic set w.r.t. the reduction-operation \axiom{redOp}.
++ Repeat while another basic set with smaller rank can be computed.
++ See code. If \axiom{pred?} is \axiom{quasiMonic?} the ideal is unchanged.
rewriteIdealWithQuasiMonicGenerators : (LP,((P,P)->B),((P,P)->P)) -> LP
++ \axiom{rewriteIdealWithQuasiMonicGenerators(lp,redOp?,redOp)} returns
++ \axiom{lq} where \axiom{lq} and \axiom{lp} generate
++ the same ideal in \axiom{R^(-1) P} and \axiom{lq}
++ has rank not higher than the one of \axiom{lp}.
++ Moreover, \axiom{lq} is computed by reducing \axiom{lp}
++ w.r.t. some basic set of the ideal generated by
++ the quasi-monic polynomials in \axiom{lp}.
if R has GcdDomain
then
squareFreeFactors : P -> LP
++ \axiom{squareFreeFactors(p)} returns the square-free factors of \axiom{p}
++ over \axiom{R}
univariatePolynomialsGcds : LP -> LP
++ \axiom{univariatePolynomialsGcds(lp)} returns \axiom{lg} where
++ \axiom{lg} is a list of the gcds of every pair in \axiom{lp}
++ of univariate polynomials in the same main variable.
univariatePolynomialsGcds : (LP,B) -> LP
++ \axiom{univariatePolynomialsGcds(lp,opt)} returns the same as
++ \axiom{univariatePolynomialsGcds(lp)} if \axiom{opt} is
++ \axiom{false} and if the previous operation does not return
++ any non null and constant polynomial, else return \axiom{[1]}.
removeRoughlyRedundantFactorsInContents : (LP, LP) -> LP
++ \axiom{removeRoughlyRedundantFactorsInContents(lp,lf)} returns
++ \axiom{newlp}where \axiom{newlp} is obtained from \axiom{lp}
++ by removing in the content of every polynomial of \axiom{lp}
++ any occurence of a polynomial \axiom{f} in \axiom{lf}. Moreover,
++ squares over \axiom{R} are first removed in the content
++ of every polynomial of \axiom{lp}.
removeRedundantFactorsInContents : (LP, LP) -> LP
++ \axiom{removeRedundantFactorsInContents(lp,lf)} returns \axiom{newlp}
++ where \axiom{newlp} is obtained from \axiom{lp} by removing
++ in the content of every polynomial of \axiom{lp} any non trivial
++ factor of any polynomial \axiom{f} in \axiom{lf}. Moreover,
++ squares over \axiom{R} are first removed in the content
++ of every polynomial of \axiom{lp}.
removeRedundantFactorsInPols : (LP, LP) -> LP
++ \axiom{removeRedundantFactorsInPols(lp,lf)} returns \axiom{newlp}
++ where \axiom{newlp} is obtained from \axiom{lp} by removing
++ in every polynomial \axiom{p} of \axiom{lp} any non trivial
++ factor of any polynomial \axiom{f} in \axiom{lf}. Moreover,
++ squares over \axiom{R} are first removed in every
++ polynomial \axiom{lp}.
if (R has EuclideanDomain) and (R has CharacteristicZero)
then
irreducibleFactors : LP -> LP
++ \axiom{irreducibleFactors(lp)} returns \axiom{lf} such that if
++ \axiom{lp = [p1,...,pn]} and \axiom{lf = [f1,...,fm]} then
++ \axiom{p1*p2*...*pn=0} means \axiom{f1*f2*...*fm=0}, and the \axiom{fi}
++ are irreducible over \axiom{R} and are pairwise distinct.
lazyIrreducibleFactors : LP -> LP
++ \axiom{lazyIrreducibleFactors(lp)} returns \axiom{lf} such that if
++ \axiom{lp = [p1,...,pn]} and \axiom{lf = [f1,...,fm]} then
++ \axiom{p1*p2*...*pn=0} means \axiom{f1*f2*...*fm=0}, and the \axiom{fi}
++ are irreducible over \axiom{R} and are pairwise distinct.
++ The algorithm tries to avoid factorization into irreducible
++ factors as far as possible and makes previously use of gcd
++ techniques over \axiom{R}.
removeIrreducibleRedundantFactors : (LP, LP) -> LP
++ \axiom{removeIrreducibleRedundantFactors(lp,lq)} returns the same
++ as \axiom{irreducibleFactors(concat(lp,lq))} assuming
++ that \axiom{irreducibleFactors(lp)} returns \axiom{lp}
++ up to replacing some polynomial \axiom{pj} in \axiom{lp}
++ by some polynomial \axiom{qj} associated to \axiom{pj}.
Implementation == add
autoRemainder: T -> List(P)
removeAssociates (lp:LP):LP ==
removeDuplicates [primPartElseUnitCanonical(p) for p in lp]
selectPolynomials (pred?,ps) ==
gps : LP := []
bps : LP := []
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)
bps := sort(infRittWu?,bps)
[gps,bps]
selectOrPolynomials (lpred?,ps) ==
gps : LP := []
bps : LP := []
while not empty? ps repeat
p := first ps
ps := rest ps
clpred? := lpred?
while (not empty? clpred?) and (not (first clpred?)(p)) repeat
clpred? := rest clpred?
if not empty?(clpred?)
then
gps := cons(p,gps)
else
bps := cons(p,bps)
gps := sort(infRittWu?,gps)
bps := sort(infRittWu?,bps)
[gps,bps]
selectAndPolynomials (lpred?,ps) ==
gps : LP := []
bps : LP := []
while not empty? ps repeat
p := first ps
ps := rest ps
clpred? := lpred?
while (not empty? clpred?) and ((first clpred?)(p)) repeat
clpred? := rest clpred?
if empty?(clpred?)
then
gps := cons(p,gps)
else
bps := cons(p,bps)
gps := sort(infRittWu?,gps)
bps := sort(infRittWu?,bps)
[gps,bps]
linear? p ==
ground? p => false
-- one?(mdeg(p))
(mdeg(p) = 1)
linearPolynomials ps ==
selectPolynomials(linear?,ps)
univariate? p ==
ground? p => false
not(ground?(init(p))) => false
tp := tail(p)
ground?(tp) => true
not (mvar(p) = mvar(tp)) => false
univariate?(tp)
univariatePolynomials ps ==
selectPolynomials(univariate?,ps)
bivariate? p ==
ground? p => false
ground? tail(p) => univariate?(init(p))
vp := mvar(p)
vtp := mvar(tail(p))
((ground? init(p)) and (vp = vtp)) => bivariate? tail(p)
((ground? init(p)) and (vp > vtp)) => univariate? tail(p)
not univariate?(init(p)) => false
vip := mvar(init(p))
vip > vtp => false
vip = vtp => univariate? tail(p)
vtp < vp => false
zero? degree(tail(p),vip) => univariate? tail(p)
bivariate? tail(p)
bivariatePolynomials ps ==
selectPolynomials(bivariate?,ps)
quasiMonicPolynomials ps ==
selectPolynomials(quasiMonic?,ps)
removeRoughlyRedundantFactorsInPols (lp,lf,opt) ==
empty? lp => lp
newlp : LP := []
stop : B := false
lp := remove(zero?,lp)
lf := sort(infRittWu?,lf)
test : Union(P,"failed")
while (not empty? lp) and (not stop) repeat
p := first lp
lp := rest lp
copylf := lf
while (not empty? copylf) and (not ground? p) and (not (mvar(p) < mvar(first copylf))) repeat
f := first copylf
copylf := rest copylf
while (((test := p exquo$P f)) case P) repeat
p := test::P
stop := opt and ground?(p)
newlp := cons(unitCanonical(p),newlp)
stop => [1$P]
newlp
removeRoughlyRedundantFactorsInPol(p,lf) ==
zero? p => p
lp : LP := [p]
first removeRoughlyRedundantFactorsInPols (lp,lf,true()$B)
removeRoughlyRedundantFactorsInPols (lp,lf) ==
removeRoughlyRedundantFactorsInPols (lp,lf,false()$B)
possiblyNewVariety?(newlp,llp) ==
while (not empty? llp) and _
(not certainlySubVariety?(newlp,first(llp))) repeat
llp := rest llp
empty? llp
certainlySubVariety?(lp,lq) ==
gs := construct(lp)$GPS
while (not empty? lq) and _
(zero? (remainder(first(lq),gs)$GPS).polnum) repeat
lq := rest lq
empty? lq
probablyZeroDim?(lp: List P) : Boolean ==
m := #lp
lv : List V := variables(first lp)
while not empty? (lp := rest lp) repeat
lv := concat(variables(first lp),lv)
n := #(removeDuplicates lv)
not (n > m)
interReduce(lp: LP): LP ==
ps := lp
rs: List(P) := []
repeat
empty? ps => return rs
ps := sort(supRittWu?, ps)
p := first ps
ps := rest ps
r := remainder(p,[ps]$GPS).polnum
zero? r => "leave"
ground? r => return []
associates?(r,p) => rs := cons(r,rs)
ps := concat(ps,cons(r,rs))
rs := []
roughRed?(p:P,q:P):B ==
ground? p => false
ground? q => true
mvar(p) > mvar(q)
roughBasicSet(lp) == basicSet(lp,roughRed?)$T
autoRemainder(ts:T): List(P) ==
empty? ts => members(ts)
lp := sort(infRittWu?, reverse members(ts))
newlp : List(P) := [primPartElseUnitCanonical first(lp)]
lp := rest(lp)
while not empty? lp repeat
p := (remainder(first(lp),construct(newlp)$GPS)$GPS).polnum
if not zero? p
then
if ground? p
then
newlp := [1$P]
lp := []
else
newlp := cons(p,newlp)
lp := rest(lp)
else
lp := rest(lp)
newlp
crushedSet(lp) ==
rec := roughBasicSet(lp)
contradiction := (rec case "failed")@B
finished : B := false
rs: LP
while (not finished) and (not contradiction) repeat
bs := (rec::RBT).bas
rs := (rec::RBT).top
rs := rewriteIdealWithRemainder(rs,bs)$T
-- contradiction := ((not empty? rs) and (one? first(rs)))
contradiction := ((not empty? rs) and (first(rs) = 1))
if not contradiction
then
rs := concat(rs,autoRemainder(bs))
rec := roughBasicSet(rs)
contradiction := (rec case "failed")@B
not contradiction => finished := not infRittWu?((rec::RBT).bas,bs)
contradiction => [1$P]
rs
rewriteSetByReducingWithParticularGenerators (ps,pred?,redOp?,redOp) ==
rs : LP := remove(zero?,ps)
any?(ground?,rs) => [1$P]
contradiction : B := false
bs1 : T := empty()$T
rec : Union(RBT,"failed")
ar : Union(T,List(P))
stop : B := false
while (not contradiction) and (not stop) repeat
rec := basicSet(rs,pred?,redOp?)$T
bs2 : T := (rec::RBT).bas
rs := (rec::RBT).top
-- ar := autoReduce(bs2,lazyPrem,reduced?)@Union(T,List(P))
ar := bs2::Union(T,List(P))
if (ar case T)@B
then
bs2 := ar::T
if infRittWu?(bs2,bs1)
then
rs := rewriteSetWithReduction(rs,bs2,redOp,redOp?)$T
bs1 := bs2
else
stop := true
rs := concat(members(bs2),rs)
else
rs := concat(ar::LP,rs)
if any?(ground?,rs)
then
contradiction := true
rs := [1$P]
rs
removeRedundantFactors (lp:LP,lq :LP, remOp : (LP -> LP)) ==
-- ASSUME remOp(lp) returns lp up to similarity
lq := removeRoughlyRedundantFactorsInPols(lq,lp,false)
lq := remOp lq
sort(infRittWu?,concat(lp,lq))
removeRedundantFactors (lp:LP,lq :LP) ==
lq := removeRoughlyRedundantFactorsInPols(lq,lp,false)
lq := removeRedundantFactors lq
sort(infRittWu?,concat(lp,lq))
if (R has EuclideanDomain) and (R has CharacteristicZero)
then
irreducibleFactors lp ==
newlp : LP := []
lrrz : List RRZ
rrz : RRZ
fp : FP
while not empty? lp repeat
p := first lp
lp := rest lp
fp := factor(p)$pf
lrrz := factors(fp)$FP
lf := remove(ground?,[rrz.factor for rrz in lrrz])
newlp := concat(lf,newlp)
removeDuplicates newlp
lazyIrreducibleFactors lp ==
lp := removeRedundantFactors(lp)
newlp : LP := []
lrrz : List RRZ
rrz : RRZ
fp : FP
while not empty? lp repeat
p := first lp
lp := rest lp
fp := factor(p)$pf
lrrz := factors(fp)$FP
lf := remove(ground?,[rrz.factor for rrz in lrrz])
newlp := concat(lf,newlp)
newlp
removeIrreducibleRedundantFactors (lp:LP,lq :LP) ==
-- ASSUME lp only contains irreducible factors over R
lq := removeRoughlyRedundantFactorsInPols(lq,lp,false)
lq := irreducibleFactors lq
sort(infRittWu?,concat(lp,lq))
if R has GcdDomain
then
squareFreeFactors(p:P) ==
sfp: Factored P := squareFree(p)$P
lsf: List P := [foo.factor for foo in factors(sfp)]
lsf
univariatePolynomialsGcds (ps,opt) ==
lg : LP := []
pInV : LP
stop : B := false
ps := sort(infRittWu?,ps)
p,g : P
v : V
while (not empty? ps) and (not stop) repeat
while (not empty? ps) and (not univariate?((p := first(ps)))) repeat
ps := rest ps
if not empty? ps
then
v := mvar(p)$P
pInV := [p]
while (not empty? ps) and (mvar((p := first(ps))) = v) repeat
if (univariate?(p))
then
pInV := cons(p,pInV)
ps := rest ps
g := gcd(pInV)$P
stop := opt and (ground? g)
lg := cons(g,lg)
stop => [1$P]
lg
univariatePolynomialsGcds ps ==
univariatePolynomialsGcds (ps,false)
removeSquaresIfCan lp ==
empty? lp => lp
removeDuplicates [squareFreePart(p)$P for p in lp]
rewriteIdealWithQuasiMonicGenerators (ps,redOp?,redOp) ==
ups := removeSquaresIfCan(univariatePolynomialsGcds(ps,true))
ps := removeDuplicates concat(ups,ps)
rewriteSetByReducingWithParticularGenerators(ps,quasiMonic?,redOp?,redOp)
removeRoughlyRedundantFactorsInContents (ps,lf) ==
empty? ps => ps
newps : LP := []
p,newp,cp,newcp,f,g : P
test : Union(P,"failed")
copylf : LP
while not empty? ps repeat
p := first ps
ps := rest ps
cp := mainContent(p)$P
newcp := squareFreePart(cp)$P
newp := (p exquo$P cp)::P
if not ground? newcp
then
copylf := [f for f in lf | mvar(f) <= mvar(newcp)]
while (not empty? copylf) and (not ground? newcp) repeat
f := first copylf
copylf := rest copylf
test := (newcp exquo$P f)
if (test case P)@B
then
newcp := test::P
if ground? newcp
then
newp := unitCanonical(newp)
else
newp := unitCanonical(newp * newcp)
newps := cons(newp,newps)
newps
removeRedundantFactorsInContents (ps,lf) ==
empty? ps => ps
newps : LP := []
p,newp,cp,newcp,f,g : P
while not empty? ps repeat
p := first ps
ps := rest ps
cp := mainContent(p)$P
newcp := squareFreePart(cp)$P
newp := (p exquo$P cp)::P
if not ground? newcp
then
copylf := lf
while (not empty? copylf) and (not ground? newcp) repeat
f := first copylf
copylf := rest copylf
g := gcd(newcp,f)$P
if not ground? g
then
newcp := (newcp exquo$P g)::P
if ground? newcp
then
newp := unitCanonical(newp)
else
newp := unitCanonical(newp * newcp)
newps := cons(newp,newps)
newps
removeRedundantFactorsInPols (ps,lf) ==
empty? ps => ps
newps : LP := []
p,newp,cp,newcp,f,g : P
while not empty? ps repeat
p := first ps
ps := rest ps
cp := mainContent(p)$P
newcp := squareFreePart(cp)$P
newp := (p exquo$P cp)::P
newp := squareFreePart(newp)$P
copylf := lf
while not empty? copylf repeat
f := first copylf
copylf := rest copylf
if not ground? newcp
then
g := gcd(newcp,f)$P
if not ground? g
then
newcp := (newcp exquo$P g)::P
if not ground? newp
then
g := gcd(newp,f)$P
if not ground? g
then
newp := (newp exquo$P g)::P
if ground? newcp
then
newp := unitCanonical(newp)
else
newp := unitCanonical(newp * newcp)
newps := cons(newp,newps)
newps
removeRedundantFactors (a:P,b:P) : LP ==
a := primPartElseUnitCanonical(squareFreePart(a))
b := primPartElseUnitCanonical(squareFreePart(b))
if not infRittWu?(a,b)
then
(a,b) := (b,a)
if ground? a
then
if ground? b
then
return([])
else
return([b])
else
if ground? b
then
return([a])
else
return(unprotectedRemoveRedundantFactors(a,b))
unprotectedRemoveRedundantFactors (a,b) ==
c := b exquo$P a
if (c case P)@B
then
d : P := c::P
if ground? d
then
return([a])
else
return([a,d])
else
g : P := gcd(a,b)$P
if ground? g
then
return([a,b])
else
return([g,(a exquo$P g)::P,(b exquo$P g)::P])
else
removeSquaresIfCan lp ==
lp
rewriteIdealWithQuasiMonicGenerators (ps,redOp?,redOp) ==
rewriteSetByReducingWithParticularGenerators(ps,quasiMonic?,redOp?,redOp)
removeRedundantFactors (a:P,b:P) ==
a := primPartElseUnitCanonical(a)
b := primPartElseUnitCanonical(b)
if not infRittWu?(a,b)
then
(a,b) := (b,a)
if ground? a
then
if ground? b
then
return([])
else
return([b])
else
if ground? b
then
return([a])
else
return(unprotectedRemoveRedundantFactors(a,b))
unprotectedRemoveRedundantFactors (a,b) ==
c := b exquo$P a
if (c case P)@B
then
d : P := c::P
if ground? d
then
return([a])
else
if infRittWu?(d,a) then (a,d) := (d,a)
return(unprotectedRemoveRedundantFactors(a,d))
else
return([a,b])
removeRedundantFactors (lp:LP) ==
lp := remove(ground?, lp)
lp := removeDuplicates [primPartElseUnitCanonical(p) for p in lp]
lp := removeSquaresIfCan lp
lp := removeDuplicates [unitCanonical(p) for p in lp]
empty? lp => lp
size?(lp,1$N)$(List P) => lp
lp := sort(infRittWu?,lp)
p : P := first lp
lp := rest lp
base : LP := unprotectedRemoveRedundantFactors(p,first lp)
top : LP := rest lp
while not empty? top repeat
p := first top
base := removeRedundantFactors(base,p)
top := rest top
base
removeRedundantFactors (lp:LP,a:P) ==
lp := remove(ground?, lp)
lp := sort(infRittWu?, lp)
ground? a => lp
empty? lp => [a]
toSee : LP := lp
toSave : LP := []
while not empty? toSee repeat
b := first toSee
toSee := rest toSee
if not infRittWu?(b,a)
then
(c,d) := (a,b)
else
(c,d) := (b,a)
rrf := unprotectedRemoveRedundantFactors(c,d)
empty? rrf => error"in removeRedundantFactors : (LP,P) -> LP from PSETPK"
c := first rrf
rrf := rest rrf
if empty? rrf
then
if associates?(c,b)
then
toSave := concat(toSave,toSee)
a := b
toSee := []
else
a := c
toSee := concat(toSave,toSee)
toSave := []
else
d := first rrf
rrf := rest rrf
if empty? rrf
then
if associates?(c,b)
then
toSave := concat(toSave,[b])
a := d
else
if associates?(d,b)
then
toSave := concat(toSave,[b])
a := c
else
toSave := removeRedundantFactors(toSave,c)
a := d
else
e := first rrf
not empty? rest(rrf) => error"in removeRedundantFactors:(LP,P)->LP from PSETPK"
-- ASSUME that neither c, nor d, nor e may be associated to b
toSave := removeRedundantFactors(toSave,c)
toSave := removeRedundantFactors(toSave,d)
a := e
if empty? toSee
then
toSave := sort(infRittWu?,cons(a,toSave))
toSave
@
\section{domain WUTSET WuWenTsunTriangularSet}
<<domain WUTSET WuWenTsunTriangularSet>>=
)abbrev domain WUTSET WuWenTsunTriangularSet
++ Author: Marc Moreno Maza (marc@nag.co.uk)
++ Date Created: 11/18/1995
++ Date Last Updated: 12/15/1998
++ Basic Functions:
++ Related Constructors:
++ Also See:
++ AMS Classifications:
++ Keywords:
++ Description: A domain constructor of the category \axiomType{GeneralTriangularSet}.
++ The only requirement for a list of polynomials to be a member of such
++ a domain is the following: no polynomial is constant and two distinct
++ polynomials have distinct main variables. Such a triangular set may
++ not be auto-reduced or consistent. The \axiomOpFrom{construct}{WuWenTsunTriangularSet} operation
++ does not check the previous requirement. Triangular sets are stored
++ as sorted lists w.r.t. the main variables of their members.
++ Furthermore, this domain exports operations dealing with the
++ characteristic set method of Wu Wen Tsun and some optimizations
++ mainly proposed by Dong Ming Wang.\newline
++ References :
++ [1] W. T. WU "A Zero Structure Theorem for polynomial equations solving"
++ MM Research Preprints, 1987.
++ [2] D. M. WANG "An implementation of the characteristic set method in Maple"
++ Proc. DISCO'92. Bath, England.
++ Version: 3
WuWenTsunTriangularSet(R,E,V,P) : Exports == Implementation where
R : IntegralDomain
E : OrderedAbelianMonoidSup
V : OrderedSet
P : RecursivePolynomialCategory(R,E,V)
N ==> NonNegativeInteger
Z ==> Integer
B ==> Boolean
LP ==> List P
A ==> FiniteEdge P
H ==> FiniteSimpleHypergraph P
GPS ==> GeneralPolynomialSet(R,E,V,P)
RBT ==> Record(bas:$,top:LP)
RUL ==> Record(chs:Union($,"failed"),rfs:LP)
pa ==> PolynomialSetUtilitiesPackage(R,E,V,P)
NLpT ==> SplittingNode(LP,$)
ALpT ==> SplittingTree(LP,$)
O ==> OutputForm
OP ==> OutputPackage
Exports == TriangularSetCategory(R,E,V,P) with
medialSet : (LP,((P,P)->B),((P,P)->P)) -> Union($,"failed")
++ \axiom{medialSet(ps,redOp?,redOp)} returns \axiom{bs} a basic set
++ (in Wu Wen Tsun sense w.r.t the reduction-test \axiom{redOp?})
++ of some set generating the same ideal as \axiom{ps} (with
++ rank not higher than any basic set of \axiom{ps}), if no non-zero
++ constant polynomials appear during the computatioms, else
++ \axiom{"failed"} is returned. In the former case, \axiom{bs} has to be
++ understood as a candidate for being a characteristic set of \axiom{ps}.
++ In the original algorithm, \axiom{bs} is simply a basic set of \axiom{ps}.
medialSet: LP -> Union($,"failed")
++ \axiom{medial(ps)} returns the same as
++ \axiom{medialSet(ps,initiallyReduced?,initiallyReduce)}.
characteristicSet : (LP,((P,P)->B),((P,P)->P)) -> Union($,"failed")
++ \axiom{characteristicSet(ps,redOp?,redOp)} returns a non-contradictory
++ characteristic set of \axiom{ps} in Wu Wen Tsun sense w.r.t the
++ reduction-test \axiom{redOp?} (using \axiom{redOp} to reduce
++ polynomials w.r.t a \axiom{redOp?} basic set), if no
++ non-zero constant polynomial appear during those reductions,
++ else \axiom{"failed"} is returned.
++ The operations \axiom{redOp} and \axiom{redOp?} must satisfy
++ the following conditions: \axiom{redOp?(redOp(p,q),q)} holds
++ for every polynomials \axiom{p,q} and there exists an integer
++ \axiom{e} and a polynomial \axiom{f} such that we have
++ \axiom{init(q)^e*p = f*q + redOp(p,q)}.
characteristicSet: LP -> Union($,"failed")
++ \axiom{characteristicSet(ps)} returns the same as
++ \axiom{characteristicSet(ps,initiallyReduced?,initiallyReduce)}.
characteristicSerie : (LP,((P,P)->B),((P,P)->P)) -> List $
++ \axiom{characteristicSerie(ps,redOp?,redOp)} returns a list \axiom{lts}
++ of triangular sets such that the zero set of \axiom{ps} is the
++ union of the regular zero sets of the members of \axiom{lts}.
++ This is made by the Ritt and Wu Wen Tsun process applying
++ the operation \axiom{characteristicSet(ps,redOp?,redOp)}
++ to compute characteristic sets in Wu Wen Tsun sense.
characteristicSerie: LP -> List $
++ \axiom{characteristicSerie(ps)} returns the same as
++ \axiom{characteristicSerie(ps,initiallyReduced?,initiallyReduce)}.
Implementation == GeneralTriangularSet(R,E,V,P) add
removeSquares: $ -> Union($,"failed")
Rep ==> LP
rep(s:$):Rep == s pretend Rep
per(l:Rep):$ == l pretend $
removeAssociates (lp:LP):LP ==
removeDuplicates [primPartElseUnitCanonical(p) for p in lp]
medialSetWithTrace (ps:LP,redOp?:((P,P)->B),redOp:((P,P)->P)):Union(RBT,"failed") ==
qs := rewriteIdealWithQuasiMonicGenerators(ps,redOp?,redOp)$pa
contradiction : B := any?(ground?,ps)
contradiction => "failed"::Union(RBT,"failed")
rs : LP := qs
bs : $
while (not empty? rs) and (not contradiction) repeat
rec := basicSet(rs,redOp?)
contradiction := (rec case "failed")@B
if not contradiction
then
bs := (rec::RBT).bas
rs := (rec::RBT).top
rs := rewriteIdealWithRemainder(rs,bs)
-- contradiction := ((not empty? rs) and (one? first(rs)))
contradiction := ((not empty? rs) and (first(rs) = 1))
if (not empty? rs) and (not contradiction)
then
rs := rewriteSetWithReduction(rs,bs,redOp,redOp?)
-- contradiction := ((not empty? rs) and (one? first(rs)))
contradiction := ((not empty? rs) and (first(rs) = 1))
if (not empty? rs) and (not contradiction)
then
rs := removeDuplicates concat(rs,members(bs))
rs := rewriteIdealWithQuasiMonicGenerators(rs,redOp?,redOp)$pa
-- contradiction := ((not empty? rs) and (one? first(rs)))
contradiction := ((not empty? rs) and (first(rs) = 1))
contradiction => "failed"::Union(RBT,"failed")
([bs,qs]$RBT)::Union(RBT,"failed")
medialSet(ps:LP,redOp?:((P,P)->B),redOp:((P,P)->P)) ==
foo: Union(RBT,"failed") := medialSetWithTrace(ps,redOp?,redOp)
(foo case "failed") => "failed" :: Union($,"failed")
((foo::RBT).bas) :: Union($,"failed")
medialSet(ps:LP) == medialSet(ps,initiallyReduced?,initiallyReduce)
characteristicSetUsingTrace(ps:LP,redOp?:((P,P)->B),redOp:((P,P)->P)):Union($,"failed") ==
ps := removeAssociates ps
ps := remove(zero?,ps)
contradiction : B := any?(ground?,ps)
contradiction => "failed"::Union($,"failed")
rs : LP := ps
qs : LP := ps
ms : $
while (not empty? rs) and (not contradiction) repeat
rec := medialSetWithTrace (qs,redOp?,redOp)
contradiction := (rec case "failed")@B
if not contradiction
then
ms := (rec::RBT).bas
qs := (rec::RBT).top
qs := rewriteIdealWithRemainder(qs,ms)
-- contradiction := ((not empty? qs) and (one? first(qs)))
contradiction := ((not empty? qs) and (first(qs) = 1))
if not contradiction
then
rs := rewriteSetWithReduction(qs,ms,lazyPrem,reduced?)
-- contradiction := ((not empty? rs) and (one? first(rs)))
contradiction := ((not empty? rs) and (first(rs) = 1))
if (not contradiction) and (not empty? rs)
then
qs := removeDuplicates(concat(rs,concat(members(ms),qs)))
contradiction => "failed"::Union($,"failed")
ms::Union($,"failed")
characteristicSet(ps:LP,redOp?:((P,P)->B),redOp:((P,P)->P)) ==
characteristicSetUsingTrace(ps,redOp?,redOp)
characteristicSet(ps:LP) == characteristicSet(ps,initiallyReduced?,initiallyReduce)
characteristicSerie(ps:LP,redOp?:((P,P)->B),redOp:((P,P)->P)) ==
a := [[ps,empty()$$]$NLpT]$ALpT
while ((esl := extractSplittingLeaf(a)) case ALpT) repeat
ps := value(value(esl::ALpT)$ALpT)$NLpT
charSet? := characteristicSetUsingTrace(ps,redOp?,redOp)
if not (charSet? case $)
then
setvalue!(esl::ALpT,[nil()$LP,empty()$$,true]$NLpT)
updateStatus!(a)
else
cs := (charSet?)::$
lics := initials(cs)
lics := removeRedundantFactors(lics)$pa
lics := sort(infRittWu?,lics)
if empty? lics
then
setvalue!(esl::ALpT,[ps,cs,true]$NLpT)
updateStatus!(a)
else
ln : List NLpT := [[nil()$LP,cs,true]$NLpT]
while not empty? lics repeat
newps := cons(first(lics),concat(cs::LP,ps))
lics := rest lics
newps := removeDuplicates newps
newps := sort(infRittWu?,newps)
ln := cons([newps,empty()$$,false]$NLpT,ln)
splitNodeOf!(esl::ALpT,a,ln)
remove(empty()$$,conditions(a))
characteristicSerie(ps:LP) == characteristicSerie (ps,initiallyReduced?,initiallyReduce)
if R has GcdDomain
then
removeSquares (ts:$):Union($,"failed") ==
empty?(ts)$$ => ts::Union($,"failed")
p := (first ts)::P
rsts : Union($,"failed")
rsts := removeSquares((rest ts)::$)
not(rsts case $) => "failed"::Union($,"failed")
newts := rsts::$
empty? newts =>
p := squareFreePart(p)
(per([primitivePart(p)]$LP))::Union($,"failed")
zero? initiallyReduce(init(p),newts) => "failed"::Union($,"failed")
p := primitivePart(removeZero(p,newts))
ground? p => "failed"::Union($,"failed")
not (mvar(newts) < mvar(p)) => "failed"::Union($,"failed")
p := squareFreePart(p)
(per(cons(unitCanonical(p),rep(newts))))::Union($,"failed")
zeroSetSplit lp ==
lts : List $ := characteristicSerie(lp,initiallyReduced?,initiallyReduce)
lts := removeDuplicates(lts)$(List $)
newlts : List $ := []
while not empty? lts repeat
ts := first lts
lts := rest lts
iic := removeSquares(ts)
if iic case $
then
newlts := cons(iic::$,newlts)
newlts := removeDuplicates(newlts)$(List $)
sort(infRittWu?, newlts)
else
zeroSetSplit lp ==
lts : List $ := characteristicSerie(lp,initiallyReduced?,initiallyReduce)
sort(infRittWu?, removeDuplicates lts)
@
\section{License}
<<license>>=
--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.
@
<<*>>=
<<license>>
<<category TSETCAT TriangularSetCategory>>
<<domain GTSET GeneralTriangularSet>>
<<package PSETPK PolynomialSetUtilitiesPackage>>
<<domain WUTSET WuWenTsunTriangularSet>>
@
\eject
\begin{thebibliography}{99}
\bibitem{1} nothing
\end{thebibliography}
\end{document}