On Proving Limited Completeness

Abstract

We give proofs of Wadsworth's classic Approximation Theorem for the pure lambda-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.