We introduce proof terms for string rewrite systems and, using these, show that various notions of equivalence on reductions known from the literature can be viewed as different perspectives on the notion of causal equivalence. In particular, we show that permutation equivalence classes (as known from the lambda-calculus and term rewriting) are uniquely represented both by trace graphs (known from physics as causal graphs) and by so-called greedy multistep reductions (as known from algebra). We present effective maps from the former to the latter, topological multi-sorting TM, and vice versa, the proof term algebra [[ ]].

翻译：我们引入字符串重写系统的证明项，并利用这些证明项表明，文献中已知的关于归约的各种等价概念，都可以被视为因果关系等价概念的不同视角。特别地，我们证明置换等价类（如λ演算和项重写中已知的）既可以由迹图（在物理学中称为因果图）唯一表示，也可以由所谓的贪心多步归约（如代数中已知的）唯一表示。我们给出了从前者到后者（拓扑多排序TM）以及反之（证明项代数[[ ]]）的有效映射。