Free polynomial strong bimonoids

Recently, in weighted automata theory the weight structure of strong bimonoids has found much interest; they form a generalization of semirings and are closely related to near-semirings studied in algebra. Here, we define polynomials over a set X of indeterminates as well as an addition and a multiplication. We show that with these operations, they form a right-distributive strong bimonoid, that this polynomial strong bimonoid is free over X in the class of all right-distributive strong bimonoids and that it is both left- and right-cancellative. We show by purely algebraic reasoning that two arbitrary terms are equivalent modulo the laws of right-distributive strong bimonoids if and only if their representing polynomials are equivalent by the laws of only associativity and commutativity of addition and associativity of multiplication. We give effective procedures for constructing the representing polynomials. As a consequence, we obtain that the equivalence of arbitrary terms modulo the laws of right-distributive strong bimonoids can be decided in exponential time. Using term-rewriting methods, we show that each term can be reduced to a unique polynomial as normal form. We also derive corresponding results for the free idempotent right-distributive polynomial strong bimonoid over X. We construct an idempotent strong bimonoid which is weakly locally finite but not locally finite and show an application of it in weighted automata theory.