Retour à la page du séminaire

### 14/05/99: John Longley (Edinburgh)

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

**abstract**
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.