Stable computation by count-conserving CRNs (CRN-3, transfer)

A population protocol is a count-conserving bimolecular CRN on the species Q [CDS14, §2.2]: the transition δ(p, q) = (p', q') is the reaction p + q → p' + q' (CRN-1's Reaction), and the count vectors reachable in the CRN are those of the configurations reachable in the protocol (Protocol.exists_network). Transitions that do not change the multiset {p, q} do not change the counts and give no reaction (CRN-1's networks have no such reactions).

A CRN with species S stably decides a predicate [CDS14, §2.2] through an injective input map I : X ↪ S (the input species) and an output map O : S → Bool (every species votes, as in the definitions of [AAE06]): from the initial count vector with xᵢ molecules of I i and nothing else, every reachable count vector can reach an output-stable one, in which every present species votes for the predicate's value, as in every count vector reachable from it. With the transfer, every stably computable predicate, hence every semilinear one, is stably decided by a count-conserving bimolecular CRN (IsSemilinearPred.exists_network).

References

• [CDS14] H.-L. Chen, D. Doty, D. Soloveichik, Deterministic function computation with chemical reaction networks, Natural Computing 13 (2014).
• [AAE06] D. Angluin, J. Aspnes, D. Eisenstat, Stably computable predicates are semilinear, PODC 2006.

def Crn.Counts.map {n : ℕ} {X : Type u_1} {S : Type u_2} [Fintype X] [Fintype S] [DecidableEq S] (f : X → S) (x : Counts X n) : Counts S n

The count vector x pushed forward along f : X → S: (x.map f) a = ∑_{i : f i = a} xᵢ. For the input map I of a CRN, x.map I is the initial count vector of the input counts x: xᵢ molecules of the input species I i and no other molecules [CDS14, §2.2].

Equations

• Crn.Counts.map f x = ⟨fun (a : S) => ∑ i : X with f i = a, ↑x i, ⋯⟩

theorem Crn.counts_comp {n : ℕ} {X : Type u_1} {S : Type u_2} [Fintype X] [DecidableEq X] [Fintype S] [DecidableEq S] (f : X → S) (ι : Fin n → X) : counts (f ∘ ι) = Counts.map f (counts ι)

Pushing input counts forward: counts (f ∘ ι) = (counts ι).map f.

def Crn.Network.Step {n : ℕ} {S : Type u_1} [Fintype S] [DecidableEq S] (N : Network S) (x y : Counts S n) : Prop

One reaction event x → y of the CRN N on count vectors [CDS14, §2.1]: some reaction of N whose reactant molecules are all present fires (Counts.react).

Equations

• N.Step x y = ∃ r ∈ N.reactions, (∀ (a : S), r.consumed a ≤ ↑x a) ∧ y = x.react r

def Crn.Network.Reaches {n : ℕ} {S : Type u_1} [Fintype S] [DecidableEq S] (N : Network S) : Counts S n → Counts S n → Prop

Reachability x →* y in the CRN N [CDS14, §2.1]: the reflexive-transitive closure of reaction events.

Equations

• N.Reaches = Relation.ReflTransGen N.Step

def Crn.Network.OutputStable {n : ℕ} {S : Type u_1} [Fintype S] [DecidableEq S] (N : Network S) (O : S → Bool) (b : Bool) (y : Counts S n) : Prop

A count vector y is output-stable with output b for the CRN N with output map O [CDS14, §2.2, every species voting]: in every count vector reachable from y, every species that is present votes b.

Equations

• N.OutputStable O b y = ∀ (z : Crn.Counts S n), N.Reaches y z → ∀ (a : S), ↑z a ≠ 0 → O a = b

def Crn.Network.StablyComputes {S : Type u_1} [Fintype S] [DecidableEq S] {X : Type u_2} [Fintype X] (N : Network S) (I : X ↪ S) (O : S → Bool) (φ : (X → ℕ) → Bool) : Prop

The CRN N with input species I : X ↪ S and output map O : S → Bool stably decides the predicate φ [CDS14, §2.2, leaderless and with every species voting]: for every nonzero input count vector x, every count vector reachable from the initial count vector x.map I can reach an output-stable count vector with output φ x.

Equations

• One or more equations did not get rendered due to their size.

theorem Crn.Protocol.exists_network {X : Type u_1} {Q : Type u_2} [Fintype Q] [DecidableEq Q] (P : Protocol X Q) (hP : ∃ (p : Q) (q : Q), s(p, q) ≠ s((P.δ (p, q)).1, (P.δ (p, q)).2)) : ∃ (N : Network Q), (∀ (r : Reaction Q), r ∈ N.reactions ↔ r.reactants ≠ r.products ∧ ∃ (p : Q) (q : Q), r.reactants = s(p, q) ∧ r.products = s((P.δ (p, q)).1, (P.δ (p, q)).2)) ∧ ∀ (n : ℕ) (c : Fin n → Q) (y : Counts Q n), N.Reaches (counts c) y ↔ ∃ (c' : Fin n → Q), P.Reaches c c' ∧ counts c' = y

CRN-3, transfer to CRNs ([CDS14, §2.2]; reachability version of CRN-1). A population protocol with finitely many states and at least one transition that changes the multiset of states of the two agents yields a count-conserving bimolecular CRN on the species Q, whose reactions are the transitions p + q → δ₁(p, q) + δ₂(p, q) that change {p, q}: in every population, the count vectors reachable in the CRN from the counts of a configuration c are exactly the counts of the configurations reachable from c in the protocol.

theorem Crn.StablyComputable.exists_network {X : Type u_1} [Fintype X] [DecidableEq X] {φ : (X → ℕ) → Bool} (h : StablyComputable φ) : ∃ (S : Type) (x : Fintype S) (x_1 : DecidableEq S) (N : Network S) (I : X ↪ S) (O : S → Bool), N.StablyComputes I O φ

CRN-3, transfer of stable computation: every predicate stably computable by a population protocol is stably decided by a count-conserving bimolecular CRN with finitely many species, injective input map and no initial context [CDS14, §2.2].

theorem Crn.IsSemilinearPred.exists_network {X : Type u_1} [Fintype X] [DecidableEq X] {φ : (X → ℕ) → Bool} (h : IsSemilinearPred φ) : ∃ (S : Type) (x : Fintype S) (x_1 : DecidableEq S) (N : Network S) (I : X ↪ S) (O : S → Bool), N.StablyComputes I O φ

CRN-3 (roadmap, easy direction, for CRNs): every Boolean combination of threshold and remainder predicates is stably decided by a count-conserving bimolecular CRN [AADFP06, Theorem 5; CDS14, Theorem 2.1, "if" direction].