Some interesting proofs using oracles

A proof with oracles exploits the following two facts about Turing Machines (TMs): 1) there exist effective representations of TMs as strings, and 2) a TM can simulate other TMs taking their representation as input. Any argument that only relies on these two facts about TMs treats them as black boxes. This post tries to collect some results with interesting oracle proofs that sketches the proof ideas.$\newcommand{\P}{{\sf P}}$ $\newcommand{\NP}{{\sf NP}}$ $\newcommand{\PSPACE}{{\sf PSPACE}}$ $\newcommand{\EXPTIME}{{\sf EXPTIME}}$
Diagonalization. Any proof exploiting diagonalization proof techniques to prove properties of TMs is a proof with oracles. A well-known application of this proof techniques is to show that the Halting problem is undecidable. That is, generally, no TM can determine whether a TM will halt on a string. The key factors leading to this result are precisely the two facts stated earlier: any TM can be represented as a string, and a TM can simulate another TM based on its string representation. To see that the Halting problem is undecidable, suppose to the contrary that we can decide whether $M$ halts on $x$ for any $M$ and $x$. (It is a convention to regard $M(x)$ as diverging if $M$ is not a valid TM.) Define a TM $N$ such that $N(M)$ halts if $M(M)$ diverges, and $N(M)$ loops if $M(M)$ halts. After some speculation, one can see that it is impossible to determine whether $N(N)$ halts, contradicting to our assumption.

Fixed-Point Theorem. Two TMs $A$ and $B$ are called semantically equivalent, denoted by $A\simeq B$, iff $A(x)=B(x)$ for any string $x$ (set $M(x):=\nearrow$ if a TM $M$ diverges on $x$). We claim that if $f$ is a TM mapping TMs to TMs, then $f$ has a fixed point, i.e., there exists a TM $M$ such that $f(M)\simeq M$. The key to prove this claim is to consider a special TM $G(M):=M(M)$. More precisely, given string $M$, $G(M)$ is a TM that loops on any input when $M(M)$ is not a valid TM, and produces $M(M)(x)$ on input $x$ otherwise. Somehow we guess that a fixed point occurs at $G(N)$ for some TM $N$. Writing down the equation $f(G(N))\simeq G(N)\simeq N(N)$ with unknown $N$, one finds that $N:=f\circ G$ is a solution and thus $G(f\circ G)$ is a fixed point of $f$. By using integers as an encoding of TMs and taking the convention that $M(x):=\nearrow$ on all $x$ when $M$ is not a valid TM, we obtain Rogers' Fixed-Point Theorem: Any total computable function has a fixed point.

P vs NP. A canonical example used to show the power of proofs with oracles is to show that the $\P$ vs $\NP$ problem doesn't relativize. That is, there exist oracles $A$ and $B$ such that a) $\P^A=\NP^A$ and b) $\P^B\neq \NP^B$. First, note that any $C$ oracle such that $\NP \subseteq C$ and $C=\texttt{co}C$ can serve as $A$. For example, $C$ can be $\PSPACE$ or $\EXPTIME$. For such $C$, $C\subseteq \P^A\subseteq \NP^A$ clearly holds. Further, $\NP^A\subseteq C$ holds as any machine in $\NP$ can be simulated in $C$ and any query to $A$ can be answered in $C$. To prove (b), we will construct an oracle $B$ such that language $L_B:=\{1^n: B$ accepts a string of length $n\}$ locates in $\NP^B \setminus \P^B$. To force $L_B \not\in \P^B$, we consider all oracle machines in $\P$ by labelling them as $M_1, M_2,....$ We hope that by the construction of $B$, there exists an integer $n_i$ for each $M_i$ such that $M_i^B$ accepts $1^{n_i}$ iff $1^{n_i} \not\in L_B$. This will then imply $L_B \not\in \P^B.$ The fact that $L_B \in \NP^B$ is clear, as $\NP^B$ can guess a string of size $n$ in $B$ by making at most $n$ non-deterministic queries to $B$.
Let $B_0=\emptyset$ and $n_0=0$. For each $i\ge 1$, we shall construct $B_i$ as follows. Let $n_i>n_{i-1}$ be any number larger than the maximal length of strings in $B_{i-1}$. Now simulate $M_i^{B_{i-1}}$ on $1^{n_i}$ for at most $2^{n_i}/3$ computation steps. If $M_i^{B_{i-1}}$ accepts $1^{n_i}$, then we set $B_i:=B_{i-1},$ which implies $1^{n_i}\not\in L_{B_i}$. If $M_i^{B_{i-1}}$ rejects $1^{n_i}$, then there exists a string $s$ of length $n_i$ not queried by $M_i^{B_{i-1}}$. Define $B_i:=B_{i-1}\cup\{s\}$, which implies $1^{n_i} \in L_{B_i}$. Hence, by construction, $M_i^{B_{i-1}}$ cannot decide the membership of $1^{n_i}$ in $L_{B_i}$ within $2^{n_i}/3$ steps. Define $B:=\bigcup_i B_i$. Observe that $B_i\nearrow B$ and $L_{B_i}\nearrow L_B$. Also, for any string $x$, $M^B(x)=M^{B_{i}}(x)$ as long as $M^B(x)$ terminates in $2^{n_i}/3$ steps. Note that every TM $M$ has infinitely many TMs that i) are semantically equivalent to $M$, ii) are of size arbitrarily larger than $M$, and iii) has the same running time as that of $M$. Since $n_i\nearrow\infty$ as $i\rightarrow\infty$, for each oracle machine $M$ in $\P$, there exists $i$ such that $M_i^B\simeq M^B$ and the running time of $M_i^B$ on $1^{n_i}$ is less than $2^{n_i}/3$. It follows that $M^B$ accepts $1^{n_i}$ iff $1^{n_i}$ is not in $L_B$, i.e., $M^B$ doesn't decide $L_B$. Hence, $L_B$ is a language in $\NP^B$ but not in $\P^B$.

A note on LTL vs CTL

• Syntax. A quantifier in a CTL formula are in form of a path quantifier $A,E$ following by a state quantifier $F,X,G,U,W$. A quantifier in an LTL is a combination of state quantifiers.
• States and paths. A CTL formula $\phi$ is a state formula, meaning that the temporal operators are state-based in structure: the derivation of a given formula is per-state and depends on the derivation of subformulas for subsequent states. For example, computing the set of states satisfying $AG\,φ$ relies on computing the set of states satisfying $φ$.
  In contrast, LTL formula $\psi$ is a path formula: the derivation of a given formula depends on the derivation of subformulas for suffixes of a path.
• Entailments. We write $M,s \models \phi$ and $M,p \models \psi$ for state $s$ and path $p$. Given a set $I$ of initial states of $M$, we write $M ⊨ φ$ if $M, s ⊨ φ$ for all $s ∈ I$, and write $M ⊨ ψ$ if $M, p ⊨ ψ$ for any path $p$ starting from $I$.
• LTL and CTL are incomparable. The reset property $AG (EF\,φ)$ (i.e. there is always a possibility that $\phi$ could hold, though it may never hold) cannot be expressed in LTL. The stability property $FG\,φ$ cannot be expressed in CTL. Consider a system $M: (s_0,s_0),(s_0,s_1),(s_1,s_2),(s_2,s_2)$ such that $s_0$ is the initial state, $s_0,s_2 \models φ$, and $s_1 \models \neg φ$. Then $M \not\models AFAG\,φ$ but $M \models FG\,φ$.
  It is known that an LTL formula can be over-approximated with ∀CTL [6]: if an ∀CTL property (consisting of AG and AF sub-properties) holds, then an analogous LTL property (where we replace AG with G and AF with F) also holds.
• Structure vs traces. CTL can characterize the structure while LTL only characterizes the traces. Consider the following two systems:
  $A:$ $(s_1,s_2),\ (s_1,s_3),\ (s_2,s_4),\ (s_3,s_5),\ (s_4,s_1),\ (s_5,s_1)$
  $B:$ $(s_1,s_2),\ (s_2,s_4),\ (s_2,s_5),\ (s_4,s_1),\ (s_5,s_1)$
  where $L(s_1)=a,\ L(s_2)=L(s_3)=b,\ L(s_4)=c,\ L(s_5)=d$. Both systems have traces $(ab(c+d))^\omega$ and thus cannot be distinguished in LTL. On the other hand, $B$ is a model of $AG(b\Rightarrow EX\ c)$ while $A$ isn't.
• There are lots of discussions over the best logic to express properties for software verification (cf. [2,5]). LTL can express important properties for software system modelling such as fairness, while the CTL must have a new semantics to express them, for example CTL* [4] or CTL+Fair [3]. But CTL algorithms are usually more efficient and can use BDD-based algorithms. Hence reachers have tried to approximate LTL verification using CTL model checking techniques, e.g., [7].

References

1. Making prophecies with decision predicates, POPL 2011.
2. Branching vs. Linear Time: Final Showdown, TACAS 2001.
3. Fairness for Infinite-State Systems, TACAS 2015.
4. Verifying Increasingly Expressive Temporal Logics for Infinite-State Systems, JACM 2017.
5. Concurrency: the Works of Leslie Lamport, ACM Press 2019.
6. The common fragment of CTL and LTL, FOCS, 2000.
7. Temporal verification of programs, PhD Thesis, 2012.

Enumeration in C#

Enumerating a collection

In C#, a collection class needs to implement IEnumerable to be used in foreach. This interface provides a function GetEnumerator that returns an IEnumerator instance (called an enumerator, which may or may not be the collection itself) supporting operations such as Reset, Current, and MoveNext. An enumerator serves as a proxy to sequentially access the elements in a collection. However, the behavior of a enumerator can be problematic if the underlying collection is modified while the enumeration is in progress. There are several approaches to deal with this problem. One is to take a snapshot of the collection for enumeration. Another approach is to locate the elements on demand, so that the ith enumerated element is always the ith element, if any, in the current collection. To guarantee this, it may take linear time to visit each element and thus quadratic time to enumerate a collection using foreach. The third approach is to throw an exception when the enumerator detects that the contents of the collection changed during enumeration. The last approach is most frequently adopted in C#'s standard libraries for performance concerns. Even so, the first approach can be realized in the call site by creating a snapshot manually using ICollection.CopyTo.
In Java, Iterator.remove is the only safe way to modify a collection during iteration; the behavior of an iterator is unspecified if the underlying collection is modified in any other way. Besides, if you happen to have a ListIterator then you can use ListIterator.add to insert elements in addition to removing them during iteration.

Enumerators are not Enumerable

While it is enumerators that are used for enumeration, foreach has to work with an IEnumerable instance from which an enumerator is obtained. Namely, one can not directly use an enumerator in a foreach loop. In Java, this is not a problem because an anonymous interface instance can be easily created on the fly when it is needed. For example, one common scenario to instantiate an interface anonymously in Java is to create a task for a thread:

new Thread (new Runnable() { public void run() { ... } }).start();

In the snippet, an anonymous Runnable class is created, used and then discarded at runtime. Anonymous classes come in handy when Java programmers want to create classes to serve as workers, listeners, adapters, etc. By contrast, C# programmers are expected to use anonymous functions (delegates or lambdas) for these purposes. While C# does supports anonymous classes, anonymous classes in C# look more like structs than classes, as they can only have public read-only properties and they are not allowed to extend classes (other than object) or implement interfaces.
Although one cannot use an enumerator with foreach, it is almost as easy to use it in a while loop:

while (enum.MoveNext()) { Process(enum.Current); }

However, in situations where an enumerable instance is explicitly required (e.g., by the constructor of a collection), it will take some tricks to convert an enumerator to an enumerable instance at runtime.

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.