Questions tagged [ct.category-theory]
Questions in category theory
122
questions
113
votes
7
answers
10k
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.3k
47
votes
2
answers
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,571
33
votes
12
answers
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 ...
- 481
28
votes
3
answers
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 ...
- 11k
28
votes
2
answers
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, ...
28
votes
2
answers
659
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,546
25
votes
3
answers
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 ...
25
votes
2
answers
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.4k
24
votes
1
answer
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 ...
- 503
23
votes
1
answer
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?
- 551
22
votes
3
answers
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,571
22
votes
1
answer
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,775
20
votes
4
answers
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
19
votes
3
answers
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
19
votes
3
answers
3k
views
Reader, Writer monads
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
18
votes
2
answers
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
18
votes
2
answers
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 ...
- 485
18
votes
1
answer
777
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 ...
18
votes
1
answer
968
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. -...
- 36.9k
17
votes
2
answers
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 ...
- 575
17
votes
2
answers
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,571
17
votes
2
answers
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 ...
- 173
17
votes
0
answers
269
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,653
15
votes
2
answers
468
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.4k
14
votes
2
answers
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 ...
- 584
14
votes
2
answers
698
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 ...
- 295
13
votes
3
answers
663
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 ...
user21269
13
votes
0
answers
268
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.4k
12
votes
4
answers
631
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
12
votes
2
answers
580
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,181
12
votes
2
answers
586
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,653
12
votes
2
answers
488
views
Is there such a thing as a weak coalgebra homomorphism?
Given an endofunctor $F : Set \rightarrow Set$, we can define observation functions as functions that are polymorphic for any $F$-coalgebra, that is $obs$ is defined for any $F$-coalgebra $\langle A, ...
- 633
12
votes
1
answer
885
views
Natural Transformations and Parametricity
In Theorems for Free!, Wadler says that the characterization of parametricity can be re-expressed in terms of lax natural transformations and this will be the subject of a further paper. Which paper ...
- 381
12
votes
1
answer
379
views
When do coherence spaces have pullbacks and pushouts?
$\newcommand{\symp}{\Bumpeq}$
A coherence relation $\symp_X$ on a set $X$ is a reflexive and symmetric relation. A coherence space is a pair $(X, \symp_X)$, and a morphism $f : X \to Y$ between ...
- 32.4k
12
votes
1
answer
439
views
Algebraically Compact Categories
I read Freyd's paper "Algebraically Complete Categories" in the famous Como90 and I have two questions about the notion of algebraic compactness he defined in that paper. (If you are not familiar with ...
- 381
11
votes
4
answers
1k
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 ...
- 2,571
11
votes
3
answers
1k
views
What is a good Category Theory-Domain Theory dictionary?
When dealing with the domain theoretic categories (say CPO and $\omega$CPO), I frequently wish for a dictionary for the language of category theory in domain theory.
That is, given a concept, say ...
- 2,667
11
votes
1
answer
385
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,653
11
votes
0
answers
208
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 ...
- 32.4k
10
votes
2
answers
1k
views
What logic correponds via Curry-Howard to a Monad?
According to Moggi's 1991 paper "Notions of computation and monads" one can represent monadic equational logic with the well known monad $(T, \eta, \mu)$ with T an functor and the two natural ...
- 575
10
votes
3
answers
585
views
Is there any known CCC closed under a probabilistic powerdomain operation?
Equivalently, is there a known denotational semantics for probabilistic higher-order functional programming languages? Specifically, is there a domain model of pure untyped $\lambda$-calculus extended ...
- 265
10
votes
2
answers
481
views
Are there semi-decision procedures for this theory?
I have the following typed theory
|- 1_X : X -> X
f : A -> B, g : B -> C |- compose(g,f) : A -> C
F, f : A -> B |- apply(F,f) : F(A) -> F(B)
...
- 221
10
votes
1
answer
193
views
Relating univalence for a theory of cateogries to the skeleton concept
Say I work in homotopy type theory and my sole objects of study are conventional categories.
Equivalences here are given by functors $F:{\bf D}\longrightarrow{\bf C}$ and $G:{\bf C}\longrightarrow{\...
- 505
10
votes
2
answers
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
10
votes
2
answers
566
views
Induction-recursion in models other than $\mathbf{Set}$
It is well-known that various flavors of induction-recursion are consistent*. Typically, this is proven by showing that the standard model of type theory in sets can be extended to include induction-...
- 313
10
votes
0
answers
212
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
9
votes
1
answer
357
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,049
9
votes
2
answers
275
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
9
votes
1
answer
206
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
9
votes
1
answer
822
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. ...
- 12.6k