### 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 language | English |
---|---|

Title of host publication | Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018 |

Pages | 669-678 |

Number of pages | 10 |

ISBN (Electronic) | 9781450355834, 9781450355834 |

DOIs | |

Publication status | Published - 9 Jul 2018 |

Event | 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018 - Oxford, United Kingdom Duration: 9 Jul 2018 → 12 Jul 2018 |

### Conference

Conference | 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018 |
---|---|

Country | United Kingdom |

City | Oxford |

Period | 9/07/18 → 12/07/18 |

### Fingerprint

### Keywords

- boolean-valued models
- denotational semantics
- random variables
- stochastic λ-calculus

### Cite this

*Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018*(pp. 669-678) https://doi.org/10.1145/3209108.3209175

}

*Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018.*pp. 669-678, 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, United Kingdom, 9/07/18. https://doi.org/10.1145/3209108.3209175

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution book

TY - GEN

T1 - Boolean-valued semantics for the stochastic -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

UR - http://www.scopus.com/inward/record.url?scp=85051105439&partnerID=8YFLogxK

U2 - 10.1145/3209108.3209175

DO - 10.1145/3209108.3209175

M3 - Conference contribution book

SP - 669

EP - 678

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

ER -