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 , .

- for any
- For any and :

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: