Abstract
It is well-known that constructing models of higher-order probabilistic programming languages is challenging. We show how to construct step-indexed logical relations for a probabilistic extension of a higher-order programming language with impredicative polymorphism and recursive types. We show that the resulting logical relation is sound and complete with respect to the contextual preorder and, moreover, that it is convenient for reasoning about concrete program equivalences. Finally, we extend the language with dynamically allocated first-order references and show how to extend the logical relation to this language. We show that the resulting relation remains useful for reasoning about examples involving both state and probabilistic choice.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Ahmed, A.: Semantics of Types for Mutable State. Ph.D. thesis, Princeton University (2004)
Ahmed, A.: Step-indexed syntactic logical relations for recursive and quantified types. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 69–83. Springer, Heidelberg (2006)
Appel, A.W., McAllester, D.: An indexed model of recursive types for foundational proof-carrying code. ACM Transactions on Programming Languages and Systems 23(5) (2001)
Birkedal, L., Bizjak, A., Schwinghammer, J.: Step-indexed relational reasoning for countable nondeterminism. Logical Methods in Computer Science 9(4) (2013)
Birkedal, L., Reus, B., Schwinghammer, J., Støvring, K., Thamsborg, J., Yang, H.: Step-indexed kripke models over recursive worlds. In: Proceedings of the 38th Symposium on Principles of Programming Languages, pp. 119–132. ACM (2011)
Bizjak, A., Birkedal, L.: Step-indexed logical relations for probability. arXiv:1501.02623 [cs.LO] (2015), long version of this paper
Crubillé, R., Dal Lago, U.: On probabilistic applicative bisimulation and call-by-value λ-calculi. In: Shao, Z. (ed.) ESOP 2014 (ETAPS). LNCS, vol. 8410, pp. 209–228. Springer, Heidelberg (2014)
Dal Lago, U., Sangiorgi, D., Alberti, M.: On coinductive equivalences for higher-order probabilistic functional programs. In: Proceedings of 41st Symposium on Principles of Programming Languages, pp. 297–308. ACM (2014)
Danos, V., Harmer, R.S.: Probabilistic game semantics. ACM Transactions on Computational Logic 3(3) (2002)
Dreyer, D., Ahmed, A., Birkedal, L.: Logical step-indexed logical relations. Logical Methods in Computer Science 7(2) (2011)
Dreyer, D., Neis, G., Birkedal, L.: The impact of higher-order state and control effects on local relational reasoning. Journal of Functional Programming 22(4-5 special issue), 477–528 (2012)
Ehrhard, T., Pagani, M., Tasson, C.: The computational meaning of probabilistic coherence spaces. In: Proceedings of the 26th IEEE Symposium on Logic in Computer Science, pp. 87–96. IEEE (2011)
Ehrhard, T., Tasson, C., Pagani, M.: Probabilistic coherence spaces are fully abstract for probabilistic pcf. In: Proceedings of 41st Symposium on Principles of Programming Languages, pp. 309–320. ACM (2014)
Johann, P., Simpson, A., Voigtländer, J.: A generic operational metatheory for algebraic effects. In: Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, pp. 209–218. IEEE (2010)
Jones, C., Plotkin, G.: A probabilistic powerdomain of evaluations. In: Proceedings of the 4th Symposium on Logic in Computer Science, pp. 186–195. IEEE (1989)
Lago, U.D., Zorzi, M.: Probabilistic operational semantics for the lambda calculus. RAIRO - Theoretical Informatics and Applications 46 (2012)
Pitts, A.M.: Parametric polymorphism and operational equivalence. Mathematical Structures in Computer Science 10(3) (2000)
Pitts, A.M.: Typed operational reasoning. In: Pierce, B.C. (ed.) Advanced Topics in Types and Programming Languages, ch. 7. MIT Press (2005)
Pitts, A.M.: Step-indexed biorthogonality: a tutorial example. In: Ahmed, A., Benton, N., Birkedal, L., Hofmann, M. (eds.) Modelling, Controlling and Reasoning About State. No. 10351 in Dagstuhl Seminar Proceedings (2010)
Ramsey, N., Pfeffer, A.: Stochastic lambda calculus and monads of probability distributions. In: Proceedings of the 29th Symposium on Principles of Programming Languages, pp. 154–165. ACM (2002)
Saheb-Djahromi, N.: Cpo’s of measures for nondeterminism. Theoretical Computer Science 12(1) (1980)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bizjak, A., Birkedal, L. (2015). Step-Indexed Logical Relations for Probability. In: Pitts, A. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2015. Lecture Notes in Computer Science(), vol 9034. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46678-0_18
Download citation
DOI: https://doi.org/10.1007/978-3-662-46678-0_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-46677-3
Online ISBN: 978-3-662-46678-0
eBook Packages: Computer ScienceComputer Science (R0)