- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Orange border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- Blue background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
- Dark green background
- the proof of this result and all its ancestors are formalized
- Dark green border
- this is in Mathlib
Species \(X\), \(Y\) (the two opinions) and \(B\) (blank), and the reactions \(X + Y \to X + B\), \(X + Y \to Y + B\), \(B + X \to X + X\), \(B + Y \to Y + Y\) (Angluin, Aspnes and Eisenstat).
A reaction \(A + B \to C + D\) consumes the unordered pair \(\{ A, B\} \) of species and produces the unordered pair \(\{ C, D\} \); a network is a nonempty finite set of reactions whose products differ from their reactants. A count vector of \(n\) molecules gives the number \(x_a\) of molecules of each species \(a\), with \(\sum _a x_a = n\); firing an applicable reaction \(r\) replaces \(x_a\) by \(x_a - \nu _a + \nu '_a\), with \(\nu \), \(\nu '\) the reactant and product multiplicities.
A network with an injective input map \(I : X \to S\) and an output map \(O : S \to \{ 0, 1\} \) stably decides \(\varphi \) if, from the initial count vector with \(x_i\) molecules of \(I(i)\) and nothing else, every reachable count vector can reach one in which, now and in every count vector reachable from it, every present species votes \(\varphi (x)\).
From \(x\) with \(a_0(x) {\gt} 0\) the jump chain fires \(r\) with probability \(a_r(x)/a_0(x)\); from a terminal state (\(a_0(x) = 0\)) it stays put.
Each of \(n \ge 2\) agents holds a species. One interaction draws a uniformly random ordered pair \((u, v)\) of distinct agents and, independently, a uniformly random reaction \(r\) of the network; if the species of \(u\) and \(v\) are the reactants of \(r\) the pair reacts and \(r\) fires, otherwise nothing changes. The protocol is observed on count vectors; conditioning on the pair reacting gives a kernel on count vectors.
With rate constant \(k\), the propensity of \(r\) at \(x\) is \(a_r(x) = k \prod _a \binom {x_a}{\nu _a}\) (Gillespie’s combinatorial form), and \(a_0(x) = \sum _r a_r(x)\).
A population protocol has an input function \(I : X \to Q\), an output function \(O : Q \to \{ 0, 1\} \) and a transition function \(\delta : Q \times Q \to Q \times Q\). An encounter of an ordered pair \((u, v)\) of distinct agents replaces their states \(p, q\) by \(\delta (p, q)\); reachability is the reflexive-transitive closure of encounters. A configuration is output-stable with output \(b\) if in every configuration reachable from it every agent outputs \(b\).
A protocol stably computes a predicate \(\varphi \) on input count vectors if, for every nonempty population and every input assignment \(\iota \), every configuration reachable from \(I \circ \iota \) can reach an output-stable configuration with output \(\varphi \) of the input counts. A predicate is stably computable if a protocol with finitely many states stably computes it.
The drawn pair has species \(\{ A, B\} \) with probability \(x_A x_B / \binom {n}{2}\) if \(A \ne B\), and \(\binom {x_A}{2} / \binom {n}{2}\) if \(A = B\). Equivalently, it has the reactants of \(r\) with probability \(a_r(x) / (k \binom {n}{2})\).
For \(A + B \to \cdots \) with \(A \ne B\) the propensity is \(k\, x_A x_B\); for \(A + A \to \cdots \) it is \(k \binom {x_A}{2}\).
With \(D = 2 x_X x_Y + x_B (x_X + x_Y) {\gt} 0\), the jump chain fires each \(X + Y\) reaction with probability \(x_X x_Y / D\), \(B + X \to X + X\) with probability \(x_B x_X / D\) and \(B + Y \to Y + Y\) with probability \(x_B x_Y / D\); a drawn pair reacts with probability \(D / (4 \binom {n}{2})\); and the jump chain is the population protocol conditioned on reacting.
For every Boolean function \(\xi \) of two arguments, if \(\varphi \) and \(\psi \) are stably computable then so is \(\xi (\varphi , \psi )\); in particular the class is closed under negation, conjunction and disjunction.
For every rate constant \(k {\gt} 0\) and \(n \ge 2\), the population protocol conditioned on the drawn pair reacting is the jump chain of mass-action kinetics, from every configuration and hence as kernels on count vectors.
For integers \(a_i\), \(c\) and \(m {\gt} 0\), the predicate \(\sum _i a_i x_i \equiv c \pmod m\) is stably computable.
The truth set of every such predicate is a semilinear set of count vectors, and every such predicate is stably computable.
The drawn pair reacts with probability \(p = a_0(x) / (k\, |N| \binom {n}{2})\), and one interaction is a jump of the mass-action chain with probability \(p\) and a no-op otherwise.
For integers \(a_i\) and \(c\), the predicates \(\sum _i a_i x_i {\lt} c\) and \(\sum _i a_i x_i \ge c\) are stably computable.
The transitions \(p + q \to \delta _1(p, q) + \delta _2(p, q)\) that change \(\{ p, q\} \) form a count-conserving bimolecular network whose reachable count vectors are the counts of the configurations reachable in the protocol. Hence every stably computable predicate, and in particular every Boolean combination of threshold and remainder predicates, is stably decided by such a network.