I got told a while ago that Streicher's "sequential" domains had solved the full abstraction problem for PCF [1] ... was it that or something else that killed off the work on game semantics?
It seems that Jon Sterling, author of the tool used to express the thoughts at the link, has made recent progress in domain theory [2] but perhaps the "synthetic" qualifier means it's not the real thing?
[1] Streicher's notes/book on domain theory sketches the construction but does not take it anywhere; I wonder what the reasoning principles are.
[2] see e.g. https://www.jonmsterling.com/jms-0064/index.xml
The full abstraction for PCF was solved in the mid 1990s by Abramsky/Jagadeesan/Malacaria [1] Hyland/Ong [2] and Nickau [3]. All three appeared simultaneously. This was a paradigm shift, because all three used used interactive rather than functional models of computation. (There was also later work on domain theoretic full abstraction, e.g. OHearn and Riecke [4], but I can't recall details. Maybe Streicher's work was in this direction?) The beauty of interative models like games is that they can naturally encode more complex behaviour, including parallelism.
[1] S. Abramsky, R. Jagadeesan, P. Malacaria, Full Abstraction for PCF.
[2] J.M. E. Hyland, C.-H. L. Ong, On Full Abstraction for PCF: I, II, and III.
[3] H. Nickau, Hereditarily sequential functionals.
[4] P. O'Hearn, J. G. Riecke, Kripke logical relations and PCF.
Game semantics is expressive but AFAIK it has not (yet) provided new tools for reasoning about programs. I wonder why those tools have (apparently) not been developed, or do they just add (not very useful?) information to the old LCF story ala Scott? Has its moment passed?
By parallelism I think you mean concurrency. (Scott's domains have a bit too much parallelism as shown by Plotkin in his classic paper on LCF; these are at the root of the failure of Scott's models to be fully abstract.) And Scott's big idea -- that computation aligns with his notion of continuity -- conflicts with fairness which is essential for showing liveness. For this reason I never saw the point in powerdomains, excepting the Hoare (safety) powerdomain.
As these notes show, models, even adequate models, are a dime a dozen. It's formulating adequate reasoning principles that is tough. And that's what Andy Pitts brought to classic domain theory in the 1990s.
dunham•8mo ago
His motivation for building it is described here: https://www.forester-notes.org/tfmt-0001/index.xml