Mitchell Wand
Ryan Culpepper
Abstract
We present a complete reasoning principle for contextual equivalence in an untyped probabilistic language. The language includes continuous (real-valued) random variables, conditionals, and scoring. It also includes recursion, since the standard call-by-value fixpoint combinator is expressible.
We demonstrate the usability of our characterization by proving several equivalence schemas, including familiar facts from lambda calculus as well as results specific to probabilistic programming. In particular, we use it to prove that reordering the random draws in a probabilistic program preserves contextual equivalence. This allows us to show, for example, that
(let x = e1 in let y = e2 in e0) =ctx (let y = e2 in let x = e1 in e0)
(provided x does not occur free in e2 and y does not occur free in e1) despite the fact that e1 and e2 may have sampling and scoring effects.
Supplemental Material
- Amal J. Ahmed. 2006. Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types. In Proc. 15th European Symposium on Programming (ESOP ’06). 69–83. Google Scholar
Digital Library
- Ales Bizjak and Lars Birkedal. 2015. Step-Indexed Logical Relations for Probability. In Proc. 18th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS ’15). 279–294.Google ScholarCross Ref
- Johannes Borgström, Ugo Dal Lago, Andrew D. Gordon, and Marcin Szymczak. 2017. A Lambda-calculus Foundation for Universal Probabilistic Programming (long version). https://arxiv.org/abs/1512.08990Google Scholar
- Johannes Borgström, Ugo Dal Lago, Andrew D. Gordon, and Marcin Szymczak. 2016. A lambda-calculus foundation for universal probabilistic programming. In Proc. 21st ACM SIGPLAN International Conference on Functional Programming (ICFP ’16). 33–46. Google ScholarDigital Library
- Raphaëlle Crubillé and Ugo Dal Lago. 2014. On Probabilistic Applicative Bisimulation and Call-by-Value λ-Calculi. In Proc. 23rd European Symposium on Programming (ESOP ’14). 209–228. Google ScholarDigital Library
- Ryan Culpepper and Andrew Cobb. 2017. Contextual Equivalence for Probabilistic Programs with Continuous Random Variables and Scoring. In Proc. 26th European Symposium on Programming (ESOP ’17). 368–392.Google ScholarDigital Library
- Thomas Ehrhard, Christine Tasson, and Michele Pagani. 2014. Probabilistic coherence spaces are fully abstract for probabilistic PCF. In Proc. 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’14). 309–320. Google ScholarDigital Library
- Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt. 2009. Semantics Engineering with PLT Redex (1st ed.). The MIT Press. Google ScholarDigital Library
- Noah D. Goodman, Vikash K. Mansinghka, Daniel M. Roy, Keith Bonawitz, and Joshua B. Tenenbaum. 2008. Church: a language for generative models. In Proc. 24th Conference in Uncertainty in Artificial Intelligence (UAI ’08). 220–229. Google ScholarDigital Library
- Daniel Huang and Greg Morrisett. 2016. An Application of Computable Distributions to the Semantics of Probabilistic Programming Languages. In Proc. 25th European Symposium on Programming (ESOP ’16). 337–363.Google ScholarDigital Library
- Oleg Kiselyov and Chung-chieh Shan. 2009. Embedded Probabilistic Programming. In Proc. IFIP TC 2 Working Conference on Domain-Specific Languages (DSL ’09). 360–384. Google ScholarDigital Library
- Vikash Mansinghka, Daniel Selsam, and Yura Perov. 2014. Venture: a higher-order probabilistic programming platform with programmable inference. http://arxiv.org/abs/1404.0099Google Scholar
- Ian Mason and Carolyn Talcott. 1991. Equivalence in functional languages with effects. J. Funct. Program. 1, 3 (1991), 287–327.Google ScholarCross Ref
- Kevin P. Murphy. 2007. Conjugate Bayesian analysis of the Gaussian distribution. https://www.cs.ubc.ca/~murphyk/ Papers/bayesGauss.pdfGoogle Scholar
- Praveen Narayanan, Jacques Carette, Wren Romano, Chung-chieh Shan, and Robert Zinkov. 2016. Probabilistic Inference by Program Transformation in Hakaru (System Description). In Proc. 13th International Symposium on Functional and Logic Programming (FLOPS ’16). 62–79.Google ScholarCross Ref
- Brooks Paige and Frank Wood. 2014. A Compilation Target for Probabilistic Programming Languages. In Proc. 31th International Conference on Machine Learning (ICML ’14). 1935–1943. Google ScholarDigital Library
- Sungwoo Park, Frank Pfenning, and Sebastian Thrun. 2008. A Probabilistic Language Based on Sampling Functions. ACM Trans. Program. Lang. Syst. 31, 1, Article 4 (Dec. 2008), 4:1–4:46 pages. Google ScholarDigital Library
- Andrew M. Pitts. 2010. Step-Indexed Biorthogonality: a Tutorial Example. In Modelling, Controlling and Reasoning About State (Dagstuhl Seminar Proceedings), Amal Ahmed, Nick Benton, Lars Birkedal, and Martin Hofmann (Eds.). http: //drops.dagstuhl.de/opus/volltexte/2010/2806/Google Scholar
- Amr Sabry and Matthias Felleisen. 1993. Reasoning about programs in continuation-passing style. LISP and Symbolic Computation 6, 3 (01 Nov 1993), 289–360. Google ScholarDigital Library
- Davide Sangiorgi and Valeria Vignudelli. 2016. Environmental bisimulations for probabilistic higher-order languages. In Proc. 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’16). 595–607. Google ScholarDigital Library
- Sam Staton. 2017. Commutative Semantics for Probabilistic Programming. In Proc. 26th European Symposium on Programming (ESOP ’17). 855–879. Google ScholarDigital Library
- Sam Staton, Hongseok Yang, Frank Wood, Chris Heunen, and Ohad Kammar. 2016. Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints. In Proc. 31st IEEE Symposium on Logic in Computer Science (LICS ’16). 525–534. Google ScholarDigital Library
- Mitchell Wand, Ryan Culpepper, Theophilos Giannakopoulos, and Andrew Cobb. 2018. Contextual Equivalence for a Probabilistic Language with Continuous Random Variables and Recursion. https://arxiv.org/abs/1807.02809 Google ScholarDigital Library
- Frank Wood, Jan-Willem van de Meent, and Vikash Mansinghka. 2014. A New Approach to Probabilistic Programming Inference. In Proc. 17th International Conference on Artificial Intelligence and Statistics (AISTATS ’14). 1024–1032.Google Scholar
Index Terms
- Contextual equivalence for a probabilistic language with continuous random variables and recursion
Recommendations
Contextual Equivalence in a Probabilistic Call-by-Need Lambda-Calculus
PPDP '22: Proceedings of the 24th International Symposium on Principles and Practice of Declarative ProgrammingTo support the understanding of declarative probabilistic programming languages, we introduce a lambda-calculus with a fair binary probabilistic choice that chooses between its arguments with equal probability. The reduction strategy of the calculus is ...
A bisimulation for type abstraction and recursion
POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languagesWe present a sound, complete, and elementary proof method, based on bisimulation, for contextual equivalence in a λ-calculus with full universal, existential, and recursive types. Unlike logical relations (either semantic or syntactic), our development ...
Names, Equations, Relations: Practical Ways to Reason about new
The nu-calculus of Pitts and Stark is a typed lambda-calculus, extended with state in the form of dynamically-generated names. These names can be created locally, passed around, and compared with one another. Through the interaction between names and ...
Comments