The Church-Rosser property for beta eta -reduction in typed lambda -calculi

摘要

The Church-Rosser property (CR) for pure type systems with beta eta -reduction is investigated. It is proved that CR (for beta eta ) on the well-typed terms of a fixed type holds, which is the maximum one can expect in view of Nederpelt's (1973) counterexample. The proof is given for a large class of pure type systems that contains, e.g., LF F, F omega , and the calculus of constructions.