Parallel reductions in \(\lambda\)-calculus (Q5903814)

The notion of parallel reduction is extracted from the Tait-Martin-Löf proof of the Church-Rosser theorem (for \(\beta\)-reduction). We define parallel \(\beta\)-, \(\eta\)- and \(\beta\) \(\eta\)-reduction by induction, and use them to give simple proofs of some fundamental theorems in \(\lambda\)- calculus; the normal reduction theorem for \(\beta\)-reduction, that for \(\beta\) \(\eta\)-reduction, the postponement theorem of \(\eta\)-reduction (in \(\beta\) \(\eta\)-reduction), and some others.