Active Set in GraphX Pregel

The original Pregel computation abstraction takes a vertex-centric view to express graph programs. In this abstraction, a vertex is a two-state machine which is either inactive or active. Each active vertex concurrently runs a vertex program, which can send messages to other vertices, update the value of the vertex, or deactivates the vertex (aka. votes to halt). A deactivated vertex remains inactive in subsequent execution steps unless it receives a message. A vertex activated by a message must vote to halt again to get deactivated. No computation is associated with edges.

The GraphX computation framework realizes Pregel based on the Gather-Apply-Scatter (GAS) pattern. GAS breaks down the computation of vertex program into purely edge-parallel and vertex-parallel stages with three user-defined functions, called gather, apply and scatter: the gather function is an associative and commutative operator over the inbound messages of a vertex; the apply function operates on a vertex and updates its value based on the inbound message; the scatter function computes and sends messages along each edge. Note that, unlike more standard implementations of Pregel, GraphX Pregel does not allow modifying edge attributes and graph topology during execution. Besides, it allows message exchanges only between the neighboring vertices. These restrictions are imposed so as to increase parallelism and enable more optimizations within GraphX.
GraphX Pregel does not provide operations to deactivate a vertex (i.e. to let a vertex vote to halt). Instead, it automatically avoids executing the scatter function on edges where neither endpoint has received a message. These edges will remain skipped until their endpoints receive a message again. Hence, an edge in GraphX Pregel is also a two-state machine, just like a vertex in the original Pregel: an edge will be deactivated if its endpoints do not receive any message and will be activated after its endpoints receive a message. In practice, GraphX decides whether an edge is activated or not by bookkeeping the set of vertices that received messages from the last execution step, called the active set. Hence, an edge is activated iff it is incident to some vertex in the active set. In addition, GraphX also uses the size of the active set as an indicator of workload and adjust message delivery strategy accordingly at runtime.
Adopting the bookkeeping mechanism allows GraphX Pregel to avoid unnecessary computation and adjust its message delivery strategy at runtime. The mechanism, however, can increase the complexity to reason about the behaviors of a Pregel program. Fortunately, it turns out that enabling bookkeeping does not change the observable behaviors of a Pregel program under certain conditions. More precisely, we have the following two facts:
Fact 1. The outcome of a GraphX Pregel program is not affected by the choice of message delivery strategy if the gather function is associative and commutative.
Fact 2. The outcome of a GraphX Pregel program is not affected by the bookkeeping mechanism if the scatter function only depends on the edge triplet, namely, the edge attribute, the source vertex, and the destination vertex.
The first fact is clear. To see why the second fact is true, consider two versions of GraphX frameworks, one of which executes the scatter function only on activated edges and the other executes it on all edges. Given the condition in Fact 2 and a deterministic apply function, we will show that a Pregel program produces the same output graph in both frameworks from the same initial message and input graph. The proof is done by induction on the number of execution steps taken by the program:
Step 0. Since the apply function is deterministic and the initial message is sent to all vertices without executing the scatter function, the program produces the same graph in both frameworks after the first step.
Step n+1. Suppose the program produces the same graph after the nth step. Consider an edge e in the (n+1)-th step. If e is active, then the scatter function behaves the same on it in both frameworks. If e is inactive, then two facts about its endpoints hold in the last step: i) they did not receive any message from e, and ii) they did not change values. Since the scatter function only checks the edge triplet of e, which is unchanged since the last step, the function will not send any message along e even if it is executed on e in this step. Hence, the scatter function sends the same messages to the same vertex in both frameworks. Moreover, since the gather function is associative and commutative, each vertex receives the same reduced inbound message in both frameworks. Finally, since the apply function is deterministic, the program will produce the same graph in both frameworks after the (n+1)-th step. This concludes our proof.
Note that the condition in Fact 2 holds when the scatter function is pure. Hence, we can safely assume that all edges are activated when we are simulating or reasoning about a pure Pregel program in GraphX. In the original Pregel model, however, active set is essential to decide whether vertex program should be executed on a vertex. It is the GAS decomposition and the restriction on edge modification that enable us to eliminate the use of active set in GraphX.

References

1. Pregel API in GraphX Programming Guide and its source code on GitHub.
2.Xin, Reynold S., et al. "Graphx: A resilient distributed graph system on spark." First International Workshop on Graph Data Management Experiences and Systems. 2013.
3. Xin, Reynold S., et al. "GraphX: Unifying data-parallel and graph-parallel analytics." arXiv preprint. 2014.
4. Gonzalez, Joseph E., et al. "Graphx: Graph processing in a distributed dataflow framework." OSDI. 2014.

Equality in first-order logic

First-order logic (FOL) can be discussed with and without regarding identity as a in-built relation. This difference matters because the semantic of identity ("anything is equal to nothing but itself") is not definable in FOL. Hence, different ways to express the concept of identity lead to different models. By contrast, identity is definable in SOL, so the issues discussed here is not a problem in SOL.

First-order logic with identity

FOL with identity is a logic where "$=$" is a primitive logic symbol, i.e., symbols with the same semantics across all possible model. As a logical symbol, we stipulate that any model $\mathcal A$ of the logic always interpreted "$=$" to the identity relation on ${\rm Dom}(\mathcal A).$ Furthermore, the incorporation of equality adds three "Axioms of Equality" to the deduction system of the logic: reflexivity and the substitution for formulas, where the second axiom (aka. Leibniz's law) is an axiom schema. Other properties such as symmetry and transitivity can be derived from these two axioms.
Remark. Note that the Axioms of Equality are actually not axioms but inference rules. In fact, these axioms do NOT characterise equality––what they characterise are arbitrary equivalence relations on the domain of discourse that is congruent with respect to the functions and relations of the interpretation.
Example. Peano Arithmetic is the FO theory of $(\omega, +, succ)$ with identity, but Modulo Arithmetic is a FO theory without identity. Instead, for a fixed $n>0$, an equivalence relation $\equiv_n$ is defined such that $a \equiv_n b$ iff $a \equiv b$ mod $n$.

First-order logic without identity

Consider a vocabulary $\sigma$ where equality is not a logical symbol. A theory that contains the Axioms of Equality is called a theory with equality. Let $T$ be such a theory of $\sigma$ where the Axioms of Equality, denoted as $A_{\rm eq}$, are defined for a binary relation $\sim$. Given a model $\mathcal A$ of $T$, it is possible that $a\sim^{\mathcal A} b$ but $a\neq b$ although $a$ and $b$ will satisfy exactly the same formulas in ${\mathcal A}$ by Leibniz's law. On the other hand, we can define the quotient structure $\mathcal B := \mathcal A/\!\!\sim$ of $\mathcal A$. Clearly, $a\sim^{\mathcal B} b$ if and only if $a=b$.

Now we have two methods to define equality in FOL. What would be the difference anyway? The first thing to note is that satisfiability is independent of which method is used. To see this, let $F$ be a formula of vocabulary $\sigma$ plus equality and let $F'$ be the formula obtained by replacing all "$=$" in $F$ with "$\sim$". Consider the theory $T_F := A_{\rm eq}\cup\{F'\}$. Note that if $\mathcal A$ is a model of $T_F$ then $\mathcal A/\!\!\sim$ is a model of $F$. It follows that $F$ and $T_F$ are equi-satisfiable, as concluded in the following facts:
Fact. A formula $F$ is satisfiable in FOL with identity iff $T_F$ is satisfiable in FOL w/o identity.
Fact. A formula $F$ is valid in FOL with identity iff $A_{\rm eq}\implies F$ is valid in FOL w/o identity.
Let $T$ be a theory of a vocabulary with $\sim$. A model $\mathcal A$ is called a normal model of $T$ if $\mathcal A$ is a model of $T$ and $a\sim^{\mathcal A} b$ implies $a=b$. Hence, a theory with equality has a model iff it has a normal model. Results about FOL in the literature often assume identity with the notion of normal model, these results can be easily rephrased without identity. For example,
Theorem. (Compactness with identity) Given a set of formula $\Sigma$, if any finite subset of $\Sigma$ has a model, then $\Sigma$ also has a model.
Theorem. (Compactness w/o identity) Given a set of formula $\Sigma$, if for any finite subset of $\Sigma$ has a normal model, then $\Sigma$ also has a normal model.

References

The Logic of Equality, Leon Henkin, 1977.

A note on semi-linear and regular sets

Regular sets

A set is called regular if it can be recognised by a finite DFA. For $L\subseteq\Sigma^*$, $\sim_L$ is called a right congruence iff $u\sim_L v \iff uw\sim_L vw$ for all $w\in\Sigma^*.$ Note that a right congruence is an equivalence relation. The classes of $\sim_L$ induce a minimal complete DFA recognising $L.$ Intuitively, words belonging to the same class in $\sim_L$ lead to the same state in the DFA. The classes containing the empty string and the strings in $L$ correspond to the initial state and the final states, respectively.
Myhill-Nerode Theorem. A set $L$ is regular iff $\sim_L$ has finite index over $\Sigma^*.$
Rational sets. A set is called rational iff it can be generated from a finite number of finite subsets of $\Sigma^*$ through a finite number of rational operations, namely union, concatenation and the Kleene star.
Kleene's theorem. A set of words is regular iff it is rational. (Note: The only-if part doesn't holds for non-length-preserving relations.)

Semi-linear sets

A subset of $\mathbb N^k$ is linear if it can be expressed as$$u_0 + \langle u_1, \dots, u_m \rangle = \{u_0 + a_1u_1 + \dots + a_mu_m \mid a_1, \dots, a_m \in \mathbb{N}\}$$such that $u_0,...,u_m$ are vectors of dimension $k$. A set is called semi-linear if it is a union of finitely many linear sets.
Fact. Semi-linear sets are closed under complement, intersection, projection, etc., in an effective way.
Fact. A set is semi-linear iff it is Presburger-definable.
Fact. If a set is upward-closed or downward-closed, then it is semi-linear.

Parikh image. Let $\Sigma=\{a_1,...,a_k\}$. Given a word $w$, we use $|w|(a)$ to denote the number of occurrences of symbol $a$ in $w$. A function $\phi:\Sigma^*\rightarrow\mathbb N^k$ is called the Parikh image if the $i$-th component of $\phi(w)$ is $|w|(a_i).$ [note]

Fact. Parikh image is a morphism from monoid $(\Sigma^*,\cdot,\epsilon)$ to monoid $(\mathbb N^k,+,0).$
Fact. A set $S\subseteq \mathbb N^k$ is semi-linear iff there is a regular set $R\subseteq\Sigma^*$ such that $\phi(R)=S$, where $\phi$ is the Parikh image. [1]

From RE to its Parikh image. The key observation to computing the Parikh image of a regular set is to describe the depths of Kleene stars by constraints over the dependency between frequencies. For example, $(a^*b)^*$ can be reduced to $a^*b^*$ plus a constraint "$|w|(b)=0$ implies $|w|(a)=0$", which can further resolve to two linear conditions "$|w|(b)=0\wedge |w|(a)=0$" and "$|w|(b)\ge 1 \wedge |w|(a)\ge 0$" corresponding to a union of two linear sets. See [2] and the references therein for more details abort constructions.

Parikh's Theorem. [1] If $L$ is a context-free language then there exists a regular language $R$ such that $\phi(L)=R.$ (This implies CFL and RL are indistinguishable when the alphabet is commutative.)

Real numbers

A relation in real closed fields is definable in the first-order logic if and only if it is a Boolean combination of polynomial equations [?].

Connection with logic

Connection with MSO. [Buchi] A set $L\subseteq\Sigma^*$ is regular iff it can be defined in $MSO(\Sigma, <_{\mathbb N}, \{P_a\}_{a\in\Sigma})$. [slide]
Connection with LTL. [?] A set is LTL-defiable iff it is $FO(\Sigma^\omega, <_{\mathbb N}, \{P_a\}_{a\in\Sigma})$-definable.
Connection with FO. A regular expression constructed without the Kleene star is called star-free. For example, $(ab)^*$ is star-free but $(aa)^*$ is not. McNaughton showed that a regular set is star-free iff it can be defined in $FO(\Sigma, <_{\mathbb N}, \{P_a\}_{a\in\Sigma})$, cf. [3]. Hence, checking star-freeness of a regular expression is equivalent to checking whether an MSO-formula is FO-definable. The former problems is shown to be PSPACE-complete, see here and here. This complexity result is generalised to checking star-freeness of rational relations, see here.

References

1. On Context-Free Languages, J. ACM, 1966.
2. Semi-linear Parikh Images of Regular Expressions via Reduction, MFCS10.
3. First-order definable languages, 2008.
4. Jewels of Formal Language Theory, 1982.

A note on checking properties of regular languages

Deterministic Finite Automata

Equivalence. If a DFA with $n$ states does not accept every string, it rejects some string of length at most $n-1$. It follows that the languages of two DFA $A$ and $B$ coincide iff they accept the same words up to length $|A|\cdot|B| - 1$. (Hint: consider automaton $A\times B$.) This observation leads to an exponential-time algorithm for language equivalence checking. In practice, equivalence between DFA is often checked by first minimising the DFA (see below). Isomorphism between DFA can be checked in linear time when an appropriate representation is used, cf. Hopcroft's method.

Minimisation. The minimal DFA of a regular language is unique by the Myhill-Nerode Theorem. We can hence check language equivalence of DFA by checking isomorphism between DFA. DFA minimisation takes $O(|\Sigma|\cdot n\log n)$ time using Hopcroft's method, which is the most commonly used approach in practice. Aho, Hopcroft and Ullman proposed an algorithm that uses union-and-find to create and locate the equivalence classes for states in a DFA (cf. Sec. 3 of [2]). The running time is $O(kn\!\cdot\!A(kn,n))$ with $k=|\Sigma|$.

Universality can be checked by checking that all reachable states are accepting.
Complement is obtained by simply flipping the accepting and the non-accepting states.
Aperiodicity (ie. existence of non-trivial cycles) of a DFA is PSPACE-complete, cf. here.
Intersection vacuity of an unbounded number of DFA is PSPACE-complete, cf. here and here.
Reversal. The trivial way to get the DFA of the reverse language is to determinise the NFA obtained by flipping the initial and the accepting states and reversing the directions of the transitions. This approach leads to exponential blowup. It is unclear as to the lower bound of this problem.

Non-deterministic Finite Automata

Equivalence. NFA equivalence problem is PSPACE-complete --- in fact, it is the first problem shown to be in this complexity class, see [5]. Practically, checking equivalence of NFA is often done by first converting NFA to DFA using subset construction, which however can lead to exponential growth in automata size. There are other determinisation methods in the literature, c.f. wiki and [4].

Universality. Using determinisation, if an NFA of size $n$ does not accept every string then it rejects some string of length at most $|\Sigma|^n-1$. Together with the classic result that reachability can be checked is in NL, we easily see that university checking for NFA is in PSPACE. One can show that the problem is PSPACE-complete and it is so even when every state of the NFA is accepting.

Complement. Complementing a DFA can be easily done by flipping the accepting and the non-accepting states. This method doesn't work for NFA: the language of the "flipped" NFA will be the superset of its complement in general (e.g., consider the NFA $\{q_0 \xrightarrow{a} q_1, q_0 \xrightarrow{a} q_2\}$ where $q_1$ is accepting). In [6], the authors give very precise bounds for complexities for complement on NFA. Particularly, there are NFA with exponentially large complement: the language of all words over $\{1,…,n\}$ which don't contain all symbols is accepted by an NFA of size $n$, but its complement needs $2^n$ states. Hence, complement of NFA is EXPSPACE-complete; no general method for complementing NFA can have better complexity than doing subset construction in theory.

Minimisation. Minimisation to/from NFA is PSPACE-hard. Given a DFA or an NFA, it is PSPACE-hard to find the size of the minimal equivalent NFA. Some hardness of approximation results have shown that it is even hard to approximate the size of the minimal equivalent NFA. Since a regular expression can be converted to an NFA of comparable size, these hardness results show that we can't expect any efficient algorithm to convert an regular expression to a minimal NFA. See these lecture notes by Artem Kaznatcheev for more details.

Regular expressions

Equivalence. Like NFA, checking equivalence of RE is PSPACE-complete. This can be expected since RE can be converted to and from NFA of roughly the same size, the complexity of checking properties of RE should be comparable to that of checking NFA. However, if intersection is allowed then the difficulty rises to EXPTIME. Further, if negation is allowed then the problem becomes non-elementary [5].

Star-freeness of RE is PSPACE-complete, see here. This problem corresponds to checking the non-existence of non-trivial cycles in DFA, which is also PSPACE-complete.
Emptiness for regular expressions with intersection is PSPACE-complete.
(Often, checking the a property for DFA is far more efficient than checking the same property for RE. So it is surprising to note that the above two problems have the same complexity for both DFA and RE.)

Star-free Regular expressions

Checking equivalence of star-free RE is NP-complete, cf. Section 2 of [3].

Resources

• Online converters: RE-to-NFA, NFA-to-RE, NFA-to-DFA
• RE equivalence matching in the wild:
  1.Backtracking (used in Perl, Python, etc): Discussion, Demo, Code
  2.Virtual-machine method (used in Ruby): Explanation

References

1. Equivalence of regular languages.
2. Testing the Equivalence of Regular Languages
3. On the equivalence, containment, and covering problems for the regular and context-free languages
4. Five determinisation algorithms
5. Word problems requiring exponential time
6. State Complexity of Concatenation and Complementation of Regular Languages
7. Complexity of Some Problems from the Theory of Automata

A note on the expressiveness of logic

Reachability problem. Fix a graph $\mathcal{G}$. A vertex $u$ is said to be reachable from a vertex $v$ in $\mathcal{G}$ if there exist $r \ge 0$ vertices $x_1$, ..., $x_r$, such that $(v, x_1)$, $(x_1, x_2)$, ..., $(x_{r−1}, u)$ are edges of $\mathcal{G}$. A formula $\phi(x,y)$ with exactly two free variables $x, y$ and one relation symbol $E$ is said to "express" reachability if and only if for any finite graph $\mathcal{G}$, vertex $u$ is reachable from vertex $v$ in $\mathcal{G}$ if and only if $\mathcal{G}$ is a model of $\phi(x,y)$ with respect to some interpretation that associates $E$ to edge relation and $x,\ y$ to vertices $u,\ v$.
Reachability is not expressible in first-order logic. Suppose $\phi(x,y)$ is a FO logic formula expressing reachability. Define three sentences $s_1$, $s_2$, and $s_3$, such that
$s_1 \equiv \forall x \forall y. \phi(x, y)$, i.e., all vertices are reachable from all vertices;
$s_2 \equiv \forall x. (\exists y. E(x, y) \wedge \forall z. E(x, z) \implies z = y)$, i.e., every vertex has out-degree one;
$s_3 \equiv \forall x. (\exists y. E(y, x) \wedge \forall z. E(z, x) \implies z = y)$, i.e., every vertex has in-degree one.
Let $s \equiv s_1 \wedge \ s_2 \wedge \ s_3$. Observe that a graph is a model of $s$ if and only if the graph is cycle. Since there are finite cycles with as many vertices as desired, $s$ has arbitrary large finite models. It then follows by Lowenheim-Skolem theorem that $s$ has an infinite model. But infinite cycles do not exist, and thus our assumption that there exists a FO logic formula expressing reachability is contradicted.
Reachability is expressible in second-order logic. Given constants $x$ and $y$ and a binary relation symbol $L$, we use the following sentences to characterize $L$ as a path from $x$ to $y$:
1. $L$ is a linear order over the vertices : $$ \begin{align*} \psi_1 \equiv\ & \forall u. \neg L(u,u) \\ & \wedge \forall u\forall v. (L(u,v) \implies \neg L(v,u)) \\ & \wedge \forall u\forall v \forall w. (L(u,v) \wedge L(v,w) \implies L(u,w)) \end{align*} $$ 2. Any two consecutive vertices in the order must be joined by an edge: $$ \begin{align*} \psi_2 \equiv\ &\forall u \forall v. ((L(u,v) \wedge \forall w. (\neg L(u,w) \vee \neg L(w,v))) \implies E(u,v)). \end{align*}$$3. The first vertex in the order is $x$, the last vertex is $y$, and $x$, $y$ are in the order: $$ \psi_3 \equiv (\forall u.\ \neg L(u,x)) \wedge (\forall v.\ \neg L(y,v)) \ \wedge L(x,y).$$ Now an expression for reachability can be defined as$$\phi(x,y) \equiv \exists L. ((x=y) \vee (\psi_1 \wedge \psi_2 \wedge \psi_3)).$$

Expressiveness of first-order Logic

It was known that the natural deduction proof system for FO logic is both sound and complete. Therefore, since verifying a proof is mechanical, deriving a proof must be as hard as checking its validity. Hence it is impossible to build a perfect automatic theorem prover for FO logic. In fact, validity of FO is undecidable since FO can formulate the Post correspondence problem. On the other hand, validity of FO is easier than satisfiability, since the former is enumerable while the latter is not.
Suppose we have only equality and edge relation in our language. A $\phi$-graph problem is to decide whether there exists an interpretation such that a given finite graph is a model of formula $\phi$. The class L-graph is formed by all $\phi$-graph problems where $\phi$ is a formula defined in logic L.
Fact. FO-graph is strictly in $P$.
The inclusion is strict because reachability problem (which is P-complete) is not expressible in FO and thus not captured by FO-graph. In fact, any FO-graph problem can be decided in LOGSPACE (check this). Immerman and Vardi (1982) added inductive definitions to FO to get the logic LFP, which is sufficient to express P problems over ordered graphs, namely, there is a distinguished relation $<$ that is interpreted as a linear order over the vertices.
Theorem. (Immerman-Vardi 1982) LFP-graph is in $P$.
However, for graphs without the ordering assumption, there are easily poly-time computable properties that are not definable in LFP. Hence LFP is still too weak to capture $P$. Grohe, Holm, and Laubner have added linear-algebraic operators to LFP. This properly extends the power of LFP with counting, but its relationship to $P$ remains an open question.

Expressiveness of second-order Logic

Second-order logic (SO) extends first-order logic with quantifications over relations and sets. Monadic second-order logic (MSO) is the restriction of SO where the second-order quantifiers are only over sets. Existential second-order logic (ESO) is a restricted version of SO where only existential quantifications are allowed.
Fact. MSO-graph is strictly between P and NP, since 3-colorability is in MSO-graph but Hamiltonian path problem is not (the latter two problems are NP-complete). However, Hamiltonian path problem can be captured by extending MSO with quantifiers over sets of edges.
The following result shows that ESO is in some senses the normal form of SO.
Proposition. (Buchi 1976) Any MSO formula can be re-written to an equivalent EMSO formula.
ESO-graph captures NP. It is straightforward to show that ESO-graph is in NP by non-deterministically choosing a relation for in polynomial time. Now let $\phi_1$ and $\phi_2$ be defined as before. In addition, define $\phi_4 \equiv \forall u\forall v. L(u, v)\vee L(v, u) \vee u = v$. Observe that $\mathcal{G}$ is a model of $\exists L. \psi_1 \wedge \psi_2 \wedge \psi_4$ if and only if $\mathcal{G}$ contains a Hamiltonian path. Since deciding the existence of a Hamiltonian path is NP-complete, we have
Theorem. (Fagin, 1974) $NP$ = ESO-graph.
By Fagin's theorem, ESO is closed under negation if and only if NP = co-NP. Since P $\subseteq$ NP$~\cap~$co-NP, second-order logic covers all languages in the polynomial time hierarchy. Other second-order concepts, e.g., least fixed-point operator and transitive closure operator, lead to logics which characterise further complexity classes like P, NLOGSPACE, PSPACE. For these results of descriptive complexity theory see [1].
The "weak" MSO (WMSO) is a further restricted version of MSO such that the set quantifiers range only over finite sets. The WMSO theory of $(\mathbb N, <)$ is a particular useful theory called Weak (monadic) Second-order Logic with one Successor (WS1S). Buchi has shown that WS1S is decidable via automata-theoretic approaches.
Theorem. (Buchi 1960) One an effectively construct an input-free finite automaton $A_\varphi$ from a sentence $\varphi$ in WS1S, such that $L(A_\varphi)\neq \emptyset$ iff $\varphi$ holds. Conversely, given an input-free automaton $A$ one can defined a sentence $\varphi_A$ in WS1S such that $L(A)\neq \emptyset$ iff $\varphi_A$ holds.
The idea of reduction is to represent numbers in binary, namely, as finite words over $\{0,1\}$, and to view a finite word as the (characteristic function of) a finite set via finite-set interpretation [3,4]. For instance, integer $21$ corresponds to the word $10101$, which is interpreted to a finite set $\{1,3,5\}$.

It is interesting to note that the expressiveness power of WS1S is equivalent to a first-order theory. Presburger Arithmetic (PA) is the first-order theory of the structure $(\mathbb N, +)$. In Buchi's 1960 paper it is noted that the decidability of PA can be inferred from that of WS1S. The decidability of Presburger arithmetic follows by translating first-order sentences in the signature $+$ to WS1S. To translate back from WS1S (or from finite automata), we would need to extend PA with some arithmetical means such as $|_2$, which associates each number $m>0$ with the greatest power of 2 that divides $m$. [4]
Theorem. A relation is definable in WS1S iff it is definable in the FO theory of $(\mathbb N, +, |_2)$.

References

1. Finite Model Theory, Springer-Verlag, New York 1995.

2. Languages, Automata, and Logic, Handbook of Formal Languages, Volume 3.
3. Transforming structures by set interpretations. LMCS 2007.
4. Automatic Structures. PhD Thesis. 2004.

Intuition behind a mathematical puzzle

Sometimes, it is helpful to reason about a mathematical puzzle in a concrete context. A solution may reveal itself after you reword the problem statement in intuitive terms. The following example shows how the solution to a seemingly nontrivial problem becomes obvious after the statement of the problem is reworded appropri-ately.
Example. Consider the following function:

function f (n: int) {
  if n == 1 return n
  choose integers a, b ≥ 0 such that a + b == n
  return a * b + f(a) + f(b)
}

Our goal is to show that the output of f(n) does not depend on how a and b are determined in the function body. This fact is far from obvious by inspecting the code. A standard approach to show this kind of fact is via mathematical induction. However, to establish the induction hypothesis, one must first express the value of f(n) in $n$. This is not easy given that values of a and b are not specified. Besides, an inductive proof typically proceeds by manipulating formulas. In that case, the proof itself is not very helpful for us to gain insights to the fact it proves.
On the other hand, the fact turns evident once you notice what the function intends to compute. The key observation here is that f(n) effectively counts the number of hand-shaking in a group of $n$ people. A group of size $n$ is is divided into two groups of size $a$ and $b.$ People from different groups then shake hand with each other. This process continues recursively until no smaller group can be form. At that time, each person eventually shakes hand with everybody else for exactly once. Therefore, the value of f(n) is $n\cdot(n-1)/2$ regardless of how groups are divided during the process.

A technique called double counting is closely related to the idea expressed above.
Example. We know that there are ${n \choose k}$ ways to select a set of size $k$ from a set $S$ of $n$ distinct elements. If $S$ is divided into two partitions of size $a$ and $b$, then selecting a subset from $S$ amounts to selecting a subset from each of the partitions respectively. Therefore, no matter how the partitions are divided, i.e., $a + b = n$, we have $$\sum_{i+j=k}{a \choose i}{b \choose j} = {n \choose k}$$(recall that ${n \choose 0}=1$ and ${n \choose k}=0$ for $k<0$ or $k>n$).