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:

The changes generalize the original model and (in my opinion) make the proof easier to explain.

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 sX. 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:I2X is a computable function that with an index set I picks out a collection of semidecidable subsets of X, then the union {xX:iI,xf(i)} 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 ,{1},{0,1} comprising the list of open sets. Continuous functions XS 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:ISX 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 nN, the set {n} 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 ISX. 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:XS, there is an algorithm implementing it. Take all the semidecidable sets contained entirely in f1(1). The union of all these sets is f1(1), 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 X:(XS)S that can be implemented by algorithm.

For the function space 2N, 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 2N2 (though with MN 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!

[1] Michael J. Fischer, Nancy A. Lynch, and Michael S. Paterson. Impossibility of distributed consensus with one faulty process. volume 32 of JACM, pages 374–382, 1985.
[2] Martín Escardó’s 2004 thesis, Synthetic topology of data types and classical spaces.