### May 20, 2019

**Jean Goubault Larrecq**(LSV - ENS Cachan)

It seems pretty obvious to add random choice to your

preferred higher-order functional language.

One can then give it an operational semantics in the form

of an infinite Markov chain whose states are

machine configurations, and with easily understandable

rules.

Denotational semantics provide helpful invariants to

reason about programs, and Jones and Plotkin’s

probabilistic powerdomain (1990) models random choice

elegantly.

One can then interpret higher-order probabilistic

programs in the category of dcpos (directed-complete

partial orders), and that works perfectly well…

except that some dcpos are rather pathological,

and that prevents us from proving all the theorems

we would like to have. As a case in point, it

is unknown whether Fubini’s theorem holds on all

dcpos, which means that drawing x then y at random

is not known to be equivalent with drawing y then x.

Such problems do not occur with so-called continuous

dcpos, but then we must face the Jung-Tix problem (1998):

we do not know of any category of continuous dcpos

that can handle both higher-order features and

the probabilistic powerdomain.

We will show that there is a simple way of getting

around the Jung-Tix problem, relying on a variant

of Levy’s call-by-push-value paradigm (2003), and provided

we also include a form of demonic non-deterministic

choice (related to must-termination, operationally).

We will argue that the language satisfies adequacy:

on programs of base type (int), the denotational semantics

computes a subprobability distribution whose

mass at any given number n is exactly the minimal probability

that the output of the program will be n.

If we have time, we will then study full abstraction,

namely the relation between denotational (in)equality

and the observational preorder. Our language is

not fully abstract. One reason is expected: the absence

of parallel conditionals. Another has surfaced

more recently, and that is the absence of so-called

statistical termination testers. With both added,

however, our language is fully abstract.