Questions tagged [ct.category-theory]

Questions in category theory

Filter by
Sorted by
Tagged with
5 votes
1 answer
299 views

Does the Category of CPOs have omega^op limits?

In "Domains and Lambdi Calculi" by Amadio and Curien, in the section on solving recursive domain equations (section 7), they give sufficient conditions on a cpo-enriched category so that the category ...
Max New's user avatar
  • 1,653
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 ...
Chill2Macht's user avatar
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. -...
Joshua Grochow's user avatar
4 votes
0 answers
116 views

Transferring results on coalgebras in one category to another

Let $F$ and $G$ be endofunctors over categories $C$ and $ D$, respectively. Suppose that there is a forgetful functor $C \to D$ that has a left adjoint. Can we infer properties of $F$-coalgebras ...
Pteromys's user avatar
  • 895
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 ...
Max New's user avatar
  • 1,653
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 ...
Neel Krishnaswami's user avatar
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 ...
Saal Hardali's user avatar
1 vote
0 answers
55 views

How to read this formula for composition in an asynchronous interaction category?

The paper is available here Interaction Categories and the Foundations of Typed Concurrent Programming Abramsky, Gay, Nagarajan p.38 composition of two processes $p:A \rightarrow B$, $q:B \rightarrow ...
Spearman's user avatar
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 ...
Max New's user avatar
  • 1,653
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, ...
Blaisorblade's user avatar
  • 2,049
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 ...
k.stm's user avatar
  • 281
1 vote
0 answers
85 views

Categorical way of factoring out points

Major rewrite justifiably asked for: I'm currently trying to get a categorical way of doing something called the Gelfond-Lifschitz reduct on a set of single-headed Horn clauses. The semantics is the ...
David Boshton's user avatar
4 votes
0 answers
341 views

Category theory in plain MLTT

I want to define a category in simple MLTT (not in HoTT). I defined it with the help of setoids. I.e. category consists of: a type of objects with equivalence relation (Obj : Set) a type of arrows ...
Konstantin Solomatov's user avatar
1 vote
1 answer
312 views

How can I formalize key value stores with set theory? [closed]

I'm currently developing a simple key-value NoSQL store and want to build its formal model. I'm interested in knowing if there some work about formalization of key-value stores outside of category ...
MainstreamDeveloper00's user avatar
3 votes
1 answer
291 views

What are the morphisms of Adj(C,T) - the category whose objects are the adjunctions of a given monad?

The Wikipedia page for Monad says just that for a monad $(T,\eta,\mu)$ we can define the category of all adjunctions that define the monad: Let $\textbf{Adj}(C,T)$ be the category whose objects ...
Petr's user avatar
  • 2,571
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 ...
Rodrigo Ribeiro's user avatar
2 votes
0 answers
93 views

How to derive a monoid's append from category theory [closed]

As I understand, a monoid $M$ is just a special kind of category; it has only one object and its morphisms can be composed through a composition operation. In principle, if $a$ is the object of the ...
Vittorio Zaccaria's user avatar
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 ...
fritzo's user avatar
  • 265
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 ...
user avatar
3 votes
0 answers
545 views

Distributive law between monads in Haskell

A distributive law between monads must satisfy laws that are usually given in terms of the units $\eta$ and multiplications $\mu$ of the two monads. Among the four laws there are: $\mu^S T \circ S l \...
Bob's user avatar
  • 381
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 ...
vzn's user avatar
  • 11k
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 ...
user3483902's user avatar
  • 1,181
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{\...
Nikolaj-K's user avatar
  • 505
8 votes
2 answers
423 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. ...
David Boshton's user avatar
3 votes
1 answer
311 views

understanding programming monads through diagrams

I am trying to understand better how the category definition of monad is related to the computer science definition. nlab has a rather terse definition of Monad in terms of a bicategory. an object $...
john mangual's user avatar
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 ...
spaceman_spiff's user avatar
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 ...
Petr's user avatar
  • 2,571
6 votes
0 answers
273 views

Generalizing Haskell: could we replace Hask with Cat?

N.B. I asked the same question on Stack Overflow but it was suggested that it is too theoretical for this forum. It is great that Haskell allows us to walk around in the category $Hask$. But ...
Bob's user avatar
  • 381
8 votes
3 answers
984 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 ...
Guy Coder's user avatar
  • 199
6 votes
3 answers
491 views

Isomorphism between algebraic data-types

I have two types of trees in Haskell, defined as the least solution of the following equations: $T_1(A) \cong 1 + A + T_1(A) \times T_1(A)$ $T_2(A) \cong 1 + A \times T_2(A) + T_2(A) \times T_2(A)$ ...
resnick's user avatar
  • 71
3 votes
1 answer
268 views

Faithful functors vs forgetful functors: exact category-theoretic defs?

In category theory, a functor between two categories $C,D$ is a map $F$ that assigns to each object (resp. morphism) $x$ of $C$ a corresponding object (resp. morphism) $F(x)$ of $D$ by respecting the ...
Super8's user avatar
  • 314
2 votes
0 answers
76 views

Composition series and isogeny

I'm not sure this question is appropriate for this site, but it might have some connections with computational algebra. Consider a fixed "category" $\sf{Cat}$ (in the sense of category theory, but ...
NisaiVloot's user avatar
  • 1,292
5 votes
0 answers
143 views

Structures admitting directed sums and directed products?

Some structures have a property of closure by a "sum" or "product" operation. Given a family of structures $(S_i)_{i \in I}$, we can then define a new structure denoted by $\sum_{i \in I} S_i$, resp. $...
NisaiVloot's user avatar
  • 1,292
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 ...
sonat's user avatar
  • 381
8 votes
0 answers
181 views

Equivalence of categories of directed complete posets

I asked this question there: https://math.stackexchange.com/questions/700975/equivalence-of-categories-of-directed-complete-posets. Since I had no answer, I try here. In the book ``Domains and Lambda-...
user21929's user avatar
  • 181
8 votes
3 answers
3k views

What's the relation between OOP and category theory?

What's the relation between OOP and category theory? Is there some related work on this topic one can read?
qazwsx's user avatar
  • 559
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 ...
sonat's user avatar
  • 381
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 ...
James's user avatar
  • 221
5 votes
1 answer
1k views

In what sense are Scala's Try[T] and Future[T] dual?

In a recent course based on Scala I found a hint that the Scala types Try[T] and Future[T] are dual. This was explained only ...
Giorgio's user avatar
  • 151
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 ...
Phillip Mates's user avatar
4 votes
1 answer
355 views

Learning road map for functional programming from the viewpoint of category theory

I am now considering about studying functional programming from the viewpoint of category theory. There are a lot of books about functional programming and category theory, I want some suggestions ...
spaceman_spiff's user avatar
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. ...
Vijay D's user avatar
  • 12.6k
5 votes
0 answers
236 views

What's the connection between these two categories of games and innocent strategies?

Lately I've been reading a lot about game semantics and in particular the problem of PCF's full abstraction. I'm trying to understand how the definition from this article relates to the one found in ...
Bakuriu's user avatar
  • 151
0 votes
1 answer
183 views

Static structure of program

Firstly, I admit that my question is just something very blurred but I hope someone please give me some documents to read. The execution of a program $P$ can be considered as a sequence of state ...
Ta Thanh Dinh's user avatar
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 ...
Darius Jahandarie's user avatar
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 ...
day's user avatar
  • 2,775
-1 votes
1 answer
228 views

Newbie question: Meta-functions?

Consider a function F that takes a function and produces a function based on structure of the input function. As an example consider F that takes all functions having at least two conditionals and ...
Andrew Butenko's user avatar
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-...
Petr's user avatar
  • 2,571
6 votes
1 answer
329 views

In what sense are coroutines dual to (sub)routines?

The name coroutine suggests that in some sense they should be dual to (sub)routines. Is there a real mathematical duality? I'm hoping for something like "in category theory subroutines are X and ...
Petr's user avatar
  • 2,571
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?
Alexey Romanov's user avatar