DATR's local inheritance mechanism provides for a simple kind of data abstraction. Thus, in the tex2html_wrap_inline4445 theory above, information about the plural suffix is stated once and for all at the abstract NOUN node. It is then available to any instance of NOUN such as Llama via local inheritance. On the other hand, information about the formation of singular and plural forms of llama must still be located at the Llama node, even though the processes involved are entirely regular. To overcome this problem, DATR provides a second form of inheritance: global inheritance. This section provides an evaluation semantics for a default-free variant of DATR\ with both local and global inheritance ( tex2html_wrap_inline4559 ). A simple tex2html_wrap_inline4559 theory is shown below:
NOUN: <cat> == noun <suff> == s. <sing> == "<root>" <plur> == "<root>" <suff>. Llama: <cat> == NOUN <root> == llama <sing> == NOUN <plur> == NOUN.The new theory is equivalent to that given previously in the sense that it associates exactly the same values with node/path pairs. However, in the tex2html_wrap_inline4559 theory global inheritance is used to capture the relevant generalizations about the singular and plural forms of nouns in English. Thus, the sentence NOUN:<sing> == "<root>" states that the singular form of any noun is identical to its root (whatever that may be). The sentence NOUN:<plur> == "<root>" <suff> states that the plural is obtained by attaching the (plural) suffix to the root.
To understand the way in which global inheritance works, it is necessary to introduce DATR's notion of global context. Suppose that we wish to determine the value of Llama:<sing> in the example tex2html_wrap_inline4559 theory. Initially, the global context will be the pair (Llama,sing). From the theory, the value of Llama:<sing> is to be inherited (locally) from NOUN:<sing>, which in turn inherits its value (globally) from the quoted path "<root>". To evaluate the quoted path, the global context is examined to find the current global node (this is Llama) and the value of "<root>" is then obtained by evaluating Llama:<root>, which yields llama as required.
More generally, the global context is used to fill in the missing node (path) when a quoted path (node) is encountered. In addition, as a side effect of evaluating a global inheritance descriptor the global context is updated. Thus, after encountering the quoted path "<root>" in the preceding example, the global context is changed from (Llama,sing) to (Llama,root). That is, the path component of the context is set to the new global path root.
Let tex2html_wrap_inline3951 be a tex2html_wrap_inline4559 theory defined with respect to the set of nodes NODE and the set of atoms ATOM. The set CONT of ( global) contexts of tex2html_wrap_inline4421 is defined as the set of all pairs of the form tex2html_wrap_inline4621 , for tex2html_wrap_inline3907 and tex2html_wrap_inline3927 . Contexts are denoted by C. The evaluation relation tex2html_wrap_inline4427 is now taken to be a mapping from elements of tex2html_wrap_inline4631 to tex2html_wrap_inline3885 . We write
displaymath4549
to mean that tex2html_wrap_inline3899 evaluates to tex2html_wrap_inline3889 in the global context C.
To axiomatise the new evaluation relation, the tex2html_wrap_inline4445 rules are modified to incorporate the global context parameter. For example, the rule for Evaluable Paths now becomes:
displaymath4550
Two similar rules are required for sentences containing quoted descriptors of the forms tex2html_wrap_inline4643 and tex2html_wrap_inline4645 . Note that the context C plays no special role here, but is simply carried unchanged from premises to conclusion. The rules for Values, Definitions and Sequences are modified in an entirely similar manner. Finally, to capture the way in which values are derived for quoted descriptors three entirely new rules are required, one for each of the quoted forms. These rules are shown in Figure 4.
[画像:figure1126]
Figure 4: Evaluation of quoted descriptors
Consider for example the Quoted Path rule. The premise states that tex2html_wrap_inline4649 evaluates to tex2html_wrap_inline3889 in the global context tex2html_wrap_inline4621 . Given this, the rule licences the conclusion that the quoted descriptor tex2html_wrap_inline4655 also evaluates to tex2html_wrap_inline3889 in any context with the same node component N. In other words, to evaluate a quoted path tex2html_wrap_inline4655 in a context tex2html_wrap_inline4663 , just evaluate the local descriptor tex2html_wrap_inline4665 in the updated global context tex2html_wrap_inline4621 . The rules dealing with global node/path pairs, and global nodes work in a similar way.
The following proof illustrates the use of the Quoted Path rule ( tex2html_wrap_inline4669 ). It demonstrates that Llama:<sing> evaluates to llama, given the tex2html_wrap_inline4559 theory, and when the initial global context is taken to be (Llama,sing).
