Foundations for type-driven probabilistic modelling
LSS@ANU: Logic Summer School at Australian National University
Ohad Kammar 4 December – 15 December 2023
The last few years have seen several breakthroughs in the semantic foundations of probabilistic and statistical modelling. In this course, 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, allowing you to develop a working knowledge and hands-on experience during the summer school and after it.
Course materials
The 2023 edition is still under development. In the meanwhile, you can look at previous editions of this course:
Previous edition: Scottish PL and Verification Summer School
Slides
-
All slides
(updated with corrections)
Lectures
1-2 (video unavailable unfortunately)
Lectures
3-4 (video)
See the Marseille course for additional content and videos.
Exercise sheet (under development)
-
Context and background
Doing all of these exercises is too much for the course, the goal is to learn something new, or — if you already know this material — help someone else learn something new.
-
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.
Qbs
construction: space combinators — you may want to spread these
exercises over several sittings.
Borel
subspaces: measurable subsets in a quasi-Borel space.
-
Function
spaces: practice the definition of the function space of two qbses,
with the Borel subsets and random element spaces.
Type
structure: use type-formers to put spaces together and form more
complex spaces.
Standard Borel spaces (under development): use measurability-by-type to
construct standard Borel spaces.
-
Measures: introductory exercises if you’ve never worked with measures
before.
Lebesgue integration: the definition of the Lebesgue integral.
Randomisable measures: the class of measures we will work with.
-
Random variable spaces: definition and basic properties of the Lebesgue
spaces.
Geometry of random variable spaces: basic geometric and topological
properties of Lebesgue spaces.
Conditional expectation: existence and almost-certain uniqueness of
Kolmogorov’s conditional expectation.
-
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.