{"id":1310,"date":"2017-11-08T12:28:28","date_gmt":"2017-11-08T11:28:28","guid":{"rendered":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/?page_id=1310"},"modified":"2022-11-19T15:20:22","modified_gmt":"2022-11-19T14:20:22","slug":"full-abstraction-for-languages-with-demonic-and-probabilistic-choice","status":"publish","type":"page","link":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/?page_id=1310","title":{"rendered":"Full Abstraction for Languages with Demonic and Probabilistic Choice"},"content":{"rendered":"

Last minute update.<\/strong>\u00a0 This problem was solved, in a call-by-push-value language instead of a variant of PCF: see this arxiv paper<\/a>.<\/p>\n

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~<\/p>\n

There is an incredible amount of papers on subjects of the form: consider a programming language L<\/strong>, with two semantics, one operational (a virtual machine), one denotational (a map \u27e6_\u27e7 from terms of L<\/strong> to elements of certains dcpos), then the two semantics compute (or no not compute) the same thing in the two semantics.<\/p>\n

I am going to be extremely vague about certain things, and experts might tell me: shouldn’t the semantics map \u27e6_\u27e7 also take an environment as argument? or similar, true, observations.\u00a0 I will keep away from such questions for the sake of simplicity.<\/p>\n

Gordon Plotkin and PCF<\/h2>\n

One early paper on that subject is Gordon Plotkin’s “LCF considered as a programming language” [1].\u00a0 This is a remarkable paper, which I recommend to anybody interested in such questions.\u00a0 Gordon is a true genius.\u00a0 Consider that he asked the basic question, and solved it (almost) completely.\u00a0 The only question that he left open is whether LCF (or, as we call it today, the language PCF) has a, necessarily different, fully abstract denotational semantics.\u00a0 That is considered solved today, using so-called game semantics.<\/p>\n

Thomas Streicher’s book [2] is a very good book on the subject, and I have also learned quite a lot from it.<\/p>\n

What does it mean for those two semantics to compute the same thing?\u00a0 The weakest notion is soundness<\/em>: if the machine terminates on the term ’42’, then its denotational value is 42.\u00a0 More generally, soundness says that denotational semantics is an invariant of computation: if the machine can go from configuration C<\/em> to configuration C’<\/em>, then
\n\u27e6C<\/em>\u27e7=\u27e6C’<\/em>\u27e7.\u00a0 The former is a consequence because, in all reasonable semantics, \u27e6’42’\u27e7=42.\u00a0 PCF, notably, is sound.<\/p>\n

A more elaborate notion is adequacy<\/em>, and that is a kind of converse.\u00a0 That says that if \u27e6C<\/em>\u27e7=42, then starting from C<\/em>, your machine will eventually terminate on ’42’.\u00a0 The difficult part is not to show that the end result is ’42’, it is that C<\/em> will terminate at all.\u00a0 Gordon invented the notion of logical relation<\/em> for that, explaining that it is inspired from reducibility in the study of the typed lambda-calculus, and proved that PCF is adequate.\u00a0 By the way, adequacy only works at ground types (int, bool), but not at function types.\u00a0 In fact, it does not even make sense to say that if \u27e6C<\/em>\u27e7=the function that maps every list to a sorted version of that list, then the machine started on C<\/em> should terminate on some canonical sorting procedure.\u00a0 That is all the more absurd as there are many sorting procedures (bubble sort, insertion sort, radix sort, merge sort, quick sort, quicker sort, etc.), and none is more canonical than the others.<\/p>\n

Once you have all that, you can look at full abstraction<\/em>.\u00a0 There is a notion of context, which is in a sence a configuration C<\/em> with a hole, where you can plug other programs.\u00a0 The result of plugging program M<\/em> is written C<\/em>[M<\/em>].\u00a0 A nice thing about denotational semantics is that it is compositional, namely that \u27e6C<\/em>[M<\/em>]\u27e7 can be defined solely from \u27e6C<\/em>\u27e7 and from \u27e6M<\/em>\u27e7; in particular, if \u27e6M<\/em>\u27e7=\u27e6N<\/em>\u27e7, then\u00a0\u27e6C<\/em>[M<\/em>]\u27e7=\u27e6C<\/em>[N<\/em>]\u27e7. That has the following consequence: if \u27e6M<\/em>\u27e7=\u27e6N<\/em>\u27e7, then for every context C<\/em> returning an object of ground type (int, bool, but not functions for example), then \u27e6C<\/em>[M<\/em>]\u27e7=\u27e6C<\/em>[N<\/em>]\u27e7 hence by adequacy the machine will return the same results when started with C<\/em>[M<\/em>] or with C<\/em>[N<\/em>]\u2014precisely, if the machine terminates when started with C<\/em>[M<\/em>], then it will also terminate when started with C<\/em>[N<\/em>], with the same value, and symmetrically.\u00a0 (That they terminate with the same value is not really important.\u00a0 What is important is that they terminate in exactly the same contexts.\u00a0 It will then follow that they must terminate with the same values.)<\/p>\n

One says that M<\/em> and N<\/em> are observationally equivalent<\/em> if and only if the machine returns the same results when started with C<\/em>[M<\/em>] or with C<\/em>[N<\/em>] (in this sense), for every context C<\/em> of ground type.\u00a0 Hence adequacy implies that two programs with the same denotation semantics are observationally equivalent.<\/p>\n

Full abstraction is the converse: a language (or rather, a pair of semantics for that language) is fully abstract<\/em> if and only if, for every two terms M<\/em> and N<\/em>, \u27e6M<\/em>\u27e7=\u27e6N<\/em>\u27e7 if and only if M<\/em> and N<\/em> are observationally equivalent.<\/p>\n

Gordon Plotkin showed that PCF is not<\/em> fully abstract.\u00a0 There is a funny function, among the values of the denotational semantics, called parallel or<\/em>, which cannot be defined in PCF, and that is the source of several oddities, which culminate in two PCF programs that are observationally equivalent, although they have different semantics.<\/p>\n

Then Gordon showed that PCF extended with a parallel or operation is<\/em> fully abstract\u2014by a proof which still seems to be magical but also rather ad hoc to me\u2014and many other things.<\/p>\n

PCF with choice<\/h2>\n

I have been interested in semantics for probabilistic, non-deterministic, and mixed probabilistic and non-deterministic choice, for a long time.\u00a0 The long-term goal of my papers on the subject was to apply that to full abstraction results of languages based on PCF, with various forms of choice as above.<\/p>\n

I have finally presented my findings at the Domains XI workshop (Gordon was uttely uninterested, too bad), then at Pierre-Louis Curien’s Festschrift in Venice, Italy (Gordon was absent, and later reiterated his total absence of interest), but that would not stop me.<\/p>\n

I published most of what I could do in a special issue of the Domains XI workshop [3], and that somehow rounds up everything that can be said in case non-determinism is angelic.\u00a0 In a nutshell: if you just have PCF + angelic non-deterministic choice (modeled through the Hoare powerdomain<\/a>), then that is fully abstract\u2014period; and PCF + probabilistic + angelic non-deterministic choice is not fully abstract, but becomes fully abstract if you add what I call a statistical termination tester<\/em> primitive.<\/p>\n

The interesting thing is that my proofs of full abstraction are, in my opinion, simpler than Gordon’s (although the two kinds of proofs do not apply to the same languages), or at least rest on clearer topological facts.\u00a0 Here is what I do in my case.\u00a0 Consider any two terms M<\/em> and N<\/em> that do not have the same denotational semantics.\u00a0 Becauses dcpos are T0<\/sub>, there must be an open set U<\/em> that contains \u27e6M<\/em>\u27e7 but not \u27e6N<\/em>\u27e7 (or conversely).\u00a0 We can even take U<\/em> from a subbase of the topology.\u00a0 Now, contexts C<\/em> (with unit type) have semantics which are Scott-continuous maps into Sierpi\u0144ski space S<\/strong>, namely, they denote opens.\u00a0 If you can show that the denotations \u27e6C<\/em>\u27e7 of contexts with unit type for a subbase for the Scott topology, then \u27e6C[M<\/em>]\u27e7 will be equal to \u22a4 (“in U<\/em>“) while\u00a0\u27e6C[N]\u27e7 will be equal to \u22a5 (“not in U<\/em>“).\u00a0 All that has to be verified, of course, and I am only trying to given you a general contour of the proof.<\/p>\n

In the end, full abstraction follows from theorems about coincidence of topologies, such as: if X<\/em> and Y<\/em> are bc-domains, then the Scott topology on [X<\/em> \u2192 Y<\/em>] coincides with the topology of pointwise convergence (see [3]).<\/p>\n

The paper [3] does much more, and I am sorry that, as a result, it is too long.\u00a0 However, that paper establishes soundness and adequacy for all possible variants of choice, mixed or not, not just the angelic forms.<\/p>\n

The proposal<\/h2>\n

Hence it might seem that full abstraction should be almost free for all the remaining variants.\u00a0 That is not true, and I strongly suspect that PCF + demonic choice (i.e., with the Smyth powerdomain, see Proposition 8.3.25 in the book<\/a>) is not fully abstract.<\/p>\n

Can you prove that conjecture?<\/p>\n

In a second step, you would have to examine the following other conjectures, which I presume have a positive answer:<\/p>\n