Inference in DATR

  The problem of constructing an explicit theory of inference for DATR was originally addressed in E&G 1989a. In this work, an attempt is made to set out a logic of DATR statements. Consider for example the following rule of inference, adapted from E&G 1989a.

$$\infer[]{N_1:P_1 == \alpha}{N_1:P_1 == N_2:P_2, & N_2:P_2 == \alpha}$$

The premises are definitional sentences which can be read: ``the value of path P<sub>1</sub> at node N<sub>1</sub> is (inherited from) the value of path P<sub>2</sub> at N<sub>2</sub>'' and ``the value of path P₂ at node N₂ is $\alpha$'', respectively. Given the premises, the rule licences the conclusion ``the value of path P₁ at node N₁ is $\alpha$''. Thus, the rule captures a logical relationship between DATR sentences. For a given DATR theory T, rules of this kind may be used to deduce additional sentences as theorems of T.

In contrast, the system of inference described here characterizes a relationship between DATR expressions (i.e., sequences of descriptors) and the values they may be used to compute. As an example, consider the following (simplified) rule of the operational semantics:

$$\begin{array} {c} \mbox{if } N_1:P_1 == \phi \in \mbox{\em T... ...1 \Longrightarrow\alpha}{\phi \Longrightarrow\alpha}\end{array}$$

The rule is applicable just in case the theory $\mbox{\em T}$ contains a definitional sentence $N_1:P_1 == \phi$. It states that if the sequence of value descriptors $\phi$ on the right of the sentence evaluates to ($\Longrightarrow$) the sequence of atoms $\alpha$, then it may be concluded that the node/path pair N₁:P₁ also evaluates to $\alpha$. Rules of this kind may be used to provide an inductive definition of an evaluation relation between DATR expressions and their values.

Both approaches to inference in DATR aim to provide a system of deduction that makes it possible to determine formally, for a given DATR theory T, what follows from the statements in T. The primary interest lies in deducing statements about the values associated with particular node/path pairs defined within the theory. Unfortunately, the proof rules described in E&G 1989a are not sufficiently general to support all of the required inferences, and it is not obvious that the approach can be extended appropriately to cover all of the available DATR constructs. A particular problem concerns DATR's notion of non-local or global inheritance. The value expressed by a global inheritance descriptor depends on more than just the properties of the nodes specified by the definitional sentences of a theory. In fact, it only makes sense to talk about the value of a global descriptor relative to a given context of evaluation, or global context. Because the proof rules of E&G 1989a just talk about DATR sentences, which do not make explicit reference to context, it is not possible to give a satisfactory account of the global inheritance mechanism. The problem is partially overcome in E&G 1989a by making use of a second kind of DATR sentence (the extensional sentence) which effectively provides an implicit reference to global context. However, this approach relies on the overly-restrictive assumption that there is at most one global inheritance descriptor on the right of each definitional sentence.

The evaluation semantics described in the following sections provides a perspicuous treatment of both local and global inheritance in DATR. The rules capture the essential details of the process of evaluating DATR expressions, and for this reason should prove of use to the language implementer.