Design decisions for the formalization of BTs

This page records the rationale for the design decisions we took during the definition of the BT data type.

Nodes formalization

Basic nodes (constructors)

The current formalization of BTs distinguishes between a set of "core nodes" (the Sequence, Fallback and Parallel composition) and a further set of primitives lumped together in a Decorator constructor (as in the book by Colledanchise-Ogren). Currently the only supported decorators are Not and IsRunning. In the book a couple of other decorators (called max-N-tries and max-T-sec) are briefly described. These decorators are characterized by the reliance on some form of "stored state": e.g. the max-N-tries is supposed to memorize how many times the child has failed and not tick it anymore when this number is higher than a certain threshold. In our formalization for BTs, nodes have no mechanism for long-term state storage (i.e. persistent between a tick and the following one), hence these algorithms are not expressible. It seems that any form of persistent state has to be implemented by providing suitable basic skills (e.g. communication with a "parameter server") and handling state using these skills. (A similar caveat also applies for the so-called "starred nodes".)

The troublesome parallel node

The parallel node is unique among BT nodes in that it is not concerned with managing the execution flow of its children (as for the sequence and fallback nodes) but only with combining their result.

Let us focus for the moment on the parallel node with 2 children only. Its action has a very nice description in terms of binary operators of a three-valued logic. Specifically:

• A node parallel 0 a b always return true.
• A node parallel 1 a b returns true iff at least one of a and b returns true, so it implements the logical OR operation.
• A node parallel 2 a b returns true iff both a and b return true, so it implements the logical AND operation.

This actually holds for any number of children: parallel 1 a1 ... an is just OR(a1, ..., an) and similarly parallel n a1 ... an coincides with AND(a1, ..., an). Since both AND and OR operators are associative, in this case it is actually possible to re-express these nodes as a composition of binary nodes, for instance one has

• parallel 1 a b c = parallel 1 a (parallel 1 b c)
• parallel 1 a b c d = parallel 1 a (parallel 1 b (parallel 1 c d))
• ...and so on.

This simplicity is deceiving, however: things become much more complicated for parallel nodes with n children and threshold i, where 1 < i < n.

Let us consider for instance the first nontrivial case, parallel 2 a b c. To express this as a composition of binary nodes we must partition in some way the set {a,b,c} into two subsets, say {a,b} and {c}. However, this is an artificial distinction which was not part of the original problem, so our answer cannot in fact depend on the chosen decomposition. In other words, we must in some way take account of all the possible subdivisions.

In this case the combinatorics is still manageable: the node parallel 2 a b c should return

• true when (parallel 2 a b) = true OR ((parallel 1 a b) = true AND c = true)
• false when (parallel 1 a b) = false OR (parallel 1 a c) = false OR (parallel 1 b c) = false

and re-expressing OR and AND operators using parallel nodes:

(parallel 2 a b c) := (parallel 1 (parallel 2 a b) (parallel 2 (parallel 1 a b) c))

So we see that a parallel node with the "intermediate" threshold 2 can actually be expressed as a combination of binary parallel nodes with "extremal" thresholds. This seems to be the case also for general values of i and n, but the details are not easy to work out and will probably involve some heavy combinatorics.

Mutual induction vs. nested induction

A priori, there are two ways to implement trees with arbitrary branching in Coq:

• As a mutual inductive type: this is the classic definition in terms of trees and forests:

     Inductive tree: Set :=
     | node: Symbol -> forest -> tree
     with forest: Set :=
     | fnil: forest
     | fcons: tree -> forest -> forest.
  

• As a nested inductive type: if we want to use the List type from the Coq standard library, the definition would be instead

     Inductive ntree: Set :=
     | leaf: Symbol -> ntree
     | node: Symbol -> list ntree -> ntree.
  

In the second case, we could use functions and theorems of the standard library. Unfortunately, working with nested inductive types is also more involved (e.g. one needs to specify induction and recursion principles by hand...)

Another reason to use mutual induction with a specialized btforest type is that in this way we can enforce the constraint according to which a BT inner node always has at least one child directly at the type level (obviously, regular Coq lists can be emtpy).