The slides are here, and the videos are on eCampus.

In computation theory, many things are finite. Automata, logical circuits and formulas, and even Turing machines (apart from their infinite tape) are finite objects. Importantly, the alphabets that various classical computation models operate upon, are usually finite.

Sometimes all this finiteness is an unwelcome restriction. In particular, we sometimes want to consider infinite alphabets to compute upon. This is useful for modelling systems that operate on data items that come from potentially infinite domains, such as names, passwords, nonces, timestamps, or indeed any data that we want to treat in an “atomic” way, disregarding any low-level representation as sequences of bits.

Computation theory over infinite alphabets is a rich and complex subject. I will present a rather radical approach to it, where infinite domains of data atoms are built into the very fabric of mathematics, all the way down to set-theoretic foundations. The advantage of this is one can develop a theory of computation with data atoms in a familiar way, using the same definitions as in the classical setting; only the definitions are interpreted over different mathematical foundations. The disadvatage is that the mathematics of sets with atoms differs from the classical theory in tricky ways: for example, the powerset of a finite set need not be finite there, so one has to be careful not to use that principle in proofs.

The presentation will be loosely based on two books (both of which contain significantly more material than what I will be able to cover):

1. Mikołaj Bojanczyk.  Slightly Infinite Sets. Draft available from the author’s Web page.
2. Andy Pitts.  Nominal Sets: Names and Symmetry in Computer Science.  Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, May 2013.  ISBN 9781107017788.