AlgebraicJulia / Catlab.jl

A framework for applied category theory in the Julia language
https://www.algebraicjulia.org
MIT License
614 stars 58 forks source link

Improved support for left pushforward data migration #436

Open epatters opened 3 years ago

epatters commented 3 years ago

Thanks to @slibkind's PR #433, we now have a first implementation of the left pushforward data migration functor for C-sets. Given a functor F: C -> D between schemas, the algorithm assumes that the graph generating D has no cycles (it performs a topological sort on D). This means that we cannot, for example, create the free reflexive graph on a graph because the schema for reflexive graphs has cycles.

In general, computing left Kan extensions is a challenging problem. The state of the art seems to be Fast Left Kan Extensions using the Chase by Spivak and Wisnesky. For a next step, I think we should just do the simplest thing that would cover standard examples like symmetric and/or reflexive graphs.

epatters commented 3 years ago

A question to get started. I think the current implementation explicitly constructs the comma categories F/d, but perhaps we should be constructing presentations of them instead? As a point of comparison, the cited paper shows how, assuming C, D, and F are finitely presented, to finitely present the collage of F (meaning the collage of the profunctor represented by F). The collage contains essentially the same data as all the comma categories used in the formula for Sigma_F (see Proposition 1 and Lemma 2).

kris-brown commented 2 years ago

This is being addressed in https://github.com/AlgebraicJulia/Catlab.jl/pull/615

epatters commented 2 years ago

Great! I was hoping that you would work on this stuff.