Automatic Groups

Here the AG method is discussed, followed by a description of the simple programming model whose programs have been analysed.

The method works with the concept of an Automatic Group, which is fully explained in [ECH⁺92]. In our approach the formal AG description is augmented with some extra information, which is described later.

Informally, an automatic group is a structure where each node is named by a string of symbols. These symbols are the generating directions and correspond to the underlying tree pointers of the data structure. For each additional link direction there is a description, given by a finite state automaton, of which set of nodes are linked by this direction. A (deterministic) finite state automaton (FSA) is a simple model of computation, where an automaton reads a string of symbols one at a time and move from state to state. If it ends up in one of the accept states when the string is exhausted, then it is accepted. The automaton consists of a finite set of states S and a transition function $F: S \times A \rightarrow S$, which gives the next state for each of the possible input symbols in A. A two-variable FSA, differs in that the automaton is attempting to accept a pair of strings and inspects one symbol from each of them at each transition. It can be thought of as a one-variable FSA, but with the set of symbols extended to $A \times A$. There is one subtlety, in that we may want to accept strings of unequal length, so the shorter is padded with the additional '-' symbol. This makes the actual set of symbols $((A \cup\{-\}) \times (A \cup\{-\})) \backslash(-,-)$.

The description with each link direction l is a two variable finite state automaton called the multiplier of that link, and denoted M_l. There is also a word acceptor automaton W that accepts the path names that correspond to valid parts of the data structure.

The AG description of the binary tree mentioned earlier is given in Fig. 4.

Automatic groups are a good choice of description, since they can be readily manipulated using existing regular language theory. In particular we can produce FSAs for words of directions from the individual FSAs for each direction. We can also perform basic operations such as AND, OR, NOT, $\forall$ and $\exists$ with the FSAs involved and hence the sets of potential sources.

These descriptions can be more accurate than the ASAP axioms, since they define a regular set of pairs of nodes, rather than two regular sets of nodes. This gives more control over which nodes are linked, but still allows some flexibility, since one pointer can point to a number of different nodes.

The AG description is more general, and supersedes the Format system, but its descriptions are somewhat less intuitive to build.

  

Figure: AG description of a binary linked tree. The rhombus nodes are start nodes and are labelled with the direction name e.g. (l). Other states are circles and are labelled with state number e.g. S:2. The boxes hold the pair of symbols for that transition. Double borders indicate an accept state.