Applied and Computational Algebraic Geometry

Proposed outline of the dissertation: This proposal is based on applied and computational algebraic geometry. Algebraic geometry is the study of varieties which are defined as the zero sets of systems of polynomial equations. We will focus on the polynomial systems arising from specific problems in theoretical computer science. In particular, we will develop theory and algorithms for our applications based on the following branches of algebraic geometry:[T1] Numerical Algebraic Geometry: Numerical Algebraic Geometry [SW05], as the name suggests, is the amalgamation of numerical techniques and algebraic geometry. The main objective of this theory is to develop new tools for numerically solving the system of polynomial equations. The two main techniques used in the area are homotopy continuation and eigenvalue methods. The former uses suitable homotopies to deform the given system of polynomial equations to a system that can be easily solved. Then tracking all the solutions of the deformed system to the initial system along with the chosen homotopy. This method helps find all the solutions of the system contrary to the other numerical solvers. The eigenvalue method converts the problem of solving the system of polynomial equations to solving the eigenvalue problem for corresponding Macaulay matrices [Te20]. In order to compute the Macaulay matrices, this method relies on symbolic computations. To solve the eigenvalue problem, this method relies on algorithms from computational linear algebra. Both of the methods provide numerical solutions to the system of polynomial equations. In order to use these solutions in applications, we need mathematical certificates for them, for this, we use Smale's theory [HS10] and Krawczyk's method. In recent works [Br20], [Te20], novel techniques from polyhedral geometry and toric geometry have been used to develop numerical algorithms for solving sparse polynomial systems. [T2] Real Algebraic Geometry: Real algebraic geometry [BCR13] is the branch of algebraic geometry that deals with finding real solutions to the polynomial equations. The main concepts of this area include quantifier elimination, decomposition theorems for semi-algebraic sets, the existence theory of reals, Positivstellensatz etc. In the applications, we are particularly interested in finding the real solutions for the system of polynomial equations. The classical theorems from this area (for example Putinar's Positivstellensatz) are already in use. But the full strength of this theory has not been fully utilized in the applications we are interested in. In particular, the existence theory of reals and decomposition theorems can be very useful for developing sufficient conditions for the existence of real solutions for the polynomial systems under consideration. There also have been recent advances in finding real numerical solutions to the polynomial equations using techniques from tropical geometry and polyhedral geometry. Moreover, for certain sparse polynomial systems, some new algorithms for counting real solutions have also been proposed very recently which can be helpful for the complexity analysis of our problems. [T3] Symbolic Computations: Symbolic computations deal with solving systems of polynomial equations using techniques from the theory of Gröbner basis and elimination theory [CLO13]. These methods differ from numerical algebraic geometry significantly as here the theory depends on algebraic manipulations of equations rather than relying on numerical operations. But both the methods complement each other as for certain numerical techniques like eigenvalue methods [T1], one of the crucial steps involves computation of Gröbner basis. Although the complexity of computation of Gröbner basis for a general polynomial system is doubly exponential in the size of the problem, this method is still useful for our application. As the systems that we are interested in have nice combinatorial structures (sparsity, low treewidth etc), the Gröbner basis computations for such systems are tractable. In particular, the main idea is to prove that our systems have a certain form of Gröbner basis, which in turn can help to reduce the time complexity for computing the Macaulay matrices required for the eigenvalue methods. For sparse polynomial systems, there have been recent developments for the efficient computations of Gröbner basis using properties of the graphs associated with the polynomial systems in considerations [Pa14]. There are also new results in the complexity analysis for the computation of Gröbner basis for sparse systems [Be19]. These new results can be of immense use for our proposed problems.We will use the above-mentioned branches of algebraic geometry to find the real roots of the system of polynomial equations arising in theoretical computer science. In particular in program verification, there have been recent advances and new connections from algebraic geometry [Go20]. We will focus on the three main problems from program verification: [P1] Reachability analysis, [P2] Invariant generation and [P3] Termination analysis. References:[BCR13] Bochnak J, Coste M, Roy MF. Real algebraic geometry. Springer Science & Business Media; 2013. [Be19] Bender, M. "Algorithms for sparse polynomial systems: Gröbner bases and resultants." PhD diss., Sorbonne université, 2019. [Br20] Brysiewicz T. Newton polytopes and numerical algebraic geometry. PhD diss., Texas A&M University, 2020[BRT20] Breiding P, Rose K, Timme S. Certifying zeros of polynomial systems using interval arithmetic. arXiv preprint arXiv:2011.05000. 2020 Nov 10.[CLO13] Cox D, Little J, OShea D. Ideals, varieties, and algorithms: an introduction to computational algebraic geometry and commutative algebra. Springer Science & Business Media; 2013. [Go20] Goharshady A. Parameterized and algebro-geometric advances in static program analysis PhD diss., Institute of Science and Technology Austria, 2020.[HS10] Hauenstein JD, Sottile F. alphaCertified: certifying solutions to polynomial systems. arXiv preprint arXiv:1011.1091. 2010. [Pa14] Pardo, D. "Exploiting chordal structure in systems of polynomial equations." PhD diss. Massachusetts Institute of Technology, 2014. [SW05] Sommese AJ, Wampler CW. The Numerical solution of systems of polynomials arising in engineering and science. World Scientific; 2005. [Te20] Simon Telen, Solving systems of polynomial equations, PhD diss., KU Leuven, 2020.[VC93] Verschelde J, Cools R. Symbolic homotopy construction. Applicable Algebra in Engineering, Communication and Computing. 1993 Sep;4(3):169-83.[VC94] Verschelde J, Cools R. Symmetric homotopy construction. Journal of Computational and Applied Mathematics. 1994 May 20;50(1-3):575-92.[VVC94] Verschelde J, Verlinden P, Cools R. Homotopies exploiting Newton polytopes for solving sparse polynomial systems. SIAM Journal on Numerical Analysis. 1994 Jun;31(3):915-30.

Keywords:Algebraic Geometry, Theoretical Computer Science, Program Verification

Disciplines:Computer science, Computational logic and formal languages, Algebraic geometry

Project type:PhD project