A Radically Elementary Probabilistic Lambda-CalculusFPW (Paris)Remote
Randomised computation – i.e. the ability for a computer program to throw a dice to decide the next execution step – is ubiquitous in real-life programming languages. The simplest way to add probabilistic features to lambda-calculus is via a binary choice operator ⊕, such that M ⊕ N reduces to M with probability 1/2, and to N also with probability 1/2. In this setting, the probabilistic behaviour of programs can be expressed using only discrete probabilities, i.e. probability distributions on countable sets. The operational and denotational semantics for discrete randomised lambda-calculi have been thoroughly studied [DLZ12, ETP14, … ]. A more involved use of probabilistic programming languages consists in building probabilistic models of external systems (e.g. physical phenomena), that can be either intrinsically probabilistic, or on which we have only incomplete information. In this setting, it is often the case that those models need to be represented as probability distributions on continuous sets, as for instance the set of real numbers. The operational and denotational semantics of continuous probabilistic languages has also been thoroughly investigated [BDLGS16, HKSY17, PW18, EG25, … ], but need more involved mathematics (measure theory, topology, presheaf categories… ) than in the discrete case. Our aim in this work in progress is to use a non-standard axiomatic to propose a much simpler semantics for continuous probabilistic lambda-calculus. Our approach is in some sense similar to the line of work aiming to use nonstandard analysis for verification of hybrid systems with continuous time [BBCP12, sPHV15, SH11a, SH11b, … ]: they use non-standard analysis in place of continuous-time differential equations, while we want to use it to remove the need for measure theory for analysis of probabilistic programs on continuous data types. In the present abstract, we first present a brief summary of the non-standard axiomatic we work with, then some preliminary definitions for a non-standard operational semantics of probabilistic programming language with continuous datatypes, followed by a speculative list of possible research directions.