University of Cambridge

Logic
&
Semantics

The Sequentially Realizable Functionals
or
When is a functional program not a functional program?

By John Longley (23rd September 1998)

I will start with a rather surprising observation: there are simply-typed ML programs whose observable behaviour is completely "functional" (in the sense that they give equal outputs for equal inputs), but the functions they compute cannot be written in the purely functional fragment of ML. An example is the function F : ((unit->unit)->unit)->bool specified by:

F g = true if forall x. g x = ()
F g = false if forall x. g x = x()
F g diverges if forall x. g x diverges.
This function can be implemented using exceptions, or using references, but not in pure functional ML.

This observation leads to the discovery of a class of "sequential" functions of finite type, strictly larger than the more familiar class of "PCF-sequential" functionals. We call this the class of *sequentially realizable* (or SR) functionals; intuitively, they include the above functional F and "all things like it". It turns out that the SR functionals have very good theoretical status, e.g. in that they admit a large number of independent (semantic and syntactic) characterizations. For example, the "full" SR functionals coincide exactly with the *strongly stable* functionals of Bucciarelli and Ehrhard.

I will introduce the class of SR functionals and survey the various characterizations of them. One striking new result is the existence of a "universal" SR functional H, from which all other effective SR functionals can be defined in PCF. I will also discuss the possibility, and potential advantages, of a programming language that incorporated the power of the SR functionals into its pure functional fragment.

More information can be gleaned from the Draft paper (incomplete!) accessible from my home page.

LS Home page or Talks in 1998/99