New pushout complement for AttrVars

docs/literate/lotka_volterra.jl

@@ -7,13 +7,14 @@ We start with importing some libraries.
 =#
 
 using Catlab, DataMigrations, AlgebraicRewriting
-using Random, Test, StructEquality
-using Luxor
+using Random, Test
+using Luxor # optional: makes the sequence of images via `view_traj` at the end
 
 using Catlab.Graphics.Graphviz: Attributes, Statement, Node
 using Catlab.Graphics.Graphviz
 
 const hom = homomorphism
+
 Random.seed!(123);
 
 # # Ontology
@@ -335,11 +336,10 @@ view_sched(par_sched; names=N)
 
 # #### Test rotation
 begin
-  ex = @acset_colim yLV begin 
-    e::E
-    s::Sheep
-    sheep_loc(s) == src(e)
-    sheep_dir(s) == :N
+  ex = @acset LV begin 
+    E=1; Sheep=1; V=2
+    src=1; tgt=2; dir=:W; countdown = [0, 0]
+    sheep_loc=1; sheep_eng=100; sheep_dir=:N
   end;
 
   expected = copy(ex); 
@@ -381,19 +381,16 @@ sheep_fwd = tryrule(RuleApp(:move_fwd, sheep_fwd_rule,
 
 # #### Moving forward test
 
-begin # test 
-  ex = @acset_colim yLV begin
-    (e1, e2)::E; s::Sheep
-    sheep_loc(s) == tgt(e1); tgt(e1) == src(e2)
-    sheep_dir(s) == :N; dir(e1) == :N; dir(e2) == :N
-    sheep_eng(s) == 10
-  end
-  expected = @acset_colim yLV begin
-    (e1, e2)::E; s::Sheep
-    sheep_loc(s) == tgt(e2); tgt(e1) == src(e2)
-    sheep_dir(s) == :N; dir(e1) == :N; dir(e2) == :N
-    sheep_eng(s) == 9
+begin
+  ex = @acset LV begin
+    V=3; E=2; Sheep=1; 
+    countdown=[0,0,0]
+    src=[1,2]; tgt=[2,3]; dir=[:N,:W]
+    sheep_loc=1; sheep_dir=:N; sheep_eng = 10
   end
+  expected = copy(ex); 
+  expected[:sheep_loc] = 2
+  expected[:sheep_eng] = 9
   @test is_isomorphic(expected, rewrite(sheep_fwd_rule, ex))
   rewrite!(sheep_fwd_rule, ex)
   @test is_isomorphic(ex, expected)
@@ -409,18 +406,17 @@ se_rule = Rule(S; expr=(Eng=[vs -> vs[1] + 4, vs -> 30],),
 sheep_eat = tryrule(RuleApp(:Sheep_eat, se_rule, S));
 
 # #### Sheep eating test
-begin 
-  ex = @acset_colim yLV begin
-    s::Sheep; e::E
-    sheep_loc(s) == tgt(e); sheep_eng(s) == 3
-    countdown(tgt(e)) == 0; countdown(src(e)) == 10
-  end
-  expected = @acset_colim yLV begin
-    s::Sheep; e::E
-    sheep_loc(s) == tgt(e); sheep_eng(s) == 7
-    countdown(tgt(e)) == 30; countdown(src(e)) == 10
+begin
+  ex = @acset LV begin
+    E=1; V=2; Sheep=1; 
+    src=1; tgt=2; dir=:S; countdown=[10, 0]
+    sheep_loc = 2; sheep_eng = 3; sheep_dir=:W
   end
 
+  expected = copy(ex)
+  expected[2,:countdown] = 30
+  expected[1,:sheep_eng] = 7
+
   @test is_isomorphic(expected, rewrite(se_rule, ex))
   rewrite!(se_rule, ex)
   @test is_isomorphic(ex, expected)
@@ -442,17 +438,15 @@ wolf_eat = tryrule(RuleApp(:Wolf_eat, we_rule, W));
 begin
   ex = @acset LV begin 
     Sheep=1; Wolf=1; V=3; E=2; 
-    src=[1,2]; tgt=[2,3];
-    countdown=[9,10,11]; dir=[:N,:N]; 
+    src=[1,2]; tgt=[2,3]; countdown=[9,10,11]; dir=[:N,:N]; 
     sheep_loc=2; sheep_eng=[3]; sheep_dir=[:N]
     wolf_loc=[2];  wolf_eng=[16];  wolf_dir=[:S]
   end
-  expected = @acset LV begin 
-    Wolf=1; V=3; E=2; 
-    src=[1,2]; tgt=[2,3]; 
-    countdown=[9,10,11];  dir=[:N,:N]; 
-    wolf_loc=[2]; wolf_eng=[36]; wolf_dir=[:S]
-  end
+
+  expected = copy(ex)
+  expected[1, :wolf_eng] = 36
+  rem_part!(expected, :Sheep, 1)
+
   @test is_isomorphic(rewrite(we_rule,ex), expected)
   rewrite!(we_rule, ex)
   @test is_isomorphic(ex,expected)
@@ -469,13 +463,16 @@ sheep_starve = (RuleApp(:starve, sheep_die_rule,
 
 # #### Sheep starvation test
 
-begin # test
-  compile_rewrite(sheep_die_rule)
-  ex = @acset_colim yLV begin 
-    s::Sheep; w::Wolf
-    sheep_eng(s) == 0; sheep_dir(s) == :W
+begin
+  ex = @acset LV begin 
+    V=1; Sheep=1; Wolf=1
+    countdown=20;
+    sheep_loc=1; sheep_eng=0; sheep_dir=:W
+    wolf_loc=1; wolf_eng=10; wolf_dir=:S
   end
-  expected = @acset_colim yLV begin v::V; w::Wolf end
+  expected = copy(ex)
+  rem_part!(expected, :Sheep, 1)
+
   @test is_isomorphic(rewrite(sheep_die_rule,ex), expected)
   rewrite!(sheep_die_rule,ex)
   @test is_isomorphic(ex, expected)
@@ -501,16 +498,19 @@ sheep_reprod = RuleApp(:reproduce, sheep_reprod_rule,
 # #### Reproduction test
 
 begin # test
-  ex = @acset_colim yLV begin 
-    s::Sheep; w::Wolf; sheep_eng(s) == 10; sheep_dir(s) == :W 
-  end
-  expected = @acset_colim yLV  begin 
-    (s1,s2)::Sheep; w::Wolf;
-    sheep_loc(s1) == sheep_loc(s2)
-    sheep_dir(s1) == sheep_dir(s2)
-    sheep_eng(s1) == sheep_eng(s2)
-    sheep_dir(s1) == :W; sheep_eng(s1) == 5;
+  ex = @acset LV begin 
+    Sheep=1; Wolf=1; V=2; 
+    countdown=[20,30]
+    sheep_loc=1; sheep_eng=10; sheep_dir=:W 
+    wolf_loc=2; wolf_eng=5; wolf_dir=:N
   end
+
+  expected = copy(ex)
+  add_part!(expected,:Sheep)
+  expected[:sheep_eng] = [5, 5]
+  expected[:sheep_loc] = [1, 1]
+  expected[:sheep_dir] = [:W, :W]
+
   @test is_isomorphic(rewrite(sheep_reprod_rule,ex),expected)
   rewrite!(sheep_reprod_rule,ex)
   @test is_isomorphic(ex, expected)

src/categorical_algebra/CSets.jl

@@ -9,7 +9,7 @@
 using Catlab
 using Catlab.CategoricalAlgebra.FinSets: IdentityFunction, VarSet
 using Catlab.CategoricalAlgebra.Chase: extend_morphism, extend_morphism_constraints
-using Catlab.CategoricalAlgebra.CSets: unpack_diagram, type_components, abstract_attributes
+using Catlab.CategoricalAlgebra.CSets: unpack_diagram, type_components, abstract_attributes, var_reference
 import ..FinSets: pushout_complement, can_pushout_complement, id_condition
 import ACSets: acset_schema
 import Catlab.CategoricalAlgebra.FinSets: predicate
@@ -19,7 +19,7 @@
 using ACSets.DenseACSets: attrtype_type, datatypes, constructor
 import ACSets: sparsify
 import Base: getindex
-using DataStructures: OrderedSet
+using DataStructures: OrderedSet, DefaultDict, IntDisjointSets, find_root!
 using StructEquality
 
 # Morphism search 
@@ -100,6 +100,47 @@
   end 
 end
 
+# Non-monotonicity
+##################
+
+"""
+Every morphism induces a partition of the parts of the domain. This function 
+finds every nontrivial partition (size greater than one element) for the objects
+of the schema.
+"""
+fibers(f::ACSetTransformation) = 
+  Dict(o => fibers(f[o]) for o in ob(acset_schema(dom(f))))
+
+function fibers(f::FinFunction)
+  dic = DefaultDict{Int,Vector{Int}}(()->Int[])
+  for v in dom(f)
+    push!(dic[f(v)], v)
+  end
+  filter(xs->length(xs)>1, collect(values(dic)))
+end
+
+unions!(i::IntDisjointSets, xs::Vector{Int}) = if length(xs) > 1 
+  [union!(i, x, y) for (x,y) in zip(xs, xs[2:end])]
+end
+
+getvalue(a::AttrVar) = a.val
+
+"""Further induced equations between AttrVars, given a specific match morphism"""
+function var_eqs(l::ACSetTransformation, m::ACSetTransformation)
+  I, L = dom(l), codom(l)
+  S = acset_schema(L)
+  eq_I = Dict(a => IntDisjointSets(nparts(I, a)) for a in attrtypes(S))
+  for (o, xss) in pairs(fibers(m)) # match induces equivalence of ob parts in L
+    for xsₗ in xss
+      xsᵢ = Vector{Int}(vcat(preimage.(Ref(l[o]), xsₗ)...))
+      for (f, _, at) in attrs(S; from=o)
+        unions!(eq_I[at], getvalue.(filter(x -> x isa AttrVar, I[xsᵢ, f])))
+      end
+    end
+  end
+  return eq_I
+end
+
 # Pushout complement
 ####################
 
@@ -111,45 +152,53 @@
 C-set will be only partially defined. To check all these conditions in advance,
 use the function [`can_pushout_complement`](@ref).
 
-Because Subobject does not work well with AttrVars, a correction is made
+In the absence of AttrVars, K is a subobject of G. But we want to be able to 
+change the value of attributes. So any variables in I are not concretized by 
+the I->K map. However, AttrVars may be merged together if `m: L -> G` merges 
+parts together.
 """
 function pushout_complement(pair::ComposablePair{<:ACSet, <:TightACSetTransformation})
-  p1,p2 = pair 
-  I,G = dom(p1), codom(p2)
+  l, m = pair 
+  I, G = dom(l), codom(m)
   S = acset_schema(I)
+  all(at->nparts(G, at)==0, attrtypes(S)) || error("Cannot rewrite with AttrVars in G")
   # Compute pushout complements pointwise in FinSet.
-  components = NamedTuple(Dict([o=>pushout_complement(ComposablePair(p1[o],p2[o])) 
-                                for o in types(S)]))
-  k_components, g_components = map(first, components), map(last, components)
+  components = NamedTuple(Dict(map(ob(S)) do o 
+      o => pushout_complement(ComposablePair(l[o], m[o]))
+  end))
+  k_components = Dict{Symbol,Any}(pairs(map(first, components)))
+  g_components = Dict{Symbol,Any}(pairs(map(last, components)))
 
   # Reassemble components into natural transformations.
-  g = hom(Subobject(G, NamedTuple(Dict(o=>g_components[o] for o in ob(S)))))
+  g = hom(Subobject(G, NamedTuple(Dict(o => g_components[o] for o in ob(S)))))
   K = dom(g)
-
-  for at in attrtypes(S)
-    add_parts!(K, at, codom(k_components[at]).n)
-  end
 
-  for (a, d, at) in attrs(S)
-    # force k to be natural
-    for p in parts(I, d)
-      K[k_components[d](p),a] = k_components[at](I[p, a])
-    end
-    # force g to be natural 
-    for p in parts(K, d)
-      gval = G[g_components[d](p), a]
-      preim = preimage(g_components[at], gval)
-      if !isempty(preim) && gval isa AttrVar
-        K[p,a] = AttrVar(only(preim))
+  var_eq = var_eqs(l, m) # equivalence class of attrvars
+
+  for at in attrtypes(S)
+    eq = var_eq[at]
+    roots = unique(find_root!.(Ref(eq), 1:length(eq)))
+    add_parts!(K, at, length(roots))
+    k_components[at] = map(parts(I, at)) do pᵢ
+      attrvar = AttrVar(findfirst(==(find_root!(eq, pᵢ)), roots))
+      for (a, d, _) in attrs(S; to=at)
+        for p in incident(I, AttrVar(pᵢ), a)
+          K[k_components[d](p), a] = attrvar
+        end
       end
+      attrvar
     end
-  end 
+    T = Union{AttrVar, attrtype_type(G, at)}
+    g_components[at] = Vector{T}(map(parts(K, at)) do v
+      f, o, val = var_reference(K, at, v)
+      G[g_components[o](val), f]
+    end)
+  end
 
   k = ACSetTransformation(I, K; k_components...)
   g = ACSetTransformation(K, G; g_components...)
-
-  force(compose(k,g)) == force(compose(p1,p2)) || error("Square doesn't commute")
-  is_natural(k) || error("k unnatural")
+  force(compose(k,g)) == force(compose(l, m)) || error("Square doesn't commute")
+  is_natural(k) || error("k unnatural $k")
   is_natural(g) || error("g unnatural")
   return ComposablePair(k, g)
 end
@@ -261,16 +310,6 @@
   results
 end
 
-# n_src = parts(codom(m), @ct(src_obj)) # BIG
-# unmatched_vals = setdiff(n_src, collect(m[@ct(src_obj)]))
-# unmatched_tgt = [codom(m)[x,@ct(morph)] for x in unmatched_vals]
-# for unmatched_val in setdiff(n_src, collect(m[@ct(src_obj)]))  # G/m(L) src
-#   unmatched_tgt = codom(m)[unmatched_val,@ct morph]
-#   if unmatched_tgt in dels[@ct(tgt_obj)]
-#     push!(results, (@ct(morph), unmatched_val, unmatched_tgt))
-#   end
-# end
-
 # Subobjects
 ############
 

src/categorical_algebra/FinSets.jl

@@ -46,37 +46,6 @@ function pushout_complement(pair::ComposablePair{<:FinSet{Int}})
   return ComposablePair(k, g)
 end
 
-"""
-This may not be the actual pushout complement in the relevant (Kleisli) category
-
-      l
-    L ← I
-  m ↓   ↓ k
-    G ← K
-      g
-
-"""
-function pushout_complement(pair::ComposablePair{<:VarSet{T}}) where {T}
-  l, m = pair
-  lm = compose(l,m)
-  I, G = dom(l), codom(m)
-  # Initialize I -> K with image of composite l⋅m
-  image_lm = unique([lm(AttrVar(i)) for i in I])
-
-  # Additionally, any vars not matched by m should be matched by g
-  unmatched = setdiff(AttrVar.(G), collect(m))
-  K = FinSet(length(image_lm) + length(unmatched))
-
-  # Construct I -> K 
-  ik = VarFunction{T}([AttrVar(findfirst(==(lm(AttrVar(i))), image_lm)) 
-                       for i in I], FinSet(length(K)))
-  # Construct K -> G 
-  kg = VarFunction{T}(Union{T,AttrVar}[
-    [lm(AttrVar(findfirst(==(AttrVar(k)), collect(ik)))) 
-     for k in 1:length(image_lm)]..., unmatched...], FinSet(length(G)))
-  return ComposablePair(ik, kg)
-end
-
 can_pushout_complement(pair::ComposablePair{<:FinSet{Int}}) =
   all(isempty, id_condition(pair))