Feature graphs

The semantics of $\cal {L}$ 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 Xlt such that X is a variable, l is a label and t is either a variable or a constant.

Definition 5 (Feature graphs)   A feature graph is

• a pair (c,$\emptyset$) where c is a constant and $\emptyset$ is the empty set; or
• a pair (X₀, E) where X₀ is a variable (the root) and E is a set of edges such that
  • if Xls and Xlt are both in E then s = t; i.e. labels are functional; and
  • if Xls is in E then X is reachable from X₀ by the edges in E; i.e. feature graphs are connected.

Note that this definition implies that no edges leave constant nodes, because edges always start with a variable. A node s is reachable from a node t in a feature graph F iff t $\rightarrow^{*}_{F}$ s where $\rightarrow^{*}_{F}$ is the transitive and reflexive closure of $\rightarrow_{F}^{}$ which is a binary relation on the nodes occurring in F:

t $$\rightarrow_{F}^{}$$ s iff tls $$\in$$ $$\mbox{the set of edges of $F$}$$

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

$$F_1 = (\mbox{\rm X}_{0},\{\mbox{\rm X}_{0}\mbox{\it l}_{1}\m... ...rm c}_{2}, \mbox{\rm X}_{1}\mbox{\it l}_{4}\mbox{\rm c}_{2}\})$$
which is graphically represented in figure 2.1.

Figure 2.1: Feature graph F₁

The expression F₁/l₂l₄ denotes c₂; and F₁/l₂ = X₁. Furthermore, F₁/l₃ is undefined.

More formally, for p = l₁...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 = _deft. Otherwise, t/l₁...l_k is defined to be the node t' if there is an edge labelled l₁ from t to t'' and t' = t''/l₂...l_k (otherwise t/l₁...l_k is undefined). Furthermore, for F a feature graph with root X₀, F/p = _defX₀/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₁ is the feature graph in figure 2.1, then we have:

$$F_1^{\mbox{\rm X}_{1}} = (\mbox{\rm X}_{1},\{\mbox{\rm X}_{1... ...\rm c}_{2},\mbox{\rm X}_{1}\mbox{\it l}_{4}\mbox{\rm c}_{2}\})$$
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:

$$F_1^{ \mbox{\it l}_{2}} = (\mbox{\rm X}_{1},\{\mbox{\rm X}_{... ...\rm c}_{2},\mbox{\rm X}_{1}\mbox{\it l}_{4}\mbox{\rm c}_{2}\})$$
Otherwise F^p is undefined.