Abstract

The theory of network computing (a.k.a. distributed graph algorithms) originally emerged as a study of the principles that govern problem-solving and coordination in large computer networks, such as the Internet. However, work done in this research area is rapidly gaining relevance also in other fields: there are direct connections between distributed graph algorithms and two fields of mathematics, namely descriptive combinatorics and stochastic processes, and results and techniques developed in distributed graph algorithms are used these days to also understand the limitations of quantum computation.

In spite of the increasingly important role of the theory of network computing, its foundations are far from solid. There is no universally-agreed-on definition of the model of distributed computing; there are numerous minor (and not so minor) variations of the theme. This makes it hard and error-prone to compose results from different sources, as different authors tend to use slightly different definitions. At the same time, one of the most celebrated recent results in the field is the classification of the distributed computational complexity of local problems, and this is a corollary of dozens of results proved by a large number of research teams over many years. Can we trust all this work? And for exactly which model variants does the classification hold? How can researchers from other fields build on this not-so-stable and not-so-accessible foundation?

In this project, we will streamline the landscape of models. We will show how a diverse spectrum of models can be sandwiched between a single pair of models, and hence a single result can be very broadly applicable.

We will promote the idea of pairs of lower-bound and upper-bound models, so that theorems are claims about a range of models, instead of being claims about one very specific model. This way it will be much easier to put together multiple theorems from different sources in a black-box manner, as we no longer need a perfect match between the models – it suffices that there is some overlap in their range of applicability. We will not only prove new results using this formalism, but we will also reformulate key prior results this way.

We will formalize the key definitions using the Lean proof assistant, and we will also formalize the statements of the key theorems. We will lay a new solid foundation for the future generations of researchers in this field.

Funding

This project is funded by the Research Council of Finland, Grant 363558.