A type theory for probabilistic and Bayesian reasoning

DOI10.4230/LIPICS.TYPES.2015.1zbMATH Open1433.68264arXiv1511.09230OpenAlexW2963712756MaRDI QIDQ4580222FDOQ4580222

Authors: Robin Adams, Bart Jacobs 

Publication date: 13 August 2018

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.

Full work available at URL: https://arxiv.org/abs/1511.09230

Recommendations

• Probabilistic reasoning about simply typed lambda terms
• A predicate/state transformer semantics for Bayesian learning
• A Type Theory for Probabilistic $$\lambda $$–calculus
• Probabilistic reasoning in a classical logic
• Linking theories in probabilistic programming

zbMATH Keywords

type theoryprobabilistic programmingprobabilistic algorithmBayesian reasoningeffect module

Mathematics Subject Classification ID

Bayesian inference (62F15) Learning and adaptive systems in artificial intelligence (68T05) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Semantic domains for combining probability and non-determinism
• Measurable Spaces and Their Effect Logic
• A probabilistic PDL
• Semantics of probabilistic programs
• New Directions in Categorical Logic, for Classical, Probabilistic and Quantum Logic
• States of Convex Sets
• A Bayesian approach to compatibility, improvement, and pooling of quantum states
• Title not available (Why is that?)
• A predicate/state transformer semantics for Bayesian learning
• From probability monads to commutative effectuses
• Semantics for probabilistic programming
• Total and Partial Computation in Categorical Quantum Foundations
• An effect-theoretic account of Lebesgue integration
• Title not available (Why is that?)
• Weakest Precondition Reasoning for Expected Run–Times of Probabilistic Programs
• Reasoning about Recursive Probabilistic Programs
• Title not available (Why is that?)
• Measure transformer semantics for Bayesian machine learning

Cited In (6)

• A Type Theory for Probabilistic $$\lambda $$–calculus
• Universal Properties in Quantum Theory
• On redundant types and Bayesian formulation of incomplete information
• Title not available (Why is that?)
• Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic
• Towards probabilistic reasoning in type theory -- the intersection type case

Uses Software

• QPEL

This page was built for publication: A type theory for probabilistic and Bayesian reasoning

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4580222)