Søren Bøgh Lassen
December 1998
This dissertation explores a uniform, relational proof style for operational arguments about program equivalences. It improves and facilitates many previously given proofs, and it is used to establish new proof rules for reasoning about term contexts, recursion, and nondeterminism in higher-order programming languages.
Part I develops an algebra of relations on terms and exploits these relations in operational arguments about contextual equivalence for a typed deterministic functional language. Novel proofs of the basic laws, sequentiality and continuity properties, induction rules, and the CIU Theorem are presented together with new relational proof rules akin to Sangiorgi's ``bisimulation up to context'' for process calculi.
Part II extends the results from the first part to
nondeterministic functional programs. May and must operational semantics and
contextual equivalences are defined and their properties are explored by
means of relational techniques. For must contextual equivalence, the failure
of ordinary syntactic -continuity in the presence of countable
nondeterminism is addressed by a novel transfinite syntactic continuity
principle. The relational techniques are also applied to the study of lower
and upper applicative simulation relations, yielding new results about their
properties in the presence of countable and fair nondeterminism, and about
their relationship with the contextual equivalences
Available as PostScript,
PDF.