An Inductive Definition of Fully Abstract Models for PCF and PCF+OR
A construction of fully abstract models for PCF and PCF^+ = PCF +
parallel conditional function OR is presented on the base of quite
general notions of sequential computational strategies and wittingly
consistent non-deterministic strategies, respectively, introduced by
the author in the seventies. This definition is given level-by-level
of the finite type hierarchy and is an alternative and, in a sense, an
analog to a later game semantics approaches of S. Abramsky,
R. Jagadeesan, and P. Malacaria; J. M. E. Hyland and C.-H. L. Ong; and
H. Nickau.
The main novelty is a straightforward level-by-level construction of
these models consisting only of functionals (hereditarily) computable
by the above mentioned computational strategies. This construction
does not involve any quotient by an equivalence relation like in game
semantics, although correctness proof does involve it.
In both cases of PCF and PCF^+ there are definable universal
(surjective) functionals U_alpha and U^+_alpha of the type (int ->
int) -> alpha. The very possibility of construction of such kind a
model for PCF^+ (of functionals computable by wittingly consistent
strategies) may serve as an answer to an informal question of
J. Longley and G. Plotkin. Also, in the second case of PCF^+ it is
easily demonstrated that the model is monotonic, but not
omega-continuous. Thus, by analogy, continuity of such fully abstract
model (with universal functionals) for pure PCF can be hardly
expected.