<p>I've recently learned about the connection between linear integer arithmetic (<a href="https://en.wikipedia.org/wiki/Presburger_arithmetic" rel="nofollow noreferrer">Presburger arithmetic</a>) and <a href="https://en.wikipedia.org/wiki/Deterministic_finite_automaton" rel="nofollow noreferrer">Deterministic Finite Automata</a> (DFAs). Namely, any formula in the first order theory of Presburger arithmetic can be converted to a DFA, which acts on binary digit representations of numbers. Then apparently, the decision problem and quantifier elimination can be done by manipulating the DFA. Key to this connection are the closure properties of Regular Languages, which are precisely the ones recognized by DFAs. Closure under unions, intersections and complements allows the translation of Boolean operations into the corresponding DFAs, while closure under projection allows the translation of existential quantification (universal quantification follows by combining with negation). This connection even has <a href="https://cs.uwaterloo.ca/%7Eshallit/walnut.html" rel="nofollow noreferrer">practical</a> <a href="https://github.com/ReedOei/Pecan" rel="nofollow noreferrer">applications</a>.</p>
<p>I wonder how far one could push the decidability of arithmetically interesting extensions of Presburger arithmetic (which is itself pretty weak) via a connection to a larger family of automata. The next common rung in the language/automata hierarchy are Context Free Languages (CFLs) and <a href="https://en.wikipedia.org/wiki/Pushdown_automaton" rel="nofollow noreferrer">Pushdown Automata</a> (PDAs). However, it seems that family does not enjoy the same closure properties (CFLs are closed under unions, but not complementation or intersection), obstructing a possible connection.</p>
<p>On the other hand, it seems that the subfamily of Deterministic CFLs/Deterministic PDAs is closed under complements, but not under unions or intersections (not sure about projection). However, DCFLs <a href="https://cs.stackexchange.com/q/58019">are closed</a> under unions and intersections with Regular Languages. This suggests that it should be possible to translate to DPDAs some restricted extension of the first order theory of Presburger arithmetic with some new relations and operations that are allowed by DPDAs. This new theory would still be decidable, via DPDA manipulation. <strong>Question:</strong> Is it known what this fragment of arithmetic is (obviously extending linear integer arithmetic)?</p>
<p>Here's an example of what could be allowed. Presburger arithmetic can talk about addition tuples of integers of fixed length (just use formulas with the required fixed number of free integer variables). But I think it can't talk about addition of tuples of integers of finite but unbounded lengths (think of polynomials with integer coefficients as an instance of this), which should be possible in the above extension. Namely, encode a polynomial <span class="math-container">$a_0 + a_1 x + \cdots + a_k x^k$</span> by shuffling together the digit expansions of the coefficients, <span class="math-container">$a_i = a_{i,0}a_{i,1}\cdots$</span>, as <span class="math-container">$(a_{0,0}) (a_{0,1}a_{1,0}) (a_{0,2}a_{1,1}a_{2,0}) \cdots$</span>. When doing addition digit by digit, the carry operation can't be recognized by a DFA, but could be by a DPDA. (I'm not really claiming to have a proof of this; it's just a heuristic observation.) What about addition of polynomials in two or more variables? What about differentiation <span class="math-container">$\frac{d}{dx}$</span> of polynomials?</p>
<p>This is all quite far away from my comfort zone, so apologies for any excessive imprecision or errors. Corrections welcome!</p>
<p><em>P.S.:</em> Just found that a <a href="https://cs.stackexchange.com/q/119966">similar question</a> was asked a while ago over at cs.SE, but did not get much attention.</p>

CC BY-SA 4.0
2024-08-11T18:49:33.597Z
The most interesting extensions here are to infinite automata, leading to decidability of S1S and S2S.
Dmytro Taranovsky
CC BY-SA 4.0
2024-08-12T04:49:02.563Z
@DmytroTaranovsky Thanks. Could you explain a little bit to a non-logician what those extensions can express, for instance relative to the examples I used above? And how are infinite automata related to the DPDAs from the question?
Igor Khavkine
CC BY-SA 4.0
2024-08-13T16:15:30.083Z
S1S allows infinite binary sequences (instead of just finite), and [S2S](https://en.wikipedia.org/wiki/S2S_(mathematics)) further extends this to the monadic second order theory of the full infinite binary tree.  In S2S, you can encode single-variable polynomials and addition, but without the ability to test for equality between coefficients for different powers.  Decidability of S2S uses infinite tree automata, but the automata are still regular.  Given their lack of closure, PDAs are a poor match for decidability of first order theories as opposed to problems more generally.
Dmytro Taranovsky
<lo.logic><automata-theory><context-free><decidability>
Extensions of linear integer arithmetic decidable via Deterministic Pushdown Automata
Igor Khavkine
# Extensions of linear integer arithmetic decidable via Deterministic Pushdown Automata

(Asked by: username_0 on 2024-08-10)

I've recently learned about the connection between linear integer arithmetic ([Presburger arithmetic](https://en.wikipedia.org/wiki/Presburger_arithmetic)) and [Deterministic Finite Automata](https://en.wikipedia.org/wiki/Deterministic_finite_automaton) (DFAs). Namely, any formula in the first order theory of Presburger arithmetic can be converted to a DFA, which acts on binary digit representations of numbers. Then apparently, the decision problem and quantifier elimination can be done by manipulating the DFA. Key to this connection are the closure properties of Regular Languages, which are precisely the ones recognized by DFAs. Closure under unions, intersections and complements allows the translation of Boolean operations into the corresponding DFAs, while closure under projection allows the translation of existential quantification (universal quantification follows by combining with negation). This connection even has [practical](https://cs.uwaterloo.ca/%7Eshallit/walnut.html) [applications](https://github.com/ReedOei/Pecan).

I wonder how far one could push the decidability of arithmetically interesting extensions of Presburger arithmetic (which is itself pretty weak) via a connection to a larger family of automata. The next common rung in the language/automata hierarchy are Context Free Languages (CFLs) and [Pushdown Automata](https://en.wikipedia.org/wiki/Pushdown_automaton) (PDAs). However, it seems that family does not enjoy the same closure properties (CFLs are closed under unions, but not complementation or intersection), obstructing a possible connection.

On the other hand, it seems that the subfamily of Deterministic CFLs/Deterministic PDAs is closed under complements, but not under unions or intersections (not sure about projection). However, DCFLs [are closed](https://cs.stackexchange.com/q/58019) under unions and intersections with Regular Languages. This suggests that it should be possible to translate to DPDAs some restricted extension of the first order theory of Presburger arithmetic with some new relations and operations that are allowed by DPDAs. This new theory would still be decidable, via DPDA manipulation. **Question:** Is it known what this fragment of arithmetic is (obviously extending linear integer arithmetic)?

Here's an example of what could be allowed. Presburger arithmetic can talk about addition tuples of integers of fixed length (just use formulas with the required fixed number of free integer variables). But I think it can't talk about addition of tuples of integers of finite but unbounded lengths (think of polynomials with integer coefficients as an instance of this), which should be possible in the above extension. Namely, encode a polynomial $a\_0 + a\_1 x + \cdots + a\_k x^k$ by shuffling together the digit expansions of the coefficients, $a\_i = a\_{i,0}a\_{i,1}\cdots$, as $(a\_{0,0}) (a\_{0,1}a\_{1,0}) (a\_{0,2}a\_{1,1}a\_{2,0}) \cdots$. When doing addition digit by digit, the carry operation can't be recognized by a DFA, but could be by a DPDA. (I'm not really claiming to have a proof of this; it's just a heuristic observation.) What about addition of polynomials in two or more variables? What about differentiation $\frac{d}{dx}$ of polynomials?

This is all quite far away from my comfort zone, so apologies for any excessive imprecision or errors. Corrections welcome!

*P.S.:* Just found that a [similar question](https://cs.stackexchange.com/q/119966) was asked a while ago over at cs.SE, but did not get much attention.

**Tags:** lo.logic, automata-theory, context-free, decidability
> **Comments:**
> **username_1**: The most interesting extensions here are to infinite automata, leading to decidability of S1S and S2S.  
> **username_0**: @DmytroTaranovsky Thanks. Could you explain a little bit to a non-logician what those extensions can express, for instance relative to the examples I used above? And how are infinite automata related to the DPDAs from the question?  
> **username_1**: S1S allows infinite binary sequences (instead of just finite), and [S2S](https://en.wikipedia.org/wiki/S2S_(mathematics)) further extends this to the monadic second order theory of the full infinite binary tree.  In S2S, you can encode single-variable polynomials and addition, but without the ability to test for equality between coefficients for different powers.  Decidability of S2S uses infinite tree automata, but the automata are still regular.  Given their lack of closure, PDAs are a poor match for decidability of first order theories as opposed to problems more generally.  

---

## 0 answers

