Tag Info

Accepted

Impact of Grothendieck's program on TCS

Grothendieck's inequality, from his days in functional analysis, was initially proved to relate fundamental norms on tensor product spaces. Grothendieck called the inequality "the fundamental theorem ...

Algebra oriented branch of theoretical computer science

There have been recent developments in dependent type theory which relate type systems to homotopy types. This is now a relatively small field, but there is a lot of exciting work being done right ...
• 13.2k

Algebra oriented branch of theoretical computer science

Algebraic geometry is used heavily in algebraic complexity theory and in particular in geometric complexity theory. Representation theory is also crucial for the latter, but it's even more useful when ...
• 35.7k

Impact of Grothendieck's program on TCS

Grothendieck's impact can be felt in type theory and logic. For instance, Bart Jacobs' 700+ page volume Categorical Logic and Type Theory gives a uniform treatment of various type theories ($X$-type ...
• 16.6k

Is there a relationship between relational algebra/calculus and category theory?

Categorical approaches to query languages is a bit of a niche interest, but I think it's a very interesting niche! Two of the key figures in this area are Peter Buneman and Torsten Grust. Obviously, ...
• 31.6k
Accepted

There are several possible notions of proof relevance. Let us consider three similar situations: An element of a sum $\Sigma (x : A) . P(x)$ is a pair $(a, p)$ where $a : A$ and $p$ is a proof of $P(... • 26.6k 17 votes Status quo of category theory and monads in theoretical computer science research? There have been a number of developments with regards to the use of monads in the theory of computation since Eugenio Moggi's work. I am not able to give a comprehensive account, but here are some ... • 26.6k 15 votes Algebra oriented branch of theoretical computer science Your knowledge of field theory would be useful in cryptography, while category theory is heavily used in the research on programming languages and typing systems, both of which are closely related to ... • 10.3k 15 votes "The" category of Turing machines? If your objects are Turing machines, there are several reasonable possibilities for morphisms. For example: 1) Consider Turing machines as the automata they are, and consider the usual morphisms of ... • 35.7k 14 votes "The" category of Turing machines? You might be interested in Turing categories by Robin Cockett and Pieter Hofstra. From the point of view of category theory the question "what is the category of Turing machines" is less interesting ... • 26.6k 14 votes Does the uncomputability of Kolmogorov complexity follow from Lawvere's Fixed Point Theorem? EDIT: Adding the caveat that Roger's fixed-point theorem may not be a special case of Lawvere's. Here is a proof that may be "close"... It uses Roger's fixed-point theorem instead of Lawvere's ... • 8,143 13 votes Accepted Category-theoretic treatment of diffs, patches and merging? As pointed by Martin, there is some work on the categorical representation of patches. Mimram and Di Giusto's "A Categorical Theory of Patches" being the most extensive categorical approach to edit-... 13 votes Proof relevance vs. proof irrelevance I recommend that everyone first read Andrej Bauer's answer, as he covers all the basics extremely well. I agree with everything he says in his answer. I humbly offer more comments, even though I know ... • 1,490 12 votes Impact of Grothendieck's program on TCS Any applications of$p$-adic cohomology, etale cohomology in point counting formulas for algebraic varieties has roots in his work. I am guessing Mulmuley's vision of generalization of Riemann ... • 12.5k 12 votes Accepted "The" category of Turing machines? Saal Hardali mentioned that he wanted a category of Turing machines to do geometry (or at least homotopy theory) on. However, there are a lot of different ways to achieve similar aims. There is a ... • 31.6k 11 votes Algebra oriented branch of theoretical computer science Field theory and algrebraic geometry would be useful in topics related to error correcting codes, both in the classical setting as well as in studying locally decodable codes and list decoding. I ... 11 votes What's the relation between OOP and category theory? There are absolutely some relationships between the semantics and practice of OOP and category theory. This is somewhat unsurprising since both fields attempt to give a principled generic account of ... • 13.2k 11 votes Accepted Relating univalence for a theory of cateogries to the skeleton concept I refer you to Chapter 9 of the HoTT book. In particular, a category is defined in such a way that isomorphic objects are equal, see Definition 9.1.6. As Example 9.1.15 points out, there really isn't ... • 26.6k 11 votes Are there knot theoretic formulations of NP complete problems? You can take a look to: Peter Golbus, Robert W. McGrail, Tomasz Przytycki, Mary Sharac, and Aleksandar Chakarov. 2009. Tricolorable torus knots are NP-complete. In Proceedings of the 47th Annual ... • 22.3k 11 votes Uses of$\infty$-categories in TCS 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 ... • 13.2k 11 votes Uses of$\infty\$-categories in TCS

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, ...
• 26.6k
Accepted

A bicartesian closed category of strict complete partial orders (Hask)

Yes, it's impossible to have a nondegenerate CCC with general recursion and categorical coproducts. The standard reference for this is: H. Huwig and A. Poigne. A note on inconsistencies caused by ...
• 31.6k
Accepted

What kind of theoretical object corresponds to a C++ concept?

From a programming language theory perspective, as opposed to the computability perspective other answers and comments have offered, C++ templates combined with concepts correspond to bounded ...
• 16.6k
Accepted

What logic correponds via Curry-Howard to a Monad?

The two papers to look at it are Benton, Bierman and de Paiva's Computational Types from a Logical Perspective, which directly gives a proof theory for Moggi's computational lambda-calculus; and Rowan ...
• 31.6k

Is there a concept of something like co-applicative functors sitting between comonads and functors?

In this post on SO I found an interesting answer - decisive functors. If we replace () by Void, ...
• 2,471
Accepted

Is there any known CCC closed under a probabilistic powerdomain operation?

The following is an extended comment, it does not answer your question in the terms you posed it but does give a semantics for higher-order probabilistic calculi which you may find of interest. In ...
• 4,823
Accepted

Explaining monad transformers in categorical terms

According to Oleksandr Manzuk, they are "translation of a monad along an adjunction", see "Calculating Monad Transformers with Category Theory". By the way, that's the third hit on Google for "monad ...
• 26.6k

Are there knot theoretic formulations of NP complete problems?

There are a few references in the first paragraph of Marc Lackenby. A polynomial upper bound on Reidemeister moves. arXiv:1302.0180 In particular, the author says that the problem of recognizing ...
• 4,309
Accepted

Category theory and parsers --- references wanted

One of the very first applications of category theory to a subject outside of algebraic geometry was to parsing! The keywords you want to guide your search are "Lambek calculus" and "categorial ...
• 31.6k