Boolean-valued semantics for the stochastic λ-calculus

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

9 Citations (Scopus)
13 Downloads (Pure)

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 publicationLICS '18 : Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science
Place of PublicationPiscataway, NJ.
Pages669-678
Number of pages10
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
Country/TerritoryUnited Kingdom
CityOxford
Period9/07/1812/07/18

Funding

This research was supported by the DFF Danish research grant FNU 4181-00360, by a grant from NSERC (Canada), and by a grant from the National Science Foundation (USA). We gratefully acknowledge the support of the Simons Institute Logical Structures in Computation Program in Fall 2016. We thank Ugo Dal Lago, Cameron Freer, Marco Gaobardi, Chris Heunen, Alex Simpson and Sam Staton for useful discussions.

Keywords

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

Fingerprint

Dive into the research topics of 'Boolean-valued semantics for the stochastic λ-calculus'. Together they form a unique fingerprint.

Cite this