A type theory for probabilistic and Bayesian reasoning
From MaRDI portal
(Redirected from Publication:4580222)
Logic in computer science (03B70) Bayesian inference (62F15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Learning and adaptive systems in artificial intelligence (68T05)
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.
Recommendations
Cites work
- 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
- scientific article; zbMATH DE number 4179422 (Why is no real title available?)
- scientific article; zbMATH DE number 512773 (Why is no real title available?)
- scientific article; zbMATH DE number 1104373 (Why is no real title available?)
- scientific article; zbMATH DE number 783783 (Why is no real title available?)
- scientific article; zbMATH DE number 7364199 (Why is no real title available?)
- 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
(10)- Probabilistic reasoning about simply typed lambda terms
- A predicate/state transformer semantics for Bayesian learning
- Towards probabilistic reasoning in type theory -- the intersection type case
- A type theory for probability density functions
- A Type Theory for Probabilistic \lambda –calculus
- scientific article; zbMATH DE number 7444845 (Why is no real title available?)
- Universal Properties in Quantum Theory
- Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic
- Checking trustworthiness of probabilistic computations in a typed natural deduction system
- On redundant types and Bayesian formulation of incomplete information
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)
