Correspondence between Composite Theories and Distributive Laws

TL;DR

This paper explores the deep connection between composite theories and distributive laws, providing methods to construct one from the other and analyzing their axiomatization using term rewriting techniques.

Contribution

It establishes a detailed correspondence between composite theories and distributive laws and introduces a method to axiomatize composite theories with minimal equations.

Findings

Constructs composite theories from distributive laws.

Shows how to derive distributive laws from composite theories.

Uses term rewriting to identify minimal axiomatizations.

Abstract

Composite theories are the algebraic equivalent of distributive laws. In this paper, we delve into the details of this correspondence and concretely show how to construct a composite theory from a distributive law and vice versa. Using term rewriting methods, we also describe when a minimal set of equations axiomatises the composite theory.