66.4 Control parameters

The Knuth-Bendix procedure is unusually sensitive to the settings of a number of parameters that control its operation. In some examples, a small change in one of these parameters can mean the difference between obtaining a confluent rewriting system fairly quickly on the one hand, and the procedure running on until it uses all available memory on the other hand.

Unfortunately, it is almost impossible to give even very general guidelines on these settings, although the ``wreathproduct" orderings appear to be more sensitive than the ``shortlex" and ``wtlex" orderings. The user can only acquire a feeling for the influence of these parameters by experimentation on a large number of examples.

The control parameters are defined by the user by setting values of certain fields of a rewriting system rws directly. These fields will now be listed.

rws.maxeqns:

A positive integer specifying the maximum number of rewriting rules allowed in rws. The default is 32767. If this number is exceeded, then KB or Automata will abort.

rws.tidyint:

A positive integer, 100 by default. During the Knuth-Bendix procedure, the search for overlaps is interrupted periodically to tidy up the existing system by removing and/or simplifying rewriting rules that have become redundant. This tidying is done after finding rws.tidyint rules since the last tidying.

rws.confnum:

A positive integer, 500 by default. If rws.confnum overlaps are processed in the Knuth-Bendix procedure but no new rules are found, then a fast test for confluence is carried out. This saves a lot of time if the system really is confluent, but usually wastes time if it is not.

rws.maxstoredlen:

This is a list of two positive integers, maxlhs and maxrhs; the default is that both are infinite. Only those rewriting rules for which the left hand side has length at most maxlhs and the right hand side has length at most maxrhs are stored; longer rules are discarded. In some examples it is essential to impose such limits in order to obtain a confluent rewriting system. Of course, if the Knuth-Bendix procedure halts with such limits imposed, then the resulting system need not be confluent. However, the confluence can then be tested be re-running KB with the limits removed. (To remove the limits, unbind the field.) It is advisable to call AddOriginalEqnsRWS on rws before re-running KB.

rws.maxoverlaplen:

This is an integer, which is infinite by default (when not set). Only those overlaps of total length rws.maxoverlaplen are processed. Similar remarks apply to those for maxstoredlen.

rws.sorteqns:

This should be true or false, and false is the default. When it is true, the rewriting rules are output in order of increasing length of left hand side. (The default is that they are output in the order that they were found).

rws.maxoplen:

This is an integer, which is infinite by default (when not set). When it is set, the rewriting rules are output in order of increasing length of left hand side (as if rws.sorteqns were true), and only those rules having left hand sides of length up to rws.maxoplen are output at all. Again, similar remarks apply to those for maxstoredlen.

rws.maxreducelen:

A positive integer, 32767 by default. This is the maximum length that a word is allowed to have during the reduction process. It is only likely to be exceeded when using the ``wreathproduct" or ``recursive" ordering.

rws.silent, rws.verbose, rws.veryVerbose:

These should be true or false, and are false by default. It only makes sense to set one of them to be true. They control the amount of diagnostic output that is printed by KB and Automata. By default there is a small amount of such output.

rws.maxstates, rws.maxwdiffs:

These are positive integers, controlling the maximum number of states of the word-reduction automaton used by KB, and the maximum number of word-differences allowed when running Automata, respectively. These numbers are normally increased automatically when required, so it unusual to want to set these flags. They can be set when either it is desired to limit these parameters (and prevent them being increased automatically), or (as occasionally happens), the number of word-differences increases too rapidly for the program to cope - when this happens, the run is usually doomed to failure anyway.

Previous Up Top Next
Index