The Groebner basis of the ideal of vanishing polynomials

TL;DR

This paper constructs an explicit minimal strong Groebner basis for the ideal of vanishing polynomials over Z/m, providing a combinatorial proof, a universal basis independent of monomial order, and algorithms for computation with applications in microelectronic system verification.

Contribution

It introduces a new combinatorial construction of a universal Groebner basis for vanishing polynomials over Z/m and provides algorithms for efficient computation.

Findings

The Groebner basis is independent of monomial order.

A recursive algorithm for basis construction in Z/m[x_1,...,x_n] is provided.

The basis has applications in formal verification of microelectronic systems.

Abstract

We construct an explicit minimal strong Groebner basis of the ideal of vanishing polynomials in the polynomial ring over Z/m for m>=2. The proof is done in a purely combinatorial way. It is a remarkable fact that the constructed Groebner basis is independent of the monomial order and that the set of leading terms of the constructed Groebner basis is unique, up to multiplication by units. We also present a fast algorithm to compute reduced normal forms, and furthermore, we give a recursive algorithm for building a Groebner basis in Z/m[x_1,x_2,...,x_n] along the prime factorization of m. The obtained results are not only of mathematical interest but have immediate applications in formal verification of data paths for microelectronic systems-on-chip.