{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,12]],"date-time":"2024-08-12T18:37:50Z","timestamp":1723487870551},"reference-count":5,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":14802,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1973,9]]},"abstract":"<jats:p>The theorem proved in this paper answers some transitivity questions (in the geometric sense) for the type free <jats:italic>\u03bb<\/jats:italic>-calculus: Which objects can be mapped on all other objects? How much can an object do by applying it to other objects (see footnote 2)?<\/jats:p><jats:p>The main result is that, for closed terms of the <jats:italic>\u03bb<\/jats:italic><jats:italic>I<\/jats:italic>-calculus, the following conditions are equivalent:<\/jats:p><jats:p>(a) <jats:italic>M<\/jats:italic> has a normal form.<\/jats:p><jats:p>(b) <jats:italic>FM<\/jats:italic> = <jats:italic>I<\/jats:italic> for some <jats:italic>\u03bbI<\/jats:italic>-term <jats:italic>F<\/jats:italic>.<\/jats:p><jats:p>(c) <jats:italic>MN<\/jats:italic><jats:sub>1<\/jats:sub> \u2026 <jats:italic>N<jats:sub>n<\/jats:sub><\/jats:italic> = <jats:italic>I<\/jats:italic> for some <jats:italic>\u03bbI<\/jats:italic>-terms <jats:italic>N<\/jats:italic><jats:sub>1<\/jats:sub> \u2026, <jats:italic>N<jats:sub>n<\/jats:sub><\/jats:italic>.<\/jats:p><jats:p>By the same method it follows that if <jats:italic>M<\/jats:italic> is a closed term of the <jats:italic>\u03bbK<\/jats:italic>-calculus having a normal form, then for some <jats:italic>\u03bbI<\/jats:italic>-terms (sic) <jats:italic>N<\/jats:italic><jats:sub>1<\/jats:sub>, \u2026, <jats:italic>N<jats:sub>n<\/jats:sub><\/jats:italic>, <jats:italic>MN<\/jats:italic><jats:sub>1<\/jats:sub>\u2026 <jats:italic>N<jats:sub>n<\/jats:sub><\/jats:italic> = <jats:italic>I<\/jats:italic> is provable in the <jats:italic>\u03bbK<\/jats:italic>-calculus.<\/jats:p><jats:p>The theorem of B\u00f6hm [2] states that if <jats:italic>M<\/jats:italic><jats:sub>1<\/jats:sub>, <jats:italic>M<\/jats:italic><jats:sub>2<\/jats:sub> are terms of the <jats:italic>\u03bbK<\/jats:italic>-calculus having different <jats:italic>\u03b2\u03b7<\/jats:italic>-normal forms, then \u2200<jats:italic>A<\/jats:italic><jats:sub>1<\/jats:sub>, <jats:italic>A<\/jats:italic><jats:sub>2<\/jats:sub> \u2203<jats:italic>N<\/jats:italic><jats:sub>1<\/jats:sub>, \u2026, <jats:italic>N<jats:sub>n<\/jats:sub>M<jats:sub>i<\/jats:sub>N<\/jats:italic><jats:sub>1<\/jats:sub> \u2026 <jats:italic>N<jats:sub>n<\/jats:sub><\/jats:italic> = <jats:italic>A<jats:sub>i<\/jats:sub><\/jats:italic> is provable in the <jats:italic>\u03bbK-\u03b2\u03b7<\/jats:italic>-calculus for <jats:italic>i<\/jats:italic> = 1, 2. As a consequence of this it was shown (implicitly) in [1, 3.2.20 1\/2 (1)] that if <jats:italic>M<\/jats:italic> has a normal form, then for some <jats:italic>\u03bbK<\/jats:italic>-terms <jats:italic>N<\/jats:italic><jats:sub>1<\/jats:sub>, \u2026, <jats:italic>N<jats:sub>n<\/jats:sub><\/jats:italic>, <jats:italic>MN<\/jats:italic><jats:sub>1<\/jats:sub> \u2026 <jats:italic>N<jats:sub>n<\/jats:sub><\/jats:italic> =<jats:italic>I<\/jats:italic> is provable in the <jats:italic>\u03bbK<\/jats:italic>-calculus.<\/jats:p><jats:p>It was not clear that this also could be proved for the <jats:italic>\u03bbK<\/jats:italic>-calculus since the proof of the theorem of B\u00f6hm essentially made use of <jats:italic>\u03bbK<\/jats:italic>-terms.<\/jats:p><jats:p>We conjecture that, using the results of this paper, the full theorem of B\u00f6hm can be proved for the <jats:italic>\u03bbI<\/jats:italic>-calculus.<\/jats:p>","DOI":"10.2307\/2273041","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T21:24:44Z","timestamp":1146950684000},"page":"441-445","source":"Crossref","is-referenced-by-count":6,"title":["A characterization of terms of the <i>\u03bbI<\/i>-calculus having a normal form"],"prefix":"10.1017","volume":"38","author":[{"given":"Henk","family":"Barendregt","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200054815_ref001","unstructured":"Barendregt Hendrik P. , Some extensional term models for \u03bb-calculi and combinatory logics, Thesis, Rijksuniversiteit, Utrecht, 1971."},{"key":"S0022481200054815_ref003","volume-title":"Annals of Mathematics Studies","author":"Church","year":"1941"},{"key":"S0022481200054815_ref005","volume-title":"Combinatory logic, Vol. 2","author":"Curry","year":"1972"},{"key":"S0022481200054815_ref004","volume-title":"Combinatory logic, Vol. 1","author":"Curry","year":"1958"},{"key":"S0022481200054815_ref002","volume-title":"Alcune proprieta della forme \u03b2-\u03b7-normali del \u03bb-K-calcolo","author":"B\u00f6hm","year":"1968"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200054815","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T19:37:51Z","timestamp":1559245071000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200054815\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1973,9]]},"references-count":5,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1973,9]]}},"alternative-id":["S0022481200054815"],"URL":"https:\/\/doi.org\/10.2307\/2273041","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1973,9]]}}}