Residuated Park Theories

TL;DR

This paper develops an algebraic framework for monotone functions over complete lattices, enriching Lawvere theories with operations like supremum, residuation, and fixed points, and applies it to regular tree languages.

Contribution

It introduces a new equational axiomatization for monotone function theories with residuation and fixed points, including an alternative star-based system, and demonstrates its application to regular tree languages.

Findings

A sound axiomatization for equations involving monotone functions, supremum, residuation, and fixed points.

An alternative axiomatization replacing fixed points with star operations.

Application of the theory to characterize regular tree languages.

Abstract

When $L$ is a complete lattice, the collection $\Mon_L$ of all monotone functions $L^p \to L^n$, $n,p \geq 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 $^\dagger$. 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 $^\dagger$, i.e., all valid equations not involving residuation. We also present an alternative axiomatization, where $^\dagger$ is replaced by a star operation, and provide an application to regular tree languages.