Interpreting Lambda Calculus in Domain-Valued Random Variables
This work provides a foundational framework for probabilistic semantics in lambda calculus, relevant to researchers in domain theory and probabilistic programming.
The paper develops Boolean-valued domain theory to interpret lambda calculus in domain-valued random variables, focusing on reflexive domain construction and showing that equation validity corresponds to the top element of the Boolean algebra.
We develop Boolean-valued domain theory and show how the lambda-calculus can be interpreted in using domain-valued random variables. We focus on the reflexive domain construction rather than the language and its semantics. The notion of equality has to be interpreted in the Boolean algebra and when we say that an equation is valid in the model we mean that its interpretation is the top element of the Boolean algebra.