Factorization -- a simple form of standardization -- is concerned with reduction strategies, i.e. how a result is computed. We present a new technique for proving factorization theorems for compound rewriting systems in a modular way, which is inspired by the Hindley-Rosen technique for confluence. Specifically, our technique is well adapted to deal with extensions of the call-by-name and call-by-value lambda-calculi. The technique is first developed abstractly. We isolate a sufficient condition (called linear swap) for lifting factorization from components to the compound system, and which is compatible with beta-reduction. We then closely analyze some common factorization schemas for the lambda-calculus. Concretely, we apply our technique to diverse extensions of the lambda-calculus, among which de Liguoro and Pipernos non-deterministic lambda-calculus and -- for call-by-value -- Carraro and Guerrieris shuffling calculus. For both calculi the literature contains factorization theorems. In both cases, we give a new proof which is neat, simpler than the original, and strikingly shorter.
Download