Residuated Park theories

Research output: Contribution to journalArticle

2 Citations (Scopus)


When L is a complete lattice, the collection MonL of all monotone functions Lp → Ln, n,p,0, forms a Lawvere theory. We enrich this Lawvere theory with the binary supremum operation, an operation of (left) residuation Crossed D sign and the parameterized least fixed point operation. We exhibit a system of equational axioms which is sound and proves all valid equations of the theories MonL involving only the theory operations, 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.

Original languageEnglish
Pages (from-to)453-471
Number of pages19
JournalJournal of Logic and Computation
Issue number2
Publication statusPublished - Apr 1 2015


  • Least fixed points
  • equational theory
  • iteration theory
  • residuals

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science
  • Arts and Humanities (miscellaneous)
  • Hardware and Architecture
  • Logic

Fingerprint Dive into the research topics of 'Residuated Park theories'. Together they form a unique fingerprint.

  • Cite this