{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:21:56Z","timestamp":1776316916019,"version":"3.50.1"},"reference-count":31,"publisher":"Oxford University Press (OUP)","issue":"5","license":[{"start":{"date-parts":[[2019,7,11]],"date-time":"2019-07-11T00:00:00Z","timestamp":1562803200000},"content-version":"vor","delay-in-days":1,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019,9,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:sec><jats:title\/><jats:p>The ${\\lambda }$-calculus enjoys the property that each ${\\lambda }$-term has at least one fixed point, which is due to the existence of a fixed point combinator. It is unknown whether it enjoys the \u2018fixed point property\u2019 stating that each ${\\lambda }$-term has either one or infinitely many pairwise distinct fixed points. We show that the fixed point property holds when considering possibly open fixed points. The problem of counting fixed points in the closed setting remains open, but we provide sufficient conditions for a ${\\lambda }$-term to have either one or infinitely many fixed points. In the main result of this paper we prove that in every sensible ${\\lambda }$-theory there exists a ${\\lambda }$-term that violates the fixed point property.<\/jats:p><\/jats:sec><jats:sec><jats:title\/><jats:p>We then study the open problem concerning the existence of a double fixed point combinator and propose a proof technique that could lead towards a negative solution. We consider interpretations of the ${\\lambda } {\\mathtt{Y}}$-calculus into the ${\\lambda }$-calculus together with two reduction extension properties, whose validity would entail the non-existence of any double fixed point combinators. We conjecture that both properties hold when typed ${\\lambda } {\\mathtt{Y}}$-terms are interpreted by arbitrary fixed point combinators. We prove reduction extension property I for a large class of fixed point combinators.<\/jats:p><\/jats:sec><jats:sec><jats:title\/><jats:p>Finally, we prove that the ${\\lambda }{\\mathtt{Y}}$-theory generated by the equation characterizing double fixed point combinators is a conservative extension of the ${\\lambda }$-calculus.<\/jats:p><\/jats:sec>","DOI":"10.1093\/logcom\/exz013","type":"journal-article","created":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T03:21:06Z","timestamp":1556680866000},"page":"831-880","source":"Crossref","is-referenced-by-count":1,"title":["The fixed point property and a technique to harness double fixed point combinators"],"prefix":"10.1093","volume":"29","author":[{"given":"Giulio","family":"Manzonetto","sequence":"first","affiliation":[{"name":"Universit\u00e9 Paris 13, Laboratoire d'Informatique de Paris-Nord, CNRS UMR 7030, France"}]},{"given":"Andrew","family":"Polonsky","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Appalachian State University Boone, NC 28608, USA"}]},{"given":"Alexis","family":"Saurin","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Paris, IRIF, CNRS, F-75013 Paris, France"}]},{"given":"Jakob Grue","family":"Simonsen","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Copenhagen (DIKU), Universitetsparken 1, 2100 Copenhagen \u00d8, Denmark"}]}],"member":"286","published-online":{"date-parts":[[2019,7,10]]},"reference":[{"key":"2019091313044505400_ref1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511983504","volume-title":"Domains and Lambda-Calculi","author":"Amadio","year":"1998"},{"key":"2019091313044505400_ref2","volume-title":"The Lambda Calculus, Its Syntax and Semantics","author":"Barendregt","year":"1984"},{"key":"2019091313044505400_ref3","first-page":"548","author":"Bethke","year":"2003","journal-title":"Lambda Calculus"},{"key":"2019091313044505400_ref4","volume-title":"Term Rewriting Systems\u2014TeReSe","author":"Bezem","year":"2003"},{"key":"2019091313044505400_ref5","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/j.tcs.2015.12.024","article-title":"Graph easy sets of mute lambda terms","volume":"629","author":"Bucciarelli","year":"2016","journal-title":"Theoretical Computer Science"},{"key":"2019091313044505400_ref6","doi-asserted-by":"crossref","DOI":"10.2168\/LMCS-9(4:21)2013","article-title":"Ordered models of the lambda calculus","volume":"9","author":"Carraro","year":"2013","journal-title":"Logical Methods in Computer Science"},{"key":"2019091313044505400_ref7","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1017\/S0956796800000952","article-title":"A-translation and looping combinators in pure type systems","volume":"4","author":"Coquand","year":"1994","journal-title":"Journal of Functional Programming"},{"key":"2019091313044505400_ref8","article-title":"Private communication","author":"Endrullis","year":"2011"},{"key":"2019091313044505400_ref9","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1109\/LICS.2010.8","article-title":"Modular construction of fixed point combinators and clocked B\u00f6hm trees","volume-title":"Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010","author":"Endrullis","year":"2010"},{"key":"2019091313044505400_ref10","doi-asserted-by":"crossref","DOI":"10.2168\/LMCS-10(2:4)2014","article-title":"Discriminating lambda-terms using clocked B\u00f6hm trees","volume":"10","author":"Endrullis","year":"2014","journal-title":"Logical Methods in Computer Science"},{"key":"2019091313044505400_ref11","first-page":"425","article-title":"Reduction under substitution","volume-title":"Rewriting Techniques and Applications, 19th International Conference, RTA 2008, Hagenberg, Austria, July 15\u201317, 2008, Proceedings","author":"Endrullis","year":"2008"},{"key":"2019091313044505400_ref12","volume-title":"On fixed point and looping combinators in type theory","author":"Geuvers","year":"2009"},{"key":"2019091313044505400_ref13","doi-asserted-by":"crossref","first-page":"320","DOI":"10.1109\/LICS.1994.316057","article-title":"On the Church\u2013Rosser property for expressive type systems and its consequences for their metatheoretic study","author":"Geuvers","year":"1994","journal-title":"In Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, pp."},{"key":"2019091313044505400_ref14","first-page":"361","article-title":"A syntactic characterization of the equality in some models for the lambda calculus","volume-title":"Journal London Mathematical Society (2)","author":"Hyland","year":"1975"},{"key":"2019091313044505400_ref15","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1006\/inco.1997.2633","article-title":"Non-existent Statman\u2019s double fixedpoint combinator does not exist, indeed","volume":"137","author":"Intrigila","year":"1997","journal-title":"Information and Computation"},{"key":"2019091313044505400_ref16","author":"Intrigila","year":"2000"},{"key":"2019091313044505400_ref17","doi-asserted-by":"crossref","first-page":"595","DOI":"10.1017\/S0960129500003091","article-title":"On the number of fixed points of a combinator in lambda calculus","volume":"10","author":"Intrigila","year":"2000","journal-title":"Mathematical Structures in Computer Science"},{"key":"2019091313044505400_ref18","first-page":"1","article-title":"Lambda theories allowing terms with a finite number of fixed points","author":"Intrigila","year":"2015","journal-title":"Mathematical Structures in Computer Science"},{"key":"2019091313044505400_ref19","first-page":"197","article-title":"New fixed point combinators from old","volume-title":"Reflections on Type Theory,lambda-Calculus, and the Mind","author":"Klop","year":"2007"},{"key":"2019091313044505400_ref20","author":"Klop","year":"2014"},{"key":"2019091313044505400_ref21","doi-asserted-by":"crossref","DOI":"10.2168\/LMCS-9(4:20)2013","article-title":"Nominal coalgebraic data types with applications to lambda calculus","volume":"9","author":"Kurz","year":"2013","journal-title":"Logical Methods in Computer Science"},{"key":"2019091313044505400_ref22","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1093\/logcom\/14.3.373","article-title":"The lattice of lambda theories","volume":"14","author":"Lusin","year":"2004","journal-title":"Journal of Logic and Computation"},{"key":"2019091313044505400_ref23","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1007\/978-3-540-85238-4_39","article-title":"From $\\lambda $-calculus to universal algebra and back","volume-title":"Mathematical Foundations of Computer Science 2008: 33rd International Symposium, MFCS 2008, Torun, Poland, August 25\u201329, 2008, Proceedings","author":"Manzonetto","year":"2008"},{"key":"2019091313044505400_ref24","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1093\/oso\/9780198537809.003.0003","article-title":"Correspondence between operational and denotational semantics","volume-title":"Handbook of Logic in Computer Science","author":"Ong","year":"1995"},{"key":"2019091313044505400_ref25","doi-asserted-by":"crossref","first-page":"313","DOI":"10.2307\/2272645","volume":"39","author":"Plotkin","year":"1974","journal-title":"Journal of Symbolic Logic"},{"key":"2019091313044505400_ref26","doi-asserted-by":"crossref","first-page":"1195","DOI":"10.2178\/jsl.7704080","article-title":"The range property fails for $\\mathcal{H}$","volume":"77","author":"Polonsky","year":"2012","journal-title":"Journal of Symbolic Logic"},{"key":"2019091313044505400_ref27","first-page":"379","article-title":"Nonmodularity results for lambda calculus","volume":"45","author":"Salibra","year":"2001","journal-title":"Fundamenta Informaticae"},{"key":"2019091313044505400_ref28","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/11538363_9","article-title":"Order structures on B\u00f6hm-like models","volume-title":"Computer Science Logic: 19th International Workshop, CSL 2005","author":"Severi","year":"2005"},{"key":"2019091313044505400_ref29","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1016\/0304-3975(93)90096-C","article-title":"Some examples of non-existent combinators","volume":"121","author":"Statman","year":"1993","journal-title":"Theoretical Computer Science"},{"key":"2019091313044505400_ref30","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1016\/j.apal.2004.04.004","article-title":"On the lambdaY calculus","volume":"130","author":"Statman","year":"2004","journal-title":"Annals of Pure and Applied Logic"},{"key":"2019091313044505400_ref31","doi-asserted-by":"crossref","first-page":"488","DOI":"10.1137\/0205036","article-title":"The relation between computational and denotational properties for Scott\u2019s ${\\mathcal{D}}_{\\infty } $-models of the lambda-calculus","volume":"5","author":"Wadsworth","year":"1976.","journal-title":"SIAM Journal of Computing"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/advance-article-pdf\/doi\/10.1093\/logcom\/exz013\/28925419\/exz013.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/29\/5\/831\/30010822\/exz013.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,17]],"date-time":"2024-07-17T14:05:45Z","timestamp":1721225145000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/29\/5\/831\/5528041"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,10]]},"references-count":31,"journal-issue":{"issue":"5","published-online":{"date-parts":[[2019,7,10]]},"published-print":{"date-parts":[[2019,9,12]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exz013","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2019,9]]},"published":{"date-parts":[[2019,7,10]]}}}