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 between the syntax and its denotational semantics. The proof exploits a mixed inductive/coinductive characterisation of the logical relation recently discovered by the author