Skip to main content
main-content

Ü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

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

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

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

4. Termination Behavior

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

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

Weitere Informationen

BranchenIndex Online

Die B2B-Firmensuche für Industrie und Wirtschaft: Kostenfrei in Firmenprofilen nach Lieferanten, Herstellern, Dienstleistern und Händlern recherchieren.

Whitepaper

- ANZEIGE -

Globales Erdungssystem in urbanen Kabelnetzen

Bedingt durch die Altersstruktur vieler Kabelverteilnetze mit der damit verbundenen verminderten Isolationsfestigkeit oder durch fortschreitenden Kabelausbau ist es immer häufiger erforderlich, anstelle der Resonanz-Sternpunktserdung alternative Konzepte für die Sternpunktsbehandlung umzusetzen. Die damit verbundenen Fehlerortungskonzepte bzw. die Erhöhung der Restströme im Erdschlussfall führen jedoch aufgrund der hohen Fehlerströme zu neuen Anforderungen an die Erdungs- und Fehlerstromrückleitungs-Systeme. Lesen Sie hier über die Auswirkung von leitfähigen Strukturen auf die Stromaufteilung sowie die Potentialverhältnisse in urbanen Kabelnetzen bei stromstarken Erdschlüssen. Jetzt gratis downloaden!

Bildnachweise