## Authors: Radu Mardare, Prakash Panangaden, Dexter Kozen, Dana Scott, Robert Furber and Giorgio Bacci

## Paper Information

Title: | Boolean-Valued Semantics for Stochastic Lambda-Calculus |

Authors: | Radu Mardare, Prakash Panangaden, Dexter Kozen, Dana Scott, Robert Furber and Giorgio Bacci |

Proceedings: | LICS PDF files |

Editors: | Anuj Dawar and Erich GrĂ¤del |

Keywords: | stochastic lambda calculus, Boolean-valued models, random variables, denotational semantics |

Abstract: | ABSTRACT. The ordinary untyped lambda-calculus has a set-theoretic model proposed in two related forms by Scott and Plotkin in the 1970s. Recently Scott saw how to extend such $\lambda$-calculus models using random variables in a standard way. However, to do reasoning and to add further features, it is better to interpret the construction in a higher-order Boolean- valued model theory using the standard measure algebra. In this paper we develop the semantics of an extended stochastic lambda-calculus suitable for a simple probabilistic programming language, and we exhibit a number of key equations satisfied by the terms of our example language. The terms are interpreted using a continuation-style semantics along with an additional argument, an infinite sequence of coin tosses which serve as a source of randomness. The construction of the model requires a subtle measure-theoretic analysis of the space of coin-tossing sequences. We also introduce a fixed-point operator as a new syntactic construct, as beta-reduction turns out not sound for all terms in our semantics. Finally, we develop a new notion of equality between terms valued by elements of the measure algebra, allowing one to reason about terms that may not be equal almost everywhere. This we hope provides a new framework for developing reasoning about probabilistic programs and their properties of higher type. |

Pages: | 10 |

Talk: | Jul 09 16:40 (Session 51E) |

Paper: |