Last minute update. This problem was solved, in a call-by-push-value language instead of a variant of PCF: see this arxiv paper.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
There is an incredible amount of papers on subjects of the form: consider a programming language L, with two semantics, one operational (a virtual machine), one denotational (a map ⟦_⟧ from terms of L to elements of certains dcpos), then the two semantics compute (or no not compute) the same thing in the two semantics.
I am going to be extremely vague about certain things, and experts might tell me: shouldn’t the semantics map ⟦_⟧ also take an environment as argument? or similar, true, observations. I will keep away from such questions for the sake of simplicity.
Gordon Plotkin and PCF
One early paper on that subject is Gordon Plotkin’s “LCF considered as a programming language” [1]. This is a remarkable paper, which I recommend to anybody interested in such questions. Gordon is a true genius. Consider that he asked the basic question, and solved it (almost) completely. 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. That is considered solved today, using so-called game semantics.
Thomas Streicher’s book [2] is a very good book on the subject, and I have also learned quite a lot from it.
What does it mean for those two semantics to compute the same thing? The weakest notion is soundness: if the machine terminates on the term ’42’, then its denotational value is 42. More generally, soundness says that denotational semantics is an invariant of computation: if the machine can go from configuration C to configuration C’, then
⟦C⟧=⟦C’⟧. The former is a consequence because, in all reasonable semantics, ⟦’42’⟧=42. PCF, notably, is sound.
A more elaborate notion is adequacy, and that is a kind of converse. That says that if ⟦C⟧=42, then starting from C, your machine will eventually terminate on ’42’. The difficult part is not to show that the end result is ’42’, it is that C will terminate at all. Gordon invented the notion of logical relation for that, explaining that it is inspired from reducibility in the study of the typed lambda-calculus, and proved that PCF is adequate. By the way, adequacy only works at ground types (int, bool), but not at function types. In fact, it does not even make sense to say that if ⟦C⟧=the function that maps every list to a sorted version of that list, then the machine started on C should terminate on some canonical sorting procedure. 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.
Once you have all that, you can look at full abstraction. There is a notion of context, which is in a sence a configuration C with a hole, where you can plug other programs. The result of plugging program M is written C[M]. A nice thing about denotational semantics is that it is compositional, namely that ⟦C[M]⟧ can be defined solely from ⟦C⟧ and from ⟦M⟧; in particular, if ⟦M⟧=⟦N⟧, then ⟦C[M]⟧=⟦C[N]⟧. That has the following consequence: if ⟦M⟧=⟦N⟧, then for every context C returning an object of ground type (int, bool, but not functions for example), then ⟦C[M]⟧=⟦C[N]⟧ hence by adequacy the machine will return the same results when started with C[M] or with C[N]—precisely, if the machine terminates when started with C[M], then it will also terminate when started with C[N], with the same value, and symmetrically. (That they terminate with the same value is not really important. What is important is that they terminate in exactly the same contexts. It will then follow that they must terminate with the same values.)
One says that M and N are observationally equivalent if and only if the machine returns the same results when started with C[M] or with C[N] (in this sense), for every context C of ground type. Hence adequacy implies that two programs with the same denotation semantics are observationally equivalent.
Full abstraction is the converse: a language (or rather, a pair of semantics for that language) is fully abstract if and only if, for every two terms M and N, ⟦M⟧=⟦N⟧ if and only if M and N are observationally equivalent.
Gordon Plotkin showed that PCF is not fully abstract. There is a funny function, among the values of the denotational semantics, called parallel or, 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.
Then Gordon showed that PCF extended with a parallel or operation is fully abstract—by a proof which still seems to be magical but also rather ad hoc to me—and many other things.
PCF with choice
I have been interested in semantics for probabilistic, non-deterministic, and mixed probabilistic and non-deterministic choice, for a long time. 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.
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.
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. In a nutshell: if you just have PCF + angelic non-deterministic choice (modeled through the Hoare powerdomain), then that is fully abstract—period; 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 primitive.
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. Here is what I do in my case. Consider any two terms M and N that do not have the same denotational semantics. Becauses dcpos are T0, there must be an open set U that contains ⟦M⟧ but not ⟦N⟧ (or conversely). We can even take U from a subbase of the topology. Now, contexts C (with unit type) have semantics which are Scott-continuous maps into Sierpiński space S, namely, they denote opens. If you can show that the denotations ⟦C⟧ of contexts with unit type for a subbase for the Scott topology, then ⟦C[M]⟧ will be equal to ⊤ (“in U“) while ⟦C[N]⟧ will be equal to ⊥ (“not in U“). All that has to be verified, of course, and I am only trying to given you a general contour of the proof.
In the end, full abstraction follows from theorems about coincidence of topologies, such as: if X and Y are bc-domains, then the Scott topology on [X → Y] coincides with the topology of pointwise convergence (see [3]).
The paper [3] does much more, and I am sorry that, as a result, it is too long. However, that paper establishes soundness and adequacy for all possible variants of choice, mixed or not, not just the angelic forms.
The proposal
Hence it might seem that full abstraction should be almost free for all the remaining variants. 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) is not fully abstract.
Can you prove that conjecture?
In a second step, you would have to examine the following other conjectures, which I presume have a positive answer:
- Is PCF + demonic choice + parallel or, fully abstract?
- Is PCF + demonic choice + probabilistic choice + statistical termination testers + parallel or, fully abstract?
Once that is done, we can start exploring erratic choice. That should be simple consequences of the angelic and demonic cases.
- Gordon Plotkin. LCF considered as a programming language. Theoretical Computer Science 5(3):223-255, 1977.
- Thomas Streicher. Domain-Theoretic Foundations of Functional Programming.
World Scientific, 132 pages, 2006. - Jean Goubault-Larrecq. Full Abstraction for Non-Deterministic and Probabilistic Extensions of PCF I: the Angelic Cases. Journal of Logic and Algebraic Methods in Programming 84(1):155-184, 2015.
— Jean Goubault-Larrecq (November 8th, 2017