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:

\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 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:

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


Denys Duchier
Version 1.2.0 (20010221)