{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:39:39Z","timestamp":1753889979659,"version":"3.41.2"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,10,12]],"date-time":"2012-10-12T00:00:00Z","timestamp":1350000000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>PCF is a sequential simply typed lambda calculus language. There is a unique\norder-extensional fully abstract cpo model of PCF, built up from equivalence\nclasses of terms. In 1979, G\\'erard Berry defined the stable order in this\nmodel and proved that the extensional and the stable order together form a\nbicpo. He made the following two conjectures: 1) \"Extensional and stable order\nform not only a bicpo, but a bidomain.\" We refute this conjecture by showing\nthat the stable order is not bounded complete, already for finitary PCF of\nsecond-order types. 2) \"The stable order of the model has the syntactic order\nas its image: If a is less than b in the stable order of the model, for finite\na and b, then there are normal form terms A and B with the semantics a, resp.\nb, such that A is less than B in the syntactic order.\" We give counter-examples\nto this conjecture, again in finitary PCF of second-order types, and also\nrefute an improved conjecture: There seems to be no simple syntactic\ncharacterization of the stable order. But we show that Berry's conjecture is\ntrue for unary PCF. For the preliminaries, we explain the basic fully abstract\nsemantics of PCF in the general setting of (not-necessarily complete) partial\norder models (f-models.) And we restrict the syntax to \"game terms\", with a\ngraphical representation.<\/jats:p>","DOI":"10.2168\/lmcs-8(4:7)2012","type":"journal-article","created":{"date-parts":[[2013,11,29]],"date-time":"2013-11-29T13:21:33Z","timestamp":1385731293000},"source":"Crossref","is-referenced-by-count":0,"title":["On Berry's conjectures about the stable order in PCF"],"prefix":"10.46298","volume":"Volume 8, Issue 4","author":[{"given":"Fritz","family":"M\u00fcller","sequence":"first","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,10,12]]},"reference":[{"key":"668:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/925\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/925\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:59:08Z","timestamp":1681243148000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/925"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,10,12]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(4:7)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1108.0556","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1108.0556","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,10,12]]},"article-number":"925"}}