Ohad's Research - SPLV2022

An introduction to statistical modelling semantics with higher-order measure theory

SPLV: The 4th Scottish Programming Languages and Verification Summer School

Ohad Kammar 11-16 July 2022

The last few years have seen several breakthroughs in the semantic foundations of statistical modelling. In this course, I will introduce one of these approaches — quasi-Borel spaces. We will review and develop a semantic tool-kit for measure theory using higher-order functions. The course will be accompanied by exercises and tutorials, allowing you to develop a working knowledge and hands-on experience.

Course materials

Slides

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

Previous instances

You can see a previous iteration of this course, given as part of the Logic of Probabilistic Programming conference in 2022: