Problems

Full Abstraction for PCF
and Related Languages

This document is also available as PostScript, DVI.

Contents

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.

Effectiveness

Finitary PCF

(1) Can the fully abstract model for finitary PCF be effectively presented?

PCF

(1') Can the fully abstract model for PCF be effectively presented?

Notes: (1) (1'), while (1') (1) remains to be checked.

Definability

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 .

Finitary PCF

(2) Is definability w.r.t. finitary PCF in the full monotone hierarchy over Bool (with ) decidable?

PCF

(2') Is the definability w.r.t. PCF of finite (compact) elements in the continuous hierarchy over Bool (with ) decidable?

Notes:

  1. In the case of finitary PCF, it is sufficient to restrict the language to exclude fixed point operations, but include , and conditional.
  2. (2) (1): Assuming (2) we can pick out the definable elements, and preorder them pointwise by how they act on definable elements of lower type. This is effective and yields an effectively presented domain on quotienting.
  3. For (2') it suffices to restrict attention to finite terms of PCF where we exclude Y from the language and include .
  4. (2') (1'): Use the finite terms of PCF to give an enumeration and effective presentation for the fully abstract model, quotienting as in (ii). (1') (2').

Counting Problems

Finitary PCF

(3)

  1. (Counting problem corresponding to (1))
    Is there a recursive function from types to the number of elements in the fully abstract model?
  2. (Counting problem corresponding to (2))
    Is there a recursive function from types to the number of definable elements in the monotone hierarchy?

Notes:

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).

Degrees of Parallelism

Finitary PCF

(4) Is the relation of Bucciarelli recursive w.r.t. finitary PCF?

Notes:

(2) (4).

Related questions:

Very-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 .

-calculus

lambda-Omega-calculus

Are there analogues of Loader's result for the -calculus?

[BRICS symbol] BRICS WWW home page