The work described here fulfills one of the objectives of the DATR programme: to provide the language with an explicit, declarative semantics. We have presented a formal model of DATR as a language for defining partial functions and this model has been contrasted with an informal view of DATR as a language for representing inheritance hierarchies. The approach provides a transparent treatment of DATR's notion of (local and global) context and accounts for DATR's default mechanism by regarding value descriptors (semantically) as families of values indexed by paths.
The provision of a formal semantics for DATR is important for several reasons. First, it provides the users of the language with a concise, implementation-independent account of the meaning of DATR\ theories. Second, it serves as a standard against which other, operational definitions of the formalism can be judged. Indeed, in the absence of such a standard, it is impossible to demonstrate formally the correctness of novel implementation strategies. Third, the process of formalisation itself aids our understanding of the language and its relationship to other non-monotonic, attribute-value formalisms. Finally, the semantics presented here provides a sound basis for subsequent investigations into the mathematical and computational properties of DATR.
