From ef5e87a57e42ba71be293f73e2fabb8fd2e91617 Mon Sep 17 00:00:00 2001 From: Kris Brown Date: Mon, 24 Jun 2024 18:56:38 -0700 Subject: [PATCH] Auto stash before merge of "allepis" and "main" no schema parameter --- Project.toml | 9 +- src/categorical_algebra/CSets.jl | 2 + src/incremental/Algorithms.jl | 165 ++++++++++++++++++---- src/incremental/IncrementalCC.jl | 36 +++-- src/incremental/IncrementalConstraints.jl | 8 +- test/Project.toml | 2 + test/incremental/Algorithms.jl | 31 +++- test/incremental/IncrementalCC.jl | 2 - 8 files changed, 206 insertions(+), 49 deletions(-) diff --git a/Project.toml b/Project.toml index d617194..003e8a5 100644 --- a/Project.toml +++ b/Project.toml @@ -14,22 +14,23 @@ Random = "9a3f8284-a2c9-5f02-9a11-845980a1fd5c" Reexport = "189a3867-3050-52da-a836-e630ba90ab69" StructEquality = "6ec83bb0-ed9f-11e9-3b4c-2b04cb4e219c" Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40" +nauty_jll = "55c6dc9b-343a-50ca-8ff2-b71adb3733d5" [weakdeps] -Luxor = "ae8d54c2-7ccd-5906-9d76-62fc9837b5bc" DataMigrations = "0c4ad18d-0c49-4bc2-90d5-5bca8f00d6ae" +Luxor = "ae8d54c2-7ccd-5906-9d76-62fc9837b5bc" [extensions] -AlgebraicRewritingLuxorExt = "Luxor" AlgebraicRewritingDataMigrationsExt = "DataMigrations" +AlgebraicRewritingLuxorExt = "Luxor" [compat] ACSets = "0.2.20" Catlab = "0.16.11" +CompTime = "0.1" DataMigrations = "0.0.3" DataStructures = "0.17, 0.18" +MLStyle = "0.4" Reexport = "^1" StructEquality = "2.1" julia = "1.9" -MLStyle = "0.4" -CompTime = "0.1" diff --git a/src/categorical_algebra/CSets.jl b/src/categorical_algebra/CSets.jl index 7789ff4..a1579b8 100644 --- a/src/categorical_algebra/CSets.jl +++ b/src/categorical_algebra/CSets.jl @@ -360,6 +360,8 @@ substitution. We do this via pushout. """ function sub_vars(X::ACSet, subs::AbstractDict=Dict(), merge::AbstractDict=Dict()) S = acset_schema(X) + show(stdout,"text/plain",X) + println("SUBS $subs") O, C = [constructor(X)() for _ in 1:2] ox_, oc_ = Dict{Symbol, Any}(), Dict{Symbol,Any}() for at in attrtypes(S) diff --git a/src/incremental/Algorithms.jl b/src/incremental/Algorithms.jl index a747889..7e5f93d 100644 --- a/src/incremental/Algorithms.jl +++ b/src/incremental/Algorithms.jl @@ -1,8 +1,24 @@ module Algorithms -using Catlab +using Catlab, nauty_jll using ...CategoricalAlgebra.CSets: invert_iso, var_reference -using ...Rewrite.Migration: pres_hash +using ...Rewrite.Migration: pres_hash, repr_dict + +const Hom = ACSetTransformation # shorter type signatures + +"""For debugging""" +function prnt(s,x::ACSet) + println(s); + show(stdout,"text/plain",x) +end + +"""For debugging""" +function prnt(s, x::Hom) + println(s) + for (k,v) in pairs(components(x)) + println("\t$k: [$(join(string.(collect(v)), ","))]") + end +end """ Break an ACSet into connected components, represented as a coproduct and an @@ -41,8 +57,7 @@ function connected_acset_components(X::ACSet) end comp = constructor(X)() copy_parts!(comp, X; d...) - ACSetTransformation(comp, X; Dict(k=>k ∈ ob(S) ? v : AttrVar.(v) - for (k, v) in pairs(d))...) + Hom(comp, X; Dict(k=>k ∈ ob(S) ? v : AttrVar.(v) for (k, v) in pairs(d))...) end |> Multicospan cp = coproduct(dom.(ιs)) return (cp, invert_iso(universal(cp, ιs))) @@ -53,15 +68,31 @@ Find all partial maps from the pattern to the addition, with some restrictions: 1. *Something* must be mapped into the newly added material. 2. Anything in L incident to a part mapped onto newly added material must be mapped to newly added material + +The shape of the addition may be different from R because it has been quotiented +due to a non-monic match. Given some I ↠ I' at runtime, the effective map I → R +is actually a composite map via pushout with I ↠ I': + + I ↣ R + ↡ ↓ + I'→⌜R' + +So we use this map I → R' rather than I → R for the purposes of the above +calculation. """ -function compute_overlaps(L::ACSet, I_R::ACSetTransformation; monic=[], - )::Vector{Span} - overlaps = Span[] - for subobj in all_subobjects(L) - abs_subobj = abstract_attributes(dom(subobj)) - for h in homomorphisms(dom(abs_subobj), codom(I_R); monic) - lft = abs_subobj ⋅ subobj - good_overlap(lft, h, I_R) && push!(overlaps, Span(lft, h)) +function compute_overlaps(L::ACSet, I_R::Hom; monic=[], S=nothing + )::Dict{Hom, Vector{Span}} + overlaps = Dict{Hom, Vector{Span}}() + subobjs = all_subobjects(L) + for I_I′ in all_epis(dom(I_R)) + overlaps[I_I′] = Span[] + I_R′ = I_R ⋅ first(pushout(I_R, I_I′)) + for subobj in subobjs + abs_subobj = abstract_attributes(dom(subobj)) + for h in homomorphisms(dom(abs_subobj), codom(I_R′); monic) + lft = abs_subobj ⋅ subobj + good_overlap(lft, h, I_R′) && push!(overlaps[I_I′], Span(lft, h)) + end end end return overlaps @@ -75,8 +106,7 @@ end Subobject O is presumed to be abstract, i.e. has only (distinct) variables """ -function good_overlap(subobj::ACSetTransformation, h::ACSetTransformation, - I_R::ACSetTransformation) +function good_overlap(subobj::Hom, h::Hom, I_R::Hom) S = acset_schema(dom(h)) L = codom(subobj) O = dom(subobj) # for "overlap" @@ -139,7 +169,7 @@ deleted, X ∖ X'). Thus, our process for finding overlaps requires only searching for morphisms between two things which are themselves pattern-sized. """ -function nac_overlap(nac, update::ACSetTransformation) +function nac_overlap(nac, update::Hom) N = codom(nac) Ob = ob(acset_schema(N)) L_parts_in_N = Dict(o=>Set(collect(nac.m[o])) for o in Ob) @@ -180,8 +210,7 @@ commute, if it exists. TODO rewrite with @comptime """ -function pull_back(f::ACSetTransformation, m::ACSetTransformation - )::Union{ACSetTransformation, Nothing} +function pull_back(f::Hom, m::Hom)::Union{Hom, Nothing} L, X′ = dom.([m, f]) comps, S = Dict(), acset_schema(L) for o in ob(S) @@ -209,11 +238,11 @@ function pull_back(f::ACSetTransformation, m::ACSetTransformation return only(vals) end end - ACSetTransformation(dom(m), dom(f); comps...) + Hom(dom(m), dom(f); comps...) end """Get the pairs for each component of the image and its component""" -partition_image(f::ACSetTransformation) = Dict(map(ob(acset_schema(dom(f)))) do o +partition_image(f::Hom) = Dict(map(ob(acset_schema(dom(f)))) do o del,nondel = Set(parts(codom(f), o)), Set{Int}() for p in parts(dom(f), o) push!(nondel, f[o](p)) @@ -227,8 +256,8 @@ Compute and cache the subobject classifier; reuse if already computed. Some schemas have no finitely presentable subobject classifier. Return `nothing` in that case. """ -function subobject_cache(T::Type; cache="cache") - S = deattr(Presentation(T)) +function subobject_cache(T::Type, S=nothing; cache="cache") + S = deattr(Presentation(isnothing(S) ? T : S)) T = AnonACSetType(Schema(S)) name = joinpath(cache,"Ω_$(nameof(T))_$(pres_hash(S)).json") mkpath(cache) @@ -255,7 +284,7 @@ end Convert a morphism X → Ω into a subobject X'↣X, assuming that Ω was generated by Catlab's `subobject_classifier` function. """ -function to_subobj(f::ACSetTransformation) +function to_subobj(f::Hom) Subobject(dom(f); Dict(map(collect(pairs(components(f)))) do (k, v) k => findall(==(1), collect(v)) end)...) @@ -269,7 +298,7 @@ function all_subobjects(X::ACSet; cache="cache") X′ = typeof(Ω)() copy_parts!(X′, X) return map(homomorphisms(X′, Ω; alg=VMSearch())) do h - f = hom(to_subobj(ACSetTransformation(X′, Ω; h...))) + f = hom(to_subobj(Hom(X′, Ω; h...))) A = constructor(X)() copy_parts!(A, dom(f)) h′ = Dict(o => get(components(f), o, []) for o in types(S)) @@ -279,7 +308,7 @@ function all_subobjects(X::ACSet; cache="cache") push!(h′[d], X[f[c](p), a]) end end - ACSetTransformation(A, X; h′...) + Hom(A, X; h′...) end end @@ -300,7 +329,7 @@ VarFunctions can both bind variables to concrete values or merge variables together. Although the overall VarFunction is not monic if either of these happens, it is only combinatorially non-monic if variables are merged together. """ -function is_combinatorially_monic(f::ACSetTransformation) +function is_combinatorially_monic(f::Hom)::Bool S = acset_schema(dom(f)) all(o -> is_monic(f[o]), ob(S)) || return false return all(attrtype(S)) do o @@ -308,4 +337,90 @@ function is_combinatorially_monic(f::ACSetTransformation) length(attrimg) == length(unique(attrimg)) end end + +function ACSetTransformation(X::ACSet, canon::CSetNautyRes) + ACSetTransformation(X, canon.canon; canon.canonmap...) +end + + +function all_epis(X::ACSet) + S = acset_schema(X) + reprs = repr_dict(typeof(X)) + + # Create schema for arrow category, where domain is NOT up to iso + S′ = copy(Presentation(S)) + gens = Dict(o => add_generator!(S′, Ob(FreeSchema, eq(o))) for o in ob(S)) + _Fix = add_generator!(S′, AttrType(FreeSchema.AttrType, :_Fix)) + for o in ob(S) + add_generator!(S′, Catlab.Hom(alpha(o), Ob(FreeSchema,o), gens[o])) + add_generator!(S′, Catlab.Attr(Symbol("$(o)_fix"), Ob(FreeSchema,o), _Fix)) + end + for (f, c, d) in homs(S) + add_generator!(S′, Catlab.Hom(eq(f), gens[c], gens[d])) + end + + # Helper functions + """Pushforward S -> S' along the codom inclusion of the collage""" + function cheap_sigma(Z::ACSet) + Z′ = AnonACSet(S′; type_assignment=Dict(:_Fix=>Int)) + for o in ob(S) + add_parts!(Z′, eq(o), nparts(Z, o)) + end + for h in homs(S; just_names=true) + Z′[eq(h)] = Z[h] + end + return Z′ + end + + """Convert an ACSet with schema S' into an epimorphism in schema S""" + function cheap_uncurry(Z::ACSet) + Z′ = constructor(X)() + comps = map(ob(S)) do o + add_parts!(Z′, o, nparts(Z, eq(o))) + o => Z[alpha(o)] + end + ACSetTransformation(X, Z′; comps...) + end + + """Unique map from the representable `o` to the i'th `o` equivalence class""" + function get_map(Z::ACSet, o::Symbol, i::Int) + R, ι = reprs[o] + homomorphism(cheap_sigma(R), Z; initial=Dict(eq(o) => Dict(ι=>i))) + end + + # Initial partition (nothing merged) + X′ = cheap_sigma(X) + copy_parts!(X′, X) + for o in ob(S) + X′[Symbol("$(o)_fix")] = X′[alpha(o)] = parts(X, o) + end + + epis, queue = Dict{String, ACSet}("" => X′), Set{ACSet}([X′]) + + # All possible pairwise mergings of eq classes, tree search + while !isempty(queue) + Q = pop!(queue) + for o in ob(S) + for i ∈ 1:(nparts(Q, eq(o))-1) + f = get_map(Q, o, i) + for j ∈ (i+1):nparts(Q, eq(o)) + g = get_map(Q, o, j) + Q′ = codom(first(coequalizer(f, g))) + hsh = call_nauty(Q′).strhsh + if !(haskey(epis, hsh)) + push!(queue, Q′) + epis[hsh] = Q′ + end + end + end + end + end + return cheap_uncurry.(collect(values(epis))) +end + +eq(x::Symbol) = Symbol("$(x)_eq") +alpha(x::Symbol) = Symbol("$(x)_α") + + + end # module diff --git a/src/incremental/IncrementalCC.jl b/src/incremental/IncrementalCC.jl index bc5f52c..6828743 100644 --- a/src/incremental/IncrementalCC.jl +++ b/src/incremental/IncrementalCC.jl @@ -17,13 +17,16 @@ using Catlab.CategoricalAlgebra.Chase: extend_morphism_constraints using StructEquality +const Hom = ACSetTransformation # shorter type signatures """ For `IncCCHomSet` the pattern (`L`) ought be a single connected component or have constraints forcing it to be treated all at once instead of componentwise. + +Precomputed overlap spans are """ @struct_hash_equal struct IncCCStatic <: IncStatic pattern::ACSet - overlaps::Dict{ACSetTransformation, Vector{Span}} + overlaps::Dict{Hom, Dict{ACSet, Dict{Hom, Vector{Span}}}} function IncCCStatic(pattern::ACSet, constr::IncConstraints, adds=[]) hs = new(pattern, Dict()) push!.(Ref(hs), Ref(constr,), adds) @@ -35,7 +38,7 @@ additions(h::IncCCStatic) = collect(keys(h.overlaps)) """Consider a new addition (and compute its partial overlaps w/ the pattern)""" function Base.push!(hs::IncCCStatic, constr::IncConstraints, - addition::ACSetTransformation) + addition::Hom) haskey(hs.overlaps, addition) && return nothing hs.overlaps[addition]=compute_overlaps(pattern(hs), addition; constr.monic) end @@ -63,7 +66,7 @@ This assumes the state of the world is changed in discrete updates. post-hoc constraints. """ @struct_hash_equal mutable struct IncCCRuntime <: IncRuntime - const match_vect::Vector{Dict{Int, ACSetTransformation}} + const match_vect::Vector{Dict{Int, Hom}} const key_vect::Vector{Pair{Int,Int}} const key_dict::Dict{Pair{Int,Int}, Int} state::ACSet @@ -89,7 +92,7 @@ state(h::IncCCRuntime) = h.state constraints::IncConstraints end -Base.getindex(i::IncCCHomSet, idx::Int)::ACSetTransformation = runtime(i)[idx] +Base.getindex(i::IncCCHomSet, idx::Int)::Hom = runtime(i)[idx] """ How many additions we've seen so far (including the initialization of the hom @@ -130,9 +133,13 @@ Note, adding things can also invalidate old matches if there are negative application or dangling conditions. Returns the 'keys' of the deleted matches and added matches. + +Optionally, pass in a map I↠I' which accounts for how the domain of the addition +has been quotiented (due to the match of the rule being non-monic). """ function addition!(stat::IncCCStatic, runt::IncCCRuntime, constr::IncConstraints, - r::ACSetTransformation, rmap::ACSetTransformation, update::ACSetTransformation) + r::Hom, rmap::Hom, + update::Hom, i_i′=nothing) invalidated_keys = Pair{Int,Int}[] # Push forward old matches @@ -153,13 +160,14 @@ function addition!(stat::IncCCStatic, runt::IncCCRuntime, constr::IncConstraints # Find newly-introduced matches Ob = ob(acset_schema(pattern(stat))) - X, L = codom(rmap), pattern(stat) - new_matches, new_keys = Dict{Int, ACSetTransformation}(), Pair{Int, Int}[] + X, L, I = codom(rmap), pattern(stat), dom(r) + i_i′ = isnothing(i_i′) ? id(I) : i_i′ + new_matches, new_keys = Dict{Int, Hom}(), Pair{Int, Int}[] push!(runt.match_vect, new_matches) strictly_old_stuff = Dict(o => setdiff(parts(X,o), collect(rmap[o])) for o in Ob) seen_constraints = Set() # non-monic match can identify different subobjects - for (subL, mapR) = stat.overlaps[r] + for (subL, mapR) in stat.overlaps[r][i_i′] initial = extend_morphism_constraints(mapR⋅rmap, subL) # make it commute (isnothing(initial) || initial ∈ seen_constraints) && continue push!(seen_constraints, initial) @@ -180,7 +188,7 @@ function addition!(stat::IncCCStatic, runt::IncCCRuntime, constr::IncConstraints # Find new matches unlocked by PAC for pac in constr.pac P = codom(pac) - for overlap in pac.overlaps[r] + for overlap in pac.overlaps[r][i_i′] to_P = left(overlap) ⋅ pac.m_complement to_R = right(overlap) ⋅ rmap initial = extend_morphism_constraints(to_R, to_P) @@ -223,11 +231,11 @@ nothing, it contains the morphism `L ↢ I` that was used in POC. Returns the 'keys' of the deleted matches and added matches. """ function deletion!(::IncCCStatic, runt::IncCCRuntime, constr::IncConstraints, - f::ACSetTransformation; dpo=nothing) + f::Hom; dpo=nothing) X = codom(f) # Initialize variables invalidated_keys, new_keys = Pair{Int,Int}[], Pair{Int,Int}[] - new_matches = Dict{Int, ACSetTransformation}() + new_matches = Dict{Int, Hom}() push!(runt.match_vect, new_matches) # Check special short circuit case when f is identity @@ -272,7 +280,7 @@ General method for discovering the newly added homs that arise from deleting some part of the world due to a NAC. """ function new_nac_homs!(runt::IncCCRuntime, constr::IncConstraints, nac::NAC, - f::ACSetTransformation, new_keys, new_matches, + f::Hom, new_keys, new_matches, X_nondeleted::Dict{Symbol, Set{Int}}) N, X = codom(nac), codom(f) Ob = ob(acset_schema(N)) @@ -304,7 +312,7 @@ the NAC to access a complete set of overlaps L ↢ O → N that send *some* part of N/L to some part of L/I. """ function new_nac_dpo!(runt::IncCCRuntime, constr::IncConstraints, nac::NAC, - f::ACSetTransformation, dpo, new_keys, new_matches, + f::Hom, dpo, new_keys, new_matches, X_nondeleted::Dict{Symbol, Set{Int}}) N, X, (l, match) = codom(nac), codom(f), dpo overlaps, Ob, seen = nac[l], ob(acset_schema(N)), Set{Dict}() @@ -333,7 +341,7 @@ end """Add a match during a deletion""" function add_match!(runt::IncCCRuntime, constr::IncConstraints, - new_keys, new_matches, m::ACSetTransformation) + new_keys, new_matches, m::Hom) # check if we've already seen it and that it satifies constraints if m ∉ values(new_matches) && can_match(constr, m) new_key = length(runt) => length(new_keys)+1 diff --git a/src/incremental/IncrementalConstraints.jl b/src/incremental/IncrementalConstraints.jl index 82133c4..cb73ca1 100644 --- a/src/incremental/IncrementalConstraints.jl +++ b/src/incremental/IncrementalConstraints.jl @@ -91,16 +91,18 @@ NAC(m::ACSetTransformation, b::Bool=false, dpo=[]) = A positive application condition L -> P means a match L -> X is valid only if there does not exist a commuting triangle. -When we add something via some addition: O -> R, this could activate hitherto +When we add something via some addition: I -> R, this could activate hitherto invalid matches which were blocked by a PAC. To detect these incrementally, we cache overlaps (indexed by possible additions) that store the ways in which the -addition could intersect with P. +addition could intersect with P. Just like with regular incremental additions, +we consider that I may have been quotiented, I ↠ I', and thus we parameterize +our overlaps by this. """ @struct_hash_equal struct PAC <: AC m::ACSetTransformation monic::Union{Bool, Vector{Symbol}} m_complement::ACSetTransformation - overlaps::Dict{ACSetTransformation, Vector{Span}} + overlaps::Dict{ACSetTransformation, Dict{ACSetTransformation,Vector{Span}}} function PAC(m::ACSetTransformation, additions::Vector{<:ACSetTransformation}, monic::Vector{Symbol}) newP = hom(~Subobject(m)) diff --git a/test/Project.toml b/test/Project.toml index 3c3089d..ed17c59 100644 --- a/test/Project.toml +++ b/test/Project.toml @@ -1,4 +1,5 @@ [deps] +ACSets = "227ef7b5-1206-438b-ac65-934d6da304b8" AlgebraicRewriting = "725a01d3-f174-5bbd-84e1-b9417bad95d9" Catlab = "134e5e36-593f-5add-ad60-77f754baafbe" DataMigrations = "0c4ad18d-0c49-4bc2-90d5-5bca8f00d6ae" @@ -9,3 +10,4 @@ Random = "9a3f8284-a2c9-5f02-9a11-845980a1fd5c" Revise = "295af30f-e4ad-537b-8983-00126c2a3abe" StructEquality = "6ec83bb0-ed9f-11e9-3b4c-2b04cb4e219c" Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40" +nauty_jll = "55c6dc9b-343a-50ca-8ff2-b71adb3733d5" diff --git a/test/incremental/Algorithms.jl b/test/incremental/Algorithms.jl index f71b037..9223555 100644 --- a/test/incremental/Algorithms.jl +++ b/test/incremental/Algorithms.jl @@ -4,7 +4,35 @@ using Test using Catlab using AlgebraicRewriting.Incremental.Algorithms: connected_acset_components, all_subobjects, subobject_cache, - to_subobj, deattr + to_subobj, deattr, all_epis + +# Test all_epis +#-------------- +@present SchF(FreeSchema) begin (A,B)::Ob; f::Hom(A,B)end +@acset_type Fun(SchF) + +X = @acset Fun begin A=3; B=3; f=[1,1,2] end +r = all_epis(X) + +grph(x::ACSet) = to_graphviz(x; node_labels=true) +grph(x::ACSetTransformation) = to_graphviz(x; node_labels=true) +cmp(x...) = force(compose(x...)) +G = Graph(3) +r = all_epis(G); + +length(r) +length(unique(force.(r))) +unique(force.(r)) +codom.(unique(force.(r))) + +par = @acset Graph begin V=2; E=2; src=1; tgt=2 end +@time r = all_epis(par ⊕ par); + +#println(length(e)) + + +@test length(all_epis(path_graph(Graph, 2))) == 2 +@test length(all_epis(path_graph(Graph, 3))) == 6 # test connected_acset_components #-------------------------------- @@ -33,6 +61,7 @@ G = SymmetricGraph(3) ⊕ cycle_graph(SymmetricGraph, 3) @time x2 = subobject_graph(G)[2]; # should be much longer than all_subobjects @test length(x1) == length(x2) # yet give same result + # Deattr #-------- @test deattr(SchWeightedGraph) == SchGraph diff --git a/test/incremental/IncrementalCC.jl b/test/incremental/IncrementalCC.jl index f0a779f..af96c8b 100644 --- a/test/incremental/IncrementalCC.jl +++ b/test/incremental/IncrementalCC.jl @@ -135,8 +135,6 @@ r = Rule(id(e), to_edge_loop′; AppCond(to_edge_loop′, false; monic=true)]); G = @acset Graph begin V=4; E=4; src=[1,1,2,3]; tgt=[1,2,3,4] end mset = IncHomSet(r, G); -# there is just one 'way' in which apply R unlocks new matches from this PAC -@test length(only(values(mset.constraints.pac[1].overlaps))) == 1 @test length(keys(mset)) == 1 rewrite!(mset, r) @test length(keys(mset)) == 1