Questions tagged [ct.category-theory]

Questions in category theory

126 questions
Filter by
Sorted by
Tagged with
11k 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 ...
• 27.5k
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 ...
• 2,611
7k 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 ...
4k 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 ...
• 11.1k
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, ...
662 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}$ ...
• 3,566
4k 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 ...
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 ...
• 32.8k
3k 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 ...
• 523
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 ...
• 2,825
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?
3k 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-...
• 2,611
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 ...
• 203
2k 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 ...
• 301
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 ...
• 2,611
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$ ...
• 557
1k 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. -...
• 37.8k
2k 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 ...
• 595
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 ...
• 281
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 ...
813 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 ...
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 ...
283 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 ...
• 1,695
678 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 ...
• 1,261
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 ...
• 646
480 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 ...
• 32.8k
724 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 ...
306 views

Categorical semantics for S5 modal logic?

Does anyone know where I can look to find out what the generally categorical semantics of S5 is? For S4, the answer is well-known: we want a Cartesian closed category with a product-preserving ...
• 32.8k
677 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 ...
413 views

Why Reflexive Graphs for Parametricity?

Looking at models of parametric polymorphism, I am curious why are reflexive graph categories are used? In particular, why do they not include relational composition? In looking at the models, they ...
• 1,695
655 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 ...
• 221
633 views

Implementing "Internal" Languages

One of the most practical consequences of the "Curry-Howard-Lambek" correspondence is that the syntax of many lambda-calucli/logics can be used to perform constructions in a sufficiently structured ...
• 1,695
494 views

• 505
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 ...
• 307
231 views

What is the "standard" lambda-calculus model for bicartesian closed categories?

(I'm familiar with the lambda-calculus, less so with its categorical models.) It is well-known that cartesian-closed categories are in tight correspondence to the simply-typed lambda-calculus with ...
• 2,040
363 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, ...
• 2,069
292 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 ...
• 171
220 views

Understanding the Beck-Chevalley Condition

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 \...
• 323