Semilinear set

In mathematics and theoretical computer science, a semilinear set (also written semi-linear set) is a set of vectors of natural numbers or integers that can be built from finitely many linear sets, each generated by a base vector together with finitely many period vectors. Semilinear sets are a higher-dimensional analogue of an arithmetic progression: where a progression is generated by repeatedly adding one common difference, a linear set is generated by repeatedly adding any of several period vectors, in any combination and any number of times.

Their importance rests on a series of equivalences established in the 1960s. The semilinear sets are exactly the sets definable in Presburger arithmetic,Template:Sfn exactly the rational subsets of the commutative monoid ${\mathbb{N}}^d$,Template:Sfn and exactly the sets arising as commutative images of context-free languages.Template:Sfn They therefore serve as a finite, effective representation of certain infinite sets of integer vectors, and are used throughout formal language theory, verification and related areas.Template:SfnTemplate:Sfn

Definition

A subset $L\subseteq {\mathbb{N}}^d$ is linear if it is of the form $$L=\{𝐛+\sum _{i=1}^m{k}_i{𝐩}_i:k_1,\dots ,k_m\in \mathbb{N}\},$$ where $m\in \mathbb{N}$ and $𝐛,{𝐩}_1,\dots ,{𝐩}_m$ are fixed vectors in ${\mathbb{N}}^d$, called the base vector and the period vectors respectively. A subset of ${\mathbb{N}}^d$ is semilinear if it is a finite union of linear sets.Template:Sfn

The number $m$ of periods may be zero, so that every singleton is linear; the empty set is semilinear as the empty union. A pair consisting of a base vector and a finite set of period vectors is called a representation of the linear set it generates, and a finite collection of such pairs a representation of the semilinear set they generate; representations are not unique.

A linear set with a single period vector $𝐩$ is the set of terms of the arithmetic progression $𝐛,𝐛+𝐩,𝐛+2𝐩,\dots$, and a general linear set is generated in the same way but from several common differences at once, applied in any combination and any number of times. The coefficients $k_i$ are unbounded, which distinguishes a linear set from a finite generalized arithmetic progression, where each coefficient is restricted to a bounded range.

Variants

The same definition is used for subsets of ${\mathbb{Z}}^d$, where the base and period vectors are allowed to have negative entries, while the coefficients $k_i$ still range over $\mathbb{N}$; in that setting the semilinear sets are the rational subsets of the group $({\mathbb{Z}}^d,+)$.Template:Sfn More generally, the definition makes sense in any finitely generated commutative monoid: a subset is linear if it has the form $x+B^{\oplus }$, where $x$ is an element of the monoid and $B^{\oplus }$ is the submonoid generated by a finite set $B$, and semilinear if it is a finite union of such sets.Template:SfnTemplate:Sfn

Because of the equivalence with definability in Presburger arithmetic, semilinear sets are also called Presburger sets or Presburger-definable sets.Template:Sfn

Examples

• Every finite subset of ${\mathbb{N}}^d$ is semilinear: it is the union of one linear set per element, each with no period vectors.
• The set of even natural numbers is the linear set with base $0$ and single period $2$.
• In ${\mathbb{N}}^2$, the set $\{(x,y)\mid x=y\}$ is linear, with base $(0,0)$ and period $(1,1)$; so is $\{(x,y)\mid x\le y\}$, with base $(0,0)$ and periods $(1,1)$ and $(0,1)$.
• The union of the two coordinate axes of ${\mathbb{N}}^2$ is semilinear but not linear.
• The set of powers of two is not semilinear, since a semilinear subset of $\mathbb{N}$ is a finite union of arithmetic progressions and hence ultimately periodic. For the same reason the set of primes and the set of squares are not semilinear.

Equivalent characterisations

Presburger arithmetic

Seymour Ginsburg and Edwin Spanier proved that the semilinear sets coincide with the sets defined by Presburger formulas, so that every such set has both an "internal" description as a finite union of linear sets and an "external" description by a formula of Presburger arithmetic, each effectively obtainable from the other.Template:Sfnm

Rational sets

Samuel Eilenberg and Marcel-Paul Schützenberger showed that the semilinear sets are precisely the rational subsets of the commutative monoid ${\mathbb{N}}^d$, that is, the sets obtainable from finite sets by union, elementwise addition and iteration.Template:Sfn

Parikh images

The Parikh image of a word over an alphabet of $d$ letters is the vector in ${\mathbb{N}}^d$ recording how many times each letter occurs; the Parikh image of a language is the set of images of its words. Parikh's theorem states that the Parikh image of every context-free language is semilinear; conversely every semilinear set is the Parikh image of a regular language, so that every context-free language has the same Parikh image as some regular language.Template:Sfn

Solutions of linear systems

The set of solutions in ${\mathbb{N}}^d$ of a finite system of linear equalities and inequalities with integer coefficients is semilinear, since such a system is expressible as a quantifier-free Presburger formula; the same holds for finite unions of such solution sets.Template:Sfnm

Closure properties

The equivalence with Presburger arithmetic gives closure under the Boolean operations of union, intersection and complement, and under projection, since the corresponding operations on formulas are disjunction, conjunction, negation and existential quantification.Template:Sfn Closure under intersection and complement is not apparent from the definition: the intersection of two linear sets need not be linear, and the complement of a linear set need not be. Eilenberg and Schützenberger derived the same closure properties algebraically, showing that the rational subsets of a finitely generated commutative monoid form a Boolean algebra.Template:Sfn

Semilinear sets are also closed under elementwise addition and under iteration, both immediately from the description as rational sets,Template:Sfn and under images and preimages of affine maps with integer coefficients.Template:Sfn

Algorithmic properties

Presburger arithmetic is decidable, a result of Mojżesz Presburger.Template:Sfn Since a semilinear representation and a defining Presburger formula can each be computed from the other, membership, emptiness, inclusion and equivalence questions for semilinear sets can be phrased as Presburger sentences and settled by the decision procedure, in either presentation.Template:Sfnm

These procedures are expensive in general: deciding the truth of a Presburger sentence requires doubly exponential nondeterministic time in the worst case. Satisfiability for the existential fragment, which suffices to express membership in a semilinear set given by a representation with binary-encoded vectors, is NP-complete.Template:Sfn

Descriptional complexity

Semilinear sets are usually presented implicitly, by a Presburger formula or by other means rather than by an explicit list of base and period vectors, and the effect of Boolean operations on the size of a description had chiefly been studied for the explicit presentation. Dmitry Chistikov and Christoph Haase developed a framework for implicitly presented semilinear sets in which size is measured by the norm, the largest magnitude of a generator, and assembled a collection of operations and decompositions with bounds stated in those terms; their approach yields exponentially better bounds for complement and for set difference than were previously known.Template:Sfn

Bounds on the magnitude of minimal solutions to systems of linear integer equalities and inequalities, due to Joachim von zur Gathen and Malte Sieveking, underlie many such estimates.Template:Sfn

Applications

Semilinearity is a recurring dividing line in the analysis of infinite-state systems, because a semilinear set of configurations can be manipulated symbolically and tested by the decision procedures for Presburger arithmetic. Oscar Ibarra showed that the reachability sets of reversal-bounded multicounter machines are effectively semilinear, which yields decidability of a range of verification questions for them.Template:Sfn By contrast, John Hopcroft and Jean-Jacques Pansiot showed that reachability sets of vector addition systems are effectively semilinear in dimension at most five but not in general, exhibiting a six-dimensional system whose reachability set is not semilinear.Template:Sfn

History

The notion arose from work on formal language theory in the 1960s. Ginsburg and Spanier introduced bounded ALGOL-like languages in 1964, where linear and semilinear sets appear in the analysis of their structure,Template:Sfn and established the equivalence with Presburger arithmetic in 1966.Template:Sfn Rohit Parikh proved the semilinearity of the commutative images of context-free languages in a 1961 technical report, published in revised form in 1966,Template:Sfn and Eilenberg and Schützenberger gave the characterisation in terms of rational sets in 1969.Template:Sfn

See also

• Presburger arithmetic
• Parikh's theorem
• Generalized arithmetic progression
• Rational set
• Context-free language
• Numerical semigroup

References

• Template:Cite conference
• Template:Cite journal
• Template:Cite journal
• Template:Cite journal
• Template:Cite journal
• Template:Cite journal
• Template:Cite journal
• Template:Cite journal
• Template:Cite conference
• Template:Cite book
• Template:Cite journal

External links

• Template:YouTube