Factorize Factorization
share
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. Factorization – a simple form of standardization – is concerned with reduction strategies, i.e. how a result is computed. The 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 technique to diverse extensions of the λ-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 obtain a novel proof which is neat and strikingly short.
READ FULL TEXT