Constraints on attributes in `maximum_common_subobject`

[slwu89]

It would be nice to be able to provide additional information to maximum_common_subobject when we have attributes (i.e. what values they "ought" to take).

Consider the example where we're making the span for a DPO rule and we want to automatically generate the graph $I$, in this case we want to get the $I$ for the rewrite rule which moves tokens around when the infection event fires. We'd like to be able to tell maximum_common_subobject that we want sname to be :I in the common subobject to filter out the results somehow. This is helpful when making lots of rules programatically.

using Catlab, AlgebraicPetri, AlgebraicRewriting

# we want a PN with a marking
@present SchMarkedLabelledPetriNet <: SchLabelledPetriNet begin
    M::Ob
    m::Hom(M,S)
end

@acset_type MarkedLabelledPetriNet(SchMarkedLabelledPetriNet, index=[:it, :is, :ot, :os]) <: AbstractLabelledPetriNet

# an SIR model with birth and death
epiPN = @acset MarkedLabelledPetriNet{Symbol} begin
    S=3
    sname=[:S,:I,:R]
    T=6
    tname=[:inf,:rec,:birth,:deathS,:deathI,:deathR]
    I=6
    it=[1,1,2,4,5,6]
    is=[1,2,2,1,2,3]
    O=4
    ot=[1,1,2,3]
    os=[2,2,3,1]
end

L = @acset MarkedLabelledPetriNet{Symbol} begin
    S=2
    sname=[:S,:I]
    M=2
    m=[1,2]
end

R = @acset MarkedLabelledPetriNet{Symbol} begin
    S=1
    sname=[:I]
    M=2
    m=[1,1]
end

only(maximum_common_subobject([L,R]))[1]

[kris-brown]

we want sname to be :I in the common subobject

I don't know how to make sense of this as written, as there could be any number of S elements in the overlap ACSet, which you don't know ahead of time.

My first thought is that a boolean keyword argument could be added to control whether or not the apex of the overlap span should have only AttrVars or attributes. The former is the current behavior, which allows us to find common structure completely ignoring attribute values. The latter is the other extreme, requiring exact agreement on attribute values. Would this work for you?

My second thought is that the rewrite rules that come out of this will still work, even if there is an AttrVar in the intermediate I ACSet (with concrete :I attributes in the L and R ACSets).

While playing around with your example I noticed an unrelated issue with maximum_common_subobject, where it can sometimes unexpectedly change the order of the feet of the resulting span, which I'll create a different issue for.

[slwu89]

Hi @kris-brown thanks for checking this out!

Yes ignore that, it was poorly written. What I meant to say was that it would be nice to somehow be able to insist on exact agreement on attribute values in some cases, such that the span maximum_common_subobject returns would have an acset with sname = :I in this specific case.

Yeah, that idea sounds really good. Would it be possible to independently select from these two behaviors for each attribute?

[kris-brown]

Yeah! That would be the natural way of supporting intermediate options between the two extremes, kind of like how the monic keyword in hom search can be boolean or a vector of Ob symbols.

[kris-brown]

Ok, the keyword is now abstract=[:Name] (or abstract=false) for your example. Let me know how it works out for you!

[slwu89]

@kris-brown thanks! I am trying it out. Looks great! So, just to be clear, the default behavior when abstract is not given is as before, when giving abstract=false we insist on exact agreement of attribute values for all AttrTypes, and when we give a vector, those AttrTypes in the vector follow the previous behavior, and those not listed in the vector follow exaxt agreement on attribute behavior? Anyway, I think this is good to close.

julia> subobj = only(maximum_common_subobject([L,R], abstract=false))
julia> subobj[1]
MarkedLabelledPetriNet{Symbol} {T:0, S:1, I:0, O:0, M:1, Name:0}
┌───┬───────┐
│ S │ sname │
├───┼───────┤
│ 1 │     I │
└───┴───────┘
┌───┬───┐
│ M │ m │
├───┼───┤
│ 1 │ 1 │
└───┴───┘