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 cha
- PDF / 2,361,360 Bytes
- 222 Pages / 439.42 x 683.15 pts Page_size
- 39 Downloads / 234 Views
Semantics of the Probabilistic Typed Lambda Calculus Markov Chain Semantics, Termination Behavior, and Denotational Semantics
Semantics of the Probabilistic Typed Lambda Calculus
Dirk Draheim
Semantics of the Probabilistic Typed Lambda Calculus Markov Chain Semantics, Termination Behavior, and Denotational Semantics
Dirk Draheim Large-Scale Systems Group Tallinn University of Technology Tallinn, Estonia
ISBN 978-3-642-55197-0 ISBN 978-3-642-55198-7 (eBook) DOI 10.1007/978-3-642-55198-7 Library of Congress Control Number: 2017932370 © Springer-Verlag Berlin Heidelberg 2017 This work is subject to copyright. All rights are reserved by the Publisher, whether the whole or part of the material is concerned, specifically the rights of translation, reprinting, reuse of illustrations, recitation, broadcasting, reproduction on microfilms or in any other physical way, and transmission or information storage and retrieval, electronic adaptation, computer software, or by similar or dissimilar methodology now known or hereafter developed. The use of general descriptive names, registered names, trademarks, service marks, etc. in this publication does not imply, even in the absence of a specific statement, that such names are exempt from the relevant protective laws and regulations and therefore free for general use. The publisher, the authors and the editors are safe to assume that the advice and information in this book are believed to be true and accurate at the date of publication. Neither the publisher nor the authors or the editors give a warranty, express or implied, with respect to the material contained herein or for any errors or omissions that may have been made. The publisher remains neutral with regard to jurisdictional claims in published maps and institutional affiliations. Printed on acid-free paper This Springer imprint is published by Springer Nature The registered company is Springer-Verlag GmbH Germany The registered company address is: Heidelberger Platz 3, 14197 Berlin, Germany
Preface
Today’s information systems operate in probabilistic environments. Programs need to react to probabilistic events. Therefore, a rigorous understanding of probabilistic program behavior becomes ever more important. Probabilistic programming is relevant in its own right, as a means to implement randomized algorithms. This book takes a foundational approach to the semantics of probabilistic programming. It deals with the probabilistic typed lambda calculus, which is the typed lambda calculus with recursion plus probabilistic choice. We elaborate a Markov chain semantics for the probabilistic lambda calculus. As part of this operational semantics, we define a reduction semantics and an evaluation semantics in terms of Markov chain hitting probabilities. The Markov chain semantics unlocks probability theory and Markov chain theory to be used in reasoning about probabilistic programs. Also, we introduce the notions of reduction graphs and reduction trees. Reduction graphs and reduction trees are not part of but rather accom
Data Loading...
