Semilinear predicates are stably computable (CRN-3, easy direction) #
[AADFP06, Theorem 5]: every Presburger-definable predicate on input counts is stably computable. Its proof applies Presburger's quantifier elimination [AADFP06, Theorem 4] to write the predicate as a Boolean combination of threshold and remainder predicates (equalities are conjunctions of two thresholds), which are stably computable [AADFP06, Lemma 5], and concludes by Boolean closure [AADFP06, Corollary 2].
We take the Boolean combinations of threshold and remainder predicates as the definition of the
class (IsSemilinearPred) and prove that all of them are stably computable. That this class is
exactly the class of semilinear (equivalently, by Ginsburg–Spanier, Presburger-definable) sets of
count vectors is not formalized; only the inclusion into Mathlib's semilinear sets is stated
(IsSemilinearPred.isSemilinearSet; Mathlib's presburger.definable_iff_isSemilinearSet then
gives Presburger definability). The converse inclusion is Presburger's quantifier elimination.
The semilinear predicates on input counts, defined as the Boolean combinations of threshold
predicates ∑ᵢ aᵢ xᵢ < c and remainder predicates ∑ᵢ aᵢ xᵢ ≡ c (mod m) [AADFP06, proof of
Theorem 5]. By Presburger's quantifier elimination [AADFP06, Theorem 4] and Ginsburg–Spanier
[AADFP06, Theorem 3] these are exactly the predicates whose truth sets are semilinear, that is,
Presburger-definable; only the inclusion IsSemilinearPred.isSemilinearSet is formalized.
- threshold
{X : Type u_1}
[Fintype X]
(a : X → ℤ)
(c : ℤ)
: IsSemilinearPred (Crn.threshold a c)
Threshold predicates
∑ᵢ aᵢ xᵢ < c[AADFP06, Lemma 5(1)]. - remainder
{X : Type u_1}
[Fintype X]
(a : X → ℤ)
(c : ℤ)
{m : ℕ}
(hm : 0 < m)
: IsSemilinearPred (Crn.remainder a c m)
Remainder predicates
∑ᵢ aᵢ xᵢ ≡ c (mod m),m > 0[AADFP06, Lemma 5(2)]. - not
{X : Type u_1}
[Fintype X]
{φ : (X → ℕ) → Bool}
: IsSemilinearPred φ → IsSemilinearPred fun (x : X → ℕ) => !φ x
Negation.
- and
{X : Type u_1}
[Fintype X]
{φ ψ : (X → ℕ) → Bool}
: IsSemilinearPred φ → IsSemilinearPred ψ → IsSemilinearPred fun (x : X → ℕ) => φ x && ψ x
Conjunction.
- or
{X : Type u_1}
[Fintype X]
{φ ψ : (X → ℕ) → Bool}
: IsSemilinearPred φ → IsSemilinearPred ψ → IsSemilinearPred fun (x : X → ℕ) => φ x || ψ x
Disjunction.
Instances For
The truth set of a semilinear predicate is a semilinear set of count vectors in Mathlib's
sense, hence Presburger-definable (presburger.definable_iff_isSemilinearSet). This checks that
IsSemilinearPred is not larger than the semilinear predicates.
CRN-3, easy direction [AADFP06, Theorem 5, with Lemma 5 and Corollary 2]: every Boolean combination of threshold and remainder predicates is stably computable by a population protocol.