{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T19:07:26Z","timestamp":1649012846176},"reference-count":31,"publisher":"Cambridge University Press (CUP)","issue":"5","license":[{"start":{"date-parts":[[2008,10,1]],"date-time":"2008-10-01T00:00:00Z","timestamp":1222819200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2008,10]]},"abstract":"<jats:p>A longstanding open problem in lambda calculus is whether there exist continuous models of the untyped lambda calculus whose theory is exactly the \u03bb\u03b2 or the least sensible \u03bb-theory \u210b (which is generated by equating all the unsolvable terms). A related question is whether, given a class of lambda models, there are a minimal \u03bb-theory and a minimal sensible \u03bb-theory represented by it. In this paper, we give a positive answer to this question for the class of graph models <jats:italic>\u00e0 la<\/jats:italic> Plotkin, Scott and Engeler. In particular, we build two graph models whose theories are the set of equations satisfied in, respectively, any graph model and any sensible graph model. We conjecture that the least sensible graph theory, where \u2018graph theory\u2019 means \u2018\u03bb-theory of a graph model\u2019, is equal to \u210b, while in one of the main results of the paper we show the non-existence of a graph model whose equational theory is exactly the \u03bb\u03b2 theory.<\/jats:p><jats:p>Another related question is whether, given a class of lambda models, there is a maximal sensible \u03bb-theory represented by it. In the main result of the paper, we characterise the greatest sensible graph theory as the \u03bb-theory \u212c generated by equating \u03bb-terms with the same B\u00f6hm tree. This result is a consequence of the main technical theorem of the paper, which says that all the equations between solvable \u03bb-terms that have different B\u00f6hm trees fail in every sensible graph model. A further result of the paper is the existence of a continuum of different sensible graph theories strictly included in \u212c.<\/jats:p>","DOI":"10.1017\/s0960129508006683","type":"journal-article","created":{"date-parts":[[2008,7,15]],"date-time":"2008-07-15T04:50:29Z","timestamp":1216097429000},"page":"975-1004","source":"Crossref","is-referenced-by-count":8,"title":["Graph lambda theories"],"prefix":"10.1017","volume":"18","author":[{"given":"ANTONIO","family":"BUCCIARELLI","sequence":"first","affiliation":[]},{"given":"ANTONINO","family":"SALIBRA","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2008,10,1]]},"reference":[{"key":"S0960129508006683_ref29","doi-asserted-by":"publisher","DOI":"10.1145\/772062.772067"},{"key":"S0960129508006683_ref27","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90094-A"},{"key":"S0960129508006683_ref24","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005018121791"},{"key":"S0960129508006683_ref26","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(83)90030-1"},{"key":"S0960129508006683_ref23","unstructured":"Kerth R. (1995) Isomorphisme et \u00e9quivalence \u00e9quationnelle entre mod\u00e8les du \u03bb-calcul, Th\u00e8se, Universit\u00e9 de Paris 7."},{"key":"S0960129508006683_ref30","doi-asserted-by":"crossref","unstructured":"Scott D. S. (1972) Continuous lattices. In: Toposes, Algebraic geometry and Logic. Springer-Verlag Lecture Notes in Mathematics 274.","DOI":"10.1007\/BFb0073967"},{"key":"S0960129508006683_ref5","doi-asserted-by":"publisher","DOI":"10.2307\/2273659"},{"key":"S0960129508006683_ref28","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932509"},{"key":"S0960129508006683_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45138-9_24"},{"key":"S0960129508006683_ref25","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00371-6"},{"key":"S0960129508006683_ref9","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.11.005"},{"key":"S0960129508006683_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90065-T"},{"key":"S0960129508006683_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45446-2_2"},{"key":"S0960129508006683_ref10","first-page":"298","article-title":"Lambda theories of effective lambda models","volume":"4646","author":"Berline","year":"2007","journal-title":"Springer-Verlag Lecture Notes in Computer Science"},{"key":"S0960129508006683_ref16","volume-title":"The calculi of lambda conversion","author":"Church","year":"1941"},{"key":"S0960129508006683_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(92)90040-P"},{"key":"S0960129508006683_ref21","unstructured":"Gouy X. (1995) Etude des th\u00e9ories \u00e9quationnelles et des propri\u00e9t\u00e9s alg\u00e9briques des mod\u00e9les stables du \u03bb-calcul, Th\u00e8se, Universit\u00e9 de Paris 7."},{"key":"S0960129508006683_ref14","volume-title":"19th Annual IEEE Symposium on Logic in Computer Science (LICS 2004)","author":"Bucciarelli","year":"2004"},{"key":"S0960129508006683_ref12","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1991.151638"},{"key":"S0960129508006683_ref15","first-page":"346","article-title":"A set of postulates for the foundation of logic","volume":"2","author":"Church","year":"1933","journal-title":"Annals of Math."},{"key":"S0960129508006683_ref4","volume-title":"The lambda calculus: Its syntax and semantics","author":"Barendregt","year":"1984"},{"key":"S0960129508006683_ref31","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00038-5"},{"key":"S0960129508006683_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037102"},{"key":"S0960129508006683_ref17","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093883253"},{"key":"S0960129508006683_ref8","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005123"},{"key":"S0960129508006683_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-08860-1_7"},{"key":"S0960129508006683_ref20","first-page":"126","article-title":"Uncountable limits and the lambda calculus","volume":"2","author":"Di Gianantonio","year":"1995","journal-title":"Nordic J. Comput."},{"key":"S0960129508006683_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00057-8"},{"key":"S0960129508006683_ref6","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(99)00015-9"},{"key":"S0960129508006683_ref18","first-page":"53","article-title":"Computing with B\u00f6hm trees","volume":"45","author":"David","year":"2001","journal-title":"Fundamenta Informaticae"},{"key":"S0960129508006683_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/S1385-7258(79)80006-2"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129508006683","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,2]],"date-time":"2019-04-02T15:24:02Z","timestamp":1554218642000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129508006683\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,10]]},"references-count":31,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2008,10]]}},"alternative-id":["S0960129508006683"],"URL":"https:\/\/doi.org\/10.1017\/s0960129508006683","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,10]]}}}