The criterion for confluence using decreasing diagrams is a generalization of several well-known confluence criteria in abstract rewriting, such as the strong confluence lemma. We give a new proof of the decreasing diagram theorem based on a geometric study of infinite reduction diagrams, arising from unsuccessful attempts to obtain a confluent diagram by tiling with elementary diagrams.

In this note, we prove that having unique head-normal forms is a sufficient condition on partial combinatory algebras to be completable. As application, we show that the pca of strongly normalizing CL-terms as well as the pca of natural numbers with partial recursive function application can be extended to total combinatory algebras.

Consideration is given to the equational theory lambda pi of lambda calculus extended with constants pi , pi /sub 0/, pi /sub 1/ and axioms for subjective pairing: pi /sub 0/( pi XY)=X, pi /sub 1/( pi XY)=Y, pi ( pi /sub 0/X)( pi /sub 1/X)=X. The reduction system that one obtains by reading the equations are reductions (from left to right) is not Church-Rosser. Despite this failure, the author obtains a syntactic consistency proof of lambda pi and shows that it is a conservative extension of the pure lambda calculus.>

Let M be a term of the type free λ-calculus and let be a set of occurrences of redexes in M. A reduction sequence from M which first contracts a member of and afterwards only residuals of is called a development (of M with respect to ). The finite developments theorem says that developments are always finite. There are several proofs of this theorem in the literature. A plausible strategy is to define some kind of measure for pairs (M, ), which—if M′ results from M by contracting a redex occurrence in and ′ is the set of residuals of in M′— decreases in passing from (M, ) to (M′, ′). This procedure is followed as a matter of fact in the proofs in Hyland [4] and in Barendregt [1] (both are covered in Klop [5]). If, as in the latter proof, the natural numbers are used as measures, then the measure of (M, ) will actually denote an upper bound of the number of reduction steps in a development of M with respect to . In the present proof we straightforwardly define for each pair (M, ) a natural number, which can easily be seen to indicate the exact number of reduction steps in a development of maximal length of M with respect to .