20 mai 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.