Initial population.

1 files changed, 167 insertions, 0 deletions

diff --git a/src/algebra/leadcdet.spad.pamphlet b/src/algebra/leadcdet.spad.pamphlet
new file mode 100644
index 00000000..73635266
--- /dev/null
+++ b/src/algebra/leadcdet.spad.pamphlet
@@ -0,0 +1,167 @@
+\documentclass{article}
+\usepackage{axiom}
+\begin{document}
+\title{\$SPAD/src/algebra leadcdet.spad}
+\author{Patrizia Gianni}
+\maketitle
+\begin{abstract}
+\end{abstract}
+\eject
+\tableofcontents
+\eject
+\section{package LEADCDET LeadingCoefDetermination}
+<<package LEADCDET LeadingCoefDetermination>>=
+)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) : C == T
+ 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))
+ 
+  C == 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, 
+ 
+  T == 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)
+
+@
+\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>>
+
+<<package LEADCDET LeadingCoefDetermination>>
+@
+\eject
+\begin{thebibliography}{99}
+\bibitem{1} nothing
+\end{thebibliography}
+\end{document}