Presburger arithmetic, rational generating functions, and quasi-polynomials

TL;DR

This paper explores the connection between Presburger arithmetic, rational generating functions, and quasi-polynomials, providing characterizations, representations, and complexity insights for sets and counting functions definable within this logical framework.

Contribution

It characterizes sets definable by Presburger formulas via rational generating functions and quasi-polynomials, and relates these to computational complexity results.

Findings

Sets definable by Presburger formulas correspond to those with rational generating functions.

Counting functions in Presburger arithmetic can be expressed as quasi-polynomials or rational generating functions.

The paper discusses complexity implications and open problems in this framework.

Abstract

Presburger arithmetic is the first-order theory of the natural numbers with addition (but no multiplication). 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. Finally, we translate known computational complexity results into this setting and discuss open directions.