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 , the additional set variables $\EQDOWNV{x}$ and $\EQUPV{x}$ as follows:

$\begin{array}{r@{{}={}}l} \EQDOWNV{x} & \EQV{x}\uplus\DOWNV{x}\\ \EQUPV{x} & \EQV{x}\uplus\UPV{x} \end{array}$

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 \begin{array}[t]{@{}cl@{{}\subseteq{}}l} &\EQDOWNV{y}&\DOWNV{x}\\ \wedge&\EQUPV{x}&\UPV{y}\\ \wedge&\SIDEV{x}&\SIDEV{y} \end{array}$

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

$\begin{array}{lc@{{}\rightarrow{}}c} \forall z& y\LE z&x\LT z\\ \forall z& z\LE x&z\LT y\\ \forall z& z\DJ x&z\DJ y \end{array}$

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

$\ENC{x\NLT y}\quad\equiv\quad \begin{array}[t]{@{}cl} &\EQV{x}\PAR\UPV{y}\\ \wedge&\EQV{y}\PAR\DOWNV{x} \end{array}$

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

$\ENC{x\DJ y}\quad\equiv\quad \begin{array}[t]{@{}cl} &\EQDOWNV{x}\subseteq\SIDEV{y}\\ \wedge&\EQDOWNV{y}\subseteq\SIDEV{x} \end{array}$

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

$\ENC{x\DJ y}\quad\equiv\quad \begin{array}[t]{@{}cl} &\EQV{x}\PAR\SIDEV{y}\\ \wedge&\EQV{y}\PAR\SIDEV{x} \end{array}$

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

$\NODE{x}\quad\equiv\quad \TUP{\EQV{x},\UPV{x},\DOWNV{x},\SIDEV{x},\EQUPV{x},\EQDOWNV{x},\DTRSV{x}}$

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}$