From 5d1317316bb93c0237269311ab6657299080addb Mon Sep 17 00:00:00 2001 From: Marek Kaluba Date: Mon, 26 Apr 2021 11:49:09 +0200 Subject: [PATCH 01/10] replace A.alphabet by letters(A::Alphabet) --- src/alphabets.jl | 42 +++++++++++++++++++++++++----------------- test/alphabets.jl | 6 +++--- 2 files changed, 28 insertions(+), 20 deletions(-) diff --git a/src/alphabets.jl b/src/alphabets.jl index 30cab6ba..e326e053 100644 --- a/src/alphabets.jl +++ b/src/alphabets.jl @@ -19,7 +19,7 @@ Alphabet of String: ``` """ mutable struct Alphabet{T} - alphabet::Vector{T} + letters::Vector{T} inversions::Vector{Int} function Alphabet{T}(init::Vector{T} = Vector{T}(); safe = true) where T if safe && T <: Integer @@ -30,19 +30,27 @@ mutable struct Alphabet{T} end new(init, fill(0, length(init))) end + + function Alphabet(letters::Vector{T}, inversions::Vector{Int}) where T + @assert !(T<:Integer) "Alphabet over a set of integers is not supported." + @assert length(letters) == length(inversions) + return new{T}(letters, inversions) + end end Alphabet() = Alphabet{Char}() Alphabet(x::Vector{T}; safe = true) where T = Alphabet{T}(x; safe = safe) -Base.length(abt::Alphabet) = length(abt.alphabet) -Base.isempty(A::Alphabet) = isempty(A.alphabet) +letters(A::Alphabet) = A.letters + +Base.length(A::Alphabet) = length(letters(A)) +Base.isempty(A::Alphabet) = isempty(letters(A)) Base.:(==)(A::Alphabet, B::Alphabet) = - A.alphabet == B.alphabet && A.inversions == B.inversions + letters(A) == letters(B) && A.inversions == B.inversions Base.hash(A::Alphabet{T}, h::UInt) where T = - hash(A.alphabet, hash(A.inversions, hash(h, hash(Alphabet{T})))) + hash(letters(A), hash(A.inversions, hash(h, hash(Alphabet{T})))) -Base.show(io::IO, A::Alphabet{T}) where T = print(io, Alphabet{T}, A.alphabet) +Base.show(io::IO, A::Alphabet{T}) where T = print(io, Alphabet{T}, letters(A)) hasinverse(i::Integer, A::Alphabet) = A.inversions[i] > 0 hasinverse(l::T, A::Alphabet{T}) where T = hasinverse(A[l], A) @@ -52,12 +60,12 @@ function Base.show(io::IO, ::MIME"text/plain", A::Alphabet{T}) where T print(io, "Empty alphabet of $(T)") else print(io, "Alphabet of $(T):") - for (i, l) in enumerate(A.alphabet) + for (i, l) in enumerate(letters(A)) print(io, "\n\t$(i).\t") show(io, l) if hasinverse(i, A) print(io, " = (") - show(io, A.alphabet[A.inversions[i]]) + show(io, letters(A)[A.inversions[i]]) print(io, ")⁻¹") end end @@ -82,10 +90,10 @@ Alphabet of String: """ function Base.push!(A::Alphabet{T}, symbols::Vararg{T,1}) where T for s in symbols - if findfirst(symbol -> symbol == s, A.alphabet) !== nothing + if findfirst(symbol -> symbol == s, letters(A)) !== nothing error("Symbol $(s) already in the alphabet.") end - push!(A.alphabet, s) + push!(A.letters, s) push!(A.inversions, 0) end A @@ -121,10 +129,10 @@ Alphabet of String: ``` """ function set_inversion!(A::Alphabet{T}, x::T, y::T) where T - if (ix = findfirst(symbol -> symbol == x, A.alphabet)) === nothing + if (ix = findfirst(symbol -> symbol == x, letters(A))) === nothing error("Element $(x) not found in the alphabet.") end - if (iy = findfirst(symbol -> symbol == y, A.alphabet)) === nothing + if (iy = findfirst(symbol -> symbol == y, letters(A))) === nothing error("Element $(y) not found in the alphabet.") end @@ -161,7 +169,7 @@ julia> getindexbysymbol(A, "c") ``` """ function getindexbysymbol(A::Alphabet{T}, x::T) where T - if (index = findfirst(symbol -> symbol == x, A.alphabet)) === nothing + if (index = findfirst(symbol -> symbol == x, letters(A))) === nothing throw(DomainError("Element '$(x)' not found in the alphabet")) end index @@ -218,12 +226,12 @@ julia> A[-A["a"]] """ function Base.getindex(A::Alphabet{T}, p::Integer) where T if p > 0 - return A.alphabet[p] + return letters(A)[p] elseif p < 0 && A.inversions[-p] > 0 - return A.alphabet[A.inversions[-p]] + return letters(A)[A.inversions[-p]] end - throw(DomainError("Inversion of $(A.alphabet[-p]) is not defined")) + throw(DomainError("Inversion of $(letters(A)[-p]) is not defined")) end """ @@ -233,7 +241,7 @@ Return the inverse of a word `w` in the context of alphabet `A`. function Base.inv(A::Alphabet, w::AbstractWord) res = similar(w) n = length(w) - for (i,l) in enumerate(reverse(w)) + for (i,l) in enumerate(Iterators.reverse(w)) hasinverse(l, A) || throw(DomainError(w, "is not invertible over $A")) res[i] = A.inversions[l] end diff --git a/test/alphabets.jl b/test/alphabets.jl index ac866f0c..0bde3b8b 100644 --- a/test/alphabets.jl +++ b/test/alphabets.jl @@ -8,19 +8,19 @@ @test Alphabet{Integer}(safe = false) isa Alphabet{Integer} A = Alphabet{Char}() - @test length(A.alphabet) == 0 && length(A.inversions) == 0 + @test length(A.letters) == 0 && length(A.inversions) == 0 @test sprint(show, A) isa String B = Alphabet(['a', 'b', 'c']) @test sprint(show, B) isa String @test B isa Alphabet{Char} - @test length(B.alphabet) == 3 && length(B.inversions) == 3 + @test length(B.letters) == 3 && length(B.inversions) == 3 @test findfirst(i -> i != 0, B.inversions) === nothing @test_throws ErrorException Alphabet(['a', 'b', 'a']) push!(A, 'a', 'b', 'c') - @test length(A.alphabet) == 3 && length(A.inversions) == 3 + @test length(A.letters) == 3 && length(A.inversions) == 3 @test findfirst(i -> i != 0, A.inversions) === nothing @test_throws ErrorException push!(A, 'a') From 8c08bbe686ca4193a2035137c42f378e2cc00409 Mon Sep 17 00:00:00 2001 From: Marek Kaluba Date: Mon, 26 Apr 2021 19:08:18 +0200 Subject: [PATCH 02/10] add more tests to RWS_examples --- test/rws_examples.jl | 25 +++++++++++++++---------- 1 file changed, 15 insertions(+), 10 deletions(-) diff --git a/test/rws_examples.jl b/test/rws_examples.jl index ffff293f..3ad56201 100644 --- a/test/rws_examples.jl +++ b/test/rws_examples.jl @@ -168,6 +168,14 @@ end @test length(rws) == 16 end +function test_kbs2_methods(R, methods, len) + rwses = [KnuthBendix.knuthbendix(R, implementation=m) for m in methods] + lengths = length.(rwses) + @test all(==(len), lengths) +end + + + @testset "KBS2 examples" begin R = RWS_Example_5_1() rws = KnuthBendix.knuthbendix(R, implementation=:naive_kbs2) @@ -175,30 +183,27 @@ end @test Set(KnuthBendix.rules(R)[1:5]) == Set(KnuthBendix.rules(rws)[1:5]) R = RWS_Example_5_2() - @test_logs (:warn,) rws = KnuthBendix.knuthbendix(R, maxrules=100, implementation=:naive_kbs2) - @test length(rws) > 50 # there could be less rules that 100 in the irreducible rws + @test_logs (:warn,) KnuthBendix.knuthbendix(R, maxrules=200, implementation=:naive_kbs2) R = RWS_Example_5_3() + test_kbs2_methods(R, (:naive_kbs2, :automata, :deletion), 6) rws = KnuthBendix.knuthbendix(R, implementation=:naive_kbs2) - @test length(rws) == 6 + a,b = Word.([i] for i in 1:2) ε = one(a) @test Set(KnuthBendix.rules(rws)) == Set([a^2=>ε, b^3=>ε, (b*a)^2=>a*b^2, a*b^2*a=>b*a*b, b^2*a*b^2=>a*b*a, (a*b)^2=>b^2*a]) R = RWS_Example_5_4() - rws = KnuthBendix.knuthbendix(R, implementation=:naive_kbs2) - @test length(rws) == 11 - + test_kbs2_methods(R, (:naive_kbs2, :automata, :deletion), 11) R = RWS_Example_5_5() - rws = KnuthBendix.knuthbendix(R, implementation=:naive_kbs2) - @test length(rws) == 18 + test_kbs2_methods(R, (:naive_kbs2, :automata, :deletion), 18) R = RWS_Example_6_4() - rws = KnuthBendix.knuthbendix(R, maxrules=100, implementation=:naive_kbs2) - @test length(rws) == 40 + test_kbs2_methods(R, (:naive_kbs2, :automata, :deletion), 18) + rws = KnuthBendix.knuthbendix(R, maxrules=100, implementation=:naive_kbs2) rwsd = KnuthBendix.knuthbendix(R, maxrules=100, implementation=:deletion) rwsa = KnuthBendix.knuthbendix(R, maxrules=100, implementation=:automata) @test Set(KnuthBendix.rules(rws)) == Set(KnuthBendix.rules(rwsd)) From 45fb14f742f7ddcc2727be25d4e9c6d238c38eb6 Mon Sep 17 00:00:00 2001 From: Marek Kaluba Date: Mon, 26 Apr 2021 19:12:06 +0200 Subject: [PATCH 03/10] split tests from examples --- test/runtests.jl | 2 + test/rws_examples.jl | 96 ------------------------------------------- test/test_examples.jl | 91 ++++++++++++++++++++++++++++++++++++++++ 3 files changed, 93 insertions(+), 96 deletions(-) create mode 100644 test/test_examples.jl diff --git a/test/runtests.jl b/test/runtests.jl index b20a37a8..a710efdb 100644 --- a/test/runtests.jl +++ b/test/runtests.jl @@ -12,5 +12,7 @@ include("abstract_words.jl") include("automata.jl") include("kbs1.jl") include("kbs.jl") + include("rws_examples.jl") + include("test_examples.jl") end diff --git a/test/rws_examples.jl b/test/rws_examples.jl index 3ad56201..e9c40884 100644 --- a/test/rws_examples.jl +++ b/test/rws_examples.jl @@ -125,99 +125,3 @@ function RWS_Closed_Orientable_Surface(n) return R end - - -@testset "KBS1 examples" begin - R = RWS_Example_5_1() - rws = KnuthBendix.knuthbendix(R, implementation=:naive_kbs1) - @test length(rws) == 8 - @test KnuthBendix.rules(R)[1:5] == KnuthBendix.rules(rws)[1:5] - - - R = RWS_Example_5_2() - @test_logs (:warn,) rws = KnuthBendix.knuthbendix(R, maxrules=100, implementation=:naive_kbs1) - @test length(rws) > 50 # there could be less rules that 100 in the irreducible rws - - R = RWS_Example_5_3() - rws = KnuthBendix.knuthbendix(R, implementation=:naive_kbs1) - @test length(rws) == 6 - a,b = Word.([i] for i in 1:2) - ε = one(a) - @test KnuthBendix.rules(rws) == [a^2=>ε, b^3=>ε, - (b*a)^2=>a*b^2, (a*b)^2=>b^2*a, a*b^2*a=>b*a*b, b^2*a*b^2=>a*b*a] - - - R = RWS_Example_5_4() - rws = KnuthBendix.knuthbendix(R, implementation=:naive_kbs1) - @test length(rws) == 11 - - R = RWS_Example_5_5() - rws = KnuthBendix.knuthbendix(R, implementation=:naive_kbs1) - @test length(rws) == 18 - - R = RWS_Example_6_4() - rws = KnuthBendix.knuthbendix(R, maxrules=100, implementation=:naive_kbs1) - @test_broken length(rws) == 81 - - R = RWS_Example_6_5() - rws = KnuthBendix.knuthbendix(R, maxrules=100, implementation=:naive_kbs1) - @test_broken length(rws) == 56 - - R = RWS_Closed_Orientable_Surface(3) - rws = KnuthBendix.knuthbendix(R, implementation=:naive_kbs1) - @test length(rws) == 16 -end - -function test_kbs2_methods(R, methods, len) - rwses = [KnuthBendix.knuthbendix(R, implementation=m) for m in methods] - lengths = length.(rwses) - @test all(==(len), lengths) -end - - - -@testset "KBS2 examples" begin - R = RWS_Example_5_1() - rws = KnuthBendix.knuthbendix(R, implementation=:naive_kbs2) - @test length(rws) == 8 - @test Set(KnuthBendix.rules(R)[1:5]) == Set(KnuthBendix.rules(rws)[1:5]) - - R = RWS_Example_5_2() - @test_logs (:warn,) KnuthBendix.knuthbendix(R, maxrules=200, implementation=:naive_kbs2) - - R = RWS_Example_5_3() - test_kbs2_methods(R, (:naive_kbs2, :automata, :deletion), 6) - rws = KnuthBendix.knuthbendix(R, implementation=:naive_kbs2) - - a,b = Word.([i] for i in 1:2) - ε = one(a) - @test Set(KnuthBendix.rules(rws)) == Set([a^2=>ε, b^3=>ε, - (b*a)^2=>a*b^2, a*b^2*a=>b*a*b, b^2*a*b^2=>a*b*a, (a*b)^2=>b^2*a]) - - R = RWS_Example_5_4() - test_kbs2_methods(R, (:naive_kbs2, :automata, :deletion), 11) - - R = RWS_Example_5_5() - test_kbs2_methods(R, (:naive_kbs2, :automata, :deletion), 18) - - R = RWS_Example_6_4() - test_kbs2_methods(R, (:naive_kbs2, :automata, :deletion), 18) - - rws = KnuthBendix.knuthbendix(R, maxrules=100, implementation=:naive_kbs2) - rwsd = KnuthBendix.knuthbendix(R, maxrules=100, implementation=:deletion) - rwsa = KnuthBendix.knuthbendix(R, maxrules=100, implementation=:automata) - @test Set(KnuthBendix.rules(rws)) == Set(KnuthBendix.rules(rwsd)) - @test Set(KnuthBendix.rules(rws)) == Set(KnuthBendix.rules(rwsa)) - - w = Word([3, 3, 2, 2, 3, 3, 3, 1, 1, 1, 3, 1, 2, 3, 2, 3, 2, 3, 3, 3]) - - @test KnuthBendix.rewrite_from_left(w, rws) == Word([1,3,1,2]) - - R = RWS_Example_6_5() - rws = KnuthBendix.knuthbendix(R, implementation=:naive_kbs2) - @test length(rws) == 40 - - R = RWS_Closed_Orientable_Surface(3) - rws = KnuthBendix.knuthbendix(R, implementation=:naive_kbs2) - @test length(rws) == 16 -end diff --git a/test/test_examples.jl b/test/test_examples.jl new file mode 100644 index 00000000..e51a12e8 --- /dev/null +++ b/test/test_examples.jl @@ -0,0 +1,91 @@ +@testset "KBS1 examples" begin + R = RWS_Example_5_1() + rws = KnuthBendix.knuthbendix(R, implementation=:naive_kbs1) + @test length(rws) == 8 + @test KnuthBendix.rules(R)[1:5] == KnuthBendix.rules(rws)[1:5] + + R = RWS_Example_5_2() + @test_logs (:warn,) rws = KnuthBendix.knuthbendix(R, maxrules=100, implementation=:naive_kbs1) + @test length(rws) > 50 # there could be less rules that 100 in the irreducible rws + + R = RWS_Example_5_3() + rws = KnuthBendix.knuthbendix(R, implementation=:naive_kbs1) + @test length(rws) == 6 + a,b = Word.([i] for i in 1:2) + ε = one(a) + @test KnuthBendix.rules(rws) == [a^2=>ε, b^3=>ε, + (b*a)^2=>a*b^2, (a*b)^2=>b^2*a, a*b^2*a=>b*a*b, b^2*a*b^2=>a*b*a] + + + R = RWS_Example_5_4() + rws = KnuthBendix.knuthbendix(R, implementation=:naive_kbs1) + @test length(rws) == 11 + + R = RWS_Example_5_5() + rws = KnuthBendix.knuthbendix(R, implementation=:naive_kbs1) + @test length(rws) == 18 + + R = RWS_Example_6_4() + rws = KnuthBendix.knuthbendix(R, maxrules=100, implementation=:naive_kbs1) + @test_broken length(rws) == 81 + + R = RWS_Example_6_5() + rws = KnuthBendix.knuthbendix(R, maxrules=100, implementation=:naive_kbs1) + @test_broken length(rws) == 56 + + R = RWS_Closed_Orientable_Surface(3) + rws = KnuthBendix.knuthbendix(R, implementation=:naive_kbs1) + @test length(rws) == 16 +end + +function test_kbs2_methods(R, methods, len) + rwses = [KnuthBendix.knuthbendix(R, implementation=m) for m in methods] + lengths = length.(rwses) + @test all(==(len), lengths) +end + +@testset "KBS2 examples" begin + R = RWS_Example_5_1() + rws = KnuthBendix.knuthbendix(R, implementation=:naive_kbs2) + @test length(rws) == 8 + @test Set(KnuthBendix.rules(R)[1:5]) == Set(KnuthBendix.rules(rws)[1:5]) + + R = RWS_Example_5_2() + @test_logs (:warn,) KnuthBendix.knuthbendix(R, maxrules=200, implementation=:naive_kbs2) + + R = RWS_Example_5_3() + test_kbs2_methods(R, (:naive_kbs2, :automata, :deletion), 6) + rws = KnuthBendix.knuthbendix(R, implementation=:naive_kbs2) + + a,b = Word.([i] for i in 1:2) + ε = one(a) + @test Set(KnuthBendix.rules(rws)) == Set([a^2=>ε, b^3=>ε, + (b*a)^2=>a*b^2, a*b^2*a=>b*a*b, b^2*a*b^2=>a*b*a, (a*b)^2=>b^2*a]) + + R = RWS_Example_5_4() + test_kbs2_methods(R, (:naive_kbs2, :automata, :deletion), 11) + + R = RWS_Example_5_5() + test_kbs2_methods(R, (:naive_kbs2, :automata, :deletion), 18) + + R = RWS_Example_6_4() + test_kbs2_methods(R, (:naive_kbs2, :automata, :deletion), 40) + + rws = KnuthBendix.knuthbendix(R, maxrules=100, implementation=:naive_kbs2) + rwsd = KnuthBendix.knuthbendix(R, maxrules=100, implementation=:deletion) + rwsa = KnuthBendix.knuthbendix(R, maxrules=100, implementation=:automata) + @test Set(KnuthBendix.rules(rws)) == Set(KnuthBendix.rules(rwsd)) + @test Set(KnuthBendix.rules(rws)) == Set(KnuthBendix.rules(rwsa)) + + w = Word([3, 3, 2, 2, 3, 3, 3, 1, 1, 1, 3, 1, 2, 3, 2, 3, 2, 3, 3, 3]) + + @test KnuthBendix.rewrite_from_left(w, rws) == Word([1,3,1,2]) + + R = RWS_Example_6_5() + rws = KnuthBendix.knuthbendix(R, implementation=:naive_kbs2) + @test length(rws) == 40 + + R = RWS_Closed_Orientable_Surface(3) + rws = KnuthBendix.knuthbendix(R, implementation=:naive_kbs2) + @test length(rws) == 16 +end From bb2f6e978340e9d30059ae04168bc8cd06027e96 Mon Sep 17 00:00:00 2001 From: Marek Kaluba Date: Mon, 26 Apr 2021 21:53:44 +0200 Subject: [PATCH 04/10] addd rules based on alphabet during creation this could be disabled by bare=true kwarg --- src/rewriting.jl | 40 +++++++++--- test/kbs1.jl | 154 +++++++++++++++++++++------------------------- test/rewriting.jl | 10 +-- 3 files changed, 107 insertions(+), 97 deletions(-) diff --git a/src/rewriting.jl b/src/rewriting.jl index f9ae006b..c2a8cbdc 100644 --- a/src/rewriting.jl +++ b/src/rewriting.jl @@ -66,8 +66,16 @@ struct RewritingSystem{W<:AbstractWord, O<:WordOrdering} <: AbstractRewritingSys act::BitArray{1} end -RewritingSystem(rwrules::Vector{Pair{W,W}}, order::O) where {W<:AbstractWord, O<:WordOrdering} = - RewritingSystem(rwrules, order, trues(length(rwrules))) +function RewritingSystem(rwrules::Vector{Pair{W,W}}, order::O; bare=false) where + {W<:AbstractWord, O<:WordOrdering} + rls = if !bare + abt_rules = rules(W, alphabet(order)) + [abt_rules; rwrules] + else + rwrules + end + return RewritingSystem(rls, order, trues(length(rls))) +end active(s::RewritingSystem) = s.act rules(s::RewritingSystem) = s.rwrules @@ -78,9 +86,9 @@ isactive(s::RewritingSystem, i::Integer) = active(s)[i] setactive!(s::RewritingSystem, i::Integer) = active(s)[i] = true setinactive!(s::RewritingSystem, i::Integer) = active(s)[i] = false -Base.push!(s::RewritingSystem{W,O}, r::Pair{W,W}) where {W<:AbstractWord, O<:WordOrdering} = +Base.push!(s::RewritingSystem{W,O}, r::Pair{W,W}) where {W, O} = (push!(rules(s), r); push!(active(s), true); s) -Base.pushfirst!(s::RewritingSystem{W,O}, r::Pair{W,W}) where {W<:AbstractWord, O<:WordOrdering} = +Base.pushfirst!(s::RewritingSystem{W,O}, r::Pair{W,W}) where {W, O} = (pushfirst!(rules(s), r); pushfirst!(active(s), true); s) Base.pop!(s::RewritingSystem) = @@ -101,13 +109,31 @@ Base.deleteat!(s::RewritingSystem, inds) = (deleteat!(rules(s), inds); deleteat!(active(s), inds); s) Base.empty!(s::RewritingSystem) = - (empty!(rules(s)); empty!(active(s)); s) -Base.empty(s::RewritingSystem{W, O}, ::Type{<:AbstractWord}=W,o::WordOrdering=ordering(s)) where {W,O} = - RewritingSystem(Pair{W,W}[], o) + (empty!(s.rwrules); empty!(s.act); s) + +function Base.empty( + s::RewritingSystem{W,O}, + ::Type{<:AbstractWord} = W, + o::WordOrdering = ordering(s), +) where {W,O} + RewritingSystem(Pair{W,W}[], o, bare=true) +end + Base.isempty(s::RewritingSystem) = isempty(rules(s)) Base.length(s::RewritingSystem) = length(rules(s)) +function rules(::Type{W}, A::Alphabet) where {W<:AbstractWord} + rls = Pair{W,W}[] + for l in letters(A) + if KnuthBendix.hasinverse(l, A) + L = inv(A, l) + push!(rls, W([A[l], A[L]]) => one(W)) + end + end + return rls +end + """ rewrite_from_left!(v::AbstractWord, w::AbstractWord, rws::RewritingSystem) Rewrites word `w` from left using active rules from a given RewritingSystem and diff --git a/test/kbs1.jl b/test/kbs1.jl index d8e4a75b..11e0b3c1 100644 --- a/test/kbs1.jl +++ b/test/kbs1.jl @@ -1,91 +1,75 @@ @testset "KBS1" begin - A = Alphabet(['a', 'e', 'b', 'p']) - KnuthBendix.set_inversion!(A, 'a', 'e') - KnuthBendix.set_inversion!(A, 'b', 'p') + Al = Alphabet(['a', 'A', 'b', 'B']) + KnuthBendix.set_inversion!(Al, 'a', 'A') + KnuthBendix.set_inversion!(Al, 'b', 'B') + lenlexord = LenLex(Al) - a = Word([1,2]) - b = Word([2,1]) - c = Word([3,4]) - d = Word([4,3]) + a, A, b, B = [Word([i]) for i in 1:4] ε = one(a) - ba = Word([3,1]) - ab = Word([1,3]) - - be = Word([3,2]) - eb = Word([2,3]) - - pa = Word([4,1]) - ap = Word([1,4]) - - pe = Word([4,2]) - ep = Word([2,4]) - - lenlexord = LenLex(A) - rs = RewritingSystem([a=>ε, b=>ε, c=>ε, d=>ε, ba=>ab], lenlexord) - rsc = RewritingSystem([a=>ε, b=>ε, c=>ε, d=>ε, ba=>ab, be=>eb, pa=>ap, pe=>ep], lenlexord) - @test KnuthBendix.getirreduciblesubsystem(rsc) == [a,b,c,d,ba,be,pa,pe] - - KnuthBendix.forceconfluence!(rs,5,1) - @test KnuthBendix.rules(rs) == [a=>ε, b=>ε, c=>ε, d=>ε, ba=>ab, Word([1,3,2])=>Word([3])] - - KnuthBendix.deriverule!(rs, Word([4,1,3]), Word([1])) - @test KnuthBendix.rules(rs) == [a=>ε, b=>ε, c=>ε, d=>ε, ba=>ab, Word([1,3,2])=>Word([3]), Word([4,1,3])=>Word([1])] - - - B = KnuthBendix.Alphabet(['a', 'b', 'p']) - KnuthBendix.set_inversion!(B, 'a', 'a') - KnuthBendix.set_inversion!(B, 'b', 'p') - - aa = Word([1,1]) - bp = Word([2,3]) - bbb = Word([2,2,2]) - ab3 = Word([1,2,1,2,1,2]) - ε = one(a) - - bb = Word([2,2]) - p = Word([3]) - - babab = Word([2,1,2,1,2]) - a = Word([1]) - - ababa = Word([1,2,1,2,1]) - p = Word([3]) - - pp = Word([3,3]) - b = Word([2]) - - pb = Word([3,2]) - # epsilon for the right side - - baba = Word([2,1,2,1]) - ap = Word([1,3]) - - abab = Word([1,2,1,2]) - pa = Word([3,1]) - - bab = Word([2,1,2]) - apa = Word([1,3,1]) - - pap = Word([3,1,3]) - aba = Word([1,2,1]) - - paba = Word([3,1,2,1]) - bap = Word([2,1,3]) - - abap = Word([1,2,1,3]) - pab = Word([3,1,2]) - - apab = Word([1,3,1,2]) - # bap for the right side - - bapa = Word([2,1,3,1]) - # pab for the right side - - lenlexordB = LenLex(B) - rsb = RewritingSystem([aa=>ε, bp=>ε, bbb=>ε, ab3=>ε, bb=>p, babab=>a, ababa=>p, pp=>b, pb=>ε, baba=>ap, abab=>pa, bab=>apa, pap=>aba, paba=>bap, abap=>pab, apab=>bap, bapa=>pab], lenlexordB) - - @test KnuthBendix.getirreduciblesubsystem(rsb) == [aa, bp, bb, pp, pb, bab, pap, paba, abap, apab, bapa] - + rs = RewritingSystem([b * a => a * b], lenlexord) + rsc = RewritingSystem( + [b * a => a * b, b * A => A * b, B * a => a * B, B * A => A * B], + lenlexord, + ) + @test KnuthBendix.getirreduciblesubsystem(rsc) == + [a * A, A * a, b * B, B * b, b * a, b * A, B * a, B * A] + + KnuthBendix.forceconfluence!(rs, 5, 1) + @test KnuthBendix.rules(rs) == + [a * A => ε, A * a => ε, b * B => ε, B * b => ε, b * a => a * b, a * b * A => b] + + KnuthBendix.deriverule!(rs, B * a * b, a) + @test KnuthBendix.rules(rs) == [ + a * A => ε, + A * a => ε, + b * B => ε, + B * b => ε, + b * a => a * b, + a * b * A => b, + B * a * b => a, + ] + + + Bl = KnuthBendix.Alphabet(['a', 'b', 'B']) + KnuthBendix.set_inversion!(Bl, 'a', 'a') + KnuthBendix.set_inversion!(Bl, 'b', 'B') + lenlexordB = LenLex(Bl) + + a, b, B = [Word([i]) for i in 1:3] + + rsb = RewritingSystem( + [ + b * b * b => ε, + (a * b)^3 => ε, + b * b => B, + b * a * b * a * b => a, + a * b * a * b * a => B, + B * B => b, + b * a * b * a => a * B, + a * b * a * b => B * a, + b * a * b => a * B * a, + B * a * B => a * b * a, + B * a * b * a => b * a * B, + a * b * a * B => B * a * b, + a * B * a * b => b * a * B, + b * a * B * a => B * a * b, + ], + lenlexordB, + ) + + @test KnuthBendix.getirreduciblesubsystem(rsb) == [ + a * a, + b * B, + B * b, + b * b, + B * B, + b * a * b, + B * a * B, + B * a * b * a, + a * b * a * B, + a * B * a * b, + b * a * B * a, + ] end diff --git a/test/rewriting.jl b/test/rewriting.jl index f5a2b5d9..f7b4ecb3 100644 --- a/test/rewriting.jl +++ b/test/rewriting.jl @@ -16,7 +16,7 @@ ba = Word([3,1]) ab = Word([1,3]) - s = RewritingSystem([a=>ε, b=>ε, c=>ε, d=>ε, ba=>ab], lenlexord) + s = RewritingSystem([a=>ε, b=>ε, c=>ε, d=>ε, ba=>ab], lenlexord, bare=true) z = empty(s) @test s isa KnuthBendix.AbstractRewritingSystem @@ -34,9 +34,9 @@ @test KnuthBendix.rules(z)[1] == (b=>ε) @test KnuthBendix.rules(z) == [b=>ε, c=>ε] - append!(z, RewritingSystem([ba=>ab], lenlexord)) + append!(z, RewritingSystem([ba=>ab], lenlexord; bare=true)) @test KnuthBendix.rules(z) == [b=>ε, c=>ε, ba=>ab] - prepend!(z, RewritingSystem([a=>ε], lenlexord)) + prepend!(z, RewritingSystem([a=>ε], lenlexord; bare=true)) @test KnuthBendix.rules(z) == [a=>ε, b=>ε, c=>ε, ba=>ab] @test KnuthBendix.rules(z)[1] == (a=>ε) @@ -54,10 +54,10 @@ @test KnuthBendix.rules(z) == [a=>ε, b=>ε, c=>ε, ba=>ab] insert!(z, 4, d=>ε) == s - @test KnuthBendix.rules(z) == KnuthBendix.rules(s) + @test issubset(KnuthBendix.rules(z), KnuthBendix.rules(s)) deleteat!(z, 5) @test KnuthBendix.rules(z) == [a=>ε, b=>ε, c=>ε, d=>ε] - deleteat!(z, 3:4) == RewritingSystem([a=>ε, b=>ε], lenlexord) + deleteat!(z, 3:4) == RewritingSystem([a=>ε, b=>ε], lenlexord, bare=true) @test KnuthBendix.rules(z) == [a=>ε, b=>ε] @test KnuthBendix.rewrite_from_left(a, s) == ε From 43f26bb36625ac93946bb8bb26e21ff0bef38963 Mon Sep 17 00:00:00 2001 From: Marek Kaluba Date: Mon, 26 Apr 2021 22:56:54 +0200 Subject: [PATCH 05/10] fix an out-of-bounds bug in rewrite with automaton --- src/automata.jl | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/src/automata.jl b/src/automata.jl index 6351af74..f22bb3d3 100644 --- a/src/automata.jl +++ b/src/automata.jl @@ -319,24 +319,27 @@ Rewrites word `w` from left using index automaton `a` and appends the result to `v`. For standard rewriting `v` should be empty. """ function rewrite_from_left!(v::AbstractWord, w::AbstractWord, a::Automaton) - past_states = a._past_states - resize!(past_states, length(w) + 1) - state = initialstate(a) - past_states[1] = state + tape = a._past_states + resize!(tape, length(w) + 1) + tape[1] = initialstate(a) initial_length = length(v) - + @debug "Rewriting $w with automaton" while !isone(w) x = popfirst!(w) k = length(v) - initial_length + 1 - state = outedges(past_states[k])[x] + @debug "" v x w + s = tape[k] + state = outedges(s)[x] if isterminal(state) lhs, rhs = name(state), rightrule(state) + @debug "applying rewriting rule $lhs → $rhs" w = prepend!(w, rhs) resize!(v, length(v) - length(lhs) + 1) else - @inbounds past_states[k+1] = state + length(tape) <= k ? push!(tape, state) : tape[k+1] = state push!(v, x) + @debug "state is not terminal, pushed $x, v=$v" end end return v From 812e986484439b4a73404589467a46030feb14e8 Mon Sep 17 00:00:00 2001 From: Marek Kaluba Date: Mon, 26 Apr 2021 22:57:22 +0200 Subject: [PATCH 06/10] nicer io for states --- src/automata.jl | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/src/automata.jl b/src/automata.jl index f22bb3d3..3cb7215f 100644 --- a/src/automata.jl +++ b/src/automata.jl @@ -70,6 +70,16 @@ function declarerightrule!(s::State, w::AbstractWord) end function Base.show(io::IO, s::State) + if isfailstate(s) + print(io, "Fail State") + elseif isterminal(s) + print(io, "TState($(name(s)) → $(rightrule(s)))") + else + print(io, "NTState($(length(inedges(s))), $(length(outedges(s))))") + end +end + +function Base.show(io::IO, ::MIME"text/plain", s::State) if isfailstate(s) print(io, "Fail state") elseif isterminal(s) @@ -301,7 +311,7 @@ function makeindexautomaton!(a::Automaton, rws::RewritingSystem) end """ - makeindexautomaton(rws::RewritingSystem, abt::Alphabet) + makeindexautomaton(rws::RewritingSystem) Creates index automaton corresponding to a given rewriting system. """ makeindexautomaton(rws::RewritingSystem) = From a0aadfe27b1f8a8f5338014c4df63e1b31f2cacc Mon Sep 17 00:00:00 2001 From: Marek Kaluba Date: Tue, 27 Apr 2021 00:14:19 +0200 Subject: [PATCH 07/10] add parsing routines for kbmag input --- Project.toml | 6 +- src/KnuthBendix.jl | 2 + src/parsing.jl | 164 ++++++++++++++++++++++++++++++++++++++++++ test/kbmag_parsing.jl | 46 ++++++++++++ test/runtests.jl | 2 + 5 files changed, 219 insertions(+), 1 deletion(-) create mode 100644 src/parsing.jl create mode 100644 test/kbmag_parsing.jl diff --git a/Project.toml b/Project.toml index 1a34f6b5..211f5bbe 100644 --- a/Project.toml +++ b/Project.toml @@ -1,10 +1,14 @@ name = "KnuthBendix" uuid = "c2604015-7b3d-4a30-8a26-9074551ec60a" authors = ["Marek Kaluba ", "Mikołaj Pabiszczak "] -version = "0.1.0" +version = "0.1.1" + +[deps] +MacroTools = "1914dd2f-81c6-5fcd-8719-6d5c9610ff09" [compat] julia = "1" +MacroTools = "0.5" [extras] Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40" diff --git a/src/KnuthBendix.jl b/src/KnuthBendix.jl index 21a329b9..7265837a 100644 --- a/src/KnuthBendix.jl +++ b/src/KnuthBendix.jl @@ -13,4 +13,6 @@ include("helper_structures.jl") include("derive_rule.jl") include("force_confluence.jl") include("kbs.jl") + +include("parsing.jl") end diff --git a/src/parsing.jl b/src/parsing.jl new file mode 100644 index 00000000..44f6cec9 --- /dev/null +++ b/src/parsing.jl @@ -0,0 +1,164 @@ +using MacroTools + +function replace_powering(x) + if @capture(x, ^(a_, n_)) + args = fill(a, n) + return :(*($(args...))) + else + return x + end +end + +function mult_args!(args, old_expr) + old_expr isa Symbol && (push!(args, old_expr); return args) + if old_expr.head === :call && old_expr.args[1] === :* + for e in @view(old_expr.args[2:end]) + mult_args!(args, e) + end + end + return args +end + + +### parsing Kbmag input files + +struct RwsGAP + generators::Vector{Symbol} + inverses::Vector{Int} + equations::Vector{Pair{Vector{Int}, Vector{Int}}} + _str::String +end + +_entry_regex(key, value) = Regex("\\s*$key\\s*:=\\s*$value,") + +function _validate_rws(input::AbstractString) + rec = r"rec\((?.*)\);"s + m = match(rec, input) + isnothing(m) && throw("file doesn't contain a record: $rec not matched") + str = m[:rec] + + let str = str + m = match(_entry_regex("isRWS", "true"), str) + isnothing(m) && throw("file does not seem to contain an rws: $isrws not matched") + end + str +end + +function _parse_gens(str::AbstractString) + r = _entry_regex("generatorOrder", "\\[(?.*?)\\]") + m = match(r, str) + isnothing(m) && error("file does not seem to contain generators: $r not matched") + return strip.(split(m[:gens], ",")) +end + +function _parse_inverses(str::AbstractString, gens::AbstractArray{<:AbstractString}) + r = _entry_regex("inverses", "\\[(?.*?)\\]") + m = match(r, str) + isnothing(m) && error("file does not seem to contain inverses: $r not matched") + invs = strip.(split(m[:gens], ",")) + + inv_ptrs = zeros(Int, length(gens)) + if !isempty(inv_ptrs) + for (i,g) in enumerate(invs) + k = findfirst(==(g), gens) + isnothing(k) && continue + inv_ptrs[i] = k + end + end + return inv_ptrs +end + +function _parse_equations(str::AbstractString, gens::AbstractArray{<:AbstractString}) + m = let str = str + r = r"\s*equations\s*:=\s*(?\[.*(?!:=)\])"s + m = match(r, str) + isnothing(m) && throw("file does not seem to contain equations: $r not matched") + m + end + + gens_or = join(gens, "|") + space = "[\\n\\s]*" + word_reg = "(($gens_or)(\\*($gens_or|($space($gens_or))))*)" + eq_r = Regex("\\[$space(?$word_reg)$space,$space(?IdWord|$word_reg)$space\\]") + + gens_dict = Dict(g=>i for (i,g) in pairs(gens)) + + eqns_ptrs = Pair{Vector{Int}, Vector{Int}}[] + + for m in eachmatch(eq_r, m[:equations]) + lhs, rhs = m[:lhs], m[:rhs] + lhs_ptrs = [gens_dict[strip(g)] for g in split(lhs, "*")] + rhs_ptrs = if rhs == "IdWord" + Int[] + else + [gens_dict[g] for g in split(rhs, "*")] + end + push!(eqns_ptrs, lhs_ptrs => rhs_ptrs) + end + length(eqns_ptrs) == 0 && throw("equations := [...] don't seem to contain properly formatted equations: no $eq_r was matched") + + return eqns_ptrs +end + + +function _parse_equations(str::AbstractString, gens::AbstractArray{<:Symbol}) + + m = let str = str + r = r"\s*equations\s*:=\s*(?\[.*(?!:=)\])"s + m = match(r, str) + isnothing(m) && throw("file does not seem to contain equations: $r not matched") + m + end + + eqns_parsed = Meta.parse(m[:equations]) + @assert eqns_parsed.head === :vect + VI = Vector{Int} + eqns_ptrs = Vector{Pair{VI, VI}}(undef, length(eqns_parsed.args)) + gens_dict = Dict(s=>i for (i,s) in pairs(gens)) + + for (idx, eqn) in enumerate(eqns_parsed.args) + @assert eqn.head === :vect + @assert length(eqn.args) == 2 + lhs_ast, rhs_ast = eqn.args + + tmp = Symbol[] + lhs_ptrs = let expr = lhs_ast, tmp=tmp + ex = MacroTools.postwalk(replace_powering, expr) + [gens_dict[g] for g in mult_args!(tmp, ex)] + end + resize!(tmp, 0) + rhs_ptrs = let expr = rhs_ast, tmp=tmp + ex = MacroTools.postwalk(replace_powering, expr) + args = mult_args!(tmp, ex) + args == [:IdWord] ? Int[] : [gens_dict[g] for g in args] + end + + eqns_ptrs[idx] = lhs_ptrs=>rhs_ptrs + end + return eqns_ptrs +end + +function parse_kbmag(input::AbstractString; method=:ast) + + @assert method in (:ast, :string) + + rws_str = _validate_rws(input) + + gens = _parse_gens(rws_str) + inverses = _parse_inverses(rws_str, gens) + equations = if method === :ast + _parse_equations(rws_str, Symbol.(gens)) + elseif method === :string + _parse_equations(rws_str, gens) + end + + return RwsGAP(Symbol.(gens), inverses, equations, rws_str) +end + +RewritingSystem(rwsgap::RwsGAP) = RewritingSystem{Word{UInt16}}(rwsgap) + +function RewritingSystem{W}(rwsgap::RwsGAP) where W + A = Alphabet(rwsgap.generators, rwsgap.inverses) + rwrules = [W(l)=>W(r) for (l,r) in rwsgap.equations] + return RewritingSystem(rwrules, LenLex(A)) +end diff --git a/test/kbmag_parsing.jl b/test/kbmag_parsing.jl new file mode 100644 index 00000000..53c32e95 --- /dev/null +++ b/test/kbmag_parsing.jl @@ -0,0 +1,46 @@ +using MacroTools + +@testset "kbmag parsing" begin + w = MacroTools.postwalk(KnuthBendix.replace_powering, :((a*c*b^2)^3)) + @test w == :((a*c*(b*b))*(a*c*(b*b))*(a*c*(b*b))) + @test KnuthBendix.mult_args!(Symbol[], w) == [:a, :c, :b, :b, :a, :c, :b, :b, :a, :c, :b, :b] + + kb_data = joinpath(@__DIR__, "..", "kb_data") + + let file_content = String(read(joinpath(kb_data, "a4"))) + # file_content = join(split(file_content), "") + rws = KnuthBendix.parse_kbmag(file_content, method=:string) + + @test rws.generators == [Symbol("g.10"), Symbol("g.20"), Symbol("g.30")] + @test rws.inverses == [1, 3, 2] + @test rws.equations == [[2,2]=>[3], [3,1,3]=>[1,2,1]] + end + + let file_content = String(read(joinpath(kb_data, "3a6"))) + # file_content = join(split(file_content), "") + rws = KnuthBendix.parse_kbmag(file_content, method=:ast) + @test rws.generators == [:a, :b, :A, :B] + @test rws.inverses == [3, 4, 1, 2] + @test rws.equations == [ + [1,1,1]=>Int[], + [2,2,2]=>Int[], + [1,2,1,2,1,2,1,2]=>Int[], + [1,4,1,4,1,4,1,4,1,4]=>Int[] + ] + end + + for f in readdir(kb_data) + rwsgap = let file_content = String(read(joinpath(kb_data, f))) + # file_content = join(split(file_content), "") + method = (f=="a4" ? :string : :ast) + rws = KnuthBendix.parse_kbmag(file_content, method=method) + @test rws isa KnuthBendix.RwsGAP + @test !isempty(rws.generators) + @test length(rws.generators) == length(rws.inverses) + @test all(!isempty(lhs) for (lhs, rhs) in rws.equations) + rws + end + @test RewritingSystem(rwsgap) isa RewritingSystem + + end +end diff --git a/test/runtests.jl b/test/runtests.jl index a710efdb..f873ad70 100644 --- a/test/runtests.jl +++ b/test/runtests.jl @@ -13,6 +13,8 @@ include("abstract_words.jl") include("kbs1.jl") include("kbs.jl") + include("kbmag_parsing.jl") + include("rws_examples.jl") include("test_examples.jl") end From e6fe44f65a193bc83e5320984ba0ab72c83e50c6 Mon Sep 17 00:00:00 2001 From: Marek Kaluba Date: Tue, 27 Apr 2021 00:16:40 +0200 Subject: [PATCH 08/10] modify rws_examples and fix test_examples uncovered issue #48 is visible as @test_broken --- test/rws_examples.jl | 18 ++++++++---------- test/test_examples.jl | 7 +++++-- 2 files changed, 13 insertions(+), 12 deletions(-) diff --git a/test/rws_examples.jl b/test/rws_examples.jl index e9c40884..84db8467 100644 --- a/test/rws_examples.jl +++ b/test/rws_examples.jl @@ -6,7 +6,7 @@ function RWS_Example_5_1() a,A,b,B = Word.([i] for i in 1:4) ε = one(a) - R = RewritingSystem([a*A=>ε, A*a=>ε, b*B=>ε, B*b=>ε, b*a=>a*b], LenLex(Al)) + R = RewritingSystem([b*a=>a*b], LenLex(Al)) return R end @@ -21,7 +21,7 @@ function RWS_Example_5_2() a,b,B,A = Word.([i] for i in 1:4) ε = one(a) - R = RewritingSystem([a*A=>ε, A*a=>ε, b*B=>ε, B*b=>ε, b*a=>a*b], LenLex(Al)) + R = RewritingSystem([b*a=>a*b], LenLex(Al)) return R end @@ -46,7 +46,7 @@ function RWS_Example_5_4() a,b,B = Word.([i] for i in 1:3) ε = one(a) - R = RewritingSystem([a^2=>ε, b*B=>ε, b^3=>ε, (a*b)^3=>ε], LenLex(Al)) + R = RewritingSystem([a^2=>ε, b^3=>ε, (a*b)^3=>ε], LenLex(Al)) return R end @@ -60,8 +60,7 @@ function RWS_Example_5_5() c, C, b, B, a, A = Word.([i] for i in 1:6) ε = one(a) - eqns = [a*A=>ε, A*a=>ε, b*B=>ε, B*b=>ε, c*C=>ε, C*c=>ε, - 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 @@ -74,9 +73,10 @@ function RWS_Example_237_abaB(n) a, b, B = Word.([i] for i in 1:3) ε = one(a) - eqns = [a^2=>ε, b*B=>ε, b^3=>ε, (a*b)^7=>ε, (a*b*a*B)^n=>ε] + # 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)) + R = RewritingSystem(eqns, LenLex(Al), bare=true) return R end @@ -88,7 +88,7 @@ function RWS_Example_6_5() a, b, B = Word.([i] for i in 1:3) ε = one(a) - eqns = [a*a=>ε, b*B=>ε, b^2=>B, (B*a)^3*B=>(a*b)^3*a, + eqns = [a*a=>ε, 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)) @@ -116,8 +116,6 @@ function RWS_Closed_Orientable_Surface(n) for i in reverse(1:n) x = 4 * i - append!(rules, [Word([x-1, x]) => ε, Word([x, x-1]) => ε]) - append!(rules, [Word([x-3, x-2]) => ε, Word([x-2, x-3]) => ε]) append!(word, [x, x-2, x-1, x-3]) end push!(rules, Word(word) => ε) diff --git a/test/test_examples.jl b/test/test_examples.jl index e51a12e8..eae0b86d 100644 --- a/test/test_examples.jl +++ b/test/test_examples.jl @@ -69,13 +69,16 @@ end test_kbs2_methods(R, (:naive_kbs2, :automata, :deletion), 18) R = RWS_Example_6_4() - test_kbs2_methods(R, (:naive_kbs2, :automata, :deletion), 40) + # uncomment when the @test_broken below is fixed + # test_kbs2_methods(R, (:naive_kbs2, :automata, :deletion), 40) rws = KnuthBendix.knuthbendix(R, maxrules=100, implementation=:naive_kbs2) rwsd = KnuthBendix.knuthbendix(R, maxrules=100, implementation=:deletion) rwsa = KnuthBendix.knuthbendix(R, maxrules=100, implementation=:automata) @test Set(KnuthBendix.rules(rws)) == Set(KnuthBendix.rules(rwsd)) - @test Set(KnuthBendix.rules(rws)) == Set(KnuthBendix.rules(rwsa)) + # when fixed, uncomment the test above + @test_broken Set(KnuthBendix.rules(rws)) == Set(KnuthBendix.rules(rwsa)) + w = Word([3, 3, 2, 2, 3, 3, 3, 1, 1, 1, 3, 1, 2, 3, 2, 3, 2, 3, 3, 3]) From ee4fc2cbcea47988d8f3f323aa2a886a6d6b4c55 Mon Sep 17 00:00:00 2001 From: Marek Kaluba Date: Tue, 27 Apr 2021 00:45:09 +0200 Subject: [PATCH 09/10] add kb_data taken from kbmag --- kb_data/237 | 11 +++++++++++ kb_data/3a6 | 12 ++++++++++++ kb_data/a4 | 8 ++++++++ kb_data/a4monoid | 11 +++++++++++ kb_data/ab1 | 8 ++++++++ kb_data/ab2 | 8 ++++++++ kb_data/c2 | 8 ++++++++ kb_data/cosets | 13 +++++++++++++ kb_data/d22 | 16 ++++++++++++++++ kb_data/degen1 | 8 ++++++++ kb_data/degen2 | 8 ++++++++ kb_data/degen3 | 8 ++++++++ kb_data/degen4a | 8 ++++++++ kb_data/degen4b | 14 ++++++++++++++ kb_data/degen4c | 23 +++++++++++++++++++++++ kb_data/e8 | 16 ++++++++++++++++ kb_data/f2 | 8 ++++++++ kb_data/f25 | 9 +++++++++ kb_data/f25monoid | 10 ++++++++++ kb_data/f27 | 10 ++++++++++ kb_data/f27_2gen | 13 +++++++++++++ kb_data/f27monoid | 12 ++++++++++++ kb_data/freenilpc3 | 15 +++++++++++++++ kb_data/funny3 | 18 ++++++++++++++++++ kb_data/heinnilp | 24 ++++++++++++++++++++++++ kb_data/l32ext | 13 +++++++++++++ kb_data/m11 | 13 +++++++++++++ kb_data/nilp2 | 10 ++++++++++ kb_data/nonhopf | 10 ++++++++++ kb_data/s16 | 30 ++++++++++++++++++++++++++++++ kb_data/s3 | 10 ++++++++++ kb_data/s4 | 10 ++++++++++ kb_data/s9 | 16 ++++++++++++++++ kb_data/torus | 8 ++++++++ kb_data/verifynilp | 25 +++++++++++++++++++++++++ 35 files changed, 444 insertions(+) create mode 100644 kb_data/237 create mode 100644 kb_data/3a6 create mode 100644 kb_data/a4 create mode 100644 kb_data/a4monoid create mode 100644 kb_data/ab1 create mode 100644 kb_data/ab2 create mode 100644 kb_data/c2 create mode 100644 kb_data/cosets create mode 100644 kb_data/d22 create mode 100644 kb_data/degen1 create mode 100644 kb_data/degen2 create mode 100644 kb_data/degen3 create mode 100644 kb_data/degen4a create mode 100644 kb_data/degen4b create mode 100644 kb_data/degen4c create mode 100644 kb_data/e8 create mode 100644 kb_data/f2 create mode 100644 kb_data/f25 create mode 100644 kb_data/f25monoid create mode 100644 kb_data/f27 create mode 100644 kb_data/f27_2gen create mode 100644 kb_data/f27monoid create mode 100644 kb_data/freenilpc3 create mode 100644 kb_data/funny3 create mode 100644 kb_data/heinnilp create mode 100644 kb_data/l32ext create mode 100644 kb_data/m11 create mode 100644 kb_data/nilp2 create mode 100644 kb_data/nonhopf create mode 100644 kb_data/s16 create mode 100644 kb_data/s3 create mode 100644 kb_data/s4 create mode 100644 kb_data/s9 create mode 100644 kb_data/torus create mode 100644 kb_data/verifynilp diff --git a/kb_data/237 b/kb_data/237 new file mode 100644 index 00000000..9b8a2b28 --- /dev/null +++ b/kb_data/237 @@ -0,0 +1,11 @@ +#Von Dyck (2,3,7) group - infinite hyperbolic - small tidyint works better +_RWS := rec( + isRWS := true, + ordering := "shortlex", + tidyint := 20, + generatorOrder := [a,A,b,B,c], + inverses := [A,a,B,b,c], + equations := [ + [a*a*a*a,A*A*A], [b*b,B], [B*A,c] +] +); diff --git a/kb_data/3a6 b/kb_data/3a6 new file mode 100644 index 00000000..06f39514 --- /dev/null +++ b/kb_data/3a6 @@ -0,0 +1,12 @@ +#3-fold cover of A_6 +_RWS := rec( + isRWS := true, + ordering := "shortlex", + generatorOrder := [a,b,A,B], + inverses := [A,B,a,b], + equations := [[a^3,IdWord], + [b^3,IdWord], + [(a*b)^4,IdWord], + [(a*B)^5,IdWord] + ] +); diff --git a/kb_data/a4 b/kb_data/a4 new file mode 100644 index 00000000..72c2a835 --- /dev/null +++ b/kb_data/a4 @@ -0,0 +1,8 @@ +#Group is A_4. Generators named by the enumerated prefix method. +_RWS := rec( + isRWS := true, + ordering := "shortlex", + generatorOrder := [g.10,g.20,g.30], + inverses := [g.10,g.30,g.20], + equations := [ [g.20*g.20,g.30], [g.30*g.10*g.30,g.10*g.20*g.10] ] +); diff --git a/kb_data/a4monoid b/kb_data/a4monoid new file mode 100644 index 00000000..e531c785 --- /dev/null +++ b/kb_data/a4monoid @@ -0,0 +1,11 @@ +#Presentation of group A_4 regarded as monoid presentation +# - gives infinite monoid. +_RWS := rec( + isRWS := true, + ordering := "shortlex", + generatorOrder := [a,b,B], + inverses := [], + equations := [ + [b*b,B], [B*a*B,a*b*a] + ] +); diff --git a/kb_data/ab1 b/kb_data/ab1 new file mode 100644 index 00000000..429efb4a --- /dev/null +++ b/kb_data/ab1 @@ -0,0 +1,8 @@ +#infinite cyclic group +_RWS := rec( + isRWS := true, + ordering := "shortlex", + generatorOrder := [a,A], + inverses := [A,a], + equations := [] +); diff --git a/kb_data/ab2 b/kb_data/ab2 new file mode 100644 index 00000000..2c9d2d7f --- /dev/null +++ b/kb_data/ab2 @@ -0,0 +1,8 @@ +#2-generator free abelian group (with this ordering KB terminates - but no all) +_RWS := rec( + isRWS := true, + ordering := "shortlex", + generatorOrder := [a,A,b,B], + inverses := [A,a,B,b], + equations := [[B*a*b,a]] +); diff --git a/kb_data/c2 b/kb_data/c2 new file mode 100644 index 00000000..c526f64b --- /dev/null +++ b/kb_data/c2 @@ -0,0 +1,8 @@ +#Cyclic group of order 2. +_RWS := rec( + isRWS := true, + ordering := "shortlex", + generatorOrder := [a], + inverses := [a], + equations := [[a^2,IdWord]] +); diff --git a/kb_data/cosets b/kb_data/cosets new file mode 100644 index 00000000..45a7eca9 --- /dev/null +++ b/kb_data/cosets @@ -0,0 +1,13 @@ +#The group is S_4, and the subgroup H of order 4. +#There are 30 reduced words - 24 for the group elements, and 6 for the +#6 cosets Hg. +_RWS := rec( + isRWS := true, + ordering := "shortlex", + generatorOrder := [H,a,A,b,B], + inverses := [,A,a,B,b], + equations := [ + [a^3,IdWord], [b^4,IdWord], [a*b*a*b,IdWord], [H*b,H], + [H*H,H], [a*H,H], [b*H,H] + ] +); diff --git a/kb_data/d22 b/kb_data/d22 new file mode 100644 index 00000000..ecfc47f7 --- /dev/null +++ b/kb_data/d22 @@ -0,0 +1,16 @@ +#This group is actually D_22 (although it wasn't meant to be). +#All generators are unexpectedly involutory. +_RWS := rec( + isRWS := true, + ordering := "shortlex", + generatorOrder := [a,A,b,B,c,C,d,D,e,E,f,F], + inverses := [A,a,B,b,C,c,D,d,E,e,F,f], + equations := [ + [a*C*A*d,IdWord], + [b*f*B*E,IdWord], + [c*e*C*D,IdWord], + [d*F*D*a,IdWord], + [e*b*E*A,IdWord], + [f*C*F*B,IdWord] + ] +); diff --git a/kb_data/degen1 b/kb_data/degen1 new file mode 100644 index 00000000..034a7153 --- /dev/null +++ b/kb_data/degen1 @@ -0,0 +1,8 @@ +#No generators - no anything! +_RWS := rec( + isRWS := true, + ordering := "shortlex", + generatorOrder := [], + inverses := [], + equations := [] +); diff --git a/kb_data/degen2 b/kb_data/degen2 new file mode 100644 index 00000000..1e526859 --- /dev/null +++ b/kb_data/degen2 @@ -0,0 +1,8 @@ +#A generator, but trivial. +_RWS := rec( + isRWS := true, + ordering := "shortlex", + generatorOrder := [a,A], + inverses := [A,a], + equations := [[a,IdWord]] +); diff --git a/kb_data/degen3 b/kb_data/degen3 new file mode 100644 index 00000000..58c960eb --- /dev/null +++ b/kb_data/degen3 @@ -0,0 +1,8 @@ +#fairly clearly the trivial group +_RWS := rec( + isRWS := true, + ordering := "shortlex", + generatorOrder := [a,A,b,B], + inverses := [A,a,B,b], + equations := [[a*b,IdWord],[a*b*b,IdWord]] +); diff --git a/kb_data/degen4a b/kb_data/degen4a new file mode 100644 index 00000000..5faab86c --- /dev/null +++ b/kb_data/degen4a @@ -0,0 +1,8 @@ +#trivial group - BHN presentation +_RWS := rec( + isRWS := true, + ordering := "shortlex", + generatorOrder := [a,A,b,B,c,C], + inverses := [A,a,B,b,C,c], + equations := [[A*b*a,b^2], [B*c*b,c^2], [C*a*c,a^2] ] +); diff --git a/kb_data/degen4b b/kb_data/degen4b new file mode 100644 index 00000000..a3128d6c --- /dev/null +++ b/kb_data/degen4b @@ -0,0 +1,14 @@ +#Second of BHN's series of increasingly complicated presentations of 1. +#Works quickest with large value of tidyint +_RWS := rec( + isRWS := true, + ordering := "shortlex", + tidyint := 3000, + generatorOrder := [x,X,y,Y,z,Z], + inverses := [X,x,Y,y,Z,z], + equations := [ + [y*y*X*Y*x*Y*z*y*Z*Z*X*y*x*Y*Y*z*z*Y*Z*y*z*z*Y*Z*y,IdWord], + [z*z*Y*Z*y*Z*x*z*X*X*Y*z*y*Z*Z*x*x*Z*X*z*x*x*Z*X*z,IdWord], + [x*x*Z*X*z*X*y*x*Y*Y*Z*x*z*X*X*y*y*X*Y*x*y*y*X*Y*x,IdWord] + ] +); diff --git a/kb_data/degen4c b/kb_data/degen4c new file mode 100644 index 00000000..3322332a --- /dev/null +++ b/kb_data/degen4c @@ -0,0 +1,23 @@ +#Third of BHN's series of increasingly complicated presentations of 1. +#This is too difficult for KB!! +_RWS := rec( + isRWS := true, + ordering := "shortlex", + tidyint := 3000, + generatorOrder := [r,R,s,S,t,T], + inverses := [R,r,S,s,T,t], + equations := [ + [S*t*s*T*T*S*t*s*T*T*s*s*R*S*r*t*t*S*T*s*R*s*r*S*S*t*t*S*T*s*T*r*t*R*R*S*t*s* + T*T*r*r*T*R*t*r*r*T*R*t*s*s*R*S*r*S*t*s*T*T*R*s*r*S*S*t*t*S*T*s*t*t*S*T*s*T* + r*t*R*R*T*r*t*R*R*t*t*S*T*s*r*r*T*R*t*S*t*s*T*T*T*r*t*R*R*T*r*t*R*R*t*t*S*T* + s*r*r*T*R*t*S*t*s*T*T, IdWord], + [T*r*t*R*R*T*r*t*R*R*t*t*S*T*s*r*r*T*R*t*S*t*s*T*T*r*r*T*R*t*R*s*r*S*S*T*r*t* + R*R*s*s*R*S*r*s*s*R*S*r*t*t*S*T*s*T*r*t*R*R*S*t*s*T*T*r*r*T*R*t*r*r*T*R*t*R* + s*r*S*S*R*s*r*S*S*r*r*T*R*t*s*s*R*S*r*T*r*t*R*R*R*s*r*S*S*R*s*r*S*S*r*r*T*R* + t*s*s*R*S*r*T*r*t*R*R, IdWord], + [R*s*r*S*S*R*s*r*S*S*r*r*T*R*t*s*s*R*S*r*T*r*t*R*R*s*s*R*S*r*S*t*s*T*T*R*s*r* + S*S*t*t*S*T*s*t*t*S*T*s*r*r*T*R*t*R*s*r*S*S*T*r*t*R*R*s*s*R*S*r*s*s*R*S*r*S* + t*s*T*T*S*t*s*T*T*s*s*R*S*r*t*t*S*T*s*R*s*r*S*S*S*t*s*T*T*S*t*s*T*T*s*s*R*S* + r*t*t*S*T*s*R*s*r*S*S, IdWord] + ] +); diff --git a/kb_data/e8 b/kb_data/e8 new file mode 100644 index 00000000..ce973bb3 --- /dev/null +++ b/kb_data/e8 @@ -0,0 +1,16 @@ +#Weyl group E8 (all gens involutory). +_RWS := rec( + isRWS := true, + ordering := "shortlex", + generatorOrder := [a,b,c,d,e,f,g,h], + inverses := [a,b,c,d,e,f,g,h], + equations := [ + [b*a*b,a*b*a],[c*a,a*c],[d*a,a*d],[e*a,a*e],[f*a,a*f],[g*a,a*g],[h*a,a*h], + [c*b*c,b*c*b],[d*b,b*d],[e*b,b*e],[f*b,b*f],[g*b,b*g],[h*b,b*h], + [d*c*d,c*d*c],[e*c*e,c*e*c],[f*c,c*f],[g*c,c*g],[h*c,c*h], + [e*d,d*e],[f*d,d*f],[g*d,d*g],[h*d,d*h], + [f*e*f,e*f*e],[g*e,e*g],[h*e,e*h], + [g*f*g,f*g*f],[h*f,f*h], + [h*g*h,g*h*g] + ] +); diff --git a/kb_data/f2 b/kb_data/f2 new file mode 100644 index 00000000..2f6f4a89 --- /dev/null +++ b/kb_data/f2 @@ -0,0 +1,8 @@ +#Free group on 2 generators +_RWS := rec( + isRWS := true, + ordering := "shortlex", + generatorOrder := [a,A,b,B], + inverses := [A,a,B,b], + equations := [] +); diff --git a/kb_data/f25 b/kb_data/f25 new file mode 100644 index 00000000..6db87477 --- /dev/null +++ b/kb_data/f25 @@ -0,0 +1,9 @@ +#Fibonacci group F(2,5) +_RWS := rec( + isRWS := true, + ordering := "shortlex", + generatorOrder := [a,A,b,B,c,C,d,D,e,E], + inverses := [A,a,B,b,C,c,D,d,E,e], + equations := [[a*b,c], [b*c,d], [c*d,e], [d*e,a], [e*a,b] + ] +); diff --git a/kb_data/f25monoid b/kb_data/f25monoid new file mode 100644 index 00000000..26ccb43e --- /dev/null +++ b/kb_data/f25monoid @@ -0,0 +1,10 @@ +#Fibonacci group F(2,5) - monoid presentation - has order 12 +# (group elements + empty word) +_RWS := rec( + isRWS := true, + ordering := "shortlex", + generatorOrder := [a,b,c,d,e], + inverses := [], + equations := [[a*b,c], [b*c,d], [c*d,e], [d*e,a], [e*a,b] + ] +); diff --git a/kb_data/f27 b/kb_data/f27 new file mode 100644 index 00000000..11d8d4bf --- /dev/null +++ b/kb_data/f27 @@ -0,0 +1,10 @@ +#Fibonacci group F(2,7) - order 29 - works better with largish tidyint +_RWS := rec( + isRWS := true, + ordering := "shortlex", + tidyint := 1000, + generatorOrder := [a,A,b,B,c,C,d,D,e,E,f,F,g,G], + inverses := [A,a,B,b,C,c,D,d,E,e,F,f,G,g], + equations := [[a*b,c], [b*c,d], [c*d,e], [d*e,f], [e*f,g], [f*g,a], [g*a,b] + ] +); diff --git a/kb_data/f27_2gen b/kb_data/f27_2gen new file mode 100644 index 00000000..c639f0aa --- /dev/null +++ b/kb_data/f27_2gen @@ -0,0 +1,13 @@ +#Two generator presentation of Fibonacci group F(2,7) - order 29 +#Large value of tidyint works better. +_RWS := rec( + isRWS := true, + ordering := "shortlex", + tidyint := 3000, + generatorOrder := [a,A,b,B], + inverses := [A,a,B,b], + equations := [ + [b*a*b*a*b^2*a*b*a*b^2*a*b^2*a*b*a*b^2*a*b,a], + [a*b^2*a*b^2*a*b*a*b^2*a*b*a,b] + ] +); diff --git a/kb_data/f27monoid b/kb_data/f27monoid new file mode 100644 index 00000000..bfd584c2 --- /dev/null +++ b/kb_data/f27monoid @@ -0,0 +1,12 @@ +#monoid presentation of F(2,7) - should produce a monoid of length 30 +#which is the same as the group, together with the empty word. +#This is a very difficult calculation indeed, however. +_RWS := rec( + isRWS := true, + ordering := "recursive", + maxstoredlen := [15,15], + generatorOrder := [a,b,c,d,e,f,g], + inverses := [], + equations := [[a*b,c], [b*c,d], [c*d,e], [d*e,f], [e*f,g], [f*g,a], [g*a,b] + ] +); diff --git a/kb_data/freenilpc3 b/kb_data/freenilpc3 new file mode 100644 index 00000000..fccf05b2 --- /dev/null +++ b/kb_data/freenilpc3 @@ -0,0 +1,15 @@ +_RWS := rec( + isRWS := true, + ordering := "recursive", + generatorOrder := [e,E,d,D,c,C,b,B,a,A], + inverses := [E,e,D,d,C,c,B,b,A,a], + equations := [ + [B*A*b*a,c], + [C*A*c*a,d], + [C*B*c*b,e], + [d*a,a*d], + [e*a,a*e], + [d*b,b*d], + [e*b,b*e] + ] +); diff --git a/kb_data/funny3 b/kb_data/funny3 new file mode 100644 index 00000000..fe2668a7 --- /dev/null +++ b/kb_data/funny3 @@ -0,0 +1,18 @@ +_RWS:= rec( + isRWS:=true, + generatorOrder:=[x,X,y,Y,z,Z], + inverses:=[X,x,Y,y,Z,z], + ordering:="shortlex", + equations:=[ + [x*x*x,IdWord], + [y*y*y,IdWord], + [z*z*z,IdWord], + [X*Y*x,Y*x*Y], + [y*z*Y,z*Y*z], + [z*x*Z,x*Z*x], + [(x*y*z*X*Y*Z)^3,IdWord], + [(Y*z*x*y*Z*X)^3,IdWord], + [(z*y*X*Z*Y*x)^3,IdWord] + ] +); + diff --git a/kb_data/heinnilp b/kb_data/heinnilp new file mode 100644 index 00000000..66a28bc1 --- /dev/null +++ b/kb_data/heinnilp @@ -0,0 +1,24 @@ +#This example verifies the nilpotence of the group using the Sims algorithm. +#The original presentation was . +# (where [] mean left-normed commutators. The presentation here was derived by +#first applying the NQA to find the maximal nilpotent quotient, and then +#introducing new generators for the PCP generators. +_RWS := rec( + isRWS := true, + ordering := "recursive", + generatorOrder := [f,F,e,E,d,D,c,C,b,B,a,A], + inverses := [F,f,E,e,D,d,C,c,B,b,A,a], + equations := [ + [B*A*b*a,c], + [C*A*c*a,d], + [C*B*c*b,e], + [D*B*d*b,f], + #[d*a,a*d], + #[b*a*B*A*b*A*B*a,a*b*a*B*A*b*A*B], + [c*B*C*b,b*c*B*C], + [b*a*b*A*B*a*B*A,a*b*A*B*a*B*A*b], + [c*B*A*C*a*b,a*b*c*B*A*C], + [B*a*b*A*B*B*A*b*a*b,a*a*b*A*B*B*A*b] + ] +); diff --git a/kb_data/l32ext b/kb_data/l32ext new file mode 100644 index 00000000..4767cff3 --- /dev/null +++ b/kb_data/l32ext @@ -0,0 +1,13 @@ +#An extension of 2^6 be L32 +_RWS := rec( + isRWS := true, + ordering := "shortlex", + generatorOrder := [a,b,B], + inverses := [a,B,b], + equations := [ + [a^2,IdWord], + [B^2,b], + [B*a*B*a*B*a*B,a*b*a*b*a*b*a], + [a*B*a*b*a*B*a*b*a*B*a*b*a*B*a*b,B*a*b*a*B*a*b*a*B*a*b*a*B*a*b*a ] + ] +); diff --git a/kb_data/m11 b/kb_data/m11 new file mode 100644 index 00000000..1774f018 --- /dev/null +++ b/kb_data/m11 @@ -0,0 +1,13 @@ +#Mathieu group M_11 +_RWS := rec( + isRWS := true, + ordering := "shortlex", + generatorOrder := [a,b,B], + inverses := [a,B,b], + equations := [ + [B^2,b^2], + [B*a*B*a*B*a*B*a*B*a*B,a*b*a*b*a*b*a*b*a*b*a], + [b^2*a*b^2*a*b^2*a,a*b^2*a*b^2*a*b^2], + [a*B*a*B*a*b*a*b*a*B*a*b*a*B^2*a*B*a*b,IdWord] + ] +); diff --git a/kb_data/nilp2 b/kb_data/nilp2 new file mode 100644 index 00000000..fd612a87 --- /dev/null +++ b/kb_data/nilp2 @@ -0,0 +1,10 @@ +#Free nilpotent group of rank 2 and class 2 +_RWS := rec( + isRWS := true, + ordering := "recursive", + generatorOrder := [c,C,b,B,a,A], + inverses := [C,c,B,b,A,a], + equations := [ + [b*a,a*b*c], [c*a,a*c], [c*b,b*c] + ] +); diff --git a/kb_data/nonhopf b/kb_data/nonhopf new file mode 100644 index 00000000..ac06a42e --- /dev/null +++ b/kb_data/nonhopf @@ -0,0 +1,10 @@ +#A nonhopfian group +_RWS := rec( + isRWS := true, + maxeqns := 100, + maxstates := 200, + ordering := "recursive", + generatorOrder := [a,A,b,B], + inverses := [A,a,B,b], + equations := [[B*a^2*b,a^3]] +); diff --git a/kb_data/s16 b/kb_data/s16 new file mode 100644 index 00000000..7706fe9e --- /dev/null +++ b/kb_data/s16 @@ -0,0 +1,30 @@ +#Symmetric group S_16 +_RWS := rec( + isRWS := true, + ordering := "shortlex", + generatorOrder := [a,b,c,d,e,f,g,h,i,j,k,l,m,n,o], + inverses := [a,b,c,d,e,f,g,h,i,j,k,l,m,n,o], + equations := [ + [b*a*b,a*b*a],[c*a,a*c],[d*a,a*d],[e*a,a*e],[f*a,a*f],[g*a,a*g],[h*a,a*h], + [i*a,a*i],[j*a,a*j],[k*a,a*k], [l*a,a*l],[m*a,a*m], [n*a,a*n], [o*a,a*o], + [c*b*c,b*c*b],[d*b,b*d],[e*b,b*e],[f*b,b*f],[g*b,b*g],[h*b,b*h], + [i*b,b*i],[j*b,b*j],[k*b,b*k], [l*b,b*l],[m*b,b*m], [n*b,b*n], [o*b,b*o], + [d*c*d,c*d*c],[e*c,c*e],[f*c,c*f],[g*c,c*g],[h*c,c*h], + [i*c,c*i],[j*c,c*j],[k*c,c*k], [l*c,c*l],[m*c,c*m], [n*c,c*n], [o*c,c*o], + [e*d*e,d*e*d],[f*d,d*f],[g*d,d*g],[h*d,d*h], + [i*d,d*i],[j*d,d*j],[k*d,d*k], [l*d,d*l],[m*d,d*m], [n*d,d*n], [o*d,d*o], + [f*e*f,e*f*e],[g*e,e*g],[h*e,e*h], + [i*e,e*i],[j*e,e*j],[k*e,e*k], [l*e,e*l],[m*e,e*m], [n*e,e*n], [o*e,e*o], + [g*f*g,f*g*f],[h*f,f*h], + [i*f,f*i],[j*f,f*j],[k*f,f*k], [l*f,f*l],[m*f,f*m], [n*f,f*n], [o*f,f*o], + [h*g*h,g*h*g], + [i*g,g*i],[j*g,g*j],[k*g,g*k], [l*g,g*l],[m*g,g*m], [n*g,g*n], [o*g,g*o], + [i*h*i,h*i*h],[j*h,h*j], [k*h,h*k], [l*h,h*l],[m*h,h*m], [n*h,h*n], [o*h,h*o], + [j*i*j,i*j*i],[k*i,i*k], [l*i,i*l],[m*i,i*m], [n*i,i*n], [o*i,i*o], + [k*j*k,j*k*j], [l*j,j*l],[m*j,j*m], [n*j,j*n], [o*j,j*o], + [l*k*l,k*l*k],[m*k,k*m], [n*k,k*n], [o*k,k*o], + [m*l*m,l*m*l], [n*l,l*n], [o*l,l*o], + [n*m*n,m*n*m], [o*m,m*o], + [o*n*o,n*o*n] + ] +); diff --git a/kb_data/s3 b/kb_data/s3 new file mode 100644 index 00000000..b8aaecb2 --- /dev/null +++ b/kb_data/s3 @@ -0,0 +1,10 @@ +#Symmetric group S_3 +_RWS := rec( + isRWS := true, + ordering := "shortlex", + generatorOrder := [a,b], + inverses := [a,b], + equations := [ + [b*a*b,a*b*a] +] +); diff --git a/kb_data/s4 b/kb_data/s4 new file mode 100644 index 00000000..6bacc047 --- /dev/null +++ b/kb_data/s4 @@ -0,0 +1,10 @@ +#Symmetric group S_4 +_RWS := rec( + isRWS := true, + ordering := "shortlex", + generatorOrder := [a,b,B], + inverses := [a,B,b], + equations := [ + [b*b,B], [B*a*B*a,a*b*a*b] + ] +); diff --git a/kb_data/s9 b/kb_data/s9 new file mode 100644 index 00000000..1dd305df --- /dev/null +++ b/kb_data/s9 @@ -0,0 +1,16 @@ +#Symmetric group S_9 +_RWS := rec( + isRWS := true, + ordering := "shortlex", + generatorOrder := [a,b,c,d,e,f,g,h], + inverses := [a,b,c,d,e,f,g,h], + equations := [ + [b*a*b,a*b*a],[c*a,a*c],[d*a,a*d],[e*a,a*e],[f*a,a*f],[g*a,a*g],[h*a,a*h], + [c*b*c,b*c*b],[d*b,b*d],[e*b,b*e],[f*b,b*f],[g*b,b*g],[h*b,b*h], + [d*c*d,c*d*c],[e*c,c*e],[f*c,c*f],[g*c,c*g],[h*c,c*h], + [e*d*e,d*e*d],[f*d,d*f],[g*d,d*g],[h*d,d*h], + [f*e*f,e*f*e],[g*e,e*g],[h*e,e*h], + [g*f*g,f*g*f],[h*f,f*h], + [h*g*h,g*h*g] + ] +); diff --git a/kb_data/torus b/kb_data/torus new file mode 100644 index 00000000..70fbfb4d --- /dev/null +++ b/kb_data/torus @@ -0,0 +1,8 @@ +# Torus group +_RWS := rec( + isRWS := true, + ordering := "shortlex", + generatorOrder := [a,A,c,C,b,B,d,D], + inverses := [A,a,C,c,B,b,D,d], + equations := [ [A*B*a*b,D*C*d*c] ] +); diff --git a/kb_data/verifynilp b/kb_data/verifynilp new file mode 100644 index 00000000..8b65a7de --- /dev/null +++ b/kb_data/verifynilp @@ -0,0 +1,25 @@ +#This example verifies the nilpotence of the group using the Sims algorithm. +#The original presentation was . +# (where [] mean left-normed commutators. The presentation here was derived by +#first applying the NQA to find the maximal nilpotent quotient, and then +#introducing new generators for the PCP generators. +#It is essential for success that reasonably low values of the maxstoredlen +#parameter are given. +_RWS := rec( + isRWS := true, + ordering := "recursive", + maxstoredlen := [10,10], + generatorOrder := [h,H,g,G,f,F,e,E,d,D,c,C,b,B,a,A], + inverses := [H,h,G,g,F,f,E,e,D,d,C,c,B,b,A,a], + equations := [ + [B*A*b*a,c], + [C*A*c*a,d], + [D*A*d*a,e], + [E*B*e*b,f], + [F*A*f*a,g], + [g*a,a*g], + [G*B*g*b,h], + [c*b,b*c], + [e*a,a*e] + ] +); From abcd1dab972646e2ae4562e1ce24b097ad0db7d6 Mon Sep 17 00:00:00 2001 From: Marek Kaluba Date: Tue, 27 Apr 2021 00:50:53 +0200 Subject: [PATCH 10/10] isnothing only works for julia-1.1 and above --- src/parsing.jl | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/parsing.jl b/src/parsing.jl index 44f6cec9..209e292c 100644 --- a/src/parsing.jl +++ b/src/parsing.jl @@ -22,6 +22,10 @@ end ### parsing Kbmag input files +if VERSION