Splitting trees

Dynamic evaluation associates a splitting tree with a computation. It is built by the allCases function as computation proceeds.

We explain here splitting trees related to computations in the dynamic constructible closure domain. They can be defined in the following way:

1. The root node represents the beginning of the computation.
2. The edges represent current information about parameters, that is constraints over parameters in their standard form.
3. The nodes represent the points in the computation where the constraints can change -- this can happen with the introduction of a new parameter (with newElement), and in the use of areEqual, areDifferent or the equality test (=).

The third point is the essential one, we will extend it more precisely, first for the case of only one parameter over the ground field, then for the case of many parameters, where recursion appears.

 

 

Figure 2: Splitting tree with box.

 

 

Figure 3: Splitting tree with open box.

Case of one parameter.

Let a be a parameter over the field , and x and y two elements in the field . At every node of the splitting tree, except the root node, there is one of the following possibilities:

• areEqual(x,y). There is only one edge coming down from this node, it corresponds to:
  • true if areEqual(x,y) implies a constraint on a which is compatible with the old ones,
  • or false otherwise. In this case, current constraints on a do not change.
• areDifferent(x,y). There is only one edge coming down from this node, it corresponds to:
  • true if areDifferent(x,y) implies a constraint on a which is compatible with the old ones,
  • or false otherwise. In this case, current constraints on a do not change.
• x = y. In this case we have several possibilities:
  • the answer is true for all the possible values of a. This node has only one edge coming down, and current constraints on a do not change.
  • the answer is false for all the possible values of a. This node has only an edge coming down, and current constraints on a do not change.
  • both answers, true and false, are possible. There are two edges coming down from this node, one for each answer. This is called a splitting point.

Figure 1 shows three basic trees for the case of one parameter. The second tree in this figure corresponds to the example of the matrix rank computation.

Case of many parameters.

Let be the parameters introduced. The main point is that the program works recursively over parameters and then the use of =, areEqual or areDifferent over expressions of level k ( ) can produce equality tests (and then splitting points) in lower levels.

Initially we show the last level only, with possible internal splittings in lower levels represented by a box. From this box, there is at least one edge coming down, but possibly many edges. During this process only constraints related to lower levels could change.

In order to show it we will study the following example:

    a:CL:= newElement('a)
    b:CL:= newElement('b)
    c:CL:= newElement('c)
    (a*b*c = 0)$CL

This corresponds to the splitting tree in figure 2. In the root node computation starts, in the second one there is the introduction of the first parameter a. From this node there is an edge coming down with the current information over this parameter that is . In the next node there is the introduction of the second parameter, and after the introduction of the parameter c we find the equality test a*b*c = 0. In order to answer this question the system works recursively over the parameters and some splitting points appear for parameters a and b. This splitting tree hides these splits in a box in which the current constraint on c ( ) does not change. From this box there are three edges coming down, with the current information about parameters a and b after split. For each edge we find a node with the question a*b*c = 0 specialized with respect to these new constraints. In two nodes there is 0 = 0, which we can answer now without additional split over c. In the other node we find the question c = 0 that needs a split over c in order to be answer.

Finally the complete answer is:

   [value is true in case any c and any b and a = 0,
    value is true in case any c and b = 0 and a /= 0,
    value is true in case c = 0 and b /= 0 and a /= 0,
    value is false in case c /= 0 and b /= 0 and a /= 0]

   Time: 1.46 sec

Let us now open the box (see figure 3). In order to answer the question a*b*c = 0 the system needs to answer a*b = 0 and for that a = 0. One split appears at the level of a, that is inside the inner box. There are two edges coming down from this box, for each of them there is a reduction step to specialize the question a*b = 0 to the new constraints on a. In one of the branches this question can be answered without more splits, in the other it is needed another split over b.

Note that boxes are used to show the change of level in the computation, where recursion acts. Also there are some boolean values that appear, they only clarify the meaning of the branch (they can be seen as a flag for the branch).