Adjunction.

The adjunction relation is defined as a relation between an (input) tree Tree, an auxiliary tree Aux of which the foot node is Foot and an (output) tree NewTree. The relation is non-deterministic with respect to which node in Tree the auxiliary tree is adjoined. Therefore, the first clause of adjoin states that the relation is true if the auxiliary tree is adjoined in one of the daughters of the input tree; the second clause states that the relation is true if the auxiliary tree is adjoined at the root node of the input tree:

For the moment, the reader should not worry about the mrk attribute. Its purpose will be explained later. The predicate $\mbox{\it adjoin\_ds}$ non-deterministically chooses a daughter from the list of daughters to adjoin the auxiliary tree in:

The second clause for adjoin states that adjunction may take place at the root node of the input tree. The resulting tree is defined as the auxiliary tree of which the foot node is instantiated with the daughters of the input tree. Furthermore we take care of the unification of the bottom and top features. The top features of the root node of the input tree are unified with the top features of the root node of the auxiliary tree; the bottom features of the root node of the input tree are unified with the bottom features of the foot node (recall figure 4.10).