{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,11]],"date-time":"2025-07-11T10:40:31Z","timestamp":1752230431897},"reference-count":14,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":4029,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[2003,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p><jats:italic>Dual combinators<\/jats:italic>emerge from the aim of assigning formulas containing \u2190 as types to combinators. This paper investigates formally some of the properties of combinatory systems that include both combinators and dual combinators. Although the addition of dual combinators to a combinatory system does not affect the unique decomposition of terms, it turns out that some terms might be redexes in two ways (with a combinator as its head, and with a dual combinator as its head). We prove a general theorem stating that<jats:italic>no dual combinatory system possesses the Church-Rosser property<\/jats:italic>. Although the lack of confluence might be problematic in some cases, it is not a problem<jats:italic>per se<\/jats:italic>. In particular, we show that no damage is inflicted upon the<jats:italic>structurally free logics<\/jats:italic>, the system in which dual combinators first appeared.<\/jats:p>","DOI":"10.2178\/jsl\/1045861508","type":"journal-article","created":{"date-parts":[[2005,3,2]],"date-time":"2005-03-02T20:53:40Z","timestamp":1109796820000},"page":"132-152","source":"Crossref","is-referenced-by-count":3,"title":["The Church-Rosser property in dual combinatory logic"],"prefix":"10.1017","volume":"68","author":[{"given":"Katalin","family":"Bimb\u00f3","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S002248120000894X_ref004","volume-title":"Combinatory logic","volume":"I","author":"Curry","year":"1958"},{"key":"S002248120000894X_ref001","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005252431462"},{"key":"S002248120000894X_ref007","first-page":"545","volume":"34","author":"Hindley","year":"1969","journal-title":"An abstract form of the Church-Rosser theorem, I"},{"key":"S002248120000894X_ref003","volume-title":"The calculi of lambda-conversion","author":"Church","year":"1941"},{"key":"S002248120000894X_ref002","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/6.3.403"},{"key":"S002248120000894X_ref014","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0062861"},{"key":"S002248120000894X_ref005","volume-title":"Combinatory logic","volume":"II","author":"Curry","year":"1972"},{"key":"S002248120000894X_ref008","volume-title":"Introduction to combinators and \u03bb-calculus","author":"Hindley","year":"1986"},{"key":"S002248120000894X_ref006","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/5.4.505"},{"key":"S002248120000894X_ref009","doi-asserted-by":"publisher","DOI":"10.2307\/1968749"},{"key":"S002248120000894X_ref010","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1093\/oso\/9780198537779.003.0008","volume-title":"Substructural logics","author":"Lambek","year":"1993"},{"key":"S002248120000894X_ref011","first-page":"463","article-title":"Dual combinators bite the dust, (abstract)","volume":"4","author":"Meyer","year":"1998","journal-title":"The Bulletin of Symbolic Logic"},{"key":"S002248120000894X_ref012","doi-asserted-by":"publisher","DOI":"10.1145\/321738.321750"},{"key":"S002248120000894X_ref013","first-page":"127","article-title":"A mathematical logic without variables","volume":"2","author":"Rosser","year":"1936","journal-title":"Annals of Mathematics"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S002248120000894X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,23]],"date-time":"2024-01-23T22:45:37Z","timestamp":1706049937000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S002248120000894X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,3]]},"references-count":14,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,3]]}},"alternative-id":["S002248120000894X"],"URL":"https:\/\/doi.org\/10.2178\/jsl\/1045861508","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003,3]]}}}