Order-sorted feature theory unification

AbstractOrder-sorted feature (OSF) terms provide an adequate representation for objects as flexible records. They are sorted, attributed, possibly nested structures, ordered thanks to a subsort ordering. Sorts definitions offer the functionality of classes imposing structural constraints on objects. These constraints involve variable sorting and equations among feature paths, including self-reference. Formally, sort definitions may be seen as axioms forming an OSF theory. OSF theory unification is the process of normalizing an OSF term taking into account sort definitions, enforcing structural constraints imposed by an OSF theory. It allows objects to inherit, and thus abide by, constraints from their classes. We propose a formal system that logically models record objects with (possibly recursive) class definitions accommodating multiple inheritance. We show that OSF theory unification is undecidable in general. However, we give a set of confluent normalization rules which is complete for detecting the inconsistency of an object with respect to an OSF theory. Furthermore, a subset consisting of all rules but one is confluent and terminating. This yields a practical complete normalization strategy, as well as an effective compilation scheme