<p>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.</p>

CC BY-SA 3.0
2014-02-11T19:42:13.897Z
2014-02-11T19:42:13.897Z
beroal
<p>A nice example is Tate et al.'s <a href="http://www.cs.cornell.edu/%7Eross/publications/proofgen/" rel="noreferrer"><em>Generating Compiler Optimizations from Proofs</em></a>. He uses pullbacks and pushouts as generalized unions and intersections, in categories where arrows are (IIRC) substitutions.</p>
<p>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 &quot;suggestive evidence&quot; (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.</p>
<blockquote>
<p>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.</p>
<p>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.</p>
</blockquote>

CC BY-SA 3.0
2015-01-05T17:15:52.880Z
2015-01-05T17:15:52.880Z
2020-06-17T09:38:08.363Z
Blaisorblade
<p>A wide field of applications is in graph transformations (applied in model-driven engineering). Two relevant papers are (given with links to Google Scholar):</p>

<ul>
<li><a href="http://scholar.google.com/scholar?cluster=8332259365699881202&amp;hl=en&amp;as_sdt=0,5" rel="noreferrer">Tutorial introduction to graph transformation: A software engineering perspective</a></li>
<li><a href="http://scholar.google.com/scholar?cluster=2396004333404064099&amp;hl=en&amp;as_sdt=0,5" rel="noreferrer">Algebraic Approaches to Graph Transformation-Part I: Basic Concepts and Double Pushout Approach.</a></li>
</ul>

<p>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.</p>

CC BY-SA 3.0
2015-01-05T17:30:13.780Z
A better explanation is in this answer by Dave Clarke: http://cstheory.stackexchange.com/a/947/989
Blaisorblade
CC BY-SA 3.0
2015-01-05T17:23:35.970Z
2015-01-05T17:23:35.970Z
Blaisorblade
<p>In <a href="http://math.mit.edu/~dspivak/CT4S.pdf" rel="noreferrer">Spivak's book</a> on page 192 he gives an example of using colimits to create <a href="http://en.wikipedia.org/wiki/Transit_map" rel="noreferrer">transit maps</a>. Also, his Application 5.2.1.2 discusses applying <a href="http://www.liquibase.org/" rel="noreferrer">Liquibase</a> like patches to a database schema over time then using the colimits to reason between old and new data in universal manner.</p>

CC BY-SA 3.0
2014-02-11T20:52:37.707Z
2014-02-11T20:52:37.707Z
Chad Brewbaker
<p>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.</p>

CC BY-SA 3.0
2014-01-14T22:25:12.083Z
Everywhere this library is used, http://hackage.haskell.org/package/data-category-0.5.1/docs/Data-Category-Limit.html
Chad Brewbaker
CC BY-SA 3.0
2014-01-15T09:27:03.777Z
Which sadly is nowhere, afaict...
Sjoerd Visscher
CC BY-SA 3.0
2014-02-12T11:37:28.407Z
Check the chapter on category theory in the handbook of logic in cs.
Kaveh
<ct.category-theory>
What are the uses of Limits and Colimits of Category Theory in every day problems?
James
# What are the uses of Limits and Colimits of Category Theory in every day problems?

(Asked by: username_0 on 2014-01-14)

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.

**Tags:** ct.category-theory

> **Comments:**
> **username_1**: Everywhere this library is used, http://hackage.haskell.org/package/data-category-0.5.1/docs/Data-Category-Limit.html  
> **username_2**: Which sadly is nowhere, afaict...  
> **username_3**: Check the chapter on category theory in the handbook of logic in cs.  

---

## 4 answers

### Answer by username_4 on 2014-02-11. Score: 9

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.


---

### Answer by username_5 on 2015-01-05. Score: 6

A nice example is Tate et al.'s [*Generating Compiler Optimizations from Proofs*](http://www.cs.cornell.edu/%7Eross/publications/proofgen/). 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.


---

### Answer by username_5 on 2015-01-05. Score: 5

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](http://scholar.google.com/scholar?cluster=8332259365699881202&hl=en&as_sdt=0,5)
* [Algebraic Approaches to Graph Transformation-Part I: Basic Concepts and Double Pushout Approach.](http://scholar.google.com/scholar?cluster=2396004333404064099&hl=en&as_sdt=0,5)

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.

> **Comments:**
> **username_5**: A better explanation is in this answer by Dave Clarke: http://cstheory.stackexchange.com/a/947/989  

---

### Answer by username_1 on 2014-02-11. Score: 5

In [Spivak's book](http://math.mit.edu/~dspivak/CT4S.pdf) on page 192 he gives an example of using colimits to create [transit maps](http://en.wikipedia.org/wiki/Transit_map). Also, his Application 5.2.1.2 discusses applying [Liquibase](http://www.liquibase.org/) like patches to a database schema over time then using the colimits to reason between old and new data in universal manner.


---

