论文标题
分解分解
Factorize Factorization
论文作者
论文摘要
分解 - 一种简单的标准化形式 - 与减少策略有关，即如何计算结果。我们提出了一种新技术，用于以模块化的方式证明复合重写系统的分解定理，这是受Hindley-Rosen技术汇合技术的启发。具体而言，我们的技术非常适合处理按名称和呼叫的lambda-calculi的扩展。该技术首先是抽象开发的。我们隔离了一个足够的条件（称为线性互换），用于从组件到复合系统的提升分解，并且与β还原兼容。然后，我们对Lambda-Calculus的一些共同分解模式进行密切分析。具体而言，我们将技术应用于Lambda-Calculus的各种延伸，其中包括Liguoro和Piperno的非确定性Lambda-Calculus，以及 - Carraro和Carraro和Guerrieri的Shuffling Colculus。对于两种结石，文献都包含分解定理。在这两种情况下，我们都提供了一个新的证明，它比原始的简单，更简单，而且更短。
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 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. In both cases, we give a new proof which is neat, simpler than the original, and strikingly shorter.
