From 99edd1d39739792a423c5e3fb42b04e4cd95253f Mon Sep 17 00:00:00 2001 From: Marek Kaluba Date: Sat, 18 Dec 2021 16:40:17 +0100 Subject: [PATCH 1/4] enhance dostrings for WordOrderings * remove generic docstrings * make the remaining dostrings more descriptive --- src/orderings.jl | 68 +++++++++++++++++++++--------------------------- 1 file changed, 29 insertions(+), 39 deletions(-) diff --git a/src/orderings.jl b/src/orderings.jl index ecf5b9da..585d481d 100644 --- a/src/orderings.jl +++ b/src/orderings.jl @@ -3,12 +3,12 @@ export LenLex, WreathOrder, RecursivePathOrder """ WordOrdering <: Ordering -Abstract type representing word orderings. +Abstract type representing well-orderings of words which are translation invariant. -The subtypes of `WordOrdering` should contain a field `A` storing the `Alphabet` -over which a particular order is defined. Moreover, an `Base.lt` method should be -defined to compare whether one word is less than the other (in the ordering -defined). +The subtypes of `WordOrdering` should implement: + * `alphabet` - function (not necessary if they contain a field `A` storing the `Alphabet`), over which a particular order is defined; + * `Base.Order.lt(o::WordOrdering, a, b)` - method to test whether `a` is less than `b` according to the ordering `o`. + * `Base.hash` - a simple hashing function. """ abstract type WordOrdering <: Ordering end @@ -17,10 +17,9 @@ Base.:(==)(o1::T, o2::T) where {T<:WordOrdering} = alphabet(o1) == alphabet(o2) """ struct LenLex{T} <: WordOrdering + LenLex(A::Alphabet) -Basic structure representing Length+Lexicographic (left-to-right) ordering of -the words over given Alphabet. Lexicographic ordering of an Alphabet is -implicitly specified inside Alphabet struct. +`LenLex` order compares words first by length and then by lexicographic (left-to-right) order determined by the order of letters `A`. """ struct LenLex{T} <: WordOrdering A::Alphabet{T} @@ -28,14 +27,9 @@ end Base.hash(o::LenLex, h::UInt) = hash(o.A, hash(h, hash(LenLex))) -""" - lt(o::LenLex, p::AbstractWord, q::AbstractWord) - -Return whether the first word is less then the other one in a given LenLex ordering. -""" function lt(o::LenLex, p::AbstractWord, q::AbstractWord) if length(p) == length(q) - for (a, b) in zip(p,q) + for (a, b) in zip(p, q) a == b || return isless(a, b) # comparing only on positive pointer values end return false @@ -44,13 +38,19 @@ function lt(o::LenLex, p::AbstractWord, q::AbstractWord) end end - """ struct WreathOrder{T} <: WordOrdering + WreathOrder(A::Alphabet) -Structure representing Basic Wreath-Product ordering (determined by the Lexicographic -ordering of the Alphabet) of the words over given Alphabet. This Lexicographic -ordering of an Alphabet is implicitly specified inside Alphabet struct. +`WreathOrder` compares words wreath-product ordering of words over the given `Alphabet`. Internal lexicographic ordering is determined by the order of letters `A`. +Here wreath product refers to +> `⟨A[1]⟩ ≀ ⟨A[2]⟩ ≀ … ≀ ⟨A[n]⟩`, +where `⟨A[i]⟩` denotes the monoid generated by `i`-th letter. + +For the precise definition see e.g. +> Charles C. Sims, _Computation with finitely presented groups_ +> Cambridge University Press 1994, +> pages 46-47. """ struct WreathOrder{T} <: WordOrdering A::Alphabet{T} @@ -58,11 +58,6 @@ end Base.hash(o::WreathOrder, h::UInt) = hash(o.A, hash(h, hash(WreathOrder))) -""" - lt(o::WreathOrder, p::AbstractWord, q::AbstractWord) - -Return whether the first word is less then the other one in a given WreathOrder ordering. -""" function lt(o::WreathOrder, p::AbstractWord, q::AbstractWord) iprefix = lcp(p, q) + 1 @@ -89,33 +84,28 @@ function lt(o::WreathOrder, p::AbstractWord, q::AbstractWord) # i.e. head_p_len == head_q_len first_pp = findfirst(isequal(max_p), pp) first_qq = findfirst(isequal(max_p), qq) - return @views lt(o, pp[1:first_pp - 1], qq[1:first_qq - 1]) + return @views lt(o, pp[1:first_pp-1], qq[1:first_qq-1]) end - """ struct RecursivePathOrder{T} <: WordOrdering + RecursivePathOrder(A::Alphabet) + +`RecursivePathOrder` represents a rewriting ordering of words over the given `Alphabet`. +Internal lexicographic ordering is determined by the order of letters `A`. -Structure representing Recursive Path Ordering (determined by the Lexicographic -ordering of the Alphabet) of the words over given Alphabet. This Lexicographic -ordering of an Alphabet is implicitly specified inside Alphabet struct. -For the definition see -> Susan M. Hermiller, Rewriting systems for Coxeter groups -> _Journal of Pure and Applied Algebra_ -> Volume 92, Issue 2, 7 March 1994, Pages 137-148. +For the precise definition see +> Susan M. Hermiller, Rewriting systems for Coxeter groups, +> _Journal of Pure and Applied Algebra_, +> Volume 92, Issue 2, 7 March 1994, pages 137-148. """ struct RecursivePathOrder{T} <: WordOrdering A::Alphabet{T} end -Base.hash(o::RecursivePathOrder, h::UInt) = hash(o.A, hash(h, hash(RecursivePathOrder))) +Base.hash(o::RecursivePathOrder, h::UInt) = + hash(o.A, hash(h, hash(RecursivePathOrder))) -""" - lt(o::RecursivePathOrder, p::AbstractWord, q::AbstractWord) - -Return whether the first word is less then the other one in a given -RecursivePathOrder ordering. -""" function lt(o::RecursivePathOrder, p::AbstractWord, q::AbstractWord) isone(p) && return !isone(q) isone(q) && return false From 99cd250b630def8820ebfe09b881643af5c96908 Mon Sep 17 00:00:00 2001 From: Marek Kaluba Date: Sat, 18 Dec 2021 16:40:41 +0100 Subject: [PATCH 2/4] add WeightedLex --- src/orderings.jl | 53 ++++++++++++++++++++++++++++++++++++++++++++++- test/orderings.jl | 11 ++++++++++ 2 files changed, 63 insertions(+), 1 deletion(-) diff --git a/src/orderings.jl b/src/orderings.jl index 585d481d..075e09b8 100644 --- a/src/orderings.jl +++ b/src/orderings.jl @@ -1,5 +1,5 @@ import Base.Order: lt, Ordering -export LenLex, WreathOrder, RecursivePathOrder +export LenLex, WreathOrder, RecursivePathOrder, WeightedLex """ WordOrdering <: Ordering @@ -122,3 +122,54 @@ function lt(o::RecursivePathOrder, p::AbstractWord, q::AbstractWord) end return false end + +""" + struct WeightedLex{T} <: WordOrdering + WeightedLex(A::Alphabet, weights::AbstractVector) + +`WeightedLex` order compares words first according to their weight and then +by the lexicographic order determined by the order of letters `A`. +The `weight` array assigns weights to each letter and the weight of a word is +simply the sum of weights of all letters. +The `LenLex` ordering is a special case of `WeightedLex` when all weights are equal to `1`. + +!!! note: + Since empty word is assigned a value of `zero(eltype(weights))` a vector of + positive weights is strongly recommended. +""" +struct WeightedLex{T,S} <: WordOrdering + A::Alphabet{T} + weights::Vector{S} + + function WeightedLex(A::Alphabet{T}, weights::AbstractVector{S}) where {T,S} + @assert length(weights) == length(A) + @assert all(w-> w >=(zero(S)), weights) + return new{T,S}(A, weights) + end +end + +Base.hash(wl::WeightedLex, h::UInt) = hash(wl.weights, hash(wl.lenlex, h)) + +Base.@propagate_inbounds weight(o::WeightedLex, l::Integer) = o.weights[l] + +function weight(o::WeightedLex, p::AbstractWord) + isone(p) && return zero(eltype(o.weights)) + return @inbounds sum(weight(o, l) for l in p) +end + +function Base.Order.lt(o::WeightedLex, p::AbstractWord, q::AbstractWord) + S = eltype(o.weights) + + weight_p = weight(o, p) + weight_q = weight(o, q) + + if weight_p == weight_q + for (a, b) in zip(p, q) + # comparing only on positive pointer values + a == b || return isless(a, b) + end + return false + else + return isless(weight_p, weight_q) + end +end diff --git a/test/orderings.jl b/test/orderings.jl index 400fdaa8..17da81dc 100644 --- a/test/orderings.jl +++ b/test/orderings.jl @@ -55,4 +55,15 @@ @test sort(a, order = rpo) == [ε, w1, w14, w214, w1224] @test sort(b, order = rpo) == [ε, w1, w2, w214, w41, w241, w32141] + @test_throws AssertionError WeightedLex(A, [1,2,3]) + @test_throws AssertionError WeightedLex(A, [1,2, 3,-4]) + + wtlex = WeightedLex(A, [1,2,3,4]) + + @test lt(wtlex, one(Word{Int}), Word([1])) + @test !lt(wtlex, Word([1]), Word([1])) + @test lt(wtlex, Word([1,1]), Word([2])) + @test lt(wtlex, Word([2]), Word([1,1,1])) + @test lt(wtlex, Word([2,4]), Word([4,2])) + @test lt(wtlex, Word([2,4]), Word([4,1,1])) end From 5add443d28c162770508b1f37dbaa33b1cc34844 Mon Sep 17 00:00:00 2001 From: Marek Kaluba Date: Sat, 18 Dec 2021 16:41:03 +0100 Subject: [PATCH 3/4] bump to 0.3.1 --- Project.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Project.toml b/Project.toml index 197dca04..f4fdaffd 100644 --- a/Project.toml +++ b/Project.toml @@ -1,7 +1,7 @@ name = "KnuthBendix" uuid = "c2604015-7b3d-4a30-8a26-9074551ec60a" authors = ["Marek Kaluba ", "Mikołaj Pabiszczak "] -version = "0.3.0" +version = "0.3.1" [deps] MacroTools = "1914dd2f-81c6-5fcd-8719-6d5c9610ff09" From e275a07ea86cd6699b23a9e3e8e0a0e1020a7040 Mon Sep 17 00:00:00 2001 From: Marek Kaluba Date: Sat, 18 Dec 2021 17:37:53 +0100 Subject: [PATCH 4/4] add Coxeter groups confluent rws to tests --- test/rws_examples.jl | 139 +++++++++++++++++++++++++++++++++++------- test/test_examples.jl | 8 +++ 2 files changed, 124 insertions(+), 23 deletions(-) diff --git a/test/rws_examples.jl b/test/rws_examples.jl index 0ba2a35d..b7e9a798 100644 --- a/test/rws_examples.jl +++ b/test/rws_examples.jl @@ -3,10 +3,10 @@ function RWS_Example_5_1() KnuthBendix.set_inversion!(Al, 'a', 'A') KnuthBendix.set_inversion!(Al, 'b', 'B') - a,A,b,B = Word.([i] for i in 1:4) + a, A, b, B = Word.([i] for i in 1:4) ε = one(a) - R = RewritingSystem([b*a=>a*b], LenLex(Al)) + R = RewritingSystem([b * a => a * b], LenLex(Al)) return R end @@ -18,10 +18,10 @@ function RWS_Example_5_2() KnuthBendix.set_inversion!(Al, 'a', 'A') KnuthBendix.set_inversion!(Al, 'b', 'B') - a,b,B,A = Word.([i] for i in 1:4) + a, b, B, A = Word.([i] for i in 1:4) ε = one(a) - R = RewritingSystem([b*a=>a*b], LenLex(Al)) + R = RewritingSystem([b * a => a * b], LenLex(Al)) return R end @@ -31,10 +31,10 @@ RWS_ZxZ_nonterminating() = RWS_Example_5_2() function RWS_Example_5_3() Al = Alphabet(['a', 'b']) - a,b = Word.([i] for i in 1:2) + a, b = Word.([i] for i in 1:2) ε = one(a) - R = RewritingSystem([a^2=>ε, b^3=>ε, (a*b)^3=>ε], LenLex(Al)) + R = RewritingSystem([a^2 => ε, b^3 => ε, (a * b)^3 => ε], LenLex(Al)) return R end @@ -43,10 +43,10 @@ function RWS_Example_5_4() Al = Alphabet(['a', 'b', 'B']) KnuthBendix.set_inversion!(Al, 'b', 'B') - a,b,B = Word.([i] for i in 1:3) + a, b, B = Word.([i] for i in 1:3) ε = one(a) - R = RewritingSystem([a^2=>ε, b^3=>ε, (a*b)^3=>ε], LenLex(Al)) + R = RewritingSystem([a^2 => ε, b^3 => ε, (a * b)^3 => ε], LenLex(Al)) return R end @@ -60,7 +60,7 @@ function RWS_Example_5_5() c, C, b, B, a, A = Word.([i] for i in 1:6) ε = one(a) - eqns = [c*a =>a*c, c*b=>b*c, b*a=>a*b*c] + eqns = [c * a => a * c, c * b => b * c, b * a => a * b * c] R = RewritingSystem(eqns, WreathOrder(Al)) return R @@ -72,7 +72,13 @@ function RWS_Example_6_4() a, b, B = Word.([i] for i in 1:3) ε = one(a) - eqns = [a*a=>ε, b*B=>ε, b^3=>ε, (a*b)^7=>ε, (a*b*a*B)^4=>ε] + eqns = [ + a * a => ε, + b * B => ε, + b^3 => ε, + (a * b)^7 => ε, + (a * b * a * B)^4 => ε, + ] R = RewritingSystem(eqns, LenLex(Al)) return R @@ -84,9 +90,14 @@ function RWS_Example_6_5() a, b, B = Word.([i] for i in 1:3) ε = one(a) - eqns = KnuthBendix.Rule.( - [a*a=>ε, b*B=>ε, b^2=>B, (B*a)^3*B=>(a*b)^3*a, (b*a*B*a)^2=>(a*b*a*B)^2] - ) + eqns = + KnuthBendix.Rule.([ + a * a => ε, + b * B => ε, + b^2 => B, + (B * a)^3 * B => (a * b)^3 * a, + (b * a * B * a)^2 => (a * b * a * B)^2, + ]) R = RewritingSystem(eqns, LenLex(Al)) return R @@ -100,9 +111,16 @@ function RWS_Example_237_abaB(n) ε = one(a) # eqns = [a^2=>ε, b^3=>ε, (a*b)^7=>ε, (a*b*a*B)^n=>ε] - eqns = [b*B=>ε, B*b=>ε, a^2=>ε, b^3=>ε, (a*b)^7=>ε, (a*b*a*B)^n=>ε] - - R = RewritingSystem(eqns, LenLex(Al), bare=true) + eqns = [ + b * B => ε, + B * b => ε, + a^2 => ε, + b^3 => ε, + (a * b)^7 => ε, + (a * b * a * B)^n => ε, + ] + + R = RewritingSystem(eqns, LenLex(Al), bare = true) return R end @@ -114,35 +132,110 @@ function RWS_Exercise_6_1(n) a, b = Word.([i] for i in 1:2) ε = one(a) - eqns = [a^2=>ε, b^3=>ε, (a*b)^n=>ε] + eqns = [a^2 => ε, b^3 => ε, (a * b)^n => ε] - R = RewritingSystem(eqns, LenLex(Al), bare=true) + R = RewritingSystem(eqns, LenLex(Al), bare = true) return R end function RWS_Closed_Orientable_Surface(n) ltrs = String[] for i in 1:n - subscript = join('₀'+d for d in reverse(digits(i))) - append!(ltrs, ["a" * subscript, "A" * subscript, "b" * subscript, "B" * subscript]) + subscript = join('₀' + d for d in reverse(digits(i))) + append!( + ltrs, + [ + "a" * subscript, + "A" * subscript, + "b" * subscript, + "B" * subscript, + ], + ) end Al = Alphabet(reverse!(ltrs)) for i in 1:n - subscript = join('₀'+d for d in reverse(digits(i))) + subscript = join('₀' + d for d in reverse(digits(i))) KnuthBendix.set_inversion!(Al, "a" * subscript, "A" * subscript) KnuthBendix.set_inversion!(Al, "b" * subscript, "B" * subscript) end ε = one(Word{UInt16}) - rules = Pair{typeof(ε), typeof(ε)}[] + rules = Pair{typeof(ε),typeof(ε)}[] word = Int[] for i in reverse(1:n) x = 4 * i - append!(word, [x, x-2, x-1, x-3]) + append!(word, [x, x - 2, x - 1, x - 3]) end push!(rules, Word(word) => ε) R = RewritingSystem(rules, RecursivePathOrder(Al)) return R end + +function RWS_Coxeter_group_cube() + _coxeter_letter(simplex) = Symbol("s", join(simplex, "")) + + function coxeter_alphabet(itr) + letters = [_coxeter_letter(v) for v in itr] + inverses = 1:length(letters) # generators are of order 2 i.e. self-inverse + return KnuthBendix.Alphabet(letters, inverses) + end + + vertices = [[i,] for i in 1:8] + edges = [ + [1, 2], + [1, 3], + [1, 5], + [2, 4], + [2, 6], + [3, 5], + [3, 7], + [4, 8], + [5, 6], + [5, 7], + [6, 8], + [7, 8], + ] # 3-cube + + A = coxeter_alphabet([edges; vertices]) + weights = [fill(2, length(edges)); fill(1, length(vertices))] + wtlex = WeightedLex(A, weights) + + S = Dict(v => Word([A[_coxeter_letter(v)]]) for v in vertices) + for σ in edges + S[σ] = Word([A[_coxeter_letter(σ)]]) + end + + rels = map(edges) do e + v1, v2 = [first(e)], [last(e)] + s1, s2, s12 = S[v1], S[v2], S[e] + return [ # (1)(2) → (12), (2)(1) → (12) + s1 * s2 => s12, + s2 * s1 => s12, + #(1)(12) → (2) (2)(12) → (1) (12)(1) → (2) (12)(2) → (1) + s1 * s12 => s2, + s2 * s12 => s1, + s12 * s1 => s2, + s12 * s2 => s1, + ] + end + + rels2 = eltype(eltype(rels))[] + for e in edges + for f in edges + if length(intersect(e, f)) == 1 + edge = union(setdiff(e, f), setdiff(f, e)) + @assert length(edge) == 2 + haskey(S, edge) || reverse!(edge) + if haskey(S, edge) + # (12)(13) → (23) + push!(rels2, S[e] * S[f] => S[edge]) + end + end + end + end + push!(rels, rels2) + + return RewritingSystem(vcat(rels...), wtlex) +end diff --git a/test/test_examples.jl b/test/test_examples.jl index 023287de..4b9e3a40 100644 --- a/test/test_examples.jl +++ b/test/test_examples.jl @@ -37,6 +37,10 @@ _length(rws) = length(collect(KnuthBendix.rules(rws))) R = RWS_Closed_Orientable_Surface(3) rws = KnuthBendix.knuthbendix(R, implementation=:naive_kbs1) @test _length(rws) == 16 + + R = RWS_Coxeter_group_cube() + rws = KnuthBendix.knuthbendix(R, implementation=:naive_kbs1, maxrules=300) + @test _length(rws) == 205 end function test_kbs2_methods(R, methods, len) @@ -89,6 +93,10 @@ end R = RWS_Closed_Orientable_Surface(3) rws = KnuthBendix.knuthbendix(R, implementation=:naive_kbs2) @test _length(rws) == 16 + + R = RWS_Coxeter_group_cube() + rws = KnuthBendix.knuthbendix(R, implementation=:naive_kbs2, maxrules=300) + @test _length(rws) == 205 end @testset "KBS-automata" begin