Merge pull request #80 from AlgebraicJulia/SPO_delete_NAC

Fix new_nac_homs

Project.toml

@@ -2,7 +2,7 @@ name = "AlgebraicRewriting"
 uuid = "725a01d3-f174-5bbd-84e1-b9417bad95d9"
 license = "MIT"
 authors = ["Kris Brown <[email protected]>"]
-version = "0.4.0"
+version = "0.4.1"
 
 [deps]
 ACSets = "227ef7b5-1206-438b-ac65-934d6da304b8"

benchmark/Agents.jl

@@ -278,7 +278,7 @@ sheep_fwd = tryrule(RuleApp(:move_fwd, sheep_fwd_rule,
 s_eat_pac = @acset_colim yWS begin s::Sheep; countdown(sheep_loc(s)) == 0 end
 
 se_rule = Rule(S; expr=(Eng=[vs -> vs[1] + 4, vs -> 30],),
-               ac=[AppCond(hom(S, s_eat_pac))])
+               ac=[PAC(hom(S, s_eat_pac))])
 sheep_eat = tryrule(RuleApp(:Sheep_eat, se_rule, S))
 
 # Eat sheep
@@ -310,7 +310,7 @@ g_inc_n = deepcopy(G)
 set_subpart!(g_inc_n, 1, :countdown, 0)
 rem_part!(g_inc_n, :Eng, 1)
 
-g_inc_rule = Rule(G; ac=[AppCond(hom(G, g_inc_n), false)],
+g_inc_rule = Rule(G; ac=[NAC(hom(G, g_inc_n))],
                   expr=(Eng=[vs -> only(vs) - 1],))
 g_inc = RuleApp(:GrassIncrements, g_inc_rule, G) |> tryrule
 

docs/literate/full_demo.jl

@@ -317,8 +317,8 @@ one, two, three, four, five = [@acset(Graph, begin
   V = 1; E = n; src = 1; tgt = 1 
 end) for n in 1:5]
 
-c2 = AppCond(homomorphism(Graph(1), two); monic=true)         # PAC
-c3 = AppCond(homomorphism(Graph(1), four), false; monic=true) # NAC
+c2 = PAC(homomorphism(Graph(1), two); monic=true)         # PAC
+c3 = NAC(homomorphism(Graph(1), four); monic=true) # NAC
 constr = c2 ⊗ c3 # logical conjunction: 2 ≤ |E| < 4
 
 rule = Rule(id(Graph(1)), id(Graph(1)); ac=[constr])

docs/literate/game_of_life.jl

@@ -249,7 +249,7 @@ BirthP1 = living_neighbors(3) # must have 3 neighbors
 BirthN1 = living_neighbors(4) # forbid the cell to have 4 neighbors
 BirthN2 = Curr() # forbid the cell to be alive (i.e. it's currently dead)
 BP1, BN1, BN2 = homomorphism.(Ref(Life(1)), [BirthP1, BirthN1, BirthN2]; initial=(V=[1],))
-bac = [AppCond(BP1; monic=true), AppCond.([BN1, BN2], false; monic=true)...]
+bac = [PAC(BP1; monic=true), NAC.([BN1, BN2]; monic=true)...]
 Birth = Rule(id(Life(1)), to_next(); ac=bac);
 
 # ### A living cell stays alive iff 2 or 3 living neighbors
@@ -259,7 +259,7 @@ end
 PersistP1 = living_neighbors(2; alive=true)
 PersistN1 = living_neighbors(4; alive=true)
 DR, DP1, DN1 = homomorphism.(Ref(Curr()), [PersistR, PersistP1, PersistN1]; initial=(V=[1],))
-pac = [AppCond(DP1; monic=true), AppCond(DN1, false; monic=true)]
+pac = [PAC(DP1; monic=true), NAC(DN1; monic=true)]
 Persist = Rule(id(Curr()), DR; ac=pac);
 
 # ### remove "Curr" status

docs/literate/lotka_volterra.jl

@@ -378,7 +378,7 @@ end;
 sheep_fwd_rule = Rule(
   hom(s_fwd_i, s_fwd_l; monic=true),
   hom(s_fwd_i, s_fwd_r; monic=true),
-  ac=[AppCond(hom(s_fwd_l, s_n), false)],
+  ac=[NAC(hom(s_fwd_l, s_n))],
   expr=(Eng=[vs -> only(vs) - 1],))
 ;
 
@@ -418,7 +418,7 @@ GS_Dir = hom(G⊕D, S; monic=true)
 GS_Dir30 = hom(G⊕D, add_time(S, 30); monic=true)
 
 se_rule = Rule(GS_Dir,GS_Dir30; expr=(Eng=[vs -> only(vs) + 4],),
-  ac=[AppCond(hom(S, s_eat_nac), false)]);
+  ac=[NAC(hom(S, s_eat_nac))]);
 
 S_to_S30 = hom(S, add_time(S, 30))
 sheep_eat = tryrule(RuleApp(:Sheep_eat, se_rule, id(S), S_to_S30));

src/incremental/IncrementalCC.jl

@@ -270,30 +270,53 @@ end
 """
 General method for discovering the newly added homs that arise from deleting 
 some part of the world due to a NAC.
+
+This function does NOT assume we have done DPO rewriting, where the possible 
+deletions are subobjects of the pattern. Deletion can extend
+beyond some statically known context, a less efficient algorithm is needed.
+
+Given an overlap which has been constructed to have *some* part intersecting 
+with the *deleted* portion of X, we extend this to a full match N->X. This is 
+done by forcing the overlap triangle to commute, and forcing everything not in 
+the overlap (as well as everything in the image of `n`, even if it is in the 
+overlap) to go to non-deleted portions of X. Every such morphism, g, is then
+pulled back to X', and then precomposed with n to get a new match from P that 
+was made possible due to the deletion X ↢ X'.
+
+```
+                                     n
+                              O  → N ← P
+                              ↓ ↙g ↓ ↙
+                              X  ← X'
+                                f
+```
 """
 function new_nac_homs!(runt::IncCCRuntime, constr::IncConstraints, nac::NAC, 
                        f::ACSetTransformation, new_keys, new_matches,
                        X_nondeleted::Dict{Symbol, Set{Int}})
   N, X = codom(nac), codom(f)
   Ob = ob(acset_schema(N))
+  nac_image = Dict(o => collect(nac.m[o]) for o in Ob)
   for spn in nac_overlap(nac, f) # N ↢ overlap -> X ↢ X'
     overlap = apex(spn)
     overlap_N = Dict(o=>Set(collect(left(spn)[o])) for o in Ob)
     # everything that is not in overlap is forced to go to a non-deleted thing
     predicates = Dict(map(Ob) do o 
       o => Dict([p => X_nondeleted[o] for p in parts(N, o) 
-                 if p ∉ overlap_N[o]])
+                 if p ∉ overlap_N[o] || p ∈ nac_image[o]])
     end)
     # force the triangle to commute
     initial = Dict(map(Ob) do o 
-      o=>Dict(map(parts(overlap, o)) do p
+      o => Dict(map(parts(overlap, o)) do p
         left(spn)[o](p) => right(spn)[o](p)
       end)
     end)
+
     # get *new* matches that were blocked from existing by this NAC
-    for h in homomorphisms(N, X; monic=nac.monic, predicates, initial)
-      h′ = pull_back(f, nac.m ⋅ h) # constrained search so that this must work
-      add_match!(runt, constr, new_keys, new_matches, h′)
+    for g in homomorphisms(N, X; monic=nac.monic, predicates, initial)
+      h = pull_back(f, nac.m ⋅ g) # constrained search so that this must work
+      isnothing(h) && error("Error in new_nac_homs!")
+      add_match!(runt, constr, new_keys, new_matches, h)
     end
   end
 end

src/rewrite/Constraints.jl

@@ -1,7 +1,7 @@
 module Constraints 
 export apply_constraint, Constraint, CGraph, arity,
        ∀, ∃, ∃!, True, False, Commutes,
-       AppCond, LiftCond, Trivial
+       AppCond, LiftCond, Trivial, PAC, NAC
 using Catlab
 import Catlab.Theories: ⊗, ⊕
 import Catlab.CategoricalAlgebra: ¬
@@ -457,7 +457,8 @@ function AppCond(f::ACSetTransformation, pos::Bool=true; monic=false)
   return Constraint(cg, pos ? expr : ¬(expr))
 end
 
-
+NAC(f; kw...) = AppCond(f, false; kw...)
+PAC(f; kw...) = AppCond(f, true; kw...)
 
 """
       ∀₂ 

test/incremental/IncrementalCC.jl

@@ -74,7 +74,7 @@ rewrite!(mset, M_rule)
 del = delete(Graph(1))
 mset = IncHomSet(Graph(1), [del], G2⊕T; nac=[del]);
 @test length(keys(mset)) == 2
-M_rule = Rule(id(Graph(1)), delete(Graph(1)); ac=[AppCond(del, false)])
+M_rule = Rule(id(Graph(1)), delete(Graph(1)); ac=[NAC(del)])
 m = ACSetTransformation(Graph(1), G2⊕T; V=[1])
 rewrite!(mset, M_rule, m)
 @test length(keys(mset)) == 1
@@ -103,7 +103,7 @@ edge_loop = @acset Graph begin V=2; E=2; src=[1,1]; tgt=[1,2] end
 to_edge_loop = homomorphism(e, edge_loop; monic=true)
 # rem edge, not if src has loop
 r = Rule(homomorphism(G2, e; initial=(V=1:2,)), id(G2);
-         ac=[AppCond(to_edge_loop, false; monic=true)]);
+         ac=[NAC(to_edge_loop; monic=true)]);
 
 mset = IncHomSet(r, edge_loop);
 @test length(keys(mset)) == 1
@@ -116,7 +116,7 @@ rewrite!(mset, r)
 #----------------------------------------------------------------
 # Remove edge, only if src has loop (no monic constraint on PAC)
 r = Rule(homomorphism(G2, e; initial=(V=1:2,)), id(G2);
-         ac=[AppCond(to_edge_loop)]);
+         ac=[PAC(to_edge_loop)]);
 mset = IncHomSet(r, edge_loop ⊕ e);
 m1, m2 = get_matches(r, state(mset)) # first one removes the loop
 rewrite!(mset, r, m1)
@@ -132,8 +132,8 @@ rewrite!(mset, r)
 edge_loop′ = @acset Graph begin V=2; E=2; src=[1,2]; tgt=[2,2] end
 to_edge_loop′ = homomorphism(e, edge_loop′; monic=true)
 r = Rule(id(e), to_edge_loop′;
-         ac=[AppCond(to_edge_loop; monic=true), 
-             AppCond(to_edge_loop′, false; monic=true)]);
+         ac=[PAC(to_edge_loop; monic=true), 
+             NAC(to_edge_loop′; 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
@@ -195,7 +195,6 @@ expected = @acset WeightedGraph{Bool} begin
 end
 @test is_isomorphic(expected, state(hset))
 
-get_matches(A_rule, state(hset))
 rewrite!(hset, A_rule)
 @test validate(hset)
 end
@@ -232,4 +231,29 @@ validate(hset)
 rewrite!(hset, Rule(id(rep), f))
 validate(hset)
 
+
+# SPO-inspired example
+#---------------------
+
+@present SchFirm(FreeSchema) begin 
+  (P,F,J,V)::Ob; 
+  v::Hom(V,F); p::Hom(J,P); f::Hom(J,F)
+end
+@acset_type Firm(SchFirm)
+P = @acset Firm begin P=1 end
+F = @acset Firm begin P=1 end
+J = @acset Firm begin J=1;F=1;P=1;f=1;p=1 end
+V = @acset Firm begin V=1;F=1;v=1 end
+
+nac = homomorphism(P⊕V, J⊕V)
+
+init =@acset Firm begin F=2; J=1; P=2; V=1; f=[1]; p=[2]; v=[2] end
+next = @acset Firm begin F=2; P=1; V=1; v=[2] end
+upd = homomorphism(next, init; initial=(F=1:2,P=[1]))
+
+# We look for Person+Vacancy pairs such that the person isn't already employed
+mset = IncHomSet(P⊕V, ACSetTransformation[], init; nac=[nac]);
+deletion!(mset, upd)
+validate(mset)
+
 end # module

test/rewrite/Constraints.jl

@@ -27,7 +27,7 @@ Positive application condition: a particular matched vertex must have self loop.
 looparr = @acset Graph begin V=2; E=2; src=[1,1]; tgt=[1,2] end 
 p2 = path_graph(Graph, 2)
 f=homomorphism(p2,looparr; monic=true)
-constr = AppCond(f, true)
+constr = PAC(f)
 
 G = @acset Graph begin V=1;E=1;src=1;tgt=1 end
 f = homomorphism(p2, G)
@@ -89,8 +89,8 @@ to_graphviz(constr)
 two_loops = @acset Graph begin V=1; E=2; src=1; tgt=1 end
 three_loops = @acset Graph begin V=1; E=3; src=1; tgt=1 end
 
-c2 = AppCond(homomorphism(Graph(1), two_loops); monic=true)
-c3 = AppCond(homomorphism(Graph(1), three_loops); monic=true)
+c2 = PAC(homomorphism(Graph(1), two_loops); monic=true)
+c3 = PAC(homomorphism(Graph(1), three_loops); monic=true)
 constr = c2 ⊕ c3
 to_graphviz(constr)
 

test/rewrite/PBPO.jl

@@ -223,7 +223,7 @@ tk = ACSetTransformation(K, K′; V=[1,2])
 l′ = homomorphism(K′,L′; monic=true, initial=(V=[1,2,3,4],)) 
 
 loop = @acset WG begin V=1;E=1;Weight=1;src=1;tgt=1;weight=[AttrVar(1)]end 
-ac = AppCond(homomorphism(L,loop), false) # cannot bind pattern to loop
+ac = NAC(homomorphism(L,loop)) # cannot bind pattern to loop
 
 """
         ∀

test/runtests.jl

@@ -13,11 +13,11 @@ using DataMigrations
 #######
 
 @testset "Full Demo" begin
-  include("../docs/literate/full_demo.jl")
+  # include("../docs/literate/full_demo.jl")
 end
 
 @testset "Lotka Volterra" begin
-  include("../docs/literate/lotka_volterra.jl")
+  # include("../docs/literate/lotka_volterra.jl")
 end
 
 @testset "Game of Life" begin