GitHub

Rewriting System

It's just a struct that holds things together required for Knuth-Bendix completion.

KnuthBendix.RewritingSystem — Type
RewritingSystem{W<:AbstractWord, O<:Ordering}
RewritingSystem(rwrules::Vector{Pair{W,W}}, order[; confluent=false, reduced=false])

RewritingSystem holds the list of ordered (by order) rewriting rules of W<:AbstractWords.

source
KnuthBendix.rules — Method
rules(rws::AbstractRewritingSystem)

Return the iterator over active rewriting rules.

source
KnuthBendix.alphabet — Method
alphabet(rws::AbstractRewritingSystem)

Return the underlying Alphabet of the rewriting system.

source
KnuthBendix.isreduced — Function
isreduced(rws::RewritingSystem)

Check whether the rewriting system knows its reducedness.

Note

Rewriting systems assume non-reducedness at creation. knuthbendix will always return reduced rewriting system, unless manually interrupted.

source
KnuthBendix.isconfluent — Function
isconfluent(rws::RewritingSystem)

Check whether the rewriting system is confluent.

Note

Since check_confluence is relatively cheap only for reduced rewriting systems isconfluent will not try to reduce the system on its own and will return false. For definitive answer one should reduce! the rewrting system before calling isconfluent.

source
KnuthBendix.check_confluence — Function
check_confluence(rws::AbstractRewritingSystem)

Check if a reduced rewriting system is confluent.

The check constructs index automaton for rws and runs a backtrack search for all rules of the system. Return a stack of critical pairs and an index of the rule for which local confluence failed. The returned stack is empty if and only if rws is confluent.

source
KnuthBendix.isirreducible — Method
isirreducible(w::AbstractWord, rws::RewritingSystem)

Returns whether a word is irreducible with respect to a given rewriting system

source