Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
@ARTICLE{PittsAM:notlrb, AUTHOR={A.~M.~Pitts}, TITLE={A Note on Logical Relations Between Semantics and Syntax}, JOURNAL={Logic Journal of the Interest Group in Pure and Applied Logics}, VOLUME=5, NUMBER=4, MONTH=jul, PAGES={589--601}, YEAR=1997, 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 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 {\em 3rd Workshop on Logic, Language, Information and Computation\/} ({\em WoLLIC'96\/}), May 8--10, Salvador (Bahia), Brazil, organised by UFPE and UFBA, sponsored by IGPL, FoLLI, and ASL.)} }