As a point of departure, this section provides rules of
inference for a restricted variant of DATR which lacks both global
inheritance and the default mechanism. This variant will be referred to
as
. The syntax of
is as given in
Section 3.1.4 except, of course, that the three forms of
global inheritance descriptor are omitted. An example of a simple
theory is presented below:
NOUN:
<cat> == noun
<suff> == s.
Llama:
<cat> == NOUN
<root> == llama
<sing> == <root>
<plur> == <root> NOUN:<suff>.
The
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
to mean that the sequences of descriptors
evaluates to the
sequence of atoms
. With respect to the
theory
above we should expect that
and that
, amongst other things.
Figure 3: Evaluation semantics for DATR
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
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.
The final rule of Figure 3 deals with DATR's evaluable
path construct. Consider a value descriptor of the form
. To determine the value of the descriptor it is
first necessary to establish what path is specified by the path
descriptor
. This involves evaluating the descriptor
and then plugging in the resultant value
to
obtain the path
. The required value is then obtained by
evaluating
. The rule for Evaluable Paths
provides a general statement of this process: if a sequence of value
descriptors
evaluates to
and
evaluates
to
, then
also evaluates to
.