This section describes an operational semantics for DATR theories. The semantics is presented as a set of inference rules that axiomatises the evaluation relationship for DATR expressions. The inference rules provide a clear picture of the way in which DATR works, and should lead to a better understanding of the mathematical and computational properties of the language.
The original 1989 publications on DATR sought to provide the language with a formal theory of inference (E&G 1989a) and a model-theoretic semantics (E&G 1989b). Unfortunately, the definitions set out in these papers are not general enough to cover all of the constructs available in the DATR language. In particular, they fail to provide a full and correct treatment of DATR's notion of global inheritance, or the widely-used evaluable path construct. A denotational semantics for DATR that covers all of the major constructs is presented in Section 4. However, it still remains to provide a suitably general, formal theory of inference for DATR, and it is this objective that is addressed here. More precisely, an operational semantics for DATR\ is provided, comprising a formal system of rules that axiomatises the essential details of how DATR expressions are evaluated. Section 3.1.4 has already provided a concise presentation of the syntax of the DATR language. Section 5.1 compares the formal theory of inference presented here to that given in 1989. Section 5.2 introduces the inference rules for a restricted version of DATR that is limited to local inheritance. Section 5.3 extends the rules to allow global inheritance. Section 5.4 then revises the theory to bring in path extensions and defaults, thus covering the full DATR\ language. Finally, in Section 5.5, we make some comments about the theory of inference presented here.