Correct Compilation of Semiring Contractions

TL;DR

This paper presents a formal semantics and a compiler for variable contraction problems over semirings, unifying various algebraic computations and demonstrating performance comparable to existing tensor algebra tools.

Contribution

It introduces a novel operational semantics for variable contraction problems and a compiler that ensures correctness and broad applicability.

Findings

Compiler performance matches state-of-the-art tensor algebra tools

The semantics guarantees correctness of fused variable contraction execution

Framework generalizes sparse/dense tensor, relational, and graph algorithms

Abstract

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.