Search

Quantifier Elimination over the Reals (QE) is a topic in Computer Algebra concerning elimination of quantifiers from boolean formulae of polynomial constraints. QE is known to be worst case doubly exponential time complexity in the number of variables, so optimisation in this area is always of interest. Otherwise, improvements with respect to interface can make usage of QE more tractable. QE problems arise in a range of contexts, notably motion planning (such as robotics), biology, mechanics, and finance. Largely, this work discusses the implementation of a new package QuantifierElimination for the Computer Algebra software Maple. This package, developed in collaboration with Maplesoft, is an amalgamation of contemporary research on two main algorithms for QE, Virtual Term Substitution (VTS) and Cylindrical Algebraic Decomposition (CAD), but a main focus is an investigation into the efficiency & efficacy of a new "poly-algorithm" between these two algorithms. The implementation of CAD includes the first known usage of the Lazard projection for CAD in Maple, and the first known implementation & investigation of new research for equational constraint optimisations with the Lazard projection in CAD. Such equational constraint optimisations may induce mathematical "curtain" occurrences which are ordinarily cause for failure to construct a CAD with frequently desired properties. In conjunction with the first implementation of relevant algorithms from other research, methodology is delineated to ignore, or else attempt to recover from any general failure to construct or evaluate parts of the CAD for QE, including curtains. QuantifierElimination also allows for generation of full CADs without the context of QE, where users can inspect individual cells via various object methods, with the package being largely object oriented where appropriate. Generation of CADs in unquantified contexts has uses in motion planning and real algebraic geometry. Quite often the thesis focuses on finer implementation details & challenges, including with respect to the recent research on equational constraints. Other aims for the package are rich output and "incrementality", to meet the usual aims of implementations of algorithms for QE to be used within Satisfiability Modulo Theory (SMT) solving for the theory of real arithmetic (QF_NRA). Rich output includes production of "witnesses" for fully homogeneously quantified problems, which prove the equivalence of a subset of problems to their quantifier free equivalent. Extension of existing methods enables production of witnesses where the framework of the new polyalgorithm is concerned. The poly-algorithmic methods are extended to be incremental for QE as well. There are a wealth of keyword options and customizable levels of user information to print for users, as the package aims to reconcile with Maple's status as a mathematical toolbox to be easy to use with in depth information being readily available for experienced geometers. Other functions are more pedagogical to accommodate users new to problem formulations in QE and real algebraic geometry. The software is compared via benchmarking against existing QE and CAD software, especially existing packages in Maple, and investigates case studies on examples to demonstrate new methodologies and research.

As verification efforts using interactive theorem proving grow, we are in need of certified algorithms in computer algebra to tackle problems over the real numbers. This is important because uncertified procedures can drastically increase the size of the trust base and under- mine the overall confidence established by interactive theorem provers, which usually rely on a small kernel to ensure the soundness of derived results. This thesis describes an ongoing effort using the Isabelle theorem prover to certify the cylindrical algebraic decomposition (CAD) algorithm, which has been widely implemented to solve non-linear problems in various engineering and mathematical fields. Because of the sophistication of this algorithm, people are in doubt of the correctness of its implementation when deploying it to safety-critical verification projects, and such doubts motivate this thesis. In particular, this thesis proposes a library of real algebraic numbers, whose distinguishing features include a modular architecture and a sign determination algorithm requiring only rational arithmetic. With this library, an Isabelle tactic based on univariate CAD has been built in a certificate-based way: external, untrusted code delivers solutions in the form of certificates that are checked within Isabelle. To lay the foundation for the multivariate case, I have formalised various analytical results including Cauchy's residue theorem and the bivariate case of the projection theorem of CAD. During this process, I have also built a tactic to evaluate winding numbers through Cauchy indices and verified procedures to count complex roots in some domains. The formalisation effort in this thesis can be considered as the first step towards a certified computer algebra system inside a theorem prover, so that various engineering projections and mathematical calculations can be carried out in a high-confidence framework.

Since their conception by Collins in 1975, Cylindrical Algebraic Decompositions (CADs) have been used to analyse the real algebraic geometry of systems of polynomials. Applications for CAD technology range from quantifier elimination to robot motion planning. Although of great use in practice, the CAD algorithm was shown to have doubly exponential complexity with respect to the number of variables for the problem, which limits its use for large examples. Due to the high complexity of CAD, much work has been done to improve its performance. In this thesis new advances will be discussed that improve the practical efficiency of CAD for a variety of problems, with a new complexity result for one set of algorithms. A new invariance condition, truth table invariance (TTICAD), and two algorithms to construct TTICADs are given and shown to be highly efficient. The idea of restricting the output of CADs, allowing for greater efficiency, is formalised as sub-decompositions and two particular ideas are investigated in depth. Efficient selection of various formulation choices for a CAD problem are discussed, with a collection of heuristics investigated and machine learning applied to assist in choosing an optimal heuristic. The mathematical expression of a problem is shown to be of great importance, with preconditioning and reformulation investigated. Finally, these advances are collected together in a general framework for applying CAD in an efficient manner to a given problem. It is shown that their combination is not cumulative and care must be taken. To this end, a prototype software CADassistant is described to help users take advantage of the advances without knowledge of the underlying theory. The effects of the various advances are demonstrated through a guiding example originally considered by Solotareff, which describes the approximation of a cubic polynomial by a linear function. Naïvely applying CAD to the problem takes 916.1 seconds of construction (from which a solution can easily be derived), which is reduced to 20.1 seconds by combining various advances from this thesis.

The classification of finite semigroups is difficult even for small orders because of their large number. Most finite semigroups are nilpotent of nilpotency rank 3. Formulae for their number up to isomorphism, and up to isomorphism and anti-isomorphism of any order are the main results in the theoretical part of this thesis. Further studies concern the classification of nilpotent semigroups by rank, leading to a full classification for large ranks. In the computational part, a method to find and enumerate multiplication tables of semigroups and subclasses is presented. The approach combines the advantages of computer algebra and constraint satisfaction, to allow for an efficient and fast search. The problem of avoiding isomorphic and anti-isomorphic semigroups is dealt with by supporting standard methods from constraint satisfaction with structural knowledge about the semigroups under consideration. The approach is adapted to various problems, and realised using the computer algebra system GAP and the constraint solver Minion. New results include the numbers of semigroups of order 9, and of monoids and bands of order 10. Up to isomorphism and anti-isomorphism there are 52,989,400,714,478 semigroups with 9 elements, 52,991,253,973,742 monoids with 10 elements, and 7,033,090 bands with 10 elements. That constraint satisfaction can also be utilised for the analysis of algebraic objects is demonstrated by determining the automorphism groups of all semigroups with 9 elements. A classification of the semigroups of orders 1 to 8 is made available as a data library in form of the GAP package Smallsemi. Beyond the semigroups themselves a large amount of precomputed properties is contained in the library. The package as well as the code used to obtain the enumeration results are available on the attached DVD.

Buchberger’s algorithm is the classical algorithm for computing a Gröbner basis, and optimized implementations are crucial for many computer algebra systems. In this thesis we introduce a new approach to Buchberger’s algorithm that uses deep reinforcement learning agents to perform S-pair selection, a key choice in the algorithm. We first study how the difficulty of the problem depends on several random distributions of polynomial ideals, about which little is known. Next, we train a policy model using proximal policy optimization to learn S-pair selection strategies for random systems of binomial equations. In certain domains the trained model outperforms state-of-the-art selection heuristics in total number of polynomial additions performed, which provides a proof-of-concept that recent developments in machine learning have the potential to improve performance of critical algorithms in symbolic computation. Finally, we apply these techniques to Bigatti’s algorithm for computing a Hilbert series, and consider extending these results with neural network value models and tree search.

This manuscript describes a number of algorithms that can be used to quickly evaluate a polynomial over a collection of points and interpolate these evaluations back into a polynomial. Engineers define the 'Fast Fourier Transform' as a method of solving the interpolation problem where the coefficient ring used to construct the polynomials has a special multiplicative structure. Mathematicians define the 'Fast Fourier Transform' as a method of solving the evaluation problem. One purpose of the document is to provide a mathematical treatment of the topic of the 'Fast Fourier Transform' that can also be understood by someone who has an understanding of the topic from the engineering perspective. The manuscript will also introduce several new algorithms that solve the fast multipoint evaluation problem over certain finite fields and require fewer finite field operations than existing techniques. The document will also demonstrate that these new algorithms can be used to multiply polynomials with finite field coefficients with fewer operations than Schonhage's algorithm in most circumstances. A third objective of this document is to provide a mathematical perspective of several algorithms which can be used to multiply polynomials of size which is not a power of two. Several improvements to these algorithms will also be discussed. Finally, the document will describe several applications of the 'Fast Fourier Transform' algorithms presented and will introduce improvements in several of these applications. In addition to polynomial multiplication, the applications of polynomial division with remainder, the greatest common divisor, decoding of Reed-Solomon error-correcting codes, and the computation of the coefficients of a discrete Fourier Series will be addressed.

Aspects of the approximate problem of finding the factors of a polynomial in many variables are considered. The idea is that an polynomial may be the result of a computation where a reducible polynomial was expected but due to introduction of floating point coefficients or measurement errors the polynomial is irreducible. Introduction of such errors will nearly always cause polynomials to become irreducible. Thus, it is important to be able to decide whether the computed polynomial is near to a polynomial that factors (and hence should be treated as reducible). If this is the case, one would like to be able to find a closest polynomial that does indeed factor. Though this problem is computable there is no known polynomial time algorithm to find the nearest polynomial that factors. However, there are a number of methods that can be used to find a nearby polynomial that factors if the original polynomial was very close to being factorizable. This dissertation gives a method to find a lower bound on the distance to the nearest polynomial that factors. If this lower bound is quite large, one can conclude that the polynomial does not have approximate factors. As part of finding this bound, a linear condition for irreducibility of polynomials from bivariate polynomials is generalized to polynomials with many variables, and a general theory of low rank approximation to extend bounds results to many different polynomial norms is given. The singular value decomposition methods used to find the above lower bound can be used to create another method to find a nearby polynomial that factors. This method is studied, and is shown to be practical. Similar methods are also shown to work for approximate division and approximate greatest common divisor computation. The results on bounding the distance to the nearest polynomial that factors can be applied to functional decomposition of univariate polynomials. Results on functional decomposition from the 1970's together with approximate factorization results allow for a method to compute a lower bound on the distance to the nearest polynomial that has a non-trivial functional decomposition and a new algorithm to compute approximate decompositions.

A fundamental task of algebraists is to classify algebraic structures. For example, the classification of finite groups has been widely studied and has benefited from the use of computational tools. Advances in computer power have allowed researchers to attack problems never possible before. In this dissertation, algorithms for noncommutative algebra, when ab is not necessarily equal to ba, are examined with practical implementations in mind. Different encodings of associative algebras and modules are also considered. To effectively analyze these algorithms and encodings, the encoding neutral analysis framework is introduced. This framework builds on the ideas used in the arithmetic complexity framework defined by Winograd. Results in this dissertation fall into three categories: analysis of algorithms, experimental results, and novel algorithms. Known algorithms for calculating the Jacobson radical and Wedderburn decomposition of associative algebras are reviewed and analyzed. The algorithms are compared experimentally and a recommendation for algorithms to use in computer algebra systems is given based on the results. A new algorithm for constructing the Drinfel'd double of finite dimensional Hopf algebras is presented. The performance of the algorithm is analyzed and experiments are performed to demonstrate its practicality. The performance of the algorithm is elaborated upon for the special case of group algebras and shown to be very efficient. The MeatAxe algorithm for determining whether a module contains a proper submodule is reviewed. Implementation issues for the MeatAxe in an encoding neutral environment are discussed. A new algorithm for constructing endomorphism rings of modules defined over path algebras is presented. This algorithm is shown to have better performance than previously used algorithms. Finally, a linear time algorithm, to determine whether a quotient of a path algebra, with a known Gröbner basis, is finite or infinite dimensional is described. This algorithm is based on the Aho-Corasick pattern matching automata. The resulting automata is used to efficiently determine the dimension of the algebra, enumerate a basis for the algebra, and reduce elements to normal forms.