Domain Approximations for Programs with Uncertain Probabilities
Axe & tâche scientifique DigiCosme : SciLex – Tâche 2
Coordinateurs :Jean Goubault-Larrecq
Nom & Prénom du Candidat : Jia, Xiaodong
Laboratoires :
Adossé à l’action DigiCosme :GT SHy
Durée & Dates de la mission : 1 an – avril 2018 – mars 2019
Contexte :
The starting point of this proposal has its origins in the paper static analysis of programs with imprecise inputs, by Adjé et al., where a static analysis framework is proposed for numerical programs with inputs given as imprecise probabilities.
Such programs form an important family of critical mission programs, including controllers in planes and trains. The imprecise probabilistic inputs are typically given by sensors, whose value is probabilistic, but obeys partially known probability distributions. For example, it might be known that a temperature sensor returns a Gaussian distributed value whose average is the outside temperature T, with standard deviation +/- 0.5 degrees C, but the outside temperature T itself is only known to be between -55 degrees and -45 degrees when the plane reaches its cruise altitude.
The above paper rests on a formal concrete semantics based on a measure-theoretic approach, where values of sensors, hence also of program variables, are certain convex sets of probability distributions encoded as so-called measure-theoretic previsions. One would like to have a domain-theoretic explanation of those mathematical objects. That would open the way to natural methods of approximation.
Objectif :
Perhaps the best way to state the objective of this project is in the form of questions:
- Can one find a measure-theoretic semantics of uncertain probabilities as a form of limit of domain-theoretic semantics of uncertain probabilities?
- Can one find measurable maps from X to R as some form of limit of lower semicontinuous maps, perhaps involving computational models in the style of Lawson, Martin, and others?
See the proposal for more details.
Productions Scientifiques :
Xiaodong Jia has arrived, and has been working on the project since May 1st, 2018. He left on April 30rd, 2019.
- The initial problem seems to be hard, and we have had to make the connection between continuous valuations (the standard domain-theoretic model of probabilistic choice) and measures more precise. We have introduced so-called LCS-complete spaces, a new class of spaces on which continuous valuations behave nicely. Notably, LCS-complete spaces form the largest known class on which every continuous valuation extends to a measure. That includes de Brecht’s quasi-Polish spaces, and in particular all Polish spaces from classical topological measure theory. The paper was accepted at the 8th International Symposium on Domain Theory (ISDT’19). This is work in common with Matthew de Brecht (Kyoto University) and is shared with Digicosme project FAC.
- A side question that occurred naturally during this study is the identification of the algebras of the monad V of continuous valuations (with the weak topology, on the category of T0 topological spaces). We have improved on work by Cohen, Escardo and Keimel (2006) and we have established a tight connection between those algebras and a Choquet-like notion of barycenters. The results were also accepted at ISDT’19.
DafPUP was also the occasion to organize a weekly ‘domain theory’ seminar in Cachan. This evolved into a traditional meeting, every Wednesday from 15pm to who knows when (meetings often extended till 19pm or 20pm). Regular participants: Jean Goubault-Larrecq, Xiaodong Jia, Zhenchao Lyu, Loïc Ricaud (since May 1st, 2019). Since May 2019, the domain theory seminar is common with Changsha University, Hunan, China, through FaceTime. A selection of themes: programming languages and logical relations, core-compact but not locally compact spaces, well-filteredness, LCS-complete spaces, powerdomains, countably-based spaces and dcpos, locales and presentations of locales, the Baire condition, Isbell’s non-sober complete lattice, etc.; discussions on recent papers; work sessions on forthcoming papers.
References:
1. Matthew de Brecht, Jean Goubault-Larrecq, Xiaodong Jia, and Zhenchao Lyu. Domain-complete and LCS-complete spaces. 8th International Symposium on Domain Theory (ISDT’19). Electronic Notes in Theoretical Computer Science, accepted, 2019.
2. Jean Goubault-Larrecq, Xiaodong Jia. Algebras of the extended probabilistic powerdomain monad. 8th International Symposium on Domain Theory (ISDT’19). Electronic Notes in Theoretical Computer Science, accepted, 2019.