diff --git a/src/categorical_algebra/HomSearch.jl b/src/categorical_algebra/HomSearch.jl index acc8f23f4..d530474ba 100644 --- a/src/categorical_algebra/HomSearch.jl +++ b/src/categorical_algebra/HomSearch.jl @@ -68,22 +68,32 @@ that the vertex map is injective but imposes no constraints on the edge map. To restrict the homomorphism to a given partial assignment, set the keyword argument `initial`. For example, to fix the first source vertex to the third -target vertex in a graph homomorphism, set `initial=(V=Dict(1 => 3),)`. Use -the keyword argument `type_components` to specify nontrivial components on -attribute types for a loose homomorphism. These components must be callable: -either Julia functions on the appropriate types or FinFunction(Dict(...)). +target vertex in a graph homomorphism, set `initial=(V=Dict(1 => 3),)`. Use the +keyword argument `type_components` to specify nontrivial components on attribute +types for a loose homomorphism. These components must be callable: either Julia +functions on the appropriate types or FinFunction(Dict(...)). Use the keyword argument `alg` to set the homomorphism-finding algorithm. By default, a backtracking search algorithm is used ([`BacktrackingSearch`](@ref)). -Use the keyword argument error_failures = true to get errors explaining -any immediate inconsistencies in specified initial data. +Use the keyword argument error_failures = true to get errors explaining any +immediate inconsistencies in specified initial data. -The keyword `predicates` accepts a Dict{Ob, Dict{Int, Union{Nothing, AbstractVector{Int}}}} -For each part of the domain, we have the option to give a constraint as a -boolean function of the current assignment and tentative value to assign. E.g. -`predicates = (E = Dict(2 => [2,4,6]))` would only find matches +The keyword `predicates` accepts a Dict{Ob, Dict{Int, Union{Nothing, +AbstractVector{Int}}}} For each part of the domain, we have the option to give a +constraint as a boolean function of the current assignment and tentative value +to assign. E.g. `predicates = (E = Dict(2 => [2,4,6]))` would only find matches which assigned edge#2 to edge #2, #4, or #6 in the codomain. +The keyword `no_bind` can be a boolean (applying to all AttrTypes) or an +iterable of specific components: it prevents attribute variables in the domain +from being sent to concrete values in the codomain. When the AttrType component +is `monic`, it is also the case that attribute variables cannot be sent to +concrete values (therefore it is redundant to set `no_bind=true` in such cases). +In both of these cases, it's possible to compute homomorphisms when there are +"free-floating" attribute variables (which are not referred to by any Attr in +the domain), as each such variable has a finite number of possibilities for it +to be mapped to. + See also: [`homomorphisms`](@ref), [`isomorphism`](@ref). """ homomorphism(X::ACSet, Y::ACSet; alg=BacktrackingSearch(), kw...) = @@ -193,20 +203,12 @@ end function backtracking_search(f, X::ACSet, Y::ACSet; monic=false, epic=false, iso=false, random=false, predicates=(;), - type_components=(;), initial=(;), error_failures=false) + type_components=(;), initial=(;), error_failures=false, no_bind=false) S, Sy = acset_schema.([X,Y]) S == Sy || error("Schemas must match for morphism search") Ob = Tuple(objects(S)) Attr = Tuple(attrtypes(S)) ObAttr = Tuple(objects(S) ∪ attrtypes(S)) - # Fail if there are "free floating attribute variables" - all(attrtypes(S)) do a_type - ats = attrs(S, just_names=true, to=a_type) - avs = collect.([filter(x->x isa AttrVar, X[f]) for f in ats]) - pa = partial_assignments(get(initial, a_type, []); is_attr=true) - initkeys = AttrVar.(keys(collect(pa))) - length(unique(vcat(initkeys, avs...))) == nparts(X, a_type) - end || error("Cannot search for morphisms with free-floating variables") # Fail early if no monic/isos exist on cardinality grounds. if iso isa Bool @@ -218,11 +220,15 @@ function backtracking_search(f, X::ACSet, Y::ACSet; if epic isa Bool epic = epic ? Ob : () end + if no_bind isa Bool + no_bind = no_bind ? Attr : () + end + iso_failures = Iterators.filter(c->nparts(X,c)!=nparts(Y,c),iso) mono_failures = Iterators.filter(c->nparts(X,c)>nparts(Y,c),monic) epi_failures = Iterators.filter(c->nparts(X,c)x isa AttrVar, X[f]) for f in attrs′])...) + assigned = partial_assignments(get(initial, a_type, []); is_attr=true) + assigned′ = first.(collect(assigned)) + unassigned = setdiff(parts(X, a_type), [v.val for v in avars] ∪ assigned′) + if !isempty(unassigned) + error("Cannot search for morphisms with free-floating variables: $unassigned") + end + end + # Injections between finite sets of the same size are bijections, so reduce to that case. monic = unique([iso..., monic...]) @@ -296,9 +316,32 @@ function backtracking_search(f, state::BacktrackingState, depth::Int; else S = acset_schema(state.dom) od = Dict{Symbol,Vector{Int}}(k=>(state.assignment[k]) for k in objects(S)) - ad = Dict(k=>last.(state.assignment[k]) for k in attrtypes(S)) - comps = merge(NamedTuple(od),NamedTuple(ad)) - return f(ACSetTransformation(comps, state.dom, state.codom)) + + # Compute possible assignments for all free variables + free_data = map(attrtypes(S)) do k + monic = !isnothing(state.inv_assignment[k]) + assigned = [v.val for (_, v) in state.assignment[k] if v isa AttrVar] + valid_targets = setdiff(parts(state.codom, k), monic ? assigned : []) + free_vars = findall(==(AttrVar(0)), last.(state.assignment[k])) + N = length(free_vars) + prod_iter = Iterators.product(fill(valid_targets, N)...) + if monic + prod_iter = Iterators.filter(x->length(x)==length(unique(x)), prod_iter) + end + (free_vars, prod_iter) # prod_iter = valid assignments for this attrtype + end + + # Homomorphism for each element in the product of the prod_iters + for combo in Iterators.product(last.(free_data)...) + ad = Dict(map(zip(attrtypes(S), first.(free_data), combo)) do (k, xs, vs) + vec = last.(state.assignment[k]) + vec[xs] = AttrVar.(collect(vs)) + k => vec + end) + comps = merge(NamedTuple(od),NamedTuple(ad)) + f(ACSetTransformation(comps, state.dom, state.codom)) + end + return false end elseif mrv == 0 # An element has no allowable assignment, so we must backtrack. @@ -401,16 +444,24 @@ assign_elem!(state::BacktrackingState{<:DynamicACSet}, depth, c, x, y) = state.unassigned[@ct c][1] -= 1 end - @ct_ctrl for (f,_,d) in attrs(S; from=c) - if subpart(X,x,@ct(f)) isa AttrVar - v = subpart(X,x,@ct(f)).val - xcount,_ = state.assignment[@ct d][v] - state.assignment[@ct d][v] = xcount+1 => subpart(Y,y,@ct(f)) + # Enforce naturality for all attrs, e.g. assigning an edge fixes its weight + @ct_ctrl for (f, _, d) in attrs(S; from=c) + if subpart(X, x, @ct(f)) isa AttrVar + v = subpart(X, x, @ct(f)).val + xcount, _ = state.assignment[@ct d][v] + Yf = subpart(Y, y, @ct(f)) + invD = state.inv_assignment[@ct d] + state.assignment[@ct d][v] = xcount+1 => Yf + if !isnothing(invD) + (Yf isa AttrVar && invD[Yf.val] ∈ [0, v]) || return false + invD[Yf.val] = v + end end end @ct_ctrl for (f, _, d) in homs(S; from=c) - assign_elem!(state, depth, @ct(d), subpart(X,x,@ct f),subpart(Y,y,@ct f)) || return false + assign_elem!(state, depth, @ct(d), subpart(X, x, @ct f), + subpart(Y, y, @ct f)) || return false end return true end @@ -442,6 +493,11 @@ unassign_elem!(state::BacktrackingState{<:DynamicACSet}, depth, c, x) = v = subpart(X,x,@ct(f)).val n, αv = state.assignment[@ct(d)][v] state.assignment[@ct(d)][v]= (n-1 => αv) + invD = state.inv_assignment[@ct d] + # Reset inv assignment if it's we're unsetting last reference + if n == 1 && αv isa AttrVar && !isnothing(invD) && invD[αv.val] == v + invD[αv.val] = 0 + end end end diff --git a/test/categorical_algebra/Chase.jl b/test/categorical_algebra/Chase.jl index 544b71c99..76d1ad4da 100644 --- a/test/categorical_algebra/Chase.jl +++ b/test/categorical_algebra/Chase.jl @@ -115,9 +115,9 @@ add_parts!(unique_l,:X,3); add_parts!(unique_l,:x,2;src_x=[1,1],tgt_x=[2,3]); add_parts!(unique_r,:X,2); add_part!(unique_r,:x;src_x=1,tgt_x=2); -ED_unique = homomorphism(unique_l, unique_r) +ED_unique = only(homomorphisms(unique_l, unique_r)) add_part!(total_l,:X) -ED_total = homomorphism(total_l, unique_r) +ED_total = ACSetTransformation(total_l, unique_r; X=[1]) # x-path of length 3 = x-path of length 2 add_parts!(three_two_l,:X,6); add_parts!(three_two_l,:x,5; src_x=[1,2,3,1,5],tgt_x=[2,3,4,5,6] ); diff --git a/test/categorical_algebra/HomSearch.jl b/test/categorical_algebra/HomSearch.jl index 4958ffedf..9483fa950 100644 --- a/test/categorical_algebra/HomSearch.jl +++ b/test/categorical_algebra/HomSearch.jl @@ -142,6 +142,46 @@ rand_hs = homomorphisms(K₆,K₆; random=true) @test hs != rand_hs # not equal given order @test homomorphism(K₆,K₆) != homomorphism(K₆,K₆;random=true) +# AttrVar constraints (monic and no_bind) +#---------------------------------------- +@present SchLSet(FreeSchema) begin X::Ob; D::AttrType; f::Attr(X,D) end +@acset_type LSet(SchLSet){Symbol} + +# Simple example +A = @acset LSet begin X=2; D=2; f=AttrVar.(1:2) end +B = @acset LSet begin X=1; D=1; f=[AttrVar(1)] end +@test isempty(homomorphisms(A, B; monic=[:D])) +@test length(homomorphisms(B, A; monic=[:D])) == 2 +@test length(homomorphisms(A, A; monic=[:D])) == 2 + +# More complicated example +G = @acset LSet begin X=3; D=2; f=[:a; AttrVar.(1:2)] end +H = @acset LSet begin X=4; D=3; f=[:a, :b, AttrVar.(1:2)...] end + +# X₂ and X₃ in G can go to any of the 4 Xs in H +@test length(homomorphisms(G, H)) == 16 + +G′ = copy(G) +add_part!(G′, :D) # add a free floating variable to domain + +# If we don't put any constraints on the free var, error b/c of infinite homs +@test_throws ErrorException homomorphisms(G′, H) + +# All attrvars going to :b forces all Xs going to X₂ +@test length(homomorphisms(G′, H; initial=(D=[:b,:b,:b],),)) == 1 + +# If we just force the free variable to go to a fixed place, it's the same as before +@test length(homomorphisms(G′, H; initial=(D=Dict(3=>:b),))) == 16 +@test length(homomorphisms(G′, H; initial=(D=Dict(3=>AttrVar(1)),))) == 16 + +# [2,1] and [1,2] for where AttrVars go +@test length(homomorphisms(G, H; monic=[:D])) == 2 +# free var forced to go to D₃ +@test length(homomorphisms(G′, H; monic=[:D])) == 2 +# D₁ D₂ go to any of the 4 Xs. D₃ goes to any of the 3 Ds +@test length(homomorphisms(G′, H; no_bind=[:D])) == 4*4*3 + + # As a macro #-----------