Characteristic Set Constraints

In order to formulate the constraints that will only license tree-shaped solved forms, we must first consider each individual case x\mathbin{r}y for r\in\{\EQ,\LT,\GT,\DJ\}. For each case x\mathbin{r}y and its negation x\mathbin{{\neg}r}y, we will formulate characteristic constraints involving the set variables that we introduced above.

Let's consider the case x\LT y for which a solution looks as shown below:

For convenience, we define, for each variable x, the additional set variables \EQDOWNV{x} and \EQUPV{x} as follows:

\EQDOWNV{x} & \EQV{x}\uplus\DOWNV{x}\\
\EQUPV{x} & \EQV{x}\uplus\UPV{x}

We write \ENC{x\LT y} for the constraint characteristic of case x\LT y and define it as follows:

\ENC{x\LT y}\quad\equiv\quad

I.e. all variables equal or below y are below x, all variables equal or above x are above y, and all variables disjoint from x are also disjoint from y. This illustrates how set constraints permit to succinctly express certain patterns of inference. Namely \ENC{x\LT y} precisely expresses:

\forall z& y\LE z&x\LT z\\
\forall z& z\LE x&z\LT y\\
\forall z& z\DJ x&z\DJ y

The negation is somewhat simpler and states that no variable equal to x is above y, and no variable equal to y is below x. Remember that S_1\PAR S_2 expresses that S_1 and S_2 are disjoint.

\ENC{x\NLT y}\quad\equiv\quad

We can define the other cases similarly. Thus \ENC{x\DJ y}:

\ENC{x\DJ y}\quad\equiv\quad

and its negation \ENC{x\NDJ y}:

\ENC{x\DJ y}\quad\equiv\quad

For the case \ENC{x\EQ y} we first introduce notation. We write \NODE{x} for the tuple defined as follows:


where \DTRSV{x}=f(\NODE{x_1},\ldots,\NODE{x_n}) when the constraint x:f(x_1,\ldots,x_n) occurs in \phi (more about this when presenting the problem-specific constraints). Now we can simply define \ENC{x\EQ y} as:

\ENC{x\EQ y}\quad\equiv\quad\NODE{x}=\NODE{y}

and its negation \ENC{x\NEQ y} as:

\ENC{x\NEQ y}\quad\equiv\quad\EQV{x}\PAR\EQV{y}

Denys Duchier
Version 1.2.0 (20010221)