Foundations for type-driven probabilistic modelling
Laboratory for Software Science Tartu Supernumerary Course
Ohad Kammar January 15 2024
The last few years have seen several breakthroughs in the semantic foundations of probabilistic and statistical modelling. In this tutorial, we will use types to introduce, use, and organise abstractions for probabilistic modelling.
We will do so first for discrete probability, and then more generally with the recently-developed quasi-Borel spaces. The course is accompanied by exercises for self-study, allowing you to develop a working knowledge and hands-on experience after it.
Course materials
Lectures
All lectures.
Planned structure:
- Lecture 1
- Motivation
- Language of probability and distribution
- Discrete model
- Simply-typed probability
- Dependently-typed probability
- Lecture 2
- events, Borel sets, and measurable spaces
- quasi-Borel spaces
- Simple type structure
- Dependent-type structure
- Standard Borel spaces
- Integration
- Random variables
- Conditioning
-
Borel
set basics: introductory exercises if you’ve never worked with Borel
sets, or looking for a refresher.
Measurable
spaces and functions: exercises exploring the structure of
measurable spaces and measurable functions.
Basic
category theory: use these exercises to improve your category
theory.
Aumann’s
theorem: consequences of and related concepts to Aumann’s theorem on
the inexistence of measurable function-spaces.
Sequences:
examples of higher-order measure theory using sequences.
Quasi-Borel
spaces: first acquaintance with quasi-Borel spaces.
Extra-curricular material
-
More
on the Borel hierarchy: a guided tour of the proof of Aumann’s
theorem.
Aumann’s
theorem for Lebesgue measurablity: extending Aumann’s theorem from
Borel measurable functions to Lebesgue measurable functions.
Qbs
construction: space combinators — you may want to spread these
exercises over several sittings.
Borel
subspaces: measurable subsets in a quasi-Borel space.
Measurability by type
-
Function
spaces: practice the definition of the function space of two qbses,
with the Borel subsets and random element spaces.
Getting help and reporting mistakes
Please never hesitate to get in touch. Approach me directly in person during the summer school or by email. You may prefer to ask a question on the #qbs channel on the SPLS Zulip server: spls.zulipchat.com . Others would benefit from your question in that case too!