diff --git a/src/categorical_algebra/CSets.jl b/src/categorical_algebra/CSets.jl index 4d1e872..09a981c 100644 --- a/src/categorical_algebra/CSets.jl +++ b/src/categorical_algebra/CSets.jl @@ -1,8 +1,8 @@ module CSets export extend_morphism, pushout_complement, can_pushout_complement, dangling_condition, invert_hom, check_pb, - gluing_conditions, extend_morphisms, postcompose_partial, sub_vars, - Migrate, invert_iso, deattr, var_pullback, remove_freevars + gluing_conditions, extend_morphisms, sub_vars, + Migrate, invert_iso, deattr, var_pullback using Catlab, Catlab.Theories using Catlab.CategoricalAlgebra @@ -24,66 +24,6 @@ using StructEquality # Morphism search ################# -""" -Given a span of morphisms, we seek to find morphisms B → C that make a -commuting triangle if possible. - - B - g ↗ ↘ ? - A ⟶ C - f - -Accepts homomorphism search keyword arguments to constrain the Hom(B,C) search. -""" -function extend_morphisms(f::ACSetTransformation, g::ACSetTransformation; - initial=Dict(), kw... - )::Vector{ACSetTransformation} - init = combine_dicts!(extend_morphism_constraints(f,g), initial) - isnothing(init) ? [] : homomorphisms(codom(g), codom(f); initial=init, kw...) -end - -""" -Combine a user-specified initial dict with that generated by constraints -`Initial` could contain vectors or int-keyed dicts as its data for each object. -""" -function combine_dicts!(init, initial) - if isnothing(init) return nothing end - for (k,vs) in collect(initial) - for (i, v) in (vs isa AbstractVector ? enumerate : collect)(vs) - if haskey(init[k], i) - if init[k][i] != v return nothing end - else - init[k][i] = v - end - end - end - return NamedTuple(init) -end - -# default behavior for types that don't explicitly implement `is_isomorphic` -is_isomorphic(x) = is_monic(x) && is_epic(x) # should be upstreamed -""" -Convert a morphism X->A to a morphism L->H using a partial morphism G->H, -if possible. - - A ↩ C → B - ↑ ↑ - X ↩⌜Y - ≅ - -This is a more categorical way to compute `update_agent` but for now will -remain unused unless we want to generalize rewriting schedules beyond ACSet -rewriting. -""" -function postcompose_partial(ACB::Span, XA::ACSetTransformation) - S = acset_schema(dom(XA)) - YX, YC = var_pullback(Cospan(XA, left(ACB))) - if all(o->is_isomorphic(YX[o]), ob(S)) - return invert_iso(YX) ⋅ YC ⋅ right(ACB) - end -end - - """ Invert some (presumed iso) components of an ACSetTransformation (given by s) """ @@ -314,23 +254,6 @@ end # Subobjects ############ -"""Recursively include anything, e.g. and edge includes its vertices """ -function complete_subobj(X::ACSet, sub) - sub = Dict([k=>Set(v) for (k,v) in pairs(sub)]) - S = acset_schema(X) - change = true - while change - change = false - for (f,c,d) in homs(S) - new_d = setdiff(Set(X[collect(sub[c]),f]), sub[d]) - if !isempty(new_d) - change = true - union!(sub[d], new_d) - end - end - end - return Dict([k=>collect(v) for (k,v) in pairs(sub)]) -end """Recursively delete anything, e.g. deleting a vertex deletes its edge""" function cascade_subobj(X::ACSet, sub) sub = Dict([k=>Set(v) for (k,v) in pairs(sub)]) @@ -357,32 +280,52 @@ end """ Given a value for each variable, create a morphism X → X′ which applies the -substitution. We do this via pushout. +substitution. We do this via pushout. + + O --> X where C has AttrVars for `merge` equivalence classes + ↓ and O has only AttrVars (sent to concrete values or eq classes + C in the map to C. -`subs` is a dictionary (keyed by attrtype names) of int-keyed dictionaries +`subs` and `merge` are dictionaries keyed by attrtype names + +`subs` values are int-keyed dictionaries indicating binding, e.g. +`; subs = (Weight = Dict(1 => 3.20, 5 => 2.32), ...)` + +`merge` values are vectors of vectors indicating equivalence classes, e.g. +`; merge = (Weight = [[2,3], [4,6]], ...)` """ -function sub_vars(X::ACSet, subs::AbstractDict) +function sub_vars(X::ACSet, subs::AbstractDict=Dict(), merge::AbstractDict=Dict()) S = acset_schema(X) O, C = [constructor(X)() for _ in 1:2] - ox_, oc_ = Dict(), Dict() + ox_, oc_ = Dict{Symbol, Any}(), Dict{Symbol,Any}() for at in attrtypes(S) d = get(subs, at, Dict()) ox_[at] = AttrVar.(filter(p->p ∈ keys(d) && !(d[p] isa AttrVar), parts(X,at))) - oc_[at] = [d[p.val] for p in ox_[at]] + oc_[at] = Any[d[p.val] for p in ox_[at]] add_parts!(O, at, length(oc_[at])) - end + + for eq in get(merge, at, []) + isempty(eq) && error("Cannot have empty eq class") + c = AttrVar(add_part!(C, at)) + for var in eq + add_part!(O, at) + push!(ox_[at], AttrVar(var)) + push!(oc_[at], c) + end + end + end ox = ACSetTransformation(O,X; ox_...) oc = ACSetTransformation(O,C; oc_...) return first(legs(pushout(ox, oc))) end +# TODO replace with CSetTransformation limit when Catlab 0.16 is released + """ Take an ACSet pullback combinatorially and freely add variables for all attribute subparts. -TODO do var_limit, more generally - This relies on implementation details of `abstract`. """ function var_pullback(c::Cospan{<:StructACSet{S,Ts}}) where {S,Ts} @@ -409,46 +352,6 @@ function var_pullback(c::Cospan{<:StructACSet{S,Ts}}) where {S,Ts} end -""" -We may replace some ... -""" -function remove_freevars(X::StructACSet{S}) where S - X = deepcopy(X) - d = Dict(map(attrtypes(S)) do at - vs = Set{Int}() - for f in attrs(S; to=at, just_names=true) - for v in filter(x->x isa AttrVar, X[f]) - push!(vs, v.val) - end - end - # Get new variable IDs - svs = sort(collect(vs)) - vdict = Dict(v=>k for (k,v) in enumerate(svs)) - n_v = length(vdict) - rem_parts!(X,at, parts(X,at)[n_v+1:end]) - for f in attrs(S; to=at, just_names=true) - for (v,fv) in filter(v_->v_[2] isa AttrVar,collect(enumerate(X[f]))) - X[v,f] = AttrVar(vdict[fv.val]) - end - end - return at => svs - end) - return X => d -end - -function remove_freevars(f::ACSetTransformation; check::Bool=false) - S = acset_schema(dom(f)) - !check || is_natural(f) || error("unnatural freevars input") - X, d = remove_freevars(dom(f)) - comps = Dict{Symbol,Any}(o=>collect(f[o]) for o in ob(S)) - for at in attrtypes(S) - comps[at] = collect(f[at])[d[at]] - end - res = ACSetTransformation(X, codom(f); comps...) - !check || is_natural(res) || error("unnatural freevars output") - return res -end - function deattr(X::StructACSet{S})::AnonACSet where S P = Presentation(FreeSchema) add_generators!(P, Ob(FreeSchema, objects(S)...)) diff --git a/src/rewrite/PBPO.jl b/src/rewrite/PBPO.jl index b2aff90..75790c1 100644 --- a/src/rewrite/PBPO.jl +++ b/src/rewrite/PBPO.jl @@ -6,16 +6,15 @@ import Catlab.CategoricalAlgebra: left, right using Catlab.CategoricalAlgebra.CSets: backtracking_search, abstract_attributes using StructEquality +using DataStructures: DefaultDict +using ACSets.DenseACSets: types, attrtype_type using ..Utils import ..Utils: rewrite_match_maps, get_matches, get_expr_binding_map, AbsRule, ruletype using ..Constraints using ...CategoricalAlgebra -using ...CategoricalAlgebra.CSets: - extend_morphism_constraints, var_pullback, remove_freevars, - combine_dicts! - +using ...CategoricalAlgebra.CSets: extend_morphism_constraints, var_pullback """ l r @@ -89,9 +88,9 @@ function canon(l,r,tl,tk,l′)::PBPORule end """ -PBPO matches consist of *two* morphisms. First, a match L → G and secondly +PBPO matches consist of *two* morphisms. First, a match m: L → G, and secondly a typing G → L′. With attributes, it is not so simple because G has concrete -values for attributes and L′ may have variables. Therefore, we actually the +values for attributes and L′ may have variables. Therefore, we actually change the typing to map out of A, an abstracted version of G (with its attributes replaced by variables). So we lift matches L->G to matches L->A, then search α∈Hom(A,L′). @@ -104,9 +103,9 @@ is set to true. L ⟶ L′ tl - ∀m + m L ⟶ G -tl ↓ ↘a ↑ (abstraction) +tl ↓ ↘a ↑ (abs = partial abstraction. Note `a` is `Labs` in the code.) L′⟵ A α @@ -117,7 +116,7 @@ we can deduce precisely what m is by looking at α. function get_matches(rule::PBPORule, G::ACSet; initial=nothing, α_unique=true, random=false, n=-1, kw...) S = acset_schema(G) - res = [] # Pairs of (m,α) + res = [] # Quadruples of of (m, Labs, abs, α) L = codom(left(rule)) # Process the initial constraints for match morphism and typing morphism @@ -137,54 +136,48 @@ function get_matches(rule::PBPORule, G::ACSet; initial=nothing, m_seen = false # keeps track if α_unique is violated for each new m if all(ac->apply_constraint(ac, m), rule.acs) @debug "m: $([k=>collect(v) for (k,v) in pairs(components(m))])" - # Construct abtract version of G. ab: A->G - ab = abstract_attributes(G) - A = dom(ab) # not completely abstract: fill in where L has concrete attrs - for (a, cd, _) in attrs(S) - for (v, fv) in filter(v_->!(v_[2] isa AttrVar),collect(enumerate(L[a]))) - A[m[cd](v), a] = fv + + # Construct partially-abtract version of G. Labs: L->A and abs: A->G + Labs, abs = partial_abstract(m) + A = codom(Labs) + + # If we have a built in function to deduce the adherence from the match + if !isnothing(rule.adherence) + init = rule.adherence(m) + # Return nothing if failure + if !isnothing(init) + αs = homomorphisms(A, codom(rule.tl); initial=init) + # Also return nothing if the result is not unique + if length(αs) ==1 + push!(res, deepcopy((m, Labs, abs, only(αs)))) + end end - end - ab = remove_freevars(ab) - A = dom(ab) # now with free variables removed - # Construct a:L->A such that m = a;ab - ainit = NamedTuple(Dict(o=>collect(m[o]) for o in ob(S))) - a = only(homomorphisms(L, A; initial=ainit)) - # Search for maps α: A -> L′ such that a;α=tl - init = combine_dicts!(extend_morphism_constraints(rule.tl,a), typinit) - if !isnothing(init) - # If we have a built in function to deduce the adherence from the match - if !isnothing(rule.adherence) - init = rule.adherence(m) # return nothing if failure - if !isnothing(init) - αs = homomorphisms(codom(a), codom(rule.tl); initial=init) - if length(αs) ==1 - push!(res, deepcopy((m,a,ab,only(αs)))) - end - end - else - # Search for adherence morphisms. - backtracking_search(codom(a), codom(rule.tl); initial=init, kw...) do α - @debug "\tα: ", [k=>collect(v) for (k,v) in pairs(components(α))] - strong_match = all(ob(S)) do o - all(parts(A,o)) do i - p1 = preimage(rule.tl[o],α[o](i)) - p2 = preimage(a[o], i) - sort(p1) == sort(p2) - end - end - if strong_match && all(lc -> apply_constraint(lc, α), rule.lcs) - all(is_natural, [m,a,ab,α]) || error("Unnatural match") - if m_seen error("Multiple α for a single match $m") end - @debug "\tSUCCESS" - push!(res, deepcopy((m,a,ab,α))) - m_seen |= α_unique - return length(res) == n - else - @debug "\tFAILURE (strong $strong_match)" - return false + else + # Search for adherence morphisms: A -> L′ + init = extend_morphism_constraints(rule.tl, Labs) + backtracking_search(A, codom(rule.tl); initial=init, kw...) do α + @debug "\tα: ", [k=>collect(v) for (k,v) in pairs(components(α))] + + # Check strong match condition + strong_match = all(types(S)) do o + prt = o ∈ ob(S) ? identity : AttrVar + all(prt.(parts(A,o))) do i + p1 = preimage(rule.tl[o],α[o](i)) + p2 = preimage(Labs[o], i) + p1 == p2 end end + if strong_match && all(lc -> apply_constraint(lc, α), rule.lcs) + all(is_natural, [m, Labs, abs, α]) || error("Unnatural match") + if m_seen error("Multiple α for a single match $m") end + @debug "\tSUCCESS" + push!(res, deepcopy((m, Labs, abs, α))) + m_seen |= α_unique + return length(res) == n + else + @debug "\tFAILURE (strong $strong_match)" + return false + end end end end @@ -193,6 +186,105 @@ function get_matches(rule::PBPORule, G::ACSet; initial=nothing, return res end + +""" +This construction addresses the following problem: ideally when we 'abstract' +an ACSet from X to A->X, maps *into* X, say B->X, can be canonically pulled back +to maps B->A which commute. However, A won't do +here, because there may not even exist any maps B->A. If B has concrete +attributes, then those cannot be sent to an AttrVar in A. Furthermore, if B +has multiple 'references' to an AttrVar (two different edges, each with +AttrVar(1), sent to two different edges with the same atttribute value in X), +then there is no longer a *canonical* place to send AttrVar(1) to in A, as there +is a distinct AttrVar for every single part+attr in X. So we need a construction +which does two things to A->X, starting with a map B->X. 1.) replaces exactly the +variables we need with concrete values in order to allow a map B->A, 2.) quotients +variables in A so that there is exactly one choice for where to send attrvars in +B such that the triangle commutes. + + +Starting with a map L -> G (where G has no AttrVars), +we want the analogous map into a "partially abstracted" version of G that +has concrete attributes replaced with AttrVars *EXCEPT* for those attributes +which are mapped to by concrete attributes of L. Likewise, multiple occurences +of the same variable in L correspond to AttrVars which should be merged in the +partially-abstracted G. + +For example, for a schema with a single Ob and Attr (where all combinatorial +maps are just {1↦1, 2↦2}): + +- L = [AttrVar(1), :foo] +- G = [:bar, :foo, :baz] +- abs(G) = [AttrVar(1), AttrVar(2), AttrVar(3)] +- expected result: [AttrVar(1), :foo, AttrVar(2)] + + L -> Partial_abs(G) + ↓ ↑ + G <- abs(G) + +This function computes the top arrow of this diagram starting with the left +arrow. The bottom arrow is computed by `abstract_attributes` and the right +arrow by `sub_vars`. Furthermore, a map from Partial_abs(G) to G is provided. + +This is the factorization system arising from a coreflective subcategory. + +(see https://ncatlab.org/nlab/show/reflective+factorization+system + and https://blog.algebraicjulia.org/post/2023/06/varacsets/) + +""" +function partial_abstract(lg::ACSetTransformation) + L, G = dom(lg), codom(lg) + S = acset_schema(L) + abs_G = abstract_attributes(G) + A = dom(abs_G) + + # Construct partially-abstracted G + #--------------------------------- + subs = Dict{Symbol,Dict{Int}}() + merges = Dict{Symbol,Vector{Vector{Int}}}() + for at in attrtypes(S) + subdict = Dict{Int, Any}() + mergelist = DefaultDict{Int,Vector{Int}}(()->Int[]) + for (f, o, _) in attrs(S; to=at) + for iₒ in parts(L, o) + var = A[lg[o](iₒ), f].val + val = L[iₒ, f] + if val isa AttrVar + push!(mergelist[val.val], var) + else + subdict[var] = val + end + end + end + subs[at] = subdict + merges[at] = collect(filter(l->!isempty(l), collect(values(mergelist)))) + end + pabs_G = sub_vars(dom(abs_G), subs, merges) + + # Construct maps + #--------------- + prt(o) = o ∈ ob(S) ? identity : AttrVar + T(o) = o ∈ ob(S) ? Int : Union{AttrVar,attrtype_type(L, o)} + + # The quotienting via `sub_vars` means L->PA determined purely by ob components + to_pabs_init = Dict{Symbol,Vector{Int}}(map(ob(S)) do o + o => map(prt(o).(collect(lg[o]))) do i + pabs_G[o](only(preimage(abs_G[o], i))) + end + end) + + from_pabs_comps = Dict(map(types(S)) do o + comp = Vector{T(o)}(map(prt(o).(parts(codom(pabs_G), o))) do Pᵢ + only(unique([abs_G[o](prt(o)(pi)) for pi in preimage(pabs_G[o], Pᵢ)])) + end) + o => comp + end) + + to_pabs = only(homomorphisms(L, codom(pabs_G); initial=to_pabs_init)) + from_pabs = ACSetTransformation(codom(pabs_G), codom(lg); from_pabs_comps...) + ComposablePair(to_pabs, from_pabs) +end + """ r K ----> R diff --git a/src/rewrite/Representable.jl b/src/rewrite/Representable.jl index cf041b3..6186d58 100644 --- a/src/rewrite/Representable.jl +++ b/src/rewrite/Representable.jl @@ -41,7 +41,7 @@ end function yoneda_cache(T::Type,S=nothing; clear=false, cache="cache") S = isnothing(S) ? Presentation(T) : S tname = nameof(T) |> string - cache_dict = Dict{Symbol,Tuple{T,Int}}(Iterators.map(generators(S, :Ob)) do ob + cache_dict = Dict{Symbol,Tuple{T,Int}}(map(generators(S, :Ob)) do ob name = nameof(ob) cache_dir = mkpath(joinpath(cache, "$tname")) path, ipath = joinpath.(cache_dir, ["$name.json", "_id_$name.json"]) diff --git a/src/schedules/Basic.jl b/src/schedules/Basic.jl index 2eaedba..0e35378 100644 --- a/src/schedules/Basic.jl +++ b/src/schedules/Basic.jl @@ -63,7 +63,7 @@ struct Initialize <: AgentBox name::Symbol state::StructACSet in_agent::Union{Nothing,StructACSet} - Initialize(s, in_agent=nothing, n="") = new(n,s,in_agent) + Initialize(s, in_agent=nothing, n=Symbol("")) = new(n,s,in_agent) end input_ports(r::Initialize) = isnothing(r.in_agent) ? [] : [r.in_agent] output_ports(r::Initialize) = [typeof(r.state)()] diff --git a/src/schedules/Wiring.jl b/src/schedules/Wiring.jl index dc59771..6500bc0 100644 --- a/src/schedules/Wiring.jl +++ b/src/schedules/Wiring.jl @@ -35,7 +35,8 @@ Names(;kw...) = Names(Dict([string(k)=>v for (k,v) in pairs(kw)])) Base.getindex(n::Names,s::String) = n.from_name[s] Base.getindex(n::Names,s::Symbol) = n[string(s)] Base.getindex(n::Names,x)::String = get(n.to_name,x,"?") -function Base.setindex(n::Names, x::String, y) +Base.length(n::Names) = length(n.from_name) +function Base.setindex!(n::Names{T}, y::T, x::String) where T n.from_name[x] = y n.to_name[y] = x end @@ -49,11 +50,11 @@ Make a wiring diagram with ob/hom generators using @program macro TODO double check that this does not introduce any wire splitting. """ -function mk_sched(t_args::NamedTuple,args::NamedTuple,names::Names, - kw::Union{NamedTuple,AbstractDict}, wd::Expr) +function mk_sched(t_args::NamedTuple,args::NamedTuple,names::Names{T}, + kw::Union{NamedTuple,AbstractDict}, wd::Expr) where T n_trace=length(t_args) - os = Dict(Symbol(k)=>v for (k,v) in collect(names.from_name)) - hs = Dict(Symbol(k)=>v isa AgentBox ? singleton(v) : v for (k,v) in pairs(kw)) + os = Dict{Symbol, T}(Symbol(k)=>v for (k,v) in collect(names.from_name)) + hs = Dict{Symbol, Schedule}(Symbol(k)=>v isa AgentBox ? singleton(v) : v for (k,v) in pairs(kw)) P = Presentation(TM) os_ = Dict(v=>add_generator!(P, Ob(TM,k)) for (k,v) in collect(os)) @@ -65,7 +66,6 @@ function mk_sched(t_args::NamedTuple,args::NamedTuple,names::Names, add_generator!(P, Hom(k, i, o)) end args_ = Expr(:tuple,[Expr(Symbol("::"), k,v) for (k,v) in pairs(merge(t_args,args))]...) - tmp = parse_wiring_diagram(P, args_, wd) Xports = Ports{ThTracedMonoidalWithBidiagonals}(input_ports(tmp)[1:n_trace]) newer_x = Ob(TM,Xports) # arbitrary gatexpr @@ -95,7 +95,7 @@ function mk_sched(t_args::NamedTuple,args::NamedTuple,names::Names, end new_d = trace(Xports, tmp) - sub = ocompose(new_d, [hs[Symbol(b.value)].d for b in boxes(new_d)]) + sub = ocompose(new_d, WiringDiagram[hs[Symbol(b.value)].d for b in boxes(new_d)]) sub.diagram[:wire_value] = nothing for x in Symbol.(["$(x)_port_type" for x in [:outer_in,:outer_out,]]) sub.diagram[:,x] = [names[v] for v in sub.diagram[x]] @@ -240,4 +240,4 @@ merge_wires(agent::StructACSet, n::Int=2)::Schedule = id(agents::AbstractVector{<:StructACSet}) = id(SPorts(Ports(agents))) -end # module \ No newline at end of file +end # module diff --git a/test/rewrite/PBPO.jl b/test/rewrite/PBPO.jl index c8a2573..fe7bbcd 100644 --- a/test/rewrite/PBPO.jl +++ b/test/rewrite/PBPO.jl @@ -2,7 +2,28 @@ module TestPBPO using Test using AlgebraicRewriting -using Catlab, Catlab.CategoricalAlgebra, Catlab.Graphs, Catlab.Graphics +using Catlab + +using AlgebraicRewriting.Rewrite.PBPO: partial_abstract + +# Partial abstract +################## +const WG = WeightedGraph{Float64} + +L = @acset WG begin + V=1; E=4; Weight=2; src=1; tgt=1; weight=[4.2, AttrVar.([1,1,2])...] +end +G = @acset WG begin V=1; E=5; src=1; tgt=1; weight=[3.1,3.1, 4.2, 6.3, 7.4] end +lg = homomorphism(L,G; initial=(E=[3,2,1,4],)) +abs,pabs = partial_abstract(lg); + +@test all(is_natural, [abs,pabs]) +@test dom(abs) == L +@test codom(pabs) == G +# Test partially-expected result: two variables merged +@test is_isomorphic(codom(abs), @acset(WG, begin + V=1; E=5; Weight=3; src=1; tgt=1; weight=[4.2, AttrVar.([1,1,2,3])...] +end)) # Example from Fig. 7 of "A PBPO+ Graph Rewriting Tutorial" ########################################################### @@ -187,7 +208,6 @@ expected = @acset Graph begin V=3; E=4; src=[1,2,1,2]; tgt=[1,2,2,3] end # Attributed problem #################### -const WG = WeightedGraph{Float64} L = @acset WG begin V=2; E=1; Weight=1; src=1; tgt=2; weight=[AttrVar(1)] end K = WG(2) diff --git a/test/schedules/Eval.jl b/test/schedules/Eval.jl index 597b259..e287ad9 100644 --- a/test/schedules/Eval.jl +++ b/test/schedules/Eval.jl @@ -35,7 +35,9 @@ end z, g1, ar, loop = Graph(), Graph(1), path_graph(Graph, 2), apex(terminal(Graph)) -N=Names(Dict("Z"=>z,"•"=>g1,"•→•"=>ar)) +N=Names(Dict("Z"=>z,"•"=>g1)) +@test length(N) == 2 +N["•→•"] = ar Dot, A = Symbol.([N[g1],N[ar]]) av = RuleApp(:add_vertex, Rule(id(z), create(g1)))