C-Par rewriting

[kris-brown]

$C$-Par rewriting is a practical necessity for certain modeling applications where we wish to use a rewrite rule to change the value of an outgoing hom for some object without deleting+recreating the object.

The intermediate state of the world (and of the rewrite rule, i.e. the $I$ component) in this case would not satisfy the discrete opfibration condition of $C$-Set. But this should be functionally equivalent to rewriting where the relevant hom has been replaced by a span.

[slwu89]

Hi @kris-brown, I know we've discussed this elsewhere but I wanted to list out the example I was talking to you about regarding the runtime schema for a colored petri net somewhere less ephemeral, since it would benefit instantly from this feature.

using Catlab, AlgebraicRewriting

@present CPNSch(FreeSchema) begin
    (C₁,C₂,M,S)::Ob
    RealType::AttrType
    IntType::AttrType
    StringType::AttrType
    c₁::Hom(C₁,M)
    c₂::Hom(C₂,M)
    m::Hom(M,S)
    sname::Attr(S,StringType)
    label₁::Attr(C₁,StringType)
    label₂::Attr(C₂,StringType)
    size::Attr(C₁,IntType)
    density::Attr(C₂,RealType)
end

@acset_type CPN(CPNSch)

cpn = @acset CPN{Float64,Int,String} begin
    S=3
    sname=["A", "B", "C"]
    C₁=1
    label₁=["job1"]
    size=1
    c₁=[1]
    C₂=1
    label₂=["job2"]
    density=0.5
    c₂=[2]
    M=2
    m=[1,1]
end

# rule to move colors of type 1 to B
L = @acset CPN{Float64,Int,String} begin
    S=2
    sname=["A", "B"]
    StringType=1
    IntType=1
    C₁=1
    label₁=[AttrVar(1)]
    size=[AttrVar(1)]
    c₁=[1]
    M=1
    m=[1]
end

# uh oh, c₁:  C₁ -> M is dangling
I = @acset CPN{Float64,Int,String} begin
    S=2
    sname=["A", "B"]
    StringType=1
    IntType=1
    C₁=1
    label₁=[AttrVar(1)]
    size=[AttrVar(1)]
end

L = @acset CPN{Float64,Int,String} begin
    S=2
    sname=["A", "B"]
    StringType=1
    IntType=1
    C₁=1
    label₁=[AttrVar(1)]
    size=[AttrVar(1)]
    c₁=[1]
    M=1
    m=[2]
end

[kris-brown]

Thanks for the example! the other one I find very motivating is a schema $P \rightarrow V \leftleftarrows E$ which has People who live on the vertices of a graph. And a rule can match any person on a vertex with an outgoing arrow and move them forward. Currently we have to delete the person in order to change which vertex they're on (from src to tgt of the edge). However, this is no longer feasible the moment there are other things in the schema which refer to $P$.