Lambda-calculi come with no fixed evaluation strategy. Different strategies may then be considered, and it is important that they satisfy some abstract rewriting property, such as factorization or nomalization theorems. We provide simple proof techniques for these theorems. Our starting point is a revisitation of Takahashi's technique to prove factorization for head reduction. Our appraoch is both simpler and more powerful, as it works in cases where Takahishi's does not. We then pair factorization with two other abstract properties, defining essential systems, and show that normalization follows. Concretely, we apply the technique to four case studies, two classic ones, head and the leftmost-outermost reductions, and two less classic ones, non-deterministic weak call-by-value and least-level reductions.

Moreover, we present a new technique for proving factorization theorems for compound rewriting systems in a modular way, which is inspired by Hindley-Rosen result for confluence. Our technique is first developed abstractly. In particular, we isolate a simple sufficient condition (called linear swap) for lifting factorization from components to the compound system. We then closely analyze some common factorization schemas for the lambda-calculus, and show that the technique simplifies even more, reducing to the test of elementary local commutations. Concretely, we apply our modular technique to various extensions of the lambda-calculus, among which de' Liguoro and Piperno's non-deterministic lambda-calculus and --for call-by-value-- Carraro and Guerrieri's shuffling calculus. For both calculi the literature contains factorization theorems. For each, we provide a novel, neat, and strikingly short modular proof.

This is joint work with Beniamino Accattoli and Claudia Faggian.