An Effective Framework for Constructing Exponent Lattice Basis of Nonzero Algebraic Numbers

TL;DR

This paper introduces a new, inductively constructible basis for the exponent lattice of algebraic numbers, enabling more efficient computation especially for large-degree fields, with applications in program verification.

Contribution

It proposes a novel framework for constructing exponent lattice bases using an inductive approach and linear Diophantine equations, improving efficiency over existing methods.

Findings

Efficient basis construction for large algebraic number fields

Successful implementation in Mathematica demonstrating effectiveness

Application to program verification for invariant detection

Abstract

Computing a basis for the exponent lattice of algebraic numbers is a basic problem in the field of computational number theory with applications to many other areas. The main cost of a well-known algorithm \cite{ge1993algorithms,kauers2005algorithms} solving the problem is on computing the primitive element of the extended field generated by the given algebraic numbers. When the extended field is of large degree, the problem seems intractable by the tool implementing the algorithm. In this paper, a special kind of exponent lattice basis is introduced. An important feature of the basis is that it can be inductively constructed, which allows us to deal with the given algebraic numbers one by one when computing the basis. Based on this, an effective framework for constructing exponent lattice basis is proposed. Through computing a so-called pre-basis first and then solving some linear Diophantine equations, the basis can be efficiently constructed. A new certificate for multiplicative independence and some techniques for decreasing degrees of algebraic numbers are provided to speed up the computation. The new algorithm has been implemented with Mathematica and its effectiveness is verified by testing various examples. Moreover, the algorithm is applied to program verification for finding invariants of linear loops.