Equationally fully abstract models of PCF

In Plotkin's applied typed lambda calculus PCF [Plo] it is natural to consider one term operationally less defined than another iff whenever the first term converges to a constant in a ground context, then the second term converges to the same constant in that context. Two terms are considered operationally equivalent iff each is less defined than the other, i.e., they have the same behaviour in all ground contexts. Terms are thus equivalent when they are interchangeable in complete programs. See [Mey] and [Sto] for detailed discussions of these concepts.

Over a decade ago, Robin Milner showed the existence of a unique order-extension al model of PCF that is inequationally fully abstract in the sense that one term is operationally less defined than another exactly when the meaning of the first is less than that of the second in the model [Mil]. (Models that consist of functions are called extensional; when in addition these functions are ordered pointwise, the models are called order-extensional.) Milner constructed this model using term model techniques, and considerable effort has been expended in attempts to synthesize his model in a more natural or semantic way; see [BerCurLév] for a survey of this work.

In practice, term equivalence is probably of greater interest than term ordering , and this suggests that one consider models that are equationally fully abstract in the sense t hat two terms are operationally equivalent exactly when they are mapped to the same semantic value . Milner's inequationally fully abstract model is clearly equationally fully abstract, and it is natural to ask whether there exist equationally fully abstract models that are not inequationally fully abstract. The purpose of this paper is to answer this question in the affirmative, and to begin the study of the category E of extensional, equationally fully abstract models and structure-preserving functions.

The paper's main results are as follows:

(i)

E is a pre-ordering with arbitrary products and coproducts and whose initial a nd terminal objects are not isomorphic.

(ii)

All objects of E are strongly algebraic (SFP) and all isolated elements of these models are definable by terms.

(iii)

There is a morphism from an object A to an object B of E iff B relates at least as many pairs of terms as does A (i.e., if the meaning of M is less than that of N in A, then the meaning of M is less than that of N in B)

(iv)

Objects of E that relate the same pairs of terms are isomorphic.

(v)

The initial object of E is also initial in the category of (not necessarily ex tensional) equationally fully abstract models.

(vi)

The terminal object of E is order-extensional and inequationally fully abstract, i.e., is Milner's original model

[BerCurLév]

G. Berry, P.-L. Curien and J.-J. L'eevy. Full abstraction for sequential languages: the state of the art. In M. Nivat and J. Reynolds (editors), Algebraic Methods in Semantics, Cambridge University Press, 1985.

[Mey]

A. Meyer and S. Cosmadakis. Semantical paradigms: notes for an invited lecture. Proc. 3rd LICS, 1988.

[Plo]

G. Plotkin. LCF considered as a programming language. Theoretical Computer Science 5, 1977.

[Sto]

A. Stoughton. Fully Abstract Models of Programming Languages. Research Notes in Theoretical Computer Science, Pitman/Wiley, 1988.