1
$\begingroup$

Q1. What are the "standard" techniques (if any) used to prove that a set of vectors in $\mathbb{N}^k$ defined using a set of constraints among the components is (or is not) a semilinear set (i.e. a finite union of linear sets) ?

For example, given:

$A = \{ \langle x_1, x_2, x_3, x_4, x_5, x_6 \rangle \mid \sum_i x_i \equiv 0 \bmod 6 \land [x_1 + x_2 + x_3 \neq x_4+x_5+x_6] \land [(x_1 + x_2 \neq x_3 + x_4) \lor (x_3 + x_4 \neq x_5 + x_6) ]\} $

how can I (dis)prove that $A$ is semilinear?

Q2. Can this process be automated assuming that the conditions are given using a set of logic expressions with numeric constants and operators $\land, \lor, +, -, =, \neq, \leq$? And if it can be automated, what is its (computational) complexity?

$\endgroup$
3
  • $\begingroup$ These are the definable sets in Presburger arithmetic en.m.wikipedia.org/wiki/Presburger_arithmetic. They are also the commutative images of context free languages. $\endgroup$ Jan 25, 2019 at 20:41
  • $\begingroup$ @BenjaminSteinberg: thanks, I was missing the theorem (Ginsburg & Spanier) A predicate is semi-linear if and only if it corresponds to a formula of Presburger’s arithmetic. My example becomes trivial: $x \equiv_k y$ iff $\exists z (x + z+z+...^{\text{k times}}...+z = y)$; and $A$ is semilinear. If you post it as an answer I'll accept it. $\endgroup$ Jan 25, 2019 at 21:38
  • $\begingroup$ I did what you asked. $\endgroup$ Jan 25, 2019 at 21:44

1 Answer 1

1
$\begingroup$

These are the definable sets in Presburger arithmetic https://en.m.wikipedia.org/wiki/Presburger_arithmetic. They are also the commutative images of context free languages.

$\endgroup$
1
  • $\begingroup$ Is there a reference for commutative images of context free languages? $\endgroup$
    – VS.
    Jun 3, 2020 at 9:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.