论文标题
正确编译半缩收缩
Correct Compilation of Semiring Contractions
论文作者
论文摘要
我们介绍了一种形式的操作语义，该语义描述了可变收缩问题的融合执行，该语义在半度性上计算了索引算术，并概括了稀疏和密集的张量代数，关系代数和图形算法。我们证明该模型相对于功能语义是正确的。我们还开发了一个用于可变收缩表达式的编译器，并表明其性能等同于最先进的稀疏张量代数编译器，同时提供了更大的一般性和正确性保证。
We introduce a formal operational semantics that describes the fused execution of variable contraction problems, which compute indexed arithmetic over a semiring and generalize sparse and dense tensor algebra, relational algebra, and graph algorithms. We prove that the model is correct with respect to a functional semantics. We also develop a compiler for variable contraction expressions and show that its performance is equivalent to a state-of-the art sparse tensor algebra compiler, while providing greater generality and correctness guarantees.
