Semantics of the Probabilistic Typed Lambda Calculus

Markov Chain Semantics, Termination Behavior, and Denotational Semantics

verfasst von: Dirk Draheim

Verlag: Springer Berlin Heidelberg

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Über dieses Buch

This book takes a foundational approach to the semantics of probabilistic programming. It elaborates a rigorous Markov chain semantics for the probabilistic typed lambda calculus, which is the typed lambda calculus with recursion plus probabilistic choice.

The book starts with a recapitulation of the basic mathematical tools needed throughout the book, in particular Markov chains, graph theory and domain theory, and also explores the topic of inductive definitions. It then defines the syntax and establishes the Markov chain semantics of the probabilistic lambda calculus and, furthermore, both a graph and a tree semantics. Based on that, it investigates the termination behavior of probabilistic programs. It introduces the notions of termination degree, bounded termination and path stoppability and investigates their mutual relationships. Lastly, it defines a denotational semantics of the probabilistic lambda calculus, based on continuous functions over probability distributions as domains.

The work mostly appeals to researchers in theoretical computer science focusing on probabilistic programming, randomized algorithms, or programming language theory.

Inhaltsverzeichnis

Frontmatter

1. Introduction

Abstract

In this chapter we explain why a rigorous understanding of probabilistic program behavior becomes ever more important. In this motivation, we take several perspectives, i.e., the perspectives of system simulation, system analytics and randomized algorithms. We outline the syntax and the Markov chain semantics of the probabilistic lambda calculus and motivate the most important concepts concerning its termination behavior. Also, we motivate the denotational semantics of the probabilistic lambda calculus.

Dirk Draheim

2. Preliminary Mathematics

Abstract

This chapter recapitulates basic mathematical tools needed in the semantics of the probabilistic lambda calculus, in particular, from the fields of probability theory, Markov chains, graph theory and domain theory. Also, it delves into the topic of inductive definitions.

Dirk Draheim

3. Syntax and Operational Semantics

Abstract

Dirk Draheim

4. Termination Behavior

Abstract

In this chapter we investigate the termination behavior of the probabilistic lambda calculus. We introduce the notion of termination degree and the notion of bounded termination. We introduce the notion of path stoppability, which characterizes a broadened class of termination and allows for the computation of program runs that are otherwise considered as non-terminating. Then, we systematically investigate the mutual dependencies between path stoppability, bounded termination and termination degrees. To achieve this, the chapter establishes the graph semantics as well as the tree semantics of the probabilistic lambda calculus. Also, it shows some needed graph cover lemmas.

Dirk Draheim

5. Denotational Semantics

Abstract

In this chapter we define a denotational semantics of the probabilistic lambda calculus, based on continuous functions over probability distributions as domains. We show the basic correspondence of the denotational semantics with respect to the Markov chain semantics.

Dirk Draheim

Backmatter

Titel: Semantics of the Probabilistic Typed Lambda Calculus
verfasst von: Dirk Draheim
Verlag: Springer Berlin Heidelberg
Electronic ISBN: 978-3-642-55198-7
Print ISBN: 978-3-642-55197-0
DOI: https://doi.org/10.1007/978-3-642-55198-7