一句话：提出 λas 演算，用 δ 抽象在参数到达前做代数化简，为复杂归约的并行化提供等式推理基础。
并行归约是并行编程的核心构件，广泛用于汇总与聚合，但哪些非平凡汇总能以并行归约实现仍缺乏清晰理解。本文提出 λas，一种带代数化简的简单类型 lambda 演算，为通过等式推理研究复杂归约的并行化提供基础。其核心机制是 δ 抽象：它与标准 λ 抽象观察等价，但在参数到达之前就利用结合律、交换律等代数性质对函数体进行化简；同时，λas 的类型系统保证由 δ 抽象引入的化简不会导致严重开销。作者通过多个复杂并行归约的开发实例展示该演算的实用性，包括含多个归约算子的情形、带跳转的循环、前缀和模式乃至树操作。
Parallel reduction is a major component of parallel programming and widely used for summarization and aggregation. It is not well understood, however, what sorts of nontrivial summarizations can be implemented as parallel reductions. This paper develops a calculus named λ as , a simply typed lambda calculus with algebraic simplification. This calculus provides a foundation for studying parallelization of complex reductions by equational reasoning. Its key feature is δ abstraction. A δ abstraction is observationally equivalent to the standard λ abstraction, but its body is simplified before the arrival of its arguments by using algebraic properties such as associativity and commutativity. In addition, the type system of λ as guarantees that simplifications due to δ abstractions do not lead to serious overheads. The usefulness of λ as is demonstrated on examples of developing complex parallel reductions, including those containing more than one reduction operator, loops with jumps, prefix-sum patterns, and even tree manipulations.
@article{paperbot582,
title = {Lambda calculus with algebraic simplification for reduction parallelization by equational reasoning},
author = {Akimasa Morihata},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {ICFP},
year = {2019},
doi = {10.1145/3341644}
}