Thomas Leventis (Institut de Mathématiques de Luminy), Theories in Probabilistic lambda-calculus.



Our goal is to extend the notion of lambda-theory to the call-by-name probabilistic lambda-calculus. We will first describe this calculus without using probabilistic reductions nor specifying a reduction strategy, so that we can give a meaning to the notion of beta-equivalence. We will then define probabilistic lambda-theories, as well as the notions of extensionality and sensibility for such theories. Lastly we will present a result similar to the one proved by Martin Hyland in usual lambda-calculus: there is a maximum consistent extensional sensible lambda-theory, and it is given by the equality of Böhm trees or equivalently by the observational equivalence of terms.