Questions tagged [ct.category-theory]
Questions in category theory
122
questions
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
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
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
3
votes
1
answer
396
views
What can the Haskell package category-extras be used for?
See here. Has anyone attempted to use this to verify category theoretic proofs? Given the relationship between categories and graphs, are there some applications with respect to graph algorithms? What ...
- 133
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 ...
2
votes
2
answers
411
views
Difference between Stencil -structures and Cellular Automata Category-theoretically?
Definitions
Stencil =
"For a given point, a stencil is a pre-determined set of nearest
neighbors (possibly including itself)."
(source)
Wikipedia's definition (source) =
It looks ...
- 71
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
4
votes
5
answers
418
views
Advantages and specific applications of massively parallel programming thesis idea
I'm nearly graduated in computer science engineering and my thesis should discuss the massively parallel computational model of CUDA and its advantages/applications.
I'm searching for an application ...
- 43
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
-6
votes
1
answer
363
views
What function has the signature $ A \times \left ( B + C \right ) \rightarrow \left ( A \times B \right ) + \left ( A \times C \right ) $?
$ A \times \left ( B + C \right ) $ is isomorphic to $ \left ( A \times B \right ) + \left ( A \times C \right ) $, right? That means there's a function from one to the other and another function back....
- 1
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
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
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
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
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
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, ...
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
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
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
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
7
votes
1
answer
183
views
Maximal subcoalgebras of an $F+1$-coalgebra corresponding to an $F$-coalgebra
This context of this question is Rutten's Universal Coalgebra, used for modelling systems.
I'm interested in finding a description of a functor between different types of coalgebras
corresponding to ...
- 16.7k
6
votes
2
answers
651
views
Proof of a unique homomorphism from an initial object
What is the proof that there is only one homomorphism from an initial object to another object?
- 293