Alex Simpson: Relating point-free and algorithmic randomness

In this seminar, I will present research carried out with Antonin Delpeuch (ENS Paris and Université Paris Diderot) during his May-August MSc intership at FMF this year.

Title: Relating point-free and algorithmic randomness

Abstract: We relate two contrasting approaches to randomness. Algorithmic randomness classifies infinite sequences as random if they pass a collection of randomness tests specified in computability-theoretic terms. An alternative point-free approach considers instead a generalised space (a locale) of random sequences, which is non-trivial even though, in this approach, individual random sequences do not exist (the locale has no points). To connect the two, we give a constructive presentation of the point-free approach, and interpret it in Hyland's effective topos Eff. In Eff, generalised spaces of random sequences characterise, via their classical points, notions of algorithmically random sequence.