Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions in category theory

10
votes
0answers
107 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 ...
4
votes
2answers
139 views

What does the category of RDF models look like in Institution Theory?

The Question in short Here is the question in its pure form. Details of my reasoning can be found below. The RDF1.1 spec semantics defines a model to consist of a set IR of objects and IP of ...
2
votes
1answer
63 views

Does an initial algebra for a class have to belong to the class itself?

In the context of algebraic data types, a concept of initial algebras is usually defined, e.g., in the following way: An algebra $S$ is initial in a class $C$ of algebras iff for every $A\in C$ ...
5
votes
2answers
180 views

The chromatic number of a graph as a functor

I was fooling around with some concept and was wondering if this viewpoint is explored at all. Let INJ-GRAPH be the subcategory of graphs (with morphisms as homomorphisms) whose morphisms consist only ...
4
votes
1answer
94 views

What are values relative to Hask?

According to ncatlab's page on category theory and haskell, "we can identify a subset of Haskell called Hask that is often used to identify concepts used in basic category theory. One considers ...
2
votes
2answers
182 views

Moggi's computational metalanguage

In Notions of Computation and Monads Moggi models the notion of a computation of type $A$, $TA$, using a monad $T$. Among other things this ensures the $T\eta$ rule: $$\frac{x: A \vdash a:TB}{x:A \...
13
votes
0answers
159 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 ...
6
votes
1answer
83 views

Can all structurally recursive functions be written without explicit recursion using a catamorphism/fold?

In particular, I am thinking of a function which involves conditionals changing the recursive behavior and multiple F-algebras. ...
6
votes
1answer
200 views

Algebraic account of Gaussian elimination?

For fun, I've been looking at the interpretation of linear logic in terms of finite-dimensional vector spaces, and ran into an interesting question about the interpretation of double-negation-...
6
votes
2answers
285 views

Explicit set of types and terms in MLTT

Whenever I read a presentation of MLTT, especially in the context of the correspondence of MLTT with LCCCs (eg. Seely's paper), they say "the type constructors/formation rules are..." and then list a ...
2
votes
0answers
71 views

Categorical model of binding / first class modules

Binders are explained using presheaves (Pitts/Gabbay A new approach to Abstract Syntax with variable binding) What is the equivalent (categorical) theory to explain first class modules as in 1ML ?
8
votes
2answers
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 ...
5
votes
1answer
108 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 ...
10
votes
1answer
614 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 ...
18
votes
1answer
573 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. -...
5
votes
0answers
109 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 ...
11
votes
1answer
236 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 ...
11
votes
0answers
165 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 ...
15
votes
3answers
594 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 ...
1
vote
0answers
50 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 ...
9
votes
2answers
358 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 ...
9
votes
1answer
229 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, ...
15
votes
2answers
1k 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 ...
1
vote
0answers
79 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 ...
4
votes
0answers
277 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 ...
1
vote
1answer
197 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 ...
2
votes
1answer
197 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 ...
13
votes
2answers
411 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 ...
2
votes
0answers
81 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 ...
10
votes
3answers
508 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 ...
12
votes
3answers
569 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 ...
3
votes
0answers
295 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 \...
27
votes
3answers
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 ...
12
votes
2answers
336 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 ...
9
votes
1answer
120 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{\...
8
votes
2answers
258 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. ...
2
votes
1answer
214 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 $...
32
votes
12answers
4k 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 ...
9
votes
2answers
642 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 ...
6
votes
0answers
219 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 ...
7
votes
3answers
647 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 ...
5
votes
2answers
241 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)$ ...
2
votes
1answer
163 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 ...
2
votes
0answers
73 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 ...
5
votes
0answers
132 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. $...
11
votes
1answer
557 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 ...
8
votes
0answers
168 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-...
5
votes
2answers
1k 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?
11
votes
1answer
302 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 ...
8
votes
4answers
345 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 ...