Orders

RewritingOrdering

Abstract type representing translation bi-invariant well-orderings on free monoids over an alphabet. Translation (bi-)invariance means that whenever u < v, then aub < avb for arbitrary words a and b. In particular ε (the monoid identity) is the smallest word for any RewritingOrdering.

The subtypes of RewritingOrdering must implement:

• alphabet which returns the underlying alphabet, over which a particular order is defined;
• Base.Order.lt(o::RewritingOrdering, a::AbstractWord, b::AbstractWord) to test whether a is less than b according to the ordering o.

alphabet(ord::RewritingOrdering)

Return the alphabet of the free monoid on which ord is defined.

alphabet(rws::AbstractRewritingSystem)

Return the underlying Alphabet of the rewriting system.

LenLex{T} <: LexOrdering
LenLex(A::Alphabet[; order=collect(A)])

Compare words first by their length, then break ties by (left-)lexicographic order.

Example

julia> Al = Alphabet([:a, :A, :b, :B]);

julia> ll1 = LenLex(Al)
LenLex: a < A < b < B

julia> ll2 = LenLex(Al, order=[:a, :b, :A, :B])
LenLex: a < b < A < B

julia> a, A, b, B = [Word([i]) for i in 1:length(Al)];

julia> lt(ll1, a*A, a*b)
true

julia> lt(ll2, a*A, a*b)
false

WeightedLex{T,S} <: LexOrdering
WeightedLex(A::Alphabet; weights[, order=collect(A)])

Compare words first by their weight, then break ties by (left-)lexicographic order.

The weights vector assigns weights to each letter as they appear in the alphabet and the weight of a word is the sum of weights of all of its letters.

With all weights equal to 1 WeightedLex becomes LenLex.

Example

julia> al = Alphabet([:a, :A, :b, :B]);

julia> a, A, b, B = (Word([i]) for i in 1:length(al));

julia> wtlex = WeightedLex(al, weights=[1, 2, 3, 4], order=[:a, :b, :B, :A])
WeightedLex: a(1) < b(3) < B(4) < A(2)

julia> lt(wtlex, b * B, B * a * a * a)
true

julia> lt(wtlex, A*B, B*A)
false

WreathOrder{T,S} <: RewritingOrdering
WreathOrder(A::Alphabet; levels[, order=collect(A)])

Compare words first by their levels, then break ties by recursion on prefixes.

The levels vector assigns levels to each letter as they appear in the alphabet and the level of a word is the maximum of levels of all its letters.

The order compare words first by their levels, then break ties by LenLex order of pure max-level words. Further ties are resolved by recursing on lower level prefixes.

Definition

Let U = U₀·a₁·U₁·…·aᵣ·Uᵣ be a decomposition of U such that

• all aᵢs are at the same (maximal) level and
• each Uᵢ is at level strictly smaller.

Let V = V₀·b₁·V₁·…·bₛ·Vₛ be a similar decomposition. Then U <≀ V if either

• a₁·…·aᵣ < b₁·…·bₛ according to LenLex order, or
• a₁·…·aᵣ = b₁·…·bₛ and U₀ <≀ V₀, or Uᵢ = Vᵢ for 0≤i<k but Uₖ <≀ Vₖ.

For more references see

1. C. Sims Computation with finitely presented groups, p. 46-47
2. D. Holt, B. Eick and E. O’Brien Handbook of Computational Group Theory, Section 12.4 Rewriting systems for polycyclic groups, p. 426-427
3. S. Rees Automatic groups associated with word orders other than shortlex Section 5.3 Wreath product orders.

Example

julia> X = Alphabet([:a, :b]);

julia> a, b = Word([1]), Word([2]);

julia> wro = WreathOrder(X, levels = [1, 2])
WreathOrder: a(1) < b(2)

julia> lt(wro, a^100, a * b * a^2) # by level only
true

julia> lt(wro, b^2*a, a^2 * b * a) # by max-level word
false

julia> lt(wro, a * b * a^2, a^2 * b * a) # by the lower level prefix
true

Recursive{Side,T} <: RewritingOrdering
Recursive{Side}(A::Alphabet; order=collect(A))

A special case of WreathOrder where each letter is given a unique level.

Since levels are unique they just linearly order letters in the alphabet A. The order generally promotes smaller generators, and larger ones will occur in minimal words relatively early. For example if a < b then a·b > b·aⁿ.

Definition

Given a partial order (A, <) on an alphabet A, for p, q ∈ A* we say that p < q w.r.t. left-recursive ordering if

1. p == ε ≠ q, or
2. p = p′·a, q = q′·b for some a, b ∈ A and
   • a == b and p′ < q′, or
   • a < b and p < q′, or
   • a > b and p′ < q

For the right-recursive ordering one needs to change the decompositions in point 2. to

p = a·p′, q = b·q′ for some a, b ∈ A …

For more details consult

M. Jentzen Confluent String Rewriting, Definition 1.2.14 p.24.

The ordering is sometimes also known as recursive path ordering and is useful e.g. for polycyclic groups.

Example

julia> X = Alphabet([:b, :a, :A],[0, 3, 2]);

julia> b, a, A = [Word([i]) for i in 1:length(X)];

julia> rec = Recursive(X, order=[:a, :A, :b])
KnuthBendix.Left-Recursive: a < A < b

julia> lt(rec, b*a^10, a*b)
true

julia> lt(rec, b*a^10, b)
false

julia> lt(rec, a*A, b*a^10)
true

julia> rt_rec = Recursive{KnuthBendix.Right}(X, order=[:a, :A, :b])
KnuthBendix.Right-Recursive: a < A < b