/usr/share/axiom-20170501/src/algebra/LEADCDET.spad is in axiom-source 20170501-3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 | )abbrev package LEADCDET LeadingCoefDetermination
++ Author : P.Gianni, May 1990
++ Description:
++ Package for leading coefficient determination in the lifting step.
++ Package working for every R euclidean with property "F".
LeadingCoefDetermination(OV,E,Z,P) : SIG == CODE where
OV : OrderedSet
E : OrderedAbelianMonoidSup
Z : EuclideanDomain
BP ==> SparseUnivariatePolynomial Z
P : PolynomialCategory(Z,E,OV)
NNI ==> NonNegativeInteger
LeadFact ==> Record(polfac:List(P),correct:Z,corrfact:List(BP))
ParFact ==> Record(irr:P,pow:Integer)
FinalFact ==> Record(contp:Z,factors:List(ParFact))
SIG ==> with
polCase : (Z,NNI,List(Z)) -> Boolean
++ polCase(contprod, numFacts, evallcs), where contprod is the
++ product of the content of the leading coefficient of
++ the polynomial to be factored with the content of the
++ evaluated polynomial, numFacts is the number of factors
++ of the leadingCoefficient, and evallcs is the list of
++ the evaluated factors of the leadingCoefficient, returns
++ true if the factors of the leading Coefficient can be
++ distributed with this valuation.
distFact : (Z,List(BP),FinalFact,List(Z),List(OV),List(Z)) ->
Union(LeadFact,"failed")
++ distFact(contm,unilist,plead,vl,lvar,lval), where contm is
++ the content of the evaluated polynomial, unilist is the list
++ of factors of the evaluated polynomial, plead is the complete
++ factorization of the leading coefficient, vl is the list
++ of factors of the leading coefficient evaluated, lvar is the
++ list of variables, lval is the list of values, returns a record
++ giving the list of leading coefficients to impose on the univariate
++ factors,
CODE ==> add
distribute: (Z,List(BP),List(P),List(Z),List(OV),List(Z)) -> LeadFact
checkpow : (Z,Z) -> NNI
polCase(d:Z,nk:NNI,lval:List(Z)):Boolean ==
-- d is the product of the content lc m (case polynomial)
-- and the cont of the polynomial evaluated
q:Z
distlist:List(Z) := [d]
for i in 1..nk repeat
q := unitNormal(lval.i).canonical
for j in 0..(i-1)::NNI repeat
y := distlist.((i-j)::NNI)
while y^=1 repeat
y := gcd(y,q)
q := q quo y
if q=1 then return false
distlist := append(distlist,[q])
true
checkpow(a:Z,b:Z) : NonNegativeInteger ==
qt: Union(Z,"failed")
for i in 0.. repeat
qt:= b exquo a
if qt case "failed" then return i
b:=qt::Z
distribute(contm:Z,unilist:List(BP),pl:List(P),vl:List(Z),
lvar:List(OV),lval:List(Z)): LeadFact ==
d,lcp : Z
nf:NNI:=#unilist
for i in 1..nf repeat
lcp := leadingCoefficient (unilist.i)
d:= gcd(lcp,vl.i)
pl.i := (lcp quo d)*pl.i
d := vl.i quo d
unilist.i := d*unilist.i
contm := contm quo d
if contm ^=1 then for i in 1..nf repeat pl.i := contm*pl.i
[pl,contm,unilist]$LeadFact
distFact(contm:Z,unilist:List(BP),plead:FinalFact,
vl:List(Z),lvar:List(OV),lval:List(Z)):Union(LeadFact,"failed") ==
h:NonNegativeInteger
c,d : Z
lpol:List(P):=[]
lexp:List(Integer):=[]
nf:NNI := #unilist
vl := reverse vl --lpol and vl reversed so test from right to left
for fpl in plead.factors repeat
lpol:=[fpl.irr,:lpol]
lexp:=[fpl.pow,:lexp]
vlp:List(Z):= [1$Z for i in 1..nf]
aux : List(P) := [1$P for i in 1..nf]
for i in 1..nf repeat
c := contm*leadingCoefficient unilist.i
c=1 or c=-1 => "next i"
for k in 1..(# lpol) repeat
lexp.k=0 => "next factor"
h:= checkpow(vl.k,c)
if h ^=0 then
if h>lexp.k then return "failed"
lexp.k:=lexp.k-h
aux.i := aux.i*(lpol.k ** h)
d:= vl.k**h
vlp.i:= vlp.i*d
c:= c quo d
if contm=1 then vlp.i:=c
for k in 1..(# lpol) repeat if lexp.k ^= 0 then return "failed"
contm =1 => [[vlp.i*aux.i for i in 1..nf],1,unilist]$LeadFact
distribute(contm,unilist,aux,vlp,lvar,lval)
|