The Computational Lense on the Relationship between Presburger Arithmetic and Context-Free Commutative Grammars

Presburger arithmetic---the first-order theory of the natural numbers with addition and order---and context-free commutative grammars---context-free grammars in which one is only interested in the number of times alphabet symbols occur in a generated word---are objects which have been studied since the early days of computer science. Ginsburg and Spanier showed in 1964 that the sets of natural numbers definable in Presburger arithmetic are semi-linear sets, and Parikh showed in 1961 that languages generated by context-free commutative grammars coincide with semi-linear sets as well. Thus, Presburger arithmetic and context-free commutative grammars are equally expressive. Taking the equivalence problem for context-free commutative grammars as a starting point, in this talk I will demonstrate that Presburger arithmetic and context-free commutative grammars are essentially equally succinct. The equivalence problem was shown to be decidable in coNEXP by Huynh in 1985, and he conjectured that it might actually be decidable in the second level of the polynomial-time hierarchy. By establishing new complexity results for Presburger arithmetic and inter-reductions between the validity problem in forall-exists-Presburger arithmetic and the equivalence problem, I will show that the equivalence problem is actually coNEXP complete, thereby answering Huynh's conjecture negatively. Partly based on joint work with Piotr Hofman (Cachan).