PoP Seminar Talk

Type-driven foundations for statistical modelling

Ohad Kammar, Senior Research Fellow, University of Edinburgh
Tuesday, 19 March, 2024; 3:30pm
GHC 8102
Host: Jan Hoffmann

Abstract

The classical foundation for statistical modelling takes as primitive the notion of an observable event, axiomatising their properties by measurable spaces and functions. While measurable spaces support concrete type structure well, one faces inherent no-go results when dealing with more abstract spaces like: spaces of measurable functions for modelling continuous-time processes; spaces of measurable functionals for measurable statistics; and measurably-dependent function spaces for conditional probabilities. In joint work with Heunen, Staton, and Yang, we proposed quasi-Borel spaces. Here the axiomatisation takes as primitive the notion of a random element, also known as random variables in concrete cases. These spaces support notions for both concrete and abstract spaces. Having arrived at this collection of spaces in a fairly abstract manner, as a full sub-category of concrete sheaves, I was pleasantly surprised to find that some of their abstract type structure does support operations at the heart of statistics, measure theory, and classical descriptive set theory.

In this talk, I will survey this line of work. I will cover the basic definitions and ideas underlying quasi-Borel spaces, as well as some abstract ones. I will then review how myself and others have used these spaces as a semantic foundation for expressive probabilistic modelling languages and their Monte Carlo Bayesian inference implementations. I will conclude with more recent work developing and applying the dependently typed structure of these spaces.

Copyright (c) Robert Harper. All Rights Reserved.

Bio

Ohad Kammar is a Senior Research Fellow in the Laboratory for the Foundations of Computer Science at the University of Edinburgh School of Informatics. He is interested in programming language theory and design, algebra, logic, and category theory.

Copyright (c) Robert Harper. All Rights Reserved.