Full Abstraction for PCF
and Related Languages
This document is also available as PostScript, DVI.
To conclude the Workshop on Full Abstraction of PCF and Related Languages we had a discussion on open problems, led by Samson Abramsky. These notes, taken by Glynn Winskel, catch the state of the blackboard during that discussion.
(1) Can the fully abstract model for finitary PCF be effectively presented?
(1') Can the fully abstract model for PCF be effectively presented?
Notes: (1) (1'), while (1') (1) remains to be checked.
The following are questions analogous to those settled by Ralph Loader in showing the ``Plotkin-Statman conjecture'' to be false. Recall the ``P-S conjecture''.
(2'') Is definability w.r.t. the simply typed -calculus for the full type hierarchy over a finite set decidable?
Notes: Loader answered ``No'' to (2'') by showing relative definability, an equivalent question, to be undecidable. This implies the technique of logical relations to be incomplete at rank .
(2) Is definability w.r.t. finitary PCF in the full monotone hierarchy over Bool (with ) decidable?
(2') Is the definability w.r.t. PCF of finite (compact) elements in the continuous hierarchy over Bool (with ) decidable?
3(i) (1) and 3(ii) (2).
For instance, assuming 3(ii), given a type we can work our way along an enumeration of finitary-PCF terms till we have obtained as many distinct functions as given by the algorithm for 3(iii), and thus obtain (2).
(4) Is the relation of Bucciarelli recursive w.r.t. finitary PCF?
One can ask the questions asked of finitary PCF for the variant where instead of beginning the hierarchy as booleans with , one begins with Sierpinski space .
Are there analogues of Loader's result for the -calculus?