Abstract
We introduce a formal meta-language for probabilistic programming, capable of expressing both programs and the type systems in which they are embedded. We are motivated here by the desire to allow an AGI to learn not only relevant knowledge (programs/proofs), but also appropriate ways of reasoning (logics/type systems). We draw on the frameworks of cubical type theory and dependent typed metagraphs to formalize our approach. In doing so, we show that specific constructions within the meta-language can be related via bisimulation (implying path equivalence) to the type systems they correspond. This allows our approach to provide a convenient means of deriving synthetic denotational semantics for various type systems. Particularly, we derive bisimulations for pure type systems (PTS), and probabilistic dependent type systems (PDTS). We discuss further the relationship of PTS to non-well-founded set theory, and demonstrate the feasibility of our approach with an implementation of a bisimulation proof in a Guarded Cubical Type Theory type checker.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Baier, C., Katoen, J.P.: Principles of Model Checking. MIT press (2008)
Barendregt, H., Augustsson, L.: Lambda calculi with types. Handb. Log. Comput. Sci. 34, 239–250 (1992)
Barwise, J., Moss, L.: Vicious circles: on the mathematics of non-wellfounded phenomena (1996)
Birkedal, L., Bizjak, A., Clouston, R., Grathwohl, H.B., Spitters, B., Vezzosi, A.: Guarded cubical type theory: path equality for guarded recursion. arXiv preprint arXiv:1606.05223 (2016)
Goertzel, B.: Modeling uncertain self-referential semantics with infinite-order probabilities (2008)
Goertzel, B.: Folding and unfolding on metagraphs. arXiv preprint arXiv:2012.01759 (2020)
Goertzel, B.: Paraconsistent foundations for probabilistic reasoning, programming and concept formation. arXiv preprint arXiv:2012.14474 (2020)
Goertzel, B.: Reflective metagraph rewriting as a foundation for an AGI ‘language of thought’. arXiv preprint arXiv:2112.08272 (2021)
Harper, R.: Notes on logical frameworks. Lect. Notes, Insts. Adv. Study Nov 29, 34 (2012)
Møgelberg, R.E., Veltri, N.: Bisimulation as path type for guarded recursive types. Proc. ACM on Program. Lang. 3(POPL), 1–29 (2019)
Møgelberg, R.E., Paviotti, M.: Denotational semantics of recursive types in synthetic guarded domain theory. Math. Struct. Comput. Sci. 29(3), 465–510 (2019)
Mokhov, A.: Algebraic graphs with class (functional pearl). ACM SIGPLAN Not. 52(10), 2–13 (2017)
Paviotti, M., Møgelberg, R.E., Birkedal, L.: A model of PCF in guarded type theory. Electron. Notes Theor. Comput. Sci. 319, 333–349 (2015)
Potapov, A.: MeTTa language specification (2021). https://wiki.opencog.org/w/Hyperon
Staton, S., Wood, F., Yang, H., Heunen, C., Kammar, O.: Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints. In: 2016 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pp. 1–10 (2016)
TrueAGI. Hyperon-experimental repository (2021). https://github.com/trueagi-io/hyperon-experimental
Veltri, N., Vezzosi, A.: Formalizing \(\pi \)-calculus in guarded cubical Agda. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 270–283 (2020)
Vezzosi, A., Mörtberg, A., Abel, A.: Cubical Agda: a dependently typed programming language with univalence and higher inductive types. J. Funct. Program. 31, 1–29 (2021)
Warrell, J., Gerstein, M.: Dependent type networks: a probabilistic logic via the curry-howard correspondence in a system of probabilistic dependent types. In: Uncertainty in Artificial Intelligence, Workshop on Uncertainty in Deep Learning (2018). http://www.gatsby.ucl.ac.uk/~balaji/udl-camera-ready/UDL-19.pdf
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Appendices
Appendices
A Proof of Bisimulation for Small-Scale Type System in a Guarded Cubical Type Theory Type Checker
Below, we provide the code for the example discussed in Sect. 5, which uses a Haskell-based GCTT type checker [4]. The code for this example is also provided at: https://github.com/jwarrell/metta_bisimulation.
Rights and permissions
Copyright information
© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Warrell, J., Potapov, A., Vandervorst, A., Goertzel, B. (2023). A Meta-Probabilistic-Programming Language for Bisimulation of Probabilistic and Non-Well-Founded Type Systems. In: Goertzel, B., Iklé, M., Potapov, A., Ponomaryov, D. (eds) Artificial General Intelligence. AGI 2022. Lecture Notes in Computer Science(), vol 13539. Springer, Cham. https://doi.org/10.1007/978-3-031-19907-3_42
Download citation
DOI: https://doi.org/10.1007/978-3-031-19907-3_42
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-19906-6
Online ISBN: 978-3-031-19907-3
eBook Packages: Computer ScienceComputer Science (R0)