### 5.4.5 Treeness Constraints

Our formal framework simply stipulated that models should be trees. In the constraint model, we provide an explicit axiomatization of this notion. A tree is a directed acyclic graph, where every node has a unique incoming edge, except for a distinguished node, called the root, which has none.

To support our axiomatization, we introduce two new variables and for each node . Again to avoid the problem that might be undefined at the root, we make it denote a set:

denotes the set of mothers of and the set of its immediate daughters. To enforce that a node has at most one mother, we pose:

The set of immediate daughters of is simply defined as the union of its daughter sets:

is a mother of iff is a daughter of :

We could introduce a variable to denote the root, but instead we introduce the variable to denote the singleton containing the root.

Now, is root iff it has no mother:

So far, we have enforced that every node (except the root) has a unique mother, but it could still have more than one incoming edge from the same mother. We can exclude this case by stating that the daughter sets for all nodes together with the root set form a partition of the input words:

In order to guarantee well-formedness, we still need to enforce acyclicity.

Denys Duchier
Version 1.2.0 (20010221)