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$
  • $\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$ – Benjamin Steinberg Jan 25 '19 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$ – Marzio De Biasi Jan 25 '19 at 21:38
  • $\begingroup$ I did what you asked. $\endgroup$ – Benjamin Steinberg Jan 25 '19 at 21:44
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.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ Is there a reference for commutative images of context free languages? $\endgroup$ – VS. Jun 3 at 9:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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