kalmarek / knuthbendix.jl Goto Github PK

View Code? Open in Web Editor NEW

8.0 8.0 2.0 804 KB

Pure Julia implementation of the Knuth-Bendix completion (focused primarily on groups and monoids)

License: MIT License

Julia 100.00%

knuthbendix.jl's People

Contributors

Stargazers

Watchers

knuthbendix.jl's Issues

automaton corruption during `knuthbendix!`?

on master:

function RWS_Example_237_abaB(n)
    Al = Alphabet(['a', 'b', 'B'])
    KnuthBendix.set_inversion!(Al, 'b', 'B')

    a, b, B = Word.([i] for i in 1:3)
    ε = one(a)

    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

this example collapses when using automata (but it shouldn't):

julia> R = RWS_Example_237_abaB(4)
Rewriting System with 6 rules ordered by LenLex{Char}(Alphabet{Char}['a', 'b', 'B']):
   1 ✓ b*B   →  (empty word)
   2 ✓ B*b   →  (empty word)
   3 ✓ a*a   →  (empty word)
   4 ✓ b*b*b     →  (empty word)
   5 ✓ a*b*a*b*a*b*a*b*a*b*a*b*a*b   →  (empty word)
   6 ✓ a*b*a*B*a*b*a*B*a*b*a*B*a*b*a*B   →  (empty word)

julia> aut = KnuthBendix.knuthbendix(R, maxrules=35, implementation=:automata)
Rewriting System with 3 rules ordered by LenLex{Char}(Alphabet{Char}['a', 'b', 'B']):
   1 ✓ a     →  (empty word)
   2 ✓ b     →  (empty word)
   3 ✓ B     →  (empty word)

julia> kbs2 = KnuthBendix.knuthbendix(R, maxrules=35, implementation=:naive_kbs2)
┌ Warning: Maximum number of rules (35) in the RewritingSystem reached.
│                 You may retry with `maxrules` kwarg set to higher value.
└ @ KnuthBendix ~/.julia/dev/KnuthBendix/src/kbs.jl:67
Rewriting System with 36 rules ordered by LenLex{Char}(Alphabet{Char}['a', 'b', 'B']):
   1 ✓ a*a   →  (empty word)
   2 ✓ B*b   →  (empty word)
   3 ✓ b*B   →  (empty word)
   4 ✓ b*b   →  B
   5 ✓ B*B   →  b
   6 ✓ b*a*b*a*b*a*b     →  a*B*a*B*a*B*a
   7 ✓ b*a*b*a*B*a*b*a*B     →  B*a*B*a*b*a*B*a
   8 ✓ b*a*B*a*b*a*B*a   →  a*b*a*B*a*b*a*B
   9 ✓ a*B*a*b*a*b*a*B*a*B*a*b   →  B*a*b*a*B*a*B*a*b*a*B
  10 ✓ B*a*B*a*b*a*b*a*B*a*B*a   →  b*a*b*a*B*a*B*a*b*a*b
  11 ✓ b*a*b*a*B*a*b*a*b*a*B*a   →  B*a*B*a*B*a*b*a*b*a*b
  12 ✓ b*a*b*a*B*a*B*a*b*a*b*a   →  B*a*B*a*b*a*b*a*B*a*B
  13 ✓ b*a*B*a*b*a*b*a*B*a*b*a   →  B*a*b*a*b*a*B*a*B*a*b
  14 ✓ a*B*a*B*a*B*a*b   →  b*a*b*a*b*a*B
  15 ✓ b*a*B*a*B*a*B*a   →  B*a*b*a*b*a*b
  16 ✓ b*a*b*a*b*a*B*a*B*a*b     →  a*B*a*b*a*b*a*B*a*b*a
  17 ✓ B*a*B*a*b*a*B*a*b     →  b*a*b*a*B*a*b*a
  18 ✓ B*a*B*a*b*a*B*a*B     →  b*a*b*a*B*a*b*a*b
  19 ✓ B*a*b*a*B*a*b*a   →  a*B*a*b*a*B*a*b
  20 ✓ B*a*B*a*b*a*b*a*B*a*b     →  a*b*a*b*a*B*a*B*a*b*a
  21 ✓ b*a*b*a*B*a*B*a*b*a*B     →  a*B*a*B*a*b*a*b*a*B*a
  22 ✓ a*B*a*b*a*B*a*B*a*b*a*B   →  B*a*b*a*b*a*B*a*B*a*b
  23 ✓ B*a*b*a*B*a*B*a*b*a*b     →  a*B*a*b*a*b*a*B*a*B*a
  24 ✓ a*b*a*b*a*B*a*B*a*b*a*b   →  B*a*B*a*b*a*b*a*B*a*B
  25 ✓ b*a*B*a*B*a*b*a*b*a*b     →  a*b*a*B*a*b*a*b*a*B*a
  26 ✓ B*a*b*a*b*a*B*a*B*a*B     →  a*B*a*b*a*B*a*B*a*b*a
  27 ✓ b*a*B*a*b*a*b*a*B*a*B     →  a*b*a*B*a*B*a*b*a*b*a
  28 ✓ B*a*b*a*b*a*b*a   →  b*a*B*a*B*a*B
  29 ✓ B*a*b*a*b*a*B*a*B*a*b*a   →  b*a*B*a*b*a*b*a*B*a*b
  30 ✓ B*a*B*a*B*a*b*a*b*a*B*a   →  a*b*a*B*a*B*a*b*a*B
  31 ✓ B*a*B*a*B*a*B     →  a*b*a*b*a*b*a
  32 ✓ a*b*a*b*a*b*a*B   →  B*a*B*a*B*a*b
  33 ✓ b*a*b*a*b*a*B*a*b*a*b*a*b     →  a*b*a*b*a*B*a*b*a*b*a
  34 ✓ a*b*a*B*a*b*a*b*a*B*a*b   →  b*a*B*a*B*a*b*a*b*a*B
  35 ✓ a*B*a*b*a*b*a*B*a*b*a*b   →  b*a*b*a*b*a*B*a*B*a*B
  36 ✓ b*a*B*a*B*a*b*a*b*a*B*a*B     →  a*B*a*b*a*b*a*B*a*B*a

however stopping the process in the middle makes knuthbendix! with automaton complete successfully:

julia> let n = 34
           kbs = KnuthBendix.knuthbendix(R, maxrules=n, implementation=:naive_kbs2)
           aut = KnuthBendix.knuthbendix(R, maxrules=n, implementation=:automata)
           @info "" length(kbs) length(aut)

           @info "" length(KnuthBendix.knuthbendix(aut, implementation=:automata)) length(KnuthBendix.knuthbendix(aut, implementation=:naive_kbs2))
       end
┌ Warning: Maximum number of rules (34) in the RewritingSystem reached.
│                 You may retry with `maxrules` kwarg set to higher value.
└ @ KnuthBendix ~/.julia/dev/KnuthBendix/src/kbs.jl:67
┌ Warning: Maximum number of rules (34) in the RewritingSystem reached.
│                 You may retry with `maxrules` kwarg set to higher value.
└ @ KnuthBendix ~/.julia/dev/KnuthBendix/src/kbs.jl:166
┌ Info: 
│   length(kbs) = 35
└   length(aut) = 35
┌ Info: 
│   length(KnuthBendix.knuthbendix(aut, implementation = :automata)) = 40
└   length(KnuthBendix.knuthbendix(aut, implementation = :naive_kbs2)) = 40

New examples

this:
https://www.sciencedirect.com/science/article/pii/0022404994900191

defines RecursivePathOrdering and applies it to surface groups; Would be great to add it to our tests.

design for multithreading [updated: kbWork]

At the moment the design of knuthbendix is strictly single-threaded, but maybe the algorithm can be divided into several steps that are easier to multithread?

Essentially given an rws we need to

generate new rules from the old ones
locate and resolve critical pairs of rules
merge the resolved critical pairs with rws

The only step that is obviously hard to multithread is the third one due to data sharing. It seems that both 1. and 2. can be multithreaded, so maybe we use threadsafe stack that threads in 1. and 2. use?

Indexing into `Word`s and `views`

To consider for later: right now when we iterate over Word we obtain Integers. If we subset Word via iterator we obtain a vector. Maybe it is sensible to always obtain Word via that protocol, i.e. Word([1,2,3])[2] = Word([2]) and Word([1,2,3])[2:3] = Word([2,3]). It would make the code for kbs1 clearer (shall I open an issue to discuss it separately? This is not something important and maybe later it will become more evident in which way this should be solved).

major refactor of IndexAutomaton??

Just collecting some ideas after #38 is merged.

walk(::Automaton, ::AbstractWord)

I think this should be renamed to trace
I think there is little advantage of breaking prematurely and returning the last (non-failed) state (even though I suggested this): maybe a simpler solution like below is better?

function trace(a::AbstractAutomaton, signature::AbstractWord, state=initialstate(a))
    for k in signature
        next = outedges(state)[k]
        isfailstate(next) ? return next : state = next
    end
    return state
end

outedges(state) → this doesn't return an edge but a neighboring state ;) LightGraphs.jl use outneighbors: https://github.com/JuliaGraphs/LightGraphs.jl/blob/ce533729381a6c0b0d8a1eb5f0c3e058833cb55b/src/interface.jl#L336
(I don't mean using LightGraphs directly, but adopting their naming)

Enumerate normal forms from a given RewritingSystem/Automaton

For a parallel project I'd need a way to enumerate words in normal form from a group.
The only prerequisite is that the group elements appear with non-decreasing word-length.

So what I'd like to produce is a struct which behaves like an AbstractVector for deterministic quering for the i-th element of the group (without actually storing all of these at the same time).

Would it be possible?

taking rewriting rules seriously

one reason why arules was so slow is that act and rwrules are kept separately (which is also bad for cache locality in the long run). We might consider creating

struct RewrtitingRule{W<:AbstractWord}
    lhs::W
    rhs::W
    active::Bool
    ....
end

to keep the information closely packed together; the drawback is the size (8 bytes per Bool), the advantage (besides locality of information) is that BitArrays are not thread-safe:

help?> BitArray
search: BitArray

  BitArray{N} <: AbstractArray{Bool, N}

  Space-efficient N-dimensional boolean array, using just one bit for each boolean value.

  BitArrays pack up to 64 values into every 8 bytes, resulting in an 8x space efficiency
  over Array{Bool, N} and allowing some operations to work on 64 values at once.

  By default, Julia returns BitArrays from broadcasting operations that generate boolean
  elements (including dotted-comparisons like .==) as well as from the functions trues and
  falses.

  │ Note
  │
  │  Due to its packed storage format, concurrent access to the elements of a
  │  BitArray where at least one of them is a write is not thread safe.

is getirrsubsystem correct?

As implemented here:

KnuthBendix.jl/src/kbs1.jl

Line 43 in 342b15e

function getirrsubsys(rs::RewritingSystem{W}) where W

shouldn't we test all subwords, not only prefixes and suffixes?

btw. rewriting and comparing a word is a poor test for irreducibility. This could be implemented e.g.

function isirreducible(w::AbstractWord, rws::RewritingSystem)
    for (lhs, _) in rules(rws)
        issubword(lhs, w) && lhs != w && return false
    end
    return true
end

without allocations

Implement Words

as a struct

abstract type AbstractWord{T} <: AbstractVector{T}

struct Word{T<:Integer}<:AbstractWord{T}
    ptrs::Vector{T}
end

implement: *, one, iteration, etc.

TagBot trigger issue

This issue is used to trigger TagBot; feel free to unsubscribe.

If you haven't already, you should update your TagBot.yml to include issue comment triggers.
Please see this post on Discourse for instructions and more details.

If you'd like for me to do this for you, comment TagBot fix on this issue.
I'll open a PR within a few hours, please be patient!

integrate IndexAutomaton with Knuth Bendix

integrate IndexAutomaton with BufferWords
update IndexAutomaton with new rules
integrate with Knuth-Bendix (knuthbendix! on an Automaton?)

Naming of functions

@kalmarek proposed:

test1! -> deriverule!
overlap1! -> isconfluent_local
(there will be isconfluent(rws::RewritingSystem))

Zipping reversed BufferWords yields error

The following yields error when one of the BufferWords in reverse is empty (i.e. is \varepsilon):

function simplifyrule!(lhs::AbstractWord, rhs::AbstractWord, A::Alphabet)
    n=1
    for (lu, lv) in zip(lhs,rhs)
        lu != lv && break
        hasinverse(lu , A) || break
        n += 1
    end
    copyto!(lhs, @view lhs[n:end])
    copyto!(rhs, @view rhs[n:end])
    resize!(lhs, length(lhs)-n+1)
    resize!(rhs, length(rhs)-n+1)
    m = 0
    for (lu, lv) in zip(reverse(lhs), reverse(rhs))
        lu != lv && break
        hasinverse(lu , A) || break
        m += 1
    end
    resize!(lhs, length(lhs)-m)
    resize!(rhs, length(rhs)-m)
end

[BTW: the above unfortunately gives 2 allocations - due to reverse.]

The example of error:

KBS2_with_deleting: Error During Test at /Users/mikolajpabiszczak/Documents/GitHub/KnuthBendix.jl/test/kbs2_with_deleting.jl:30
  Test threw exception
  Expression: Set(KnuthBendix.rules(KnuthBendix.knuthbendix2delinactive(rs))) == crs
  BoundsError: attempt to access 0-element BufferWord{UInt16} at index [1]
  Stacktrace:
   [1] throw_boundserror(::BufferWord{UInt16}, ::Tuple{Int64}) at ./abstractarray.jl:541
   [2] checkbounds at ./abstractarray.jl:506 [inlined]
   [3] setindex! at /Users/mikolajpabiszczak/Documents/GitHub/KnuthBendix.jl/src/bufferwords.jl:62 [inlined]
   [4] reverse(::BufferWord{UInt16}, ::Int64, ::Int64) at ./array.jl:1598
   [5] reverse at ./array.jl:1593 [inlined]
   [6] simplifyrule!(::BufferWord{UInt16}, ::BufferWord{UInt16}, ::Alphabet{Char}) at /Users/mikolajpabiszczak/Documents/GitHub/KnuthBendix.jl/src/rewriting.jl:152
   [7] deriverule!(::RewritingSystem{Word{UInt16},LenLex{Char}}, ::Array{Pair{Word{UInt16},Word{UInt16}},1}, ::KnuthBendix.kbWork{UInt16}, ::LenLex{Char}, ::Bool) at /Users/mikolajpabiszczak/Documents/GitHub/KnuthBendix.jl/src/kbs2_with_deleting.jl:59
   [8] knuthbendix2delinactive!(::RewritingSystem{Word{UInt16},LenLex{Char}}, ::LenLex{Char}; maxrules::Int64) at /Users/mikolajpabiszczak/Documents/GitHub/KnuthBendix.jl/src/kbs2_with_deleting.jl:93
   [9] #knuthbendix2delinactive#33 at /Users/mikolajpabiszczak/Documents/GitHub/KnuthBendix.jl/src/kbs2_with_deleting.jl:117 [inlined]
   [10] knuthbendix2delinactive(::RewritingSystem{Word{UInt16},LenLex{Char}}) at /Users/mikolajpabiszczak/Documents/GitHub/KnuthBendix.jl/src/kbs2_with_deleting.jl:117
   [11] top-level scope at /Users/mikolajpabiszczak/Documents/GitHub/KnuthBendix.jl/test/kbs2_with_deleting.jl:30
   [12] top-level scope at /Users/julia/buildbot/worker/package_macos64/build/usr/share/julia/stdlib/v1.5/Test/src/Test.jl:1115
   [13] top-level scope at /Users/mikolajpabiszczak/Documents/GitHub/KnuthBendix.jl/test/kbs2_with_deleting.jl:3

Let me note that this error is due to BufferWords: the same simplifyrule! when used with the naïve implementation of KnuthBendix2 (i.e. the one which does not use BufferWords from BufferPairs) works ok (so the error occurs only for kbs2 with deleting or with automata)

Implement KBS_1

according to p. 70 of Sims book:

words #3 #6 #16
alphabet #4 #7 #9
ordering? (each of them as a struct <: AbstractOrdering) #10
data structure for rewriting rules (Tuples?)

Shaving off even more allocations

Currently (even with #23) the number of allocations in each iteration of knuthbendix2(rws)

KnuthBendix.jl/src/kbs2.jl

Line 80 in 665ad03

while (j ≤ i && isactive(tmprs, i))

is proportional to length(rws) which is killing the performance in the long run;
We should aim at O(number of new rules added).

But this would need several changes which prompted me to think about the design:

create the buffers v::BufferWord{T} and w::BufferWord{T} once per knuthbendix2 call and pass those through calls forceconfluence!(...) → deriverule!(...) → rewrite_from_left!(...). Moreover we'd need more than these v and w, since two subsequent calls to rewrite_from_left! happen in deriverule!(...), so more permanent storage is needed there to keep the results of rewriting from being overwritten (essentially two vs and two ws need to be passed through). This feels clumsy and error-prone.
add those vs and ws as fields of rws which is already passed through the chain. This is very much kbmag style :P and has the added "benefit" of not being thread-safe. I'd not go this way.
borrow the design from hpc solvers, i.e. create a separate KnuthBendixWork struct (not a very pretty name, I know:) once (per thread) which encapsulates the needed temporaries, runtime parameters, etc. Then call the function chain above on KnuthBendixWork. E.g. of such design is in SCS: https://github.com/cvxgrp/scs/blob/master/include/scs.h.

@bprzybylski @mikolajpabiszczak

Example 5.5 - Sims does not replicate

There is some problem with Example 5.5 / p. 74 form the Sims' book. Our code yields:

rws = KnuthBendix.knuthbendix1(R)
Rewriting System with 18 rules ordered by WreathOrder{Char}(Alphabet{Char}['c', 'C', 'b', 'B', 'a', 'A']):
   1 ✓ a*A       →      (empty word)
   2 ✓ A*a       →      (empty word)
   3 ✓ b*B       →      (empty word)
   4 ✓ B*b       →      (empty word)
   5 ✓ c*C       →      (empty word)
   6 ✓ C*c       →      (empty word)
   7 ✓ c*a       →      a*c
   8 ✓ c*b       →      b*c
   9 ✓ b*a       →      a*b*c
  10 ✓ c*A       →      A*c
  11 ✓ C*a       →      a*C
  12 ✓ c*B       →      B*c
  13 ✓ C*b       →      b*C
  14 ✓ b*A       →      A*b*C
  15 ✓ B*a       →      a*B*C
  16 ✓ C*A       →      A*C
  17 ✓ C*B       →      B*C
  18 ✓ B*A       →      A*B*c

which is not the same as the system claimed by Sims - namely the right-hand sides of rules 14 and 15 (rules 27 and 36 in the Table 2.5.5 / p. 75) differ. (Note that the the sizes of final systems agree in book and in our implementation - 18 rules).

Checking all the rules that our kbs1 returns:

Rewriting System with 37 rules ordered by WreathOrder{Char}(Alphabet{Char}['c', 'C', 'b', 'B', 'a', 'A']):
   1 ✓ a*A       →      (empty word)
   2 ✓ A*a       →      (empty word)
   3 ✓ b*B       →      (empty word)
   4 ✓ B*b       →      (empty word)
   5 ✓ c*C       →      (empty word)
   6 ✓ C*c       →      (empty word)
   7 ✓ c*a       →      a*c
   8 ✓ c*b       →      b*c
   9 ✓ b*a       →      a*b*c
  10 ✓ a*c*A     →      c
  11 ✓ C*a*c     →      a
  12 ✓ b*c*B     →      c
  13 ✓ C*b*c     →      b
  14 ✓ a*b*c*A   →      b
  15 ✓ B*a*b*c   →      a
  16 ✓ c*A       →      A*c
  17 ✓ C*a       →      a*C
  18 ✓ c*B       →      B*c
  19 ✓ C*b       →      b*C
  20 ✓ b*A*c     →      A*b
  21 ✓ a*b*A*b*c         →      b*b
  22 ✓ B*a*b     →      a*C
  23 ✓ B*a*c     →      a*B
  24 ✓ C*A*c     →      A
  25 ✓ a*C*A     →      C
  26 ✓ a*b*A     →      b*C
  27 ✓ C*B*c     →      B
  28 ✓ b*C*B     →      C
  29 ✓ B*A*b     →      A*c
  30 ✓ b*A       →      A*b*C
  31 ✓ C*A*b     →      A*b*C
  32 ✓ B*a       →      a*C*B
  33 ✓ a*C*B     →      a*B*C
  34 ✓ a*B*A     →      B*c
  35 ✓ C*A       →      A*C
  36 ✓ C*B       →      B*C
  37 ✓ B*A       →      A*B*c

looking at this second list we have less rules (37) than in the Table 2.5.5. / p.75 (41) and the first rule that does not agree with the table is number 17.

I will just hint that I am inclined to believe that this is an error in the book (I tracked one such error earlier).

incorporate example Monoid implementation?

See:
https://gist.github.com/kalmarek/9475f36e768046cd7ef7fc08891bf553

julia> include("Monoids.jl")

julia> using .Monoids

julia> function example_monoid(n::Integer)
           A = Alphabet([[Symbol('a', i) for i in 1:n]; [Symbol('b', i) for i in 1:n]])
           F = FreeMonoid(A)
           rels = let S = gens(F)
               squares = [g^2=>one(g) for g in S]
               @views a, b = S[1:n], S[n+1:end]
               aibj = [a[i]*b[j] => b[j]*a[i] for i in 1:n for j in 1:n]
               [squares; aibj]
           end

           return F/rels
       end
example_monoid (generic function with 1 method)

julia> M = example_monoid(2)
monoid with 8 relations over Alphabet{Symbol}[:a1, :a2, :b1, :b2]

julia> a, b = M(rand(1:4, 20)), M(rand(1:4, 20))
(a1*a2*a1*a2*b1*b2*b1*b2*b1*b2, a2*a1*a2*a1*a2*b2*b1*b2)

julia> a*b
a2*b1*b2*b1

julia> b*a
a2*a1*a2*a1*a2*a1*a2*a1*a2*b2*b1*b2*b1*b2*b1*b2*b1*b2

julia> x = M(rand(1:4, 20)); isreduced(x)
false

julia> y = deepcopy(x); normalform!(y); isreduced(y)
true

julia> x === y
false

julia> x == y
true

Possible improvements

use DataStructures.Stack as stack
prioritize short overlaps (therein, p.84)
rules balancing (Sims, Secion 2.7 p. 85)
skipping overlaps (Prop 7.1, p.87)

Low hanging technical issues:

periodically remove dead rules

kalmarek / knuthbendix.jl Goto Github PK

knuthbendix.jl's People

Contributors

Stargazers

Watchers

knuthbendix.jl's Issues

Recommend Projects

Recommend Topics

Recommend Org