This section provides the notational conventions and syntactic framework for the subsequent formal discussion of DATR's semantics (Section 4) and theory of inference (Section 5).
Let NODE and ATOM be finite sets of symbols. Elements of NODE are called nodes and denoted by N. Elements of ATOM are called atoms and denoted by a. Elements of tex2html_wrap_inline3885 are called values and denoted by tex2html_wrap_inline3887 , tex2html_wrap_inline3889 , tex2html_wrap_inline3891 . The set DESC of DATR value descriptors (or simply descriptors), and denoted by d, is built up from the nodes and atoms as shown below. In the following, sequences of descriptors ( tex2html_wrap_inline3895 ),in tex2html_wrap_inline3897 are denoted tex2html_wrap_inline3899 , tex2html_wrap_inline3901 .
Value descriptors are either atoms or inheritance descriptors, where an inheritance descriptor is further distinguished as either local (unquoted) or global (quoted). There is just one kind of local descriptor (node/path), but three kinds of global descriptor (node/path, path and node). The syntax presented informally in Section 3.1.2, above, and in E&G (1989a, 1989b) permits nodes and paths to stand as local descriptors. However, these additional forms can be viewed as conventional abbreviations, in the appropriate syntactic context, for node/path pairs.
A path tex2html_wrap_inline3919 is a (possibly empty) sequence of atoms enclosed in angle brackets. Paths are denoted by P. For N a node, P a path and tex2html_wrap_inline3927 a (possibly empty) sequence of atoms, an equation of the form tex2html_wrap_inline3929 is called an extensional sentence. Intuitively, an extensional sentence tex2html_wrap_inline3929 states that the value associated with the path P at node N is tex2html_wrap_inline3887 . For tex2html_wrap_inline3899 a (possibly empty) sequence of value descriptors, an equation of the form tex2html_wrap_inline3941 is called a definitional sentence. A definitional sentence tex2html_wrap_inline3941 specifies a property of the node N, namely that the path P is associated with the value defined by the sequence of value descriptors tex2html_wrap_inline3899 .
A collection of equations can be used to specify the properties of different nodes in terms of one another, and a finite set of DATR\ sentences tex2html_wrap_inline3951 is called a DATR theory. In principle, a DATR theory tex2html_wrap_inline3951 may consist of any combination of DATR\ sentences, either definitional or extensional, but in practice, DATR\ theories are more restricted than this. The theory tex2html_wrap_inline3951 is said to be definitional if it consists solely of definitional sentences and it is said to be functional if it meets the following condition:
displaymath3879
Functionality for DATR theories, as defined above, is really a syntactic notion. However, it approximates a deeper, semantic requirement that the nodes should correspond to (partial) functions from paths to valuesgif. Functionality is discussed in greater detail in Section 3.1.5, below.
In the formal semantics (4) and inference (5) sections of this document, we will use the term (DATR) theory always in the sense functional, definitional (DATR) theory. For a given DATR theory tex2html_wrap_inline3951 and node N of tex2html_wrap_inline3951 , we write tex2html_wrap_inline3965 to denote that subset of the sentences in tex2html_wrap_inline3951 that relate to the node N. That is:
eqnarray576
The set tex2html_wrap_inline3965 is referred to as the definition of N (in tex2html_wrap_inline3951 ).