Lambda calculus with algebraic simplification for reduction parallelization by equational reasoning
Lambda calculus with algebraic simplification for reduction parallelization by equational reasoning
复制标题
通过代数简化进行 Lambda 演算，通过方程推理进行简化并行化
DOI：
10.1145/3341644
复制
发表时间：
2019
影响因子：
--
通讯作者：
Morihata Akimasa
中科院分区：
文献类型：
--
作者：
直井由樹;山田浩史;Morihata Akimasa
并行归约是并行编程的一个重要组成部分，广泛用于汇总和聚合。然而，什么样的非平凡摘要可以作为并行约简来实现，这一点还没有很好地理解。本文开发了一种名为λas的演算，这是一种具有代数简化的简单类型λ演算。该演算为研究方程推理的复杂约简的并行化提供了基础。它的主要特征是δ抽象。δ抽象在观测上等价于标准的λ抽象，但它的主体在其参数到达之前通过使用代数性质如结合性和交换性而被简化。此外，λ 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 λasguarantees that simplifications due to δ abstractions do not lead to serious overheads. The usefulness of λasis 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.