Hostname: page-component-745bb68f8f-lrblm Total loading time: 0 Render date: 2025-01-13T00:56:30.098Z Has data issue: false hasContentIssue false
  • English
  • Français

A trustful monad for axiomatic reasoning with probability and nondeterminism

Published online by Cambridge University Press:  15 July 2021

REYNALD AFFELDT Open the ORCID record for REYNALD AFFELDT [Opens in a new window] ,
JACQUES GARRIGUE ,
DAVID NOWAK  and
TAKAFUMI SAIKAWA
REYNALD AFFELDT
Affiliation:
National Institute of Advanced Industrial Science and Technology, Digital Architecture Research Center, Tokyo, Japan (e-mail: [email protected])
JACQUES GARRIGUE
Affiliation:
Nagoya University, Graduate School of Mathematics, Nagoya, Japan (e-mail: [email protected])
DAVID NOWAK
Affiliation:
Univ. Lille, CNRS, Centrale Lille, UMR 9189 CRIStAL, F-59000 Lille, France
TAKAFUMI SAIKAWA
Affiliation:
Nagoya University, Graduate School of Mathematics, Nagoya, Japan (e-mail: [email protected])
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

The algebraic properties of the combination of probabilistic choice and nondeterministic choice have long been a research topic in program semantics. This paper explains a formalization in the Coq proof assistant of a monad equipped with both choices: the geometrically convex monad. This formalization has an immediate application: it provides a model for a monad that implements a nontrivial interface, which allows for proofs by equational reasoning using probabilistic and nondeterministic effects. We explain the technical choices we made to go from the literature to a complete Coq formalization, from which we identify reusable theories about mathematical structures such as convex spaces and concrete categories, and that we integrate in a framework for monadic equational reasoning.

Type
Research Article
Information
Journal of Functional Programming , Volume 31 , 2021 , e17
Check for updates
Copyright
© The Author(s), 2021. Published by Cambridge University Press

References

Abou-Saleh, F., Cheung, K.-H. & Gibbons, J. (2016) Reasoning about probability and nondeterminism. In POPL Workshop on Probabilistic Programming Semantics.Google Scholar
Affeldt, R., Hagiwara, M. & Sénizergues, J. (2014) Formalization of Shannon’s theorems. J. Automat. Reason. 53(1), 63–103.CrossRefGoogle Scholar
Affeldt, R., Cohen, C. & Rouhling, D. (2018) Formalization techniques for asymptotic reasoning in classical analysis. J. Formaliz. Reason. 11(1), 43–76.Google Scholar
Affeldt, R., Nowak, D. & Saikawa, T. (2019) A hierarchy of monadic effects for program verification using equational reasoning. In 13th International Conference on Mathematics of Program Construction (MPC 2019), Porto, Portugal, October 7–9, 2019, Hutton, G. (ed), Lecture Notes in Computer Science, vol. 11825. Springer, pp. 226–254.CrossRefGoogle Scholar
Affeldt, R., Garrigue, J. & Saikawa, T. (2020a) Formal adventures in convex and conical spaces. In 13th International Conference on Intelligent Computer Mathematics (CICM 2020), Bertinoro, Italy, July 26–31, 2020, Benzmüller, C. & Miller, B. R. (eds), Lecture Notes in Computer Science, vol. 12236. Springer, pp. 23–38.Google Scholar
Affeldt, R., Garrigue, J. & Saikawa, T. (2020b) Reasoning with conditional probabilities and joint distributions in Coq. Comput. Softw. 37(3), 79–95.Google Scholar
Beaulieu, G. (2008) Probabilistic Completion of Nondeterministic Models. PhD thesis, Faculty of Graduate and Postdoctoral Studies, University of Ottawa.Google Scholar
Beck, J. (1969) Distributive laws. In Seminar on Triples and Categorical Homology Theory, Eckmann, B. (ed), Lecture Notes in Mathematics, vol. 80. Springer, pp. 119–140.CrossRefGoogle Scholar
Bergman, G. (2015) An Invitation to General Algebra and Universal Constructions. Universitext. Springer International Publishing.CrossRefGoogle Scholar
Bonchi, F., Silva, A. & Sokolova, A. (2017) The power of convex algebras. In 28th International Conference on Concurrency Theory (CONCUR 2017), September 5–8, 2017, Berlin, Germany, Meyer, R. & Nestmann, U. (eds), LIPIcs, vol. 85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 23:1–23:18.Google Scholar
Bonchi, F., Sokolova, A. & Vignudelli, V. (2019) The theory of traces for systems with nondeterminism and probability. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2019), Vancouver, BC, Canada, June 24–27, 2019. IEEE, pp. 1–14.CrossRefGoogle Scholar
Bonchi, F., Sokolova, A. & Vignudelli, V. (2020a) Presenting convex sets of probability distributions by convex semilattices and unique bases. https://arxiv.org/abs/2005.01670. arXiv cs.LO.Google Scholar
Bonchi, F., Sokolova, A. & Vignudelli, V. (2020b) The Theory of Traces for Systems with Nondeterminism, Probability, and Termination. https://arxiv.org/abs/1808.00923v4. arXiv cs.LO.Google Scholar
Brady, E. (2013) Idris, a general-purpose dependently typed programming language: Design and implementation. J. Funct. Program. 23(5), 552–593.CrossRefGoogle Scholar
Cheung, K.-H. (2017) Distributive Interaction of Algebraic Effects. PhD thesis, Merton College, University of Oxford.Google Scholar
Cock, D. (2014) Leakage in Trustworthy Systems. PhD thesis, School of Computer Science and Engineering, The University of New South Wales, Sydney, Australia.Google Scholar
Cohen, C. & Sakaguchi, K. (2015) A Finset and Finmap Library: Finite Sets, Finite Maps, Multisets and Order. Available at: https://github.com/math-comp/finmap. Last stable release: 1.5.0 (2020).Google Scholar
Cohen, C., Sakaguchi, K. & Tassi, E. (2020) Hierarchy builder: Algebraic hierarchies made easy in Coq with Elpi (system description). In FSCD 2020. LIPIcs, vol. 167, pp. 34:1–34:21.Google Scholar
Fritz, T. (2015) Convex Spaces I: Definition and Examples. https://arxiv.org/abs/0903.5522. arXiv math.MG. First version: 2009.Google Scholar
Garillot, F., Gonthier, G., Mahboubi, A. & Rideau, L. (2009) Packaging mathematical structures. In 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2009), Munich, Germany, August 17–20, 2009, Berghofer, S., Nipkow, T., Urban, C. & Wenzel, M. (eds), Lecture Notes in Computer Science, vol. 5674. Springer, pp. 327–342.CrossRefGoogle Scholar
Gibbons, J. (2012) Unifying theories of programming with monads. In Revised Selected Papers of the 4th International Symposium on Unifying Theories of Programming (UTP 2012), Paris, France, August 27–28, 2012, Wolff, B., Gaudel, M. and Feliachi, A. (eds), Lecture Notes in Computer Science, vol. 7681. Springer, pp. 23–67.Google Scholar
Gibbons, J. & Hinze, R. (2011) Just do it: Simple monadic equational reasoning. In Proceeding of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19–21, 2011, Chakravarty, M. M. T., Hu, Z. & Danvy, O. (eds), pp. 2–14. ACM.CrossRefGoogle Scholar
Giry, M. (1982) A categorical approach to probability theory. In Categorical Aspects of Topology and Analysis, Banaschewski, B. (ed). Lecture Notes in Mathematics, vol. 915. Springer, pp. 68–85.CrossRefGoogle Scholar
Goy, A. & Petrisan, D. (2020) Combining probabilistic and non-deterministic choice via weak distributive laws. In 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2020), Saarbrücken, Germany, July 8–11, 2020. ACM, pp. 454–464.CrossRefGoogle Scholar
Gross, J., Chlipala, A. & Spivak, D. I. (2014) Experience implementing a performant category-theory library in Coq. In Interactive Theorem Proving, Klein, G. & Gamboa, R. (eds). Springer International Publishing, pp. 275–291.CrossRefGoogle Scholar
Infotheo. (2021) A Coq Formalization of Information Theory and Linear Error-Correcting Codes. https://github.com/affeldt-aist/infotheo. Open source software. Since 2009. Version 0.3.2. Software Heritage Archive: swh:1:dir:f8c270f648dd5bc6f822ef16e9354195ddb8f6ad.Google Scholar
Jacobs, B. (2010) Convexity, duality and effects. In IFIP TCS. IFIP Advances in Information and Communication Technology, vol. 323. Springer, pp. 1–19.CrossRefGoogle Scholar
Kaminski, B. L., Katoen, J., Matheja, C. & Olmedo, F. (2016) Weakest precondition reasoning for expected run-times of probabilistic programs. In 25th European Symposium on Programming Languages and Systems (ESOP 2016), Eindhoven, The Netherlands, April 2–8, 2016, Thiemann, P. (ed), Lecture Notes in Computer Science, vol. 9632. Springer, pp. 364–389.CrossRefGoogle Scholar
Keimel, K. & Plotkin, G. D. (2017) Mixed powerdomains for probability and nondeterminism. Logical Methods in Computer Science 13(1:2), 1–84.Google Scholar
Konig, H. (1986) Theory and applications of superconvex spaces. In Aspects of Positivity in Functional Analysis, Nagel, R., Schloterbeck, U. & Wolff, M. (eds), Mathematics Studies, vol. 122. North-Holland, pp. 79–118.CrossRefGoogle Scholar
Mac Lane, S. (1998) Categories for the Working Mathematician, 2nd edn. Graduate Texts in Mathematics, vol. 5. Berlin and New York: Springer-Verlag.Google Scholar
Mahboubi, A. & Tassi, E. (2013) Canonical structures for the working Coq user. In 4th International Conference on Interactive Theorem Proving (ITP 2013), Rennes, France, July 22–26, 2013, Blazy, S., Paulin-Mohring, C. & Pichardie, D. (eds), Lecture Notes in Computer Science, vol. 7998. Springer, pp. 19–34.CrossRefGoogle Scholar
Mathematical Components Team. (2007) Mathematical Components Library. https://github.com/math-comp/math-comp. Development version. Last stable version 1.12 (2020). Available on the same website.Google Scholar
McBride, C. (1999) Dependently Typed Functional Programs and their Proofs. PhD thesis, University of Edinburgh.Google Scholar
McIver, A. & Morgan, C. (2005) Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer.Google Scholar
Mio, M. & Vignudelli, V. (2020) Monads and Quantitative Equational Theories for Nondeterminism and Probability. https://arxiv.org/abs/2005.07509. arXiv cs.LO.Google Scholar
Mislove, M., Ouaknine, J. & Worrell, J. (2004) Axioms for probability and nondeterminism. Electronic Notes in Theoretical Computer Science 96, 7–28. Proceedings of the 10th International Workshop on Expressiveness in Concurrency.CrossRefGoogle Scholar
Mislove, M. W. (2000) Nondeterminism and probabilistic choice: Obeying the laws. In 11th International Conference on Concurrency Theory (CONCUR 2000), University Park, PA, USA, August 22–25, 2000, Palamidessi, C. (ed), Lecture Notes in Computer Science, vol. 1877. Springer, pp. 350–364.CrossRefGoogle Scholar
Monae. (2021) Monadic Effects and Equational Reasoning in Coq. https://github.com/affeldt-aist/monae. Open source software. Since 2018. Version 0.3.2. Software Heritage Archive: swh:1:dir:2d68878d365fe72744f8b085fa29df385567f6c9.Google Scholar
Mu, S.-C. (2019a) Calculating a Backtracking Algorithm: An Exercise in Monadic Program Derivation. Tech. rept. TR-IIS-19-003. Institute of Information Science, Academia Sinica.Google Scholar
Mu, S.-C. (2019b) Equational Reasoning for Non-deterministic Monad: A Case study of Spark Aggregation. Tech. rept. TR-IIS-19-002. Institute of Information Science, Academia Sinica.Google Scholar
Stone, M. H. (1949) Postulates for the barycentric calculus. Annali di Matematica Pura ed Applicata 29, 25–30.CrossRefGoogle Scholar
Tassarotti, J. & Harper, R. (2019) A separation logic for concurrent randomized programs. Proc. ACM Program. Lang. 3(POPL), 64:1–64:30.CrossRefGoogle Scholar
The Agda Team. (2020) The Agda User Manual. Available at: https://agda.readthedocs.io/en/v2.6.0.1. Version 2.6.0.1.Google Scholar
The Coq Development Team. (2019) The Logic of Coq. Available at: https://github.com/coq/coq/wiki/The-Logic-of-Coq. Part of the Coq FAQ.Google Scholar
The Coq Development Team. (2021) The Coq Proof Assistant Reference Manual. Inria. Available at: https://coq.inria.fr. Version 8.13.0.Google Scholar
Timany, A. & Jacobs, B. (2016) Category theory in Coq 8.5. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), June 22–26, 2016, Porto, Portugal, Kesner, D. and Pientka, B. (eds), LIPIcs, vol. 52, pp. 30:1–30:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik.Google Scholar
Tix, R., Keimel, K. & Plotkin, G. D. (2009) Semantic domains for combining probability and non-determinism. Electron. Notes Theor. Comput. Sci. 222, 3–99.CrossRefGoogle Scholar
Varacca, D. & Winskel, G. (2006) Distributing probability over nondeterminism. Mathematical Structures in Compuer Science 16(1), 87–113.CrossRefGoogle Scholar
Voevodsky, V., Ahrens, B., Grayson, D., et al. (2014) UniMath — A Computer-Checked Library of Univalent Mathematics. Available at: https://github.com/UniMath/UniMath. Last stable release 0.1 (2016).Google Scholar
Zwart, M. & Marsden, D. (2019) No-go theorems for distributive laws. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2019), Vancouver, BC, Canada, June 24–27, 2019. IEEE, pp. 1–13.CrossRefGoogle Scholar
Submit a response

Discussions

No Discussions have been published for this article.