The Equivalence of Two Semantic Definitions: A Case Study in LCF
Avra Cohn · SIAM Journal on Computing · 1983
We present a case study in LCF of the equivalence of two semantic definitions for a small language. The language contains recursive and nonrecursive procedure declarations, and static binding of variables is intended. A standard semantics is proved equivalent to a closure semantics in which procedures denote closures (textual objects). This proof is discussed abstractly in [1]. A similar equivalence is proved by J. Stoy in [6, Chap. 13], based on work by R. Milne and C. Strachey [4]. We describe the formalization of the problem in LCF, the informal proof by structural induction over programs of the language, and the strategy for performing the proof mechanically. The strategy is quite general even though it involves rather subtle handling of lemmas and induction hypotheses. A basic understanding of Scott’s theory of domains is assumed, including the least fixed point operator and domain constructing operations such as domain equations.