Ordering Constraints over Feature Trees.
Feature trees are the formal basis for algorithms manipulating record like structures in constraint programming, computational linguistics and in concrete applications like software configuration management. Feature trees model records, and constraints over feature trees yield extensible and modular record descriptions. We introduce the constraint system FEAT of ordering constraints interpreted over feature trees. Under the view that feature trees the relation \leq corresponds to the information ordering (carries less information than). We present two algorithms in cubic time, one for the satisfiability problem and one for the entailment problem of FEAT.  We show that FEAT has the independence property. We are thus able to handle negative conjuncts via entailment and obtain a cubic algorithm that decides the satisfiability of conjunctions of positive and negated ordering constraints over feature trees. Furthermore, we reduce the satisfiability problem of Drres weak subsumption constraints to the satisfiability problem of FEAT and improve the complexity bound for solving weak subsumption constraints from O(n^5) to O(n^3).
Introduction
Feature constraints have been used for describing records in constraint programming
[2, 24, 23] and record like structures in computational linguistics [13, 12, 20, 18, 19].
Following [3, 5, 4] we consider feature constraints as predicate logic formulae that are
interpreted in the structure of feature trees.
A feature tree is a possibly infinite tree with unordered labeled edges and with possibly
labeled nodes. Edge labels are functional; i.e., the labels of the edges departing
from the same node must be pairwise different. Under the view that feature trees represent
symbolic information, the feature tree t 1 represents less information than the feature
tree t 2 if t 1 has fewer edges and node
labels than t 2 . The relation - that we define
corresponds to the information ordering
in precisely this sense. Algebraically,
there is a homomorphic embed-
wine
red
color -
wine
red 1997
color year
ding from t 1 to t 2 (i.e., a mapping from nodes in t 1 to nodes in t 2 under which the node
labeling is invariant). An example is given in the picture.
We introduce the constraint system FT- of information ordering constraints over feature
trees. The system FT- is obtained by adding ordering constraints to the constraint
system FT [3]. The syntax of FT- constraints j is defined by
where x and x 0 are variables and a is a label. The semantics of FT- is given by the
interpretation over feature trees where the symbol - is interpreted as information ordering
on feature trees. The semantics of x[a]y and a(x) are defined as in FT . For in-
stance, both trees depicted above are possible values for x in solutions of the constraint
It is clear that FT- is more expressive than FT since the information ordering is antisymmetric
(i.e., As we show in the paper, FT- is
strictly more expressive than FT . For instance, no constraint in FT can be equivalent to
x-x 0 . Also, we do not know of any formula over FT (even with existential quantifiers)
equivalent to 9x(x 1 -x- x 2 -x)-9x(x 1 -x- x 3 -x); this FT- formula expresses that x 1
is unifiable with both x 2 and x 3 (but does not imply unifiability of x 2 and x 3 ).
We show that the satisfiability problem of conjunctions of positive and negative FT-
constraints j-:j 1 -:j n is decidable in O(n 3 ). This result includes a decision
procedure for the entailment problem of the form j 0
if and only if the formula j 0 -:j is unsatisfiable. To establish our result, we prove that
FT- has the fundamental independence property (similar to its relatives RT [6], FT [3],
and CFT [24]).
We reduce the satisfiability problem of D-orre's weak-subsumption constraints [7] over
feature algebras linearly to the one in FT- . Thereby, our algorithm improves on the best
known satisfiability test for weak subsumption constraints which uses finite automata
techniques and has an O(n 5 )-complexity bound [7].
Plan of the Paper. Section 2 surveys related work. Section 3 defines FT- . Section 4
presents the satisfiability test for FT- constraints. Section 8 contains the completeness
proof. Section 5 presents the entailment test for FT- constraints, and proves the independence
property of FT- . Section 6 defines weak subsumption constraints and reduces
their satisfiability problem to the one of FT- constraints. Section 7 shows that FT- is
strictly more expressive than FT .
Related Work
Ines Constraints. In previous work [17], we have introduced the constraint system
INES of inclusion constraints over non-empty sets of trees and a cubic satisfiability test.
The satisfiability test for FT- is inspired by and subsumes the one for INES. However, the
entailment problems for FT- and INES constraints are different. The entailment problem
of INES constraints is coNP-hard [16]. Intuitively, the entailment problem of FT- is less
expressive than the one of INES because an FT- constraint j cannot uniquely describe a
single feature tree (in absence of arity constraints); in contrast, INES constraints (which
are inclusions between first-order terms with an implicit arity restriction) can uniquely
describe a constructor tree as a singleton set. For instance, the INES constraint x'a
describes the singleton fag. As a consequence, the entailment proposition x'a-a'y
x'y holds in INES. No similar entailment phenomenon exists for FT- .
Feature Constraints. The constraint system CFT [24] extends FT by arity constraints
of the form xf f saying that the denotation of x has subtrees exactly at the features
rational tree constraint system RT [6]
but provides finer-grained constraints. The system EF [25] extends CFT by feature
constraints x[y]z, providing for first-class features. Complete axiomatizations for FT
and CFT have been given in [5] and [4], respectively. The satisfiability of EF constraints
is shown NP-hard in [25]. The system FT- (sort) extends FT- by allowing a
partial order on labels [15].
Subsumption Constraints. Subsumption is an ordering on the domain of feature alge-
bras. Subsumption constraints have been considered in the context of unification-based
grammars to model coordination phenomena in natural language [9, 7, 21]. There, one
wants to express that two feature structures representing different parts of speech share
common properties. For example, the analysis of "programming" and "linguistics" in
the phrase
Feature constraints for [ NP programming] and [ NP linguistics]
should share (but might refine differently) the information common to all noun phrases.
Since the satisfiability of subsumption constraints is undecidable [9], D-orre proposed
subsumption as an decidable approximation of subsumption. As we show, the
information ordering over feature trees (as investigated in this paper) coincides with the
subsumption ordering interpreted over (the algebra of) feature trees.
Independent Constraint Systems. A constraint system has the fundamental independence
property if negated conjuncts are independent from each other, or: its constraints
cannot express disjunctions (we will give a formal definition later). Apart from the mentioned
tree constraint systems RT , FT , CFT [6, 1, 24, 3], constraint systems with the
independence property include linear equations over the real numbers [14], or infinite
boolean algebras with positive constraints [10].
3 Syntax and Semantics of FT-
The constraint system FT- is defined by a set of constraints together with an interpretation
over feature trees. We assume an infinite set of variables ranged over by x;y;z,
and an infinite set L of labels ranged over by a;b.
Feature Trees. A path p is a finite sequence of labels. The empty path is denoted by e
and the free-monoid concatenation of paths p and p 0 as pp 0 ; we have
Given paths p and q, p 0 is called a prefix of p if
domain is a non-empty prefix closed set of paths. A feature tree t is a pair (D; L)
consisting of a tree domain D and partial labeling function L : D * L . Given a feature
tree t, we write D t for its tree domain and L t for its labeling function. The set of all
feature trees is denoted by F . A feature tree is called finite if its tree domain is finite,
and infinite otherwise.
Syntax. An FT- constraint j is defined by the following abstract syntax.
An FT- constraint is a conjunction of basic constraints which are either inclusion
constraints x-y, labeling constraints a(x), selection constraints x[a]y, or compatibility
constraints x-y. Compatibility constraints are needed in our algorithm and can be
expressed by first-order formulae over inclusion constraints (see Proposition 1). We
identify to associativity and commutativity of conjunction, i.e.,
we view j as a multiset of inclusion, labeling, selection, and compatibility constraints.
We write j in j 0 if all conjuncts in j are contained in j 0 . The size of a constraint j is
defined as the number of label and variable occurrences in j.
Semantics. We next define the structure F over feature trees in which we interpret
constraints. The signature of F contains the binary relation symbols - and - and
for every label a a unary relation symbol a() and a binary relation symbol [a]. In F
these relation symbols are interpreted
is a partial function (on D t 1
Let F denote first-order formulae built from FT- constraints with the usual first order
connectives. We call F satisfiable (valid) if F is satisfiable (valid) in the structure F .
We say that F entails F 0 , written F is valid, and that F is equivalent
to F 0 if F 1 $F 2 is valid. We denote with V (F) the set of variables occurring free in F
and with L(F) the set of labels occurring in F.
Proposition 1. The formulae x-y and 9z(x-z- y-z) are equivalent in F .
Proof. Let s be a variable assignment into F which also is a solution of the formula
9z(x-z- y-z). Since L s(x) [L s(y) ' L s(z) and L s(z) is a partial function, L s(x) [L s(y) is
also a partial function. Hence s is a solution of x-y. Conversely, if s is a solution of x-y
then L s(x) [L s(y) is a partial function. Thus, the pair
is a feature tree and the variable assignment s 0 defined by s 0
for x 6= z is a solution of x-z- y-z. 2
4 Satisfiability Test
We present a set of axioms valid for FT- and then interpret these axioms as an algorithm
that solves the satisfiability problem of FT- . The axioms and the algorithm are inspired
by the ones for INES constraints presented in [17].

Table

contains five axiom schemes F1 - F5 that we regard as sets of axioms. The
union of these sets of axioms is denoted by F, i.e., For instance, an
axiom scheme x-x represents the infinite set of axioms obtained by instantiation of the
meta variable x. An axiom is either a constraint j, an implication between constraints
or an implication
Proposition 2. The structure F is a model of the axioms in F.
F1 x-x and x-y- y-z ! x-z
false for a 6= b

Table

1. Satisfiability of FT- Constraints.
Proof. By a routine check. For illustration, we prove the statement for the second rule
in F3, namely x-y- y-y . The following implications hold:
The Algorithm F. The set of axioms F induces a fixed point algorithm F that, given an
input constraint j, iteratively adds logical consequences of F [fjg to j. (Observe that
actually only constraints of the form x-y and x-y are derived). More precisely, in every
step F inputs a constraint j and terminates with false or outputs a constraint
Termination with false takes place if there exists j 00 in j such that j 00 ! false 2 F.
Output of j-j 0 is possible if j 0 2 F or there exists j 00 in j with
Example 1. Inconsistency can be due to incompatible upper bounds. Consider:
false for a 6= b
We may add x-z by F3:1, then z-x via F3:3, then y-x with F3:2, and finally terminate
with false via F5.
Example 2. We need F4 for deriving the unsatisfiability of the constraint:
Algorithm F may add x-y after several steps as shown in Example 1. Then it may
proceed with x-y 0 via F4 and terminate with false via F5.
Termination. The fixed point algorithm F terminates when reflexivity of inclusion
x-x is restricted to variables x 2 V (j). Given a subset F of F, a constraint j is
called F-closed if algorithm F under this restriction and w.r.t. the axioms in F cannot
proceed on j. Note that false is not F-closed since it is not a constraint by definition.
Example 3. Our control takes care of termination in presence of cycles like x[a]x. For
instance, the following constraint is F-closed.
In particular, F2 and F4 do not loop through the cycle x[a]x infinitely often. This example
also illustrates why the fixed point algorithm would not be terminating if based in
the axiom x[a]x
Proposition 3. If j is a constraint with m variables then algorithm F with input j
terminates under the above control in at most 2
Proof. Since F does not introduce new variables, it may add at most m 2 non-disjointness
constraints x-y and m 2 inclusions x-y. 2
Proposition 4. Every F-closed constraint j is satisfiable over FT- .
Proof. See Section 8. 2
Theorem 5. The satisfiability of FT- constraints can be decided in time O(n 3 ) (offline
and online;see [11]) where n is the constraint size.
Proof. Proposition 2 shows that j is unsatisfiable if F started with j terminates with
false. Proposition 4 proves that j is satisfiable if F started with j terminates with a
constraint. Since F terminates for all input constraints under the above control (Prop.
this yields a effective decision procedure. The main idea of the complexity proof is
that one needs at most O(n 2 ) steps (Prop. 3) each of which can be implemented in
time O(n). The implementation can be organized incrementally by exploiting that algorithm
F leaves the order unspecified in which the axioms are applied. Hence, we obtain
that off-line and on-line complexity are the same. The implementation details and the
complexity proof are omitted here, since they are similar to those presented in [17]. 2
5 Entailment, Independence, Negation
In this section, we give a cubic algorithm testing entailment j 0
We then prove the independence property of FT- . Hence we can solve
conjunctions of positive and negative FT-constraints j-:j
A basic constraint - is a conjunction free constraint j, i.e., given by the following
abstract syntax:
The entailment j 0 is equivalent to the fact that the entailment j j=- holds for all
basic constraints - in j.
Next we characterize entailment problems j 0 syntactically. We say that a constraint
syntactically contains -, written j ' -, if one of the following holds:
exist x 0 , y 0 such that x 0 [a]y 0 in j;
We say that a first-order formula F syntactically contains -, F ' -, if
some j and F 0 such that j ' -.
Lemma 6. Given a F-closed constraint j, we can compute a representation of j in
linear time that allows to test syntactic containment j ' - for all - in time O(1).
Proof. Simple. 2
It is easy to see that syntactic containment is semantically correct, i.e., j ' - implies
-. For deciding entailment, we have to show that our notion of syntactic containment
is semantically complete, i.e., if j 6' - then j 6j= - (Proposition 13). The idea is to
construct a satisfiable extension of j (its saturation) which syntactically and simultaneously
contradicts all - not syntactically contained by j (Lemma 12).
Saturation is defined in terms of two operators G 1 and G 2 on constraints. The operator G 2
is such that G 2 (j) contradicts all - of the form x-y, x-y, and a(x) (i.e., no selection
constraints) which are not syntactically contained in j (Lemma 10). The operator G 1
serves for contradicting selection constraints. For instance, consider j
y-y. In this case, G 1 (j) enforces the existence of the feature a in the denotation
of x by adding to j the constraint x[a]v xa for a fresh variable v xa . Now G 2 (G 1 (j))
is such that it contradicts either y-v xa or v xa -y. (see Example 4). In this sense, G 1 is a
"preprocessor" for G 2 .
Definition 7. Let j be a constraint, v 1 and v 2 distinct fresh variables, and l 1 and l 2
distinct labels. Furthermore, for every pair of variables x; y 2 V (j), and label every
label a 2 L(j) let l x and l xy be fresh labels and v xa a fresh variable. We define G 1 (j)
and G 2 (j) in dependence of
Example 4. Consider the constraint which is F-closed up to trivial
constraints and which does not entail x[a]y. In order to contradict x[a]y we compute
the F-closure of G 1 (j 0 ) which is G 0
v xa -x-x-v xa -y-v xa and observe that it does not v xa -y. By definition of G 2 , G 2 (G 0
contradicts v xa -y. Hence, G 2 (G 0
x[a]y.
Lemma 8. Let j be an F-closed (and hence satisfiable) constraint. Then G 1 (j) is satisfiable
and its F closure G 0
satisfies the following two properties for all basic constraints
-:
1. If j 6' - and V (-) 'V (j), then G 0
2. If j 6' x[a]y then G 0
Proof. The F-closure G 0
1 (j) of G 1 (j) has the following form up-to trivial constraints
and symmetry of compatibility constraints.
exist
exist
exist
instance note that v xa -x 0 - x 0 -v xa in G 0
by clauses (4.2, 4.3) and
reflexivity). All constraints in G 0
either belong to G 1 (j) or a derived from it by
axioms in F. The F-closedness of G 0
1 (j) can be proved by a somewhat tedious case
distinction. The same holds for the two additional properties of G 0
Lemma 9. If j is F-closed then G 2 (j) is satisfiable.
Proof. It is not difficult to show that the constraint part of G 2 (j) is F-closed up to
trivial constraints (x-x and x-x) and symmetric compatibility constraints. The critical
bit is to check that the negated selection constraints added in clause (1) of G 2 (j) are
consistent. Let :9y 0 (y[l x ]y 0 ) in G 2 (j). We must show that G 2 (j) 6j= 9y 0 (y[l x ]y 0 ). Assume
the converse, G 2 (j) by Corollary 27 in Section 8, there exist z and
z 0 such that G 0
By definition of G 2 (j) we know that z = x. However,
(by definition of G 2 clause (1) does not apply.
Thus :9y 0 (y[l x ]y 0 ) cannot be contained in G 2 (j), in contradiction to our assumption. 2
Lemma 10. Let j be an FT-constraint and let - be a basic constraint of the form x-y,
x-y, or a(x) (i.e., not a selection constraint). Then G 2 (j)
Proof. By inspection of the definition of G 2 (j). Clause (1) contradicts entailment of
x-y by j by forcing x to have a feature l x which y must not have. Clause (2) contradicts
x-y by forcing x and y to have a common feature l xy such that the subtrees of x and y
at l xy are incompatible. Clause (3) contradicts a(x) for any label by forcing x to be
unlabeled (i.e., compatible with at least two trees with distinct label). 2
Definition 11 Saturation. Let j be an F-closed constraint and G 0
1 (j) the F-closure of
exists according to Lemma 8. The saturation of j is the formula Sat(j)
given by
Lemma 12. Let j be an F-closed constraint For all - such that V (-) ' V (j), j 6' -
implies
Proof. Let G 0
1 (j) the F-closure of G 1 (j) such that
- is not a selection constraint, then G 2 (G 0
by Lemma 10. Otherwise, let
Lemma 8.2. By Lemma 10, either G 2 (G 0
holds.
In both cases, G 2 (G 0
Proposition 13. The notions of entailment and of syntactic containment coincide for
basic constraints: If j is F-closed and - a basic constraint then j
Proof. We assume j (The converse is correctness of syntactic con-
tainment.) If V (-) 6' V (j) then - is of the form x-x or x-x such that j ' -. Otherwise,
since Sat(j) contains j. Moreover, Sat(j) is
satisfiable (Lemmas 8 and 9) such that Sat(j) 6j= :-. Hence, j ' - by Lemma 12. 2
Theorem 14 Entailment. Entailment problems of the form j 0 can be tested in
cubic time.
Proof. Let n be the size of j 0 -j. To decide j 0 first test whether j 0 is satisfiable.
By Theorem 5 this can be done by computing the F-closure -
this test fails then the entailment test is trivial. Otherwise, from Lemma 12 we obtain
and hence that -
j. There are O(n) such -
and -
0 is of size O(n 2 ), hence, by Lemma 6, this is decidable in time O(n). The overall
complexity sums up to O(n 3
Theorem 15 Independence. The constraint system FT- has the independence prop-
erty; i.e., for every n - 1 and constraints j;j
Proof. Assume
unsatisfiable we are done. Also, if
satisfiable for some j, then j
is. Now let j and j-j i be
satisfiable for all i and let j be F-closed (wlog. by Prop. 2). If there exists i with
for all - syntactically contained by j i , then j and we are done. Otherwise, for all i
there exists - i such that j 6' - i . Lemma 12 yields Sat(j)
satisfiable (Lemma 8) and entails j, this contradicts our assumption that j
Corollary Negation. The satisfiability of conjunctions of positive and negative FT-
constraints j-:j 1 -:j k can be tested in time O(n 3 ) where n is the size of the
given conjunction.
Proof. If j is non-satisfiable then j- n
trivially non-satisfiable. By Proposition
5, satisfiability of j is decidable in time O(n 3 ). Now assume j to be satisfiable. By
the Independence Theorem 15, j- n
nonsatisfiable if and only if j
some i. By Lemma 12 this is equivalent to the existence of i such that for all - if
-. Overall, there are O(n 2 ) candidates - to be tested for syntactic containment
and O(n) possible can be tested in time O(1) such that the total
complexity sums up to time O(n 3
6 Weak Subsumption Constraints
We next introduce weak subsumption constraints that are used in computational linguistics
We show that their satisfiability problem is subsumed by the one for FT- .
Syntax. We assume given a set C of constants c and a set D of features d. We consider
the set of labels subsumption constraint h is a FT- constraint of
the following form.
Note that compatibility constraints do not occur in [7]. We add them here to simplify
our comparison.
Semantics. We interpret weak subsumption constraints over the whole class of feature
algebras with the induced weak subsumption ordering, which we will define below.
A feature algebra A over C and D consists of a set dom A that is called the domain of A ,
a unary relation c() A on dom A for every constant c 2 C , and a binary relation [d] A on
dom A for every feature d 2 D, which satisfy the following properties for all a;a 0 ; a 00 2
dom A , constants c; c
1: if a[d] A a 0 and a[d] A a 00 then a
2: if c 1 (a) A and c 2 (a) A then c
In the literature [22, 7] a slightly different notion of feature algebras with constants has
been considered. We will give a formal comparison between the two notions at the end
of the present section.
Proposition 17. The structure F over L is a feature algebra over C and D.
Proof. The above properties follow from the axioms in F and the antisymmetry of the
information ordering in FT- (x-y- y-x ! x=y). 2
Given a feature algebra A , we define the weak subsumption ordering - A as follows. A
simulation for A is a binary relation D on the domain of A that satisfies the following
properties for all elements a 1 , a 2 , a 0
2 of A's domain:
1: if a 1
2: if a 1 Da 2 ; a 1 [d] A a 0
2 then a 0
subsumption ordering - A of A is the greatest simulation relation for A . The
subsumption relation on A induces a compatibility relation - A :
exists a such that a 1 - A a and a 2 - A a
A feature algebra A induces a structure with the same signature as F , in which - is
interpreted as weak subsumption ordering - A , - as - A , c() as c() A , and [d] as [d] A .
Proposition [8]. The structure F coincides with the structure induced by the
feature algebra defined by F .
Proof. It is sufficient to prove that the weak subsumption relation of the feature algebra
defined by F coincides with the information ordering on F . The proof in the case for
feature algebras with constants can be found in [8] on page 24 (Satz 6 and Satz 7).
There the algebra of feature trees has been called algebra of path functions. A direct
proof (additional 5 lines) is omitted for lack of space. 2
Theorem 19. A weak subsumption constraint h is satisfiable (over F ) if and only if h
is satisfiable over the structure induced by some feature algebra A .
Proof. If h is satisfiable then it is satisfiable over the structure induced by the feature
algebra defined by F . Conversely, every structure induced by a feature algebra is a
model of the axioms in F. Thus, if h is satisfiable over one such structure then it is
equivalent to an F-closed constraint (and not false) and hence satisfiable over F . 2
Alternative Notions of Feature Algebras. In the literature [22, 7] a restricted notion
of feature algebra has been considered that we call feature algebra with constants in the
sequel. The focus on feature algebras with constants leads to a restricted satisfiability
problem. This shows that the presented results properly extend the results in [7].
A feature algebra with constants is a feature algebra with the additional property that
if c(a) A then not a[d] A a 0 (1)
In order to handle the new property we consider the following mapping of weak subsumption
constraints over C and D to weak subsumption constraints over C [ flabelg
and D where label is a new constant not contained in C .
Proposition 20. A constraint h is satisfiable in some feature algebra if and only if [
is satisfiable in some feature algebra with constants.
Proof. If [
is satisfiable over a feature algebra A with constants C and features D [
flabelg then h is satisfiable over the feature algebra F with labels C [D. Given a
solution s 0 of [
over A a solution s of h over F can be defined as follows:
exists a in domain of A : s 0 (x)[p] A a and p 2 D   g
exists a in domain of A : s 0 (x)[plabel] A a and c(a) A g
Conversely, let h be satisfiable in a feature algebra A . Then h is satisfiable in F by
Theorem 19. We consider the following feature algebra with constants F   and show
that [
is satisfiable over F   . The constants and features of F   are C and D[flabelg,
respectively. The domain of F   contains all feature trees t without labeled internal
nodes where a labeled internal node of t is a path p such that p 2 D t , exists c with
not exists d with pd 2 D t . The selection and labeling relations of F
are those of FT- restricted to trees without internal labels. Obviously, F   satisfies all
three axioms of a feature algebra with constants. Now let s be an A-solution of h. Then
the variable assignment s 0 mapping x on s 0 (x) as given below is an F   -solution of [
exists a
7 Expressiveness
We show that FT- is strictly more expressive than FT but that FT- cannot express an
constraint. An FT constraint h is of the form x=y, a(x), x[a]y, or h-h 0 , and an
arity constraint of the form xfa g. An arity constraint xfa holds if x
denotes a tree with subtrees at exactly a 1 through a n .
Proposition 21. There is no FT- constraint which expresses that a variable x denotes
the empty feature tree, i.e., if a 6= b then there is no constraint equivalent to
Proof. If j were such a FT- constraint, then j as well as its finite F-closure would
entail x-y for all variables y. This contradicts Proposition 13 for all those y such that
(j)). Such a variable y
exists since V (j) is finite. 2
Lemma 22. Let h be an FT constraint. Then h
Proof. The FT constraint h is equivalent to the FT- constraint j obtained from h by
replacing all equalities x=y by inequalities x-y- y-x. Hence, x-y in j iff y-x in j,
and since algorithm F preserves this invariant it also holds for the F-closure of j. The
claim follows from Proposition 13. 2
Proposition 23. If x 6= y then there is no FT constraint h equivalent to x-y.
Proof. This follows immediately from Lemma 22 and Proposition 13. 2
8 Completeness of the Satisfiability Test
Proposition 4. Every F-closed constraint j is satisfiable over FT- .
The proof is based on the notion of path reachability and covers the rest of the sec-
tion. We proceed as follows. We first define path reachability, then give two Lemmas,
and finally compose the proof of Proposition 4 from these Lemmas.
For all paths p and constraint j, we define a binary relation j
"y is reachable from x over path p in j":
a y if x[a]y in j;
a meaning that "a can be reached from x over path p in j":
For example, if j is the constraint x-y - a(y) - x[a]u - x[b]z - z[a]x - b(z) then the
following reachability propositions hold: y j
y, x j
as x j
Definition 24 Path Consistency. We call a constraint j path consistent if the following
two conditions hold for all x, y, p, a, and b.
1. If x j
2. If x j
Lemma 25. Every F1-F2-closed and path consistent constraint is satisfiable.
Proof. Let j be F1-F2-closed and path consistent. We define the variable assignment
trees as follows:
ag
The path consistency of j condition 1 implies that L min j (x) is a partial function. Thus
is a feature tree. We now verify that min j is a solution of j.
- Let x-y in j. For all x 0 , if y j
by the definition of path reachability.
Thus, D min j (y) 'D min j (x) . For all a if y j
a by the definition of path
reachability. Thus, L min j (y) ' L min j (x) , i.e., min j (y)-min j (x).
Consider x[a]y in j. We have to prove for all p, z, and b the equivalences
The first equivalence is equivalent to D min j and the second
one to L min g. We start proving the first equivalence.
If y j
ap z since x[a]y in j. Suppose x j
ap z. By definition of path
reachability there exists x 0 and y 0 such that
The F1-closedness of j and x j
imply x-x 0 in j. The F2-closedness ensures
y-y 0 in j such that y j
holds. We now prove the second equivalence above. If
ap b then there exists z such that x j
ap z and b(z). The first equivalence implies
z and thus y j
b. The converse is simple.
- Let a(x) in j. Reflexivity (F1:1-closedness) implies x-x in j. Thus x j
e a such
that (e; a) 2 L x .
- Let x-y in j. We have to show that the set L min j (x) [L min j (y) is partial function. If
a and y j
b. The path consistency
of
Lemma 26. Every F3;F4;F5-closed constraint is path consistent.
Proof. Let j be F3;F4;F5-closed. Condition 1 of Definition 24 follows from condition
2 of Definition 24 and F3:1-closedness. The proof of condition 2 is by induction
on paths p. We assume x, y, a, and b such that x j
in j, and x j
e,
then there exist n;m - 0, x
F3-closedness implies that x n -ym in j (F3:2 yields x-y 1 in in j. Therefore
y m-x in j by F3:3-closedness, and hence y m-x 1 in
closedness.) Hence, F5-closedness implies a = b.
In the case there exists there exist x 0 , y 0 , -
y
x in
y in
Since x-x 0 in j we have x 0 -y 0 in j by F3-closedness (as above). Thus, F4-closedness
implies -
x-
y in j such that a=b holds by induction hypothesis. 2
Proof of Proposition 4. If j is F-closed then j is path consistent by Lemma 26 and
thus satisfiable by Lemma 25. 2
Corollary 27. Let j be an F-closed constraint. Then j only if there
are variables x 0 and y 0 such that j ' x 0 [a]y 0 and j ' x 0 -x.
Proof. Assume holds for the minimal solution min j of an
F-closed constraint that a 62 L min j (y) . Hence j 6j= 9y(x[a]y). 2.

Acknowledgments

. We would like to thank Jochen D-orre, Gert Smolka, and Ralf
Treinen for discussions on the topic of this paper. We would also like to acknowledge
many helpful remarks of the referees. The research reported in this paper has been
supported by the the Esprit Working Group CCL II (EP 22457) the SFB 378 at the
Universit?t des Saarlandes.



--R




A Complete Axiomatization of a Theory with Feature and Arity Constraints.
A complete and recursive feature theory.
In 2 nd Future Generation Computer Systems


On Subsumption and Semiunification in Feature Algebras.

Constraint logic programming: A survey.

Functional Grammar.
Applications of a Canonical Form for Generalized Linear Con- straints
Ordering Constraints over Feature Trees with Ordered Sorts.
Entailment for Set Constraints is not Feasible.
Inclusion Constraints over Non-Empty Sets of Trees

Feature Logics.
An Introduction to Unification-based Approaches to Grammar
Parsing and Type Inference for Natural and Computer Languages.
Feature constraint logics for unification grammars.
The Oz Programming Model.
Records for Logic Programming.
Feature constraints with first-class features
--TR

--CTR
Franois Pottier, A versatile constraint-based type inference system, Nordic Journal of Computing, v.7 n.4, p.312-347, Winter 2000
Jens Palsberg , Tian Zhao , Trevor Jim, Automatic discovery of covariant read-only fields, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.1, p.126-162, January 2005
Ernst Althaus , Denys Duchier , Alexander Koller , Kurt Mehlhorn , Joachim Niehren , Sven Thiel, An efficient graph algorithm for dominance constraints, Journal of Algorithms, v.48 n.1, p.194-219, August
Michael Benedikt , Leonid Libkin , Frank Neven, Logical definability and query languages over ranked and unranked trees, ACM Transactions on Computational Logic (TOCL), v.8 n.2, p.11-es, April 2007
weak subsumption;feature constraints;complexity;tree orderings;satisfiability;entailment