eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-15
1:1
1:34
10.4230/LIPIcs.TYPES.2015.1
article
A Type Theory for Probabilistic and Bayesian Reasoning
Adams, Robin
Jacobs, Bart
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol069-types2015/LIPIcs.TYPES.2015.1/LIPIcs.TYPES.2015.1.pdf
Probabilistic programming
probabilistic algorithm
type theory
effect module
Bayesian reasoning