Matrix and matricial iteration theories. II (Q2366692)

In Part I (reviewed above), the authors investigated matrix iteration theories. The present paper contains similar results for \textit{matricial} iteration theories. A matricial theory \(T=\text{Matr}(S;V)\) is an algebraic theory whose morphisms \(n\to p\) consist of pairs \((a;x)\), where \(a\) is an \(n\) by \(p\) matrix over a semiring \(S\) and where \(x\) is an element in the monoid \(V^ n\). The authors characterize the matricial iteration theories \(\text{Matr}(S;V)\) by identities involving theory operations, a star operation \(S\to S\) and an omega operation \(S\to V\). The initial matricial iteration theory is described explicitly. An extension theory for matricial theories, analogous to the extension theorem in Part I for matrix theories, is provided. The obtained results are applied to: (1) finding equational axioms for logical systems in which all valid identities of regular languages and closed regular \(\omega\)-languages are derivable, and to (2) program correctness logic.