A Type Theory for Probabilistic and Bayesian Reasoning

TL;DR

This paper presents a new type theory and logic designed for probabilistic reasoning, enabling formal computation of Bayesian inference with fuzzy predicates and a novel predicate-action correspondence.

Contribution

It introduces a probabilistic type theory with a unique predicate-action correspondence, facilitating formal Bayesian inference and reasoning.

Findings

Derived computation rules for Bayesian inference

Applied rules to graphical models for Bayesian reasoning

Potential foundation for mechanized Bayesian inference

Abstract

This paper introduces a novel type theory and logic for probabilistic reasoning. Its logic is quantitative, with fuzzy predicates. It includes normalisation and conditioning of states. This conditioning uses a key aspect that distinguishes our probabilistic type theory from quantum type theory, namely the bijective correspondence between predicates and side-effect free actions (called instrument, or assert, maps). The paper shows how suitable computation rules can be derived from this predicate-action correspondence, and uses these rules for calculating conditional probabilities in two well-known examples of Bayesian reasoning in (graphical) models. Our type theory may thus form the basis for a mechanisation of Bayesian inference.