Triviality of asynchronous consensus allowing one faulty process

The classic “FLP” paper^[1] says that it is impossible to have a computable non-trivial asynchronous consensus protocol that allows one process to fail silently. Computable means its reaches consensus in finite time, non-trivial means the protocol doesn’t reduce to just using a pre-determined constant outcome, and a process fails by not receiving some messages addressed to it.

Having seen the slides for a presentation and a summary of work by Martín Escardó^[2], it seemed that there was a way to understand the FLP result from a topological point of view.

The paper can be simplified to a statement about continuous functions from the space of valid message sequences (modulo re-serialization) to the set $\{0,1\}$. Leveraging semi-reliability, one can show that any such function must be constant (in other words: the domain is a connected space). I thought it would be an interesting exercise to try to strip the FLP paper down to its core while making the proofs more constructive. Hence, Triviality of asynchronous consensus allowing one faulty process (pdf).

Some changes to the model:

• Instead of keeping track of internal states, processes are given the set of all messages they have received so far. We also don’t assume anything about the computability of the processes.
• Instead of output registers, we have an omniscient arbiter function that observes the sequence messages received by all the processes, and it is responsible for deciding the outcome of the protocol. Its only constraint is that it must make its decision after observing finitely many messages.
• Instead of input registers, we have an initial set of messages addressed to the processes. A consensus protocol is a map from an input register configuration to a set of initial messages.
• Messages can have an arbitrary amount of information, and there can even be uncountably many different messages.

One takeaway is that asynchronous consensus would be non-trivial if one could find some reasonable additional property that makes the domain a disconnected space.

Computability and topology

I am fairly confused about the details for how computable and continuous are equivalent. As far as topology goes for arbiters, giving the space of sequences of messages the product topology corresponds to only allowing the arbiter to observe finitely many messages. This section is me trying to figure things out better.

In computability theory, a language is a subset of finite strings over a fixed finite alphabet. A language $X$ is semidecidable if there is some algorithm that when given a string $s$ halts if and only if $s\in X$. Decidable languages are those where both the language and its complementary language are semidecidable. Finite unions and intersections of semidecidable languages are semidecidable, and so are the empty language and the language of all strings.

The set of semidecidable languages is sort of, but not quite, a topology. I’m not exactly sure how to deal with arbitrary unions, though with a suitably intuitionistic point of view, the only sets of open sets we can even speak of are those that can be constructed, and we can use the construction to produce an algorithm for the union by a dovetailing argument.

Unions are like introducing nondeterminism in the computational model. If $f:I\to 2^X$ is a computable function that with an index set $I$ picks out a collection of semidecidable subsets of $X$, then the union $\{x\in X:\exists i\in I,x\in f(i\left)\right\}$ is a semidecidable subset of $X$ that is computable, at least in the sense that membership is certifiable with an element of $I$.

To be a bit more precise: the Sierpiński space $S=\{0,1\}$ is a two-point space with $\varnothing ,\left\{1\right\},\{0,1\}$ comprising the list of open sets. Continuous functions $X\to S$ are in one-to-one correspondence with open subsets of $X$. If $I$ and $X$ are sets that are allowable in our computation model, and if $f:I\to S^X$ is a computable function, then the union of the images is a semidecidable set.

The space of natural numbers seems to have the discrete topology. Given $n\in N$, the set $\left\{n\right\}$ ought to be semidecidable because equality testing for naturals ought to be doable in finite time. A big problem, then, with arbitrary unions is that every subset of $N$ would be semidecidable, which is absurd because there are uncountably many subsets.

I think a solution to the arbitrary unions problem is to introduce a new concept: observable sets. These seem to be semidecidable sets along with unions coming from functions $I\to S^X$. An omniscient being can prove to you in finite time whether an element is in an observable set.

If $X$ is compact, then for a continuous $f:X\to S$, there is an algorithm implementing it. Take all the semidecidable sets contained entirely in $f^{-1}\left(1\right)$. The union of all these sets is $f^{-1}\left(1\right)$, since they form a basis, and by compactness we need only finitely many; with these we can construct an algorithm to implement $f$. A striking result is that compact sets correspond to whether there is a universal quantification functional ${\forall }_X:(X\to S)\to S$ that can be implemented by algorithm.

For the function space $2^N$, compactness implies the functions must be uniformly continuous (Heine-Cantor), where the interpretation is that each function has a fixed-length prefix that it will ever look at to compute its value. Roughly speaking, I think the FLP paper can be re-stated in a way something like the following. What I called an arbiter is like a function function $2^N\to 2$ (though with $M^N$ instead). The arbiter is unable to tell whether or not a process has failed, and with this we can contradict uniform continuity. I would be interested to see a more topological proof of FLP than the fairly direct translation I was able to produce!