The (Algebraic) Congruence of Two Programming Language Definitions
Clem Baker-Finch. In Science of Computer Programming, 4, 1990, pages 81-96.
Since the beginning of the development of Scott-Strachey denotational
semantics, one of the most useful formal results required by
practitioners has been the congruence of dissimilar definitions of the
semantics of some programming languages. While appropriate techniques
are well-established, such proofs are undeniably difficult especially
for the common case where one definition is operational and the other
is denotational. In this paper we demonstrate an alternative proof
technique that we believe is much simpler and more direct for cases
involving an operational semantics. We proceed by reworking the
example presented by Stoy in "The Congruence of Two Programming
Language Definitions." Our approach is fundamentally algebraic and
depends on a slightly different (we believe more appropriate)
foundation of operational semantics.
to obtain a paper copy.