[Prev][Next][Index][Thread]

relative definability




[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

The paper

A relative PCF-definability result for strongly stable functions
and some corollaries

is available by anonymous ftp on the site
iml.univ-mrs.fr /pub/ehrhard/rel.[dvi,ps].Z

\begin{abstract}
We prove that, in the hierarchy of simple Curry types based on
the type of natural numbers, any finite strongly stable function is equal
to the application of the semantics of a PCF-definable functional
to some strongly stable (generally not PCF-definable)
functionals of type two. Applying a logical relations technique, we derive
from this result
that the strongly stable model of PCF is the extensional collapse
of its sequential algorithms model.
\end{abstract}