I am interested in knowing how we can use the concepts of Limits and Colimits in modeling problems in every day life? Could anyone provide (Software) engineering examples, perhaps? Or describe intuitively in general for what sorts of modeling problems we can use these concepts? Thank you.
Take some relations $R_0\subseteq A_0\times A_1$, $R_1\subseteq A_1\times A_2$. Let $\pi_1:R_0\to A_1$, $\pi_0:R_1\to A_1$ be projections with domains restricted to relations $R_0$, $R_1$. Then the pullback of $\pi_0$, $\pi_1$ is the join of $R_0$ and $R_1$ in the SQL sense.
In Spivak's book on page 192 he gives an example of using colimits to create transit maps. Also, his Application 126.96.36.199 discusses applying Liquibase like patches to a database schema over time then using the colimits to reason between old and new data in universal manner.
A nice example is Tate et al.'s Generating Compiler Optimizations from Proofs. He uses pullbacks and pushouts as generalized unions and intersections, in categories where arrows are (IIRC) substitutions.
Ross Tate claims (on the paper webpage) that details were overwhelming without the abstraction afforded by category theory. Personally, I'd like to submit as "suggestive evidence" (if there can be any evidence of such a claim) diagrams (6) and (7) in their paper — they look complex enough in diagrammatic form. Let me quote their comments inline.
Some have asked us why we abstracted our proof generalization technique at all, and why we used category theory as our abstraction. However, we actually designed the abstract algorithm first, using category theory, and then used that to figure out how to solve our concrete problem. We got stuck with the concrete problem, overwhelmed by the details and the variables, and any solution we could think of seemed arbitrary. In order to reflect and simplify, we decided to phrase our question categorically. This lead to a diagram of sources and sinks, so we just used pushouts and pullbacks to glue things together. The biggest challenge was coming up with pushout completions, rather than using some existing standard concept. The categorical formulation was easy to specify and reason about. Afterwards, we instantiated the abstract processes, such as pushouts, with concrete algorithms, such as unification, in order to produce our final implementation with strong generality guarantees.
We have actually found this process of abstracting to category theory whenever we get stuck to be quite fruitful. Not only does it end up solving our concrete problem, but we end up with a better understanding of our own problem as well as an abstract solution which can be easily adapted to other applications. Thus, our experience suggests that category theory may be useful in constructing actual algorithms, in addition to being useful as a framework for formalization. We would be interested to know of other similar experiences, either positive or negative.
A wide field of applications is in graph transformations (applied in model-driven engineering). Two relevant papers are (given with links to Google Scholar):
- Tutorial introduction to graph transformation: A software engineering perspective
- Algebraic Approaches to Graph Transformation-Part I: Basic Concepts and Double Pushout Approach.
EDIT: again, (part of) the basic idea is that pushouts act as a union with some glue. This allows defining "rewrite rules" for graphs — you match the left-hand side to the graph, and then glue the right-hand side to the (rest of) the graph in a corresponding manner. I'm afraid I can't add details because I've never gotten more than the intuition.