NOUN:
<cat> == noun
<suff> == s.
Llama:
<cat> == NOUN
<root> == llama
<sing> == <root>
<plur> == <root> NOUN:<suff>.
The
theory defines the
properties of two nodes, NOUN and Llama. The
definitional sentences specify values for node/path pairs, where the
specification is either direct (a particular value is
exhibited), or indirect (the value is obtained by local
inheritance). For example, the value of the node/path pair
NOUN:<cat> is specified directly as noun. In
contrast, the node/path pair Llama:<cat> obtains its value
indirectly, by local inheritance from the value of
NOUN:<cat>. Thus Llama:<cat> also has the
value noun. The value of Llama:<plur> is
specified indirectly by a sequence of descriptors
Llama:<root> NOUN:<suff>. Intuitively,
the required value is obtained by concatenating the values of the
descriptors Llama:<root> and NOUN:<suff>,
yielding llama s.
We wish to provide an inductive
definition of an evaluation relation (denoted
) between
sequences of DATR descriptors in
and sequences of atoms
(i.e., values) in
. We write
![]()
The formal definition of
for
is provided by just
four rules of inference, as shown in Figure 3. The rule
for Values states simply that a sequence of atoms evaluates to
itself. Another way of thinking about this is that atom sequences are
basic, and thus cannot be evaluated further. The rule for
Definitions was briefly discussed in the previous section. It
permits inferences to be made about the values associated with node/path
pairs, provided that the theory T contains the appropriate
definitional sentences. The third rule deals with the evaluation of
sequences of descriptors, by breaking them up into shorter
sequences. Given that the values of the sequences
and
are
known, then the value of
can be obtained simply by
concatenation. Note that this rule introduces some non-determinism,
since in general there is more than one way to break up a sequence of
value descriptors. However, whichever way the sequence is broken up, the
result (i.e., value obtained) should be the same. The following proof
serves to illustrate the use of the rules Val, Def and Seq. It
establishes formally that the node/path pair Llama:<plur>
does indeed evaluate to llama s given the
theory above.
![\begin{displaymath}
\infer[\mbox{\em Def\/}]{{\tt \mbox {\tt Llama}\!:\!{\tt <pl...
...{\em Val\/}]{\mbox{\tt s}\Longrightarrow\mbox{\tt s}}{}
}
}
}\end{displaymath}](datrimg82.gif)
