Home
About
Submission
Updating Entries
Using Entries
Search
Statistics
Index
Download

 

 

 

Executable Multivariate Polynomials

 

Title: Executable Multivariate Polynomials
Authors: Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com), René Thiemann, Alexander Maletzky, Fabian Immler, Florian Haftmann, Andreas Lochbihler and Alexander Bentkamp (bentkamp /at/ gmail /dot/ com)
Submission date: 2010-08-10
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.
Change history: [2010-09-17]: Moved theories on arbitrary (ordered) semirings to Abstract Rewriting.
[2016-10-28]: Added abstract representation of polynomials and authors Maletzky/Immler.
[2018-01-23]: Added authors Haftmann, Lochbihler after incorporating their formalization of multivariate polynomials based on Polynomial mappings. Moved material from Bentkamp's entry "Deep Learning".
BibTeX: 
@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   = aug,
  year    = 2010,
  note    = {\url{http://isa-afp.org/entries/Polynomials.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: GNU Lesser General Public License (LGPL)
Depends on: Abstract-Rewriting, Matrix, Show
Used by: Deep_Learning, Groebner_Bases, Lambda_Free_KBOs
Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Proof outline
Proof document
Browse theories
Download this entry
Older releases: