Parallel Reductions in λ-Calculus

Abstract

The notion of parallel reduction is extracted from the simple proof of the Church-Rosser theorem by Tait and Martin-Löf. Intuitively, this means to reduce a number of redexes (existing in a λ-term) simultaneously. Thus in the case of β-reduction the effect of a parallel reduction is same as that of a "complete development" which is defined by using "residuals" of β-redexes. A nice feature of parallel reduction, however, is that it can be defined directly by induction on the structure of λ-terms (without referring to residuals or other auxiliary notions), and the inductive definition provides us exactly what we need in proving the theorem inductively. Moreover, the notion can be easily extended to other reduction systems such as Girard′s second-order system F and Gödel′s system T. In this paper, after reevaluating the significance of the notion of parallel reduction in Tait-and-Martin-Löf type proofs of the Church-Rosser theorems, we show that the notion of parallel reduction is also useful in giving short and direct proofs of some other fundamental theorems in reduction theory of λ-calculus; among others, we give such simple proofs of the standardization theorem for β-reduction (a special case of which is known as the leftmost reduction theorem for β-reduction), the quasi-leftmost reduction theorem for β-reduction, the postponement theorem of η-reduction (in βη-reduction), and the leftmost reduction theorem for βη-reduction. © 1995 Academic Press. All rights reserved.