×

A type theory for probabilistic and Bayesian reasoning. (English) Zbl 1433.68264

Uustalu, Tarmo (ed.), 21st international conference on types for proofs and programs, TYPES 2015, May 18–21, 2015, Tallinn, Estonia. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 69, Article 1, 34 p. (2018).
Summary: 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.
For the entire collection see [Zbl 1392.68035].

MSC:

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

Software:

QPEL
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] R. Adams. QPEL: Quantum program and effect language. In B. Coecke, I. Hasuo, and P. Panangaden, editors, {\it Proc. of 11th Int. Workshop on Quantum Physics and Logic, QPL} {\it 2014}, volume 172 of {\it Electron. Proc. Theor. Comput. Sci.}, pages 133-153. Open Publishing Assoc., 2014. doi:10.4204/eptcs.172.10. · Zbl 1464.68068
[2] :32
[3] :31 {\it Science, LICS ’16, New York, NY, USA, July 5-8, 2016}, pages 525-534. ACM, 2016. doi:10.1145/2933575.2935313.
[4] :33 Γ ‘ {\it r }: {\it A }+ {\it B}∆{\it , z }: {\it A }‘ {\it s }: {\it C }⊗ {\it D} ∆{\it , w }: {\it B }‘ {\it s}0: {\it C }⊗ {\it D}Θ{\it , x }: {\it C, y }: {\it D }‘ {\it t }: {\it E} (let-case) Γ{\it , }∆{\it , }Θ ‘ let {\it x}⊗{\it y }= case {\it r }of inl ({\it z}) 7→ {\it s }| inr ({\it w}) 7→ {\it s}0 in {\it t }= case {\it r }of inl ({\it z}) 7→ let {\it x}⊗{\it y }= {\it s }in {\it t }| inr ({\it w}) 7→ let {\it x}⊗{\it y }= {\it s}0 in {\it t }: {\it E}
[5] :30
[6] :34
[7] ({\it β}inlr 1) Γ ‘B 1(«{\it s, t}») = {\it s }: {\it A }+ 1 Γ ‘ {\it s }: {\it A }+ 1Γ ‘ {\it t }: {\it B }+ 1Γ ‘ {\it s }↓= {\it t }↑:
[8] Γ ‘ {\it t }:
[9] {\it x }: {\it A }‘ {\it q }:
[10] ‘ {\it ρ }: {\it A}‘ {\it t }= do_← {\it t}; return {\it ρ }: {\it A }+ 1 ({\it η}nrm) Γ ‘ {\it ρ }= nrm ({\it t}) : {\it A}
[11] ({\it β}nrm) Γ ‘ {\it t }= do_← {\it t}; return nrm ({\it t}) : {\it A }+ 1 ‘ {\it t }: {\it A }+ 1‘ 1{\it /n }≤ {\it t }↓:
[12] (nrm) Γ ‘ nrm ({\it t}) : {\it A} ‘ {\it t }: {\it A }+ 1‘ 1{\it /n }≤ {\it t }↓:
[13] These ensure that 1{\it /n }is the unique scalar whose sum with itself {\it n }times is >. The term {\it b}{\it mn}ensures that the term ({\it m }+ 1) · 1{\it /n }is well-typed.
[14] (B 2− {\it b}{\it mn})(1 ≤ {\it m < n}) Γ ‘ do {\it x }← {\it b}{\it mn}; return ∇({\it x}) = {\it m }· 1{\it /n }:
[15] Γ ‘ {\it b}{\it mn}:
[16] (divide)({\it b}{\it mn})(1 ≤ {\it m < n}) Γ ‘ {\it t }= 1{\it /n }:
[17] Γ ‘ {\it n }· {\it t }= > :
[18] Γ ‘ {\it n }· 1{\it /n }= > :
[19] Γ ‘ {\it t }: {\it A} ({\it β}left)({\it η}left) Γ ‘ inl (left ({\it t})) = {\it t }: {\it A }+ {\it B}Γ ‘ left (inl ({\it t})) = {\it t }: {\it A}
[20] (left-eq) Γ ‘ left ({\it t}) = left ({\it t}0) : {\it A} Γ ‘ {\it t }: {\it A }+ {\it B}Γ ‘ inl? ({\it t}) = > :
[21] (left) Γ ‘ left ({\it t}) : {\it A} Γ ‘ {\it t }= {\it t}0: {\it A }+ {\it B}Γ ‘ inl? ({\it t}) = > :
[22] ({\it β}inlr 2) Γ ‘B 2(«{\it s, t}») = {\it t }: {\it B }+ 1 Γ ‘ {\it t }: {\it A }+ {\it B} ({\it η}inlr) Γ ‘ {\it t }= «B 1({\it t}){\it ,}B 2({\it t})» : {\it A }+ {\it B}
[23] (inlr) Γ ‘ «{\it s, t}» : {\it A }+ {\it B} Γ ‘ {\it s }= {\it s}0: {\it A }+ 1Γ ‘ {\it t }= {\it t}0: {\it B }+ 1Γ ‘ {\it s }↓= {\it t }↑:
[24] N. Benton, G. Bierman, V. de Paiva, and M. Hyland. A term calculus for intuitionistic linear logic. In M. Bezem and J. F. Groote, editors, {\it Proc. of Int. Conf. on Typed Lambda} {\it Calculi and Applications, TLCA ’93}, volume 664 of {\it Lect. Notes in Comput. Sci.}, pages 75-90. Springer, 1993. doi:10.1007/bfb0037099. · Zbl 0795.68127
[25] (inlr-eq) Γ ‘ «{\it s, t}» = «{\it s}0{\it , t}0» : {\it A }+ {\it B} Γ ‘ {\it s }: {\it A }+ 1Γ ‘ {\it t }: {\it B }+ 1Γ ‘ {\it s }↓= {\it t }↑:
[26] (B 1− {\it b}{\it mn})(1 ≤ {\it m < n}) Γ ‘ do {\it x }← {\it b}{\it mn};B 1({\it x}) = 1{\it /n }:
[27] Johannes Borgström, Andrew D. Gordon, Michael Greenberg, James Margetson, and Jur gen Van Gael. Measure transformer semantics for Bayesian machine learning. In Gilles Barthe, editor, {\it Programming Languages and Systems - 20th European Symposium on Pro-} {\it gramming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and} {\it Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Pro-} {\it ceedings}, volume 6602 of {\it Lecture Notes in Computer Science}, pages 77-96. Springer, 2011. doi:10.1007/978-3-642-19718-5_5. · Zbl 1326.68217
[28] K. Cho. Total and partial computation in categorical quantum foundations. In C. Heunen, P. Selinger, and J. Vicary, editors, {\it Proc. of 12th Int. Workshop on Quantum Physics and} {\it Logic, QPL 2015}, volume 195 of {\it Electron. Proc. in Theor. Comput. Sci.}, pages 116-135. Open Publishing Assoc., 2015. doi:10.4204/eptcs.195.9. · Zbl 1477.81028
[29] K. Cho, B. Jacobs, A. Westerbaan, and B. Westerbaan. An introduction to effectus theory, 2015. arXiv preprint 1512.05813. URL: https://arxiv.org/abs/1512.05813. · Zbl 1352.81011
[30] K. Cho, B. Jacobs, A. Westerbaan, and B. Westerbaan. Quotient comprehension chains. In C. Heunen, P. Selinger, and J. Vicary, editors, {\it Proc. of 12th Int. Workshop on Quantum} {\it Physics and Logic, QPL 2015}, volume 195 of {\it Electron. Proc. in Theor. Comput. Sci.}, pages 136-147. Open Publishing Assoc., 2015. doi:10.4204/eptcs.195.10. · Zbl 1477.03256
[31] Andrew D. Gordon, Thomas A. Henzinger, Aditya V. Nori, and Sriram K. Rajamani. Prob abilistic programming. In James D. Herbsleb and Matthew B. Dwyer, editors, {\it Proceedings} {\it of the on Future of Software Engineering, FOSE 2014, Hyderabad, India, May 31 - June 7,} {\it 2014}, pages 167-181. ACM, 2014. doi:10.1145/2593882.2593900.
[32] B. Jacobs. Measurable spaces and their effect logic. In {\it Proc. of 28th Annual ACM/IEEE} {\it Symp. on Logic in Computer Science, LICS ’13}, pages 83-92. IEEE, 2013. doi:10.1109/ lics.2013.13. · Zbl 1433.03162
[33] B. Jacobs. New directions in categorical logic, for classical, probabilistic and quantum logic. {\it Log. Methods Comput. Sci.}, 11(3):article 24, 2015. doi:10.2168/lmcs-11(3:24)2015. · Zbl 1338.03117
[34] Bart Jacobs. From probability monads to commutative effectuses. {\it J. Log. Algebr. Meth.} {\it Program.}, 94:200-237, 2018. doi:10.1016/j.jlamp.2016.11.006. · Zbl 1382.68073
[35] Bart Jacobs, Bas Westerbaan, and Bram Westerbaan. States of convex sets. In Andrew M. Pitts, editor, {\it Foundations of Software Science and Computation Structures - 18th Inter-} {\it national Conference, FoSSaCS 2015, Held as Part of the European Joint Conferences on} {\it Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceed-} {\it ings}, volume 9034 of {\it Lecture Notes in Computer Science}, pages 87-101. Springer, 2015. doi:10.1007/978-3-662-46678-0_6. · Zbl 1459.68068
[36] Bart Jacobs and Fabio Zanasi. A predicate/state transformer semantics for bayesian learn ing. {\it Electr. Notes Theor. Comput. Sci.}, 325:185-200, 2016. doi:10.1016/j.entcs.2016. 09.038. · Zbl 1401.68173
[37] C. Jones and G. D. Plotkin. A probabilistic powerdomain of evaluations. In {\it Proc. of 4th} {\it Ann. IEEE Symp. on Logic in Computer Science, LICS ’89}, pages 186-195. IEEE, 1989. doi:10.1109/lics.1989.39173. · Zbl 0716.06003
[38] Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo. Weakest precondition reasoning for expected run-times of probabilistic programs. In Peter Thiemann, editor, {\it Programming Languages and Systems - 25th European Symposium on} {\it Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory} {\it and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016,} {\it Proceedings}, volume 9632 of {\it Lecture Notes in Computer Science}, pages 364-389. Springer, 2016. doi:10.1007/978-3-662-49498-1_15. · Zbl 1335.68058
[39] Dexter Kozen. Semantics of probabilistic programs. {\it J. Comput. Syst. Sci.}, 22(3):328-350, 1981. doi:10.1016/0022-0000(81)90036-2. · Zbl 0476.68019
[40] Dexter Kozen. A probabilistic PDL. {\it J. Comput. Syst. Sci.}, 30(2):162-178, 1985. doi: 10.1016/0022-0000(85)90012-1. · Zbl 0575.03013
[41] M. S. Leifer and R. W. Spekkens. Towards a formulation of quantum theory as a causally neutral theory of Bayesian inference. {\it Phys. Rev. A}, 88(5):article 052130, 2013. doi:10. 1103/physreva.88.052130. · Zbl 1302.60017
[42] Carroll Morgan, Annabelle McIver, and Karen Seidel. Probabilistic predicate transformers. {\it ACM Trans. Program. Lang. Syst.}, 18(3):325-353, 1996. doi:10.1145/229542.229547. · Zbl 0885.68032
[43] Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. Reasoning about recursive probabilistic programs. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, {\it Proceedings of the 31st Annual ACM/IEEE Symposium on} {\it Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016}, pages 672-681. ACM, 2016. doi:10.1145/2933575.2935317. · Zbl 1401.68048
[44] S. Russell and P. Norvig. {\it Artificial Intelligence: A Modern Approach}. Prentice Hall, 2003. · Zbl 0835.68093
[45] Sam Staton, Hongseok Yang, Frank D. Wood, Chris Heunen, and Ohad Kammar. Se mantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints.In Martin Grohe, Eric Koskinen, and Natarajan Shankar, ed itors, {\it Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer} · Zbl 1395.68082
[46] Regina Tix, Klaus Keimel, and Gordon D. Plotkin.Semantic domains for combining probability and non-determinism.{\it Electr. Notes Theor. Comput. Sci.}, 222:3-99, 2009. doi:10.1016/j.entcs.2009.01.002. · Zbl 1271.68005
[47] E. S. Yudkowsky. An intuitive explanation of Bayesian reasoning. Essay, 2003. URL: http://yudkowsky.net/rational/bayes.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.