Limits of sets

Wikipedia has an article that rigorously defines this concept using scaring symbols such as limsup, liminf, bigcap, and bigcup. However, I found a post on MO that explains the same idea intuitively. The keypoint is we can categorize every point ever appearing in the infinite sequence of sets $S_1,S_2,...$ into three partitions:
I) Present in the all but finitely many sets
II) Present only in finitely many sets
III) Present in and absent from the sets infinitely often
If partition III is nonempty then the limit of the sequence clearly doesn't exist. If the limit does exist, then it should contain exactly the points in partition I. The limit of a monotone set sequence always exist because every point in this sequence falls in the first two partitions. Hence for any sequence of sets $S_1,S_2,...$ the following sequences converge: $A_n\equiv \bigcup_{i=1}^n S_i$, $B_n\equiv \bigcup_{i=n}^\infty S_i$, $C_n\equiv \bigcap_{i=1}^n S_i$, $A_n\equiv \bigcap_{i=n}^\infty S_i.$

A note on frameworks for computational logics

A fundamentional computational assumption

SMT-based verification techniques such as [1,..] make fundamental assumptions about an background structure $\mathfrak{S}$, an r.e. universe $U$, and an r.e. set $\Phi$ of quantifier-free formulas such that
1. All elements of $U$ can be named by ground terms in the language of $\mathfrak{S}$.
2. All quantifier-free formulas in the language of $\mathfrak{S}$ are in $\Phi$.
3. If $a\in U$ and $\varphi \in \Phi$, then $\varphi[a/x]\in \Phi$.
4. If $\varphi_1, \varphi_2 \in \Phi$, then $\varphi_1\vee \varphi_2$, $\varphi_1\wedge \varphi_2$, and $\neg \varphi_1$ are all in $\Phi$.
5. Satisfiability of formulas in $\Phi$ is decidable.
Expressiveness. The above formalism does not capture all decidable languages. For example, it cannot express context-free languages as they are not closed under intersection. However, the formalism does embody the basic properties of the theories supported by any state-of-the-art SMT solver.
Working with a solver. The specialisation on quantifier-free formulas is important for SMT solvers, since theory combination in SMT solvers use quanti er free formulas and becomes undecidable when quantifiers are allowed. This fact limits what we are allowed to express in $\mathfrak{S}$ without sacrificing decidability – in general, only positive existential quantifiers are allowed, while other quantifiers are not.
Computation of witness. The assumption that $U$ is r.e. allows us to effectively compute a witness whenever a formula is satisfiable. Here effectiveness means that we have a solver which decides satisfiability and finds a witness in a finite number of steps.

Multi-typed universe & structure

In [2, 3], the background universe $U$ is an r.e. multi-typed carrier set. For each type $\tau,$ $U$ contains a sub-universe $U^\tau$ of elements of type $\tau$. For example, $U^{Bool} = \{⊥, ⊤\}$ and $U^{Int} = ℤ$. Terms are defined by induction over the language of $𝔖$ and are assumed to be well-typed. In a multi-typed structure, formulas are simply terms of type $Bool$, i.e., no distinction is made between formulas and Boolean terms. As before, we assume that all elements in $U$ can be named by the ground terms in the language.
Interpretations. An uninterpreted function symbol of arity n ≥ 1 is a function symbol $f$ with a domain sort $\sigma_1 × ⋯ × \sigma_n$ and a range sort $\sigma$. An interpretation for $f$ is a function from $U^{\sigma_1} × ⋯ × U^{\sigma_n}$ to $U^\sigma$. An interpretation of a variable of sort $\tau$ is an element in $U^\tau$. A constant is also called a function symbol of arity 0.
Semantics. The Tarski semantics of a closed term $t : \tau$ is denoted by $[\![ t ]\!] ∈ U^\tau$. For example, given a $\lambda $-term $\lambda x. t : \tau → \sigma$, $[\![ \lambda x. t ]\!]$ denotes a function mapping $a ∈ U^\tau$ to $[\![ t[x/a] ]\!] ∈ U^\sigma$. A $\lambda $-term $φ : \tau → Bool$ is called a $\tau$-predicate. Note that the semantics of $\tau$-predicates is defined differently than other $\lambda $-terms: given a $\tau$-predicate $φ$, we shall use $[\![ φ ]\!]$ to denote the set $\{ a ∈ U^\tau ∣ [\![ φ ]\!](a) = ⊤ \}$. Hence $\tau$-predicates are closed under Boolean operations, e.g., $[\![ φ ∧ ψ ]\!] = [\![ φ ]\!] ∩ [\![ ψ ]\!]$, $[\![ ¬φ ]\!] = U^\tau \setminus [\![ φ ]\!]$, etc. Under the previous assumption, satisfiability for $\tau$-predicates is decidable and a witness is computable. Hence we can assume for $\tau$-predicates an effective function $w_\tau$ such that $w_\tau(φ) ∈ [\![ φ ]\!] ∪ \{ ⊥ \}$.

References

1. Monadic Decomposition, Journal of ACM, 2017.
2. Symbolic Transducers, Microsoft Technical Report, 2011
3. Symbolic Finite State Transducers: Algorithms and Applications, POPL 2012.

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