Unification and Matching in Separable Theories – technicalities

The present work studies problems of unification and matching in equational theories based on idempotent semirings. We concentrate on matching because for the three particular theories that we started from (i.e., constraint semirings (CS), synchronous actions algebra (SAA), and idempotent semirings (IS)), we show that their unification prob-lems are undecidable. On the other hand, their matching problems are decidable and a general pattern can be drawn. We build this pattern into a general matching algorithm for theories that we call separable. In particular we exemplify how this general algorithm is applicable to the three theories CS, SAA, and IS. Separability is a general re-quirement, satisfied by theories based on idempotent semirings; yet separability is similar to the finite variant property which does not hold for theories with distributivity, like idempotent semirings. If fi-nite variant property is useful in solving unification, separability is useful in solving matching, where unification may be undecidable