kalmarek / KnuthBendix.jl

Pure Julia implementation of the Knuth-Bendix completion (focused primarily on groups and monoids)
MIT License
8 stars 2 forks source link

Enumerate normal forms from a given RewritingSystem/Automaton #35

Open kalmarek opened 4 years ago

kalmarek commented 4 years ago

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?

kalmarek commented 1 year ago

Just enumerating is running a bfs exploration through IndexAutomaton. Getting just i-th element is not possible.

kalmarek commented 1 year ago

Example implementation

# to be moved to KnuthBendix
function KnuthBendix.alphabet(idx::KnuthBendix.IndexAutomaton)
    return KnuthBendix.alphabet(KnuthBendix.ordering(idx))
end

# to be moved to KnuthBendix.Automata
function irreducible_words(
    idxA::KnuthBendix.IndexAutomaton{S};
    radius,
) where {S}
    W = KnuthBendix.word_type(idxA)
    queue = [(KnuthBendix.Automata.initial(idxA), one(W))]
    words = W[last(first(queue))]
    sizes = Int[]
    while !isempty(queue)
        (σ, w) = popfirst!(queue)
        if length(w) ≥ radius
            push!(sizes, length(words))
            break
        end

        for letter in 1:length(alphabet(idxA))
            τ = KnuthBendix.Automata.trace(letter, idxA, σ)
            if KnuthBendix.Automata.isterminal(idxA, τ)
                continue
            else
                w_copy = copy(w)
                push!(w_copy, letter)
                if length(w_copy) > length(last(words))
                    push!(sizes, length(words))
                end
                push!(words, w_copy)
                push!(queue, (τ, w_copy))
            end
        end
    end
    if isempty(queue)
        for _ in (length(sizes)+1):radius
            push!(sizes, last(sizes))
        end
    end
    sizes = sizes[2:end]
    @assert length(sizes) == radius
    return words, sizes
end

using Test

@testset "irreducible_words.jl" begin
    π₁Σ₃ = π₁_surface(; genus = 3)
    # precompilation:
    irreducible_words(π₁Σ₃.rw; radius = 2)

    E, sizes = irreducible_words(π₁Σ₃.rw; radius = 0)
    @test length(E) == 1
    @test E[1] == one(Word{UInt8})
    @test sizes == Int[]

    E, sizes = irreducible_words(π₁Σ₃.rw; radius = 1)
    @test length(E) == 13
    @test sizes == [13]
    @test [length(w) for w in E] == [0; fill(1, 12)]

    E, sizes = irreducible_words(π₁Σ₃.rw; radius = 2)
    @test length(E) == 145
    @test sizes == [13, 145]
    @test allequal(length(w) for w in E[(sizes[1]+1):sizes[2]])

    SIZES = [13, 145, 1597, 17569, 193261, 2125861]

    for R in 1:5
        k = @allocations sizes = last(irreducible_words(π₁Σ₃.rw; radius = R))
        v = k - 2sizes[end]
        @test v < 20 || (sizes[end] > 1000 && v / k < 1 / 100)
        @test sizes == SIZES[1:R]
    end
end