A note on logical relations between semantics and syntax

Abstract

This note gives a new proof of the 'operational extensionality' property of Abramsky's lazy lambda calculus-namely the coincidence of contextual equivalence with a co-inductively defined notion of 'applicative bisimilarity'. This purely syntactic results is here proved using a logical relation (due to Plotkin) between the syntax and its denotational semantics. The proof exploits a mixed inductive/coinductive characterisation of the logical relation recently discovered by the author. Keywords: denotational semantics, logical relation, lambda calculus, contextual equivalence