Residuated Park Theories

Abstract

When $L$ is a complete lattice, the collection $\Mon_L$ of all monotone functions $L^p\to L^n$, $n,p\ge 0$, forms a Lawvere theory. We enrich this Lawvere theory with the binary supremum operation $\vee$, an operation of (left) residuation $\res$ and the parameterized least fixed point operation ${}^{†}$. We exhibit a system of \emph{equational} axioms which is sound and proves all valid equations of the theories $\Mon_L$ involving only the theory operations, $\vee$ and ${}^{†}$, i.e., all valid equations not involving residuation. We also present an alternative axiomatization, where ${}^{†}$ is replaced by a star operation, and provide an application to regular tree languages.