GitHub

Implementations of Knuth-Bendix completion

In KnuthBendix.jl

There are currently two actively developed implementations available:

  1. KBIndex - a modification of KBStack (see below) which uses IndexAutomaton for rewrites and PrefixAutomaton for reducing the rewriting system.
  2. KBPrefix - uses PrefixAutomaton for both rewriting and (partial!) reduction of the rewriting system.

Three more implementations following Sims book directly are available, however their simplistic nature makes them suitable for educational purposes only.

  1. KBPlain which follows the naive version,
  2. KBStack which uses stack and rule deactivation to maintain reducedness.
  3. KBS2AlgRuleDel - a modification of KBStack which frequently deletes the rules which are deemed redundant.

In general all of those methods dispatch through a common interface:

KnuthBendix.knuthbendix — Function
knuthbendix(rws::AbstractRewritingSystem)
knuthbendix(settings::Settings, rws::AbstractRewritingSystem)

Perform Knuth-Bendix completion on rewriting system rws using algorithm defined by method.

Warn

Rewriting systems returned by the completion algorithm may not be confluent. Usually this happens when

  • number of rules stored in rws exceeds the one permitted in settings,
  • the completion process is manually interrupted,
  • or when the settings allow the algorithm to skip the processing of certain critical pairs.

You should always assume that the rewriting system is not confluent, unless isconfluent returns true.

Unless manually interrupted the returned rewriting system will be reduced.

source
KnuthBendix.Settings — Type
Settings{CA<:CompletionAlgorithm}
Settings(alg; kwargs...)

Struct encompassing knobs and switches for the knuthbendix completion.

Arguments:

  • alg::CompletionAlgorithm: the algorithms used for Knuth-Bendix completion

Keyword arguments

  • max_rules: forcefully terminate Knuth-Bendix completion if the number of rules exceeds max_rules. Note: this is only a hint, the returned rws may contain more or fewer rewriting rules.
  • reduce_delay: Reduce the rws (and incorporate new found rules into rws) whenever the number of discovered rules since last reduction exceeds reduce_delay.
  • confluence_delay: Attempt a confluence check whenever no new critical pairs are discovered after considering confluence_delay pairs of rules.
  • max_length_lhs: The upper bound on the length of lhs of new rules considered in the algorithm.
  • max_length_lhs: The upper bound on the length of rhs of new rules considered in the algorithm.
  • max_length_overlap: The upper bound on the overlaps considered when finding new critical pairs.
  • collect_dropped: The discovered critical pairs which are not admissible ( due to the length limiting options above) will be collected during completion. To access those pairs you will need to use knuthbendix! function and pass Workspace directly.
  • verbosity: Specifies the level of verbosity.
Note

Not all flags have effect for every completion algorithm. E.g. the length-limiting and collection will be used only for KBIndex and KBPrefix.

source

Knuth-Bendix on Monoids and Automatic Groups (kbmag)

The baseline C-implementation of the Knuth-Bendix completion (and much more!) used by the GAP System. See kbmag source code and the documentation of the GAP interface.

Much wider functionality (automatic structures, etc.) and way more tuning options. In maintainance mode since ca. 1996.

Monoid Automata Factory (maf)

Somehow more advanced and modern C++-implementation of similar functionality to kbmag (it even has kbmag interface!). According to their docs

MAF succeeds on many examples where KBMAG either fails, or requires a very careful selection of options to succeed. In particular, MAF will usually work better with recursive orderings.

See package documentation and its source code. Not actively developed since 2011.