On Proving Limiting Completeness

We give two proofs of Wadsworth's classic approximation theorem for the pure A-calculus. One of these illustrates a new method utilising a certain kind of intermediate semantics for proving correspondences between denotational and operational semantics. The other illustrates a direct technique of Milne, employing recursively-specified inclusive relations. 1. Introduction. Suppose that we have both a (standard) denotational semantics and an operational semantics for some programming language. (For examples see (Stol), (Mil2), (deB).) We would like to prove that they are equivalent, in that the output given by the operational semantics, for each program and input, corresponds exactly to the output specified by the denotational semantics. Thus not only is the former to be consistent with the latter, but also it is to be complete. For diverging computations, completeness is only required "in the limit": the (perhaps partial) outputs given by finite computations of the operational semantics are to converge to the full output specified by the denotational semantics. Following (Wad), we shall refer to this property as limiting completeness. In (Wad), Wadsworth studied the A-calculus, considering arbitrary A-terms as programs. (including their "input"). The "approximate normal forms" of terms, obtained by finite sequences of//-reductions (followed by the replacement ofremaining fl-redexes by a special constant symbol (l that denoted _L), were regarded as outputs. The classic Approximation Theorem (Wad, Thm. 5.2) shows that the denotations of the approximate normal forms of a term do indeed converge to the denotation of the term itself. Thus the theory ofr-conversion, although tooweak forproving all equations between terms whose denotations are equal, is complete in this limiting sense, and adequate for the evaluation of A-terms. I.n general, it is quite easy to prove consistency, using structural induction. See (Stol), (deB) for some examples. We shall not consider consistency proofs any further in this paper. Sometimes, it is also possible to prove limiting completeness quite directly using structural induction with subsidiary appeal to fixpoint induction for recursive constructs such as loops (where structural induction fails). However, when the program- ming languages concerned allow self-applicationmeither explicitly as with Algol 60 procedures, or implicitly as with dynamic bindings in LISPnthen the direct method seems to be precluded, for structural induction fails but there is no obvious recursive construct in the language where fixed-point methods could be applied. In such cases, the domains of denotations are defined reflexively (that is, recursively), and what one wants is to use induction on the level of the projective approximations of the domains. Wadsworth solved this problem in his study of the A-calculus (Wad) by labelling expressions M (and their subexpressions) with integers n, so that M n) denoted the nth projection of the denotation of M. Having introduced some extra syntax to make