Document Open Access Logo

A Categorical Approach to DIBI Models

Authors Tao Gu , Jialu Bao , Justin Hsu , Alexandra Silva, Fabio Zanasi

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2024.17.pdf
  • Filesize: 0.96 MB
  • 20 pages

Document Identifiers

Author Details

Tao Gu
  • University College London, UK
Jialu Bao
  • Cornell University, Ithaca, NY, USA
Justin Hsu
  • Cornell University, Ithaca, NY, USA
Alexandra Silva
  • Cornell University, Ithaca, NY, USA
Fabio Zanasi
  • University College London, UK
  • University of Bologna, OLAS team (INRIA), Italy

Funding

  • Gu, Tao: Tao Gu is supported by the UK EPSRC grant EP/S013008/1.
  • Hsu, Justin: Justin Hsu is partially supported by NSF grant #194313.
  • Silva, Alexandra: Silva was partially supported by ERC grant Autoprobe (no. 101002697).
  • Zanasi, Fabio: Fabio Zanasi acknowledges support from EPSRC EP/V002376/1 and MIUR P2022HXNSC (PRIN 2022 PNRR - Next Generation EU).

Acknowledgements

We thank the anonymous reviewers for their close reading and detailed feedback.

Cite AsGet BibTex

Tao Gu, Jialu Bao, Justin Hsu, Alexandra Silva, and Fabio Zanasi. A Categorical Approach to DIBI Models. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 17:1-17:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.FSCD.2024.17

Abstract

The logic of Dependence and Independence Bunched Implications (DIBI) is a logic to reason about conditional independence (CI); for instance, DIBI formulas can characterise CI in discrete probability distributions and in relational databases, using a probabilistic DIBI model and a similarly-constructed relational model. Despite the similarity of the two models, there lacks a uniform account. As a result, the laborious case-by-case verification of the frame conditions required for constructing new models hinders them from generalising the results to CI in other useful models such that continuous distribution. In this paper, we develop an abstract framework for systematically constructing DIBI models, using category theory as the unifying mathematical language. We show that DIBI models arise from arbitrary symmetric monoidal categories with copy-discard structure. In particular, we use string diagrams - a graphical presentation of monoidal categories - to give a uniform definition of the parallel composition and subkernel relation in DIBI models. Our approach not only generalises known models, but also yields new models of interest and reduces properties of DIBI models to structures in the underlying categories. Furthermore, our categorical framework enables a comparison between string diagrammatic approaches to CI in the literature and a logical notion of CI, defined in terms of the satisfaction of specific DIBI formulas. We show that the logical notion is an extension of string diagrammatic CI under reasonable conditions.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • Theory of computation → Semantics and reasoning
  • Theory of computation → Models of computation
Keywords
  • Conditional Independence
  • Dependence Independence Bunched Implications
  • String Diagrams
  • Markov Categories

Metrics

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

References

  1. Samuel Balco. Display calculi and nominal string diagrams. PhD thesis, University of Leicester, 2020. Google Scholar
  2. Samuel Balco and Alexander Kurz. Partially monoidal categories and the algebra of simultaneous substitutions, 2018. Available at URL: https://gdlyrttnap.pl/resources/papers/syco1.pdf.
  3. Samuel Balco and Alexander Kurz. Nominal String Diagrams. In Markus Roggenbach and Ana Sokolova, editors, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019), volume 139 of Leibniz International Proceedings in Informatics (LIPIcs), pages 18:1-18:20, Dagstuhl, Germany, 2019. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CALCO.2019.18.
  4. Jialu Bao, Simon Docherty, Justin Hsu, and Alexandra Silva. A bunched logic for conditional independence. In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-14. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470712.
  5. Gilles Barthe, Justin Hsu, and Kevin Liao. A probabilistic separation logic. Proceedings of the ACM on Programming Languages, 4(POPL):1-30, 2019. URL: https://doi.org/10.1145/3371123.
  6. Thomas Bayes. Lii. an essay towards solving a problem in the doctrine of chances. by the late rev. mr. bayes, f. r. s. communicated by mr. price, in a letter to john canton, a. m. f. r. s. Philosophical Transactions of the Royal Society of London, 53:370-418, 1763. URL: https://doi.org/10.1098/rstl.1763.0053.
  7. Filippo Bonchi, Paweł Sobociński, and Fabio Zanasi. Deconstructing lawvere with distributive laws. Journal of logical and algebraic methods in programming, 95:128-146, 2018. URL: https://doi.org/10.1016/j.jlamp.2017.12.002.
  8. Surajit Chaudhuri and Moshe Y Vardi. Optimization of real conjunctive queries. In Proceedings of the twelfth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, pages 59-70, 1993. URL: https://doi.org/10.1145/153850.153856.
  9. Kenta Cho and Bart Jacobs. Disintegration and Bayesian inversion via string diagrams. Mathematical Structures in Computer Science, 29(7):938-971, 2019. URL: https://doi.org/10.1017/S0960129518000488.
  10. Simon Docherty. Bunched logics: a uniform approach. PhD thesis, UCL (University College London), 2019. Google Scholar
  11. Brendan Fong and David I Spivak. An invitation to applied category theory: seven sketches in compositionality. Cambridge University Press, 2019. URL: https://doi.org/10.1017/9781108668804.
  12. Tobias Fritz. A synthetic approach to markov kernels, conditional independence and theorems on sufficient statistics. Advances in Mathematics, 370:107239, August 2020. URL: https://doi.org/10.1016/j.aim.2020.107239.
  13. Dan Geiger and Judea Pearl. Logical and algorithmic properties of conditional independence and graphical models. The annals of statistics, 21(4):2001-2021, 1993. Google Scholar
  14. Clark Glymour, Kun Zhang, and Peter Spirtes. Review of causal discovery methods based on graphical models. Frontiers in genetics, 10:524, 2019. URL: https://doi.org/10.3389/fgene.2019.00524.
  15. Peter V Golubtsov. Monoidal kleisli category as a background for information transformers theory. Inf. Process., 2(1):62-84, 2002. Google Scholar
  16. Todd J. Green. Bag Semantics, pages 201-206. Springer US, Boston, MA, 2009. URL: https://doi.org/10.1007/978-0-387-39940-9_979.
  17. C. Hermida and R.D. Tennent. Monoidal indeterminates and categories of possible worlds. Theoretical Computer Science, 430:3-22, 2012. Mathematical Foundations of Programming Semantics (MFPS XXV). URL: https://doi.org/10.1016/j.tcs.2012.01.001.
  18. Martin Hofmann. On the interpretation of type theory in locally cartesian closed categories. In Leszek Pacholski and Jerzy Tiuryn, editors, Computer Science Logic, pages 427-441, Berlin, Heidelberg, 1995. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/BFb0022273.
  19. Bart Jacobs. Semantics of weakening and contraction. Annals of pure and applied logic, 69(1):73-106, 1994. URL: https://doi.org/10.1016/0168-0072(94)90020-5.
  20. Achim Klenke. Probability theory: a comprehensive course. Springer Science & Business Media, 2013. URL: https://doi.org/10.1007/978-1-84800-048-3.
  21. Daphne Koller and Nir Friedman. Probabilistic graphical models: principles and techniques. MIT press, 2009. Google Scholar
  22. Joachim Lambek and Philip J Scott. Introduction to higher-order categorical logic, volume 7. Cambridge University Press, 1988. URL: https://doi.org/10.5555/7517.
  23. F William Lawvere. Functorial semantics of algebraic theories. Proceedings of the National Academy of Sciences, 50(5):869-872, 1963. URL: https://doi.org/10.1073/pnas.50.5.869.
  24. John M Li, Amal Ahmed, and Steven Holtzen. Lilac: a modal separation logic for conditional probability. Proceedings of the ACM on Programming Languages, 7(PLDI):148-171, 2023. URL: https://doi.org/10.1145/3591226.
  25. Pierre Simon marquis de Laplace. Théorie analytique des probabilités, volume 7. Courcier, 1820. Google Scholar
  26. Ueli Maurer. Abstract models of computation in cryptography. In Cryptography and Coding: 10th IMA International Conference, Cirencester, UK, December 19-21, 2005. Proceedings 10, pages 1-12. Springer, 2005. Google Scholar
  27. Eugenio Moggi. Notions of computation and monads. Information and computation, 93(1):55-92, 1991. URL: https://doi.org/10.1016/0890-5401(91)90052-4.
  28. Peter W O'Hearn and David J Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215-244, 1999. URL: https://doi.org/10.2307/421090.
  29. Duško Pavlović. Categorical logic of names and abstraction in action calculi. Mathematical Structures in Computer Science, 7(6):619-637, 1997. URL: https://doi.org/10.1017/S0960129597002296.
  30. Dusko Pavlovic. Chasing diagrams in cryptography. In Categories and Types in Logic, Language, and Physics: Essays Dedicated to Jim Lambek on the Occasion of His 90th Birthday, pages 353-367. Springer, 2014. Google Scholar
  31. Dusko Pavlovic. Programs as diagrams: From categorical computability to computable categories. Springer Nature, 2023. URL: https://doi.org/10.1007/978-3-031-34827-3.
  32. Judea Pearl. Causality. Cambridge university press, 2009. URL: https://doi.org/10.1017/CBO9780511803161.
  33. Robin Piedeleu and Fabio Zanasi. An introduction to string diagrams for computer scientists. CoRR, abs/2305.08768, 2023. Google Scholar
  34. David J Pym. The semantics and proof theory of the logic of bunched implications, volume 26. Springer Science & Business Media, 2013. URL: https://doi.org/10.1007/978-94-017-0091-7.
  35. John C Reynolds. Separation logic: A logic for shared mutable data structures. In Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pages 55-74. IEEE, 2002. URL: https://dl.acm.org/doi/10.5555/645683.664578.
  36. Peter Selinger. A survey of graphical languages for monoidal categories. In New structures for physics, pages 289-355. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12821-9_4.
  37. Claude E Shannon. Communication theory of secrecy systems. The Bell system technical journal, 28(4):656-715, 1949. Google Scholar
  38. Alfred Tarski. Logic, semantics, metamathematics: papers from 1923 to 1938. Hackett Publishing, 1983. URL: https://doi.org/10.2307/2216869.
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