# Questions tagged [ct.category-theory]

Questions in category theory

104 questions
Filter by
Sorted by
Tagged with
9k views

### Solid applications of category theory in TCS?

I've been learning a few bits of category theory. It certainly is a different way of looking at things. (Very rough summary for those who haven't seen it: category theory gives ways of expressing all ...
6k views

### Explaining Applicative functor in categorical terms - monoidal functors

I'd like to understand Applicative in terms of category theory. The documentation for Applicative says that it's a strong lax ...
6k views

### Algebra oriented branch of theoretical computer science

I have a very strong base in algebra, namely commutative algebra, homological algebra, field theory, category theory, and I am currently learning algebraic geometry. I am a math major with an ...
2k views

### A category of NP-complete problems?

Does it make sense to consider a category of all NP-complete problems, with morphisms as poly-time reductions between different instances? Has anyone ever published a paper about this, and if so, ...
646 views

### Bounded-input bijections of infinite sequences

Here is a puzzle I haven't managed to solve. I would like to know if this problem is already known, or has an easy solution. It is possible to define a bijection $3^\mathbb{N} \cong 5^\mathbb{N}$ ...
3k views

### Impact of Grothendieck's program on TCS

Grothendieck has passed away. He had massive impact on 20th century mathematics continuing into the 21st century. This question is asked somewhat in the style/spirit, for example, of Alan Turing's ...
1k views

### What is the folk model of linear logic?

Probably the most common application of linear types in PL is to use them to give languages which control aliasing (i.e., a linear value has a single pointer to it, more or less). But there's a ...
3k views

### Regular languages from category-theoretical point of view

I noticed that regular languages over the alphabet $\Sigma$ can be naturally thought of as a poset, and indeed a lattice. Moreover, concatenation together with the empty language $\epsilon$ defines a ...
2k views

### What is the difference between arrows and exponential objects in a cartesian closed category?

In a Cartesian Closed Category (CCC), there exist the so-called exponential objects, written $B^A$. When a CCC is considered as a model of the simply-typed $\lambda$-calculus, an exponential object ...
1k views

### How are Futures described in terms of category theory?

Is there a useful description of futures or promises in terms of category theory? In particular, what could the categorical dual of Future be?
2k views

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

I am aware of at least two different theoretical approaches for understanding relational databases: Codd's relational algebra/calculus, and category theory. Is there any relationship between these ...
3k views

### Data Structure isomorphisms

Disclaimer: I am not a CS theorist. Coming from abstract algebra, I'm used to dealing with things that are equal up to a isomorphism - but I'm having a trouble translating this concept to data ...
2k views

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

Any monad is also an applicative functor and any applicative functor is a functor. Also, any comonad is a functor. Is there a similar concept between comonads and functors, something like co-...
3k views

Let $C$ be a CCC. Let $(\times)$ be a product bifunctor on $C$. As Cat is CCC, we can curry $(\times)$: $curry (\times) : C \rightarrow(C \Rightarrow C)$ $curry (\times) A = \lambda B. A \times B$ ...
1k views

### “The” category of Turing machines?

Disclaimer: I know very little about complexity theory. I'm sorry but there is really no way to ask this question without being (terribly) concise: What should be the morphisms in "the" category ...
659 views

### What is the categorical semantics of subtyping?

Starting from Curry-Howard-Lambek, there has been a nice trinity of type theories, logics, and categories. I'm curious what categorical semantics you get when you add (coercive) subtyping to a type ...
2k views

### Status quo of category theory and monads in theoretical computer science research?

Background. I am a bachelor student who is interested in research related to category theory, monads and Haskell, and I want to find a topic for my bachelor’s thesis in that area. I have looked at ...
839 views

### Does the uncomputability of Kolmogorov complexity follow from Lawvere's Fixed Point Theorem?

Many theorems and "paradoxes" - Cantor's diagonalization, undecidability of hatling, undeciability of Kolmogorov complexity, Gödel Incompleteness, Chaitin Incompleteness, Russell's paradox, etc. -...
3k views

### Category theory, computational complexity, and combinatorics connections?

I have been trying to read “Pearls of Functional Algorithm design”, and subsequently “The Algebra of Programming”, and there is an obvious correspondence between recursively (and polynomially) defined ...
222 views

### Using Dependent Type Theory for Categories that are not LCCC

I have recently been working with polynomial functors and monads based mostly on Gambino-Kock. There they define polynomial functors in a Locally Cartesian Closed Category (LCCC) and extensively use ...
2k views

### Category-theoretic treatment of diffs, patches and merging?

Is there a category of patches that looks roughly like this: The objects are strings in some base alphabet The morphisms are edit scripts ("diffs" or "patches") between the strings I'm interested in ...
1k views

### A mathematical (categorical) description of type classes

A functional language can be viewed as a category where its objects are types and morphisms functions between them. How do type classes fit in this model? I assume we should only consider those ...
2k views

### Full Completeness vs Full Abstraction of a program translation

Compiler verification efforts often come down to proving the compiler fully abstract: that it preserves and reflects (contextual) equivalences. Instead of providing full abstraction proofs, some ...
422 views

### Proof theory of biproducts?

A category has biproducts when the same objects are both the products and coproducts. Has anyone investigated the proof theory of categories with biproducts? Perhaps the best-known example is the ...
1k views

### Proof relevance vs. proof irrelevance

I want to use use Agda to help me write proofs, but I am getting contradictory feedback about the value of proof relevance. Jacques Carette wrote a Proof-relevant Category Theory in Agda library. But ...
625 views

### Uses of $\infty$-categories in TCS

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 ...
566 views

### Category theory and parsers — references wanted

Since I'm interested in parsers (mainly in parser expression grammars), I'm wondering if there's some work that gives a categorical treatment of parsing. Any reference on applications of category ...
545 views

### What are the uses of Limits and Colimits of Category Theory in every day problems?

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 ...
495 views

### Are there knot theoretic formulations of NP complete problems?

Are there NP complete(or even NP-hard, or NP) problems that have good topological properties to study. Do NP problems have knot theoretic formulations? We know about #$P$ results about the Jones ...
465 views

150 views

### Do Banach spaces and linear contraction maps form a model of ILL with an exponential?

Recently, I read on the nLab that the category of Banach spaces and linear contractions is small complete, small cocomplete, and monoidal closed. This means that Banach spaces and short linear maps ...
905 views

### Explaining monad transformers in categorical terms

Most resource regarding categorical notions in programming describe monads, but I've never seen a categorical description of monad transformers. How could monad transformers be described in the terms ...
253 views

### Closure ordinals for inductive types with function spaces

Functors built from finite products and sums have closure ordinal $\omega$, detailed nicely in this manuscript by Francois Metayer. i.e. we can reach the inductive type $nat := \mu X. 1 + X$ by ...
772 views

### Hyperdoctrines and Monadic Second Order Logic

This question is essentially the question I asked on Mathoverflow. Monadic Second Order (MSO) logic is second order logic with quantification over unary predicates. That is, quantification over sets. ...
304 views

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

It seems to be well-known that programming languages can't have sums, products and nontermination together. Q1. Is this true? Below (or in the above link I gave) is a partial argument. However, ...
869 views

### Categories a computer scientist should know about

I am a computer scientist with a CS degree from the 80's. I am learning category theory by myself. I am looking for advice about learning category theory. E.g. it is quite helpful in learning category ...
1k views

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

I am lacking a background in theoretical computer science but I would have liked to understand to what kind of theoretical objects C++ concepts corresponds to. Basically, C++ concepts allow to define ...
357 views

### Categorical semantics for non-monotonic logics?

Are there any categorical semantics for non-monotonic logics? It appears that the simple answer to this is "No" since the obvious notion of composition fails for any model of a non-monotonic logic. ...
I've been reading through Bart Jacobs' "Categorical Logic and Type Theory", and lemma 1.8.9 has me stumped. The lemma is stated as follows: Let $p : \mathbb E \to \mathbb B$ and \$q : \mathbb D \to \...