|
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. 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]. |
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".
[2019-04-18]: Added material about polynomials whose power-products are represented themselves
by polynomial mappings. |
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, Well_Quasi_Orders |
Used by: |
Deep_Learning, Groebner_Bases, Lambda_Free_KBOs, Symmetric_Polynomials |
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.
|
|