A type theory for probabilistic and Bayesian reasoning

DOI10.4230/LIPICS.TYPES.2015.1zbMATH Open1433.68264OpenAlexW2963712756MaRDI 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?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• A Bayesian approach to compatibility, improvement, and pooling of quantum states
• A predicate/state transformer semantics for Bayesian learning
• A probabilistic PDL
• An effect-theoretic account of Lebesgue integration
• From probability monads to commutative effectuses
• Measurable spaces and their effect logic
• Measure transformer semantics for Bayesian machine learning
• New directions in categorical logic, for classical, probabilistic and quantum logic
• Quotient-comprehension chains
• Reasoning about Recursive Probabilistic Programs
• Semantic domains for combining probability and non-determinism
• Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints
• Semantics of probabilistic programs
• States of convex sets
• Total and partial computation in categorical quantum foundations
• Weakest precondition reasoning for expected run-times of probabilistic programs

Cited In (9)

• A type theory for probability density functions
• A Type Theory for Probabilistic $$\lambda $$–calculus
• Universal Properties in Quantum Theory
• On redundant types and Bayesian formulation of incomplete information
• A predicate/state transformer semantics for Bayesian learning
• Title not available (Why is that?)
• Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic
• Probabilistic reasoning about simply typed lambda terms
• 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)