Proper Semirings and Proper Convex Functors

TL;DR

This paper extends the concept of properness from semirings to functors, providing a method to prove properness for new classes, which has implications for automata equivalence and probabilistic systems.

Contribution

It introduces a general method for establishing properness of functors and applies it to novel cases involving convex algebras and real number semirings.

Findings

Properness of positive rational and real semirings established.

Properness of functors on convex algebras demonstrated.

Method enables broader applications in automata and probabilistic systems.

Abstract

Esik and Maletti introduced the notion of a proper semiring and proved that some important (classes of) semirings -- Noetherian semirings, natural numbers -- are proper. Properness matters as the equivalence problem for weighted automata over a semiring which is proper and finitely and effectively presented is decidable. Milius generalised the notion of properness from a semiring to a functor. As a consequence, a semiring is proper if and only if its associated "cubic functor" is proper. Moreover, properness of a functor renders soundness and completeness proofs for axiomatizations of equivalent behaviour. In this paper we provide a method for proving properness of functors, and instantiate it to cover both the known cases and several novel ones: (1) properness of the semirings of positive rationals and positive reals, via properness of the corresponding cubic functors; and (2) properness of two functors on (positive) convex algebras. The latter functors are important for axiomatizing trace equivalence of probabilistic transition systems. Our proofs rely on results that stretch all the way back to Hilbert and Minkowski.