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 result is here proved using a logical
relation (due to Plotkin) between the syntax and its denotational
semantics. The proof exploits a mixed inductive/co-inductive
characterisation of the logical relation recently discovered by the author.
(Full version of an invited paper presented at the *3rd Workshop on
Logic, Language, Information and Computation* (WoLLIC'96), May 8--10,
Salvador (Bahia), Brazil, organised by UFPE and UFBA, sponsored by IGPL,
FoLLI, and ASL.)