Equational axioms associated with finite automata for fixed point operations in cartesian categories

TL;DR

This paper explores the axiomatic foundations of fixed point operations in categories, showing how automata-related identities, combined with Conway identities, form a complete basis for iteration theories under certain conditions.

Contribution

It establishes the completeness of automata-based identities with Conway identities for iteration categories, linking automaton properties to algebraic group quotients.

Findings

Automata identities plus Conway identities are complete for iteration categories.

Each automaton identity implies identities for input extensions of automata.

A stronger result applies to automata with a distinguished initial state.

Abstract

The axioms of iteration theories, or iteration categories, capture the equational properties of fixed point operations in several computationally significant categories. Iteration categories may be axiomatized by the Conway identities and identities associated with finite automata. We show that in conjunction with the Conway identities, each identity associated with a finite automaton implies the identity associated with any input extension of the automaton. We conclude that the Conway identities and the identities associated with the members of a subclass $\cQ$ of finite automata is complete for iteration categories iff for every finite simple group $G$ there is an automaton $\bQ \in \cQ$ such that $G$ is a quotient of a group in the monoid $M(\bQ)$ of the automaton $\bQ$. We also prove a stronger result that concerns identities associated with finite automata with a distinguished initial state.