Algebraically complete semirings and Greibach normal form

We give inequational and equational axioms for semirings with a fixed-point operator and formally develop a fragment of the theory of context-free languages. In particular, we show that Greibach’s normal form theorem depends only on a few equational properties of least pre-fixed points in semirings, and eliminations of chain and deletion rules depend on their inequational properties (and the idempotence of addition). It follows that these normal form theorems also hold in non-continuous semirings having enough fixed points.