{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T12:17:41Z","timestamp":1790079461266,"version":"4.0.1"},"reference-count":38,"publisher":"Society for Industrial & Applied Mathematics (SIAM)","issue":"3","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["SIAM J. Comput."],"published-print":{"date-parts":[[1996,6]]},"abstract":"<jats:p>It is impossible to add a combinator to PCF to achieve full abstraction for models such as Berry\u2019s stable domains in a way analogous to the addition of the \u201cparallel-or\u201d combinator that achieves full abstraction for the familiar complete partial order (cpo) model. In particular, we define a general notion of rewriting system of the kind used for evaluating simply typed $\\lambda $-terms in Scott\u2019s PCF. Any simply typed $\\lambda $-calculus with such a \u201cPCF-like\u201d rewriting semantics is shown necessarily to satisfy Miler\u2019s Context Lemma. A simple argument demonstrates that any denotational semantics that is adequate for PCF, and in which certain simple Boolean functionals exist, cannot be fully abstract for any extension of PCF satisfying the Context Lemma. An immediate corollary is that stable domains cannot be fully abstract for any extension of PCF definable by PCF-like rules.<\/jats:p>","DOI":"10.1137\/s0097539791224212","type":"journal-article","created":{"date-parts":[[2005,2,24]],"date-time":"2005-02-24T06:43:31Z","timestamp":1109227411000},"page":"663-696","source":"Crossref","is-referenced-by-count":9,"title":["Full Abstraction and the Context Lemma"],"prefix":"10.1137","volume":"25","author":[{"given":"Trevor","family":"Jim","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Albert R.","family":"Meyer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"351","published-online":{"date-parts":[[2006,7,13]]},"reference":[{"key":"R1","unstructured":"S. Abramsky,  D. L. Turner,  The lazy lambda calculus,  Research Topics in Functional Programming, Addison-Wesley, Reading, MA,  1989"},{"key":"R2","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90065-T"},{"key":"R3","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57887-0_87"},{"key":"R4","volume-title":"The Lambda Calculus: Its Syntax and Semantics","author":"Barendregt H. P.","year":"1984"},{"key":"R5","first-page":"67","volume-title":"Transformations de programmes (Proc. Third Internat. Sympos. Programming, Paris, 1978)","author":"Berry G.","year":"1978"},{"key":"R6","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-08860-1_7"},{"key":"R7","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(82)80002-9"},{"key":"R8","first-page":"35","volume-title":"Algebraic methods in semantics (Fontainebleau, 1982)","author":"Berry G.","year":"1985"},{"key":"R9","first-page":"89","volume-title":"Algebraic methods in semantics (Fontainebleau, 1982)","author":"Berry G.","year":"1985"},{"key":"R10","doi-asserted-by":"crossref","unstructured":"B. Bloom,  Can LCF be topped? Flat lattice models of typed lambda calculus (preliminary report),  3rd Annual Symposium on Logic in Computer Science [22], IEEE Press, Piscataway, NJ,  1988,  282\u2013295","DOI":"10.1109\/LICS.1988.5127"},{"key":"R11","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90064-O"},{"key":"R12","doi-asserted-by":"publisher","DOI":"10.1145\/200836.200876"},{"key":"R13","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-54233-7_123"},{"key":"R14","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1033"},{"key":"R15","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1047"},{"key":"R16","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0317-9"},{"key":"R17","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(86)90044-7"},{"key":"R18","volume-title":"Introduction to combinators and \u03bb-calculus","author":"Hindley J. Roger","year":"1986"},{"key":"R19","doi-asserted-by":"crossref","unstructured":"D. J. Howe,  Equality in lazy computation systems,  Proc. 4th Annual Symposium on Logic in Computer Science, IEEE Press, Piscataway, NJ,  1989,  198\u2013203 0716.68065","DOI":"10.1109\/LICS.1989.39174"},{"key":"R20","unstructured":"G. Huet, J.J. L\u00e9vy,  Computations in nonambiguous term rewriting systems, Tech. Report, 359, INRIA, Rocquencourt, France,  1979"},{"key":"R21","doi-asserted-by":"crossref","unstructured":"J. Hyland, C.H. Ong,  Pi-calculus, dialogue games and PCF,  Conference Record of FPCA '95: Conference on Functional Programming Languages and Computer Architecture, Association for Computing Machinery, New York,  1995,  96\u2013107","DOI":"10.1145\/224164.224189"},{"key":"R22","unstructured":"3rd Annual Symposium on Logic in Computer Science, IEEE Press, Piscataway, NJ,  1988"},{"key":"R23","unstructured":"T. Jim, A. R. Meyer,  Communication in the TYPES electronic forum,  1989, June 17"},{"key":"R24","volume-title":"Combinatory reduction systems","author":"Klop J. W.","year":"1980"},{"key":"R25","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0035784"},{"key":"R26","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(82)80087-9"},{"key":"R27","doi-asserted-by":"crossref","unstructured":"A. R. Meyer,  Semantical paradigms: Notes for an invited lecture, with two appendices by Stavros Cosmadakis,  3rd Annual Symposium on Logic in Computer Science [22], IEEE Press, Piscataway, NJ,  236\u2013253","DOI":"10.1109\/LICS.1988.5123"},{"key":"R28","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90053-6"},{"key":"R29","unstructured":"K. Mulmuley, Masters Thesis,  Full Abstraction and Semantic Equivalence, ACM Doctoral Dissertation Award, 1986, MIT Press,  1987"},{"key":"R30","unstructured":"C.H. L. Ong, Ph.D. Thesis,  The lazy lambda calculus: An investigation into the foundations of functional programming, Imperial College, University of London, London,  1988"},{"key":"R31","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"R32","doi-asserted-by":"publisher","DOI":"10.1007\/BF01876321"},{"key":"R33","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0073967"},{"key":"R34","doi-asserted-by":"publisher","DOI":"10.1137\/0205037"},{"key":"R35","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90095-B"},{"key":"R36","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55511-0_3"},{"key":"R37","volume-title":"Fully abstract models of programming languages","author":"Stoughton Allen","year":"1988"},{"key":"R38","doi-asserted-by":"crossref","unstructured":"C. Talcott,  Programming and proving with function and control abstractions, Tech. Report, STAN-CS-89-1288, Stanford University, Stanford, CA,  1988","DOI":"10.21236\/ADA324006"}],"container-title":["SIAM Journal on Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/epubs.siam.org\/doi\/pdf\/10.1137\/S0097539791224212","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,21]],"date-time":"2026-08-21T18:16:19Z","timestamp":1787336179000},"score":1,"resource":{"primary":{"URL":"https:\/\/epubs.siam.org\/doi\/10.1137\/S0097539791224212"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,6]]},"references-count":38,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1996,6]]}},"alternative-id":["10.1137\/S0097539791224212"],"URL":"https:\/\/doi.org\/10.1137\/s0097539791224212","relation":{},"ISSN":["0097-5397","1095-7111"],"issn-type":[{"value":"0097-5397","type":"print"},{"value":"1095-7111","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,6]]}}}