Knuth-Bendix helper functions

Defined in knuth-bendix-helpers.hpp.

This page contains documentation for some helper functions for the KnuthBendix class. In particular, these functions include versions of several of the member functions of KnuthBendix (that accept iterators) whose parameters are not iterators, but objects instead. The helpers documented on this page all belong to the namespace knuth_bendix.

See also

Common congruence helpers

Functions
template<typename Word, typename Rewriter, typename ReductionOrder>
void	by_overlap_length (KnuthBendix< Word, Rewriter, ReductionOrder > &kb)
	Run the Knuth-Bendix algorithm by considering all overlaps of a given length.
template<typename Word, typename Rewriter, typename ReductionOrder>
bool	is_reduced (KnuthBendix< Word, Rewriter, ReductionOrder > &kb)
	Check if the all rules are reduced with respect to each other.
template<typename Word, typename Time>
std::vector< Word >::const_iterator	redundant_rule (Presentation< Word > const &p, Time t)
	Return an iterator pointing at the left hand side of a redundant rule.

Function Documentation

by_overlap_length()

template<typename Word, typename Rewriter, typename ReductionOrder>

void by_overlap_length

(

KnuthBendix< Word, Rewriter, ReductionOrder > &

kb

)

Defined in knuth-bendix-helpers.hpp.

This function runs the Knuth-Bendix algorithm on the rewriting system represented by a KnuthBendix instance by considering all overlaps of a given length \(n\) (according to the overlap) before those overlaps of length \(n + 1\).

Template Parameters

Word	the type of the words in the presentation.
Rewriter	the first template parameter for KnuthBendix.
ReductionOrder	the second template parameter for KnuthBendix.

Parameters

kb	the KnuthBendix instance.

Complexity

See warning.

Warning

This will terminate when the KnuthBendix instance is confluent, which might be never.

See also

KnuthBendix::run.

is_reduced()

template<typename Word, typename Rewriter, typename ReductionOrder>

bool is_reduced ( KnuthBendix< Word, Rewriter, ReductionOrder > & kb )

nodiscard

Defined in knuth-bendix-helpers.hpp.

Template Parameters

Word	the type of the words in the presentation.
Rewriter	the first template parameter for KnuthBendix.
ReductionOrder	the second template parameter for KnuthBendix.

Parameters

kb	the KnuthBendix instance defining the rules that are to be checked for being reduced.

Returns

true if for each pair \((A, B)\) and \((C, D)\) of rules stored within the KnuthBendix instance, \(C\) is neither a subword of \(A\) nor \(B\). Returns false otherwise.

redundant_rule()

template<typename Word, typename Time>

std::vector< Word >::const_iterator redundant_rule ( Presentation< Word > const & p, Time t )

nodiscard

Defined in knuth-bendix-helpers.hpp.

Starting with the last rule in the presentation, this function attempts to run the Knuth-Bendix algorithm on the rules of the presentation except for the given omitted rule. For every such omitted rule, Knuth-Bendix is run for the length of time indicated by the second parameter t, and then it is checked if the omitted rule can be shown to be redundant (rewriting both sides of the omitted rule using the other rules using the output of the, not necessarily finished, Knuth-Bendix algorithm).

If the omitted rule can be shown to be redundant in this way, then an iterator pointing to its left hand side is returned.

If no rule can be shown to be redundant in this way, then an iterator pointing to p.cend() is returned.

Template Parameters

Word	type of words in the Presentation p.
Time	type of the 2nd parameter (time to try running Knuth-Bendix).

Parameters

p	the presentation.
t	time to run KnuthBendix for every omitted rule.

Warning

The progress of the Knuth-Bendix algorithm may differ between different calls to this function even if the parameters are identical. As such this is non-deterministic, and may produce different results with the same input.