text:
\section{Introduction}
\input{sec-introduction}

\section{Preliminaries}\label{sec:prelims}
\input{sec-preliminaries}

\section{Population protocols}\label{sec:popprot}
\input{sec-protocols}

\section{Main result}\label{sec:main}
\input{sec-main}

\section{Succinct protocols for large populations}\label{sec:large}
\input{sec-large}

\section{Succinct protocols for small populations}\label{sec:small}
\input{sec-small}

\section{Conclusion and further work}\label{sec:conc}
\input{sec-conclusion}

\subsubsection{Remainder protocols}\label{subsec:app-remainder}

This section describes a family of protocols with helpers computing
remainder predicates under reversible dynamic initialization. The
construction, its correctness proof and its intermediary propositions
are similar to those presented in \cref{subsec:app-threshold} for
the case of threshold predicates. For completeness, we repeat and
adapt them in full details.

Let us fix a remainder predicate $\varphi$ over variables $X$.
Let $\varphi(\vec{v}) \defeq \vec{a} \cdot \vec{v} \equiv_m b$
where $\vec{a} \in \Z^X$ and $m \in \N_{\geq 2}$ and $b \in \Z$.
Without loss of generality\footnote{If this is not the case for some coefficient
	 $\vec{a}(x)$, then we can replace it by $\vec{a}(x) \bmod m$,
	 which yields an equivalent predicate.},
we may assume $0 \leq b < m$ and $0 \leq \vec{a}(x) < m$ for each $x \in X$.

Instead of directly constructing a protocol for $\varphi(\vec{v})$, we rewrite the predicate. This yields a different but equivalent predicate $\varphi'(\vec{v})$:
\begin{align*}
\varphi'(v) \defeq
	\begin{cases}
		\vec{a} \cdot \vec{v} \not \geq 1~(\text{mod } m)
			& \text{ if } b = 0, \\
		\vec{a} \cdot \vec{v} \geq b ~(\text{mod } m) \land \vec{a} \cdot \vec{v} \not\geq b + 1 ~(\text{mod } m)
			& \text{ if } b > 0. \\
	\end{cases}
\end{align*}

As we can handle negations and conjunctions separately in \cref{subsec:finsets},
it is enough to describe a protocol for the predicate
$\varphi(\vec{v}) \defeq \vec{a} \cdot \vec{v} \geq b~(\text{mod } m)$ where
$\vec{a} \in \N^X$, $m \in \N_{\geq 2}$, $0 < b < m$ and $0 \leq \vec{a}(x) < m$ for each $x \in X$.

We construct a simple population protocol $\PP_{\text{rem}}$ with helpers that
computes $\varphi$ under reversible dynamic initialization, and prove its correctness.

\parag{Notation} Let $n$ be the smallest number such that $2^n >
\norm{\varphi}$. Let $P \defeq \{\q{2^i} : 0 \leq i \leq
n\}$, $Z \defeq \{\q{0}\}$, $N \defeq P \cup Z$ and $B \defeq \{\q{f},
\q{t}\}$, where $P$, $Z$, $N$ and $B$ respectively stand for
``$P$owers of two'', ``$Z$ero'', ``$N$umerical values'' and
``$B$oolean values''. For every set $S$ and every $x \in X$, let $S_x
\defeq \{q_x : q \in S\}$ and $S_X \defeq S \cup \bigcup_{x \in X}
S_x$.

For every $d \in \N$, let $\mathrm{bits}(d)$ denote the unique set $J
\subseteq \N$ such that $d = \sum_{j \in J} 2^j$,
\eg\ $\mathrm{bits}(13) = \mathrm{bits}(1101_2) = \{3, 2, 0\}$. The \emph{canonical representation} of an integer $d \in \Z$ is the multiset $\mathrm{rep}(d)$ defined as follows:
$$
\mathrm{rep}(d) \defeq
\begin{cases}
\multiset{\q{2^i} : i \in \mathrm{bits}(d)}   & \text{if } d > 0, \\
\multiset{\q{0}}                              & \text{if } d = 0.
\end{cases}
$$

\parag{The protocol} The RDI-protocol $\PP_{\text{rem}} = (Q, T_\infty, T_\dagger, L, X, I, O)$ is defined as
follows:
\begin{itemize}
\setlength\itemsep{4pt}

  \item  $Q \defeq X \cup N_X \cup B$. \\
	Intuitively, the states of $X$ are the ``ports'' through which the agents for each variable
	enter and exit the protocol.

	\item  $I \defeq x \mapsto \q{x}$. \\
	That is, the initial state for variable $x$ is $x$.

	\item $L \defeq \multiset{2n \cdot \q{0}, \q{f}}$. \\
	So, we have $2n$ helpers in state $\q{0}$, and one helper in state $\q{f}$, i.e., initially
	the protocol assumes that the predicate does not hold.

	\item $O(q) \defeq q \mapsto (0 \text{ if } q = \q{f} \text{ else } 1
	\text{ if } q = \q{t} \text{ else } \bot)$. \\
	That is, the output of the protocol is completely determined by the number of agents
	in states $\q{t}$ and $\q{f}$

	\item $T_\infty$ is the following set of (``permanent'') transitions:
	\begin{alignat*}{3}
		\mathsf{add}_{x}:\ &&
		\multiset{x, |\mathrm{rep}(\vec{a}(x))| \cdot \q{0}}
		& \mapsto \multiset{\q{0}_x} \mplus \mathrm{rep}(\vec{a}(x))
		&& \qquad \text{for every $x \in X$,} \\
		%
		\mathsf{up}_i:\ &&
		\multiset{\q{2^i}, \q{2^i}}
		&  \mapsto \multiset{\q{2^{i+1}}, \q{0}}
		&& \qquad\text{for every $0 \leq i < n$,} \\
		%
		\mathsf{down}_i:\ &&
		\multiset{\q{2^i}, \q{0}}
		&  \mapsto \multiset{\q{2^{i-1}}, \q{{2^{i-1}}}}
		&& \qquad\text{for every $0 < i \leq n$,} \\
		%
		\mathsf{modulo}_q:\ &&
		\mathrm{rep}(b) \mplus \multiset{q}
		&  \mapsto \mathrm{rep}(b) \mplus \multiset{\q{f}}
		&& \qquad\text{for every $q \in B$,} \\
		%
		\mathsf{swap}_{p, q}^x:\ &&
		\multiset{p, q_x}
		& \mapsto \multiset{p_x, q}
		&& \qquad \text{for every $p, q \in N$ and $x \in X$,} \\
		%
		\mathsf{equal}:\ &&
		\mathrm{rep}(b) \mplus \multiset{\q{f}}
		& \mapsto \mathrm{rep}(b) \mplus \multiset{\q{t}}, \\
		%
		\mathsf{false}:\ &&
		\multiset{\q{f}, \q{t}} & \mapsto \multiset{\q{f}, \q{f}}.
	\end{alignat*}
	Intuitively, $\mathsf{add}_{x}$ converts an agent which arrived via port $x$ into
	the canonical representation of $\vec{a}(x)$. Transitions of the form $\mathsf{up}_i,
	\mathsf{down}_i$ allow the protocol to change
	the representation of a value, without changing the value itself.
	The $\mathsf{modulo}$ transition reduces the overall value by $m$.
	Transition $\mathsf{equal}$ allows the protocol to detect that the current value
	is at least $b$, which moves a helper from state $\q{f}$ to $\q{t}$.
	\item Finally, $T_{\dagger}$ is the following set of RDI-transitions:
	\begin{alignat*}{3}
		\mathsf{add}_{x,q}^{-1}:\ &&
		\multiset{\q{0}_x, q} \mplus \mathrm{rep}(\vec{a}(x))
		& \mapsto \multiset{x, \q{f}, |\mathrm{rep}(\vec{a}(x))| \cdot \q{0}}
		&& \quad \text{for every $x \in X$ and $q \in B$,} \\
		%
		\mathsf{modulo}_q^{-1}:\ &&
		\mathrm{rep}(b) \mplus \multiset{q}
		&  \mapsto \mathrm{rep}(b) \mplus \multiset{\q{f}}
		&& \quad\text{for every $q \in B$,} \\
		%
		\mathsf{reset}:\ &&
		\multiset{\q{t}}
		& \mapsto \multiset{\q{f}}.
	\end{alignat*}
	The first two transitions are needed to reverse the changes of
	$\mathsf{add}$ and $\mathsf{modulo}$ transitions while the dynamic
	initialization is not finished. Both types of transitions reset the output of the protocol
	by leaving an agent in the default output state $\q{f}$. The
	$\mathsf{reset}$ transition resets the output by moving agents from
	$\q{t}$ to $\q{f}$.
\end{itemize}

\noindent Let $\PP_\infty = (Q, T_\infty, L, X, I , O)$.
Let $T \defeq T_\infty \cup T_\dagger$. For the sake of readability,
we will sometimes omit the subscripts and superscripts from transitions names
when they are irrelevant, \eg\ ``a
$\mathsf{swap}$ transition is enabled'' instead of ``there exist $p, q
\in N$ and $x \in X$ such that $\mathsf{swap}_{p,q}^x$ is enabled''.\medskip

\parag{Size} Note that $\PP_{\text{rem}}$ has $|Q| = |X| + |N_X| + |B|
= |X| + (n+2) \cdot (|X|+1) + 2 = \O(\log \norm{\varphi} \cdot |X|)$
states and $|L| = 2n+1 = \O(\log \norm{\varphi})$ helpers. Moreover,
since families of transitions are parameterized by $X$, $B$ and $N$ or $N^2$,
there are $\O(|N|^2 \cdot |X|) = \O(\log^2 \norm{\varphi} \cdot |X|)
\subseteq \O(|\varphi|^3)$ transitions. Finally, each transition uses at most
$\O(|\mathrm{rep}(\norm{\varphi})|) = \O(\log \norm{\varphi})
\subseteq \O(|\varphi|)$ states.\medskip

\parag{Auxiliary definitions and observations} Before proving that
$\PP_{\text{rem}}$ works as intended, let us first introduce auxiliary
definitions. Let $\val \colon Q \to \N$ be the function that
associates a value to each state as follows:
\begin{align*}
	\val(\q{0}) &= \val(\q{f}) = \val(\q{t}) \defeq 0, \\
	%
	\val(x) &\defeq \vec{a}(x)
	&& \text{for every } x \in X, \\
	%
	\val(\q{2^i}) &\defeq 2^i
	&& \text{for every } 0 \leq i \leq n, \\
	%
	\val(q_x) &\defeq \val(q)
	&& \text{for every } q \in N \text{ and } x \in X.
\end{align*}
\noindent So, for example, for the predicate $5x + 6y \geq 4\ (\bmod\ m)$ we have $\val(x) = 5$ and
$\val(y) = 6$.
For every configuration $C$ and set of states $S \subseteq Q$, let
$$\val_S(C) \defeq \sum_{q \in S} \val(q) \cdot C(q).$$
In particular, let $\val(C) \defeq \val_Q(C)$.
Intuitively, $C$ can be seen as an encoding of the value $\val(C)$.
The following properties, relating values and configurations, can be derived from
the above definitions:
\begin{proposition}\label{prop:rem:prop}
	For every initialization sequence $\pi$ with effective input $\vec{w}$ such
	that $L' \trans{\pi} C$ for some $L' \succeq L$, the following holds:
	\begin{enumerate}
		\item $\val(C) \equiv_m \vec{a} \cdot \vec{w}$, \label{itm:rem:val:inv}

		\item $\val(C) \leq \vec{a} \cdot \vec{w}$, \label{itm:rem:val:dec}

		\item $|C| = C(N) + C(B) + |\vec{w}|$, \label{itm:rem:config:size}

		\item $C(N) \geq L(N)$ and $C(B) \geq L(B)$, \label{itm:rem:preservation}

		\item $C(N_x) + C(x) = \vec{w}(x)$ for every $x \in
		X$. \label{itm:rem:preservation:x}
	\end{enumerate}
\end{proposition}

\parag{Auxiliary propositions} We say that a configuration $C$ is
\emph{clean} if for every $p, q \in P_X$ with $\val(p) = \val(q)$ and $\val(p)
\not= 2^n$, it holds that $C(\{p, q\}) \leq 1$. Intuitively, in a clean configuration
no agent can be promoted to a higher power of 2.

We show that any configuration can be cleaned using only permanent transitions.
This implies that once the dynamic initialization has terminated, every fair
execution visits clean configurations infinitely often.

\begin{proposition}\label{prop:rem:cleaning}
	For every initialization sequence $\pi$ such that $L' \trans{\pi} C$
	for some $L' \succeq L$, there exists a clean configuration $D$
	such that $C \trans{T_{\infty}^*} D$.
\end{proposition}
\begin{proof}
	If $C$ is clean, then we pick $D \defeq C$. Otherwise, we claim there
	exists a configuration $C'$ such that $C \trans{*} C'$ and $C(P_X) >
	C'(P_X)$. If $C'$ is clean, then we are	done. Otherwise, this process
	is repeated until a clean configuration $D$ has been reached. This must
	terminate as the number of agents in $P_X$ cannot become negative.

	Let us prove the claim. If $C$ is not clean, then $C(\{p, q\}) \geq 2$
	for some $p, q \in P_X$ such that $\val(p) = \val(q)$ and $\val(p)
	\not= 2^n$. By \cref{prop:rem:prop}~\eqref{itm:rem:preservation}, we have
	$C(N) \geq L(N) \geq 2$ and hence it is possible to consecutively
	fire at least two $\mathsf{swap}$ transitions. Note that they do not
	change the amount of agents in $P_X$. For this reason, we may assume
	without loss of generality that $p = q = \q{2^i}$ for some $0 \leq i \leq
	n$. Therefore, firing transition $\mathsf{up}_i$ decreases
	$C(P_X)$ by one.
\end{proof}

We now bound the number of agents in states from $X \cup P_X$ in a
clean configuration.

\begin{proposition} \label{prop:rem:top:small}
	For every initialization sequence $\pi$ with effective input $\vec{w}$
	such that $L' \trans{\pi} C$ for some $L' \succeq L$, if $C$ is clean,
	then $C(X) + C(P_X) \leq |\vec{w}| + n$.
\end{proposition}

\begin{proof}
	Let $S_{2^n} \defeq \{q \in P_X : \val(q) = 2^n\}$. Let $\vec{u} \in \N^X$
	be such that $\vec{u}(x) \defeq C(x)$ for every $x \in X$.
	Note that $|\vec{u}| = C(X)$, and that $\vec{u} \leq \vec{w}$ by
	\cref{prop:rem:prop}~\eqref{itm:rem:preservation:x}.
	Since $C$ is clean, we have $C(P_X \setminus S_{2^n}) \leq n$.
	Thus, it suffices to show	that $C(S_{2^n}) \leq |\vec{w}| - |\vec{u}|$.
	Suppose this is not	the case. This yields a contradiction:
	\begin{align*}
		\val_{P_X}(C)
		&\geq 2^n \cdot C(S_{2^n}) \\
		%
		&> 2^n \cdot (|\vec{w}| - |\vec{u}|)
		&& \text{(by assumption)} \\
		%
		&\geq \vec{a} \cdot (\vec{w} - \vec{u}) && \text{(since $2^n >
			\norm{\vec{a}}$ and $\vec{w} \geq \vec{u}$)} \\
		%
		&= \vec{a} \cdot \vec{w} - \vec{a} \cdot \vec{u} \\
		%
		&\geq \val(C) - \val_X(C)
		&& \text{(by Prop.~\ref{prop:rem:prop}~\eqref{itm:rem:val:dec} and
			def.\ of $\vec{u}$)} \\
		%
		&= \val_{P_X}(C)
		&& \text{(by def.\ of $\val$)} \qedhere
	\end{align*}
\end{proof}

The following corollary shows that the number of agents in state
$\q{0}$ can always be increased back to at least $n$. This will later
be useful in arguing that the number of agents in $X$ can eventually
be decreased to zero.

\begin{corollary} \label{cor:rem:enough:zero}
	For every initialization sequence $\pi$ with effective input $\vec{w}$ such
	that $L' \trans{\pi} C$ for some $L' \succeq L$, there exists a clean
	configuration $D$ such that $C \trans{T_{\infty}^*} D$ and $D(\q{0}) \geq n$.
\end{corollary}

\begin{proof}
	By \cref{prop:rem:cleaning}, there exist a clean configuration $C'$ such
	that $C \trans{\pi' \in T_\infty^*} C'$. Let us first prove that $C'(Z_X) \geq n$.
	Note that $\pi\pi'$ is an initialization sequence with effective input
	$\vec{w}$ such that $L \trans{\pi\pi'} C'$. Thus:
	\begin{align*}
		C'(Z_X)
		&= |C'| - C'(X) - C'(P_X) - C'(B)
		&& \text{(by def.\ of $Q$)} \\
		%
		&= (C'(N) + C'(B) + |\vec{w}|) - C'(X) - C'(P_X) - C'(B)
		&& \text{(by Prop.~\ref{prop:rem:prop}~\eqref{itm:rem:config:size})} \\
		%
		&\geq (L(N) + C'(B) + |\vec{w}|) - C'(X) - C'(P_X) - C'(B)
		&& \text{(by Prop.~\ref{prop:rem:prop}~\eqref{itm:rem:preservation})} \\
		%
		&\geq (L(N) + C'(B) + |\vec{w}|) - (|\vec{w}| + n) - C'(B)
		&& \text{(by Prop.~\ref{prop:rem:top:small})} \\
		%
		&= L(N) - n \\
		%
		&\geq n
		&& \text{(by def.\ of $L$)}
	\end{align*}
	Now, by \cref{prop:rem:prop}~\eqref{itm:rem:preservation}, we have
	$C'(N) \geq L(N) \geq n$. Thus, using $\mathsf{swap}$ transitions, we
	can swap $n$ agents from $Z_X$ to $\q{0}$. This way, we obtain a
	configuration $D$ such that $C' \trans{T_{\infty}^*} D$ and $D(\q{0}) \geq
	n$. We are done since $\mathsf{swap}$ transitions preserve
	cleanness.
\end{proof}
We now show that, once dynamic initialization has terminated, fair executions
stabilize to configurations of a certain ``normal form''.

\begin{proposition}\label{prop:remainder:stabilize}
	For every initialization sequence $\pi$ with effective input $\vec{w}$ such that
	$L' \trans{\pi} C$ for some $L' \succeq L$ and for every fair execution
	$\sigma$ of $\PP_\infty$ starting from $C$, there exist
	$i \in \N, r \geq 0$ such that
	\begin{enumerate}
		\item $\sigma_i(X) = \sigma_{i+1}(X) = \cdots = 0$,

		\item $\val(\sigma_i) = \val(\sigma_{i+1}) = \cdots =
		r < m$.
	\end{enumerate}
\end{proposition}

\begin{proof}
	For the sake of contradiction, assume there exist infinitely many
	indices $j$ such that $\sigma_j(X) > 0$. Let $j \in \N$ be such an
	index. By \cref{cor:rem:enough:zero}, there exists a configuration $C_j$
	such that $\sigma_j \trans{T_{\infty}^*} C_j$ and $C_j(\q{0}) \geq n$. Hence,
	there exists $x \in X$ such that transition $\mathsf{add}_x$ is
	enabled in $C_j$. Since this holds for infinitely many indices and
	since $X$ is finite, fairness implies that some $\mathsf{add}$
	transition can be enabled infinitely often and hence occurs
	infinitely often along $\sigma$. This is impossible since the number
	of agents in $X$ cannot be increased by any transition in $T_\infty$,
	and thus would eventually drop below zero.
	Therefore, there exists $h \in \N$ such that
	$\sigma_h(X) = \sigma_{h+1}(X) = \cdots = 0$.

	Transitions $\mathsf{modulo_{\q{t}}}$ and $\mathsf{modulo_{\q{f}}}$
	reduce the value of a configuration by $m > 0$.
	$\mathsf{add}$ transitions are disabled in every configuration $\val(\sigma_{i})$
	with $i \geq h$ and all other transitions in $T_\infty$
	do not change the value of a configuration.
	Moreover, the value of a configuration is always non-negative.
	Thus, there exist $i \geq h$, $r \geq 0$ such that
	$\val(\sigma_{i}) =\val(\sigma_{i+1}) = \cdots = r$.

	For the sake of contradiction, assume that $r \geq m$.
	As the execution is infinite but there are only finitely many
	different configurations for a fixed number of agents, there
	exists a configuration $D$ with $D(X) = 0$ and $\val(D) = r$
	that occurs infinitely often in $\sigma$.
	We claim that $D$ can reach a configuration that enables a
	$\mathsf{modulo}$ transition.
	This claim, together with fairness, yields a contradiction because
	the overall value would drop below $r$.

	Let us prove the claim. By \cref{cor:rem:enough:zero}, we have $D \trans{*} D'$
	where $D'$ is clean and $D'(\q{0}) \geq n$.
	Furthermore, $D'(X) = 0$ as $D(X) = 0$ and the number of agents in $X$ cannot be increased.
	By \cref{prop:rem:prop} \eqref{itm:rem:preservation}, we have $D'(B) \geq L(B) = 1$.
	Thus, it suffices to show that $D' \trans{T_{\infty}^*} D''$ for some $D'' \geq \mathrm{rep}(m)$.

	If $\val(D') = m$, then $D'$ contains precisely the binary representation of $m$,
	because $D'$ is clean and $D'(X) = 0$.
	Hence, $D' \geq \mathrm{rep}(m)$. Thus, assume $\val(D') > m$.
	Let $0 \leq d \leq n$ be the largest exponent for which there exists a state
	$q \in P_X$ such that $D(q) > 0$, $\val(q) = 2^d$ and $d \not\in \mathrm{bits}(m)$.
	Since $D'(\q{0}) \geq n \geq d$, the sequence of transitions $\mathsf{down}_d \cdot
	\mathsf{down}_{d-1} \cdots \mathsf{down}_1$ can be fired from $D'$, which yields a
	configuration $D'' \geq \mathrm{rep}(m)$.
\end{proof}

\parag{Main proof} We are now ready to prove that $\PP_{\text{rem}}$
works as intended.

\begin{theorem}
	$\PP_{\text{rem}}$ computes $\varphi$ under reversible dynamic initialization.
\end{theorem}

\begin{proof}
	We first show that $\PP_{\text{rem}}$ is input reversible, and then
	that it correctly computes $\varphi$.

	\medskip\noindent\emph{Input reversibility.} Let $\pi$ be an
	initialization sequence with effective input $\vec{w}$ such that
	$L' \trans{\pi} C$ for some $L' \succeq L$. By
	\cref{prop:rem:prop}~\eqref{itm:rem:preservation:x}, we have $C(I(x)) =
	C(x) = \vec{w}(x) - C(N_x) \leq \vec{w}(x)$ for every $x \in X$,
	which proves the first required property.

	For every configuration $C$, let $\mathrm{false}(C) \defeq D$ where $D(t)
	\defeq 0$, $D(f) \defeq C(t) + C(f)$ and $D(q) \defeq C(q)$ for
	every $q \in Q \setminus \{f, t\}$. Observe that for every
	configuration $C$, the following holds:
	\begin{align}
		C \trans{\mathsf{reset}^{C(\q{t})}} \mathrm{false}(C) \text{ and }
		\mathrm{false}(C) \in [C].\label{eq:rem:reset:false}
	\end{align}
	It remains to show that if $C \trans{\pi_\triangleright \in T^*} D$
	and $D' \in [D]$, then $D' \trans{\pi_\triangleleft \in T^*} C'$ for
	some $C' \in \DiEq{C}$. By~\ref{eq:rem:reset:false}, it is enough to
	argue that $\mathrm{false}(D) \trans{T^*} \mathrm{false}(C)$.

	Let $C_i \trans{t_i} C_{i+1}$ be the $i^\text{th}$ step of
	$\pi_\triangleright$. We argue that $\mathrm{false}(C_{i+1}) \trans{t_i'}
	\mathrm{false}(C_i)$ for some $t_i' \in T \cup \{\varepsilon\}$. By
	induction, this implies $\mathrm{false}(D) \trans{T^*} \mathrm{false}(C)$ as
	desired. If $t_i$ is an $\mathsf{equal}$, $\mathsf{false}$ or
	$\mathsf{reset}$ transition, then we already have $\mathrm{false}(C_{i+1}) =
	\mathrm{false}(C_i)$. Otherwise we revert the step as follows, where ``$s
	\mapsto u$'' indicates that if $t_i = s$, then we reverse it with
	$t_i' = u$:
	\begin{align*}
		\mathsf{add}_x &\mapsto \mathsf{add}_{x,\q{f}}^{-1}
		&& \text{for every $x \in X$,} \\
		%
		\mathsf{add}_{x,q}^{-1} &\mapsto \mathsf{add}_x
		&& \text{for every $x \in X$ and $q \in B$,} \\
		%
		\mathsf{up}_i &\mapsto \mathsf{down}_{i+1}
		&& \text{for every $0 \leq i < n$,}\\
		%
		\mathsf{down}_i &\mapsto \mathsf{up}_{i-1}
		&& \text{for every $0 < i \leq n$,} \\
		%
		\mathsf{modulo}_{q} &\mapsto \mathsf{modulo}_{\q{f}}^{-1}
		&& \text{for every $q \in B$,} \\
		%
		\mathsf{modulo}_{q}^{-1} &\mapsto \mathsf{modulo}_{\q{f}}
		&& \text{for every $q \in B$,}\\
		%
		\mathsf{swap}_{p, q}^x &\mapsto \mathsf{swap}_{q, p}^x
		&& \text{for every $p, q \in N$ and $x \in X$.}
	\end{align*}
	Note that $t_i'$ is not the exact reverse transition of $t_i$, as it
	may differ over $B$. Indeed, $t_i'$ may require an agent in state
	$\q{f}$, which may not have been produced by $t_i$. However, this is
	not an issue since, by definition of $\mathrm{false}$ and by
	\cref{prop:thr:prop}~\eqref{itm:preservation}, we have:
	$$\mathrm{false}(C_{i+1})(\q{f}) = C_{i+1}(B) \geq L(B) > 0.$$ Thus, we have
	$\mathrm{false}(C_{i+1}) \trans{t_i'} \mathrm{false}(C_i)$ as desired, which
	completes the proof.

	\medskip\noindent\emph{Correctness.} Let $\pi$ be an initialization
	sequence with effective input $\vec{w}$ such that $L' \trans{\pi} C$
	for some $L' \succeq L$.
	Let $\sigma$ be a fair execution of $\PP_\infty$ starting from $C$.
	By \cref{prop:remainder:stabilize}, there exist $i \in \N, r \geq 0$ such that:
	\begin{enumerate}[(a)]
		\item $\sigma_i(X) = \sigma_{i+1}(X) = \cdots = 0$, \label{itm:rem:input:stab}

		\item $\val(\sigma_i) = \val(\sigma_{i+1}) = \cdots =
		r < m$. \label{itm:rem:val:stab}
	\end{enumerate}

	Let us first show that $O(\sigma) \in \{0, 1\}$. We make a case distinction on
	whether $v \geq b$.\medskip

	\noindent\emph{Case $r \geq b$.} We show that $O(\sigma) = 1$. Note that $r < m$.
	The $\mathsf{modulo}$ transitions reduce the overall value by $m$.
	As the value of a configuration is never negative, no $\mathsf{modulo}$ transition
	can be fired again.
	Thus, it suffices to show that $\sigma_j(\q{f}) = 0$ for some $j \geq i$.
	If $\sigma_i(\q{f}) = 0$ then we are done.
	For the sake of contradiction, suppose this is not the case.
	As $\sigma$ is infinite but there are only finitely many different configurations
	for a fixed number of agents, there exists a configuration $D$ that occurs infinitely
	often in $\sigma$ such that $D(X) = 0$, $\val(D) = r$ and $D(\q{f}) > 0$.
	We claim that $D$ can reach a configuration that enables the transition $\mathsf{equal}$.
	This claim, together with fairness, yields a contradiction because $\mathsf{equal}$
	can move all agents form state $\q{f}$ to state $\q{t}$.

	Let us prove the claim.
	By \cref{cor:rem:enough:zero}, we have $D \trans{T_{\infty}^*} D'$ where $D'$ is clean and
	$D'(\q{0}) \geq n$.
	Furthermore, $D'(X) = 0$ as $D(X) = 0$ and the number of agents in $X$ cannot be
	increased by transitions in $T_\infty$.
	We show that $D' \trans{*} D''$ for some $D'' \geq \mathrm{rep}(m)$.
	If $\val(D') = m$, then $D'$ contains precisely the binary representation of $m$,
	because $D'$ is clean and $D'(X) = 0$.
	Hence, $D' \geq \mathrm{rep}(m)$. Thus, assume $\val(D') > m$.
	Let $0 \leq d \leq n$ be the largest exponent for which there exists a state $q \in P_X$
	such that $D(q) > 0$, $\val(q) = 2^d$ and $d \not\in \mathrm{bits}(m)$.
	Since $D'(\q{0}) \geq n \geq d$, the sequence of transitions
	$\mathsf{down}_d \cdot \mathsf{down}_{d-1} \cdots \mathsf{down}_1$ can be fired from $D'$,
	which yields a configuration $D'' \geq \mathrm{rep}(m)$.
	If $D''(\q{f}) = 0$, then the claim holds because the only transition that reduces the
	number of agents in state $\q{f}$ is transition $\mathsf{equal}$.
	If $D''(\q{f}) > 0$, then the claim holds because $D''$ enables $\mathsf{equal}$. \medskip

	\noindent\emph{Case $r < b$.} We show that $O(\sigma) = 0$. First note
	that $\mathsf{equal}$ is disabled in $\sigma_j$ for every
	$j \geq i$, as otherwise we would have
	$\sigma_j \geq \mathrm{rep}(b)$ which implies that $r
	= \val(\sigma_j) \geq b$. Thus, it suffices to show that there
	are infinitely many indices $j$ such that $\sigma_j(\q{f}) >
	0$. Indeed, if this is the case, then, by fairness, $\mathsf{false}$
	permanently moves all agents in state $\q{t}$ to state $\q{f}$.

	For the sake of contradiction, suppose the claim does not hold.
	Let $\sigma' \defeq \pi\sigma$. Let $j \in \N$ be the largest index
	such that $\sigma_j'(\q{f}) > 0$.
	Note that this configuration exists as $\sigma_0' = L' \succeq L$ and $L(\q{f}) > 0$.
	The only transition that reduces the number of agents in $\q{f}$ is $\mathsf{equal}$.
	Thus, $\sigma_j' \trans{\mathsf{equal}} \sigma_{j+1}'$ and $\val(\sigma_j') \geq b$.
	As finally, $r < b$, some $\mathsf{modulo}$ or $\mathsf{add}^{-1}$ transition
	must be fired in $\sigma'_{j'}$ for some $j' > j$.
	In both cases there is afterwards an agent in state $\q{f}$.
	This contradicts the maximality of $j$. \medskip

	We are done proving $O(\sigma) \in \{0, 1\}$.
	It remains to argue that $O(\sigma) = \varphi(\vec{w})$.
	We have $m > r = \val(\sigma_i) \equiv_m \vec{a} \cdot \vec{w}$
	by \cref{prop:rem:prop}~\eqref{itm:rem:val:inv}.
	If $\vec{a} \cdot \vec{w} \geq b~(\text{mod } m)$, then $r \geq b$ and
	hence $O(\sigma) = 1$, which is correct.
	If $\vec{a} \cdot \vec{w} < b~(\text{mod } m)$, then $r < b$ and
	hence $O(\sigma) = 0$, which is also correct.
\end{proof}

\section{Proofs of Section \ref{sec:large}: Protocols for large populations} \label{app:large}

\subsection{Proof of Theorem \ref{thm:remove:helpers}}\label{app:rem:helpers}
\input{helpers}

\subsection{Proof of Proposition \ref{prop:mult}}\label{app:mult}
\input{mult}

\subsection{Proof of Theorem \ref{thm:atomic:mult:helpers}}\label{app:atomic:mult}
\input{atomic-parallel}

\subsection{Proof of Theorem \ref{thm:atomic:helpers}}\label{app:threshold}
\input{threshold}
\input{remainder}

\section{Equivalence of simple and standard population protocols} \label{appendix_output}
Recall that a simple population protocol (SPP), has two unique states
$\q{f}, \q{t} \in Q$ with outputs $O(\q{f}) = 0$ and $O(\q{t}) = 1$ and all other states $q$ have output $O(q) = \bot$.

In the standard definition of population protocols used in the literature, all states $q$ have an output
$O(q) \in \{0,1\}$. In this section we call such a protocol a \emph{full output population protocols} (FOPP). In a FOPP,  a configuration $C$ is a consensus configuration if
$O(p) = O(q)$ for every $p, q \in \supp{C}$. If $C$ is a consensus configuration, then its output $O(C)$ is the unique output of its states, otherwise it is $\bot$.
An execution $\sigma = C_0 C_1 \cdots$ stabilizes to $b \in \{0, 1\}$
if $O(C_i) = O(C_{i+1}) = \cdots = b$ for some $i \in \mathbb{N}$.
The output of $\sigma$ is $O(\sigma) = b$ if it stabilizes to $b$, and $O(\sigma)= \bot$ otherwise.
A consensus configuration $C$ is
stable if every configuration $C'$
reachable from $C$ is a consensus configuration such that
$O(C') = O(C)$. It is easy to see that a fair execution of a FOPP stabilizes to $b \in \{0, 1\}$ if and only if it contains a stable configuration whose output is $b$.

A FOPP $\PP$ computes a predicate $\varphi \colon
\N^X \to \{0, 1\}$ if for every $\vec{v} \in \N^X$ every fair
execution $\sigma$ starting from $C_{\vec{v}}$ stabilizes to $\varphi(\vec{v})$.

In the rest of the section we show that every FOPP has an equivalent SPP, and vice versa.
Both translations have linear blow-up.

\parag{FOPP $\rightarrow$ SPP}
Let $\PP = (Q, T, L, X, I, O)$ be a FOPP computing a predicate $\varphi$.  We obtain a SPP protocol $\PP'$ by adding two output states $\{\q{f},\q{t}\}$ to $\PP$, plus a new state $\q{\bot}$.
The output function of $\PP'$ is the mapping $O': q \mapsto (0 \text{ if } q = \q{f} \text{ else } 1
\text{ if } q = \q{t} \text{ else } \bot)$. The set $L'$ of leaders of $\PP'$ is obtained by
adding one leader to $L$, initially in state $\q{\bot}$. Finally, the set $T'$ of transitions is obtained by adding to $T$, for all $b \in \{\q{f},\q{t},\q{\bot}\}$, a transition
$\multiset{q, b} \mapsto \multiset{q, \q{f}}$ for every state $q \in Q$ such that $O(q)=0$ and
a transition $\multiset{q, b} \mapsto \multiset{q, \q{t}}$ for every state $q \in Q$ such that $O(q)=1$.

We show that $\PP'$ also computes $\varphi$.
Let $C'_0 C'_1 \cdots$ be a fair execution of $\PP'$ from $C_0'$. Projecting it onto the set of states of $\PP$ yields a fair execution of $\PP$. Since $\PP$ computes $\varphi$, the execution outputs some $b \in \{0,1\}$. Assume that $b=0$ (the case $b=1$ is symmetric).
Let $i \in \N$ such that the output of every state populated by $C_j$ is $b$ for every $j \geq i$.
Now, no matter the state populated by the additional leader in $C_j$ (which is one of $\{\q{f},\q{t},\q{\bot}\}$), the transition $\multiset{q, b} \mapsto \multiset{q, \q{f}}$
is enabled for every state $q$ such that $C_j(q)=0$. By fairness, the leader will thus eventually move to state $\q{f}$ and it will be stuck there, and $\PP'$ outputs $0$ as well.

\medskip
\parag{SPP $\rightarrow$ FOPP}
Let $\PP = (Q, T, L, X, I, O)$ be an SPP with output states $\q{f}, \q{t} \in Q$ computing a predicate $\varphi$. Let $\PP'$ be the FOPP with two disjoint copies $Q_0,Q_1$ of $Q$ as states. For $a \in Q$, let $a_b$ denote the copy of $a$ in $Q_b$, for $b \in \{0,1\}$.
We define $O'(q)=b$ for all $q \in Q_b$.
The set $T'$ of transitions is the following. First,
for every transition $\multiset{x, y} \mapsto \multiset{z, u}$ of $T$, the set $T'$
contains a transition $\multiset{x_b, y_c} \mapsto \multiset{z_d, u_e}$
for every $b,c,d,e \in \{0,1\}$ such that if $b=c$ then $d=e=b=c$.
Further, $T'$ also contains a set $T''$ of transitions consisting of
$\multiset{\q{f}_1} \mapsto \multiset{\q{f}_0}$,
$\multiset{\q{t}_0} \mapsto \multiset{\q{t}_1}$,
$\multiset{a_1,\q{f}_0} \mapsto \multiset{a_0,\q{f}_0}$
and
$\multiset{a_0,\q{t}_1} \mapsto \multiset{a_1,\q{t}_1}$
for every $a \in Q$.

The input mapping and leader multiset of $\PP'$ are the ``0'' copies of the input mapping and leader multiset of $\PP$.
Hence, for any input $\vec{v}$ the initial configuration $C'_{\vec{v}}$ of $\PP'$ is the ``0'' copy of the initial configuration $C_{\vec{v}}$ in $\PP$.

We show that $\PP'$ also computes $\varphi$. Let $C'_0 C'_1 \cdots$ be a fair execution of $\PP'$ from $C'_0$. For every $i \in \mathbb{N}$, let $C_i=\pi(C'_i)$, where $\pi$ is the mapping defined by $\pi(q_b)=b$ for every $q_b \in Q_0 \cup Q_1$.
It is easy to see that $C_0 C_1 \cdots$
is a fair execution of $\PP$, with possible repetitions $C_i=C_{i+1}$
when the transition from $C'_i$ to $C'_{i+1}$ is in $T''$.
Hence $C_0 C_1 \cdots$ eventually stabilizes to an output $b$.
Assume that $b=0$ (the case $b=1$ is symmetric).
By fairness, because of the transitions
$\multiset{\q{f}_1} \mapsto \multiset{\q{f}_0}$,
and
$\multiset{a_1,\q{f}_0} \mapsto \multiset{a_0,\q{f}_0}$, the execution $C'_0 C'_1 \cdots$ eventually reaches, and gets trapped in, configurations of $\mathbb{N}^{Q_0}$. So the execution also stabilizes to the output $0$.

\section{Proof of Theorem \ref{thm:hardness:PA}} \label{appendix_PA}

\thmHardnessPA*

\begin{proof}
 We show that if such an algorithm runs in time $2^{p(n)}$ for some polynomial $p$, then the validity problem for PA formulas  is in EXPTIME, contradicting the fact that its complexity lies between 2-NEXP and 2-EXPSPACE~\cite{Berman80, Haase14}. Recall that the validity problem for PA formulas asks whether a given sentence, i.e., a formula without free variables, is true or false.

Let $\varphi$ be a sentence of PA, and let $n \defeq |\varphi|$. Consider the formula $\psi(x) \defeq (x \geq 2) \wedge \varphi$ (notice that the smallest possible size of a population is 2). Clearly, $\varphi$ is valid if{}f $\psi(2)$ holds. Assume there exists an algorithm that on input $\psi$ executes at most $f(n)$ steps and outputs a population protocol $\PP$ that computes $\psi$. Clearly, $\PP$ has at most $\O(f(n))$ states, and $\varphi$ is valid if{}f $\PP$ computes 1 for input $x = 2$.

Let $C$ be the initial configuration of $\PP$ for input $x = 2$. A configuration of $\PP$ with two agents can be stored in space $\O(\log f(n))$, and so $C$, and every configuration reachable from it, can be stored using $\O(\log f(n))$ space. Protocol $\PP$ computes $1$ from $C$ if{}f there exists a configuration $C'$ such that:
\begin{enumerate}[(i)]
\item $C \trans{*} C'$,

\item $C'$ has output 1,

\item for every configuration $C''$, if  $C' \trans{*} C''$, then $C'' \trans{*} C'$.
\end{enumerate}

Observe that (i)-(iii) can be expressed in FO(TC), \ie\ first-order logic with transitive-closure. By Immermann's theorem, deciding (i)-(iii) belongs to NSPACE($\log f(n)$)~\cite{Immerman99}, and so it can be solved in $\O(f(n)^k)$ deterministic time for some $k \geq 1$. Consequently, if there exists a polynomial $p$ such that $f \in \O(2^{p(n)})$, then the validity of $\varphi$ can be decided in time $2^{\O(p(n))}$, and so the validity problem for PA is in EXPTIME. The latter is impossible by the time hierarchy theorem.
\end{proof}

\section{Proofs of Section \ref{sec:small}: Protocols for small populations} \label{app:small}

\subsection{Proof of Theorem \ref{thm:removing:leaders}}
\input{construction-leaderless-small}

\subsection{Proof of Theorem \ref{lemma:halting-conj-disj}} \label{app:construction-halting-conj-dis}
\input{construction-halting-conj-dis}

\subsection{Proof of Theorem \ref{thm:halting:threshold}}\label{app:constr-halting-threshold}
\input{construction-halting-threshold}

\subsection{From protocols with helpers to leaderless protocols}
\label{subsec:helpers}

Intuitively, a protocol with helpers is a protocol with leaders satisfying an additional
property: adding more leaders does not change the predicate computed
by the protocol. Formally, let $\PP = (Q, T, L, X, I, O)$ be a population
protocol computing a predicate $\varphi$. We say that $\PP$ is a
protocol \emph{with helpers} if for every $L' \succeq L$ the protocol
$\PP' = (Q, T, L', X, I, O)$ also computes $\varphi$, where $L'
\succeq L \; \defeq \; \forall q \in Q \colon (L'(q) = L(q)=0 \vee
L'(q) \geq L(q) > 0)$. If $|L| = \cutoffvar$, then we say that $\PP$ is a protocol \emph{ with $\cutoffvar$ helpers}.

\begin{restatable}{theorem}{thmRemoveHelpers} \label{thm:remove:helpers}
  Let $\PP = (Q, T, L, X, I, O)$ be a
  $\kwayvar$-way population protocol with $\cutoffvar$-helpers
  computing some predicate $\varphi$. There exists a 2-way leaderless
  population protocol with $\O(\cutoffvar \cdot |X| + (\kwayvar \cdot |T|+|Q|)^2)$ states that computes $(|\vec{v}|  \geq \cutoffvar) \rightarrow \varphi(\vec{v})$.
\end{restatable}

\begin{proof}[Proof sketch]
  By~\cite[Lemma~3]{BEJ18}, $\PP$ can be transformed into a 2-way
  population protocol (with helpers\footnote{Lemma~3 of~\cite{BEJ18}
    deals with leaders and not the more specific case of
    helpers. Nonetheless, computation under helpers is preserved as
    the input mapping of $\PP$ remains unchanged in the proof of the
    lemma.})  computing the same predicate $\varphi$, and with at most
  $|Q| + 3\kwayvar \cdot |T|$ states. Thus, we assume $\PP$ to be 2-way in
  the rest of the sketch.

  For simplicity, assume $X = \{x\}$ and $L = \multiset{3 \cdot q, 5
    \cdot q'}$; that is, $\PP$ has 8 helpers, and initially 3 of them
  are in state $q$, and $5$ are in $q'$. We describe a leaderless
  protocol $\PP'$ that simulates $\PP$ for every input $\vec{v}$ such
  that $|\vec{v}| \geq |L| = \cutoffvar$. Intuitively, $\PP'$ runs in two phases:
  \begin{itemize}
  \item In the first phase each agent gets assigned a number between 1
    and 8, ensuring that each number is assigned to at least one agent
    (this is the point at which the condition
	 $|\vec{v}| \geq \cutoffvar$ is needed).
	 At the end of the phase, each agent is in a state of the
    form $(x, i)$, meaning that the agent initially represented one
    unit of input for variable $x$, and that it has been assigned
    number $i$.  To achieve this, initially every agent is placed in
    state $(x, 1)$. Transitions are of the form $ \multiset{ (x, i),
      (x, i)} \mapsto \multiset{ (x, i+1), (x, i)}$ for every $1 \leq
    i \leq 7$. The transitions guarantee that all but one agent is
    promoted to $(x, 2)$, all but one to $(x, 3)$, etc. In other
    words, one agent is ``left behind'' at each step.

  \item In the second phase, an agent's state is a multiset:
    agents in state $(x, i)$ move to state
    $\multiset{I(x), q}$ if $1 \leq i \leq 3$, and to state
    $\multiset{I(x), q'}$ if $4 \leq i \leq 8$.  Intuitively, after
    this move each agent has been assigned two jobs: simultaneously
    simulate a regular agent of $\PP$ starting at state $x$,
    \emph{and} a helper of $L$ starting at state $q$ or $q'$. Since in
    the first phase each number is assigned to at least one agent,
    $\PP'$ has at least 3 agents simulating helpers in state $q$, and
    at least 5 agents simulating helpers in state $q'$. There may be
    many more helpers, but this is harmless, because, by definition,
    additional helpers do not change the computed
    predicate. \smallskip

    The transitions of $\PP'$ are designed according to this double
    role of the agents of $\PP'$. More precisely, for all multisets
    $\vec{p}, \vec{q}, \vec{p}', \vec{q}'$ of size two,
    $\multiset{\vec{p}, \vec{q}} \mapsto \multiset{\vec{p}',
      \vec{q}'}$ is a transition of $\PP'$ if{}f $(\vec{p} + \vec{q})
    \trans{} (\vec{p}' + \vec{q}')$ in $\PP$.
    \qedhere
  \end{itemize}
\end{proof}

\subsection{From multi-output protocols to protocols with helpers}
\label{subsec:finsets}

A \emph{$k$-output population protocol} is a tuple $\mathcal{Q} = (Q,
T, L, X, I, O)$ where $O \colon [k] \times Q \to \{0, 1, \bot\}$ and
$\mathcal{Q}_i \defeq (Q, T, L, X, I, O_i)$ is a population protocol
for every $i \in [k]$, where $O_i$ denotes the mapping such that
$O_i(q) \defeq O(i, q)$ for every $q \in Q$. Intuitively, since each
$\mathcal{Q}_i$ only differs by its output mapping, $\mathcal{Q}$ can
be seen as a single population protocol whose executions have $k$
outputs. More formally, $\mathcal{Q}$ \emph{computes} a set of
predicates $P = \{\varphi_1, \varphi_2, \ldots, \varphi_k\}$ if
$\mathcal{Q}_i$ computes $\varphi_i$ for every $i \in
[k]$. Furthermore, we say that $\mathcal{Q}$ is \emph{simple} if
$\mathcal{Q}_i$ is simple for every $i \in [k]$. Whenever the number
$k$ is irrelevant, we use the term \emph{multi-output population
  protocol} instead of $k$-output population protocol.

\begin{restatable}{proposition}{PropMult}
\label{prop:mult}
Assume that every finite set $A$ of {\em atomic} predicates is computed by some
$|A|$-way multi-output protocol with $\O(|A|^3)$ helpers and states, and
$\O(|A|^5)$ transitions. Every
QFPA predicate $\varphi$ is computed by some
simple $|\varphi|$-way protocol with
$\O(|\varphi|^3)$ helpers and states, and
$\O(|\varphi|^5)$ transitions.
\end{restatable}

\begin{proof}[Proof sketch]
Consider a binary tree decomposing the boolean operations of $\varphi$.
We design a protocol for $\varphi$ by induction on the height of the tree.

The case where the height is $0$, and $\varphi$ is atomic, is trivial.
We sketch the induction step for the case where the root is labeled with $\land$, that is $\varphi = \varphi_1 \land \varphi_2$, the other cases are similar.
By induction hypothesis, we have simple protocols $\PP_1,\PP_2$ computing $\varphi_1,\varphi_2$, respectively. Let $\q{t}_j,\q{f}_j$ be the output states of $\PP_j$ for $j \in \{1,2\}$ such that $O_j(\q{t}_j) = 1$ and $O_j(\q{f}_j) = 0$. We add two new states $\q{t}, \q{f}$ (the output states of the new protocol) and an additional helper starting in state $\q{f}$. To compute $\varphi_1 \land \varphi_2$ we add the following transitions for every $b_1 \in \{\q{t}_1,\q{f}_1\}, b_2 \in \{\q{t}_2,\q{f}_2\}$, and $b \in \{\q{t},\q{f}\}$:
$\multiset{b_1,b_2,b} \mapsto \multiset{b_1,b_2,\q{t}}$ if $b_1 = \q{t}_1 \land b_2 = \q{t}_2$, and $\multiset{b_1,b_2,b} \mapsto \multiset{b_1,b_2,\q{f}}$ otherwise.
The additional helper computes the conjunction as desired.
\end{proof}

\subsection{From reversible dynamic initialization to multi-output protocols}
\label{subsec:finat}

Let $P = \{\varphi_1, \ldots, \varphi_k\}$ be a set of $k \geq 2$
atomic predicates of arity $n \geq 1$ over a set $X = \{x_1, \ldots, x_n\}$ of variables.
We construct a multi-output protocol $\PP$ for $P$ of size
$\poly(|\varphi_1|+ \cdots + |\varphi_k|)$.

Let $\PP_1, \ldots, \PP_k$ be protocols for
$\varphi_1, \ldots, \varphi_k$. Observe that $\PP$ cannot be a ``product protocol'' that executes $\PP_1, \ldots, \PP_k$ synchronously. Indeed, the states of such a $\PP$ are tuples $(q_1, \ldots, q_k)$ of states of $\PP_1, \ldots, \PP_k$,  and so $\PP$ would have exponential size in $k$.
Further, $\PP$ cannot execute $\PP_1, \ldots, \PP_k$  asynchronously in parallel, because, given an input $\vec{x} \in \N^n$, it must dispatch $k \cdot \vec{x}$ agents ($\vec{x}$ to the input states of each $\PP_j$), but it only has $\vec{x}$.
Such a $\PP$ would need $(k-1)|\vec{x}|$ helpers, which is not possible, because a protocol of size  $\poly(|\varphi_1|+ \cdots + |\varphi_k|)$ can only use $\poly(|\varphi_1|+ \cdots + |\varphi_k|)$ helpers, whatever the input $\vec{x}$.

The solution is to use a more sophisticated parallel asynchronous computation. Consider two copies of inputs, denoted
$\overline{X} = \{\overline{x}_1, \ldots, \overline{x}_n\}$ and $\underline{X} = \{\underline{x}_1, \ldots, \underline{x}_n\}$.
For each predicate $\varphi$ over $X$,
consider predicate $\tilde{\varphi}$ over
$\overline{X} \cup \underline{X}$
satisfying $\tilde{\varphi}(\overline{\vec{x}},\underline{\vec{x}}) =
\varphi(k\overline{\vec{x}}+\underline{\vec{x}})$
for every $(\overline{\vec{x}},\underline{\vec{x}}) \in \N^{\overline{X} \cup \underline{X}}$.
We obtain
$\tilde{\varphi}(\overline{\vec{x}},\underline{\vec{x}}) =
\varphi(\vec{x})$ whenever $k \overline{\vec{x}} + \underline{\vec{x}} = \vec{x}$, \eg\ for
$\overline{\vec{x}}:=  {\lfloor}\frac{{\vec{x}}}{k}{\rfloor}$ and $\underline{\vec{x}} :=\rem{{\vec{x}}}{k}$.
With this choice, $\PP$ needs to dispatch a total of
$k \left( |\overline{\vec{x}} + \underline{\vec{x}}| \right)
\leq |\vec{x}| + n \cdot (k-1)^2$
agents to compute $\tilde{\varphi}_1(\overline{\vec{x}},\underline{\vec{x}}), \ldots, \tilde{\varphi}_k(\overline{\vec{x}},\underline{\vec{x}})$.
That is, $n \cdot (k-1)^2$ helpers are sufficient to compute $\PP$.
Formally, we define $\tilde{\varphi}$ in the following way:

\begin{quote}
For $\displaystyle \varphi(\vec{x}) = \left(\sum_{i=1}^n \alpha_i x_i > \beta \right)$, we define $\displaystyle \tilde{\varphi}(\overline{\vec{x}}, \underline{\vec{x}}) := \left(\sum_{i=1}^n (k \cdot \alpha_i) \overline{x}_i + \alpha_i\underline{x}_i > \beta \right)$
\end{quote}
\noindent and similarly for modulo predicates.
For instance, if $\varphi(x_1,x_2)=3 x_1 - 2x_2 > 6$
and $k=4$, then $\tilde{\varphi}(\overline{x}_1,\underline{x}_1,\overline{x}_2,\underline{x}_2)=12 \overline{x}_1 + 3 \underline{x}_1 -
8 \overline{x}_2 - 2 \underline{x}_2 > 6$.
As required, $\tilde{\varphi}(\overline{\vec{x}},\underline{\vec{x}})=
\varphi(k\overline{\vec{x}}+\underline{\vec{x}})$.

Let us now describe how
the protocol $\PP$ computes $\tilde{\varphi}_1(\overline{\vec{x}}, \underline{\vec{x}}), \ldots, \tilde{\varphi}_k(\overline{\vec{x}}, \underline{\vec{x}})$.
Let $\tilde{\PP}_1, \ldots, \tilde{\PP}_k$ be protocols computing $\tilde{\varphi}_1, \ldots, \tilde{\varphi}_k$.
Let $X= \{\q{x_1}, \ldots, \q{x_n}\}$ be the input states of $\PP$,
and let
$\q{\overline{x}^j_1}, \ldots, \q{\overline{x}^j_n}$ and $\q{\underline{x}^j_1}, \ldots, \q{\underline{x}^j_n}$ be the input states of $\tilde{\PP}_j$
for every $1 \leq j \leq k$.
Protocol $\PP$
repeatedly chooses an index $1 \leq i \leq n$, and executes one of these two actions: (a)~take $k$ agents from $\q{x_i}$, and dispatch them to $\q{\overline{x}^1_i}, \ldots, \q{\overline{x}^k_i}$ (one agent to each state); or (b)~take one agent from $\q{x_i}$ and $(k-1)$ helpers, and dispatch them to $\q{\underline{x}^1_i}, \ldots, \q{\underline{x}^k_i}$. The index and the action are chosen nondeterministically.
Notice that if
for some input $\q{x}_i$,
all $\ell$ agents of $\q{x_i}$ are dispatched, then
$k \q{\overline{x}^j_i} + \q{\underline{x}^j_i}=\ell$ for all $j$.
If all agents of $\q{x_i}$ are dispatched for every $1 \leq i \leq n$, then we say that the {\em dispatch is correct}.

The problem is that, because of the nondeterminism,
the dispatch may or may not be correct.
Assume, \eg, that $k=5$ and $n=1$. Consider the input $x_1=17$, and assume that $\PP$ has $n \cdot (k-1)^2=16$ helpers. $\PP$ may correctly dispatch
$\overline{x}_1 =  {\lfloor}\frac{17}{5}{\rfloor}=3$ agents to each of $\q{\overline{x}^1_1}, \ldots, \q{\overline{x}^1_5}$
and $\underline{x}_1 = (\rem{17}{5})=2$ to each of $\q{\underline{x}^1_1}, \ldots, \q{\underline{x}^1_5}$; this gives a total of $(3+2)\cdot 5 = 25$ agents, consisting of the $17$ agents for the input plus $8$
helpers. However, it may also wrongly dispatch $2$ agents to each of $\q{\overline{x}^1_1}, \ldots, \q{\overline{x}^1_5}$ and
$4$ agents to each of $\q{\underline{x}^1_1}, \ldots, \q{\underline{x}^1_5}$, with a total of $(2+4) \cdot 5 = 30$ agents, consisting of $14$ input agents plus $16$ helpers. In the second case, each $\PP_j$
wrongly computes $\tilde{\varphi}_j(2, 4) = \varphi_j(2\cdot 5 + 4) = \varphi_j(14)$, instead of the correct value $\varphi_j(17)$.

To solve this problem we ensure that $\PP$ can always recall agents already dispatched
to $\tilde{\PP}_1, \ldots, \tilde{\PP}_k$ as long as the dispatch is not yet correct.
This allows $\PP$ to ``try out'' dispatches until it dispatches correctly, which eventually happens by fairness.
For this we design $\PP$ so that (i) the atomic protocols $\tilde{\PP}_1, \ldots, \tilde{\PP}_k$ can work with inputs agents that arrive over time ({\em dynamic initialization}), and (ii) $\tilde{\PP}_1, \ldots, \tilde{\PP}_k$ can always return to their initial configuration and send agents back to $\PP$, unless the  dispatch is correct ({\em reversibility}).
To ensure that $\PP$ stops redistributing after dispatching a correct distribution, it suffices to replace each reversing transition $\vec{p} \mapsto \vec{q}$ by transitions $\vec{p} + \multiset{\q{x_i}} \mapsto \vec{q} + \multiset{\q{x_i}}$, one for each $1 \leq i \leq n$: All these transitions become disabled when $\q{x_1}, \ldots, \q{x_n}$ are not populated.

\parag{Reversible dynamic initialization} Let us now formally introduce the class of \emph{protocols with reversible dynamic initialization} that enjoys all properties needed for our construction. A simple protocol with \emph{reversible dynamic initia\-li\-zation} (\emph{RDI-protocol} for short) is a tuple $\PP = (Q, T_\infty, T_\dagger, L, X, I , O)$, where $\PP_\infty = (Q, T_\infty, L, X, I , O)$ is a simple population protocol, and $T_\dagger$ is the set of transitions making the system reversible, called the \emph{RDI-transitions}.

Let $T \defeq T_\infty \cup T_\dagger$, and let $\mathsf{In} \defeq \{\mathsf{in}_x
: x \in X\}$ and $\mathsf{Out} \defeq \{\mathsf{out}_x : x \in X\}$ be the sets of
\emph{input} and \emph{output transitions}, respectively, where
$\mathsf{in}_x \defeq (\vec{0}, \multiset{I(x)})$ and $\mathsf{out}_x \defeq
(\multiset{I(x)}, \vec{0})$. An \emph{initialization sequence} is a
finite execution $\pi \in \left( T \cup \mathsf{In} \cup \mathsf{Out}\right)^*$ from
the \emph{initial configuration} $L'$ with $L' \succeq L$. The \emph{effective input} of
$\pi$ is the vector $\vec{w}$ such that $\vec{w}(x) \defeq
|\pi|_{\mathsf{in}_x} - |\pi|_{\mathsf{out}_x}$ for every $x \in X$. Intuitively, a
RDI-protocol starts with helpers only, and is dynamically initialized
via the input and output transitions.

\newcommand{\DiEq}[1]{\left[#1\right]}

Let $\q{f}, \q{t} \in Q$ be the unique states of $\PP$ with $O(\q{f}) = 0$ and
$O(\q{t}) = 1$. For every configuration $C$, let $\DiEq{C} \defeq \left\{C' : C'(\q{f}) + C'(\q{t}) = C(\q{f}) + C(\q{t}) \text{ and }
C'(q) = C(q) \text{ for all } q \in Q \setminus \{\q{f}, \q{t}\} \right\}$. Intuitively, all configurations $C' \in
\DiEq{C}$ are equivalent to $C$ in all but the output states.

An RDI-protocol is required to be \emph{reversible}, that is
for every initialization sequence $\pi$ with effective input $\vec{w}$,
and such that $L' \trans{\pi} C$ for some $L' \succeq L$, the following holds:
\begin{itemize}
\item if $C \trans{T^*} D$ and $D' \in \DiEq{D}$, then $D' \trans{T^*} C'$ for some $C' \in \DiEq{C}$, and

\item $C(I(x)) \leq \vec{w}(x)$ for all $x \in X$.
\end{itemize}
Intuitively, an RDI-protocol can never have more agents in an input state than the effective number of agents it received via the input and output transitions.
Further, an RDI-protocol can always reverse all sequences that do not contain input or output transitions.
This reversal does not involve the states $\q{f}$ and $\q{t}$, which have a special role as output states. Since RDI-protocols have a default output, we need to ensure that the default output state is populated when dynamic initialization ends, and reversal for $\q{f}$ and $\q{t}$ would prevent that.

An RDI-protocol $\PP$ \emph{computes} $\varphi$ if for every initialization sequence $\pi$ with effective input $\vec{w}$ such that $L' \trans{\pi} C$ for some $L' \succeq L$, the standard population protocol $\PP_\infty$ computes $\varphi(\vec{w})$ from $C$ (that is with $T_\dagger$ disabled). Intuitively, if the dynamic initialization terminates, the RDI-transitions $T_\dagger$ become disabled, and then the resulting standard protocol $\PP_\infty$ converges to the output corresponding to the dynamically initialized input.

\begin{restatable}{theorem}{thmAtomicMultHelpers} \label{thm:atomic:mult:helpers}
Assume that for every atomic predicate $\varphi$, there exists a
$|\varphi|$-way RDI-protocol with
$\O(|\varphi|)$ helpers,
$\O(|\varphi|^2)$ states and
$\O(|\varphi|^3)$ transitions
that computes $\varphi$.
For every finite set  $P$ of atomic predicates, there exists a $|P|$-way
simple {\em multi-output} protocol, with
$\O(|P|^3)$  helpers and states, and
$\O(|P|^5)$ transitions, that computes $P$.
\end{restatable}

\subsection{Atomic predicates under reversible dynamic initialization}
\label{subsec:findyn}

Lastly, we show that atomic predicates are succinctly computable
by RDI-protocols:

\begin{restatable}{theorem}{thmAtomicHelpers} \label{thm:atomic:helpers}
Every atomic predicate $\varphi$ over variables $X$ can be computed by a simple $|\varphi|$-way population protocol with reversible dynamic initialization that has
$\O(|\varphi|)$ helpers,
$\O(|\varphi|^2)$ states, and
$\O(|\varphi|^3)$
transitions.
\end{restatable}

\begin{figure}[htb]
	\vspace*{-15pt}
	\centering\input{fig-remainder}%
	\vspace*{-6pt}
	\caption{Partial representation of the protocol computing $5x + 6y
		\geq 4 \pmod{7}$ as a Petri net, where places (circles), transitions
		(squares) and tokens (smaller filled circles) represent
		respectively states, transitions and agents. Non-helper agents
		remember their input variable (labeled here within tokens).
		The depicted configuration is obtained from input $x = 2$, $y = 1$ by
		firing the bottom leftmost transition (dark blue).}\label{fig:petri:remainder}
\end{figure}

The protocols for arbitrary threshold and remainder predicates satisfying the conditions
of \cref{thm:atomic:helpers}, and their correctness proofs, are given in \Cref{app:threshold}. Note that the threshold
protocol is very similar to the protocol for linear inequalities given in Section 6 of \cite{BEJ18}. Thus, as an
example, we will instead describe how to handle the remainder predicate $5x - y \equiv_7 4$. Note, that the
predicate can be rewritten as $\left(5x + 6y \geq 4 \pmod{7}\right)\land \left(5x + 6y \not\geq 5
\pmod{7}\right)$. As we can handle negations and conjunctions separately in \cref{subsec:finsets}, we will now
explain the protocol for $\varphi \defeq 5x + 6y \geq 4 \pmod{7}$. The protocol is partially depicted in
\cref{fig:petri:remainder} using Petri net conventions for the graphical representation.

The protocol has an \emph{input state} $\q{x}$ for each variable $x \in X$,
\emph{output states} $\q{f}$ and $\q{t}$, a \emph{neutral state} $\q{0}$, and
\emph{numerical states} of the form $\q{+2^i}$ for every $0 \leq i
\leq n$, where $n$ is the smallest number such that $2^n > \norm{\varphi}$.
Initially, (at least) one helper is set to $\q{f}$ and (at least) $2n$ helpers set to $\q{0}$.
In order to compute $5x + 6y \geq 4 \pmod{7}$ for $x:= r$ and $y:= s$, we
initially place $r$ and $s$ agents in the states $\q{x}$ and $\q{y}$, i.e.,
the agents in state $\q{x}$ encode the number $r$ in unary, and similarly for $\q{y}$.
The blue transitions on the left of \cref{fig:petri:remainder} ``convert'' each agents in input states to a binary
representation of their corresponding coefficient.
In our example, agents in state $\q{x}$ are converted to $\vec{a}(x) = 5 = 0101_2$ by putting one agent in $\q{4}$ and another one in $\q{1}$.
Since two agents are needed to encode $5$, the transition ``recruits'' one helper from state $\q{0}$.
Observe that, since the inputs can be arbitrarily large, but a protocol can only use a constant number of helpers, the protocol must reuse helpers in order to convert all agents in input states.
This happens as follows.
If two agents are in the same power of two, say $\q{+2^i}$, then one of them can be ``promoted'' to $\q{+2^{i+1}}$, while the other one moves to state $\q{0}$, ``liberating'' one helper.
This allows the agents to represent the overall value of all converted agents in the most efficient representation.
That is, from any configuration, one can always reach a configuration where there is at most one agent in each place $2^0, \ldots, 2^{n-1}$, there are at most the number of agents converted from input places in place $2^n$, and hence there are at least $n$ agents in place $0$, thus ready to convert some agent from the input place.
Similar to promotions, ``demotions'' to smaller powers of two can also happen.
Thus, the agents effectively shift through all possible binary representations of the overall value of all converted agents.
The $\equiv_7$ transition in \cref{fig:petri:remainder} allows 3 agents in states $\q{4}$, $\q{2}$ and $\q{1}$ to ``cancel out'' by moving to state $\q{0}$, and it moves the
output helper to $\q{f}$.
Furthermore, there are RDI-transitions that allow to revert the effects of conversion and cancel transitions.
These are not shown in \cref{fig:petri:remainder}.

We have to show that this protocol computes $\varphi$ under reversible dynamic initialization.
First note, that while dynamic initialization has not terminated, all transitions have a corresponding reverse transition.
Thus, it is always possible to return to wrong initial configurations.
However, reversing the conversion transitions can create more agents in input states than the protocol effectively received.
To forbid this, each input agent is ``tagged'' with its variable (see tokens in \cref{fig:petri:remainder}).
Therefore, in order to reverse a conversion transitions, the original input agent is needed.
This implies, that the protocol is reversible.

Next, we need to argue that the protocol without the RDI-transitions computes $\varphi$ once the dynamic
initialization has terminated.
The agents will shift through the binary representations of the overall value.
Because of fairness, the $\equiv_7$ transition will eventually reduce the overall value to at most $6$.
There is a $\geq 4$-transition which detects the case where the final value is at least $4$ and moves the output helper from $\q{f}$ to state $\q{t}$. Notice that whenever transition $\equiv_7$ occurs, we reset the output by moving the output helper to state $\q{f}$.

\subsection{From fixed-sized protocols with one leader to leaderless protocols}
\label{subsec:fixedsize}

\renewcommand{\cond}[2]{( #1 \mid #2 )}

We now define when a population protocol computes a predicate {\em for inputs of a fixed size}.
Intuitively,
it should compute the correct value for every initial configurations of this size;
for inputs of other sizes, the protocol may converge to the wrong result, or may not converge.

\begin{definition}
Let $\varphi$ be a predicate and let $i \geq 2$.
A protocol $\PP$ \emph{computes $\varphi$ for inputs of size $i$}, denoted \emph{``$\PP$ computes $\cond{\varphi}{i}$}'', if for every input $\vec{v}$ of size $i$, every fair execution of $\PP$ starting at $C_{\vec{v}}$ stabilizes to $\varphi(\vec{v})$.
\end{definition}

We show that if, for each small number $i$, some succinct protocol computes $\cond{\varphi}{i}$, then there is a single succinct protocol that computes $\varphi$ for all small inputs.

\begin{restatable}{theorem}{propRemovingLeaders}\label{thm:removing:leaders}
Let $\varphi$ be a predicate over a set of variables $X$, and let $\cutoffvar \in \N$.
Assume that for every $i \in \{2,3, \ldots, \cutoffvar-1\}$, there exists a protocol with at most one leader and at most $m$ states that computes $\cond{\varphi}{i}$. Then, there is a leaderless population protocol with $\O(\cutoffvar^4 \cdot m^2 \cdot |X|^3)$ states that computes $(\vec{x} <  \cutoffvar) \rightarrow \varphi(\vec{x})$.
\end{restatable}

\begin{proof}[Proof sketch]
Fix a predicate $\varphi$ and $\cutoffvar \in \N$. For every
$2 \leq i < \cutoffvar$, let $\PP_i$ be a protocol computing
$\cond{\varphi}{i}$. We describe the protocol $\PP=(Q, T, X, I, O)$ that computes $(\vec{x} \geq \cutoffvar) \lor \varphi(\vec{x}) \equiv (\vec{x} <  \cutoffvar) \rightarrow \varphi(\vec{x})$.
The input mapping $I$ is the identity. During the computation, agents never forget their initial state -- that is, all successor states of an agent are annotated with their initial state. The protocol initially performs a leader election. Each provisional leader stores how many agents it has ``knocked out'' during the leader election in a counter from $0$ to $\cutoffvar-1$. After increasing the counter to a given value $i<\cutoffvar$, it resets the state of $i$ agents and itself to the corresponding initial state of $\PP_{i+1}$, annotated with $X$, and initiates a simulation of $\PP_{i+1}$.
    When the counter of an agent reaches $\cutoffvar-1$, the agent knows that the population size must be $\geq \cutoffvar$, and turns the population into a permanent $1$-consensus.
    Now, if the population size $i$ is smaller than $\cutoffvar$, then eventually a leader gets elected who resets the population to the initial population of $\PP_i$. Since $\PP_i$ computes $\cond{\varphi}{i}$, the simulation of $\PP_i$ eventually yields the correct output.
\end{proof}

\subsection{Computing boolean combinations of predicates for fixed-size inputs}
\label{subsec:halting}

We want to produce a population protocol $\PP$
for a boolean combination $\varphi$ of atomic predicates $(\varphi_i)_{i \in [k]}$ for which we have population protocols $(\PP_i)_{i \in [k]}$.
As in Section~\ref{subsec:finat}, we cannot use a standard ``product protocol'' that executes $\PP_1, \ldots, \PP_k$ synchronously because
the number of states would be exponential in $k$.
Instead, we want to simulate the \emph{concatenation} of
$(\PP_i)_{i \in [k]}$. However, this is only possible if for all $i \in [k]$, the executions of $\PP_i$ eventually ``halt'', i.e.
some agents are eventually certain that the output of the protocol
will not change anymore, which is not the case in general population protocols.
For this reason we restrict our attention to ``halting'' protocols.

\begin{definition}
Let $\PP$ be a simple protocol with output states $\q{f}$ and $\q{t}$. We say that $\PP$ is a \emph{halting protocol} if every configuration $C$ reachable from an initial configuration satisfies:
\begin{itemize}
\item $C(\q{f}) = 0 \lor C(\q{t}) = 0$,

\item $C \trans{*} C' \land C(q) > 0 \Rightarrow C'(q) > 0$ for every $q \in \{\q{f}, \q{t}\}$ and every configuration $C'$.
\end{itemize}
\end{definition}

Intuitively, a halting protocol is a simple protocol in which states $\q{f}$ and $\q{t}$ behave like ``final states'': If an agent reaches $q \in \{\q{f}, \q{t}\}$, then the agent stays in $q$ forever.
In other words, the protocol reaches consensus $0$ (resp.\ $1$) if{}f an agent ever reaches $\q{f}$ (resp.\ $\q{t}$).

\begin{restatable}{theorem}{thmHaltingConjDis}\label{lemma:halting-conj-disj}
Let $k, i \in \N$.
Let $\varphi$ be a boolean combination of atomic predicates $(\varphi_j)_{j \in [k]}$.
Assume that for every $j \in [k]$, there is a  simple halting  protocol $\PP_j=(Q_j, L_j, X, T_j, I_j, O_j)$ with one leader computing $\cond{\varphi_j}{i}$. Then there exists
a simple halting protocol $\PP$ that computes $\cond{\varphi}{i}$,
with one leader and $\mathcal{O}\left(|X| \cdot  \left(\len(\varphi) +|Q_1| + \ldots + |Q_k|\right) \right)$ states.
\end{restatable}

\begin{proof}[Proof sketch]
\newcommand{\pres}[1]{\text{pres}(#1)}
We only sketch the construction
for $\varphi=\varphi_1 \wedge \varphi_2$.
The main intuition is that, since $\PP_1$ and $\PP_2$ are halting, we can construct a protocol that, given an input $\vec{v}$, first simulates $\PP_1$ on $\vec{v}$, and, after $\PP_1$ halts, either halts if $\PP_1$ converges to $0$, or simulates $\PP_2$ on $\vec{v}$ if $\PP_1$ converges to $1$.
Each agent remembers in its state the input variable it corresponds to, in order to simulate $\PP_2$ on $\vec{v}$.
\end{proof}

\subsection{Computing atomic predicates for fixed-size inputs}
\label{subsec:atomic}

We describe a halting protocol that computes a given threshold predicate for fixed-size inputs.

\begin{restatable}{theorem}{thmHaltingThreshold}\label{thm:halting:threshold}
Let $\varphi(\vec{x}, \vec{y}) \defeq  \vec{\alpha} \cdot \vec{x} - \vec{\beta}\cdot \vec{y} > 0$.
For every $i \in \N$, there exists a halting protocol with one leader and $\O(i^2 (|\varphi| + \log i)^3)$
states that computes $\cond{\varphi}{i}$.
\end{restatable}

\newcommand{\GreaterSum}{\sf{Greater}\text{-}\sf{Sum}}

\noindent We first describe a sequential algorithm $\GreaterSum(\vec{x}, \vec{y})$, that
for every input $\vec{x}, \vec{y}$ satisfying $|\vec{x}|+|\vec{y}|=i$
decides whether $\vec{\alpha} \cdot \vec{x} - \vec{\beta}\cdot \vec{y} > 0$ holds. Then we simulate $\GreaterSum$
by means of a halting protocol with $i$ agents.

Since each agent can only have $\O(\log i + \log |\varphi|)$ bits of memory (the logarithm of the number of states),
$\GreaterSum$ must use at most $\O(i \cdot (\log i + \log |\varphi|))$ bits of memory, otherwise it cannot be
simulated by the agents. Because of this requirement, $\GreaterSum$ cannot just compute, store, and then compare
$\vec{\alpha} \cdot \vec{x}$ and $\vec{\beta}\cdot \vec{y}$; this uses too much memory.

$\GreaterSum$ calls procedures $\textit{Probe}_1(j)$ and $\textit{Probe}_2(j)$ that return the $j$-th bits of
$\vec{\alpha} \vec{x}$ and $\vec{\beta} \vec{y}$,  respectively, where $j=1$ is the most significant bit. Since $|\vec{x}| \leq  i$,
and the largest constant in $\vec{\alpha}$ is  at most $||\varphi||$, we have $\vec{\alpha} \cdot \vec{x} \leq i \cdot ||\varphi||$, and so
$\vec{\alpha} \cdot \vec{x}$ has at most $m \defeq |\varphi|+\lfloor\log(i)\rfloor+1$ bits, and the same holds for $\vec{\beta} \vec{y}$.
So we have $ 1 \leq j \leq m$.  Let us first describe $\GreaterSum$, and then  $\textit{Probe}_1(j)$; the procedure $\textit{Probe}_2(j)$ is similar.

$\GreaterSum(\vec{x}, \vec{y})$ loops through $j=1, \ldots, m$. For each $j$, it calls $\textit{Probe}_1(j)$ and $\textit{Probe}_2(j)$.
If $\textit{Probe}_1(j)>\textit{Probe}_2(j)$, then it answers $\varphi(\vec{x}, \vec{y})=1$, otherwise it moves to $j+1$.
If $\GreaterSum$ reaches the end of the loop, then it answers $\varphi(\vec{x}, \vec{y})=0$. Observe that
 $\GreaterSum$ only needs to store the current value of $j$ and the bits returned by $\textit{Probe}_1(j)$ and $\textit{Probe}_2(j)$.
 Since $j \leq m$, $\GreaterSum$ only needs $\O(\log(|\varphi|+\log i))$ bits of memory.

$\textit{Probe}_1(j)$
uses a decreasing counter $k = m, \ldots, j$ to successively compute the bits $b_{1}(k)$ of $\vec{\alpha} \cdot \vec{x}$,
starting at the least significant bit. To compute $b_{1}(k)$, the procedure stores the carry $c_k \leq i$
of the computation of $b_1(k+1)$; it then computes the sum $s_k := c_k + \vec{\alpha}(k) \cdot \vec{x}$
(where $\vec{\alpha}(k)$ is the $k$-th vector of bits of $\vec{\alpha}$), and sets $b_{k} := s_k \bmod 2$ and
$c_{k-1} := s_k \div 2$.
The procedure needs $\O(\log (|\varphi|+\log i))$ bits of memory for counter $k$,
$\log(i)+1$ bits for encoding $s_k$, and
$\O(\log(i))$ bits for encoding $c_k$. So it only uses $\O(\log(|\varphi|+\log i))$ bits of memory.

Let us now simulate $\GreaterSum(\vec{x}, \vec{y})$ by a halting protocol with one leader agent.
Intuitively, the protocol proceeds in rounds corresponding to the counter $k$.
The leader stores in its state the value $j$ and the current values of the program counter, of counter $k$, and of variables $b_k$, $s_k$, and $c_k$.
The crucial part is the implementation of the instruction
$s_k := c_k + \vec{\alpha}(k) \cdot \vec{x}$ of $\textit{Probe}_1(j)$.
In each round, the leader adds input agents one by one. As the protocol only needs to work for populations with $i$ agents,
it is possible for each agent to know if it already interacted with the leader in this round, and for the leader to count the number of agents it has interacted with this round, until it reaches $i$ to start the next round.

\subsubsection{Threshold protocols}\label{subsec:app-threshold}

Let us fix a threshold predicate $\varphi$ over variables $X$. Without
loss of generality\footnote{If $b \leq 0$, then we can instead
  consider the equivalent predicate $\neg(-\vec{a} \cdot \vec{v} \geq
  -b + 1)$, construct a protocol for $-\vec{a} \cdot \vec{v} \geq -b +
  1$ and handle the negation separately in \cref{subsec:finsets}.}, we
have $\varphi(\vec{v}) = \vec{a} \cdot \vec{v} \geq b$ where $\vec{a}
\in \Z^X$ and $b > 0$. We construct a simple
population protocol $\PP_{\text{thr}}$ that computes $\varphi$ under
reversible dynamic initialization, and prove its correctness.

\parag{Notations} Let $n$ be the smallest number such that $2^n >
\norm{\varphi}$. Let $P \defeq \{\q{+2^i}, \q{-2^i} : 0 \leq i \leq
n\}$, $Z \defeq \{\q{0}\}$, $N \defeq P \cup Z$ and $B \defeq \{\q{f},
\q{t}\}$, where $P$, $Z$, $N$ and $B$ respectively stand for
``$P$owers of two'', ``$Z$ero'', ``$N$umerical values'' and
``$B$oolean values''. For every set $S$ and every $x \in X$, let $S_x
\defeq \{q_x : q \in S\}$ and $S_X \defeq S \cup \bigcup_{x \in X}
S_x$.

For every $d \in \N$, let $\mathrm{bits}(d)$ denote the unique set $J
\subseteq \N$ such that $d = \sum_{j \in J} 2^j$,
\eg\ $\mathrm{bits}(13) = \mathrm{bits}(1101_2) = \{3, 2, 0\}$. The \emph{canonical representation} of an integer $d \in \Z$ is the multiset
$\mathrm{rep}(d)$ defined as follows:

$$
\mathrm{rep}(d) \defeq
\begin{cases}
  \multiset{\q{+2^i} : i \in \mathrm{bits}(d)}  & \text{if } d > 0, \\
  \multiset{\q{-2^i} : i \in \mathrm{bits}(|d|)} & \text{if } d < 0, \\
  \multiset{\q{0}}                               & \text{if } d = 0.
\end{cases}
$$

\parag{The protocol} The RDI-protocol $\PP_{\text{thr}} = (Q, T_\infty, T_\dagger, L, X, I, O)$ is defined as
follows:
\begin{itemize}
\setlength\itemsep{4pt}

\item  $Q \defeq X \cup N_X \cup B$. \\
Intuitively, the states of $X$ are the ``ports'' through which the agents for each variable
enter and exit the protocol.

\item  $I \defeq x \mapsto \q{x}$. \\
That is, the initial state for variable $x$ is $x$.

\item $L \defeq \multiset{2n \cdot \q{0}, \q{f}}$. \\
So, we have $2n$ helpers in state $\q{0}$, and one helper in state $\q{f}$, i.e., initially
the protocol assumes that the predicate does not hold.

\item $O(q) \defeq q \mapsto (0 \text{ if } q = \q{f} \text{ else } 1
\text{ if } q = \q{t} \text{ else } \bot)$. \\
That is, the output of the protocol is completely determined by the number of agents in states
$\q{t}$ and $\q{f}$

\item $T_\infty$ is the following set of (``permanent'') transitions:
\begin{alignat*}{3}
	\mathsf{add}_{x}:\ &&
	\multiset{x, |\mathrm{rep}(\vec{a}(x))| \cdot \q{0}}
	& \mapsto \multiset{\q{0}_x} \mplus \mathrm{rep}(\vec{a}(x))
	&& \quad \text{for all $x \in X$,} \\
	%
	\mathsf{up}_i^\circ:\ &&
	\multiset{\q{\circ2^i}, \q{\circ2^i}}
	&  \mapsto \multiset{\q{\circ2^{i+1}}, \q{0}}
	&& \quad\text{for all $0 \leq i < n$ and $\circ \in \{+, -\}$,} \\
	%
	\mathsf{down}_i^\circ:\ &&
	\multiset{\q{\circ2^i}, \q{0}}
	&  \mapsto \multiset{\q{\circ2^{i-1}}, \q{\circ{2^{i-1}}}}
	&& \quad\text{for all $0 < i \leq n$ and $\circ \in \{+, -\}$,} \\
	%
	\mathsf{cancel}_{i, q}:\ &&
	\multiset{\q{+2^i}, \q{-2^i}, q}
	&  \mapsto \multiset{\q{0}, \q{0}, \q{f}}
	&& \quad\text{for all $0 \leq i \leq n$ and $q \in B$,} \\
	%
	\mathsf{swap}_{p, q}^x:\ &&
	\multiset{p, q_x}
	& \mapsto \multiset{p_x, q}
	&& \quad \text{for all $p, q \in N$ and $x \in X$,} \\
	%
	\mathsf{equal}:\ &&
	\mathrm{rep}(b) \mplus \multiset{\q{f}}
	& \mapsto \mathrm{rep}(b) \mplus \multiset{\q{t}}, \\
	%
	\mathsf{false}:\ &&
	\multiset{\q{f}, \q{t}} & \mapsto \multiset{\q{f}, \q{f}}.
\end{alignat*}
Intuitively, $\mathsf{add}_{x}$ converts an agent which arrived via port $x$ into
the canonical representation of $\vec{a}(x)$. Transitions of the form $\mathsf{up}_i^\circ,
\mathsf{down}_i^\circ$ and $\mathsf{cancel}_{i, q}$ allow the protocol to change
the representation of a value, without changing the value itself.
Transition $\mathsf{equal}$ allows the protocol to detect that the current value
of $\vec{a}\cdot \vec{x}$, for the current input $\vec{x}$, is at least $b$, which moves
a helper from state $\q{f}$ to $\q{t}$.
\item Finally, $T_{\dagger}$ is the following set of RDI-transitions:
\begin{alignat*}{3}
	\mathsf{add}_{x,q}^{-1}:\ &&
	\multiset{\q{0}_x, q} \mplus \mathrm{rep}(\vec{a}(x))
	& \mapsto \multiset{x, \q{f}, |\mathrm{rep}(\vec{a}(x))| \cdot \q{0}}
	&& \quad \text{for all $x \in X$ and $q \in B$,} \\
	%
	\mathsf{cancel}_{i,q}^{-1}:\ &&
	\multiset{\q{0}, \q{0}, q}
	&  \mapsto \multiset{\q{+2^i}, \q{-2^i}, \q{f}}
	&& \quad\text{for all $0 \leq i \leq n$ and $q \in B$,}
	\\
	%
	\mathsf{reset}:\ &&
	\multiset{\q{t}}
	& \mapsto \multiset{\q{f}}.
\end{alignat*}
The first two transitions are needed to reverse the changes of
$\mathsf{add}$ and $\mathsf{cancel}$ transitions while the dynamic
initialization is not finished. Both types of transitions reset the
output of the protocol by leaving an agent in the default output state
$\q{f}$. The $\mathsf{reset}$ transition resets the output by moving
agents from $\q{t}$ to $\q{f}$.
\end{itemize}

\noindent Let $\PP_\infty = (Q, T_\infty, L, X, I , O)$.
Let $T \defeq T_\infty \cup T_\dagger$. For the sake of readability,
we will sometimes omit the subscripts and superscripts from transitions names
when they are irrelevant, \eg\ ``a
$\mathsf{swap}$ transition is enabled'' instead of ``there exist $p, q
\in N$ and $x \in X$ such that $\mathsf{swap}_{p,q}^x$ is enabled''.\medskip

\parag{Size} Note that $\PP_{\text{thr}}$ has $|Q| = |X| + |N_X| + |B|
= |X| + (2n+3) \cdot (|X|+1) + 2 \in \O(\log \norm{\varphi} \cdot
|X|)$ states and $|L| = 2n+1 \in \O(\log \norm{\varphi})$
helpers. Moreover, since families of transitions are parameterized by
$X$, $B$, $N$ or $N^2$, and $\{+, -\}$, there are $\O(|N|^2 \cdot |X|)
= \O(\log^2 \norm{\varphi} \cdot |X|) \subseteq \O(|\varphi|^3)$
transitions. Finally, each transition uses at most
$\O(|\mathrm{rep}(\norm{\varphi})|) = \O(\log \norm{\varphi})
\subseteq \O(|\varphi|)$ states.

\medskip

\parag{Auxiliary definitions and observations} Before proving that
$\PP_{\text{thr}}$ works as intended, let us first introduce auxiliary
definitions. Let $\val \colon Q \to \N$ be the function that
associates a value to each state as follows:
\begin{align*}
  \val(\q{0}) &= \val(\q{f}) = \val(\q{t}) \defeq 0, \\
  %
  \val(x) &\defeq \vec{a}(x)
  && \text{for every } x \in X, \\
  %
  \val(\q{\circ2^i}) &\defeq \circ2^i
  && \text{for every } 0 \leq i \leq n \text{ and } \circ \in \{+, -\}, \\
  %
  \val(q_x) &\defeq \val(q)
  && \text{for every } q \in N \text{ and } x \in X.
\end{align*}
\noindent So, for example, for the predicate $3x - 4y \geq 2$ we have $\val(x) = 3$ and
$\val(y) = -4$.
For every configuration $C$ and every set of states $S \subseteq Q$, let
$$\val_S(C) \defeq \sum_{q \in S} \val(q) \cdot C(q).$$ In particular,
let $\val(C) \defeq \val_Q(C)$. Intuitively, $C$ can be seen as an encoding of the value
$\val(C)$. The following properties, relating
values and configurations, can be derived from the above definitions:
\begin{proposition}\label{prop:thr:prop}
  For every initialization sequence $\pi$ with effective input $\vec{w}$
  such that $L' \trans{\pi} C$ for some $L' \succeq L$, the following holds:
  \begin{enumerate}
  \item $\val(C) = \vec{a} \cdot \vec{w}$, \label{itm:val:inv}

  \item $|C| = C(N) + C(B) + |\vec{w}|$,\label{itm:config:size}

  \item $C(N) \geq L(N)$ and $C(B) \geq L(B)$, \label{itm:preservation}

  \item $C(N_x) + C(x) = \vec{w}(x)$ for every $x \in
    X$. \label{itm:preservation:x}
  \end{enumerate}
\end{proposition}

\noindent In particular, \eqref{itm:config:size} states that the
number of agents is always equal to the number of helpers plus the
\emph{net} amount of agents that dynamically entered the population.

\parag{Auxiliary propositions} We say that a configuration $C$ is
\emph{clean} if the following holds for every $p, q \in
P_X$:\smallskip
\begin{itemize}
\item If $\val(p) + \val(q) = 0$, then $C(p) = 0$ or $C(q) = 0$. \\
For example, a configuration with agents in $\q{+2^i}_x$ and
$\q{-2^i}_y$ is not clean, since $\val(\q{+2^i}_x) + \val(\q{-2^i}_y) = 0$.
Intuitively, no pair of agents can cancel in a clean configuration.\medskip

\item If $\val(p) = \val(q)$ and $\val(p) \not\in \{-2^n, +2^n\}$,
  then $C(\{p, q\}) \leq 1$. \\
For example, a configuration with two agents in $\q{+2^i}_x$, where $i < n$,
is not clean. Intuitively, in a clean configuration no agent can be promoted to
a higher power of 2.
\end{itemize}

We show that any configuration can be cleaned using only permanent transitions.
This implies that once the dynamic initialization has terminated, every fair
execution visits clean configurations infinitely often.

\begin{proposition}\label{prop:cleaning}
  For every initialization sequence $\pi$ such that $L' \trans{\pi} C$ for some
  $L' \succeq L$, there exists a clean configuration $D$
  such that $C \trans{T_{\infty}^*} D$.
\end{proposition}

\begin{proof}
  If $C$ is clean, then we pick $D \defeq C$. Otherwise, at least one
  of the following holds:
  \begin{enumerate}[(a)]
    \item $C(p) > 0$, $C(q) > 0$ and $\val(p) + \val(q) = 0$ for some
      $p, q \in P_X$; \label{itm:clean:eq}

    \item $C(\{p, q\}) \geq 2$ for some $p, q \in P_X$ such that
      $\val(p), \val(q) \not\in \{-2^n, +2^n\}$. \label{itm:clean:up}
  \end{enumerate}

  We claim there exists a configuration $C'$ such that $C \trans{T_{\infty}^*}
  C'$ and $C(P_X) > C'(P_X)$. Let us show that if the claim is true then the result holds. If $C'$ is clean, then we are
  done. Otherwise, this process is repeated until a clean
  configuration $D$ has been reached. The process terminates as the
  number of agents in $P_X$ cannot become negative.

  Let us now prove the claim. Suppose~\eqref{itm:clean:eq}
  holds. By \cref{prop:thr:prop}~\eqref{itm:preservation}, we have
  $C(N) \geq L(N) \geq 2$ and hence it is possible to consecutively
  fire at least two $\mathsf{swap}$ transitions. Note that they do not
  change the amount of agents in $P_X$. For this reason, we may assume
  without loss of generality that $p = \q{+2^i}$ and $q = \q{-2^i}$
  for some $0 \leq i \leq
  n$. By \cref{prop:thr:prop}~\eqref{itm:preservation}, we have
  $C(B) \geq L(B) > 0$. Thus, there exists $r \in B$ such that $C(r) >
  0$. Therefore, firing transition $\mathsf{cancel}_{i, r}$ decreases
  $C(P_X)$ by two.

  Similarly, if case~\eqref{itm:clean:up} holds, then we may assume
  without loss of generality that $C(\q{\circ2^i}) \geq 2$ for some $0
  \leq i < n$ and $\circ \in \{+, -\}$. Thus, firing transition
  $\mathsf{up}_i^\circ$ decreases $C(P_X)$ by one.
\end{proof}

We now bound the number of agents in states from $X \cup P_X$ in a
clean configuration.

\begin{proposition} \label{prop:top:small}
  For every initialization sequence $\pi$ with effective input $\vec{w}$
  such that $L' \trans{\pi} C$ for some $L' \succeq L$, if $C$ is clean,
  then $C(X) + C(P_X) \leq |\vec{w}| + n$.
\end{proposition}

\begin{proof}
  Let $S_{\circ 2^n} \defeq \{q \in P_X : \val(q) = \circ2^n\}$ for
  both $\circ \in \{+, -\}$. Since $C$ is clean, we have $C(S_{\circ
    2^n}) = 0$ for some $\circ \in \{+, -\}$. Let us consider the case
  where $\circ = -$. The other case is proven analogously.

  Let $\vec{u} \in \N^X$ be such that $\vec{u}(x) \defeq C(x)$ for
  every $x \in X$. Note that $|\vec{u}| = C(X)$, and that $\vec{u}
  \leq \vec{w}$ by \cref{prop:thr:prop}~\eqref{itm:preservation:x}. Since $C$ is clean, we
  have $C(P_X \setminus S_{+2^n}) \leq n$. Thus, it suffices to show
  that $C(S_{+2^n}) \leq |\vec{w}| - |\vec{u}|$. Suppose this is not
  the case. This yields a contradiction:
  \begin{align*}
    \val_{P_X}(C)
    &> 2^n \cdot C(S_{+2^n}) - 2^n
    && \text{(since $C$ is clean)} \\
    %
    &\geq 2^n \cdot (|\vec{w}| - |\vec{u}| + 1) - 2^n
    && \text{(by assumption)} \\
    %
    &= 2^n \cdot (|\vec{w}| - |\vec{u}|) \\
    %
    &\geq \vec{a} \cdot (\vec{w} - \vec{u}) && \text{(since $2^n >
      \norm{\vec{a}}$ and $\vec{w} \geq \vec{u}$)} \\
    %
    &= \vec{a} \cdot \vec{w} - \vec{a} \cdot \vec{u} \\
    %
    &= \val(C) - \val_X(C)
    && \text{(by Prop.~\ref{prop:thr:prop}~\eqref{itm:val:inv} and
      def.\ of $\vec{u}$)} \\
    %
    &= \val_{P_X}(C)
    && \text{(by def.\ of $\val$)} \qedhere
  \end{align*}
\end{proof}

The following corollary shows that the number of agents in state
$\q{0}$ can always be increased back to at least $n$. This will later
be useful in arguing that the number of agents in $X$ can eventually
be decreased to zero.

\begin{corollary} \label{cor:enough:zero}
  For every initialization sequence $\pi$ with effective input $\vec{w}$ such
  that $L' \trans{\pi} C$ for some $L' \succeq L$, there exists a clean
  configuration $D$ such that $C \trans{T_{\infty}^*} D$ and $D(\q{0}) \geq n$.
\end{corollary}

\begin{proof}
  By \cref{prop:cleaning}, there exists a clean configuration $C'$
  such that $C \trans{\pi' \in T_\infty^*} C'$. Let us first prove that $C'(Z_X) \geq n$.
  Note that $\pi\pi'$ is an initialization sequence with effective input
  $\vec{w}$ such that $L' \trans{\pi\pi'} C'$. Thus:
  \begin{align*}
    C'(Z_X)
    &= |C'| - C'(X) - C'(P_X) - C'(B)
    && \text{(by def.\ of $Q$)} \\
    %
    &= (C'(N) + C'(B) + |\vec{w}|) - C'(X) - C'(P_X) - C'(B)
    && \text{(by Prop.~\ref{prop:thr:prop}~\eqref{itm:config:size})} \\
    %
    &\geq (L(N) + C'(B) + |\vec{w}|) - C'(X) - C'(P_X) - C'(B)
    && \text{(by Prop.~\ref{prop:thr:prop}~\eqref{itm:preservation})} \\
    %
    &\geq (L(N) + C'(B) + |\vec{w}|) - (|\vec{w}| + n) - C'(B)
    && \text{(by Prop.~\ref{prop:top:small})} \\
    %
    &= L(N) - n \\
    %
    &\geq n
    && \text{(by def.\ of $L$)}
  \end{align*}
  Now, by \cref{prop:thr:prop}~\eqref{itm:preservation}, we have
  $C'(N) \geq L(N) \geq n$. Thus, using $\mathsf{swap}$ transitions, we
  can swap $n$ agents from $Z_X$ to $\q{0}$. This way, we obtain a
  configuration $D$ such that $C' \trans{T_{\infty}^*} D$ and $D(\q{0}) \geq
  n$. We are done since $\mathsf{swap}$ transitions preserve
  cleanness.
\end{proof}

For every configuration $C$, let
\begin{align*}
  \val^+(C) &\defeq \sum_{\substack{q \in P_X \\ \val(q) > 0}} \val(q)
  \cdot C(q), &
  %
  \val^-(C) &\defeq \sum_{\substack{q \in P_X \\ \val(q) < 0}} \val(q)
  \cdot C(q).
\end{align*}
We now show that, once dynamic initialization has terminated, fair executions stabilize to configurations of a
certain ``normal form''.

\begin{proposition}\label{prop:threshold:stabilize}
  For every initialization sequence $\pi$ with effective input $\vec{w}$
  such that $L' \trans{\pi} C$ for some $L' \succeq L$ and for every fair execution
  $\sigma$ of $\PP_\infty$ starting from $C$,
  there exist $i \in \N$, $m_+ \geq 0$ and $m_- \leq 0$ such that:
  \begin{enumerate}
  \item $\sigma_i(X) = \sigma_{i+1}(X) = \cdots = 0$,

  \item $\val^\circ(\sigma_i) = \val^\circ(\sigma_{i+1}) = \cdots =
    m_\circ$ for both $\circ \in \{+, -\}$,

  \item $m_+ = 0 \lor m_- = 0$.
  \end{enumerate}
\end{proposition}

\begin{proof}
  For the sake of contradiction, assume there exist infinitely many
  indices $j$ such that $\sigma_j(X) > 0$. Let $j \in \N$ be such an
  index. By \cref{cor:enough:zero}, there exists a configuration $C_j$
  such that $\sigma_j \trans{T_{\infty}^*} C_j$ and $C_j(\q{0}) \geq n$. Hence,
  there exists $x \in X$ such that transition $\mathsf{add}_x$ is
  enabled in $C_j$. Since this holds for infinitely many indices and
  since $X$ is finite, fairness implies that some $\mathsf{add}$
  transition can be enabled infinitely often and hence occurs
  infinitely often along $\sigma$. This is impossible since the number
  of agents in $X$ cannot be increased by any transition in $T_\infty$,
  and thus would eventually drop below zero.
  Therefore, there exists $h \in \N$ such that
  $\sigma_h(X) = \sigma_{h+1}(X) = \cdots = 0$.

  Since $X$ is permanently empty from index $h$, the $\mathsf{add}$ transitions
  are permanently disabled. No other transition in $T_\infty$ can increase
  the absolute value of $\val^\circ$ for any $\circ \in \{+, -\}$. Thus, we have
  $|\val^\circ(\sigma_h)| \geq |\val^\circ(\sigma_{h+1})| \geq
  \cdots$ for both $\circ \in \{+, -\}$. Therefore, there exist $i
  \geq h$, $m_+ \geq 0$ and $m_- \leq 0$ such that
  \begin{align}
    \val^+(\sigma_i) &= \val^+(\sigma_{i+1}) = \cdots = m_+,\label{eq:stab1} \\
    \val^-(\sigma_i) &= \val^-(\sigma_{i+1}) = \cdots = m_-.\label{eq:stab2}
  \end{align}

  It remains to show that $m_+ = 0$ or $m_- = 0$. For the sake of
  contradiction, suppose this is not the case. For every $j \geq i$,
  \cref{cor:enough:zero} yields a configuration $C_j$ such that
  $\sigma_j \trans{T_{\infty}^*} C_j$ and $C_j(\q{0}) \geq n$. Thus, by fairness,
  there exist infinitely many indices $j \geq i$ such that
  $\sigma_j(\q{0}) \geq n$. Let $j$ be such an index. Let $0 \leq d,
  d' \leq n$ be the largest indices for which there exist states $q,
  q' \in P_X$ such that $\sigma_j(q) > 0$, $\sigma_j(q') > 0$,
  $\val(q) = 2^{d}$ and $\val(q') = -2^{d'}$. Note that these indices
  exist because $m_+ \neq 0$ and $m_- \neq 0$.

  Assume without loss of generality that $d \geq d'$, as the other
  case is symmetric. By \cref{prop:thr:prop}~\eqref{itm:preservation},
  there exists $r \in B$ such that $C(r) > 0$. Since $C_j(\q{0}) \geq
  n \geq d - d'$, the sequence of transitions $\mathsf{down}_d^+,
  \mathsf{down}_{d-1}^+, \ldots, \mathsf{down}_{d'+1}^+$ can be fired
  from $C_j$. From there, we can fire $\mathsf{cancel}_{d', r}$ which
  leads to a configuration $D_j$ such that $|\val^\circ(D_j)| <
  |m_\circ|$ for both $\circ \in \{+, -\}$. Since there are infinitely
  many such indices $j$, fairness implies that some such configuration
  $D_j$ occurs (infinitely often) along $\sigma$, which contradicts
  both~(\ref{eq:stab1}) and~(\ref{eq:stab2}).
\end{proof}

\parag{Main proof} We are now ready to prove that $\PP_{\text{thr}}$
works as intended.

\newcommand{\mathrm{false}}{\mathrm{false}}

\begin{theorem}
  $\PP_{\text{thr}}$ computes $\varphi$ with helpers and under
  reversible dynamic initialization.
\end{theorem}

\begin{proof}
  We first show that $\PP_{\text{thr}}$ is input reversible, and then
  that it correctly computes $\varphi$.

  \medskip\noindent\emph{Input reversibility.} Let $\pi$ be an
  initialization sequence with effective input $\vec{w}$ such that
  $L' \trans{\pi} C$ for some $L' \succeq L$. By
  \cref{prop:thr:prop}~\eqref{itm:preservation:x}, we have $C(I(x)) =
  C(x) = \vec{w}(x) - C(N_x) \leq \vec{w}(x)$ for every $x \in X$,
  which proves the first required property.

  For every configuration $C$, let $\mathrm{false}(C) \defeq D$ where $D(t)
  \defeq 0$, $D(f) \defeq C(t) + C(f)$ and $D(q) \defeq C(q)$ for
  every $q \in Q \setminus \{f, t\}$. Observe that for every
  configuration $C$, the following holds:
  \begin{align}
    C \trans{\mathsf{reset}^{C(\q{t})}} \mathrm{false}(C) \text{ and }
    \mathrm{false}(C) \in [C].\label{eq:reset:false}
  \end{align}
  It remains to show that if $C \trans{\pi_\triangleright \in T^*} D$
  and $D' \in [D]$, then $D' \trans{\pi_\triangleleft \in T^*} C'$ for
  some $C' \in \DiEq{C}$. By~\eqref{eq:reset:false}, it is enough to
  argue that $\mathrm{false}(D) \trans{T^*} \mathrm{false}(C)$.

  Let $C_i \trans{t_i} C_{i+1}$ be the $i^\text{th}$ step of
  $\pi_\triangleright$. We argue that $\mathrm{false}(C_{i+1}) \trans{t_i'}
  \mathrm{false}(C_i)$ for some $t_i' \in T \cup \{\varepsilon\}$. By
  induction, this implies $\mathrm{false}(D) \trans{T^*} \mathrm{false}(C)$ as
  desired. If $t_i$ is an $\mathsf{equal}$, $\mathsf{false}$ or
  $\mathsf{reset}$ transition, then we already have $\mathrm{false}(C_{i+1}) =
  \mathrm{false}(C_i)$. Otherwise we revert the step as follows, where ``$s
  \mapsto u$'' indicates that if $t_i = s$, then we reverse it with
  $t_i' = u$:
  \begin{align*}
    \mathsf{add}_x &\mapsto \mathsf{add}_{x,\q{f}}^{-1}
    && \text{for every $x \in X$,} \\
    %
    \mathsf{add}_{x,q}^{-1} &\mapsto \mathsf{add}_x
    && \text{for every $x \in X$ and $q \in B$,} \\
    %
    \mathsf{up}_i^\circ &\mapsto \mathsf{down}^\circ_{i+1}
    && \text{for every $0 \leq i < n$ and $\circ \in \{+, -\}$,}\\
    %
    \mathsf{down}^\circ_i &\mapsto \mathsf{up}_{i-1}^\circ
    && \text{for every $0 < i \leq n$ and $\circ \in \{+, -\}$,} \\
    %
    \mathsf{cancel}_{i,q} &\mapsto \mathsf{cancel}_{i,\q{f}}^{-1}
    && \text{for every $0 \leq i \leq n$ and $q \in B$,} \\
    %
    \mathsf{cancel}_{i,q}^{-1} &\mapsto \mathsf{cancel}_{i,\q{f}}
    && \text{for every $0 \leq i \leq n$ and $q \in B$,}\\
    %
    \mathsf{swap}_{p, q}^x &\mapsto \mathsf{swap}_{q, p}^x
    && \text{for every $p, q \in N$ and $x \in X$.}
  \end{align*}
  Note that $t_i'$ is not the exact reverse transition of $t_i$, as it
  may differ over $B$. Indeed, $t_i'$ may require an agent in state
  $\q{f}$, which may not have been produced by $t_i$. However, this is
  not an issue since, by definition of $\mathrm{false}$ and by
  \cref{prop:thr:prop}~\eqref{itm:preservation}, we have:
  $$\mathrm{false}(C_{i+1})(\q{f}) = C_{i+1}(B) \geq L(B) > 0.$$ Thus, we have
  $\mathrm{false}(C_{i+1}) \trans{t_i'} \mathrm{false}(C_i)$ as desired, which
  completes the proof.

  \medskip\noindent\emph{Correctness.} Let $\pi$ be an initialization
  sequence with effective input $\vec{w}$ such that $L' \trans{\pi} C$
  for some $L' \succeq L$.
  Let $\sigma$ be a fair execution of $\PP_\infty$ starting from $C$.
  By \cref{prop:threshold:stabilize}, there exist
  $i \in \N$, $m_+ \geq 0$ and $m_- \leq 0$ such that:\smallskip
  \begin{enumerate}[(a)]
    \item $\sigma_i(X) = \sigma_{i+1}(X) = \cdots =
      0$, \label{itm:input:stab}

    \item $\val^\circ(\sigma_i) = \val^\circ(\sigma_{i+1}) = \cdots =
      m_\circ$ for both $\circ \in \{+, -\}$, \label{itm:val:stab}

    \item $m_+ = 0 \lor m_- = 0$.
  \end{enumerate}

  First, let us show that $O(\sigma) \in \{0, 1\}$. We make a case
  distinction on whether $m_+ \geq b$.\medskip

  \noindent\emph{Case $m_+ \geq b$.} We show that $O(\sigma) =
  1$. Note that $m_+ \geq b > 0$ which implies that $m_- = 0$. Thus,
  by~\eqref{itm:val:stab}, no $\mathsf{cancel}$ transition is enabled
  in $\sigma_j$ for every $j \geq i$. Thus, it suffices to show that
  $\sigma_j(\q{f}) = 0$ for some $j \geq i$. For the sake of
  contradiction, suppose this is not the case. Let $j \geq i$ be such
  that $\sigma_j(\q{f}) > 0$. We claim that $\sigma_j$ can reach some
  configuration $D_j$ enabling transition $\mathsf{equal}$,
  \ie\ larger or equal to $\mathrm{rep}(b)$. This claim, together with
  fairness, yields a contradiction since this transition can move all
  agents in state $\q{f}$ to state $\q{t}$.

  Let us prove the claim. By \cref{cor:enough:zero}, we have $\sigma_j
  \trans{T_\infty^*} C_j$ where $C_j(\q{0}) \geq n$. Note that $\val^+(C_j) =
  \val^+(\sigma_j)$. If $\val^+(C_j) = b$, then, by cleanness, $C_j$
  contains precisely the binary representation of $b$, and hence $C_j
  \geq \mathrm{rep}(b)$. Thus, assume $\val^+(C_j) > b$. Let $0 \leq d
  \leq n$ be the largest exponent for which there exists a state $q
  \in P_X$ such that $C_j(q) > 0$, $\val(q) = 2^d$ and $d \not\in
  \mathrm{bits}(b)$. Since $C_j(\q{0}) \geq n \geq d$, the sequence of
  transitions $\mathsf{down}_d^+ \cdot \mathsf{down}_{d-1}^+ \cdots
  \mathsf{down}_1^+$ can be fired from $C_j$, which yields a
  configuration $D_j \geq \mathrm{rep}(b)$.\medskip

  \noindent\emph{Case $m_+ < b$.} We show that $O(\sigma) = 0$. First note
  that $\mathsf{equal}$ is disabled in $\sigma_j$ for every
  $j \geq i$, as otherwise we would have
  $\sigma_j \geq \mathrm{rep}(b)$ which implies that $m_+
  = \val^+(\sigma_j') \geq b$. Thus, it suffices to show that there
  are infinitely many indices $j$ such that $\sigma_j(\q{f}) >
  0$. Indeed, if this is the case, then, by fairness, $\mathsf{false}$
  permanently moves all agents in state $\q{t}$ to state $\q{f}$.

  For the sake of contradiction, suppose the claim does not hold.
  Let $\sigma' \defeq \pi\sigma$. Let $j \in \N$ be the largest index
  such that $\sigma_j'(\q{f}) > 0$.
  Note that this configuration exists as $\sigma_0' = L' \succeq L$ and $L(\q{f}) > 0$.
  The only transition that reduces the number of agents in $\q{f}$ is $\mathsf{equal}$.
  Thus, $\sigma_j' \trans{\mathsf{equal}} \sigma_{j+1}'$ and $\val^+(\sigma_j') \geq b$.
  As finally, $m_+ < b$, some $\mathsf{cancel}$ or $\mathsf{add}^{-1}$ transition
  must be fired in $\sigma'_{j'}$ for some $j' > j$.
  In both cases there is afterwards an agent in state $\q{f}$.
  This contradicts the maximality of $j$. \medskip

  We are done proving $O(\sigma) \in \{0, 1\}$. It remains to
  argue that $O(\sigma) = \varphi(\vec{w})$. We have:
  \begin{align*}
    \vec{a} \cdot \vec{w}
    %
    &= \val(\sigma_i)
    && \text{(by Prop.~\ref{prop:thr:prop}~\eqref{itm:val:inv})}\\
    %
    &= \val^+(\sigma_i) + \val^-(\sigma_i)
    && \text{(by~\eqref{itm:input:stab})} \\
    %
    &= m_+ + m_-.
    && \text{(by~\eqref{itm:val:stab})}
  \end{align*}
  Recall that $m_+ \geq 0$, $m_- \leq 0$ and $(m_+ = 0 \lor m_- =
  0)$. If $\vec{a} \cdot \vec{w} \geq b$, then we must have $m_+ \geq
  b > 0$ and $m_- = 0$. Therefore, the first case above holds, and
  hence $O(\sigma) = 1$, which is correct. If $\vec{a} \cdot \vec{w} <
  b$, then we must have $m_+ < b$. Therefore, the second case above
  holds, and hence $O(\sigma) = 0$, which is also correct.
\end{proof}

\section{Introduction}
\input{sec-introduction}

\section{Preliminaries}\label{sec:prelims}
\input{sec-preliminaries}

\section{Population protocols}\label{sec:popprot}
\input{sec-protocols}

\section{Main result}\label{sec:main}
\input{sec-main}

\section{Succinct protocols for large populations}\label{sec:large}
\input{sec-large}

\section{Succinct protocols for small populations}\label{sec:small}
\input{sec-small}

\section{Conclusion and further work}\label{sec:conc}
\input{sec-conclusion}

\subsubsection{Remainder protocols}\label{subsec:app-remainder}

This section describes a family of protocols with helpers computing
remainder predicates under reversible dynamic initialization. The
construction, its correctness proof and its intermediary propositions
are similar to those presented in \cref{subsec:app-threshold} for
the case of threshold predicates. For completeness, we repeat and
adapt them in full details.

Let us fix a remainder predicate $\varphi$ over variables $X$.
Let $\varphi(\vec{v}) \defeq \vec{a} \cdot \vec{v} \equiv_m b$
where $\vec{a} \in \Z^X$ and $m \in \N_{\geq 2}$ and $b \in \Z$.
Without loss of generality\footnote{If this is not the case for some coefficient
	 $\vec{a}(x)$, then we can replace it by $\vec{a}(x) \bmod m$,
	 which yields an equivalent predicate.},
we may assume $0 \leq b < m$ and $0 \leq \vec{a}(x) < m$ for each $x \in X$.

Instead of directly constructing a protocol for $\varphi(\vec{v})$, we rewrite the predicate. This yields a different but equivalent predicate $\varphi'(\vec{v})$:
\begin{align*}
\varphi'(v) \defeq
	\begin{cases}
		\vec{a} \cdot \vec{v} \not \geq 1~(\text{mod } m)
			& \text{ if } b = 0, \\
		\vec{a} \cdot \vec{v} \geq b ~(\text{mod } m) \land \vec{a} \cdot \vec{v} \not\geq b + 1 ~(\text{mod } m)
			& \text{ if } b > 0. \\
	\end{cases}
\end{align*}

As we can handle negations and conjunctions separately in \cref{subsec:finsets},
it is enough to describe a protocol for the predicate
$\varphi(\vec{v}) \defeq \vec{a} \cdot \vec{v} \geq b~(\text{mod } m)$ where
$\vec{a} \in \N^X$, $m \in \N_{\geq 2}$, $0 < b < m$ and $0 \leq \vec{a}(x) < m$ for each $x \in X$.

We construct a simple population protocol $\PP_{\text{rem}}$ with helpers that
computes $\varphi$ under reversible dynamic initialization, and prove its correctness.

\parag{Notation} Let $n$ be the smallest number such that $2^n >
\norm{\varphi}$. Let $P \defeq \{\q{2^i} : 0 \leq i \leq
n\}$, $Z \defeq \{\q{0}\}$, $N \defeq P \cup Z$ and $B \defeq \{\q{f},
\q{t}\}$, where $P$, $Z$, $N$ and $B$ respectively stand for
``$P$owers of two'', ``$Z$ero'', ``$N$umerical values'' and
``$B$oolean values''. For every set $S$ and every $x \in X$, let $S_x
\defeq \{q_x : q \in S\}$ and $S_X \defeq S \cup \bigcup_{x \in X}
S_x$.

For every $d \in \N$, let $\mathrm{bits}(d)$ denote the unique set $J
\subseteq \N$ such that $d = \sum_{j \in J} 2^j$,
\eg\ $\mathrm{bits}(13) = \mathrm{bits}(1101_2) = \{3, 2, 0\}$. The \emph{canonical representation} of an integer $d \in \Z$ is the multiset $\mathrm{rep}(d)$ defined as follows:
$$
\mathrm{rep}(d) \defeq
\begin{cases}
\multiset{\q{2^i} : i \in \mathrm{bits}(d)}   & \text{if } d > 0, \\
\multiset{\q{0}}                              & \text{if } d = 0.
\end{cases}
$$

\parag{The protocol} The RDI-protocol $\PP_{\text{rem}} = (Q, T_\infty, T_\dagger, L, X, I, O)$ is defined as
follows:
\begin{itemize}
\setlength\itemsep{4pt}

  \item  $Q \defeq X \cup N_X \cup B$. \\
	Intuitively, the states of $X$ are the ``ports'' through which the agents for each variable
	enter and exit the protocol.

	\item  $I \defeq x \mapsto \q{x}$. \\
	That is, the initial state for variable $x$ is $x$.

	\item $L \defeq \multiset{2n \cdot \q{0}, \q{f}}$. \\
	So, we have $2n$ helpers in state $\q{0}$, and one helper in state $\q{f}$, i.e., initially
	the protocol assumes that the predicate does not hold.

	\item $O(q) \defeq q \mapsto (0 \text{ if } q = \q{f} \text{ else } 1
	\text{ if } q = \q{t} \text{ else } \bot)$. \\
	That is, the output of the protocol is completely determined by the number of agents
	in states $\q{t}$ and $\q{f}$

	\item $T_\infty$ is the following set of (``permanent'') transitions:
	\begin{alignat*}{3}
		\mathsf{add}_{x}:\ &&
		\multiset{x, |\mathrm{rep}(\vec{a}(x))| \cdot \q{0}}
		& \mapsto \multiset{\q{0}_x} \mplus \mathrm{rep}(\vec{a}(x))
		&& \qquad \text{for every $x \in X$,} \\
		%
		\mathsf{up}_i:\ &&
		\multiset{\q{2^i}, \q{2^i}}
		&  \mapsto \multiset{\q{2^{i+1}}, \q{0}}
		&& \qquad\text{for every $0 \leq i < n$,} \\
		%
		\mathsf{down}_i:\ &&
		\multiset{\q{2^i}, \q{0}}
		&  \mapsto \multiset{\q{2^{i-1}}, \q{{2^{i-1}}}}
		&& \qquad\text{for every $0 < i \leq n$,} \\
		%
		\mathsf{modulo}_q:\ &&
		\mathrm{rep}(b) \mplus \multiset{q}
		&  \mapsto \mathrm{rep}(b) \mplus \multiset{\q{f}}
		&& \qquad\text{for every $q \in B$,} \\
		%
		\mathsf{swap}_{p, q}^x:\ &&
		\multiset{p, q_x}
		& \mapsto \multiset{p_x, q}
		&& \qquad \text{for every $p, q \in N$ and $x \in X$,} \\
		%
		\mathsf{equal}:\ &&
		\mathrm{rep}(b) \mplus \multiset{\q{f}}
		& \mapsto \mathrm{rep}(b) \mplus \multiset{\q{t}}, \\
		%
		\mathsf{false}:\ &&
		\multiset{\q{f}, \q{t}} & \mapsto \multiset{\q{f}, \q{f}}.
	\end{alignat*}
	Intuitively, $\mathsf{add}_{x}$ converts an agent which arrived via port $x$ into
	the canonical representation of $\vec{a}(x)$. Transitions of the form $\mathsf{up}_i,
	\mathsf{down}_i$ allow the protocol to change
	the representation of a value, without changing the value itself.
	The $\mathsf{modulo}$ transition reduces the overall value by $m$.
	Transition $\mathsf{equal}$ allows the protocol to detect that the current value
	is at least $b$, which moves a helper from state $\q{f}$ to $\q{t}$.
	\item Finally, $T_{\dagger}$ is the following set of RDI-transitions:
	\begin{alignat*}{3}
		\mathsf{add}_{x,q}^{-1}:\ &&
		\multiset{\q{0}_x, q} \mplus \mathrm{rep}(\vec{a}(x))
		& \mapsto \multiset{x, \q{f}, |\mathrm{rep}(\vec{a}(x))| \cdot \q{0}}
		&& \quad \text{for every $x \in X$ and $q \in B$,} \\
		%
		\mathsf{modulo}_q^{-1}:\ &&
		\mathrm{rep}(b) \mplus \multiset{q}
		&  \mapsto \mathrm{rep}(b) \mplus \multiset{\q{f}}
		&& \quad\text{for every $q \in B$,} \\
		%
		\mathsf{reset}:\ &&
		\multiset{\q{t}}
		& \mapsto \multiset{\q{f}}.
	\end{alignat*}
	The first two transitions are needed to reverse the changes of
	$\mathsf{add}$ and $\mathsf{modulo}$ transitions while the dynamic
	initialization is not finished. Both types of transitions reset the output of the protocol
	by leaving an agent in the default output state $\q{f}$. The
	$\mathsf{reset}$ transition resets the output by moving agents from
	$\q{t}$ to $\q{f}$.
\end{itemize}

\noindent Let $\PP_\infty = (Q, T_\infty, L, X, I , O)$.
Let $T \defeq T_\infty \cup T_\dagger$. For the sake of readability,
we will sometimes omit the subscripts and superscripts from transitions names
when they are irrelevant, \eg\ ``a
$\mathsf{swap}$ transition is enabled'' instead of ``there exist $p, q
\in N$ and $x \in X$ such that $\mathsf{swap}_{p,q}^x$ is enabled''.\medskip

\parag{Size} Note that $\PP_{\text{rem}}$ has $|Q| = |X| + |N_X| + |B|
= |X| + (n+2) \cdot (|X|+1) + 2 = \O(\log \norm{\varphi} \cdot |X|)$
states and $|L| = 2n+1 = \O(\log \norm{\varphi})$ helpers. Moreover,
since families of transitions are parameterized by $X$, $B$ and $N$ or $N^2$,
there are $\O(|N|^2 \cdot |X|) = \O(\log^2 \norm{\varphi} \cdot |X|)
\subseteq \O(|\varphi|^3)$ transitions. Finally, each transition uses at most
$\O(|\mathrm{rep}(\norm{\varphi})|) = \O(\log \norm{\varphi})
\subseteq \O(|\varphi|)$ states.\medskip

\parag{Auxiliary definitions and observations} Before proving that
$\PP_{\text{rem}}$ works as intended, let us first introduce auxiliary
definitions. Let $\val \colon Q \to \N$ be the function that
associates a value to each state as follows:
\begin{align*}
	\val(\q{0}) &= \val(\q{f}) = \val(\q{t}) \defeq 0, \\
	%
	\val(x) &\defeq \vec{a}(x)
	&& \text{for every } x \in X, \\
	%
	\val(\q{2^i}) &\defeq 2^i
	&& \text{for every } 0 \leq i \leq n, \\
	%
	\val(q_x) &\defeq \val(q)
	&& \text{for every } q \in N \text{ and } x \in X.
\end{align*}
\noindent So, for example, for the predicate $5x + 6y \geq 4\ (\bmod\ m)$ we have $\val(x) = 5$ and
$\val(y) = 6$.
For every configuration $C$ and set of states $S \subseteq Q$, let
$$\val_S(C) \defeq \sum_{q \in S} \val(q) \cdot C(q).$$
In particular, let $\val(C) \defeq \val_Q(C)$.
Intuitively, $C$ can be seen as an encoding of the value $\val(C)$.
The following properties, relating values and configurations, can be derived from
the above definitions:
\begin{proposition}\label{prop:rem:prop}
	For every initialization sequence $\pi$ with effective input $\vec{w}$ such
	that $L' \trans{\pi} C$ for some $L' \succeq L$, the following holds:
	\begin{enumerate}
		\item $\val(C) \equiv_m \vec{a} \cdot \vec{w}$, \label{itm:rem:val:inv}

		\item $\val(C) \leq \vec{a} \cdot \vec{w}$, \label{itm:rem:val:dec}

		\item $|C| = C(N) + C(B) + |\vec{w}|$, \label{itm:rem:config:size}

		\item $C(N) \geq L(N)$ and $C(B) \geq L(B)$, \label{itm:rem:preservation}

		\item $C(N_x) + C(x) = \vec{w}(x)$ for every $x \in
		X$. \label{itm:rem:preservation:x}
	\end{enumerate}
\end{proposition}

\parag{Auxiliary propositions} We say that a configuration $C$ is
\emph{clean} if for every $p, q \in P_X$ with $\val(p) = \val(q)$ and $\val(p)
\not= 2^n$, it holds that $C(\{p, q\}) \leq 1$. Intuitively, in a clean configuration
no agent can be promoted to a higher power of 2.

We show that any configuration can be cleaned using only permanent transitions.
This implies that once the dynamic initialization has terminated, every fair
execution visits clean configurations infinitely often.

\begin{proposition}\label{prop:rem:cleaning}
	For every initialization sequence $\pi$ such that $L' \trans{\pi} C$
	for some $L' \succeq L$, there exists a clean configuration $D$
	such that $C \trans{T_{\infty}^*} D$.
\end{proposition}
\begin{proof}
	If $C$ is clean, then we pick $D \defeq C$. Otherwise, we claim there
	exists a configuration $C'$ such that $C \trans{*} C'$ and $C(P_X) >
	C'(P_X)$. If $C'$ is clean, then we are	done. Otherwise, this process
	is repeated until a clean configuration $D$ has been reached. This must
	terminate as the number of agents in $P_X$ cannot become negative.

	Let us prove the claim. If $C$ is not clean, then $C(\{p, q\}) \geq 2$
	for some $p, q \in P_X$ such that $\val(p) = \val(q)$ and $\val(p)
	\not= 2^n$. By \cref{prop:rem:prop}~\eqref{itm:rem:preservation}, we have
	$C(N) \geq L(N) \geq 2$ and hence it is possible to consecutively
	fire at least two $\mathsf{swap}$ transitions. Note that they do not
	change the amount of agents in $P_X$. For this reason, we may assume
	without loss of generality that $p = q = \q{2^i}$ for some $0 \leq i \leq
	n$. Therefore, firing transition $\mathsf{up}_i$ decreases
	$C(P_X)$ by one.
\end{proof}

We now bound the number of agents in states from $X \cup P_X$ in a
clean configuration.

\begin{proposition} \label{prop:rem:top:small}
	For every initialization sequence $\pi$ with effective input $\vec{w}$
	such that $L' \trans{\pi} C$ for some $L' \succeq L$, if $C$ is clean,
	then $C(X) + C(P_X) \leq |\vec{w}| + n$.
\end{proposition}

\begin{proof}
	Let $S_{2^n} \defeq \{q \in P_X : \val(q) = 2^n\}$. Let $\vec{u} \in \N^X$
	be such that $\vec{u}(x) \defeq C(x)$ for every $x \in X$.
	Note that $|\vec{u}| = C(X)$, and that $\vec{u} \leq \vec{w}$ by
	\cref{prop:rem:prop}~\eqref{itm:rem:preservation:x}.
	Since $C$ is clean, we have $C(P_X \setminus S_{2^n}) \leq n$.
	Thus, it suffices to show	that $C(S_{2^n}) \leq |\vec{w}| - |\vec{u}|$.
	Suppose this is not	the case. This yields a contradiction:
	\begin{align*}
		\val_{P_X}(C)
		&\geq 2^n \cdot C(S_{2^n}) \\
		%
		&> 2^n \cdot (|\vec{w}| - |\vec{u}|)
		&& \text{(by assumption)} \\
		%
		&\geq \vec{a} \cdot (\vec{w} - \vec{u}) && \text{(since $2^n >
			\norm{\vec{a}}$ and $\vec{w} \geq \vec{u}$)} \\
		%
		&= \vec{a} \cdot \vec{w} - \vec{a} \cdot \vec{u} \\
		%
		&\geq \val(C) - \val_X(C)
		&& \text{(by Prop.~\ref{prop:rem:prop}~\eqref{itm:rem:val:dec} and
			def.\ of $\vec{u}$)} \\
		%
		&= \val_{P_X}(C)
		&& \text{(by def.\ of $\val$)} \qedhere
	\end{align*}
\end{proof}

The following corollary shows that the number of agents in state
$\q{0}$ can always be increased back to at least $n$. This will later
be useful in arguing that the number of agents in $X$ can eventually
be decreased to zero.

\begin{corollary} \label{cor:rem:enough:zero}
	For every initialization sequence $\pi$ with effective input $\vec{w}$ such
	that $L' \trans{\pi} C$ for some $L' \succeq L$, there exists a clean
	configuration $D$ such that $C \trans{T_{\infty}^*} D$ and $D(\q{0}) \geq n$.
\end{corollary}

\begin{proof}
	By \cref{prop:rem:cleaning}, there exist a clean configuration $C'$ such
	that $C \trans{\pi' \in T_\infty^*} C'$. Let us first prove that $C'(Z_X) \geq n$.
	Note that $\pi\pi'$ is an initialization sequence with effective input
	$\vec{w}$ such that $L \trans{\pi\pi'} C'$. Thus:
	\begin{align*}
		C'(Z_X)
		&= |C'| - C'(X) - C'(P_X) - C'(B)
		&& \text{(by def.\ of $Q$)} \\
		%
		&= (C'(N) + C'(B) + |\vec{w}|) - C'(X) - C'(P_X) - C'(B)
		&& \text{(by Prop.~\ref{prop:rem:prop}~\eqref{itm:rem:config:size})} \\
		%
		&\geq (L(N) + C'(B) + |\vec{w}|) - C'(X) - C'(P_X) - C'(B)
		&& \text{(by Prop.~\ref{prop:rem:prop}~\eqref{itm:rem:preservation})} \\
		%
		&\geq (L(N) + C'(B) + |\vec{w}|) - (|\vec{w}| + n) - C'(B)
		&& \text{(by Prop.~\ref{prop:rem:top:small})} \\
		%
		&= L(N) - n \\
		%
		&\geq n
		&& \text{(by def.\ of $L$)}
	\end{align*}
	Now, by \cref{prop:rem:prop}~\eqref{itm:rem:preservation}, we have
	$C'(N) \geq L(N) \geq n$. Thus, using $\mathsf{swap}$ transitions, we
	can swap $n$ agents from $Z_X$ to $\q{0}$. This way, we obtain a
	configuration $D$ such that $C' \trans{T_{\infty}^*} D$ and $D(\q{0}) \geq
	n$. We are done since $\mathsf{swap}$ transitions preserve
	cleanness.
\end{proof}
We now show that, once dynamic initialization has terminated, fair executions
stabilize to configurations of a certain ``normal form''.

\begin{proposition}\label{prop:remainder:stabilize}
	For every initialization sequence $\pi$ with effective input $\vec{w}$ such that
	$L' \trans{\pi} C$ for some $L' \succeq L$ and for every fair execution
	$\sigma$ of $\PP_\infty$ starting from $C$, there exist
	$i \in \N, r \geq 0$ such that
	\begin{enumerate}
		\item $\sigma_i(X) = \sigma_{i+1}(X) = \cdots = 0$,

		\item $\val(\sigma_i) = \val(\sigma_{i+1}) = \cdots =
		r < m$.
	\end{enumerate}
\end{proposition}

\begin{proof}
	For the sake of contradiction, assume there exist infinitely many
	indices $j$ such that $\sigma_j(X) > 0$. Let $j \in \N$ be such an
	index. By \cref{cor:rem:enough:zero}, there exists a configuration $C_j$
	such that $\sigma_j \trans{T_{\infty}^*} C_j$ and $C_j(\q{0}) \geq n$. Hence,
	there exists $x \in X$ such that transition $\mathsf{add}_x$ is
	enabled in $C_j$. Since this holds for infinitely many indices and
	since $X$ is finite, fairness implies that some $\mathsf{add}$
	transition can be enabled infinitely often and hence occurs
	infinitely often along $\sigma$. This is impossible since the number
	of agents in $X$ cannot be increased by any transition in $T_\infty$,
	and thus would eventually drop below zero.
	Therefore, there exists $h \in \N$ such that
	$\sigma_h(X) = \sigma_{h+1}(X) = \cdots = 0$.

	Transitions $\mathsf{modulo_{\q{t}}}$ and $\mathsf{modulo_{\q{f}}}$
	reduce the value of a configuration by $m > 0$.
	$\mathsf{add}$ transitions are disabled in every configuration $\val(\sigma_{i})$
	with $i \geq h$ and all other transitions in $T_\infty$
	do not change the value of a configuration.
	Moreover, the value of a configuration is always non-negative.
	Thus, there exist $i \geq h$, $r \geq 0$ such that
	$\val(\sigma_{i}) =\val(\sigma_{i+1}) = \cdots = r$.

	For the sake of contradiction, assume that $r \geq m$.
	As the execution is infinite but there are only finitely many
	different configurations for a fixed number of agents, there
	exists a configuration $D$ with $D(X) = 0$ and $\val(D) = r$
	that occurs infinitely often in $\sigma$.
	We claim that $D$ can reach a configuration that enables a
	$\mathsf{modulo}$ transition.
	This claim, together with fairness, yields a contradiction because
	the overall value would drop below $r$.

	Let us prove the claim. By \cref{cor:rem:enough:zero}, we have $D \trans{*} D'$
	where $D'$ is clean and $D'(\q{0}) \geq n$.
	Furthermore, $D'(X) = 0$ as $D(X) = 0$ and the number of agents in $X$ cannot be increased.
	By \cref{prop:rem:prop} \eqref{itm:rem:preservation}, we have $D'(B) \geq L(B) = 1$.
	Thus, it suffices to show that $D' \trans{T_{\infty}^*} D''$ for some $D'' \geq \mathrm{rep}(m)$.

	If $\val(D') = m$, then $D'$ contains precisely the binary representation of $m$,
	because $D'$ is clean and $D'(X) = 0$.
	Hence, $D' \geq \mathrm{rep}(m)$. Thus, assume $\val(D') > m$.
	Let $0 \leq d \leq n$ be the largest exponent for which there exists a state
	$q \in P_X$ such that $D(q) > 0$, $\val(q) = 2^d$ and $d \not\in \mathrm{bits}(m)$.
	Since $D'(\q{0}) \geq n \geq d$, the sequence of transitions $\mathsf{down}_d \cdot
	\mathsf{down}_{d-1} \cdots \mathsf{down}_1$ can be fired from $D'$, which yields a
	configuration $D'' \geq \mathrm{rep}(m)$.
\end{proof}

\parag{Main proof} We are now ready to prove that $\PP_{\text{rem}}$
works as intended.

\begin{theorem}
	$\PP_{\text{rem}}$ computes $\varphi$ under reversible dynamic initialization.
\end{theorem}

\begin{proof}
	We first show that $\PP_{\text{rem}}$ is input reversible, and then
	that it correctly computes $\varphi$.

	\medskip\noindent\emph{Input reversibility.} Let $\pi$ be an
	initialization sequence with effective input $\vec{w}$ such that
	$L' \trans{\pi} C$ for some $L' \succeq L$. By
	\cref{prop:rem:prop}~\eqref{itm:rem:preservation:x}, we have $C(I(x)) =
	C(x) = \vec{w}(x) - C(N_x) \leq \vec{w}(x)$ for every $x \in X$,
	which proves the first required property.

	For every configuration $C$, let $\mathrm{false}(C) \defeq D$ where $D(t)
	\defeq 0$, $D(f) \defeq C(t) + C(f)$ and $D(q) \defeq C(q)$ for
	every $q \in Q \setminus \{f, t\}$. Observe that for every
	configuration $C$, the following holds:
	\begin{align}
		C \trans{\mathsf{reset}^{C(\q{t})}} \mathrm{false}(C) \text{ and }
		\mathrm{false}(C) \in [C].\label{eq:rem:reset:false}
	\end{align}
	It remains to show that if $C \trans{\pi_\triangleright \in T^*} D$
	and $D' \in [D]$, then $D' \trans{\pi_\triangleleft \in T^*} C'$ for
	some $C' \in \DiEq{C}$. By~\ref{eq:rem:reset:false}, it is enough to
	argue that $\mathrm{false}(D) \trans{T^*} \mathrm{false}(C)$.

	Let $C_i \trans{t_i} C_{i+1}$ be the $i^\text{th}$ step of
	$\pi_\triangleright$. We argue that $\mathrm{false}(C_{i+1}) \trans{t_i'}
	\mathrm{false}(C_i)$ for some $t_i' \in T \cup \{\varepsilon\}$. By
	induction, this implies $\mathrm{false}(D) \trans{T^*} \mathrm{false}(C)$ as
	desired. If $t_i$ is an $\mathsf{equal}$, $\mathsf{false}$ or
	$\mathsf{reset}$ transition, then we already have $\mathrm{false}(C_{i+1}) =
	\mathrm{false}(C_i)$. Otherwise we revert the step as follows, where ``$s
	\mapsto u$'' indicates that if $t_i = s$, then we reverse it with
	$t_i' = u$:
	\begin{align*}
		\mathsf{add}_x &\mapsto \mathsf{add}_{x,\q{f}}^{-1}
		&& \text{for every $x \in X$,} \\
		%
		\mathsf{add}_{x,q}^{-1} &\mapsto \mathsf{add}_x
		&& \text{for every $x \in X$ and $q \in B$,} \\
		%
		\mathsf{up}_i &\mapsto \mathsf{down}_{i+1}
		&& \text{for every $0 \leq i < n$,}\\
		%
		\mathsf{down}_i &\mapsto \mathsf{up}_{i-1}
		&& \text{for every $0 < i \leq n$,} \\
		%
		\mathsf{modulo}_{q} &\mapsto \mathsf{modulo}_{\q{f}}^{-1}
		&& \text{for every $q \in B$,} \\
		%
		\mathsf{modulo}_{q}^{-1} &\mapsto \mathsf{modulo}_{\q{f}}
		&& \text{for every $q \in B$,}\\
		%
		\mathsf{swap}_{p, q}^x &\mapsto \mathsf{swap}_{q, p}^x
		&& \text{for every $p, q \in N$ and $x \in X$.}
	\end{align*}
	Note that $t_i'$ is not the exact reverse transition of $t_i$, as it
	may differ over $B$. Indeed, $t_i'$ may require an agent in state
	$\q{f}$, which may not have been produced by $t_i$. However, this is
	not an issue since, by definition of $\mathrm{false}$ and by
	\cref{prop:thr:prop}~\eqref{itm:preservation}, we have:
	$$\mathrm{false}(C_{i+1})(\q{f}) = C_{i+1}(B) \geq L(B) > 0.$$ Thus, we have
	$\mathrm{false}(C_{i+1}) \trans{t_i'} \mathrm{false}(C_i)$ as desired, which
	completes the proof.

	\medskip\noindent\emph{Correctness.} Let $\pi$ be an initialization
	sequence with effective input $\vec{w}$ such that $L' \trans{\pi} C$
	for some $L' \succeq L$.
	Let $\sigma$ be a fair execution of $\PP_\infty$ starting from $C$.
	By \cref{prop:remainder:stabilize}, there exist $i \in \N, r \geq 0$ such that:
	\begin{enumerate}[(a)]
		\item $\sigma_i(X) = \sigma_{i+1}(X) = \cdots = 0$, \label{itm:rem:input:stab}

		\item $\val(\sigma_i) = \val(\sigma_{i+1}) = \cdots =
		r < m$. \label{itm:rem:val:stab}
	\end{enumerate}

	Let us first show that $O(\sigma) \in \{0, 1\}$. We make a case distinction on
	whether $v \geq b$.\medskip

	\noindent\emph{Case $r \geq b$.} We show that $O(\sigma) = 1$. Note that $r < m$.
	The $\mathsf{modulo}$ transitions reduce the overall value by $m$.
	As the value of a configuration is never negative, no $\mathsf{modulo}$ transition
	can be fired again.
	Thus, it suffices to show that $\sigma_j(\q{f}) = 0$ for some $j \geq i$.
	If $\sigma_i(\q{f}) = 0$ then we are done.
	For the sake of contradiction, suppose this is not the case.
	As $\sigma$ is infinite but there are only finitely many different configurations
	for a fixed number of agents, there exists a configuration $D$ that occurs infinitely
	often in $\sigma$ such that $D(X) = 0$, $\val(D) = r$ and $D(\q{f}) > 0$.
	We claim that $D$ can reach a configuration that enables the transition $\mathsf{equal}$.
	This claim, together with fairness, yields a contradiction because $\mathsf{equal}$
	can move all agents form state $\q{f}$ to state $\q{t}$.

	Let us prove the claim.
	By \cref{cor:rem:enough:zero}, we have $D \trans{T_{\infty}^*} D'$ where $D'$ is clean and
	$D'(\q{0}) \geq n$.
	Furthermore, $D'(X) = 0$ as $D(X) = 0$ and the number of agents in $X$ cannot be
	increased by transitions in $T_\infty$.
	We show that $D' \trans{*} D''$ for some $D'' \geq \mathrm{rep}(m)$.
	If $\val(D') = m$, then $D'$ contains precisely the binary representation of $m$,
	because $D'$ is clean and $D'(X) = 0$.
	Hence, $D' \geq \mathrm{rep}(m)$. Thus, assume $\val(D') > m$.
	Let $0 \leq d \leq n$ be the largest exponent for which there exists a state $q \in P_X$
	such that $D(q) > 0$, $\val(q) = 2^d$ and $d \not\in \mathrm{bits}(m)$.
	Since $D'(\q{0}) \geq n \geq d$, the sequence of transitions
	$\mathsf{down}_d \cdot \mathsf{down}_{d-1} \cdots \mathsf{down}_1$ can be fired from $D'$,
	which yields a configuration $D'' \geq \mathrm{rep}(m)$.
	If $D''(\q{f}) = 0$, then the claim holds because the only transition that reduces the
	number of agents in state $\q{f}$ is transition $\mathsf{equal}$.
	If $D''(\q{f}) > 0$, then the claim holds because $D''$ enables $\mathsf{equal}$. \medskip

	\noindent\emph{Case $r < b$.} We show that $O(\sigma) = 0$. First note
	that $\mathsf{equal}$ is disabled in $\sigma_j$ for every
	$j \geq i$, as otherwise we would have
	$\sigma_j \geq \mathrm{rep}(b)$ which implies that $r
	= \val(\sigma_j) \geq b$. Thus, it suffices to show that there
	are infinitely many indices $j$ such that $\sigma_j(\q{f}) >
	0$. Indeed, if this is the case, then, by fairness, $\mathsf{false}$
	permanently moves all agents in state $\q{t}$ to state $\q{f}$.

	For the sake of contradiction, suppose the claim does not hold.
	Let $\sigma' \defeq \pi\sigma$. Let $j \in \N$ be the largest index
	such that $\sigma_j'(\q{f}) > 0$.
	Note that this configuration exists as $\sigma_0' = L' \succeq L$ and $L(\q{f}) > 0$.
	The only transition that reduces the number of agents in $\q{f}$ is $\mathsf{equal}$.
	Thus, $\sigma_j' \trans{\mathsf{equal}} \sigma_{j+1}'$ and $\val(\sigma_j') \geq b$.
	As finally, $r < b$, some $\mathsf{modulo}$ or $\mathsf{add}^{-1}$ transition
	must be fired in $\sigma'_{j'}$ for some $j' > j$.
	In both cases there is afterwards an agent in state $\q{f}$.
	This contradicts the maximality of $j$. \medskip

	We are done proving $O(\sigma) \in \{0, 1\}$.
	It remains to argue that $O(\sigma) = \varphi(\vec{w})$.
	We have $m > r = \val(\sigma_i) \equiv_m \vec{a} \cdot \vec{w}$
	by \cref{prop:rem:prop}~\eqref{itm:rem:val:inv}.
	If $\vec{a} \cdot \vec{w} \geq b~(\text{mod } m)$, then $r \geq b$ and
	hence $O(\sigma) = 1$, which is correct.
	If $\vec{a} \cdot \vec{w} < b~(\text{mod } m)$, then $r < b$ and
	hence $O(\sigma) = 0$, which is also correct.
\end{proof}

\section{Proofs of Section \ref{sec:large}: Protocols for large populations} \label{app:large}

\subsection{Proof of Theorem \ref{thm:remove:helpers}}\label{app:rem:helpers}
\input{helpers}

\subsection{Proof of Proposition \ref{prop:mult}}\label{app:mult}
\input{mult}

\subsection{Proof of Theorem \ref{thm:atomic:mult:helpers}}\label{app:atomic:mult}
\input{atomic-parallel}

\subsection{Proof of Theorem \ref{thm:atomic:helpers}}\label{app:threshold}
\input{threshold}
\input{remainder}

\section{Equivalence of simple and standard population protocols} \label{appendix_output}
Recall that a simple population protocol (SPP), has two unique states
$\q{f}, \q{t} \in Q$ with outputs $O(\q{f}) = 0$ and $O(\q{t}) = 1$ and all other states $q$ have output $O(q) = \bot$.

In the standard definition of population protocols used in the literature, all states $q$ have an output
$O(q) \in \{0,1\}$. In this section we call such a protocol a \emph{full output population protocols} (FOPP). In a FOPP,  a configuration $C$ is a consensus configuration if
$O(p) = O(q)$ for every $p, q \in \supp{C}$. If $C$ is a consensus configuration, then its output $O(C)$ is the unique output of its states, otherwise it is $\bot$.
An execution $\sigma = C_0 C_1 \cdots$ stabilizes to $b \in \{0, 1\}$
if $O(C_i) = O(C_{i+1}) = \cdots = b$ for some $i \in \mathbb{N}$.
The output of $\sigma$ is $O(\sigma) = b$ if it stabilizes to $b$, and $O(\sigma)= \bot$ otherwise.
A consensus configuration $C$ is
stable if every configuration $C'$
reachable from $C$ is a consensus configuration such that
$O(C') = O(C)$. It is easy to see that a fair execution of a FOPP stabilizes to $b \in \{0, 1\}$ if and only if it contains a stable configuration whose output is $b$.

A FOPP $\PP$ computes a predicate $\varphi \colon
\N^X \to \{0, 1\}$ if for every $\vec{v} \in \N^X$ every fair
execution $\sigma$ starting from $C_{\vec{v}}$ stabilizes to $\varphi(\vec{v})$.

In the rest of the section we show that every FOPP has an equivalent SPP, and vice versa.
Both translations have linear blow-up.

\parag{FOPP $\rightarrow$ SPP}
Let $\PP = (Q, T, L, X, I, O)$ be a FOPP computing a predicate $\varphi$.  We obtain a SPP protocol $\PP'$ by adding two output states $\{\q{f},\q{t}\}$ to $\PP$, plus a new state $\q{\bot}$.
The output function of $\PP'$ is the mapping $O': q \mapsto (0 \text{ if } q = \q{f} \text{ else } 1
\text{ if } q = \q{t} \text{ else } \bot)$. The set $L'$ of leaders of $\PP'$ is obtained by
adding one leader to $L$, initially in state $\q{\bot}$. Finally, the set $T'$ of transitions is obtained by adding to $T$, for all $b \in \{\q{f},\q{t},\q{\bot}\}$, a transition
$\multiset{q, b} \mapsto \multiset{q, \q{f}}$ for every state $q \in Q$ such that $O(q)=0$ and
a transition $\multiset{q, b} \mapsto \multiset{q, \q{t}}$ for every state $q \in Q$ such that $O(q)=1$.

We show that $\PP'$ also computes $\varphi$.
Let $C'_0 C'_1 \cdots$ be a fair execution of $\PP'$ from $C_0'$. Projecting it onto the set of states of $\PP$ yields a fair execution of $\PP$. Since $\PP$ computes $\varphi$, the execution outputs some $b \in \{0,1\}$. Assume that $b=0$ (the case $b=1$ is symmetric).
Let $i \in \N$ such that the output of every state populated by $C_j$ is $b$ for every $j \geq i$.
Now, no matter the state populated by the additional leader in $C_j$ (which is one of $\{\q{f},\q{t},\q{\bot}\}$), the transition $\multiset{q, b} \mapsto \multiset{q, \q{f}}$
is enabled for every state $q$ such that $C_j(q)=0$. By fairness, the leader will thus eventually move to state $\q{f}$ and it will be stuck there, and $\PP'$ outputs $0$ as well.

\medskip
\parag{SPP $\rightarrow$ FOPP}
Let $\PP = (Q, T, L, X, I, O)$ be an SPP with output states $\q{f}, \q{t} \in Q$ computing a predicate $\varphi$. Let $\PP'$ be the FOPP with two disjoint copies $Q_0,Q_1$ of $Q$ as states. For $a \in Q$, let $a_b$ denote the copy of $a$ in $Q_b$, for $b \in \{0,1\}$.
We define $O'(q)=b$ for all $q \in Q_b$.
The set $T'$ of transitions is the following. First,
for every transition $\multiset{x, y} \mapsto \multiset{z, u}$ of $T$, the set $T'$
contains a transition $\multiset{x_b, y_c} \mapsto \multiset{z_d, u_e}$
for every $b,c,d,e \in \{0,1\}$ such that if $b=c$ then $d=e=b=c$.
Further, $T'$ also contains a set $T''$ of transitions consisting of
$\multiset{\q{f}_1} \mapsto \multiset{\q{f}_0}$,
$\multiset{\q{t}_0} \mapsto \multiset{\q{t}_1}$,
$\multiset{a_1,\q{f}_0} \mapsto \multiset{a_0,\q{f}_0}$
and
$\multiset{a_0,\q{t}_1} \mapsto \multiset{a_1,\q{t}_1}$
for every $a \in Q$.

The input mapping and leader multiset of $\PP'$ are the ``0'' copies of the input mapping and leader multiset of $\PP$.
Hence, for any input $\vec{v}$ the initial configuration $C'_{\vec{v}}$ of $\PP'$ is the ``0'' copy of the initial configuration $C_{\vec{v}}$ in $\PP$.

We show that $\PP'$ also computes $\varphi$. Let $C'_0 C'_1 \cdots$ be a fair execution of $\PP'$ from $C'_0$. For every $i \in \mathbb{N}$, let $C_i=\pi(C'_i)$, where $\pi$ is the mapping defined by $\pi(q_b)=b$ for every $q_b \in Q_0 \cup Q_1$.
It is easy to see that $C_0 C_1 \cdots$
is a fair execution of $\PP$, with possible repetitions $C_i=C_{i+1}$
when the transition from $C'_i$ to $C'_{i+1}$ is in $T''$.
Hence $C_0 C_1 \cdots$ eventually stabilizes to an output $b$.
Assume that $b=0$ (the case $b=1$ is symmetric).
By fairness, because of the transitions
$\multiset{\q{f}_1} \mapsto \multiset{\q{f}_0}$,
and
$\multiset{a_1,\q{f}_0} \mapsto \multiset{a_0,\q{f}_0}$, the execution $C'_0 C'_1 \cdots$ eventually reaches, and gets trapped in, configurations of $\mathbb{N}^{Q_0}$. So the execution also stabilizes to the output $0$.

\section{Proof of Theorem \ref{thm:hardness:PA}} \label{appendix_PA}

\thmHardnessPA*

\begin{proof}
 We show that if such an algorithm runs in time $2^{p(n)}$ for some polynomial $p$, then the validity problem for PA formulas  is in EXPTIME, contradicting the fact that its complexity lies between 2-NEXP and 2-EXPSPACE~\cite{Berman80, Haase14}. Recall that the validity problem for PA formulas asks whether a given sentence, i.e., a formula without free variables, is true or false.

Let $\varphi$ be a sentence of PA, and let $n \defeq |\varphi|$. Consider the formula $\psi(x) \defeq (x \geq 2) \wedge \varphi$ (notice that the smallest possible size of a population is 2). Clearly, $\varphi$ is valid if{}f $\psi(2)$ holds. Assume there exists an algorithm that on input $\psi$ executes at most $f(n)$ steps and outputs a population protocol $\PP$ that computes $\psi$. Clearly, $\PP$ has at most $\O(f(n))$ states, and $\varphi$ is valid if{}f $\PP$ computes 1 for input $x = 2$.

Let $C$ be the initial configuration of $\PP$ for input $x = 2$. A configuration of $\PP$ with two agents can be stored in space $\O(\log f(n))$, and so $C$, and every configuration reachable from it, can be stored using $\O(\log f(n))$ space. Protocol $\PP$ computes $1$ from $C$ if{}f there exists a configuration $C'$ such that:
\begin{enumerate}[(i)]
\item $C \trans{*} C'$,

\item $C'$ has output 1,

\item for every configuration $C''$, if  $C' \trans{*} C''$, then $C'' \trans{*} C'$.
\end{enumerate}

Observe that (i)-(iii) can be expressed in FO(TC), \ie\ first-order logic with transitive-closure. By Immermann's theorem, deciding (i)-(iii) belongs to NSPACE($\log f(n)$)~\cite{Immerman99}, and so it can be solved in $\O(f(n)^k)$ deterministic time for some $k \geq 1$. Consequently, if there exists a polynomial $p$ such that $f \in \O(2^{p(n)})$, then the validity of $\varphi$ can be decided in time $2^{\O(p(n))}$, and so the validity problem for PA is in EXPTIME. The latter is impossible by the time hierarchy theorem.
\end{proof}

\section{Proofs of Section \ref{sec:small}: Protocols for small populations} \label{app:small}

\subsection{Proof of Theorem \ref{thm:removing:leaders}}
\input{construction-leaderless-small}

\subsection{Proof of Theorem \ref{lemma:halting-conj-disj}} \label{app:construction-halting-conj-dis}
\input{construction-halting-conj-dis}

\subsection{Proof of Theorem \ref{thm:halting:threshold}}\label{app:constr-halting-threshold}
\input{construction-halting-threshold}

\subsection{From protocols with helpers to leaderless protocols}
\label{subsec:helpers}

Intuitively, a protocol with helpers is a protocol with leaders satisfying an additional
property: adding more leaders does not change the predicate computed
by the protocol. Formally, let $\PP = (Q, T, L, X, I, O)$ be a population
protocol computing a predicate $\varphi$. We say that $\PP$ is a
protocol \emph{with helpers} if for every $L' \succeq L$ the protocol
$\PP' = (Q, T, L', X, I, O)$ also computes $\varphi$, where $L'
\succeq L \; \defeq \; \forall q \in Q \colon (L'(q) = L(q)=0 \vee
L'(q) \geq L(q) > 0)$. If $|L| = \cutoffvar$, then we say that $\PP$ is a protocol \emph{ with $\cutoffvar$ helpers}.

\begin{restatable}{theorem}{thmRemoveHelpers} \label{thm:remove:helpers}
  Let $\PP = (Q, T, L, X, I, O)$ be a
  $\kwayvar$-way population protocol with $\cutoffvar$-helpers
  computing some predicate $\varphi$. There exists a 2-way leaderless
  population protocol with $\O(\cutoffvar \cdot |X| + (\kwayvar \cdot |T|+|Q|)^2)$ states that computes $(|\vec{v}|  \geq \cutoffvar) \rightarrow \varphi(\vec{v})$.
\end{restatable}

\begin{proof}[Proof sketch]
  By~\cite[Lemma~3]{BEJ18}, $\PP$ can be transformed into a 2-way
  population protocol (with helpers\footnote{Lemma~3 of~\cite{BEJ18}
    deals with leaders and not the more specific case of
    helpers. Nonetheless, computation under helpers is preserved as
    the input mapping of $\PP$ remains unchanged in the proof of the
    lemma.})  computing the same predicate $\varphi$, and with at most
  $|Q| + 3\kwayvar \cdot |T|$ states. Thus, we assume $\PP$ to be 2-way in
  the rest of the sketch.

  For simplicity, assume $X = \{x\}$ and $L = \multiset{3 \cdot q, 5
    \cdot q'}$; that is, $\PP$ has 8 helpers, and initially 3 of them
  are in state $q$, and $5$ are in $q'$. We describe a leaderless
  protocol $\PP'$ that simulates $\PP$ for every input $\vec{v}$ such
  that $|\vec{v}| \geq |L| = \cutoffvar$. Intuitively, $\PP'$ runs in two phases:
  \begin{itemize}
  \item In the first phase each agent gets assigned a number between 1
    and 8, ensuring that each number is assigned to at least one agent
    (this is the point at which the condition
	 $|\vec{v}| \geq \cutoffvar$ is needed).
	 At the end of the phase, each agent is in a state of the
    form $(x, i)$, meaning that the agent initially represented one
    unit of input for variable $x$, and that it has been assigned
    number $i$.  To achieve this, initially every agent is placed in
    state $(x, 1)$. Transitions are of the form $ \multiset{ (x, i),
      (x, i)} \mapsto \multiset{ (x, i+1), (x, i)}$ for every $1 \leq
    i \leq 7$. The transitions guarantee that all but one agent is
    promoted to $(x, 2)$, all but one to $(x, 3)$, etc. In other
    words, one agent is ``left behind'' at each step.

  \item In the second phase, an agent's state is a multiset:
    agents in state $(x, i)$ move to state
    $\multiset{I(x), q}$ if $1 \leq i \leq 3$, and to state
    $\multiset{I(x), q'}$ if $4 \leq i \leq 8$.  Intuitively, after
    this move each agent has been assigned two jobs: simultaneously
    simulate a regular agent of $\PP$ starting at state $x$,
    \emph{and} a helper of $L$ starting at state $q$ or $q'$. Since in
    the first phase each number is assigned to at least one agent,
    $\PP'$ has at least 3 agents simulating helpers in state $q$, and
    at least 5 agents simulating helpers in state $q'$. There may be
    many more helpers, but this is harmless, because, by definition,
    additional helpers do not change the computed
    predicate. \smallskip

    The transitions of $\PP'$ are designed according to this double
    role of the agents of $\PP'$. More precisely, for all multisets
    $\vec{p}, \vec{q}, \vec{p}', \vec{q}'$ of size two,
    $\multiset{\vec{p}, \vec{q}} \mapsto \multiset{\vec{p}',
      \vec{q}'}$ is a transition of $\PP'$ if{}f $(\vec{p} + \vec{q})
    \trans{} (\vec{p}' + \vec{q}')$ in $\PP$.
    \qedhere
  \end{itemize}
\end{proof}

\subsection{From multi-output protocols to protocols with helpers}
\label{subsec:finsets}

A \emph{$k$-output population protocol} is a tuple $\mathcal{Q} = (Q,
T, L, X, I, O)$ where $O \colon [k] \times Q \to \{0, 1, \bot\}$ and
$\mathcal{Q}_i \defeq (Q, T, L, X, I, O_i)$ is a population protocol
for every $i \in [k]$, where $O_i$ denotes the mapping such that
$O_i(q) \defeq O(i, q)$ for every $q \in Q$. Intuitively, since each
$\mathcal{Q}_i$ only differs by its output mapping, $\mathcal{Q}$ can
be seen as a single population protocol whose executions have $k$
outputs. More formally, $\mathcal{Q}$ \emph{computes} a set of
predicates $P = \{\varphi_1, \varphi_2, \ldots, \varphi_k\}$ if
$\mathcal{Q}_i$ computes $\varphi_i$ for every $i \in
[k]$. Furthermore, we say that $\mathcal{Q}$ is \emph{simple} if
$\mathcal{Q}_i$ is simple for every $i \in [k]$. Whenever the number
$k$ is irrelevant, we use the term \emph{multi-output population
  protocol} instead of $k$-output population protocol.

\begin{restatable}{proposition}{PropMult}
\label{prop:mult}
Assume that every finite set $A$ of {\em atomic} predicates is computed by some
$|A|$-way multi-output protocol with $\O(|A|^3)$ helpers and states, and
$\O(|A|^5)$ transitions. Every
QFPA predicate $\varphi$ is computed by some
simple $|\varphi|$-way protocol with
$\O(|\varphi|^3)$ helpers and states, and
$\O(|\varphi|^5)$ transitions.
\end{restatable}

\begin{proof}[Proof sketch]
Consider a binary tree decomposing the boolean operations of $\varphi$.
We design a protocol for $\varphi$ by induction on the height of the tree.

The case where the height is $0$, and $\varphi$ is atomic, is trivial.
We sketch the induction step for the case where the root is labeled with $\land$, that is $\varphi = \varphi_1 \land \varphi_2$, the other cases are similar.
By induction hypothesis, we have simple protocols $\PP_1,\PP_2$ computing $\varphi_1,\varphi_2$, respectively. Let $\q{t}_j,\q{f}_j$ be the output states of $\PP_j$ for $j \in \{1,2\}$ such that $O_j(\q{t}_j) = 1$ and $O_j(\q{f}_j) = 0$. We add two new states $\q{t}, \q{f}$ (the output states of the new protocol) and an additional helper starting in state $\q{f}$. To compute $\varphi_1 \land \varphi_2$ we add the following transitions for every $b_1 \in \{\q{t}_1,\q{f}_1\}, b_2 \in \{\q{t}_2,\q{f}_2\}$, and $b \in \{\q{t},\q{f}\}$:
$\multiset{b_1,b_2,b} \mapsto \multiset{b_1,b_2,\q{t}}$ if $b_1 = \q{t}_1 \land b_2 = \q{t}_2$, and $\multiset{b_1,b_2,b} \mapsto \multiset{b_1,b_2,\q{f}}$ otherwise.
The additional helper computes the conjunction as desired.
\end{proof}

\subsection{From reversible dynamic initialization to multi-output protocols}
\label{subsec:finat}

Let $P = \{\varphi_1, \ldots, \varphi_k\}$ be a set of $k \geq 2$
atomic predicates of arity $n \geq 1$ over a set $X = \{x_1, \ldots, x_n\}$ of variables.
We construct a multi-output protocol $\PP$ for $P$ of size
$\poly(|\varphi_1|+ \cdots + |\varphi_k|)$.

Let $\PP_1, \ldots, \PP_k$ be protocols for
$\varphi_1, \ldots, \varphi_k$. Observe that $\PP$ cannot be a ``product protocol'' that executes $\PP_1, \ldots, \PP_k$ synchronously. Indeed, the states of such a $\PP$ are tuples $(q_1, \ldots, q_k)$ of states of $\PP_1, \ldots, \PP_k$,  and so $\PP$ would have exponential size in $k$.
Further, $\PP$ cannot execute $\PP_1, \ldots, \PP_k$  asynchronously in parallel, because, given an input $\vec{x} \in \N^n$, it must dispatch $k \cdot \vec{x}$ agents ($\vec{x}$ to the input states of each $\PP_j$), but it only has $\vec{x}$.
Such a $\PP$ would need $(k-1)|\vec{x}|$ helpers, which is not possible, because a protocol of size  $\poly(|\varphi_1|+ \cdots + |\varphi_k|)$ can only use $\poly(|\varphi_1|+ \cdots + |\varphi_k|)$ helpers, whatever the input $\vec{x}$.

The solution is to use a more sophisticated parallel asynchronous computation. Consider two copies of inputs, denoted
$\overline{X} = \{\overline{x}_1, \ldots, \overline{x}_n\}$ and $\underline{X} = \{\underline{x}_1, \ldots, \underline{x}_n\}$.
For each predicate $\varphi$ over $X$,
consider predicate $\tilde{\varphi}$ over
$\overline{X} \cup \underline{X}$
satisfying $\tilde{\varphi}(\overline{\vec{x}},\underline{\vec{x}}) =
\varphi(k\overline{\vec{x}}+\underline{\vec{x}})$
for every $(\overline{\vec{x}},\underline{\vec{x}}) \in \N^{\overline{X} \cup \underline{X}}$.
We obtain
$\tilde{\varphi}(\overline{\vec{x}},\underline{\vec{x}}) =
\varphi(\vec{x})$ whenever $k \overline{\vec{x}} + \underline{\vec{x}} = \vec{x}$, \eg\ for
$\overline{\vec{x}}:=  {\lfloor}\frac{{\vec{x}}}{k}{\rfloor}$ and $\underline{\vec{x}} :=\rem{{\vec{x}}}{k}$.
With this choice, $\PP$ needs to dispatch a total of
$k \left( |\overline{\vec{x}} + \underline{\vec{x}}| \right)
\leq |\vec{x}| + n \cdot (k-1)^2$
agents to compute $\tilde{\varphi}_1(\overline{\vec{x}},\underline{\vec{x}}), \ldots, \tilde{\varphi}_k(\overline{\vec{x}},\underline{\vec{x}})$.
That is, $n \cdot (k-1)^2$ helpers are sufficient to compute $\PP$.
Formally, we define $\tilde{\varphi}$ in the following way:

\begin{quote}
For $\displaystyle \varphi(\vec{x}) = \left(\sum_{i=1}^n \alpha_i x_i > \beta \right)$, we define $\displaystyle \tilde{\varphi}(\overline{\vec{x}}, \underline{\vec{x}}) := \left(\sum_{i=1}^n (k \cdot \alpha_i) \overline{x}_i + \alpha_i\underline{x}_i > \beta \right)$
\end{quote}
\noindent and similarly for modulo predicates.
For instance, if $\varphi(x_1,x_2)=3 x_1 - 2x_2 > 6$
and $k=4$, then $\tilde{\varphi}(\overline{x}_1,\underline{x}_1,\overline{x}_2,\underline{x}_2)=12 \overline{x}_1 + 3 \underline{x}_1 -
8 \overline{x}_2 - 2 \underline{x}_2 > 6$.
As required, $\tilde{\varphi}(\overline{\vec{x}},\underline{\vec{x}})=
\varphi(k\overline{\vec{x}}+\underline{\vec{x}})$.

Let us now describe how
the protocol $\PP$ computes $\tilde{\varphi}_1(\overline{\vec{x}}, \underline{\vec{x}}), \ldots, \tilde{\varphi}_k(\overline{\vec{x}}, \underline{\vec{x}})$.
Let $\tilde{\PP}_1, \ldots, \tilde{\PP}_k$ be protocols computing $\tilde{\varphi}_1, \ldots, \tilde{\varphi}_k$.
Let $X= \{\q{x_1}, \ldots, \q{x_n}\}$ be the input states of $\PP$,
and let
$\q{\overline{x}^j_1}, \ldots, \q{\overline{x}^j_n}$ and $\q{\underline{x}^j_1}, \ldots, \q{\underline{x}^j_n}$ be the input states of $\tilde{\PP}_j$
for every $1 \leq j \leq k$.
Protocol $\PP$
repeatedly chooses an index $1 \leq i \leq n$, and executes one of these two actions: (a)~take $k$ agents from $\q{x_i}$, and dispatch them to $\q{\overline{x}^1_i}, \ldots, \q{\overline{x}^k_i}$ (one agent to each state); or (b)~take one agent from $\q{x_i}$ and $(k-1)$ helpers, and dispatch them to $\q{\underline{x}^1_i}, \ldots, \q{\underline{x}^k_i}$. The index and the action are chosen nondeterministically.
Notice that if
for some input $\q{x}_i$,
all $\ell$ agents of $\q{x_i}$ are dispatched, then
$k \q{\overline{x}^j_i} + \q{\underline{x}^j_i}=\ell$ for all $j$.
If all agents of $\q{x_i}$ are dispatched for every $1 \leq i \leq n$, then we say that the {\em dispatch is correct}.

The problem is that, because of the nondeterminism,
the dispatch may or may not be correct.
Assume, \eg, that $k=5$ and $n=1$. Consider the input $x_1=17$, and assume that $\PP$ has $n \cdot (k-1)^2=16$ helpers. $\PP$ may correctly dispatch
$\overline{x}_1 =  {\lfloor}\frac{17}{5}{\rfloor}=3$ agents to each of $\q{\overline{x}^1_1}, \ldots, \q{\overline{x}^1_5}$
and $\underline{x}_1 = (\rem{17}{5})=2$ to each of $\q{\underline{x}^1_1}, \ldots, \q{\underline{x}^1_5}$; this gives a total of $(3+2)\cdot 5 = 25$ agents, consisting of the $17$ agents for the input plus $8$
helpers. However, it may also wrongly dispatch $2$ agents to each of $\q{\overline{x}^1_1}, \ldots, \q{\overline{x}^1_5}$ and
$4$ agents to each of $\q{\underline{x}^1_1}, \ldots, \q{\underline{x}^1_5}$, with a total of $(2+4) \cdot 5 = 30$ agents, consisting of $14$ input agents plus $16$ helpers. In the second case, each $\PP_j$
wrongly computes $\tilde{\varphi}_j(2, 4) = \varphi_j(2\cdot 5 + 4) = \varphi_j(14)$, instead of the correct value $\varphi_j(17)$.

To solve this problem we ensure that $\PP$ can always recall agents already dispatched
to $\tilde{\PP}_1, \ldots, \tilde{\PP}_k$ as long as the dispatch is not yet correct.
This allows $\PP$ to ``try out'' dispatches until it dispatches correctly, which eventually happens by fairness.
For this we design $\PP$ so that (i) the atomic protocols $\tilde{\PP}_1, \ldots, \tilde{\PP}_k$ can work with inputs agents that arrive over time ({\em dynamic initialization}), and (ii) $\tilde{\PP}_1, \ldots, \tilde{\PP}_k$ can always return to their initial configuration and send agents back to $\PP$, unless the  dispatch is correct ({\em reversibility}).
To ensure that $\PP$ stops redistributing after dispatching a correct distribution, it suffices to replace each reversing transition $\vec{p} \mapsto \vec{q}$ by transitions $\vec{p} + \multiset{\q{x_i}} \mapsto \vec{q} + \multiset{\q{x_i}}$, one for each $1 \leq i \leq n$: All these transitions become disabled when $\q{x_1}, \ldots, \q{x_n}$ are not populated.

\parag{Reversible dynamic initialization} Let us now formally introduce the class of \emph{protocols with reversible dynamic initialization} that enjoys all properties needed for our construction. A simple protocol with \emph{reversible dynamic initia\-li\-zation} (\emph{RDI-protocol} for short) is a tuple $\PP = (Q, T_\infty, T_\dagger, L, X, I , O)$, where $\PP_\infty = (Q, T_\infty, L, X, I , O)$ is a simple population protocol, and $T_\dagger$ is the set of transitions making the system reversible, called the \emph{RDI-transitions}.

Let $T \defeq T_\infty \cup T_\dagger$, and let $\mathsf{In} \defeq \{\mathsf{in}_x
: x \in X\}$ and $\mathsf{Out} \defeq \{\mathsf{out}_x : x \in X\}$ be the sets of
\emph{input} and \emph{output transitions}, respectively, where
$\mathsf{in}_x \defeq (\vec{0}, \multiset{I(x)})$ and $\mathsf{out}_x \defeq
(\multiset{I(x)}, \vec{0})$. An \emph{initialization sequence} is a
finite execution $\pi \in \left( T \cup \mathsf{In} \cup \mathsf{Out}\right)^*$ from
the \emph{initial configuration} $L'$ with $L' \succeq L$. The \emph{effective input} of
$\pi$ is the vector $\vec{w}$ such that $\vec{w}(x) \defeq
|\pi|_{\mathsf{in}_x} - |\pi|_{\mathsf{out}_x}$ for every $x \in X$. Intuitively, a
RDI-protocol starts with helpers only, and is dynamically initialized
via the input and output transitions.

\newcommand{\DiEq}[1]{\left[#1\right]}

Let $\q{f}, \q{t} \in Q$ be the unique states of $\PP$ with $O(\q{f}) = 0$ and
$O(\q{t}) = 1$. For every configuration $C$, let $\DiEq{C} \defeq \left\{C' : C'(\q{f}) + C'(\q{t}) = C(\q{f}) + C(\q{t}) \text{ and }
C'(q) = C(q) \text{ for all } q \in Q \setminus \{\q{f}, \q{t}\} \right\}$. Intuitively, all configurations $C' \in
\DiEq{C}$ are equivalent to $C$ in all but the output states.

An RDI-protocol is required to be \emph{reversible}, that is
for every initialization sequence $\pi$ with effective input $\vec{w}$,
and such that $L' \trans{\pi} C$ for some $L' \succeq L$, the following holds:
\begin{itemize}
\item if $C \trans{T^*} D$ and $D' \in \DiEq{D}$, then $D' \trans{T^*} C'$ for some $C' \in \DiEq{C}$, and

\item $C(I(x)) \leq \vec{w}(x)$ for all $x \in X$.
\end{itemize}
Intuitively, an RDI-protocol can never have more agents in an input state than the effective number of agents it received via the input and output transitions.
Further, an RDI-protocol can always reverse all sequences that do not contain input or output transitions.
This reversal does not involve the states $\q{f}$ and $\q{t}$, which have a special role as output states. Since RDI-protocols have a default output, we need to ensure that the default output state is populated when dynamic initialization ends, and reversal for $\q{f}$ and $\q{t}$ would prevent that.

An RDI-protocol $\PP$ \emph{computes} $\varphi$ if for every initialization sequence $\pi$ with effective input $\vec{w}$ such that $L' \trans{\pi} C$ for some $L' \succeq L$, the standard population protocol $\PP_\infty$ computes $\varphi(\vec{w})$ from $C$ (that is with $T_\dagger$ disabled). Intuitively, if the dynamic initialization terminates, the RDI-transitions $T_\dagger$ become disabled, and then the resulting standard protocol $\PP_\infty$ converges to the output corresponding to the dynamically initialized input.

\begin{restatable}{theorem}{thmAtomicMultHelpers} \label{thm:atomic:mult:helpers}
Assume that for every atomic predicate $\varphi$, there exists a
$|\varphi|$-way RDI-protocol with
$\O(|\varphi|)$ helpers,
$\O(|\varphi|^2)$ states and
$\O(|\varphi|^3)$ transitions
that computes $\varphi$.
For every finite set  $P$ of atomic predicates, there exists a $|P|$-way
simple {\em multi-output} protocol, with
$\O(|P|^3)$  helpers and states, and
$\O(|P|^5)$ transitions, that computes $P$.
\end{restatable}

\subsection{Atomic predicates under reversible dynamic initialization}
\label{subsec:findyn}

Lastly, we show that atomic predicates are succinctly computable
by RDI-protocols:

\begin{restatable}{theorem}{thmAtomicHelpers} \label{thm:atomic:helpers}
Every atomic predicate $\varphi$ over variables $X$ can be computed by a simple $|\varphi|$-way population protocol with reversible dynamic initialization that has
$\O(|\varphi|)$ helpers,
$\O(|\varphi|^2)$ states, and
$\O(|\varphi|^3)$
transitions.
\end{restatable}

\begin{figure}[htb]
	\vspace*{-15pt}
	\centering\input{fig-remainder}%
	\vspace*{-6pt}
	\caption{Partial representation of the protocol computing $5x + 6y
		\geq 4 \pmod{7}$ as a Petri net, where places (circles), transitions
		(squares) and tokens (smaller filled circles) represent
		respectively states, transitions and agents. Non-helper agents
		remember their input variable (labeled here within tokens).
		The depicted configuration is obtained from input $x = 2$, $y = 1$ by
		firing the bottom leftmost transition (dark blue).}\label{fig:petri:remainder}
\end{figure}

The protocols for arbitrary threshold and remainder predicates satisfying the conditions
of \cref{thm:atomic:helpers}, and their correctness proofs, are given in \Cref{app:threshold}. Note that the threshold
protocol is very similar to the protocol for linear inequalities given in Section 6 of \cite{BEJ18}. Thus, as an
example, we will instead describe how to handle the remainder predicate $5x - y \equiv_7 4$. Note, that the
predicate can be rewritten as $\left(5x + 6y \geq 4 \pmod{7}\right)\land \left(5x + 6y \not\geq 5
\pmod{7}\right)$. As we can handle negations and conjunctions separately in \cref{subsec:finsets}, we will now
explain the protocol for $\varphi \defeq 5x + 6y \geq 4 \pmod{7}$. The protocol is partially depicted in
\cref{fig:petri:remainder} using Petri net conventions for the graphical representation.

The protocol has an \emph{input state} $\q{x}$ for each variable $x \in X$,
\emph{output states} $\q{f}$ and $\q{t}$, a \emph{neutral state} $\q{0}$, and
\emph{numerical states} of the form $\q{+2^i}$ for every $0 \leq i
\leq n$, where $n$ is the smallest number such that $2^n > \norm{\varphi}$.
Initially, (at least) one helper is set to $\q{f}$ and (at least) $2n$ helpers set to $\q{0}$.
In order to compute $5x + 6y \geq 4 \pmod{7}$ for $x:= r$ and $y:= s$, we
initially place $r$ and $s$ agents in the states $\q{x}$ and $\q{y}$, i.e.,
the agents in state $\q{x}$ encode the number $r$ in unary, and similarly for $\q{y}$.
The blue transitions on the left of \cref{fig:petri:remainder} ``convert'' each agents in input states to a binary
representation of their corresponding coefficient.
In our example, agents in state $\q{x}$ are converted to $\vec{a}(x) = 5 = 0101_2$ by putting one agent in $\q{4}$ and another one in $\q{1}$.
Since two agents are needed to encode $5$, the transition ``recruits'' one helper from state $\q{0}$.
Observe that, since the inputs can be arbitrarily large, but a protocol can only use a constant number of helpers, the protocol must reuse helpers in order to convert all agents in input states.
This happens as follows.
If two agents are in the same power of two, say $\q{+2^i}$, then one of them can be ``promoted'' to $\q{+2^{i+1}}$, while the other one moves to state $\q{0}$, ``liberating'' one helper.
This allows the agents to represent the overall value of all converted agents in the most efficient representation.
That is, from any configuration, one can always reach a configuration where there is at most one agent in each place $2^0, \ldots, 2^{n-1}$, there are at most the number of agents converted from input places in place $2^n$, and hence there are at least $n$ agents in place $0$, thus ready to convert some agent from the input place.
Similar to promotions, ``demotions'' to smaller powers of two can also happen.
Thus, the agents effectively shift through all possible binary representations of the overall value of all converted agents.
The $\equiv_7$ transition in \cref{fig:petri:remainder} allows 3 agents in states $\q{4}$, $\q{2}$ and $\q{1}$ to ``cancel out'' by moving to state $\q{0}$, and it moves the
output helper to $\q{f}$.
Furthermore, there are RDI-transitions that allow to revert the effects of conversion and cancel transitions.
These are not shown in \cref{fig:petri:remainder}.

We have to show that this protocol computes $\varphi$ under reversible dynamic initialization.
First note, that while dynamic initialization has not terminated, all transitions have a corresponding reverse transition.
Thus, it is always possible to return to wrong initial configurations.
However, reversing the conversion transitions can create more agents in input states than the protocol effectively received.
To forbid this, each input agent is ``tagged'' with its variable (see tokens in \cref{fig:petri:remainder}).
Therefore, in order to reverse a conversion transitions, the original input agent is needed.
This implies, that the protocol is reversible.

Next, we need to argue that the protocol without the RDI-transitions computes $\varphi$ once the dynamic
initialization has terminated.
The agents will shift through the binary representations of the overall value.
Because of fairness, the $\equiv_7$ transition will eventually reduce the overall value to at most $6$.
There is a $\geq 4$-transition which detects the case where the final value is at least $4$ and moves the output helper from $\q{f}$ to state $\q{t}$. Notice that whenever transition $\equiv_7$ occurs, we reset the output by moving the output helper to state $\q{f}$.

\subsection{From fixed-sized protocols with one leader to leaderless protocols}
\label{subsec:fixedsize}

\renewcommand{\cond}[2]{( #1 \mid #2 )}

We now define when a population protocol computes a predicate {\em for inputs of a fixed size}.
Intuitively,
it should compute the correct value for every initial configurations of this size;
for inputs of other sizes, the protocol may converge to the wrong result, or may not converge.

\begin{definition}
Let $\varphi$ be a predicate and let $i \geq 2$.
A protocol $\PP$ \emph{computes $\varphi$ for inputs of size $i$}, denoted \emph{``$\PP$ computes $\cond{\varphi}{i}$}'', if for every input $\vec{v}$ of size $i$, every fair execution of $\PP$ starting at $C_{\vec{v}}$ stabilizes to $\varphi(\vec{v})$.
\end{definition}

We show that if, for each small number $i$, some succinct protocol computes $\cond{\varphi}{i}$, then there is a single succinct protocol that computes $\varphi$ for all small inputs.

\begin{restatable}{theorem}{propRemovingLeaders}\label{thm:removing:leaders}
Let $\varphi$ be a predicate over a set of variables $X$, and let $\cutoffvar \in \N$.
Assume that for every $i \in \{2,3, \ldots, \cutoffvar-1\}$, there exists a protocol with at most one leader and at most $m$ states that computes $\cond{\varphi}{i}$. Then, there is a leaderless population protocol with $\O(\cutoffvar^4 \cdot m^2 \cdot |X|^3)$ states that computes $(\vec{x} <  \cutoffvar) \rightarrow \varphi(\vec{x})$.
\end{restatable}

\begin{proof}[Proof sketch]
Fix a predicate $\varphi$ and $\cutoffvar \in \N$. For every
$2 \leq i < \cutoffvar$, let $\PP_i$ be a protocol computing
$\cond{\varphi}{i}$. We describe the protocol $\PP=(Q, T, X, I, O)$ that computes $(\vec{x} \geq \cutoffvar) \lor \varphi(\vec{x}) \equiv (\vec{x} <  \cutoffvar) \rightarrow \varphi(\vec{x})$.
The input mapping $I$ is the identity. During the computation, agents never forget their initial state -- that is, all successor states of an agent are annotated with their initial state. The protocol initially performs a leader election. Each provisional leader stores how many agents it has ``knocked out'' during the leader election in a counter from $0$ to $\cutoffvar-1$. After increasing the counter to a given value $i<\cutoffvar$, it resets the state of $i$ agents and itself to the corresponding initial state of $\PP_{i+1}$, annotated with $X$, and initiates a simulation of $\PP_{i+1}$.
    When the counter of an agent reaches $\cutoffvar-1$, the agent knows that the population size must be $\geq \cutoffvar$, and turns the population into a permanent $1$-consensus.
    Now, if the population size $i$ is smaller than $\cutoffvar$, then eventually a leader gets elected who resets the population to the initial population of $\PP_i$. Since $\PP_i$ computes $\cond{\varphi}{i}$, the simulation of $\PP_i$ eventually yields the correct output.
\end{proof}

\subsection{Computing boolean combinations of predicates for fixed-size inputs}
\label{subsec:halting}

We want to produce a population protocol $\PP$
for a boolean combination $\varphi$ of atomic predicates $(\varphi_i)_{i \in [k]}$ for which we have population protocols $(\PP_i)_{i \in [k]}$.
As in Section~\ref{subsec:finat}, we cannot use a standard ``product protocol'' that executes $\PP_1, \ldots, \PP_k$ synchronously because
the number of states would be exponential in $k$.
Instead, we want to simulate the \emph{concatenation} of
$(\PP_i)_{i \in [k]}$. However, this is only possible if for all $i \in [k]$, the executions of $\PP_i$ eventually ``halt'', i.e.
some agents are eventually certain that the output of the protocol
will not change anymore, which is not the case in general population protocols.
For this reason we restrict our attention to ``halting'' protocols.

\begin{definition}
Let $\PP$ be a simple protocol with output states $\q{f}$ and $\q{t}$. We say that $\PP$ is a \emph{halting protocol} if every configuration $C$ reachable from an initial configuration satisfies:
\begin{itemize}
\item $C(\q{f}) = 0 \lor C(\q{t}) = 0$,

\item $C \trans{*} C' \land C(q) > 0 \Rightarrow C'(q) > 0$ for every $q \in \{\q{f}, \q{t}\}$ and every configuration $C'$.
\end{itemize}
\end{definition}

Intuitively, a halting protocol is a simple protocol in which states $\q{f}$ and $\q{t}$ behave like ``final states'': If an agent reaches $q \in \{\q{f}, \q{t}\}$, then the agent stays in $q$ forever.
In other words, the protocol reaches consensus $0$ (resp.\ $1$) if{}f an agent ever reaches $\q{f}$ (resp.\ $\q{t}$).

\begin{restatable}{theorem}{thmHaltingConjDis}\label{lemma:halting-conj-disj}
Let $k, i \in \N$.
Let $\varphi$ be a boolean combination of atomic predicates $(\varphi_j)_{j \in [k]}$.
Assume that for every $j \in [k]$, there is a  simple halting  protocol $\PP_j=(Q_j, L_j, X, T_j, I_j, O_j)$ with one leader computing $\cond{\varphi_j}{i}$. Then there exists
a simple halting protocol $\PP$ that computes $\cond{\varphi}{i}$,
with one leader and $\mathcal{O}\left(|X| \cdot  \left(\len(\varphi) +|Q_1| + \ldots + |Q_k|\right) \right)$ states.
\end{restatable}

\begin{proof}[Proof sketch]
\newcommand{\pres}[1]{\text{pres}(#1)}
We only sketch the construction
for $\varphi=\varphi_1 \wedge \varphi_2$.
The main intuition is that, since $\PP_1$ and $\PP_2$ are halting, we can construct a protocol that, given an input $\vec{v}$, first simulates $\PP_1$ on $\vec{v}$, and, after $\PP_1$ halts, either halts if $\PP_1$ converges to $0$, or simulates $\PP_2$ on $\vec{v}$ if $\PP_1$ converges to $1$.
Each agent remembers in its state the input variable it corresponds to, in order to simulate $\PP_2$ on $\vec{v}$.
\end{proof}

\subsection{Computing atomic predicates for fixed-size inputs}
\label{subsec:atomic}

We describe a halting protocol that computes a given threshold predicate for fixed-size inputs.

\begin{restatable}{theorem}{thmHaltingThreshold}\label{thm:halting:threshold}
Let $\varphi(\vec{x}, \vec{y}) \defeq  \vec{\alpha} \cdot \vec{x} - \vec{\beta}\cdot \vec{y} > 0$.
For every $i \in \N$, there exists a halting protocol with one leader and $\O(i^2 (|\varphi| + \log i)^3)$
states that computes $\cond{\varphi}{i}$.
\end{restatable}

\newcommand{\GreaterSum}{\sf{Greater}\text{-}\sf{Sum}}

\noindent We first describe a sequential algorithm $\GreaterSum(\vec{x}, \vec{y})$, that
for every input $\vec{x}, \vec{y}$ satisfying $|\vec{x}|+|\vec{y}|=i$
decides whether $\vec{\alpha} \cdot \vec{x} - \vec{\beta}\cdot \vec{y} > 0$ holds. Then we simulate $\GreaterSum$
by means of a halting protocol with $i$ agents.

Since each agent can only have $\O(\log i + \log |\varphi|)$ bits of memory (the logarithm of the number of states),
$\GreaterSum$ must use at most $\O(i \cdot (\log i + \log |\varphi|))$ bits of memory, otherwise it cannot be
simulated by the agents. Because of this requirement, $\GreaterSum$ cannot just compute, store, and then compare
$\vec{\alpha} \cdot \vec{x}$ and $\vec{\beta}\cdot \vec{y}$; this uses too much memory.

$\GreaterSum$ calls procedures $\textit{Probe}_1(j)$ and $\textit{Probe}_2(j)$ that return the $j$-th bits of
$\vec{\alpha} \vec{x}$ and $\vec{\beta} \vec{y}$,  respectively, where $j=1$ is the most significant bit. Since $|\vec{x}| \leq  i$,
and the largest constant in $\vec{\alpha}$ is  at most $||\varphi||$, we have $\vec{\alpha} \cdot \vec{x} \leq i \cdot ||\varphi||$, and so
$\vec{\alpha} \cdot \vec{x}$ has at most $m \defeq |\varphi|+\lfloor\log(i)\rfloor+1$ bits, and the same holds for $\vec{\beta} \vec{y}$.
So we have $ 1 \leq j \leq m$.  Let us first describe $\GreaterSum$, and then  $\textit{Probe}_1(j)$; the procedure $\textit{Probe}_2(j)$ is similar.

$\GreaterSum(\vec{x}, \vec{y})$ loops through $j=1, \ldots, m$. For each $j$, it calls $\textit{Probe}_1(j)$ and $\textit{Probe}_2(j)$.
If $\textit{Probe}_1(j)>\textit{Probe}_2(j)$, then it answers $\varphi(\vec{x}, \vec{y})=1$, otherwise it moves to $j+1$.
If $\GreaterSum$ reaches the end of the loop, then it answers $\varphi(\vec{x}, \vec{y})=0$. Observe that
 $\GreaterSum$ only needs to store the current value of $j$ and the bits returned by $\textit{Probe}_1(j)$ and $\textit{Probe}_2(j)$.
 Since $j \leq m$, $\GreaterSum$ only needs $\O(\log(|\varphi|+\log i))$ bits of memory.

$\textit{Probe}_1(j)$
uses a decreasing counter $k = m, \ldots, j$ to successively compute the bits $b_{1}(k)$ of $\vec{\alpha} \cdot \vec{x}$,
starting at the least significant bit. To compute $b_{1}(k)$, the procedure stores the carry $c_k \leq i$
of the computation of $b_1(k+1)$; it then computes the sum $s_k := c_k + \vec{\alpha}(k) \cdot \vec{x}$
(where $\vec{\alpha}(k)$ is the $k$-th vector of bits of $\vec{\alpha}$), and sets $b_{k} := s_k \bmod 2$ and
$c_{k-1} := s_k \div 2$.
The procedure needs $\O(\log (|\varphi|+\log i))$ bits of memory for counter $k$,
$\log(i)+1$ bits for encoding $s_k$, and
$\O(\log(i))$ bits for encoding $c_k$. So it only uses $\O(\log(|\varphi|+\log i))$ bits of memory.

Let us now simulate $\GreaterSum(\vec{x}, \vec{y})$ by a halting protocol with one leader agent.
Intuitively, the protocol proceeds in rounds corresponding to the counter $k$.
The leader stores in its state the value $j$ and the current values of the program counter, of counter $k$, and of variables $b_k$, $s_k$, and $c_k$.
The crucial part is the implementation of the instruction
$s_k := c_k + \vec{\alpha}(k) \cdot \vec{x}$ of $\textit{Probe}_1(j)$.
In each round, the leader adds input agents one by one. As the protocol only needs to work for populations with $i$ agents,
it is possible for each agent to know if it already interacted with the leader in this round, and for the leader to count the number of agents it has interacted with this round, until it reaches $i$ to start the next round.

\subsubsection{Threshold protocols}\label{subsec:app-threshold}

Let us fix a threshold predicate $\varphi$ over variables $X$. Without
loss of generality\footnote{If $b \leq 0$, then we can instead
  consider the equivalent predicate $\neg(-\vec{a} \cdot \vec{v} \geq
  -b + 1)$, construct a protocol for $-\vec{a} \cdot \vec{v} \geq -b +
  1$ and handle the negation separately in \cref{subsec:finsets}.}, we
have $\varphi(\vec{v}) = \vec{a} \cdot \vec{v} \geq b$ where $\vec{a}
\in \Z^X$ and $b > 0$. We construct a simple
population protocol $\PP_{\text{thr}}$ that computes $\varphi$ under
reversible dynamic initialization, and prove its correctness.

\parag{Notations} Let $n$ be the smallest number such that $2^n >
\norm{\varphi}$. Let $P \defeq \{\q{+2^i}, \q{-2^i} : 0 \leq i \leq
n\}$, $Z \defeq \{\q{0}\}$, $N \defeq P \cup Z$ and $B \defeq \{\q{f},
\q{t}\}$, where $P$, $Z$, $N$ and $B$ respectively stand for
``$P$owers of two'', ``$Z$ero'', ``$N$umerical values'' and
``$B$oolean values''. For every set $S$ and every $x \in X$, let $S_x
\defeq \{q_x : q \in S\}$ and $S_X \defeq S \cup \bigcup_{x \in X}
S_x$.

For every $d \in \N$, let $\mathrm{bits}(d)$ denote the unique set $J
\subseteq \N$ such that $d = \sum_{j \in J} 2^j$,
\eg\ $\mathrm{bits}(13) = \mathrm{bits}(1101_2) = \{3, 2, 0\}$. The \emph{canonical representation} of an integer $d \in \Z$ is the multiset
$\mathrm{rep}(d)$ defined as follows:

$$
\mathrm{rep}(d) \defeq
\begin{cases}
  \multiset{\q{+2^i} : i \in \mathrm{bits}(d)}  & \text{if } d > 0, \\
  \multiset{\q{-2^i} : i \in \mathrm{bits}(|d|)} & \text{if } d < 0, \\
  \multiset{\q{0}}                               & \text{if } d = 0.
\end{cases}
$$

\parag{The protocol} The RDI-protocol $\PP_{\text{thr}} = (Q, T_\infty, T_\dagger, L, X, I, O)$ is defined as
follows:
\begin{itemize}
\setlength\itemsep{4pt}

\item  $Q \defeq X \cup N_X \cup B$. \\
Intuitively, the states of $X$ are the ``ports'' through which the agents for each variable
enter and exit the protocol.

\item  $I \defeq x \mapsto \q{x}$. \\
That is, the initial state for variable $x$ is $x$.

\item $L \defeq \multiset{2n \cdot \q{0}, \q{f}}$. \\
So, we have $2n$ helpers in state $\q{0}$, and one helper in state $\q{f}$, i.e., initially
the protocol assumes that the predicate does not hold.

\item $O(q) \defeq q \mapsto (0 \text{ if } q = \q{f} \text{ else } 1
\text{ if } q = \q{t} \text{ else } \bot)$. \\
That is, the output of the protocol is completely determined by the number of agents in states
$\q{t}$ and $\q{f}$

\item $T_\infty$ is the following set of (``permanent'') transitions:
\begin{alignat*}{3}
	\mathsf{add}_{x}:\ &&
	\multiset{x, |\mathrm{rep}(\vec{a}(x))| \cdot \q{0}}
	& \mapsto \multiset{\q{0}_x} \mplus \mathrm{rep}(\vec{a}(x))
	&& \quad \text{for all $x \in X$,} \\
	%
	\mathsf{up}_i^\circ:\ &&
	\multiset{\q{\circ2^i}, \q{\circ2^i}}
	&  \mapsto \multiset{\q{\circ2^{i+1}}, \q{0}}
	&& \quad\text{for all $0 \leq i < n$ and $\circ \in \{+, -\}$,} \\
	%
	\mathsf{down}_i^\circ:\ &&
	\multiset{\q{\circ2^i}, \q{0}}
	&  \mapsto \multiset{\q{\circ2^{i-1}}, \q{\circ{2^{i-1}}}}
	&& \quad\text{for all $0 < i \leq n$ and $\circ \in \{+, -\}$,} \\
	%
	\mathsf{cancel}_{i, q}:\ &&
	\multiset{\q{+2^i}, \q{-2^i}, q}
	&  \mapsto \multiset{\q{0}, \q{0}, \q{f}}
	&& \quad\text{for all $0 \leq i \leq n$ and $q \in B$,} \\
	%
	\mathsf{swap}_{p, q}^x:\ &&
	\multiset{p, q_x}
	& \mapsto \multiset{p_x, q}
	&& \quad \text{for all $p, q \in N$ and $x \in X$,} \\
	%
	\mathsf{equal}:\ &&
	\mathrm{rep}(b) \mplus \multiset{\q{f}}
	& \mapsto \mathrm{rep}(b) \mplus \multiset{\q{t}}, \\
	%
	\mathsf{false}:\ &&
	\multiset{\q{f}, \q{t}} & \mapsto \multiset{\q{f}, \q{f}}.
\end{alignat*}
Intuitively, $\mathsf{add}_{x}$ converts an agent which arrived via port $x$ into
the canonical representation of $\vec{a}(x)$. Transitions of the form $\mathsf{up}_i^\circ,
\mathsf{down}_i^\circ$ and $\mathsf{cancel}_{i, q}$ allow the protocol to change
the representation of a value, without changing the value itself.
Transition $\mathsf{equal}$ allows the protocol to detect that the current value
of $\vec{a}\cdot \vec{x}$, for the current input $\vec{x}$, is at least $b$, which moves
a helper from state $\q{f}$ to $\q{t}$.
\item Finally, $T_{\dagger}$ is the following set of RDI-transitions:
\begin{alignat*}{3}
	\mathsf{add}_{x,q}^{-1}:\ &&
	\multiset{\q{0}_x, q} \mplus \mathrm{rep}(\vec{a}(x))
	& \mapsto \multiset{x, \q{f}, |\mathrm{rep}(\vec{a}(x))| \cdot \q{0}}
	&& \quad \text{for all $x \in X$ and $q \in B$,} \\
	%
	\mathsf{cancel}_{i,q}^{-1}:\ &&
	\multiset{\q{0}, \q{0}, q}
	&  \mapsto \multiset{\q{+2^i}, \q{-2^i}, \q{f}}
	&& \quad\text{for all $0 \leq i \leq n$ and $q \in B$,}
	\\
	%
	\mathsf{reset}:\ &&
	\multiset{\q{t}}
	& \mapsto \multiset{\q{f}}.
\end{alignat*}
The first two transitions are needed to reverse the changes of
$\mathsf{add}$ and $\mathsf{cancel}$ transitions while the dynamic
initialization is not finished. Both types of transitions reset the
output of the protocol by leaving an agent in the default output state
$\q{f}$. The $\mathsf{reset}$ transition resets the output by moving
agents from $\q{t}$ to $\q{f}$.
\end{itemize}

\noindent Let $\PP_\infty = (Q, T_\infty, L, X, I , O)$.
Let $T \defeq T_\infty \cup T_\dagger$. For the sake of readability,
we will sometimes omit the subscripts and superscripts from transitions names
when they are irrelevant, \eg\ ``a
$\mathsf{swap}$ transition is enabled'' instead of ``there exist $p, q
\in N$ and $x \in X$ such that $\mathsf{swap}_{p,q}^x$ is enabled''.\medskip

\parag{Size} Note that $\PP_{\text{thr}}$ has $|Q| = |X| + |N_X| + |B|
= |X| + (2n+3) \cdot (|X|+1) + 2 \in \O(\log \norm{\varphi} \cdot
|X|)$ states and $|L| = 2n+1 \in \O(\log \norm{\varphi})$
helpers. Moreover, since families of transitions are parameterized by
$X$, $B$, $N$ or $N^2$, and $\{+, -\}$, there are $\O(|N|^2 \cdot |X|)
= \O(\log^2 \norm{\varphi} \cdot |X|) \subseteq \O(|\varphi|^3)$
transitions. Finally, each transition uses at most
$\O(|\mathrm{rep}(\norm{\varphi})|) = \O(\log \norm{\varphi})
\subseteq \O(|\varphi|)$ states.

\medskip

\parag{Auxiliary definitions and observations} Before proving that
$\PP_{\text{thr}}$ works as intended, let us first introduce auxiliary
definitions. Let $\val \colon Q \to \N$ be the function that
associates a value to each state as follows:
\begin{align*}
  \val(\q{0}) &= \val(\q{f}) = \val(\q{t}) \defeq 0, \\
  %
  \val(x) &\defeq \vec{a}(x)
  && \text{for every } x \in X, \\
  %
  \val(\q{\circ2^i}) &\defeq \circ2^i
  && \text{for every } 0 \leq i \leq n \text{ and } \circ \in \{+, -\}, \\
  %
  \val(q_x) &\defeq \val(q)
  && \text{for every } q \in N \text{ and } x \in X.
\end{align*}
\noindent So, for example, for the predicate $3x - 4y \geq 2$ we have $\val(x) = 3$ and
$\val(y) = -4$.
For every configuration $C$ and every set of states $S \subseteq Q$, let
$$\val_S(C) \defeq \sum_{q \in S} \val(q) \cdot C(q).$$ In particular,
let $\val(C) \defeq \val_Q(C)$. Intuitively, $C$ can be seen as an encoding of the value
$\val(C)$. The following properties, relating
values and configurations, can be derived from the above definitions:
\begin{proposition}\label{prop:thr:prop}
  For every initialization sequence $\pi$ with effective input $\vec{w}$
  such that $L' \trans{\pi} C$ for some $L' \succeq L$, the following holds:
  \begin{enumerate}
  \item $\val(C) = \vec{a} \cdot \vec{w}$, \label{itm:val:inv}

  \item $|C| = C(N) + C(B) + |\vec{w}|$,\label{itm:config:size}

  \item $C(N) \geq L(N)$ and $C(B) \geq L(B)$, \label{itm:preservation}

  \item $C(N_x) + C(x) = \vec{w}(x)$ for every $x \in
    X$. \label{itm:preservation:x}
  \end{enumerate}
\end{proposition}

\noindent In particular, \eqref{itm:config:size} states that the
number of agents is always equal to the number of helpers plus the
\emph{net} amount of agents that dynamically entered the population.

\parag{Auxiliary propositions} We say that a configuration $C$ is
\emph{clean} if the following holds for every $p, q \in
P_X$:\smallskip
\begin{itemize}
\item If $\val(p) + \val(q) = 0$, then $C(p) = 0$ or $C(q) = 0$. \\
For example, a configuration with agents in $\q{+2^i}_x$ and
$\q{-2^i}_y$ is not clean, since $\val(\q{+2^i}_x) + \val(\q{-2^i}_y) = 0$.
Intuitively, no pair of agents can cancel in a clean configuration.\medskip

\item If $\val(p) = \val(q)$ and $\val(p) \not\in \{-2^n, +2^n\}$,
  then $C(\{p, q\}) \leq 1$. \\
For example, a configuration with two agents in $\q{+2^i}_x$, where $i < n$,
is not clean. Intuitively, in a clean configuration no agent can be promoted to
a higher power of 2.
\end{itemize}

We show that any configuration can be cleaned using only permanent transitions.
This implies that once the dynamic initialization has terminated, every fair
execution visits clean configurations infinitely often.

\begin{proposition}\label{prop:cleaning}
  For every initialization sequence $\pi$ such that $L' \trans{\pi} C$ for some
  $L' \succeq L$, there exists a clean configuration $D$
  such that $C \trans{T_{\infty}^*} D$.
\end{proposition}

\begin{proof}
  If $C$ is clean, then we pick $D \defeq C$. Otherwise, at least one
  of the following holds:
  \begin{enumerate}[(a)]
    \item $C(p) > 0$, $C(q) > 0$ and $\val(p) + \val(q) = 0$ for some
      $p, q \in P_X$; \label{itm:clean:eq}

    \item $C(\{p, q\}) \geq 2$ for some $p, q \in P_X$ such that
      $\val(p), \val(q) \not\in \{-2^n, +2^n\}$. \label{itm:clean:up}
  \end{enumerate}

  We claim there exists a configuration $C'$ such that $C \trans{T_{\infty}^*}
  C'$ and $C(P_X) > C'(P_X)$. Let us show that if the claim is true then the result holds. If $C'$ is clean, then we are
  done. Otherwise, this process is repeated until a clean
  configuration $D$ has been reached. The process terminates as the
  number of agents in $P_X$ cannot become negative.

  Let us now prove the claim. Suppose~\eqref{itm:clean:eq}
  holds. By \cref{prop:thr:prop}~\eqref{itm:preservation}, we have
  $C(N) \geq L(N) \geq 2$ and hence it is possible to consecutively
  fire at least two $\mathsf{swap}$ transitions. Note that they do not
  change the amount of agents in $P_X$. For this reason, we may assume
  without loss of generality that $p = \q{+2^i}$ and $q = \q{-2^i}$
  for some $0 \leq i \leq
  n$. By \cref{prop:thr:prop}~\eqref{itm:preservation}, we have
  $C(B) \geq L(B) > 0$. Thus, there exists $r \in B$ such that $C(r) >
  0$. Therefore, firing transition $\mathsf{cancel}_{i, r}$ decreases
  $C(P_X)$ by two.

  Similarly, if case~\eqref{itm:clean:up} holds, then we may assume
  without loss of generality that $C(\q{\circ2^i}) \geq 2$ for some $0
  \leq i < n$ and $\circ \in \{+, -\}$. Thus, firing transition
  $\mathsf{up}_i^\circ$ decreases $C(P_X)$ by one.
\end{proof}

We now bound the number of agents in states from $X \cup P_X$ in a
clean configuration.

\begin{proposition} \label{prop:top:small}
  For every initialization sequence $\pi$ with effective input $\vec{w}$
  such that $L' \trans{\pi} C$ for some $L' \succeq L$, if $C$ is clean,
  then $C(X) + C(P_X) \leq |\vec{w}| + n$.
\end{proposition}

\begin{proof}
  Let $S_{\circ 2^n} \defeq \{q \in P_X : \val(q) = \circ2^n\}$ for
  both $\circ \in \{+, -\}$. Since $C$ is clean, we have $C(S_{\circ
    2^n}) = 0$ for some $\circ \in \{+, -\}$. Let us consider the case
  where $\circ = -$. The other case is proven analogously.

  Let $\vec{u} \in \N^X$ be such that $\vec{u}(x) \defeq C(x)$ for
  every $x \in X$. Note that $|\vec{u}| = C(X)$, and that $\vec{u}
  \leq \vec{w}$ by \cref{prop:thr:prop}~\eqref{itm:preservation:x}. Since $C$ is clean, we
  have $C(P_X \setminus S_{+2^n}) \leq n$. Thus, it suffices to show
  that $C(S_{+2^n}) \leq |\vec{w}| - |\vec{u}|$. Suppose this is not
  the case. This yields a contradiction:
  \begin{align*}
    \val_{P_X}(C)
    &> 2^n \cdot C(S_{+2^n}) - 2^n
    && \text{(since $C$ is clean)} \\
    %
    &\geq 2^n \cdot (|\vec{w}| - |\vec{u}| + 1) - 2^n
    && \text{(by assumption)} \\
    %
    &= 2^n \cdot (|\vec{w}| - |\vec{u}|) \\
    %
    &\geq \vec{a} \cdot (\vec{w} - \vec{u}) && \text{(since $2^n >
      \norm{\vec{a}}$ and $\vec{w} \geq \vec{u}$)} \\
    %
    &= \vec{a} \cdot \vec{w} - \vec{a} \cdot \vec{u} \\
    %
    &= \val(C) - \val_X(C)
    && \text{(by Prop.~\ref{prop:thr:prop}~\eqref{itm:val:inv} and
      def.\ of $\vec{u}$)} \\
    %
    &= \val_{P_X}(C)
    && \text{(by def.\ of $\val$)} \qedhere
  \end{align*}
\end{proof}

The following corollary shows that the number of agents in state
$\q{0}$ can always be increased back to at least $n$. This will later
be useful in arguing that the number of agents in $X$ can eventually
be decreased to zero.

\begin{corollary} \label{cor:enough:zero}
  For every initialization sequence $\pi$ with effective input $\vec{w}$ such
  that $L' \trans{\pi} C$ for some $L' \succeq L$, there exists a clean
  configuration $D$ such that $C \trans{T_{\infty}^*} D$ and $D(\q{0}) \geq n$.
\end{corollary}

\begin{proof}
  By \cref{prop:cleaning}, there exists a clean configuration $C'$
  such that $C \trans{\pi' \in T_\infty^*} C'$. Let us first prove that $C'(Z_X) \geq n$.
  Note that $\pi\pi'$ is an initialization sequence with effective input
  $\vec{w}$ such that $L' \trans{\pi\pi'} C'$. Thus:
  \begin{align*}
    C'(Z_X)
    &= |C'| - C'(X) - C'(P_X) - C'(B)
    && \text{(by def.\ of $Q$)} \\
    %
    &= (C'(N) + C'(B) + |\vec{w}|) - C'(X) - C'(P_X) - C'(B)
    && \text{(by Prop.~\ref{prop:thr:prop}~\eqref{itm:config:size})} \\
    %
    &\geq (L(N) + C'(B) + |\vec{w}|) - C'(X) - C'(P_X) - C'(B)
    && \text{(by Prop.~\ref{prop:thr:prop}~\eqref{itm:preservation})} \\
    %
    &\geq (L(N) + C'(B) + |\vec{w}|) - (|\vec{w}| + n) - C'(B)
    && \text{(by Prop.~\ref{prop:top:small})} \\
    %
    &= L(N) - n \\
    %
    &\geq n
    && \text{(by def.\ of $L$)}
  \end{align*}
  Now, by \cref{prop:thr:prop}~\eqref{itm:preservation}, we have
  $C'(N) \geq L(N) \geq n$. Thus, using $\mathsf{swap}$ transitions, we
  can swap $n$ agents from $Z_X$ to $\q{0}$. This way, we obtain a
  configuration $D$ such that $C' \trans{T_{\infty}^*} D$ and $D(\q{0}) \geq
  n$. We are done since $\mathsf{swap}$ transitions preserve
  cleanness.
\end{proof}

For every configuration $C$, let
\begin{align*}
  \val^+(C) &\defeq \sum_{\substack{q \in P_X \\ \val(q) > 0}} \val(q)
  \cdot C(q), &
  %
  \val^-(C) &\defeq \sum_{\substack{q \in P_X \\ \val(q) < 0}} \val(q)
  \cdot C(q).
\end{align*}
We now show that, once dynamic initialization has terminated, fair executions stabilize to configurations of a
certain ``normal form''.

\begin{proposition}\label{prop:threshold:stabilize}
  For every initialization sequence $\pi$ with effective input $\vec{w}$
  such that $L' \trans{\pi} C$ for some $L' \succeq L$ and for every fair execution
  $\sigma$ of $\PP_\infty$ starting from $C$,
  there exist $i \in \N$, $m_+ \geq 0$ and $m_- \leq 0$ such that:
  \begin{enumerate}
  \item $\sigma_i(X) = \sigma_{i+1}(X) = \cdots = 0$,

  \item $\val^\circ(\sigma_i) = \val^\circ(\sigma_{i+1}) = \cdots =
    m_\circ$ for both $\circ \in \{+, -\}$,

  \item $m_+ = 0 \lor m_- = 0$.
  \end{enumerate}
\end{proposition}

\begin{proof}
  For the sake of contradiction, assume there exist infinitely many
  indices $j$ such that $\sigma_j(X) > 0$. Let $j \in \N$ be such an
  index. By \cref{cor:enough:zero}, there exists a configuration $C_j$
  such that $\sigma_j \trans{T_{\infty}^*} C_j$ and $C_j(\q{0}) \geq n$. Hence,
  there exists $x \in X$ such that transition $\mathsf{add}_x$ is
  enabled in $C_j$. Since this holds for infinitely many indices and
  since $X$ is finite, fairness implies that some $\mathsf{add}$
  transition can be enabled infinitely often and hence occurs
  infinitely often along $\sigma$. This is impossible since the number
  of agents in $X$ cannot be increased by any transition in $T_\infty$,
  and thus would eventually drop below zero.
  Therefore, there exists $h \in \N$ such that
  $\sigma_h(X) = \sigma_{h+1}(X) = \cdots = 0$.

  Since $X$ is permanently empty from index $h$, the $\mathsf{add}$ transitions
  are permanently disabled. No other transition in $T_\infty$ can increase
  the absolute value of $\val^\circ$ for any $\circ \in \{+, -\}$. Thus, we have
  $|\val^\circ(\sigma_h)| \geq |\val^\circ(\sigma_{h+1})| \geq
  \cdots$ for both $\circ \in \{+, -\}$. Therefore, there exist $i
  \geq h$, $m_+ \geq 0$ and $m_- \leq 0$ such that
  \begin{align}
    \val^+(\sigma_i) &= \val^+(\sigma_{i+1}) = \cdots = m_+,\label{eq:stab1} \\
    \val^-(\sigma_i) &= \val^-(\sigma_{i+1}) = \cdots = m_-.\label{eq:stab2}
  \end{align}

  It remains to show that $m_+ = 0$ or $m_- = 0$. For the sake of
  contradiction, suppose this is not the case. For every $j \geq i$,
  \cref{cor:enough:zero} yields a configuration $C_j$ such that
  $\sigma_j \trans{T_{\infty}^*} C_j$ and $C_j(\q{0}) \geq n$. Thus, by fairness,
  there exist infinitely many indices $j \geq i$ such that
  $\sigma_j(\q{0}) \geq n$. Let $j$ be such an index. Let $0 \leq d,
  d' \leq n$ be the largest indices for which there exist states $q,
  q' \in P_X$ such that $\sigma_j(q) > 0$, $\sigma_j(q') > 0$,
  $\val(q) = 2^{d}$ and $\val(q') = -2^{d'}$. Note that these indices
  exist because $m_+ \neq 0$ and $m_- \neq 0$.

  Assume without loss of generality that $d \geq d'$, as the other
  case is symmetric. By \cref{prop:thr:prop}~\eqref{itm:preservation},
  there exists $r \in B$ such that $C(r) > 0$. Since $C_j(\q{0}) \geq
  n \geq d - d'$, the sequence of transitions $\mathsf{down}_d^+,
  \mathsf{down}_{d-1}^+, \ldots, \mathsf{down}_{d'+1}^+$ can be fired
  from $C_j$. From there, we can fire $\mathsf{cancel}_{d', r}$ which
  leads to a configuration $D_j$ such that $|\val^\circ(D_j)| <
  |m_\circ|$ for both $\circ \in \{+, -\}$. Since there are infinitely
  many such indices $j$, fairness implies that some such configuration
  $D_j$ occurs (infinitely often) along $\sigma$, which contradicts
  both~(\ref{eq:stab1}) and~(\ref{eq:stab2}).
\end{proof}

\parag{Main proof} We are now ready to prove that $\PP_{\text{thr}}$
works as intended.

\newcommand{\mathrm{false}}{\mathrm{false}}

\begin{theorem}
  $\PP_{\text{thr}}$ computes $\varphi$ with helpers and under
  reversible dynamic initialization.
\end{theorem}

\begin{proof}
  We first show that $\PP_{\text{thr}}$ is input reversible, and then
  that it correctly computes $\varphi$.

  \medskip\noindent\emph{Input reversibility.} Let $\pi$ be an
  initialization sequence with effective input $\vec{w}$ such that
  $L' \trans{\pi} C$ for some $L' \succeq L$. By
  \cref{prop:thr:prop}~\eqref{itm:preservation:x}, we have $C(I(x)) =
  C(x) = \vec{w}(x) - C(N_x) \leq \vec{w}(x)$ for every $x \in X$,
  which proves the first required property.

  For every configuration $C$, let $\mathrm{false}(C) \defeq D$ where $D(t)
  \defeq 0$, $D(f) \defeq C(t) + C(f)$ and $D(q) \defeq C(q)$ for
  every $q \in Q \setminus \{f, t\}$. Observe that for every
  configuration $C$, the following holds:
  \begin{align}
    C \trans{\mathsf{reset}^{C(\q{t})}} \mathrm{false}(C) \text{ and }
    \mathrm{false}(C) \in [C].\label{eq:reset:false}
  \end{align}
  It remains to show that if $C \trans{\pi_\triangleright \in T^*} D$
  and $D' \in [D]$, then $D' \trans{\pi_\triangleleft \in T^*} C'$ for
  some $C' \in \DiEq{C}$. By~\eqref{eq:reset:false}, it is enough to
  argue that $\mathrm{false}(D) \trans{T^*} \mathrm{false}(C)$.

  Let $C_i \trans{t_i} C_{i+1}$ be the $i^\text{th}$ step of
  $\pi_\triangleright$. We argue that $\mathrm{false}(C_{i+1}) \trans{t_i'}
  \mathrm{false}(C_i)$ for some $t_i' \in T \cup \{\varepsilon\}$. By
  induction, this implies $\mathrm{false}(D) \trans{T^*} \mathrm{false}(C)$ as
  desired. If $t_i$ is an $\mathsf{equal}$, $\mathsf{false}$ or
  $\mathsf{reset}$ transition, then we already have $\mathrm{false}(C_{i+1}) =
  \mathrm{false}(C_i)$. Otherwise we revert the step as follows, where ``$s
  \mapsto u$'' indicates that if $t_i = s$, then we reverse it with
  $t_i' = u$:
  \begin{align*}
    \mathsf{add}_x &\mapsto \mathsf{add}_{x,\q{f}}^{-1}
    && \text{for every $x \in X$,} \\
    %
    \mathsf{add}_{x,q}^{-1} &\mapsto \mathsf{add}_x
    && \text{for every $x \in X$ and $q \in B$,} \\
    %
    \mathsf{up}_i^\circ &\mapsto \mathsf{down}^\circ_{i+1}
    && \text{for every $0 \leq i < n$ and $\circ \in \{+, -\}$,}\\
    %
    \mathsf{down}^\circ_i &\mapsto \mathsf{up}_{i-1}^\circ
    && \text{for every $0 < i \leq n$ and $\circ \in \{+, -\}$,} \\
    %
    \mathsf{cancel}_{i,q} &\mapsto \mathsf{cancel}_{i,\q{f}}^{-1}
    && \text{for every $0 \leq i \leq n$ and $q \in B$,} \\
    %
    \mathsf{cancel}_{i,q}^{-1} &\mapsto \mathsf{cancel}_{i,\q{f}}
    && \text{for every $0 \leq i \leq n$ and $q \in B$,}\\
    %
    \mathsf{swap}_{p, q}^x &\mapsto \mathsf{swap}_{q, p}^x
    && \text{for every $p, q \in N$ and $x \in X$.}
  \end{align*}
  Note that $t_i'$ is not the exact reverse transition of $t_i$, as it
  may differ over $B$. Indeed, $t_i'$ may require an agent in state
  $\q{f}$, which may not have been produced by $t_i$. However, this is
  not an issue since, by definition of $\mathrm{false}$ and by
  \cref{prop:thr:prop}~\eqref{itm:preservation}, we have:
  $$\mathrm{false}(C_{i+1})(\q{f}) = C_{i+1}(B) \geq L(B) > 0.$$ Thus, we have
  $\mathrm{false}(C_{i+1}) \trans{t_i'} \mathrm{false}(C_i)$ as desired, which
  completes the proof.

  \medskip\noindent\emph{Correctness.} Let $\pi$ be an initialization
  sequence with effective input $\vec{w}$ such that $L' \trans{\pi} C$
  for some $L' \succeq L$.
  Let $\sigma$ be a fair execution of $\PP_\infty$ starting from $C$.
  By \cref{prop:threshold:stabilize}, there exist
  $i \in \N$, $m_+ \geq 0$ and $m_- \leq 0$ such that:\smallskip
  \begin{enumerate}[(a)]
    \item $\sigma_i(X) = \sigma_{i+1}(X) = \cdots =
      0$, \label{itm:input:stab}

    \item $\val^\circ(\sigma_i) = \val^\circ(\sigma_{i+1}) = \cdots =
      m_\circ$ for both $\circ \in \{+, -\}$, \label{itm:val:stab}

    \item $m_+ = 0 \lor m_- = 0$.
  \end{enumerate}

  First, let us show that $O(\sigma) \in \{0, 1\}$. We make a case
  distinction on whether $m_+ \geq b$.\medskip

  \noindent\emph{Case $m_+ \geq b$.} We show that $O(\sigma) =
  1$. Note that $m_+ \geq b > 0$ which implies that $m_- = 0$. Thus,
  by~\eqref{itm:val:stab}, no $\mathsf{cancel}$ transition is enabled
  in $\sigma_j$ for every $j \geq i$. Thus, it suffices to show that
  $\sigma_j(\q{f}) = 0$ for some $j \geq i$. For the sake of
  contradiction, suppose this is not the case. Let $j \geq i$ be such
  that $\sigma_j(\q{f}) > 0$. We claim that $\sigma_j$ can reach some
  configuration $D_j$ enabling transition $\mathsf{equal}$,
  \ie\ larger or equal to $\mathrm{rep}(b)$. This claim, together with
  fairness, yields a contradiction since this transition can move all
  agents in state $\q{f}$ to state $\q{t}$.

  Let us prove the claim. By \cref{cor:enough:zero}, we have $\sigma_j
  \trans{T_\infty^*} C_j$ where $C_j(\q{0}) \geq n$. Note that $\val^+(C_j) =
  \val^+(\sigma_j)$. If $\val^+(C_j) = b$, then, by cleanness, $C_j$
  contains precisely the binary representation of $b$, and hence $C_j
  \geq \mathrm{rep}(b)$. Thus, assume $\val^+(C_j) > b$. Let $0 \leq d
  \leq n$ be the largest exponent for which there exists a state $q
  \in P_X$ such that $C_j(q) > 0$, $\val(q) = 2^d$ and $d \not\in
  \mathrm{bits}(b)$. Since $C_j(\q{0}) \geq n \geq d$, the sequence of
  transitions $\mathsf{down}_d^+ \cdot \mathsf{down}_{d-1}^+ \cdots
  \mathsf{down}_1^+$ can be fired from $C_j$, which yields a
  configuration $D_j \geq \mathrm{rep}(b)$.\medskip

  \noindent\emph{Case $m_+ < b$.} We show that $O(\sigma) = 0$. First note
  that $\mathsf{equal}$ is disabled in $\sigma_j$ for every
  $j \geq i$, as otherwise we would have
  $\sigma_j \geq \mathrm{rep}(b)$ which implies that $m_+
  = \val^+(\sigma_j') \geq b$. Thus, it suffices to show that there
  are infinitely many indices $j$ such that $\sigma_j(\q{f}) >
  0$. Indeed, if this is the case, then, by fairness, $\mathsf{false}$
  permanently moves all agents in state $\q{t}$ to state $\q{f}$.

  For the sake of contradiction, suppose the claim does not hold.
  Let $\sigma' \defeq \pi\sigma$. Let $j \in \N$ be the largest index
  such that $\sigma_j'(\q{f}) > 0$.
  Note that this configuration exists as $\sigma_0' = L' \succeq L$ and $L(\q{f}) > 0$.
  The only transition that reduces the number of agents in $\q{f}$ is $\mathsf{equal}$.
  Thus, $\sigma_j' \trans{\mathsf{equal}} \sigma_{j+1}'$ and $\val^+(\sigma_j') \geq b$.
  As finally, $m_+ < b$, some $\mathsf{cancel}$ or $\mathsf{add}^{-1}$ transition
  must be fired in $\sigma'_{j'}$ for some $j' > j$.
  In both cases there is afterwards an agent in state $\q{f}$.
  This contradicts the maximality of $j$. \medskip

  We are done proving $O(\sigma) \in \{0, 1\}$. It remains to
  argue that $O(\sigma) = \varphi(\vec{w})$. We have:
  \begin{align*}
    \vec{a} \cdot \vec{w}
    %
    &= \val(\sigma_i)
    && \text{(by Prop.~\ref{prop:thr:prop}~\eqref{itm:val:inv})}\\
    %
    &= \val^+(\sigma_i) + \val^-(\sigma_i)
    && \text{(by~\eqref{itm:input:stab})} \\
    %
    &= m_+ + m_-.
    && \text{(by~\eqref{itm:val:stab})}
  \end{align*}
  Recall that $m_+ \geq 0$, $m_- \leq 0$ and $(m_+ = 0 \lor m_- =
  0)$. If $\vec{a} \cdot \vec{w} \geq b$, then we must have $m_+ \geq
  b > 0$ and $m_- = 0$. Therefore, the first case above holds, and
  hence $O(\sigma) = 1$, which is correct. If $\vec{a} \cdot \vec{w} <
  b$, then we must have $m_+ < b$. Therefore, the second case above
  holds, and hence $O(\sigma) = 0$, which is also correct.
\end{proof}

redpajama_set_name: RedPajamaArXiv