CoCoALib is a C++ software library o ering operations on polynomials, ideals of polynomials, and related objects. The principal developers of CoCoALib are members of the SC2 project. We give an overview of the latest developments of the library, especially those relating to the project SC2. The CoCoA software suite includes also the programmable, interactive system CoCoA-5. Most of the operations in CoCoALib are also accessible via CoCoA-5. The programmability of CoCoA-5 together with its interactivity help in fast prototyping and testing conjectures.
We brie y recall what is described in [
The CoCoA software has a modular design: its \mathematical expertise"
resides in the C++ software library [
We give an overview of the latest developments of the library and of the
system (for the summer 2018 release). There are some new aspects of particular
interest to the project SC2. One feature is an implementation in CoCoALib of
a new e cient algorithm for computing the minimal polynomial ([
Another feature of interest to SC2 is the prototype interface for communication between CoCoALib and MathSAT (Section 4).
Improving usability of CoCoA for SC2 2.1
A exible \timeout" mechanism has been added to CoCoALib. It has a simple user interface, and can be used with several function calls to CoCoALib. The exact behaviour of the timeout depends on the speci c function: e.g. some functions either return the correct and complete answer within the requested time limit, or throw an exception to say that the result could not be computed quickly enough; other functions, which compute approximations to some exact value, return the best approximation which could be obtained within the given time limit.
One purpose of the timeout mechanism is to allow a \speculative" approach to solving: i.e. a potentially costly algorithm may be called with a time limit, and in fortunate cases the answer is returned, but in the worst case of a vain attempt only the speci ed amount of time has been consumed. For example, one may attempt to nd all real solutions to a 0-dimensional polynomial system (internally this computes a Grobner basis); if successful then the result is valuable, but in some unlucky cases the Grobner basis computation may be unreasonably slow, so we use the timeout mechanism to avoid the \black hole", and must then proceed without knowing what the solutions to the system are | this technique has already been successfully employed inside CoCoALib itself: for example, in testing primality of zero-dimensional ideals (which is called during the factorization of polynomials over algebraic extensions, Section 3.1). 2.2
We have implemented a prototype for GBasisRealSolve which removes some non-real components during Grobner basis computation. The critical internal operation is a quick function for \approximating" the real radical of a polynomial. In this context \approximating" means applying quick heuristics for determining whether a polynomial admits any real solutions; the heuristic may respond true, false or uncertain. Factors which surely have no real roots are removed, whereas those which do have or may have real roots are retained.
The heuristic employs two other ideas mentioned here: real root counting (via Sturm Sequences), and timeout. Even though this heuristic approach is, mathematically speaking, not a satisfactory solution to the general problem, the function GBasisRealSolve seems to work well on examples arising from SMT computations (see Section 4).
A mathematically complete solution could go via Cylindrical Algebraic Decomposition. Towards this end, we have developed in CoCoA factorisation of polynomials over algebraic extensions, and evaluation of polynomials over real intervals (Section 3).
CoCoALib has had for some time the capability to compute with polynomials whose coe cients lie in an algebraic extension. The extension may be speci ed by any maximal ideal, and does not require that a primitive element be furnished. One important step for CAD is the computation of isolating intervals for the real roots of a polynomial with coe cients in a (real) algebraic extension. CoCoALib is not yet able to do this last operation, but we are developing the various components necessary to reach this goal. 3.1
In this section we describe an e ective method for factorizing univariate
polynomials over nite eld extensions. This method, based on the computation of
primary decompositions of zero-dimensional ideals, is described in the PhD
thesis [
Example 1. Let L = F2[a]=M = F8 be the base eld, where M = ha3 + a + 1i is a maximal ideal, and consider f (x) = x5 + x + 1 2 L[x], the polynomial to be factorized.
This is the algorithm implemented in CoCoALib. Let S = K[a1; : : : ; am] be
a polynomial ring over a perfect eld K, let M be a maximal ideal in S, let
L = S=M, and let f (x) 2 L[x] be a univariate polynomial. The factorization of
f (x) is obtained by computing the primary decomposition of the ideal M+hf (x)i
in the polynomial ring K[a1; : : : ; am; x]; for the proof of correctness see [
RemainingFactor := (1) , factors := [x +( a ^2+ a +1) , multiplicities := [1 , 1, x +( a ^2+1) , 1, 1] x +( a +1) , x ^2+ x +(1)] , 1 create the ring P = K[a1; : : : ; am; x] let : S ! P , de ned by ai 7! ai let : P ! L[x], de ned by ai 7! ai and x 7! x 2 let MP = h (g) j g 2 gens(M)i P let fP 2 1(f ), a representative of f in P let J = MP + hfP i ideal in P 3 compute the primary decomposition of J ! Q1 \ \ Qs 4 compute gi, the monic generator of (Qi) in L[x] | note: L[x] is PID 5 compute hi = rad(gi) and let mi = ddeegg((hgii)) Output LC(f ) Qs
j=1 himi, the factorization of f in L[x] Example 2. The internal computation for Example 1, following the algorithm above, actually performs these steps: and these are indeed the (square-free) factors of f .
Next we see a call to factor in an algebraic extension which is given by a non-principal, maximal ideal, L = Q[a; b]=ha2 3; b2 ab 4i, /* */ use S ::= QQ [a , b ]; /* */ M := ideal (a ^2 -3 , b^2 -a*b -4); /* */ IsMaximal (M ); // check that M is a maximal ideal true /* */ L := S/M; /* */ use Lx ::= L[x ]; /* */ factor (x ^6 +( b ^2)* x ^4 +( -55* b ^2+80)* x ^2 +(315* b ^2 -528)); record [
RemainingFactor := (1) ,
factors := [x ^2 +(3* b ^2) , x +( -b), x +( b)] ,
multiplicities := [
We have implemented a function for computing a primitive Sturm sequence of a given (univariate) polynomial with rational coe cients. Sturm sequences enable one to compute easily the number of real roots a given (univariate) polynomial has in a given real interval; in particular, they can be used to tell whether a given (univariate) polynomial has any real roots. CoCoA also o ers a function to count the number of real roots: /* */ W := product ([x -k | k in 1..20]); // Wilkinson 's polynomial /* */ W2 := W + (1/7402570310)* x ^19; /* */ NumRealRoots ( W2 ); 18 /* */ W3 := W + (1/7402570311)* x ^19; /* */ NumRealRoots ( W3 ); 20
The interactive CoCoA-5 system o ers a suite of interpreted functions for computing tight isolating intervals for real roots. This code is not yet available in CoCoALib, but we are planning to port it (though this lengthy task will likely be completed after the end of this rst SC2 project). While a list of isolating intervals gives more explicit information than a Sturm sequence, it is also generally more costly to compute. 3.3
CoCoA now also o ers a collection of functions for obtaining a good upper bound for the absolute value of every complex root of a given (univariate) polynomial. The main function strikes an automatic balance between speed of computation and tightness of the computed bound; an optional second argument lets the caller choose a di erent balance. A root bound gives less information than a Sturm sequence but can be computed faster, and may sometimes give enough information to decide unsolvability. A root bound can be computed for any nonconstant (univariate) polynomial, but gives no indication whether any of the roots is real. /* */ H := HermitePoly (50 , x ); // largest real root is 9.18 /* */ RootBound (f ); // fair compromise for speed / accuracy 295/32 // 9.22 /* */ RootBound (f ,0); // fastest , 0 iterations 237/8 // 29.625 ( quite loose ) /* */ RootBound (f ,1); // still fast , 1 iteration 115/8 // 14.375 ( better than 0 iters ) 3.4 Interval arithmetic, and range of a polynomial We have recently added to CoCoALib a prototype suite of functions for \interval arithmetic" on closed real intervals with rational endpoints. The suite includes a more advanced function for evaluating a given (univariate) polynomial with rational coe cients (or interval coe cients) over a given interval. The result is another interval, comprising e ectively a lower bound for the minimum and an upper bound for the maximum for the polynomial over the given interval. In general, the result contains strictly the true interval of reachable values: in fact, the true range interval may have irrational end points; e.g. if f = x3 x then its range over the interval [ 1; 1] has both end points being irrational, namely [ 2p3 p
9 ; 2 9 3 ]. Consequently, when using intervals with rational end points only an approximation to the correct answer can be produced.
We are still studying the compromise between speed of computation and tightness of the resulting interval. Naturally, it can help answer some questions of solvability where both the variable and the value of the polynomial are limited to nite intervals. One future aim is to use this suite to allow isolation of real roots of polynomials whose coe cients are real algebraic numbers (each represented as a small isolating interval together with the minimal polynomial).
As an example we can compute the range of values of the 10-th Chebyshev polynomial evaluated on the interval I = [ 1; 1]. From the theory we know that the true answer is the interval [ 1; 1]; our current prototype implementation produces a fair approximation, being the wider interval from 1:15 to 1:12. The Chebyshev polynomials are an interesting test case because they have many local maximums and minimums, which become global maximums and minimums when we restrict the domain to the interval I. We do not give an explicit example in CoCoA-5 since the user interface is not yet settled. 4
Interface MatSAT$CoCoA-5
In [
The construction in CoCoALib of polynomial rings with user de ned orderings (such as elimination orderings) has been reorganized so that it makes fewer repeated checks on the admissibility of the term-ordering. This is not a problem in the usual context of Commutative Algebra, where the cost of the computation of a Grobner basis exceeds by far the time spent in the preliminary construction of the polynomial ring. But the rst collection of examples arising from MathSAT computations, highlighted that this is indeed an issue when we deal with many indeterminates and relatively simple Grobner basis computations.
The communication between CoCoALib and MathSAT has been improved, so the overhead for the data conversions is now negligible.
Indeed, thanks to this collaboration both CoCoALib and MathSAT speeded up their code in some parts which had never been highlighted during their respectively normal usage.
Using this new interface, we have built a rst collection of examples of systems of polynomial equalities and inequalities generated from MathSAT computations, for experimenting with CoCoA. Since CoCoA natively handles only equalities, we applied an input manipulation which converts MathSAT inequalities into CoCoA equalities by adding squares of slack variables, with further increase of the number of indeterminates. Then we tested the function GBasisRealSolve (Section 2.2), using a speci c weighted graduation and term-ordering, and observed it works very e ectively on these examples, detecting UNSAT in remarkably few steps.
We wrote a prototype CoCoA-5 package using MSatLinSolve, the rst
MathSAT function in CoCoA-5 (see [