Full abstraction and limiting completeness in equational languages

AbstractThis paper introduces a notion of full abstraction for equational languages under which each language has a unique fully abstract model which can also be characterized as the final object in a category of coherent computable models for the language. We describe two potentially different approaches to limiting completeness with respect to the fully abstract model—a traditional one based on normal forms and a new one based on the usable data content of terms. The former is used to prove limiting completeness for the language of regular systems [5] which includes as subsets and restrictions the equational parts of many other languages. The latter is used to define an abstract version of limiting completeness based on information systems [17] which allows us to derive a set of sufficient conditions for an equational language to be limiting complete for its fully abstract semantics. We discuss cases where the two notions coincide—as they do for regular systems—and cases where they do not. We believe that limiting completeness based on observable data content accurately reflects programming intuition. If this thesis is accepted, the appropriateness of the corresponding definition of approximant can be seen as a design principle to test the mutual suitability of the parameters defining a language