Full Abstraction for Languages with Demonic and Probabilistic Choice
Axe & tâche scientifique DigiCosme : SciLex –
Coordinateurs :Jean-Goubault Larrecq, LSV – Evelyne Contejean, LRI
Nom & Prénom du Candidat : Zhenchao LIU
Adresse mail :
Laboratoire gestionnaire: LSV
Adossé à l’action DigiCosme :GT PeRSPECTIVE
Durée & Dates de la mission : 1 an – 01/09/2018 — 31/08/2019
Contexte :
The full abstraction problem was introduced by Plotkin in 1977 for the higher-order, call-by-name, purely functional, deterministic language PCF Plo77. Let us describe what the full abstraction problem is about—for a general programming language L, not just PCF. In brief, the problem is to be able to prove that concrete implementations of L (as compilers, or interpreters) do exactly what the mathematical, denotational
semantics of L prescribe. This is a surprisingly hard problem. It is also needed to make the link between: proofs of software correctness based upon the denotational semantics, using tools such as the theorem provers and proof assistants developed in team VALS—and, to a certain extent, at LSV, although the activities of LSV are more centered on specific software systems and less on programs written in all purpose langages;and actual implementations of languages L, which typically rely on an operational semantics—see below. There are at least two ways of describing what programs in L do. The first one is through a denotational semantics, and is a map from programs to values JK in some domain. In other words, it is a description of what the program computes. The other one is through an operational semantics, and describes how a machine would actually execute , by saying how it should pass from one configuration to the next one in an actual computation. Denotational semantics are good as a basis for reasoning about programs. Operational semantics are good for describing implementations of languages. They are also good for reasoning about some classes of programs, for example, imperative programs under callby-value semantics and no or little higher-order programming. For more complex programs, however, nothing beats denotational semantics. A good example of that is Berger’s functional Ber93, later improved upon by Escardó Esc07, an amazing function (written in the higher-order, call-by-need language Haskell) that allows you to explore certain infinite sets—exhaustively—in finite time. Its only reasonable proof of correctness is via topology, and notably the realization that the universal quantifier on a topological space X is a continuous map if and only if X is compact. The only known way to show that through an operational semantics instead, is through operational domain theory EH09, which is a pretty complicated way of simulating topology from operational semantics. Given two semantics for a language L, one operational, the other denotational, one is naturally led to the following question, first asked by Plotkin in 1977: do the two semantics actually compute the same thing? That is of course an important question if one ever hopes that proofs done with denotational semantics would apply to machines implementing the operational semantics. But the question has several different meanings, depending on what “the same thing” means: Soundness: if the operational semantics says that computing eventually terminates and returns some natural number n, then the value JK of is the denotational semantics should be n as well. Adequacy (a form of converse): if JK = n for some natural number, then computing operationally will terminate (this is the hard point) and eventually return n. Full abstraction. This is more complicated. Write C[] for the program that you obtain by plugging program inside some context C. A context is merely a program with a hole in it, and represents any execution context, for example any operating system you might run in. Two programs and 0 are contextually equivalent if and only if you cannot distinguish them under any context, namely: for every context C, for every natural number n, C[] returns n if and only if C0 returns n. Soundness and adequacy imply that any two programs and 0 with the same value (JK = J0K) are contextually equivalent. Full abstraction is the converse property: L is fully abstract if and only if, for all programs and 0 of L, JK = J0K if and only if and 0 are contextually equivalent. Plotkin showed that PCF satisfies soundness and adequacy, but not full abstraction. He also showed that PCF enriched with a so-called parallel or operator had all three properties. Since Plotkin’s seminal work, many papers have studied full abstraction for various forms of languages. Research concentrated for a long time on finding fully abstract models for PCF without parallel or Mil77, Ber79, with relatively complex solutions involving Kripke logical relations OR95, RS02, JT93, and final solutions based on so-called game semantics HO00, AJM00]. In the presence of side-effects (assignments and global stores, input/output for example), the question was studied by OT92, OT95, Red96, OR99 among others. Others have varied the notion of full abstraction LP96, or the notion of model
Mul86, for example.
Objectif :
The purpose of the current proposal is to study the question of full abstraction for languages with choice: probabilistic choice, where we have primitives for drawing data at random, along some predefined distributions, and non-deterministic choice, where the outcome of a choice is not determined by a random draw, but by the decision of a deterministic, external scheduler1. That scheduler may be angelic (we specify the best possible outcomes, and this is related to may-equivalence in operational semantics), or demonic (we specify the worst possible outcomes; this is known as an adversarial setting in security, and is related to
must-equivalence in operational semantics). The proponent already has some partial results Gou15 in the case of PCF plus angelic non-deterministic choice, and in the case of PCF plus both angelic non-deterministic
choice and probabilistic choice. There is no question that the study of languages with some probabilistic features is important. Countless programs use some form of random computation: Monte-Carlo simulation,
efficient primality testing, property testing, etc. The question of non-deterministic choice may seem more intriguing. The demonic case of non-determinism is pretty well suited to modeling some forms of security protocols, where a malicious adversary (the demon) tries to obtain some secret, or to impersonate somebody, or to force you to reveal your vote. One way of defending the program and its data against such a malicious adversary is to use cryptography (which is, at least formally, outside the scope of this proposal, although see the proponent’s previous work GLNZ04), and random generation of nonces, identities, or other important pieces of data.
Productions Scientifiques :
We have defined a version of Paul B. Levy’s call-by-push-value language, with probabilistic choice and demonic non-deterministic choice, and we have showed that, together with a parallel or construct and a statistical termination tester operation, it is indeed fully abstract. The paper was accepted at the LICS’19 conference.
Additional talks on this work: at the seminar of the LACL, May 20th, 2019; at the PPS seminar, June 06th, 2019.
The related paper is a case study where we examine the following situation. The language is a variant of PCF with probabilistic choice only, no non-deterministic choice, and no call-by-push-value trick. That language is not fully abstract, in particular because one cannot define a parallel or primitive, as usual. However, one can define a poor man’s parallel or, which fools the parallel or tester with probability 8/27. We show that this is optimal.
As a side-effect, we have studied so-called LCS-complete spaces, a new class of spaces on which Jones and Plotkin’s probabilistic powerdomain has nice properties. (The probabilistic powerdomain is the space of all continuous valuations, and is the standard way of modeling probabilistic choice in higher-order languages.)
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 DafPUP.
The FAC project is the opportunity to weave stronger links between team VALS and LSV. In this setting, the new ‘GdT topologie’ is a new common seminar on introductory themes of topology, organized roughly in alternation between Cachan and Saclay (but mostly in Cachan for now).
- Thursday, April 11th, LSV library, 11-12am: topologies, convergence, the lattice of open sets of a space.
- Thursday, April 18th, LSV library, 11-12am: distributive lattices and frames, the lattice of open sets is a frame, complete Heyting algebras, completely prime filters and points.
- Friday, May 10th, LSV library, 15-16pm: the space of points of a complete lattice, and its (hull-kernel) topology, examples (video).
- Friday, May 17th, LRI, salle des thèses, 14.30-16pm: alternative presentation of points as meet-prime elements, the standard sobrification, sobriety, the standard sobrification is always sober (video).
- Wednesday, May 29th, LSV library, 11-12am: the topological spaces that we can reconstruct from their lattices of open sets are exactly the sober spaces; examples of sober spaces: Hausdorff spaces, continuous dcpos; every sober space induces a dcpo in its specialization ordering (video).
- Wednesday, June 19th, LSV library, 10.30-11.30am: free objects, the example of free monoids; adjunctions (video).
- Tuesday, July 9th, LRI room 445, 16.00-17pm: sobrification is left adjoint to the inclusion functor from Top into Sob, and the open lattice functor is left adjoint to the point functor between Top and the category of locales.
- Thursday, July 18th, LSV library, 14.00-15pm: logics and Stone duality.
Starting from Session 3, all sessions are available on video. Thanks to Igor Khmelnitsky, Hugues Moretto-Viry, and all the gang!
Publications:
1. Jean Goubault-Larrecq. A Probabilistic and Non-Deterministic Call-by-Push-Value Language. ACM/IEEE Symposium on Logics in Computer Science (LICS’19), 2019.
2. Jean Goubault-Larrecq. Fooling the Parallel Or Tester with Probability 8/27. Accepted. Springer Verlag LNCS.
3. 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.