Operational Subsumption

                              Laurent DAMI

	(Work expanded from a technical abstract published in 
	 ICALP'97, and from a paper submitted to POPL'98).


Usually semantic studies of programming languages aim at capturing
program equivalences. This however is ill-adapted to capture the
notion of extensibility of software promoted by object-oriented
systems.  Throughout its evolution a software fragment may be extended
with new functionalities (e.g. adding functions to a module, adding
methods to an inherited class); then obviously it will not be
equivalent to its former version, but nevertheless can _subsume_ it,
in the sense that it can safely replace it in any program context.

To capture this asymetrical subsumption relation, we develop an 
operational semantics framework based on the observation of runtime 
errors. The fundamental assumptions of this approach are that:

	- errors are essentially different from divergence
	  and are externally observable (typically
	  an error message from the runtime system);

	- errors are unrecoverable.

Then subsumption is defined simply as: a subsumes b (a <= b) iff, for
every context C[-], if C[a] reduces to an error, then C[b] reduces to
an error also. Given the assumptions above, this relation is closely
related to the well-known approximation ordering (based on observation
of convergence), and in many cases obeys to a "context" or "ciu"
theorem, which greatly helps in proving subsumption laws by reducing
the set of contexts to study.

The most direct use of observational subsumption is to establish safe
substitutability in untyped languages. However it is also useful for
an ideal model of types.  Usual subtyping then directly corresponds to
inclusion of ideals. In addition, we can semantically define an other
relation between ideals corresponding to what is called "structural
subtyping" in the literature. Informally, structural subtyping
expresses that a subtype preserves some structure from the supertype;
this intuitively matches common object-oriented practice, and is
useful for introducing more powerful typing rules.  However structural
subtyping so far had no semantic definition, and was handled by
syntactic means (for example in the book of Abadi and Cardelli).  Our
semantic interpretation is based on embedding-projection pairs, very
similar to the familiar notions from domain theory, and therefore
gives a natural explanation of what it means to "preserve structure"
between types.