### Abstract

We define multivariate polynomials over arbitrary (ordered) semirings in combination with (executable) operations like addition, multiplication, and substitution. We also define (weak) monotonicity of polynomials and comparison of polynomials where we provide standard estimations like absolute positiveness or the more recent approach of Neurauter, Zankl, and Middeldorp. Moreover, it is proven that strongly normalizing (monotone) orders can be lifted to strongly normalizing (monotone) orders over polynomials. Our formalization was performed as part of the IsaFoR/CeTA-system which contains several termination techniques. The provided theories have been essential to formalize polynomial interpretations.

This formalization also contains an abstract representation as coefficient functions with finite support and a type of power-products. If this type is ordered by a linear (term) ordering, various additional notions, such as leading power-product, leading coefficient etc., are introduced as well. Furthermore, a lot of generic properties of, and functions on, multivariate polynomials are formalized, including the substitution and evaluation homomorphisms, embeddings of polynomial rings into larger rings (i.e. with one additional indeterminate), homogenization and dehomogenization of polynomials, and the canonical isomorphism between R[X,Y] and R[X][Y].

### License

GNU Lesser General Public License (LGPL)

### History

April 18, 2019
  Added material about polynomials whose power-products are represented themselves by polynomial mappings.
January 23, 2018
  Added authors Haftmann, Lochbihler after incorporating their formalization of multivariate polynomials based on Polynomial mappings. Moved material from Bentkamp's entry "Deep Learning".
October 28, 2016
  Added abstract representation of polynomials and authors Maletzky/Immler.
September 17, 2010
  Moved theories on arbitrary (ordered) semirings to Abstract Rewriting.

### Topics

- Mathematics/Analysis
- Mathematics/Algebra
- Computer science/Algorithms/Mathematical

### Session Polynomials

- Utils
- MPoly_Type
- More_MPoly_Type
- Power_Products
- More_Modules
- MPoly_Type_Class
- MPoly_Type_Class_Ordered
- Poly_Mapping_Finite_Map
- MPoly_Type_Class_FMap
- PP_Type
- OAlist
- OAlist_Poly_Mapping
- Term_Order
- MPoly_Type_Class_OAlist
- Quasi_PM_Power_Products
- MPoly_PM
- MPoly_Type_Univariate
- Polynomials
- Show_Polynomials
- NZM

### Depends on

- Abstract Rewriting
- Executable Matrix Operations on Matrices of Arbitrary Dimensions
- Haskell’s Show Class in Isabelle/HOL
- Well-Quasi-Orders

### Used by

- Undecidability Results on Orienting Single Rewrite Rules
- The Sumcheck Protocol
- Factorization of Polynomials with Algebraic Coefficients
- Verified Quadratic Virtual Substitution for Real Arithmetic
- Practical Algebraic Calculus Checker
- Symmetric Polynomials
- Formalization of Knuth–Bendix Orders for Lambda-Free Higher-Order Terms
- Expressiveness of Deep Learning
- Gröbner Bases Theory

## Cite

×

Polynomials-AFP

    @article{Polynomials-AFP,
      author  = {Christian Sternagel and René Thiemann and Alexander Maletzky and Fabian Immler and Florian Haftmann and Andreas Lochbihler and Alexander Bentkamp},
      title   = {Executable Multivariate Polynomials},
      journal = {Archive of Formal Proofs},
      month   = {August},
      year    = {2010},
      note    = {\url{https://isa-afp.org/entries/Polynomials.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jan 14, 2020 : Isabelle2019
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Feb 16, 2013 : Isabelle2013
- May 24, 2012 : Isabelle2012
- Oct 11, 2011 : Isabelle2011-1
- Feb 11, 2011 : Isabelle2011
- Aug 11, 2010 : Isabelle2009-2