On subsumption and semiunification in feature algebras

We consider a generalization of term subsumption, or matching, to a class of mathematical structures which we call feature algebras. We show how these generalize both first-order terms and the feature structures used in computational linguistics. The notion of term subsumption generalizes to a natural notion of algebra homomorphism. In the setting of feature algebras, unification, corresponds naturally to solving constraints involving equalities between strings of unary function symbols, and semiunification also allows inequalities representing subsumption constraints. Our generalization allows us to show that the semiunification problem for finite feature algebras is undecidable. This implies that the corresponding problem for rational trees (cyclic terms) is also undecidable.