Merge pull request #918 from AlgebraicJulia/bind_kwarg

Monic constraint and `no_bind` kwarg for AttrVars in hom search

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)<nparts(Y,c),epic)  
 
-  if !all(isempty, [iso_failures,mono_failures,epi_failures])
+  if !all(isempty, [iso_failures, mono_failures, epi_failures])
     if !error_failures 
       return false 
     else error("""
@@ -233,6 +239,20 @@ function backtracking_search(f, X::ACSet, Y::ACSet;
       """)
     end
   end
+
+  # Fail if there are "free floating attribute variables"
+  for a_type in attrtypes(S) 
+    a_type ∈ (monic ∪ iso ∪ no_bind) && continue # attrvars ↦ attrvars
+    attrs′ = attrs(S, just_names=true, to=a_type)
+    avars = union(collect.([filter(x->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
 

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] ); 

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
 #-----------