一句话：提出带代数化简的简单类型 λ 演算 λ_AS，用 δ 抽象和类型系统为复杂归约的并行化提供等式推理基础。
并行归约是并行编程的核心，但哪些非平凡汇总可表示为并行归约仍缺乏理解。本文提出 λ_AS：一个带代数化简的简单类型 Lambda 演算，为通过等式推理研究复杂归约的并行化提供基础。其核心是 δ 抽象。δ 抽象与标准 λ 抽象观察等价，但会利用结合律、交换律等代数性质，在参数到达前先化简函数体；类型系统则保证这些化简不会引入严重开销。作者通过多个复杂并行归约的推导实例展示其有效性，包括含多个归约算子的情形、带条件跳转的循环、前缀和模式以及树操作。
Abstract Parallel reduction is a major component of parallel programming and widely used for summarisation and aggregation. It is not well understood, however, what sorts of non-trivial summarisations 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 a parallelisation 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 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 conditional jumps, prefix sum patterns and even tree manipulations.
@article{paperbot1234,
title = {Lambda calculus with algebraic simplification for reduction parallelisation: Extended study},
author = {AKIMASA MORIHATA},
journal = {Journal of Functional Programming},
volume = {31},
year = {2021},
doi = {10.1017/s0956796821000058}
}