I'm not a theoretical computer scientist. I'm a stable homotopy theorist using $\infty$-categories. I've seen applications of category theory and topos theory to theoretical computer science, and I was wondering if there was any way one could use $\infty$-categories (and preferably for me, stable homotopy theory) in theoretical computer science. I think HoTT mught be one such application, but I may very well be wrong because I know close to nothing about HoTT. (So I also don't know how HoTT is used in TCS.)
$\begingroup$
$\endgroup$
4
-
1$\begingroup$ Have you taken a look at the HoTT Book? For example, the suspension theorem is proven in chapter 8. $\endgroup$– codyCommented Dec 22, 2014 at 21:31
-
$\begingroup$ @cody Yes, I've looked at it (but not in much detail); I'm not really interested in the application of HoTT to homotopy theory (or vice versa) but the application of homotopy theory and $\infty$-categories to TCS. Do you know some such applications? $\endgroup$– user21269Commented Dec 22, 2014 at 21:33
-
1$\begingroup$ You should ask this question five years from now. We don't know yet exactly how we're going to use $\infty$-categories in computer science. At the moment we have a pretty good idea about $\infty$-groupoids: they improved greatly our understanding of type theory. $\endgroup$– Andrej BauerCommented Dec 23, 2014 at 18:53
-
$\begingroup$ Have a look at Michael Shulmans section "Expository notes and talks" at the bottom of his page home.sandiego.edu/~shulman/papers/index.html. Mike is a homotopy-theorist by training, so you might find his stuff more easily understandable. $\endgroup$– Andrej BauerCommented Dec 23, 2014 at 19:39
Add a comment
|
3 Answers
$\begingroup$
$\endgroup$
1
Applying higher homotopy-theoretic ideas to CS is still a very nascent field! My understanding is that it's not even that old as a mathematical field.
Certainly HoTT is the central impetus for such ideas. Even there though, there only have been few applications of category theory of "dimension" higher than 2.
One nice "computer science-y" one is Homotopical Patch Theory by Anguili et al. They show that some common operations and properties inherent git like version control systems can be best understood using homotopy type theory.
Another rather unrelated train of thought is some interesting work on the relationship between (2-)Homology theory and confluence of term rewrite systems (or more complex structures such as higher algebras). Some examples are
Y. Guiraud Confluence of linear rewriting and homology of algebras .
Y. Lafont & A. Proute Church-Rosser property and homology of monoids.
-
$\begingroup$ Thanks, cody! I'll wait to see if there are any more answers before accepting. $\endgroup$– user21269Commented Dec 23, 2014 at 15:21
$\begingroup$
$\endgroup$
Theoretical computer scientists do many things, one of which is mathematical modeling of various computer-sciency things. For instance, we like to provide mathematical models of programming languages, so that people can actually prove things about programs (such as proving that the program does what it's supposed to). In this sense it is always good to have a good supply of mathematical techniques that will give us models for various things that computer scientists come up with.
In fact theoretical computer scientists had to invent some pretty advanced mathematical models because they wanted to get a good mathematical graps of what computer scientists were doing. Often classical set theory is not good enough for our purposes, for example because we want a non-tivial complete small category or a non-trivial set $D$ satisfying $D \cong D^D$.
Recently a connection between type theory (which is a common generalization of programming languages, logic and set theory) and homotopy theory has been uncovered. It is still very early to tell what exactly will come out of it, but our understanding of type theory has certainly been advanced by the homotopy-theoretic ideas. Conversely, it is becoming clear that intensional type theory, whatever that is, is a very good formal language for describing $(\infty,1)$-categories. People suspect there ought to be "directed type theory" which would correspond to $\infty$-categories, but nobody is sure yet. This is active area of research.
The only connection between stable homotopy theory and type theory I am aware of is the work of Matthijs Vákár on linear dependent type theory. Apparently, one model of it is stable homotopy theory, but this has not been published yet, only hinted at the end of the linked paper.
Another place where you could look for applications of homotopy theory (stable or not) in computer science is computational topology. There persistent homology has recently found many uses, and people are surely looking at homotopy-theoretic applications of a similar kind. The basic idea is to use algebraic topology to study properties of large datasets.
Without a doubt there are other applications. Cody mentioned the use of homotopy theory (in the guise of homotopy type theory) to study revision control systems. There are also applications of homotopy theory to the study of parallel and cuncurrent computations, such as "Algebraic topology and concurrency". Someone more knowledgable may be kind enough to provide better references. In any case, you will notice that all these applications (with the possible exception of homotopy type theory) are fairly unsophisticated from a mathematical point of view – which does not mean they are worthless!
answered Dec 23, 2014 at 19:35
$\begingroup$
$\endgroup$
this attempts to sketch out more general connections. some of this program can be considered a very recent & more elaborate extension of the old Curry-Howard correspondence noted between proofs and programs. there is also a close connection with automated theorem proving (aka proof assistants). many techniques used in automated theorem proving proofs are not on entirely solid mathematical ground and homotopy theory adds firmer grounding.
this proposal by a sizeable team captures/ surveys much of the currently known connections with CS: Homotopy Type Theory: Unified Foundations of Mathematics and Computation (MURI Proposal)
Licata from that team is esp interested in computer scientific applications of homotopy theory. some of his talks, and one by Voevodsky founder of the standout Univalence axiom:
Mathematical and Computational Applications of Homotopy Type Theory. Colloquium at University of Iowa. November, 2013. [slides]
Computer-Checked Proofs in the Logic of Homotopy Theory. Invited Talk at the Association for Symbolic Logic North American Meeting. May, 2013. [slides]
Programming and Proving in Homotopy Type Theory. Colloquium at Wesleyan, Princeton, and Cornell. Spring, 2013. [slides]
Computer Science and Homotopy Theory, 10m video lecture by Voevodsky / IAS
