Composite Predicates

Sometimes, it is possible to define predicates from other primitive predicates by using a IF-THEN-ELSE construct. Note that each predicate is defined as a three-tuple $\langle$ A, C , ${\cal A}$$\rangle$. An abstract syntax of if-then-else construct can be described as:

$P_r$ $\equiv$ if $P_f$ then $P_t$ else $P_e$
where,

 		$P_r$ = ( $A_r$, $C_r$, 
${\cal A}_r$ ),

 $P_f$ = ( $A_f$, $C_f$, 
${\cal A}_f$ ),

 $P_t$ = ( $A_t$, $C_t$, 
${\cal A}_t$ ),and 

 $P_e$ = ( $A_e$, $C_e$, 
${\cal A}_e$ ). 

The argument-list $A_r$ of the composed predicate $P_r$ is given by:

$A_r$ $\equiv$ $A_f$ $\cup$ $A_t$ $\cup$ $A_e$

Any evaluation of check-code C is a mapping ${\it eval}_c$: C $\rightarrow$ $\mathbb{B}$.

Therefore, the evaluation of check-code $C_r$ of the composed predicate $P_r$ is defined as :

$${\it eval}_c(C_r) \equiv \left\{\begin{array}{r@{\quad\quad}l}... ...it eval}_c(C_e) & \mbox{if } {\it eval}_c(C_f)={\it false} \end{array}\right.$$

The auto-completion rules ${\cal A}_r$ of the resultant predicate $P_r$ can be defined as:

${\cal A}_r$ $\equiv$ ${\cal A}_t$ $\uplus$ ${\cal A}_e$
where,

 		
${\cal A}_t$ = { $R_{1t}$, $R_{2t}$, ...., $R_{nt}$} , 

 
${\cal A}_e$ = { $R_{1e}$, $R_{2e}$, ....,$R_{me}$}, and 

 
${\cal A}_r$ = { $R'_{1t}$, $R'_{2t}$,....,$R'_{nt}$, 
$R'_{(n+1)e}$,....,
$R'_{(n+m)e}$} 

The operation $\uplus$ is a union of auto-completion rules that are transformed as described below.

For ${\cal A}_t$ the transformation is defined as :

$\mathbb{T}_t$ : $R_t$ $\Longrightarrow$ $R_{t'}$

Consider a rule $R_t$ = ( $G_t$, ${\cal M}_t$, $f_t$, $A_t$, $r_t$) and the transformed rule $R'_t$ = ( $G'_t$, ${\cal M}_t$, $f_t$, $A_t$, $r_t$ ). It is clear from above that only the guards are affected by the transformation $\mathbb{T}_t$. Let $T_{G_t}$ and $T_{G'_t}$ denote the expression tree associated with guard $G_t$ and $G'_t$ respectively, then the transformation on guards is given as:

$$T_{G'_t} \equiv \left\{\begin{array}{l@{\quad\quad}l} maketr... ... maketree(C_f)\circ T_{G_t}& \mbox{ } otherwise \\ \par\end{array}\right.$$

where ,
${\it maketree}$: C $\rightarrow$ T creates a new expression tree. The binary operator $\circ$ returns a new expression tree with a boolean operator and as a non-terminal node and operands(to the function) as children to this node. This transformation ensures that all calls to JavaScript functions are still in the terminal nodes.
Similarly, consider a rule $R_e$ = ( $G_e$, ${\cal M}_e$, $f_e$, $A_e$, $r_e$ ) and the transformed rule $R'_e$ = ( ${G'}_e$, ${\cal M}_e$, $f_e$, $A_e$, $r_e$ ). Here again only the guards are affected by the transformation $\mathbb{T}_e$.

For ${\cal A}_e$ the transformation is $\mathbb{T}_e$ defined as :
$\mathbb{T}_e$ : $R_e$ $\Longrightarrow$ ${R'}_e$

Let $T_{G_e}$ and $T_{G'_e}$ denote the expression tree associated with guard $G_e$ and $G'_e$ respectively, then the transformation on guards is given as:

$$T_{G'_e} \equiv \left\{\begin{array}{l@{\quad\quad}l} maketr... ... maketree(C_{f'})\circ T_{G_e}& \mbox{ } otherwise \\ \par\end{array}\right.$$

where,
the function ${\it maketree}$ and the operator $\circ$ have already been described above.

The relation between $C_f$ and $C_{f'}$ is given by:

$$eval_c(C_f) \equiv \left\{\begin{array}{l@{\quad\quad}l} true & ... ...eval_c(C_{f'}) = false \\ false & \mbox{ } otherwise \\ \end{array}\right.$$

Based on the above transformations, Figure 6 shows a concrete example of a predicate being composed from a number of primitive predicates.

Figure 6: Composing predicates from primitive predicates.

We can generalise the condition part of IF-THEN-ELSE construct from a single predicate reference to a full predicate expression by specifying a boolean expression tree as described in Section 4.3. This gives greater expressive power to our formalism but in most cases a single predicate reference will suffice.