4.2.2 Solved Forms of Dominance Constraints

If a dominance constraint is satisfiable, it has infinitely many models; in particular, if is a solution of $\phi$ , then any tree that contains 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 is a first-order term. Instead of attempting to enumerate all models, a solver returns a most general unifier:

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 and 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 and 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.