Boolean-valued semantics for the stochastic Lambda-calculus

Giorgio Bacci, Robert Furber, Dexter Kozen, Radu Mardare, Prakash Panangaden, Dana Scott

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

3 Citations (Scopus)

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.
Original languageEnglish
Title of host publicationProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018
Number of pages10
PublisherAssociation for Computing Machinery
Publication date9 Jul 2018
Pages669-678
ISBN (Electronic)978-1-4503-5583-4
DOIs
Publication statusPublished - 9 Jul 2018
Event33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018 - Oxford, United Kingdom
Duration: 9 Jul 201812 Jul 2018

Conference

Conference33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018
CountryUnited Kingdom
CityOxford
Period09/07/201812/07/2018
SponsorACM Special Interest Group on Logic and Computation (SIGLOG), European Association for Computer Science Logic (EACSL), IEEE Computer Society (IEEE-CS\DATC)

Fingerprint

Stochastic Calculus
Lambda Calculus
Measure Algebra
Term
Higher Order
Probabilistic Programming
Fixpoint
Randomness
Continuation
Programming Languages
Correctness
Equality
Calculus
Reasoning
Random variable
Semantics
Model
Operator
Modeling

Keywords

  • Boolean-valued models
  • Denotational semantics
  • Random variables
  • Stochastic λ-calculus

Cite this

Bacci, G., Furber, R., Kozen, D., Mardare, R., Panangaden, P., & Scott, D. (2018). Boolean-valued semantics for the stochastic Lambda-calculus. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018 (pp. 669-678). Association for Computing Machinery. https://doi.org/10.1145/3209108.3209175
Bacci, Giorgio ; Furber, Robert ; Kozen, Dexter ; Mardare, Radu ; Panangaden, Prakash ; Scott, Dana. / Boolean-valued semantics for the stochastic Lambda-calculus. Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018. Association for Computing Machinery, 2018. pp. 669-678
@inproceedings{9a19d854af8544a9b2fcfff3559ec817,
title = "Boolean-valued semantics for the stochastic Lambda-calculus",
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.",
keywords = "Boolean-valued models, Denotational semantics, Random variables, Stochastic λ-calculus",
author = "Giorgio Bacci and Robert Furber and Dexter Kozen and Radu Mardare and Prakash Panangaden and Dana Scott",
year = "2018",
month = "7",
day = "9",
doi = "10.1145/3209108.3209175",
language = "English",
pages = "669--678",
booktitle = "Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018",
publisher = "Association for Computing Machinery",
address = "United States",

}

Bacci, G, Furber, R, Kozen, D, Mardare, R, Panangaden, P & Scott, D 2018, Boolean-valued semantics for the stochastic Lambda-calculus. in Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018. Association for Computing Machinery, pp. 669-678, 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, United Kingdom, 09/07/2018. https://doi.org/10.1145/3209108.3209175

Boolean-valued semantics for the stochastic Lambda-calculus. / Bacci, Giorgio; Furber, Robert; Kozen, Dexter; Mardare, Radu; Panangaden, Prakash; Scott, Dana.

Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018. Association for Computing Machinery, 2018. p. 669-678.

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

TY - GEN

T1 - Boolean-valued semantics for the stochastic Lambda-calculus

AU - Bacci, Giorgio

AU - Furber, Robert

AU - Kozen, Dexter

AU - Mardare, Radu

AU - Panangaden, Prakash

AU - Scott, Dana

PY - 2018/7/9

Y1 - 2018/7/9

N2 - 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.

AB - 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.

KW - Boolean-valued models

KW - Denotational semantics

KW - Random variables

KW - Stochastic λ-calculus

U2 - 10.1145/3209108.3209175

DO - 10.1145/3209108.3209175

M3 - Article in proceeding

AN - SCOPUS:85051105439

SP - 669

EP - 678

BT - Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018

PB - Association for Computing Machinery

ER -

Bacci G, Furber R, Kozen D, Mardare R, Panangaden P, Scott D. Boolean-valued semantics for the stochastic Lambda-calculus. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018. Association for Computing Machinery. 2018. p. 669-678 https://doi.org/10.1145/3209108.3209175