{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,6]],"date-time":"2026-04-06T15:43:13Z","timestamp":1775490193783,"version":"3.50.1"},"reference-count":18,"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":14621,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1974,3]]},"abstract":"<jats:p>This paper is a continuation of <jats:italic>An abstract form of the Church-Rosser theorem<\/jats:italic>. I (this Journal, vol. 35 (1969), pp. 545\u2013560). In Part I, the Church-Rosser property was deduced from abstract premises (A1)\u2013(A8). The original draft of Part II contained some applications of this result, and a fairly simple abstract result by which the Church-Rosser property could be extended from \u03bb\u03b2-reduction to \u03bb\u03b2\u03b7-reduction (Curry's notation [3, Chapter 3]). But since this draft was written, these results have been obtained independently and improved by other workers, and a simple and natural new proof for \u03bb\u03b2-reduction has been discovered by W. W. Tait and P. Martin-L\u00f6f (see \u00a711 later, and [17, \u00a72.4.3]).<\/jats:p><jats:p>So the main purpose of the present Part II is merely to justify the claim in Part I that the abstract theorem does cover the case of \u03bb\u03b2-reduction (and various modifications). I shall also include a summary of the main kinds of Church-Rosser proofs. The paragraph and theorem numbers in Part II will continue from those of Part I.<\/jats:p><jats:p>In \u00a7\u00a75 and 6 below, Theorem 1 will be specialised to reductions defined by replacements of parts of expressions by others (Theorems 2 and 2A). At the end of \u00a76 an important subclass of such reductions will be treated (Theorem 3).<\/jats:p><jats:p>In \u00a77, Theorem 3 will be applied to prove the Church-Rosser property for combinatory weak reduction [10, \u00a711B], with or without type-restrictions and extra \u201carithmetical\u201d reduction-rules (Theorems 4 and 5). (In the original draft Theorem 5 was deduced directly from Theorem 2A; the present intervening Theorem 3 is an independent result of B. Rosen [7].)<\/jats:p>","DOI":"10.2307\/2272337","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T21:27:55Z","timestamp":1146950875000},"page":"1-21","source":"Crossref","is-referenced-by-count":26,"title":["An abstract Church-Rosser theorem. II: Applications"],"prefix":"10.1017","volume":"39","author":[{"given":"R.","family":"Hindley","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200065361_ref011","first-page":"56","volume":"5","author":"Church","year":"1940","journal-title":"A formulation of the simple theory of types"},{"key":"S0022481200065361_ref004","doi-asserted-by":"publisher","DOI":"10.2307\/1968867"},{"key":"S0022481200065361_ref017","volume-title":"An intuitionistic theory of types","author":"Martin-L\u00f6f","year":"1972"},{"key":"S0022481200065361_ref002","volume-title":"The calculi of Lambda-conversion","author":"Church","year":"1941"},{"key":"S0022481200065361_ref010","volume-title":"Combinatory Logic, Volume II","author":"Curry","year":"1972"},{"key":"S0022481200065361_ref001","first-page":"16","article-title":"A new proof of the Church-Rosser Theorem","volume":"55","author":"Curry","year":"1952","journal-title":"Koninklijke Nederlandse Akademie van Wetenschappen. Proceedings"},{"key":"S0022481200065361_ref008","doi-asserted-by":"publisher","DOI":"10.1007\/BF02008531"},{"key":"S0022481200065361_ref005","first-page":"377","volume":"24","author":"Rosser","year":"1956","journal-title":"Review of \u201cA new proof of the Church-Rosser Theorem\u201d"},{"key":"S0022481200065361_ref007","doi-asserted-by":"publisher","DOI":"10.1145\/321738.321750"},{"key":"S0022481200065361_ref012","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093956080"},{"key":"S0022481200065361_ref016","volume-title":"London Mathematical Society Lecture Notes Series","author":"Hindley","year":"1972"},{"key":"S0022481200065361_ref003","volume-title":"Combinatory logic, Volume I","author":"Curry","year":"1958"},{"key":"S0022481200065361_ref013","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1936-1501858-0"},{"key":"S0022481200065361_ref015","doi-asserted-by":"publisher","DOI":"10.4064\/fm-50-3-281-303"},{"key":"S0022481200065361_ref018","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-010-2913-1"},{"key":"S0022481200065361_ref014","first-page":"198","volume":"32","author":"Tait","year":"1967","journal-title":"Intensional interpretations of functionals of finite type. I"},{"key":"S0022481200065361_ref006","unstructured":"Schroer D. E. , The Church-Rosser theorem, Ph.D. thesis, Cornell University, Ithaca, N.Y., 1965."},{"key":"S0022481200065361_ref009","doi-asserted-by":"publisher","DOI":"10.2307\/1968669"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200065361","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T21:37:39Z","timestamp":1559165859000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200065361\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1974,3]]},"references-count":18,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1974,3]]}},"alternative-id":["S0022481200065361"],"URL":"https:\/\/doi.org\/10.2307\/2272337","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1974,3]]}}}