conegation rewriting

Project.toml

@@ -20,7 +20,7 @@ Luxor = "ae8d54c2-7ccd-5906-9d76-62fc9837b5bc"
 AlgebraicRewritingLuxorExt = "Luxor"
 
 [compat]
-ACSets = "0.2.3"
+ACSets = "0.2.9"
 Catlab = "0.15.4"
 DataStructures = "0.17, 0.18"
 Reexport = "^1"

docs/make.jl

@@ -11,7 +11,8 @@ end
 makedocs(
     sitename = "AlgebraicRewriting",
     format = Documenter.HTML(),
-    modules = [AlgebraicRewriting]
+    modules = [AlgebraicRewriting],
+    warnonly = true
 )
 
 

docs/src/full_demo.jl

@@ -11,8 +11,6 @@ This is a regular julia file that can be run interactively.
 Importantly: 
  - use Julia 1.9 (not yet official released)
  - ]activate the environment in AlgebraicRewriting.jl/docs 
- - check (via ]status) that Catlab branch "varacsets4" is used
- - check that AlgebraicRewriting.jl branch "compat_varacsets" is used
  - check that graphviz is installed locally (test via "which dot" in terminal)
 
 Table of contents:

src/categorical_algebra/CSets.jl

@@ -217,6 +217,7 @@ end
 function can_pushout_complement(pair::ComposablePair{<:ACSet})
   S = acset_schema(dom(pair))
   Ts = datatypes(dom(pair))
+  all(is_natural, pair) || error("Unnatural inputs")
 
   all(can_pushout_complement, unpack_diagram(pair; S=S, Ts=Ts)) &&
     isempty(dangling_condition(pair))

src/rewrite/CoNeg.jl

@@ -0,0 +1,48 @@
+module CoNeg 
+using Catlab.CategoricalAlgebra
+
+using ...CategoricalAlgebra.CSets
+using ..Utils
+import ..Utils: rewrite_match_maps
+import Catlab.CategoricalAlgebra: Subobject
+
+Subobject(X::ACSet, f::ACSetTransformation) = 
+  Subobject(X; Dict([k=>collect(vs) for (k,vs) in pairs(components(f))])...)
+
+"""    rewrite_match_maps(r::Rule{:CoNeg}, m)
+Apply a CoNegation rewrite rule (given as a span, L↩I->R) to a ACSet
+using a monic match morphism `m` which indicates where to apply the rewrite.
+              l   r
+           L <- I -> R
+         m ↓    ↓    ↓
+           G <- K -> H   where  K = ~L ∨ I
+
+This works for any type that implements bi-Heyting logic operators ~ and ∨.
+
+This is described [here](https://topos.site/blog/2023/04/conegation-rewriting).
+Essentially, it is partway between DPO and SPO. Suppose the rule tries to delete
+two things, one of which satisfies the dangling condition, the other violates it.
+While DPO would fail to apply at all, and SPO would delete both things (cascading 
+the deletion for the latter), co-negation rewriting would simply delete the item 
+which can be deleted without cascading and ignore the other element.
+
+It includes a quote which indicates that this method should work even when the 
+match morphism isn't monic, if it satisfies the identification condition. 
+Supporting this is not yet implemented.
+
+Match morphisms which bind attribute variables are not monic, hence we this 
+form of rewriting doesn't support VarACSets. Intuitively, it feels like this 
+restriction could be relaxed.
+"""
+function rewrite_match_maps(r::Rule{:CoNeg}, m; check::Bool=false)
+  !check || is_monic(m) || error("Can only use CoNeg rewriting with monic matches: $m")
+  L = codom(m)
+  L′ = Subobject(L, m)
+  I′ = Subobject(L, compose(left(r), m))
+  K′ = ~L′ ∨ I′
+  ik = hom(Subobject(dom(hom(K′)), hom(I′)))
+  rh, kh = pushout(right(r), ik)
+  Dict(:ik => ik, :kg => hom(K′), :rh => rh, :kh => kh)
+end
+
+end # module

src/rewrite/Rewrite.jl

@@ -5,6 +5,7 @@ using Reexport
 include("Constraints.jl")
 include("Utils.jl")
 include("DPO.jl")
+include("CoNeg.jl")
 include("SPO.jl")
 include("SqPO.jl")
 include("PBPO.jl")
@@ -14,6 +15,7 @@ include("Representable.jl")
 @reexport using .Utils
 @reexport using .Representable
 @reexport using .DPO
+@reexport using .CoNeg
 @reexport using .SPO
 @reexport using .SqPO
 @reexport using .PBPO

src/rewrite/Utils.jl

@@ -26,7 +26,7 @@ The L structure encodes a pattern to be matched.
 The R morphism encodes a replacement pattern to be substituted in.
 They are related to each other by an interface I with maps: L ⟵ I ⟶ R 
 
-A semantics (DPO, SPO, or SqPO) must be chosen.
+A semantics (DPO, SPO, CoNeg, or SqPO) must be chosen.
 
 Control the match-finding process by specifying whether the match is
 intended to be monic or not, as well as an optional application
@@ -94,11 +94,12 @@ right(r::Rule{T}) where T = r.R
 
 # Extracting specific maps from rewriting output data 
 #####################################################
+DPO′ = [:DPO, :CoNeg] # these have identical diagrams
 
 """Extract the map from the R to the result from the full output data"""
 function get_rmap(sem::Symbol, maps)
   if isnothing(maps)  nothing
-  elseif sem == :DPO  maps[:rh]
+  elseif sem ∈ DPO′  maps[:rh]
   elseif sem == :SPO  invert_hom(maps[:rmono], epic=false) ⋅ maps[:rmap]
   elseif sem == :SqPO maps[:r]
   elseif sem == :PBPO maps[:w]
@@ -111,7 +112,7 @@ get_result(sem::Symbol, maps) = codom(get_rmap(sem, maps))
 """Extract the partial map (derived rule) from full output data"""
 function get_pmap(sem::Symbol, maps)
   if isnothing(maps)  nothing
-  elseif sem == :DPO  Span(maps[:kg], maps[:kh])
+  elseif sem ∈ DPO′  Span(maps[:kg], maps[:kh])
   elseif sem == :SPO  Span(maps[:gmono], maps[:gmap])
   elseif sem == :SqPO Span(maps[:i], maps[:o])
   elseif sem == :PBPO Span(maps[:gl], maps[:gr])

test/rewrite/CoNeg.jl

@@ -0,0 +1,18 @@
+module TestCoNeg 
+
+using Test
+using AlgebraicRewriting, Catlab
+
+# Graphs
+########
+L = Graph(2)
+R = ob(terminal(Graph))
+r = Rule{:CoNeg}(create.([L,R])...)
+
+G = path_graph(Graph, 2) ⊕ Graph(1)
+m = ACSetTransformation(L, G; V=[1,3]);
+
+expected = path_graph(Graph, 2) ⊕ R
+@test is_isomorphic(expected, rewrite_match(r, m))
+
+end # module

test/rewrite/DPO.jl

@@ -117,21 +117,16 @@ end
 # Graphs with attributes
 ########################
 
-@present TheoryDecGraph(FreeSchema) begin
-  E::Ob
-  V::Ob
-  src::Hom(E,V)
-  tgt::Hom(E,V)
-
+@present SchDecGraph <: SchGraph begin
   X::AttrType
   dec::Attr(E,X)
 end
 
-@present TheoryLabeledDecGraph <: TheoryDecGraph begin
+@present SchLabeledDecGraph <: SchDecGraph begin
   label::Attr(V,X)
 end
 
-@acset_type LabeledDecGraph(TheoryLabeledDecGraph, index=[:src,:tgt])
+@acset_type LabeledDecGraph(SchLabeledDecGraph, index=[:src,:tgt])
 
 aI2 = @acset LabeledDecGraph{String} begin
   V = 2;  label = ["a","b"]

test/runtests.jl

@@ -47,6 +47,10 @@ end
   include("rewrite/DPO.jl")
 end
 
+@testset "CoNeg" begin
+  include("rewrite/CoNeg.jl")
+end
+
 @testset "SPO" begin
   include("rewrite/SPO.jl")
 end