Equational properties of fixed-point operations in cartesian categories: An overview

Research output: Contribution to journalArticle

Abstract

Several fixed-point models share the equational properties of iteration theories, or iteration categories, which are cartesian categories equipped with a fixed point or dagger operation subject to certain axioms. After discussing some of the basic models, we provide equational bases for iteration categories and offer an analysis of the axioms. Although iteration categories have no finite base for their identities, there exist finitely based implicational theories that capture their equational theory. We exhibit several such systems. Then we enrich iteration categories with an additive structure and exhibit interesting cases where the interaction between the iteration category structure and the additive structure can be captured by a finite number of identities. This includes the iteration category of monotonic or continuous functions over complete lattices equipped with the least fixed-point operation and the binary supremum operation as addition, the categories of simulation, bisimulation, or language equivalence classes of processes, context-free languages, and others. Finally, we exhibit a finite equational system involving residuals, which is sound and complete for monotonic or continuous functions over complete lattices in the sense that it proves all of their identities involving the operations and constants of cartesian categories, the least fixed-point operation and binary supremum, but not involving residuals.

Original languageEnglish
Pages (from-to)909-925
Number of pages17
JournalMathematical Structures in Computer Science
Volume29
Issue number6
DOIs
Publication statusPublished - Jun 1 2019

    Fingerprint

Keywords

  • automata theory
  • Conway categories
  • Fixed point theories
  • iteration categories

ASJC Scopus subject areas

  • Mathematics (miscellaneous)
  • Computer Science Applications

Cite this