The KnuthBendix class

Class containing an implementation of the Knuth-Bendix Algorithm.

On this page we describe the functionality relating to the Knuth-Bendix algorithm for semigroups and monoids in libsemigroups_pybind11. This page contains details of the member functions of the class KnuthBendix. This class is used to represent a string rewriting system defining a 1- or 2-sided congruence on a finitely presented monoid or semigroup.

KnuthBendix inherits from Runner and has the nested class KnuthBendix.options.

See also

Runner.

Important

The class KnuthBendix has all the methods of the Runner class but, for boring technical reasons, is not a subclass of Runner. If thing is an instance of KnuthBendix, then you can use thing as if it were an instance of Runner but isinstance(thing, Runner) will return False.

>>> from libsemigroups_pybind11 import (KnuthBendix, Presentation,
... presentation, congruence_kind)
>>> p = Presentation("abc")
>>> presentation.add_rule(p, "aaaa", "a")
>>> presentation.add_rule(p, "bbbb", "b")
>>> presentation.add_rule(p, "cccc", "c")
>>> presentation.add_rule(p, "abab", "aaa")
>>> presentation.add_rule(p, "bcbc", "bbb")
>>> kb = KnuthBendix(congruence_kind.twosided, p)
>>> not kb.confluent()
True
>>> kb.run()
>>> kb.number_of_active_rules()
31
>>> kb.confluent()
True

Contents

`KnuthBendix`	Class containing an implementation of the Knuth-Bendix Algorithm.
`KnuthBendix.active_rules`(…)	Return a copy of the active rules.
`KnuthBendix.add_generating_pair`(…)	Add a generating pair.
`KnuthBendix.check_confluence_interval`(…)	Overloaded function.
`KnuthBendix.confluent`(…)	Check confluence of the current rules.
`KnuthBendix.confluent_known`(…)	Check if the current system knows the state of confluence of the current rules.
`KnuthBendix.contains`(…)	Check containment of a pair of words.
`KnuthBendix.copy`(…)	Copy a `KnuthBendix` object.
`KnuthBendix.currently_contains`(…)	Check whether a pair of words is already known to belong to the congruence.
`KnuthBendix.generating_pairs`(…)	Get the generating pairs of the congruence.
`KnuthBendix.gilman_graph`(…)	Return the Gilman `WordGraph`.
`KnuthBendix.gilman_graph_node_labels`(…)	Return the node labels of the Gilman `WordGraph`
`KnuthBendix.init`(…)	Overloaded function.
`KnuthBendix.kind`(…)	The kind of the congruence (1- or 2-sided).
`KnuthBendix.max_overlap`(…)	Overloaded function.
`KnuthBendix.max_pending_rules`(…)	Overloaded function.
`KnuthBendix.max_rules`(…)	Overloaded function.
`KnuthBendix.number_of_active_rules`(…)	Return the current number of active rules.
`KnuthBendix.number_of_classes`(…)	Compute the number of classes in the congruence.
`KnuthBendix.number_of_generating_pairs`(…)	Returns the number of generating pairs.
`KnuthBendix.number_of_inactive_rules`(…)	Return the current number of inactive rules.
`KnuthBendix.overlap_policy`(…)	Overloaded function.
`KnuthBendix.presentation`(…)	Get the presentation used to define a `KnuthBendix` instance (if any).
`KnuthBendix.reduce`(…)	Reduce a word.
`KnuthBendix.reduce_no_run`(…)	Reduce a word.
`KnuthBendix.total_rules`(…)	Return the number of rules that have been created

Full API

class KnuthBendix

__init__(*args, **kwargs)

Overloaded function.

__init__(word: type, rewriter: str) → None

Default constructor.

This function default constructs an uninitialised KnuthBendix instance.

Keyword Arguments:

word (type) – the type of words to use, must be either str or list[int]
rewriter (str) – the type of rewriter to use, must be either "RewriteTrie" or "RewriteFromLeft".

__init__(self: KnuthBendix, knd: congruence_kind, p: Presentation) → None

Construct from congruence_kind and Presentation.

This function constructs a KnuthBendix instance representing a congruence of kind knd over the semigroup or monoid defined by the presentation p.

Parameters:

knd (congruence_kind) – the kind (onesided or twosided) of the congruence.
p (Presentation) – the presentation.

Raises:

LibsemigroupsError – if p is not valid.

active_rules(self: KnuthBendix) → collections.abc.Iterator[tuple[str, str]]

Return a copy of the active rules.

This member function returns an iterator yielding of the pairs of strings which represent the rewriting rules. The first entry in every such pair is greater than the second according to the reduction ordering of the KnuthBendix instance. The rules are sorted according to the reduction ordering used by the rewriting system, on the first entry.

Returns:: An iterator yielding the currently active rules.
Return type:: collections.abc.Iterator[tuple[str, str]]

add_generating_pair(self: KnuthBendix, u: list[int] | str, v: list[int] | str) → KnuthBendix

Add a generating pair.

This function adds a generating pair to the congruence represented by a KnuthBendix instance.

Parameters:

u (list[int] | str) – the first item in the pair.
v (list[int] | str) – the second item in the pair.

Returns:

self.

Return type:

KnuthBendix

Raises:

LibsemigroupsError – if any of the values in u or v is out of range, i.e. they do not belong to presentation().alphabet() and Presentation.throw_if_letter_not_in_alphabet raises.
LibsemigroupsError – if Runner.started returns True.

check_confluence_interval(*args, **kwargs)

Overloaded function.

check_confluence_interval(self: KnuthBendix) → int

Return the interval at which confluence is checked.

The function Runner.run periodically checks if the system is already confluent. This function can be used to return how frequently this happens. It is the number of new overlaps that should be considered before checking confluence.

Returns:: The interval at which confluence is checked.
Return type:: int

See also

Runner.run.

check_confluence_interval(self: KnuthBendix, val: int | LimitMax) → KnuthBendix

Set the interval at which confluence is checked.

The function Runner.run() periodically checks if the system is already confluent. This function can be used to set how frequently this happens. It is the number of new overlaps that should be considered before checking confluence. Setting this value too low can adversely affect the performance of Runner.run.

The default value is 4096, and should be set to LIMIT_MAX if Runner.run should never check if the system is already confluent.

Parameters:: val (int | LimitMax) – The new value of the interval.
Returns:: self.
Return type:: KnuthBendix

confluent(self: KnuthBendix) → bool

Check confluence of the current rules.

Returns:: True if the KnuthBendix instance is confluent and False if it is not.
Return type:: bool

confluent_known(self: KnuthBendix) → bool

Check if the current system knows the state of confluence of the current rules.

Returns:: True if the confluence of the rules in the KnuthBendix instance is known, and False if it is not.
Return type:: bool

contains(self: KnuthBendix, u: list[int] | str, v: list[int] | str) → bool

Check containment of a pair of words.

This function checks whether or not the words u and v are contained in the congruence represented by a KnuthBendix instance.

Parameters:

u (list[int] | str) – the first word.
v (list[int] | str) – the second word.

Returns:

Whether or not the pair belongs to the congruence.

Return type:

bool

Raises:

LibsemigroupsError – if any of the values in u or v is out of range, i.e. they do not belong to presentation().alphabet() and Presentation.throw_if_letter_not_in_alphabet raises.

copy(self: KnuthBendix) → KnuthBendix

Copy a KnuthBendix object.

Returns:: A copy.
Return type:: KnuthBendix

currently_contains(self: KnuthBendix, u: list[int] | str, v: list[int] | str) → tril

Check whether a pair of words is already known to belong to the congruence.

This function checks whether or not the words u and v are already known to be contained in the congruence represented by a KnuthBendix instance. This function performs no enumeration, so it is possible for the words to be contained in the congruence, but that this is not currently known.

Parameters:

u (list[int] | str) – the first word.
v (list[int] | str) – the second word.

Returns:

tril.true if the words are known to belong to the congruence;
tril.false if the words are known to not belong to the congruence;
tril.unknown otherwise.

Return type:

tril

Raises:

LibsemigroupsError – if any of the values in u or v is out of range, i.e. they do not belong to presentation().alphabet() and Presentation.throw_if_letter_not_in_alphabet raises.

generating_pairs(self: KnuthBendix) → list[list[int] | str]

Get the generating pairs of the congruence.

This function returns the generating pairs of the congruence as added via KnuthBendix.add_generating_pair.

Returns:: The list of generating pairs.
Return type:: list[list[int] | str]

gilman_graph(self: KnuthBendix) → WordGraph

Return the Gilman WordGraph.

The Gilman WordGraph is a digraph where the labels of the paths from the initial node (corresponding to the empty word) correspond to the short-lex normal forms of the semigroup elements.

The semigroup is finite if the graph is acyclic, and infinite otherwise.

Returns:: The Gilman WordGraph.
Return type:: WordGraph

Warning

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

gilman_graph_node_labels(self: KnuthBendix) → list[str]

Return the node labels of the Gilman WordGraph

Return the node labels of the Gilman WordGraph, corresponding to the unique prefixes of the left-hand sides of the rules of the rewriting system.

Returns:: The node labels of the Gilman WordGraph
Return type:: list[str]

See also

gilman_graph.

init(*args, **kwargs)

Overloaded function.

init(self: KnuthBendix) → KnuthBendix

Re-initialize a KnuthBendix instance.

This function puts a KnuthBendix instance back into the state that it would have been in if it had just been newly default constructed.

Returns:: self.
Return type:: KnuthBendix

init(self: KnuthBendix, knd: congruence_kind, p: Presentation) → KnuthBendix

Re-initialize a KnuthBendix instance.

This function re-initializes a KnuthBendix instance as if it had been newly constructed from knd and p.

Parameters:

knd (congruence_kind) – the kind (onesided or twosided) of the congruence.
p (Presentation) – the presentation.

Returns:

self.

Return type:

KnuthBendix

Raises:

LibsemigroupsError – if p is not valid.

kind(self: Congruence | Kambites | KnuthBendix | ToddCoxeter) → congruence_kind

The kind of the congruence (1- or 2-sided).

This function returns the kind of the congruence represented by self. See congruence_kind for details.

Returns:: The kind of the congruence (1- or 2-sided).
Return type:: congruence_kind
Complexity:: Constant.

max_overlap(*args, **kwargs)

Overloaded function.

max_overlap(self: KnuthBendix) → int | PositiveInfinity

Return the maximum length of overlaps to be considered.

This function returns the maximum length of the overlap of two left hand sides of rules that should be considered in Runner.run.

Returns:: The maximum overlap length
Return type:: int | PositiveInfinity

See also

Runner.run.

max_overlap(self: KnuthBendix, val: int | PositiveInfinity) → KnuthBendix

Set the maximum length of overlaps to be considered.

This function can be used to specify the maximum length of the overlap of two left hand sides of rules that should be considered in Runner.run.

If this value is less than the longest left hand side of a rule, then Runner.run can terminate without the system being confluent.

Parameters:: val (int | PositiveInfinity) – The new value of the maximum overlap length.
Returns:: self.
Return type:: KnuthBendix

See also

Runner.run.

max_pending_rules(*args, **kwargs)

Overloaded function.

max_pending_rules(self: KnuthBendix) → int

Return the number of pending rules that must accumulate before they are reduced, processed, and added to the system.

The default value is 128. A value of 1 means Runner.run should attempt to add each rule as it is created without waiting for rules to accumulate.

Returns:: The batch size.
Return type:: int

See also

Runner.run.

max_pending_rules(self: KnuthBendix, val: int) → KnuthBendix

Specify the number of pending rules that must accumulate before they are reduced, processed, and added to the system.

The default value is 128, and should be set to 1 if Runner.run should attempt to add each rule as it is created without waiting for rules to accumulate.

Parameters:: val (int) – The new value of the batch size.
Returns:: self.
Return type:: KnuthBendix

See also

Runner.run.

max_rules(*args, **kwargs)

Overloaded function.

max_rules(self: KnuthBendix) → int | PositiveInfinity

Return the maximum number of rules.

This member function returns the (approximate) maximum number of rules that the system should contain. If this is number is exceeded in calls to Runner.run or knuth_bendix.by_overlap_length, then they will terminate and the system may not be confluent.

Returns:: The maximum number of rules the system should contain.
Return type:: int | PositiveInfinity

See also

Runner.run.

max_rules(self: KnuthBendix, val: int | PositiveInfinity) → KnuthBendix

Set the maximum number of rules.

This member function sets the (approximate) maximum number of rules that the system should contain. If this is number is exceeded in calls to Runner.run or knuth_bendix.by_overlap_length, then they will terminate and the system may not be confluent.

By default this value is POSITIVE_INFINITY.

Parameters:: val (int | PositiveInfinity) – The maximum number of rules.
Returns:: self.
Return type:: KnuthBendix

See also

Runner.run.

number_of_active_rules(self: KnuthBendix) → int

Return the current number of active rules.

Returns:: The current number of active rules.
Return type:: int

number_of_classes(self: KnuthBendix) → int | PositiveInfinity

Compute the number of classes in the congruence. This function computes the number of classes in the congruence represented by a KnuthBendix instance.

Returns:: The number of congruence classes of a KnuthBendix instance if this number is finite, or POSITIVE_INFINITY in some cases if this number is not finite.
Return type:: int | PositiveInfinity

number_of_generating_pairs(self: Congruence | Kambites | KnuthBendix | ToddCoxeter) → int

Returns the number of generating pairs.

This function returns the number of generating pairs of the congruence.

Returns:: The number of generating pairs.
Return type:: int
Complexity:: Constant.

number_of_inactive_rules(self: KnuthBendix) → int

Return the current number of inactive rules.

Returns:: The current number of inactive rules.
Return type:: int

overlap_policy(*args, **kwargs)

Overloaded function.

overlap_policy(self: KnuthBendix) → KnuthBendix.options.overlap

Return the overlap policy.

This function returns the way that the length of an overlap of two words in the system is measured.

Returns:: The overlap policy.
Return type:: KnuthBendix.options.overlap

See also

overlap.

overlap_policy(self: KnuthBendix, val: KnuthBendix.options.overlap) → KnuthBendix

Set the overlap policy.

This function can be used to determine the way that the length of an overlap of two words in the system is measured.

Parameters:: val (KnuthBendix.options.overlap) – The overlap policy.
Returns:: self.
Return type:: KnuthBendix

See also

overlap.

presentation(self: KnuthBendix) → Presentation

Get the presentation used to define a KnuthBendix instance (if any). If a KnuthBendix instance is constructed or initialised using a presentation, then this presentation is returned by this function.

Returns:: The presentation used to construct or initialise a KnuthBendix instance.
Return type:: Presentation

reduce(self: KnuthBendix, w: list[int] | str) → list[int] | str

Reduce a word.

This function triggers a full enumeration of an KnuthBendix object and then reduces the word w. As such the returned word is a normal form for the input word.

Parameters:: w (list[int] | str) – the input word.
Returns:: A normal form for the input word.
Return type:: list[int] | str
Raises:: LibsemigroupsError – if any of the values in w is out of range, i.e. they do not belong to presentation().alphabet() and Presentation.throw_if_letter_not_in_alphabet raises.

reduce_no_run(self: KnuthBendix, w: list[int] | str) → list[int] | str

Reduce a word.

If Runner.finished returns True, then this function returns a normal form for the input word w.

Otherwise, this function returns the word w rewritten according to the current rules in the KnuthBendix instance.

Parameters:: w (list[int] | str) – the input word.
Returns:: A word equivalent to the input word.
Return type:: list[int] | str
Raises:: LibsemigroupsError – if any of the values in w is out of range, i.e. they do not belong to presentation().alphabet() and Presentation.throw_if_letter_not_in_alphabet raises.

total_rules(self: KnuthBendix) → int

Return the number of rules that have been created

Return the total number of Rule instances that have been created whilst whilst the Knuth-Bendix algorithm has been running. Note that this is not the sum of number_of_active_rules and number_of_inactive_rules, due to the re-initialisation of rules where possible.

Returns:: The total number of rules.
Return type:: int