Missing codiagonal / logical structure in Bicategory of Relations implementation

[jpfairbanks]

The implementation in Catlab is

@signature MonoidalCategoryWithDiagonals(Ob,Hom) => BicategoryRelations(Ob,Hom) begin
  # Dagger category.
  dagger(f::Hom(A,B))::Hom(B,A) <= (A::Ob,B::Ob)
  
  # Self-dual compact closed category.
  dunit(A::Ob)::Hom(munit(), otimes(A,A))
  dcounit(A::Ob)::Hom(otimes(A,A), munit())
end

but your paper Knowledge Representation in the Bicategory of Relations has this table

It looks like a lot of this is missing, like codiagonal and logical. Are these morphisms defined somewhere else? It looks like AbelianBicategoryRelations has the codiagonal but it is called plus/coplus instead of merge/copy.

@signature BicategoryRelations(Ob,Hom) => AbelianBicategoryRelations(Ob,Hom) begin
  # Second diagonal and codiagonal.
  mplus(A::Ob)::Hom(otimes(A,A),A)
  mzero(A::Ob)::Hom(munit(),A)
  coplus(A::Ob)::Hom(A,otimes(A,A))
  cozero(A::Ob)::Hom(A,munit())
end

Is that understanding right?

[jpfairbanks]

(related to #49)

[epatters]

Good point. I'm not sure what I was thinking at the time, but I guess it was to omit some of the derived structure in BicategoryRelations, e.g., you can get mmerge(X) as dagger(mcopy(X)). But there are two problems with this:

1. As you point out, it's not consistent with how I did AbelianBicategoryRelations, where there is both mplus and coplus.

2. More importantly, I usually prefer to include everything in the signature, even derived operations, and leave how to handle this up to specific instances and syntax systems. This is the most flexible approach. So you would have both mcopy and mmerge in the signature, and in a particular syntax system you could have mmerge(X) automatically translate to dagger(mcopy(X)) or not.

So, I would suggest making BicategoryRelations inherit MonoidalCategoryWithBidiagonals, instead of MonoidalCategoryWithDiagonals, and then fill out whatever else remains, such as the logical operations.

[epatters]

To get started, maybe you can try to fix just BicategoryRelations, as sketched above?

[jpfairbanks]

Cool, I'll take a look at it soon, I will probably have questions, but this is a good target for learning how Catlab works. I currently have the minimal understanding necessary to make wiring diagrams.

[jpfairbanks]

Hey Evan, I just wrote down the stuff in Table two in the language of @signature is this what you had in mind?

@signature MonoidalCategoryWithBiDiagonals(Ob,Hom) => BicategoryRelations(Ob,Hom) begin
  # We inherit the following special morphisms:
  #   mcopy(A::Ob)::Hom(A,otimes(A,A))
  #   mmerge(A::Ob)::Hom(otimes(A,A),A)
  #   delete(A::Ob)::Hom(A,munit())
  #   create(A::Ob)::Hom(munit(),A)
  # Dagger category.
  dagger(f::Hom(A,B))::Hom(B,A) <= (A::Ob,B::Ob)
  
  # Self-dual compact closed category.
  # the objects in Rel (sets) satisfy dual(X) = X
  dunit(A::Ob)::Hom(munit(), otimes(A,A))
  dcounit(A::Ob)::Hom(otimes(A,A), munit())

  # logical primitives
  intersection(f::Hom(A,B), g::Hom(A,B))::Hom(A,B)
  # intersection(f,g) = compose(mcopy(dom(f)), otimes(f,g), mmerge(codom(f))
  ltrue()::Hom(munit(),munit())
  # ltrue() = compose(mdelete(munit()), mcreate(munit())
  lmax(A::Ob,B::Ob)::Hom(A,B)
  # lmax(A,B) = compose(mdelete(A), mcreate(B)
end

The ltrue() = compose(mdelete(munit()), mcreate(munit()) seems suspicious to me because it deletes and creates I, which I thought was the "no wire" type.

I think I'll need to edit the @syntax definition

@syntax FreeBicategoryRelations(ObExpr,HomExpr) BicategoryRelations begin
  otimes(A::Ob, B::Ob) = associate_unit(Super.otimes(A,B), munit)
  otimes(f::Hom, g::Hom) = associate(Super.otimes(f,g))
  compose(f::Hom, g::Hom) = associate(Super.compose(f,g; strict=true))

  function dagger(f::Hom)
    f = anti_involute(Super.dagger(f), dagger, compose, id)
    distribute_unary(f, dagger, otimes)
  end
end

For the syntax we need to define that the otimes and compose are inherited from the super type, and the dagger is an involution that distributes over the monoidal product. Why don't we need to define anything about the dunit,dcounit in the @syntax macrocall? It might be helpful to understand the @syntax better in general.

[epatters]

Thanks, this is definitely the general strategy I had in mind.

I'll write up something soon about the difference between @signature and @syntax and the general philosophy behind this design. I don't think this is yet documented anywhere, so your confusion is understandable.

[epatters]

FYI, I'm currently writing up an introduction to the core modules (see #61), but I haven't yet written the part about @syntax. Coming soon!

Still, any feedback about what I have so far is welcome.

[epatters]

I've finished writing the introduction, at least for now.

[epatters]

I added the missing codiagonal and logical operations. I decided to use the lattice, rather than the logical, terminology, because meet and top are not used in the Julia language/standard library, while intersect and true are.