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?

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

1 Answer 1

Reset to default
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.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Is there a reference for commutative images of context free languages? $\endgroup$
    – VS.
    Commented Jun 3, 2020 at 9:33
  • $\begingroup$ Its called Parikh's theorem, Parikh published it in two papers in '61 und '66 (see wikipedia entry). Different proofs have been published that investigate complexity and descriptive aspects; an algebraic proof was given by Donald Pilling for example. $\endgroup$
    – StefanH
    Commented Nov 12 at 14:36

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .