An abstract Church-Rosser theorem. II: Applications

Abstract

This paper is a continuation of An abstract form of the Church-Rosser theorem . I (this Journal, vol. 35 (1969), pp. 545–560). In Part I, the Church-Rosser property was deduced from abstract premises (A1)–(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 λβ-reduction to λβη-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 λβ-reduction has been discovered by W. W. Tait and P. Martin-Löf (see §11 later, and [17, §2.4.3]). 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 λβ-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. In §§5 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 §6 an important subclass of such reductions will be treated (Theorem 3). In §7, Theorem 3 will be applied to prove the Church-Rosser property for combinatory weak reduction [10, §11B], with or without type-restrictions and extra “arithmetical” 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].)