A deterministic rewrite system for the probabilistic λ-calculus

Source abstract

Abstract In this paper we present an operational semantics for the ‘call-by-name’ probabilistic λ -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 λ -calculus. In particular we prove it to be confluent, and we prove a standardisation theorem.