Subsections

• Proposition (Computation of V-equivalent basic constraint).
• Proof.

Notation.

Determining satisfiability

A constraint is satisfiable iff it has a solution. Not all constraints are satisfiable. For example, the constraint c₁ $\doteq$ c₂ is unsatisfiable, because for all assignments the denotation of c₁ will be the feature graph (c₁,$\emptyset$) and the denotation of c₂ will be (c₂,$\emptyset$) which is not the same graph. Clearly a constraint may also define such a clash indirectly, as in the constraint:

$$\begin{array}{l} \mbox{\rm X}_{0} \mbox{\it l}_{1} \doteq \m... ...\rm X}_{2} \mbox{\it l}_{1} \doteq \mbox{\rm c}_{2} \end{array}$$

The problem whether a constraint is satisfiable is decidable. Algorithms deciding satisfiability for more powerful feature logics (extending the current logic with disjunction and negation) are for example presented in [39], [89]. The present algorithm is an adaptation to $\cal {L}$ of the algorithm presented in [89]. The algorithm consists of a number of simplification rules. Rules are applied until no rules can be applied anymore. In that case the constraint is said to be in normal form or normal. For normal constraints it is trivial to check whether the constraint is satisfiable (clash-free). A constraint is solved iff it is normal and clash-free.

The simplification algorithm is presented here in two steps. Firstly, I show how to remove all complex paths (paths containing more than one label), by the introduction of some new variables. The resulting constraint, which is called basic, is shown to be satisfiable iff the original constraint was. The next step then rewrites constraints without complex path expressions into normal form.

A basic constraint is a constraint in which each equation has one of the following forms:

$$\begin{array}{l} s \doteq t\\ sl \doteq t \end{array}$$
An arbitrarily constraint $\phi$ can be mapped into a basic constraint $\phi{^\prime}$ by the introduction of new variables. $\phi{^\prime}$ is satisfiable iff $\phi$ is. We will say that two assignments agree on a set of variables iff they assign the same elements in the domain to these variables.

Definition 6 (V-equivalence)   Two constraints $\phi$,$\psi$ are V-equivalent, for V a set of variables, iff:

1.

If $\alpha$ $\in$ $\phi^{\cal{I}}_{}$, then there exist $\beta$ $\in$ $\psi^{\cal{I}}_{}$ such that $\alpha$ and $\beta$ agree on V.

2.

If $\alpha$ $\in$ $\psi^{\cal{I}}_{}$, then there exist $\beta$ $\in$ $\phi^{\cal{I}}_{}$ such that $\alpha$ and $\beta$ agree on V.

If constraints $\phi$ and $\psi$ are V-equivalent then $\phi$ is satisfiable iff $\psi$ is satisfiable (this follows immediately from the definition).

In the following, C is a constraint, [X| s]C is the constraint obtained from C by replacing each occurrence of variable X with s.

Proposition (Computation of V-equivalent basic constraint).

For every constraint $\phi$ one can compute a V-equivalent basic constraint.

Proof.

The following algorithm computes for a given constraint $\phi$ a basic constraint $\phi{^\prime}$. We will show that $\phi{^\prime}$ thus obtained is V-equivalent with $\phi$.

Apply any of the rules, until the rules are not applicable:

1.

$$\frac{\Gamma,~ s~\mbox{\it l}_{1}\dots \mbox{\it l}_{n} \dot... ...elta} \mbox{~where $n>1$, $\mbox{\rm X}_{i}$\ a new variable.}$$

2.

$$\frac{\Gamma,~d \doteq s~\mbox{\it l}_{1}\dots \mbox{\it l}_... ...elta} \mbox{~where $n>1$, $\mbox{\rm X}_{i}$\ a new variable.}$$

3.

$$\frac{\Gamma,~ s~\mbox{\it l} \doteq t~\mbox{\it l}, ~\Delta... ...{i},~\Delta} \mbox{~where $\mbox{\rm X}_{i}$\ a new variable.}$$

It is easy to verify that if none of the rules is applicable, the resulting constraint is indeed a basic constraint. Also observe that the algorithm terminates because each of the steps replaces an atomic constraint with two new atomic constraints, one of which already is basic, and the other has a shorter path than the previous constraint.

Each step of the algorithm preserves satisfiability, hence a sequence of steps preserves satisfiability as well. Step 1 of the algorithm changes a constraint $\phi$ into $\psi$. It is straightforward to show that $\phi$ is V-equivalent with $\psi$ (and hence $\phi$ is satisfiable iff $\psi$ is). Assume that $\cal {I}$, $\alpha$ $\in$ $\phi^{\cal{I}}_{}$ then let $\beta$ be the assignment which is exactly like $\alpha$, except that the newly introduced X_i is mapped to the feature graph $\alpha$(s)^l₁...l_n-1. Clearly, $\beta$ $\in$ $\psi^{\cal{I}}_{}$. The other way around is similar. The same reasoning applies for the steps 2 and 3.

Example 7   Consider the following constraint

$$\phi : \begin{array}{l} \mbox{\rm X}_{0} \mbox{\it l}_{1} \... ... \mbox{\rm X}_{0} \mbox{\it l}_{1} \mbox{\it l}_{3} \end{array}$$
This constraint is simplified, according to the rules above, in the following three steps, using respectively rule 1, 2 and 3:

$$\phi \Rightarrow \begin{array}{l} \mbox{\rm X}_{0} \mbox... ...\rm X}_{0} \mbox{\it l}_{2} \doteq \mbox{\rm X}_{3} \end{array}$$

Given a basic constraint, the following simplification rules rewrite this constraint into its equivalent normal form.

Definition 8 (Normal form)   Applying any of the following simplification rules to a basic constraint until no rule is applicable, results in a normal form constraint:

1.

$$\frac{\Gamma,~\mbox{\rm X} \doteq s, ~\Delta} {[X\vert s]\Ga... ...Delta} \mbox{~if $\mbox{\rm X}$\ occurs in $C$\ and $X\neq s$}$$

2.

$$\frac{\Gamma,~\mbox{\rm c} \doteq \mbox{\rm X}, ~\Delta} {\Gamma,~\mbox{\rm X} \doteq \mbox{\rm c}, ~\Delta}$$

3.

$$\frac{\Gamma,~\mbox{\rm X}\mbox{\it l} \doteq s, \mbox{\rm X}... ...\Gamma,~\mbox{\rm X}\mbox{\it l} \doteq s, s \doteq t, ~\Delta}$$

4.

$$\frac{\Gamma,~s \doteq s, ~\Delta } {\Gamma, \Delta}$$

To show that a normal form of a constraint C computed by this algorithm is equivalent to C observe that each of the simplification rules preserves equivalence. In the first rule the variable X is `isolated'; in the rest of the constraint the variable is replaced by the constant or variable it is equated with. Clearly in this case $\phi$ and $\psi$ are equivalent, because, by definition $\alpha$(X) = $\alpha$(s), hence C^{$\cal {I}$} = C[X| s]^{$\cal {I}$}. As for the third rule, note that the solutions of {Xl $\doteq$ s,Xl $\doteq$ t} are those assignments such that the descriptors Xl, s, t have the same denotation. The same is the case for the solutions of {Xl $\doteq$ s, s $\doteq$ t}. Hence the third rule preserves equivalence. The second rule and the fourth rule clearly preserve equivalence.

Furthermore, the simplification algorithm always terminates, because clearly there cannot be an infinite sequence of simplification rules starting from any basic constraint $\phi$. To see this, note that there is only a finite number of variables in a given constraint. The first rule `isolates' such a variable, hence this rule can be applied at most once for each variable; furthermore none of the other rules introduce new variables. The second rule can only be applied a finite number of cases because the number of constants is also finite, and not increased by any of the other rules. The third rule can only be applied a finite number of times because it reduces the length of the paths in a constraint; none of the other rules increase this length. The final rule can only be applied a finite number of times because it reduces the number of equations in a constraint, and none of the other rules increases this number.

The simplification algorithm is very similar to the `unification' algorithms based on the simplification rules for a system of term equations as presented for example in [5]. Note though that this system does not contain an `occur check' as I did not exclude cyclic structures.

A normal constraint is clash-free if it does not contain any of the following constraints:

• cl $\doteq$ d (constant/compound clash)
• c₁ $\doteq$ c₂ (constant clash)

A normal and clash-free constraint is called solved. A solved constraint consists exclusively of atomic constraints of the form:

• Xl $\doteq$ s
• X $\doteq$ s

Furthermore, if an equation is of the second type then the variable X occurs only once (the variable is said to be isolated). For this reason it is very easy to see that solved constraints are satisfiable, because they can be interpreted as a recipe to define an appropriate assignment. Such an assignment is called the principal solution. For $\phi$ a solved constraint, $\alpha$(x) = _defFG[x,$\phi$] is a principal solution of $\phi$. The function FG is defined as follows:

$${\rm FG}[s,\phi] =_{def} \left\{ \begin{array}{l} (s,\empty... ...phi \mbox{\rm X}\}) \hfill\mbox{~otherwise} \end{array}\right.$$
where $\rightarrow^{*}_{\phi}$ is the transitive and reflexive closure of $\rightarrow_{\phi}^{}$ which is a binary relation on the variables occurring in $\phi$:

$$\mbox{\rm X} \rightarrow_\phi \mbox{\rm Y} \mbox{ iff } \mbox{\rm X}\mbox{\it l} \doteq \mbox{\rm Y} \in \phi$$

Example 9   Consider the following constraint $\psi$, which was the result of example 7 of the computation of basic constraints:

$$\psi : \begin{array}{l} \mbox{\rm X}_{0} \mbox{\it l}_{1} ... ...\rm X}_{0} \mbox{\it l}_{2} \doteq \mbox{\rm X}_{3} \end{array}$$

This constraint can then be rewritten into normal form, for example in the following steps, using the rules 3, 1, 3 and 1 of definition 8. The application of the rules 2 and 4 are performed implicitly in the example (for simplicity).

$$\psi \Rightarrow \begin{array}{l} \mbox{\rm X}_{0} \mbox{... ...\rm X}_{0} \mbox{\it l}_{2} \doteq \mbox{\rm c}_{2} \end{array}$$
The principal solution $\alpha$ of this constraint is defined as follows:

$$\begin{array}{l} \alpha(\mbox{\rm X}_{0}) = (\mbox{\rm X}_{0}... ...ox{\rm X}_{1},\mbox{\rm X}_{2},\mbox{\rm X}_{3}\}$} \end{array}$$

The first two assignments $\alpha$(X₀) and $\alpha$(X₁) can be illustrated as:

Notation.

Once constraints get more complicated they tend to be difficult to read. For that reason I will often use a special representation, called matrix notation, to represent the interpretation of a (satisfiable) constraint on some variable.

The matrix representation of a constraint on a variable is best introduced using an example. For the result of example 9, the matrix representation for the constraints on variable X₀ looks as follows:

$$\avm[{\mbox{\rm X}_{0}}]{\mbox{\it l}_{1}: \avm[{\mbox{\rm X... ...{3}: \mbox{\rm c}}_{2}\\ \mbox{\it l}_{2}: \mbox{\rm c}}_{2}$$
The names of variables only matter in case they are referred to more than once. In the foregoing example, I therefore omit the variables and instead write:

$$\avm{\mbox{\it l}_{1}: \avm{\mbox{\it l}_{3}: \mbox{\rm c}}_{2}\\ \mbox{\it l}_{2}: \mbox{\rm c}}_{2}$$
As another example of this notation, consider the following constraint:

$$\begin{array}{l} \mbox{\rm X}_{0}~\mbox{\it syn} ~\mbox{\it c... ...q \mbox{\rm X}_{0}~\mbox{\it phon}~ \mbox{\it out} \end{array}$$
The matrix representation of the constraints on X₀ looks as follows:

$$\avm{ \mbox{\it syn} : \avm{ \mbox{\it cat} : \mbox{\rm s} }... ..._{1}]{} } }}\\ \mbox{\it out} :\avm[{\mbox{\rm X}}_{1}]{} } }$$
Usually an empty feature structure will not be shown explicitly, but instead only the corresponding variable will be shown, i.e. instead of

$$\avm{\mbox{\it r}:\avm[\mbox{\rm X}]{}}$$
I write

$$\avm{\mbox{\it r}:\mbox{\rm X}}$$

Furthermore, I use a special notation for parts of such matrices that are used to encode lists and difference lists. If no confusion arises I use the HPSG [69] convention of writing a list within angled brackets, where the comma separates elements of the list, and the vertical bar may be used to separate the head from the tail of the list. In path equations the elements of such lists are referred to with attributes f and r (for first and rest), the empty list is represented with the constant $\langle$$\rangle$. In case of difference lists I moreover write the `out' part of the difference list right after the `in'-part, separated by `-'. The attributes in and out are used in path equations to refer to these parts. Moreover, in case of a difference list where the tail of the `in' part is reentrant with the `out' part, I simply write the `in' list within `` ''. As an example I write ``letters from mexico get lost'' for $\langle$letters, from, mexico, get, lost|X₁$\rangle$ - X₁.

As a further abbreviation I sometimes use the functor-argument notation for semantic structures, as introduced in section 1.2.3. Using these abbreviations, the foregoing constraint is written as:

$$\avm{ \mbox{\it syn} : \avm{ \mbox{\it cat} : \mbox{\rm s} }... ... {\i}ti)} \\ phon : \mbox{\lq\lq graham visited ha\uml {\i}ti''} }$$