The semantics of
employing labels *L*, constants *C*, and
variables *V* is defined with respect to the domain of *feature
graphs*, built from *L*, *C*, and *V*.
A feature graph is a directed
graph which is finite, rooted, and connected. Furthermore, the labels
of the edges leaving a node must be pairwise distinct. Every inner
node of a feature graph is a variable, and every terminal node is
either a variable or a constant. Edges are triples
X*l**t*
such that
X is a variable,
*l* is a label and *t* is
either a variable or a constant.

- a pair (c,) where c is a constant and is the empty set; or
- a pair
(X
_{0},*E*) where X_{0}is a variable (the root) and*E*is a set of edges such that- if
X
*l**s*and X*l**t*are both in*E*then*s*=*t*; i.e. labels are functional; and - if
X
*l**s*is in*E*then X is reachable from X_{0}by the edges in*E*; i.e. feature graphs are connected.

- if
X

The following notation to traverse feature graphs is introduced. If
*F* is a feature graph and *p*
is a path, then *F*/*p* is the variable or constant that is reached from
the root of *F* where the labels
in the path correspond to the labels of the edges. For example
consider the following feature graph

which is graphically represented in figure 2.1.

More formally, for
*p* = *l*_{1}...*l*_{k} a path, and *t* a node
(variable or atom), define *t*/*p* to be the node given as follows. If
*k* = 0 then
*t*/*p* = _{def}*t*. Otherwise,
*t*/*l*_{1}...*l*_{k} is defined
to be the node *t'* if there is an edge labelled
*l*_{1} from *t*
to *t''* and
*t'* = *t''*/*l*_{2}...*l*_{k} (otherwise
*t*/*l*_{1}...*l*_{k} is undefined). Furthermore, for *F* a feature graph with
root
X_{0},
*F*/*p* = _{def}X_{0}/*p*.

A feature graph *F* is called a *subgraph* of a feature graph *F'*
if the root of *F* is a variable or atom occurring in *F'* and every
edge of *F* is an edge of *F'*. If *F* is a feature graph and *s* a
node of *F*, then *F*^{s} denotes the unique maximal subgraph of *F*
of which the root is *s*. In that case, *F*^{s} has as its root the node *s*,
and as its edges are all those edges of the form *tlt'* present in *F*
such that both *t*, *t'* are reachable from *s* in *F*. For example, if
*F*_{1} is the feature graph in figure 2.1, then we have:

Furthermore, for *F* a feature graph and *p* a path, *F*^{p} denotes
the subgraph *F*^{s} where *F*/*p* = *s*, if
this is defined.
For example:

Otherwise *F*^{p} is undefined.

1998-09-30