2026-07-29T10:45:17Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:8471 2024-03-06T10:39:27Z ddc:004 open_access

A Type Theory for Probabilistic and Bayesian Reasoning Adams, Robin Jacobs, Bart Probabilistic programming probabilistic algorithm type theory effect module Bayesian reasoning 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Robin Adams and Bart Jacobs 2018 Is Part Of LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2015.1 urn:nbn:de:0030-drops-84714 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.1 eng https://creativecommons.org/licenses/by/3.0/legalcode