4.2.2 Solved Forms of Dominance Constraints

If a dominance constraint is satisfiable, it has infinitely many models; in particular, if T is a solution of \phi, then any tree that contains T is also a solution. For example, here are a few models of x\LE y:

The problem is similar when solving equations on first-order terms. The equation f(a,X_1,X_2)=f(Y_1,b,Y_2) has infinitely many models, namely all first-order terms of the form f(a,b,T) where T is a first-order term. Instead of attempting to enumerate all models, a solver returns a most general unifier:

X_1=b, Y_1=a, X_2=Y_2

A unifier is also known as a solved form: it represents a non-empty family of solutions.

For a dominance constraint \phi, we are going to proceed similarly and search for solved forms rather than for solution trees. The idea is that we simply want to arrange the nodes interpreting the variables of \phi into a tree shape.

For our purpose, a solved form will make explicit the relationship x\mathbin{r}y that holds between every two variables x and y of the description: i.e. in a solved form r\in\{\EQ,\LT,\GT,\DJ\}. In [DN00], we show that it is possible to use less explicit solved forms while preserving completeness: the relationship between x and y need not be fully decided, but merely one of x\LE y or x\NLE y. For simplicity of presentation, we will only consider fully explicit solved forms, but, in practice, less explicit solved forms are to be preferred since they require less search. In [DN00], we show that the less explicit solved forms may avoid an exponential number of choice points.

Denys Duchier
Version 1.2.0 (20010221)