research-article

Boolean-Valued Semantics for the Stochastic λ-Calculus

Authors:

Prakash Panangaden,

Dana ScottAuthors Info & Claims

LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

Pages 669 - 678

https://doi.org/10.1145/3209108.3209175

Published: 09 July 2018 Publication History

Abstract

The ordinary untyped λ-calculus has a λ-theoretic model proposed in two related forms by Scott and Plotkin in the 1970s. Recently Scott showed how to introduce probability by extending these models with random variables. However, to reason about correctness and to add further features, it is useful to reinterpret the construction in a higher-order Boolean-valued model involving a measure algebra. We develop the semantics of an extended stochastic λ-calculus suitable for modeling a simple higher-order probabilistic programming language. We exhibit a number of key equations satisfied by the terms of our language. The terms are interpreted using a continuation-style semantics with an additional argument, an infinite sequence of coin tosses, which serves as a source of randomness. We also introduce a fixpoint operator as a new syntactic construct, as β-reduction turns out not to be sound for unrestricted terms. Finally, we develop a new notion of equality between terms interpreted in a measure algebra, allowing one to reason about terms that may not be equal almost everywhere. This provides a new framework and reasoning principles for probabilistic programs and their higher-order properties.

References

[1]

John L. Bell. 1985. Boolean-Valued Models and Independence Proofs in Set Theory (2nd ed.). Number 12 in Oxford Logic Guides. Oxford University Press.

[2]

David H. Fremlin. 2003. Measure Theory, Volume 4. http://www.essex.ac.uk/maths/people/fremlin/mt.htm. (2003).

[3]

R. M. Friedberg and H. Rogers. 1959. Reducibility and Completeness for sets of integers. Mathematical Logic Quarterly 5 (1959), 117--125.

[4]

Noah Goodman, Vikash Mansingkha, Daniel Roy, Keith Bonawitz, and Joshua Tenenbaum. 2008. Church: a language for generative models. In Proceedings of the 24th Conference on Uncertainty in Artificial Intelligence. 220--229.

Digital Library

[5]

Andrew D. Gordon, Thore Graepel, Nicolas Rolland, Claudio V. Russo, Johannes Borgström, and John Guiver. 2014. Tabular: a schema-driven probabilistic programming language. In Proceedings of POPL '14, San Diego, CA, USA, January 20-21, 2014. 321--334.

Digital Library

[6]

V. Gupta, R. Jagadeesan, and P. Panangaden. 1999. Stochastic Processes as Concurrent Constraint Programs. In Proceedings of the 26th Proceedings Of The Annual ACM Symposium On Principles Of Programming Languages. 189--202.

Digital Library

[7]

Chris Heunen, Ohad Kammar, Sam Staton, and Hongseok Yang. 2017. A convenient category for higher-order probability theory. In Proceedings of the Thirty-second Annual ACM-IEEE Symposium on Logic in Computer Science.

[8]

C. Jones and G. D. Plotkin. 1989. A Probabilistic Powerdomain of Evaluations. In Proceedings of the Fourth Annual IEEE Symposium On Logic In Computer Science. 186--195.

Digital Library

[9]

A. Jung and R. Tix. 1998. The troublesome probabilistic powerdomain. Electronic Notes in Theoretical Computer Science 13 (1998).

[10]

Olav Kallenberg. 2006. Probabilistic symmetries and invariance principles. Springer Science and Business Media.

[11]

D. Kozen. 1981. Semantics of Probabilistic Programs. Journal of Computer and Systems Sciences 22 (1981), 328--350.

[12]

Ugo Dal Lago, Davide Sangiorgi, and Michele Alberti. 2014. On Coinductive Equivalences for Higher-order Probabilistic Functional Programs. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '14). ACM, New York, NY, USA, 297--308.

Digital Library

[13]

Norman Ramsey and Avi Pfeffer. 2002. Stochastic lambda calculus and monads of probability distributions. In The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 154--165.

Digital Library

[14]

H. Rogers. 1967. Theory of Recursive Functions and Effective Computability. McGraw-Hill.

Digital Library

[15]

Vladimir A. Rohlin. 1952. On the Fundamental Ideas of Measure Theory. Amer. Math. Soc. Transl. 71 (1952).

[16]

N. Saheb-Djahromi. 1978. Probabilistic LCF. In Mathematical Foundations Of Computer Science (Lecture Notes In Computer Science). Springer-Verlag.

[17]

Dana Scott. 1967. A Proof of the Independence of the Continuum Hypothesis. Mathematical Systems Theory 1, 2 (1967), 89--111.

[18]

D. Scott. 2014. Stochastic Lambda Calculi: An extended Abstract. Journal of Applied Logic 12 (2014), 369--376.

Digital Library

[19]

S. Smolka, P. Kumar, N. Fosterand D. Kozen, and A. Silva. 2017. Cantor meets Scott: Domain-theoretic foundations for probabilistic network programming. In Proceedings of the 44th ACM SIGPLAN Symp. Principles of Programming Languages (POPL'17). ACM, 557--571. ACM SIGPLAN Notices - POPL '17, Volume 52 Issue 1.

Digital Library

[20]

Sam Staton, Hongseok Yang, Frank Wood, Chris Heunen, and Ohad Kammar. 2017. Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints. In Proceedings of the 31st Annual ACM-IEEE Symposium On Logic In Computer Science. 525--534.

Digital Library

[21]

David Tolpin, Jan-Willem van de Meent, Hongseok Yang, and Frank Wood. 2016. Design and implementation of probabilistic programming language anglican. In Proceedings of the 28th Symposium on the Implementation and Application of Functional Programming Languages. ACM, 6.

Digital Library

[22]

David Williams. 1991. Probability with Martingales. Cambridge University Press.

Cited By

Di Gianantonio PEdalat ASobocinski PLago UEsparza J(2024)A Cartesian Closed Category for Random VariablesProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662126(1-14)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662126
Kubyshkina EPrimiero G(2024)A possible worlds semantics for trustworthy non-deterministic computationsInternational Journal of Approximate Reasoning10.1016/j.ijar.2024.109212172:COnline publication date: 1-Sep-2024
https://dl.acm.org/doi/10.1016/j.ijar.2024.109212
de Amorim PKozen DMardare RPanangaden PRoberts MGorla D(2021)Universal semantics for the stochastic λ-calculusProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470747(1-12)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470747
Show More Cited By

Recommendations

The Bang Calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value
PPDP '16: Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming

We introduce and study the Bang Calculus, an untyped functional calculus in which the promotion operation of Linear Logic is made explicit and where application is a bilinear operation. This calculus, which can be understood as an untyped version of ...
A certified type-preserving compiler from lambda calculus to assembly language
PLDI '07: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation

We present a certified compiler from the simply-typed lambda calculus to assembly language. The compiler is certified in the sense that it comes with a machine-checked proof of semantics preservation, performed with the Coq proof assistant. The compiler ...
A certified type-preserving compiler from lambda calculus to assembly language
Proceedings of the 2007 PLDI conference

We present a certified compiler from the simply-typed lambda calculus to assembly language. The compiler is certified in the sense that it comes with a machine-checked proof of semantics preservation, performed with the Coq proof assistant. The compiler ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

July 2018

960 pages

ISBN:9781450355834

DOI:10.1145/3209108

Copyright © 2018 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGLOG: ACM Special Interest Group on Logic and Computation
EACSL: European Association for Computer Science Logic
IEEE-CS\DATC: IEEE Computer Society

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 July 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Conference

LICS '18

Sponsor:

SIGLOG
EACSL
IEEE-CS\DATC

LICS '18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

July 9 - 12, 2018

Oxford, United Kingdom

Acceptance Rates

Overall Acceptance Rate 215 of 622 submissions, 35%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
138
Total Downloads

Downloads (Last 12 months)13
Downloads (Last 6 weeks)2

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Di Gianantonio PEdalat ASobocinski PLago UEsparza J(2024)A Cartesian Closed Category for Random VariablesProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662126(1-14)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662126
Kubyshkina EPrimiero G(2024)A possible worlds semantics for trustworthy non-deterministic computationsInternational Journal of Approximate Reasoning10.1016/j.ijar.2024.109212172:COnline publication date: 1-Sep-2024
https://dl.acm.org/doi/10.1016/j.ijar.2024.109212
de Amorim PKozen DMardare RPanangaden PRoberts MGorla D(2021)Universal semantics for the stochastic λ-calculusProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470747(1-12)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470747
Faggian CRocca SBouyer P(2019)Lambda calculus and probabilistic computationProceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3470152.3470186(1-13)Online publication date: 24-Jun-2019
https://dl.acm.org/doi/10.5555/3470152.3470186
Kobayashi NLago UGrellois CBouyer P(2019)On the termination problem for probabilistic higher-order recursive programsProceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3470152.3470177(1-14)Online publication date: 24-Jun-2019
https://dl.acm.org/doi/10.5555/3470152.3470177
Vákár MKammar OStaton S(2019)A domain theory for statistical probabilistic programmingProceedings of the ACM on Programming Languages10.1145/32903493:POPL(1-29)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290349
Faggian CRocca S(2019)Lambda Calculus and Probabilistic Computation2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS.2019.8785699(1-13)Online publication date: Jun-2019
https://doi.org/10.1109/LICS.2019.8785699

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents