Re: [Axiom-developer] PFE, Complex and INT

[Waldek Hebisch]

Martin Rubey wrote:
> Dear all,
> 
> regarding Issue #352 and possibly #351, I experimented a little.  The starting
> point is the documentation of PFECAT, in catdef.spad:
> 
> )abbrev category PFECAT PolynomialFactorizationExplicit
> ++ Author: James Davenport
> ++ Description:
> ++ This is the category of domains that know "enough" about
> ++ themselves in order to factor univariate polynomials over themselves.
> ++ This will be used in future releases for supporting factorization
> ++ over finitely generated coefficient fields, it is not yet available
> ++ in the current release of axiom.
> 
> Many domain constructors like, for example, Complex export PFECAT, with the
> condition that their arguments has PFECAT and possibly satisfies some other
> conditions, too.  However, at the moment, not even Integer exports PFECAT, so,
> in effect, it is not yet used.  Curiously, it implements most of the 
> operations
> needed, so I'd think we could simply make Integer or rather 
> IntegerNumberSystem
> export PFECAT.
>

I think that this requres deeper investigation.  Namely, gcd and
factorization is currently provided by different packages using somewhat
different method.  We have to check which method is better and turn it
on.  Also, it looks that in the meantime better algorithms appeared,
so we may prefer to implement them and forget abot old ones.

> A related category is UniqueFactorizationDomain, also defined in catdef:
> 
> )abbrev category UFD UniqueFactorizationDomain
> ++ A constructive unique factorization domain, i.e. where
> ++ we can constructively factor members into a product of
> ++ a finite number of irreducible elements.
> 
> What I really wanted is to be able to say
> 
> (5) -> 2::FR COMPLEX INT
> 
>                      2
>    (5)  - %i (1 + %i)
>                                                Type: Factored Complex Integer
> 
> So, I modified COMPCAT as follows, i.e., since I don't know about square free
> factorization, I just used factor.
> 
> I'd be very interested in comments.
> 
> Martin
> 
> diff -c /home/martin/lib/axiom/target/i686-pc-linux/src/algebra/gaussian.spad
> /home/martin/gaussian.spad
> *** /home/martin/lib/axiom/target/i686-pc-linux/src/algebra/gaussian.spad
> 2007-05-02 20:39:25.000000000 +0200
> --- /home/martin/gaussian.spad  2007-05-03 09:30:12.000000000 +0200
> ***************
> *** 91,96 ****
> --- 91,97 ----
>            ++ "failed" if x is not a rational number.
>        if R has PolynomialFactorizationExplicit and R has EuclideanDomain then
>           PolynomialFactorizationExplicit
> +      if R has UniqueFactorizationDomain then UniqueFactorizationDomain

                  ^^^^^^^^^^^^^^^^^^^^^^^^^

That looks like overgeneralization.  First, Complex R may have zero
divisors (so we will hit bug 351).  Even if Complex R is an integral
domain, it is not clear if it has unique factorization (do you know
about any theorem asserting this?).  Finally, even if Complex R
has unique factorization AFAICS we do not have any factorization
algorithm working in Complex R.  So I would just write:

        if R is Integer then UniqueFactorizationDomain
  
which seem to agree with implementation.

>    add
>          import MatrixCategoryFunctions2(%, Vector %, Vector %, Matrix %,
>                                          R, Vector R, Vector R, Matrix R)
> ***************
> *** 116,121 ****
> --- 117,130 ----
>                --!gcdPolynomial(pp,qq) == modularGcd(pp,qq)$TT
>                solveLinearPolynomialEquation(lp:List Sup,p:Sup) ==
>                  
> solveLinearPolynomialEquation(lp,p)$ComplexIntegerSolveLinearPolynomialEquation(R,%)
> + 
> +              squareFree x == 
> +                y: Complex Integer := complex(convert(real x)@Integer, 
> +                                              convert(imag x)@Integer)
> +                z: Factored Complex Integer :=
> factor(y)$GaussianFactorizationPackage
> +                mf: Complex Integer -> % := complex(real(#1)::R, imag(#1)::R)
> +                map(mf #1, z)$FactoredFunctions2(Complex Integer, %)
> + 
>             normPolynomial: Sup -> SupR
>             normPolynomial pp ==
>                 map(retract(address@hidden)::R,pp * map(conjugate,pp))
> 
> 


-- 
                              Waldek Hebisch
address@hidden