We give two geometry of interaction models for a typed lambda-calculus with recursion endowed with operators for sampling from a continuous uniform distribution and soft conditioning, namely a paradigmatic calculus fo...
详细信息
We give two geometry of interaction models for a typed lambda-calculus with recursion endowed with operators for sampling from a continuous uniform distribution and soft conditioning, namely a paradigmatic calculus for higher-order Bayesian programming. The models are based on the category of measurable spaces and partial measurable functions, and the category of measurable spaces and s-finite kernels, respectively. The former is proved adequate with respect to both a distribution-based and a sampling-based operational semantics, while the latter is proved adequate with respect to a sampling-based operational semantics.
We introduce a system of monadic affine sized types, which substantially generalizes usual sized types and allows in this way to capture probabilistic higher-order programs that terminate almost surely. Going beyond p...
详细信息
We introduce a system of monadic affine sized types, which substantially generalizes usual sized types and allows in this way to capture probabilistic higher-order programs that terminate almost surely. Going beyond plain, strong normalization without losing soundness turns out to be a hard task, which cannot be accomplished without a richer, quantitative notion of types, but also without imposing some affinity constraints. The proposed type system is powerful enough to type classic examples of probabilistically terminating programs such as random walks. The way typable programs are proved to be almost surely terminating is based on reducibility but requires a substantial adaptation of the technique.
In this paper we present an operational semantics for the 'call-by-name' probabilistic lambda-calculus, whose main feature is to use only deterministic relations and to have no constraint on the reduction stra...
详细信息
In this paper we present an operational semantics for the 'call-by-name' probabilistic lambda-calculus, whose main feature is to use only deterministic relations and to have no constraint on the reduction strategy. The calculus enjoys similar properties to the usual lambda-calculus. In particular we prove it to be confluent, and we prove a standardisation theorem.
We study the notion of observational equivalence in the call-by-name probabilistic lambda-calculus, where two terms are said observationally equivalent if under any context, their head reductions converge with the sam...
详细信息
ISBN:
(纸本)9781450355834
We study the notion of observational equivalence in the call-by-name probabilistic lambda-calculus, where two terms are said observationally equivalent if under any context, their head reductions converge with the same probability. Our goal is to generalise the separation theorem to this probabilistic setting. To do so we define probabilistic Bohm trees and probabilistic Nakajima trees, and we mix the well-known Bohm-out technique with some new techniques to manipulate and separate probability distributions.
In this paper we show how the framework of probabilistic abstract interpretation can be applied to statically analyse a probabilistic lambda-calculus. We start by reviewing the classical framework of abstract interpre...
详细信息
In this paper we show how the framework of probabilistic abstract interpretation can be applied to statically analyse a probabilistic lambda-calculus. We start by reviewing the classical framework of abstract interpretation. We choose to use (first-order) strictness analysis as our running example. We present the definition of probabilistic abstract interpretation and use it to construct a probabilistic strictness analysis.
暂无评论