Presburger arithmetic, rational generating functions, and quasi-polynomials
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.
Keywords
Cite
@article{arxiv.1211.0020,
title = {Presburger arithmetic, rational generating functions, and quasi-polynomials},
author = {Kevin Woods},
journal= {arXiv preprint arXiv:1211.0020},
year = {2015}
}
Comments
revised, including significant additions explaining computational complexity results. To appear in Journal of Symbolic Logic. Extended abstract in ICALP 2013. 17 pages