David Corfield




P(A|B)P(B)=P(B|A)P(A)P(A|B) \cdot P(B) = P(B|A) \cdot P(A) resembles the way of breaking up a type as a dependent sum.

Take non-dependent types. Then x:AB y:BA\sum_{x:A}B \simeq \sum_{y:B}A. So There is an equivalence between distributions on these which will map between z 1:D(A),z 2:[A,D(B)]z_1: D(A), z_2: [A, D(B)] and w 1:D(B),w 2:[B,D(A)]w_1: D(B), w_2: [B, D(A)].

w 1(b)= a:Az 1(a).z 2(a)(b);w 2(b)(a)=z 2(a)(b).z 1(a)/w 1(b). w_1(b) = \sum_{a:A}z_1(a).z_2(a)(b); w_2(b)(a) =z_2(a)(b).z_1(a)/w_1(b).

What happens when there is true dependence? Such as anaphora,

Prob(Jill comes tumbling after him|Jack falls down).

(Sam Staton points to disintegration

D( a:A(Ba)) a:A(D(Ba))D(\sum_{a : A} (B a)) \to \prod_{a : A} (D(B a))

Seems like the dependent linear De Morgan duality (Prop. 3.18, p. 43) of Urs’s paper

(Note his pointer to here.)

Perhaps that’s not surprising if we take D(X)D(X) as some subobject of [X, 0][X, \mathbb{R}^{\geq 0}].

People are certainly thinking of [0,1][0,1] playing a dualizing role

The role played by the two-element set {0,1}\{0,1\} in these classical results—e.g.as “schizophrenic” object—is played in our probabilistic analogues by the unit interval [0,1][0,1] (The Expectation Monad in Quantum Foundations, p. 2)

Take a simple case of tossing a coin until the first Head. If iterated dependent sum needs terms of the same length, we could construe things as though after reaching H, it returns H with probability 1.

Markov processes and dependency.


Probability theory meets type theory and/or category theory:

  • Topos Institute workshop

  • Bart Jacobs, Fabio Zanasi, and Octavio Zapata, Bayesian Factorisation as Adjoint, abstract Adjunction between Bayesian nets and distributions. How can one net be assigned?

  • Bart Jacobs, Structured Probabilistic Reasoning, pdf

  • Bart Jacobs, Categorical Aspects of Parameter Learning, slides

  • Kenta Cho, Bart Jacobs, Disintegration and Bayesian Inversion via String Diagrams, (arXiv:1709.00322)

  • Bart Jacobs, Sam Staton, De Finetti’s construction as a categorical limit, (arXiv:2003.01964)

  • Jonathan H. Warrell, A Probabilistic Dependent Type System based on Non-Deterministic Beta Reduction, (arXiv:1602.06420)

  • Jonathan Warrell, Mark Gerstein, Dependent Type Networks: A Probabilistic Logic via the Curry-Howard Correspondence in a System of Probabilistic Dependent Types (pdf)

  • Gianluca Giorgolo, Ash Asudeh, One Semiring to Rule Them All, (pdf)

  • Harry Crane, Logic of probability and conjecture, (pdf) (longer version in progress)

  • Bob Coecke, Eric Oliver Paquette, Dusko Pavlovic, Classical and quantum structuralism, (arXiv:0904.1997)

  • Bob Coecke, Robert W. Spekkens, Picturing classical and quantum Bayesian inference, (arXiv:1102.2368)

  • Robin Adams, Bart Jacobs, A Type Theory for Probabilistic and Bayesian Reasoning, (arXiv:1511.09230)

  • Bart Jacobs, Fabio Zanasi, The Logical Essentials of Bayesian Reasoning, (arXiv:1804.01193)

  • Bart Jacobs, Aleks Kissinger, Fabio Zanasi, Causal Inference by String Diagram Surgery, (arXiv:1811.08338)

  • Julian Hough, Matthew Purver, Probabilistic Type Theory for Incremental Dialogue Processing, (pdf)

  • Krasimir Angelov, Probability Distributions in Type Theory with Applications in Natural Language Syntax

  • Tobias Fritz, Paolo Perrone, Bimonoidal Structure of Probability Monads, (arXiv:1804.03527)

  • Tobias Fritz, Paolo Perrone, A Probability Monad as the Colimit of Finite Powers, (arXiv:1712.05363)

  • Paolo Perrone, Categorical Probability and Stochastic Dominance in Metric Spaces, (thesis)

  • Tobias Fritz? and Paolo Perrone, A Probability Monad as the Colimit of Spaces of Finite Samples, (arXiv:1712.05363).

  • Tobias Fritz, A synthetic approach to Markov kernels, conditional independence, and theorems on sufficient statistics, (arXiv:1908.07021)

  • Tobias Fritz, Paolo Perrone, Sharwin Rezagholi, Probability, valuations, hyperspace: Three monads on Top and the support as a morphism, (arXiv:1910.03752)

  • Alex Simpson, Synthetic probability theory, slides

  • Alex Simpson, Probability Sheaves and the Giry Monad, (pdf)

  • B. Jacobs. New directions in categorical logic, for classical, probabilistic and quantum logic. Logical Methods in Computer Science, 11(3):1–76, 2015

  • Kirk Sturtz, Categorical Probability Theory (arXiv:1406.6030) + others

  • Norman Ramsey, Avi Pfeffer, Stochastic Lambda Calculus and Monads of Probability Distributions, (pdf).

  • Chris Heunen, Ohad Kammar, Sam Staton, Hongseok Yang, A Convenient Category for Higher-Order Probability Theory, (arXiv:1701.02547)

  • Matthijs Vákár, Ohad Kammar, Sam Staton, A Domain Theory for Statistical Probabilistic Programming, (arXiv:1811.04196)

  • Adam Ścibior, Ohad Kammar, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K. Moss, Chris Heunen, Zoubin Ghahramani, Denotational validation of higher-order Bayesian inference, (arXiv:1711.03219)

  • A. Ścibior, Z. Ghahramani, and A. D. Gordon, Practical probabilistic programming with monads, In Proceedings of the 8th ACM SIGPLAN Symposium on Haskell, pages 165–176. ACM, 2015. (pdf)

  • A. Ścibior, A.D.Gordon, Parameterized probability monad, (pdf)

  • Flori C. (2013) Probabilities in Topos Quantum Theory. In: A First Course in Topos Quantum Theory. Lecture Notes in Physics, vol 868. Springer, Berlin, Heidelberg

  • Juan Pablo Vigneaux, Generalized information structures and their cohomology, (arXiv:1709.07807)

  • Florian Faissole and Bas Spitters, Synthetic topology in Homotopy Type Theory for probabilistic programming, (pdf)

  • Ugo Dal Lago, Naohiko Hoshino, The Geometry of Bayesian Programming, (arXiv:1904.07425)

  • Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Aleš Bizjak, Marco Gaboardi, Deepak Garg, Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus, (arXiv:1802.09787)

  • Pieter Collins, Computable Stochastic Processes, (arXiv:1409.4667)

  • Prakash Panangaden, A categorical view of conditional expectation, (slides)

  • Dario Stein, Sam Staton, Compositional Semantics for Probabilistic Programs with Exact Conditioning, (arXiv:2101.11351)

  • Bart Jacobs, A Channel-Based Perspective on Conjugate Priors, (arXiv:1707.00269)

  • Dan Shiebler, Categorical Stochastic Processes and Likelihood,(arXiv:2005.04735)

For big picture in probability theory see answers to

Discussion from a perspective of formal logic/type theory is in

  • Neil Toronto, Useful Languages for Probabilistic Modeling and Inference, PhD Thesis, 2014 (pdf, slides)

Homotopy probability theory

Expressivism about probability

Yalcin, S. (2011). Nonfactualism about epistemic modality. In Andy Egan & Brian Weatherson (Eds.),Epistemic modality. Oxford: Oxford University Press.

Yalcin, S. (2012). Bayesian expressivism.Proceedings of the Aristotelian Society,112, 123–160.123

Last revised on July 30, 2021 at 09:14:34. See the history of this page for a list of all contributions to it.