Allen Stoughton
In Michael Main, Austin Melton, Michael Mislove, and David Schmidt, editors, Mathematical Foundations of Programming Semantics: 5th International Conference (Tulane University, New Orleans, Louisiana, 1989, March/April), number 442 in Lecture Notes in Computer Science, pages 271--283, Berlin, 1990. Springer-Verlag
Available as PostScript.
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: