Search

In this paper, we consider a constructive proof of the termination of the normal form (NF) algorithm for multivariate polynomials, as well as the related concept of admissible ordering < on monomials. In classical mathematics, the well-quasiorder property of relation < is derived from Dickson's lemma, and this is sufficient to justify the termination of the NF algorithm. In provable programming based on constructive type theory (Coq and Agda), a somewhat stronger condition (in constructive mathematics) of the well-foundedness of the ordering (in its constructive version) is required. We propose a constructive proof of this theorem (T) for < , which is based on a known method that we refer to here as the "pattern method." This theorem on the well-foundedness of an arbitrary admissible ordering is also important in itself, independently of the NF algorithm. We are not aware of any other works on constructive proof of this theorem. However, it turns out that it follows, not very difficultly, from the results achieved by other researchers in 2003. We program this proof in the Agda language in the form of our library AdmissiblePPO-wellFounded of provable computational algebra programs. This development also uses the theorem to prove termination of the NF algorithm for polynomials. Thus, the library also contains a set of provable programs for polynomial algebra, which is significantly larger than that needed to prove Theorem T. [ABSTRACT FROM AUTHOR]

In this paper, we propose a method for computing and visualizing the amoeba of a Laurent polynomial in several complex variables, which is applicable in arbitrary dimension. The algorithms developed based on this method are implemented as a free web service (http://amoebas.ru), which enables interactive computation of amoebas for polynomials in two variables, as well as provides a set of precomputed amoebas and their cross-sections in higher dimensions. The correctness and running time of the proposed algorithms are tested against a set of optimal polynomials in two, three, and four variables, which are generated using Mathematica computer algebra system. The developed program code makes it possible, in particular, to generate optimal hypergeometric polynomials in an arbitrary number of variables supported in an arbitrary zonotope given by a set of generating vectors. [ABSTRACT FROM AUTHOR]

The set of polynomial mappings of n-dimensional complex space into itself the Jacobian matrix of which has a constant nonzero determinant is known to be very vast in any dimension that exceeds one. The well-known Jacobian conjecture states that any such mapping is polynomially invertible. Even though the computation of the determinant of the Jacobian matrix is very well supported in modern computer algebra systems, the algorithmic inversion of a polynomial mapping is still a problem of considerable computational complexity. In this paper, we present a Mathematica package JC that can be used for construction and inversion of polynomial mappings and more general analytic mappings with the unit determinant of the Jacobian matrix. The package includes functions that allow one to algorithmically construct these mappings for a given dimension of the space of variables and a given degree of mapping components. The package, together with a library of datasets for testing it and results of computational experiments, is available for free public use at https://www.researchgate.net/publication/358409332_JC_Package_and_Datasets. [ABSTRACT FROM AUTHOR]

In this paper, we propose an algorithm for solving the Cauchy problem for a two-dimensional difference equation with constant coefficients at a point, based on its coefficients and the initial data for the Cauchy problem, which are defined in a "strip." For this purpose, computer algebra methods are employed. To automate the process of computing the solution, the algorithm is implemented in MATLAB, with the input data being the matrix of coefficients of the two-dimensional polynomial difference equation, the coordinates of the initial data matrix (which defines the structure of the difference equation), and the coordinates of the point that determines the dimension of the initial data matrix. The output of the algorithm is a solution of the Cauchy problem (with the initial data defined in a "strip") for the two-dimensional difference equation, which is a function value at the desired point. [ABSTRACT FROM AUTHOR]

The design of a certified program for the Karatsuba method to multiply univariate polynomials is described. A machine-checked proof of the equivalence between the simplest method for polynomial multiplication and the Karatsuba method is implemented. This is a small part of the DoCon-A library of certified computer algebra programs designed by the author of this paper. The equivalence is proved for an arbitrary commutative ring of coefficients, and our library includes a certified generation of commutative ring structure for domain R[x] of polynomials over any commutative ring R. The programs in the DoCon-A system include definitions of the corresponding mathematical concepts and proofs for the main properties of the methods implemented. These proofs are checked by the compiler. The purely functional programming language Agda, which supports dependent types, is used. General principles of designing certified programs in Agda are considered. A comparison with another approach to certified programming of the Karatsuba method is carried out. [ABSTRACT FROM AUTHOR]