The locale of random sequences

Alex Simpson ( School of Informatics, University of Edinburgh )

If one tosses a fair coin ad infinitum one generates a "random sequence" in {0,1}^\omega. Empirically, such sequences exhibit two contrasting properties: a local irregularity - knowing an initial segment of the sequence does not yield any information about the remainder of the sequence; and a global regularity - there is an asymptotic satisfaction of probabilistic laws such as the law of large numbers.

The naive approach to formalising the notion of random sequence is to define a sequence to be random if it satisfies all probabilistic laws. This does not work because there are no such sequences. Existing mathematical theories of randomness circumvent this problem by restricting to subclasses of probabilistic laws. Typically, such subclasses are defined by invoking computability considerations, or by using notions of logical definability. Such definitions have led to the rich and successful mathematical theory of algorithmically random sequences.

The purpose of this talk is to rescue the naive approach to randomness. I will show that there is a meaningful sense in which the sequences that satisfy all probabilistic laws form a natural and non-trivial "space". The tool needed to make sense of this idea is locale theory. The aim of the talk is to present sufficient background on randomness and locale theory to lead up to the eventual very natural definition of the "locale of random sequences". Finally, I'll discuss some interesting properties of this "space".