Document Open Access Logo

A Type Theory for Probabilistic and Bayesian Reasoning

Authors Robin Adams, Bart Jacobs

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2015.1.pdf
  • Filesize: 0.69 MB
  • 34 pages

Document Identifiers

Author Details

Robin Adams
Bart Jacobs

Cite AsGet BibTex

Robin Adams and Bart Jacobs. A Type Theory for Probabilistic and Bayesian Reasoning. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 1:1-1:34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.TYPES.2015.1

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.
Keywords
  • Probabilistic programming
  • probabilistic algorithm
  • type theory
  • effect module
  • Bayesian reasoning

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. R. Adams. QPEL: Quantum program and effect language. In B. Coecke, I. Hasuo, and P. Panangaden, editors, Proc. of 11th Int. Workshop on Quantum Physics and Logic, QPL 2014, volume 172 of Electron. Proc. Theor. Comput. Sci., pages 133-153. Open Publishing Assoc., 2014. URL: http://dx.doi.org/10.4204/eptcs.172.10.
  2. 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, Proc. of Int. Conf. on Typed Lambda Calculi and Applications, TLCA '93, volume 664 of Lect. Notes in Comput. Sci., pages 75-90. Springer, 1993. URL: http://dx.doi.org/10.1007/bfb0037099.
  3. Johannes Borgström, Andrew D. Gordon, Michael Greenberg, James Margetson, and Jurgen Van Gael. Measure transformer semantics for Bayesian machine learning. In Gilles Barthe, editor, Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings, volume 6602 of Lecture Notes in Computer Science, pages 77-96. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-19718-5_5.
  4. K. Cho. Total and partial computation in categorical quantum foundations. In C. Heunen, P. Selinger, and J. Vicary, editors, Proc. of 12th Int. Workshop on Quantum Physics and Logic, QPL 2015, volume 195 of Electron. Proc. in Theor. Comput. Sci., pages 116-135. Open Publishing Assoc., 2015. URL: http://dx.doi.org/10.4204/eptcs.195.9.
  5. 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.
  6. K. Cho, B. Jacobs, A. Westerbaan, and B. Westerbaan. Quotient comprehension chains. In C. Heunen, P. Selinger, and J. Vicary, editors, Proc. of 12th Int. Workshop on Quantum Physics and Logic, QPL 2015, volume 195 of Electron. Proc. in Theor. Comput. Sci., pages 136-147. Open Publishing Assoc., 2015. URL: http://dx.doi.org/10.4204/eptcs.195.10.
  7. Andrew D. Gordon, Thomas A. Henzinger, Aditya V. Nori, and Sriram K. Rajamani. Probabilistic programming. In James D. Herbsleb and Matthew B. Dwyer, editors, Proceedings of the on Future of Software Engineering, FOSE 2014, Hyderabad, India, May 31 - June 7, 2014, pages 167-181. ACM, 2014. URL: http://dx.doi.org/10.1145/2593882.2593900.
  8. B. Jacobs. Measurable spaces and their effect logic. In Proc. of 28th Annual ACM/IEEE Symp. on Logic in Computer Science, LICS '13, pages 83-92. IEEE, 2013. URL: http://dx.doi.org/10.1109/lics.2013.13.
  9. B. Jacobs. New directions in categorical logic, for classical, probabilistic and quantum logic. Log. Methods Comput. Sci., 11(3):article 24, 2015. URL: http://dx.doi.org/10.2168/lmcs-11(3:24)2015.
  10. Bart Jacobs. From probability monads to commutative effectuses. J. Log. Algebr. Meth. Program., 94:200-237, 2018. URL: http://dx.doi.org/10.1016/j.jlamp.2016.11.006.
  11. Bart Jacobs, Bas Westerbaan, and Bram Westerbaan. States of convex sets. In Andrew M. Pitts, editor, Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, volume 9034 of Lecture Notes in Computer Science, pages 87-101. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-662-46678-0_6.
  12. Bart Jacobs and Fabio Zanasi. A predicate/state transformer semantics for bayesian learning. Electr. Notes Theor. Comput. Sci., 325:185-200, 2016. URL: http://dx.doi.org/10.1016/j.entcs.2016.09.038.
  13. C. Jones and G. D. Plotkin. A probabilistic powerdomain of evaluations. In Proc. of 4th Ann. IEEE Symp. on Logic in Computer Science, LICS '89, pages 186-195. IEEE, 1989. URL: http://dx.doi.org/10.1109/lics.1989.39173.
  14. 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, Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9632 of Lecture Notes in Computer Science, pages 364-389. Springer, 2016. URL: http://dx.doi.org/10.1007/978-3-662-49498-1_15.
  15. Dexter Kozen. Semantics of probabilistic programs. J. Comput. Syst. Sci., 22(3):328-350, 1981. URL: http://dx.doi.org/10.1016/0022-0000(81)90036-2.
  16. Dexter Kozen. A probabilistic PDL. J. Comput. Syst. Sci., 30(2):162-178, 1985. URL: http://dx.doi.org/10.1016/0022-0000(85)90012-1.
  17. M. S. Leifer and R. W. Spekkens. Towards a formulation of quantum theory as a causally neutral theory of Bayesian inference. Phys. Rev. A, 88(5):article 052130, 2013. URL: http://dx.doi.org/10.1103/physreva.88.052130.
  18. Carroll Morgan, Annabelle McIver, and Karen Seidel. Probabilistic predicate transformers. ACM Trans. Program. Lang. Syst., 18(3):325-353, 1996. URL: http://dx.doi.org/10.1145/229542.229547.
  19. 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, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 672-681. ACM, 2016. URL: http://dx.doi.org/10.1145/2933575.2935317.
  20. S. Russell and P. Norvig. Artificial Intelligence: A Modern Approach. Prentice Hall, 2003. Google Scholar
  21. Sam Staton, Hongseok Yang, Frank D. Wood, Chris Heunen, and Ohad Kammar. Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 525-534. ACM, 2016. URL: http://dx.doi.org/10.1145/2933575.2935313.
  22. Regina Tix, Klaus Keimel, and Gordon D. Plotkin. Semantic domains for combining probability and non-determinism. Electr. Notes Theor. Comput. Sci., 222:3-99, 2009. URL: http://dx.doi.org/10.1016/j.entcs.2009.01.002.
  23. E. S. Yudkowsky. An intuitive explanation of Bayesian reasoning. Essay, 2003. URL: http://yudkowsky.net/rational/bayes.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact