A Type Theory for Probabilistic and Bayesian Reasoning

TL;DR

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.

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.

Figures (3)

• Figure 1: Typing rules for $\mathbf{COMET}$
• Figure 2: Rule for Ordering in $\mathbf{COMET}$
• Figure 3: Computation rules for $\mathbf{COMET}$

Theorems & Definitions (73)

• lemma 1
• proof
• lemma 2
• proof
• corollary 1
• proof
• lemma 3
• proof
• lemma 4
• proof