Reasoning about sequential functions via logical relations
Kurt Sieber · Cambridge University Press eBooks · 1992
Introduction In his seminal paper [Plo77], Plotkin introduced the functional language PCF (‘programming language for computable functions’) together with the standard denotational model of cpo's and continuous functions. He proved that this model is computationally adequate for PCF, but not fully abstract. In order to obtain full abstraction he extended PCF by a parallel conditional operator. The problem with this operator is, that it changes the nature of the language. All computations in the original language PCF can be executed sequentially, but the new operator requires expressions to be evaluated in parallel. Here we address the problem of full abstraction for the original sequential language PCF, i. e. instead of extending the language we try to improve the model. Our approach is to cut down the standard model with the aid of certain logical relations, which we call sequentiality relations . We give a semantic characterization of these relations and illustrate how they can be used to reason about sequential (i. e. PCF-definable) functions. Finally we prove that this style of reasoning is ‘complete’ for proving observational congruences between closed PCF-expressions of order ≤ 3. Technically, this completeness can be expressed as a full abstraction result for the sublanguage which consists of these expressions. Sequential PCF In [Plo77], PCF is defined as a simply typed λ-calculus over the ground types ι (of integers) and o (of Booleans).