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 are called values and denoted by , , .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 (),in are denoted , .
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 is a (possibly empty) sequence of atoms enclosed in angle brackets. Paths are denoted by P. For N a node, P a path and a (possibly empty) sequence of atoms, an equation of the form is called an extensional sentence. Intuitively, an extensional sentence states that the value associated with the path P at node N is . For a (possibly empty) sequence of value descriptors, an equation of the form is called a definitional sentence. A definitional sentence specifies a property of the node N, namely that the path P is associated with the value defined by the sequence of value descriptors .
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 T is called a DATR theory. In principle, a DATR theory T may consist of any combination of DATR sentences, either definitional or extensional, but in practice, DATR theories are more restricted than this. The theory T 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:
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 values. We continue to oversimplify matters somewhat. The meaning of a node depends on the global context, and a node thus really denotes a function from global contexts to partial functions from paths to values. Though important, this point is tangential to the issue addressed here. 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 T and node N of T, we write to denote that subset of the sentences in T that relate to the node N. That is:
The set is referred to as the definition of N (in T).