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

Lectures

All lectures so far.

1. Lecture 1 (Mon 11 Dec): type-driven probability and the discrete model (part 1)

2. Lecture 2 (Tue): type-driven probability and the discrete model (part 2)

3. Lecture 3 (Wed): Borel sets, measurable, standard Borel, and quasi-Borel spaces

   Relevant exercise sheets:

   • 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.

4. Lecture 4 (Thur): Simple- and dependent-type structure, and standard Borel spaces

   Relevant exercise sheets:

   • 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.

5. Lecture 5 (Fri): Integration and random variables

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!

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.
• An introduction to Quasi-Borel spaces
  • 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.
• Measurability by type
  • 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 and integration (under development)
  • 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.
• Kolmogorov’s conditional expectation (under development)
  • 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.
• 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.

Invited Tutorial at Logic of Probabilistic Programming 2022

• Videos: lecture 1, lecture 2
• Slides