Presburger Arithmetic, Rational Generating Functions, and Quasi-Polynomials

A Presburger formula is a Boolean formula with variables in N that can be written using addition, comparison (<=, =, etc.), Boolean operations (and, or, not), and quantifiers (for all and there exists). We characterize sets that can be defined by a Presburger formula as exactly the sets whose characteristic functions can be represented by rational generating functions; a geometric characterization of such sets is also given. In addition, if p = (p(1),...,p(n)) are a subset of the free variables in a Presburger formula, we can define a counting function g(p) to be the number of solutions to the formula, for a given p. We show that every counting function obtained in this way may be represented as, equivalently, either a piecewise quasi-polynomial or a rational generating function. In the full version of this paper, we also translate known computational complexity results into this setting and discuss open directions.