22 votes
Accepted

Proof relevance vs. proof irrelevance

There are several possible notions of proof relevance. Let us consider three similar situations: An element of a sum $\Sigma (x : A) . P(x)$ is a pair $(a, p)$ where $a : A$ and $p$ is a proof of $P(...
Andrej Bauer's user avatar
  • 28.9k
20 votes

Is there a relationship between relational algebra/calculus and category theory?

Categorical approaches to query languages is a bit of a niche interest, but I think it's a very interesting niche! Two of the key figures in this area are Peter Buneman and Torsten Grust. Obviously, ...
Neel Krishnaswami's user avatar
15 votes

"The" category of Turing machines?

You might be interested in Turing categories by Robin Cockett and Pieter Hofstra. From the point of view of category theory the question "what is the category of Turing machines" is less interesting ...
Andrej Bauer's user avatar
  • 28.9k
15 votes

"The" category of Turing machines?

If your objects are Turing machines, there are several reasonable possibilities for morphisms. For example: 1) Consider Turing machines as the automata they are, and consider the usual morphisms of ...
Joshua Grochow's user avatar
14 votes

Does the uncomputability of Kolmogorov complexity follow from Lawvere's Fixed Point Theorem?

EDIT: Adding the caveat that Roger's fixed-point theorem may not be a special case of Lawvere's. Here is a proof that may be "close"... It uses Roger's fixed-point theorem instead of Lawvere's ...
Neal Young's user avatar
  • 10.6k
14 votes

Proof relevance vs. proof irrelevance

I recommend that everyone first read Andrej Bauer's answer, as he covers all the basics extremely well. I agree with everything he says in his answer. I humbly offer more comments, even though I know ...
Jacques Carette's user avatar
13 votes
Accepted

What logic correponds via Curry-Howard to a Monad?

The two papers to look at it are Benton, Bierman and de Paiva's Computational Types from a Logical Perspective, which directly gives a proof theory for Moggi's computational lambda-calculus; and Rowan ...
Neel Krishnaswami's user avatar
13 votes
Accepted

Category-theoretic treatment of diffs, patches and merging?

As pointed by Martin, there is some work on the categorical representation of patches. Mimram and Di Giusto's "A Categorical Theory of Patches" being the most extensive categorical approach to edit-...
Victor Miraldo's user avatar
12 votes
Accepted

What kind of theoretical object corresponds to a C++ concept?

From a programming language theory perspective, as opposed to the computability perspective other answers and comments have offered, C++ templates combined with concepts correspond to bounded ...
Dave Clarke's user avatar
  • 16.7k
12 votes
Accepted

A bicartesian closed category of strict complete partial orders (Hask)

Yes, it's impossible to have a nondegenerate CCC with general recursion and categorical coproducts. The standard reference for this is: H. Huwig and A. Poigne. A note on inconsistencies caused by ...
Neel Krishnaswami's user avatar
12 votes
Accepted

"The" category of Turing machines?

Saal Hardali mentioned that he wanted a category of Turing machines to do geometry (or at least homotopy theory) on. However, there are a lot of different ways to achieve similar aims. There is a ...
Neel Krishnaswami's user avatar
8 votes

Category-theoretic treatment of diffs, patches and merging?

There is quite a bit of work in this direction. You could start by looking at [1, 2], but they don't exhaust the topic. S. Mimram, C. Di Giusto, A Categorical Theory of Patches. C. Angiuli, E. ...
Martin Berger's user avatar
8 votes

Categorical equivalent of higher order logic

The structure you want is due to Andy Pitts, and is called a tripos. It extends the notion of hyperdoctrine, which gives a categorical model for first-order logic, with enough structure to model ...
Neel Krishnaswami's user avatar
8 votes
Accepted

Categorical equivalent of higher order logic

It seems to me there isn't an agreement about what "HOL" means. The OP indicates in their question that they are thinking of the formalization of higher-order logic within the formalism of ...
Andrej Bauer's user avatar
  • 28.9k
7 votes
Accepted

Implementing "Internal" Languages

In Extending Type Theory with Forcing by Guilhem Jaber, Nicolas Tabareau and Matthieu Sozeau, 2012, intuitionistic forcing is presented as an internalization of the presheaf construction, implemented ...
gasche's user avatar
  • 2,040
7 votes
Accepted

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

Your function is completely structurally recursive on n, so it is pretty much just a change of notation to make it a catamorphism on the natural numbers. ...
Neel Krishnaswami's user avatar
7 votes

Explicit set of types and terms in MLTT

How do you actually construct the sets of types and terms (more) formally in set theory, and convince me that these actually do form a set? It's essentially the same argument that BNF grammars ...
Neel Krishnaswami's user avatar
7 votes

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

Yes, the initial algebra is by definition one of the members of the class for which it is initial. You may however be interested in the category-theoretic concept of a limit. Given a diagram (a ...
Andrej Bauer's user avatar
  • 28.9k
7 votes
Accepted

Understanding the Beck-Chevalley Condition

So we need to construct a natural transformation $\phi : K(I)u^\# \Rightarrow u^*(K(J))$, which are functors from $D_J$ to $E_I$. So for every $d \in D_J$ we need a morphism $K(I)(u^\#(d)) \to u^*(K(J)...
Max New's user avatar
  • 1,675
7 votes
Accepted

Composition with recursion in functions between types

(I'm going to try to write an answer for functional programmers, with Haskell-like code.) First, you should know that using higher-order functions, recursive definitions can be turned into fixed-point ...
Lê Thành Dũng 'Tito' Nguyễn's user avatar
6 votes
Accepted

What are values relative to Hask?

At the level of precision used in the nlab page, values are global elements -- i.e., a value of type $A$ corresponds to a morphism $1 \to A$. If you want to be serious about this, there are some ...
Neel Krishnaswami's user avatar
6 votes
Accepted

Does the Category of CPOs have omega^op limits?

Here's an attempt (please check!). We have that $\bot_D = d$, where $$ d_i = \bigsqcup^{D_i} \{\bot_i,f_i(\bot_{i+1}),f_i(f_{i+1}(\bot_{i+2})),\ldots\} $$ By construction (and monotonicity), the ...
chi's user avatar
  • 668
5 votes

Moggi's computational metalanguage

It is an interesting problem to figure out what bothers the OP. First of all, it is not at all the case that the equation put forward by the OP says "different computations have the same value". For ...
Andrej Bauer's user avatar
  • 28.9k
5 votes

Algebraic account of Gaussian elimination?

You really should read Gowers' essay carefully - it cleanly details the reasons why you need a basis in general. So if there is going to be an algebraic account of Gauss-Jordan, it will necessarily ...
Jacques Carette's user avatar
5 votes

Algebra oriented branch of theoretical computer science

Here are a lot of interesting answer, but nobody mentioned that every language $L \subseteq X^{\ast}$ is naturally associated with a monoid structure via the Nerode-Myhill congruence relation. The ...
StefanH's user avatar
  • 2,077
5 votes

Solid applications of category theory in TCS?

The more recent book Seven Sketches in Compositionality lists several applications of category theory in computer science and engineering. Notable the chapter on databases where the authors describe ...
michid's user avatar
  • 151
5 votes

Solid applications of category theory in TCS?

"TCS-A" applications that come to my mind are Joyal's combinatorial species (generalisations of power series to functors so as to describe combinatorial objects like trees, sets, multisets, etc) and ...
Martin Hofmann's user avatar
5 votes

What's the relation between OOP and category theory?

Bart Jacobs tackled this problem at one point. In his view, classes can be considered as coalgebras. Roughly, we have a polynomial endofunctor $F : \mathbf{Sets} \to \mathbf{Sets}$ which gives the ...
Kevin Clancy's user avatar
5 votes

Implementing "Internal" Languages

If you're going to work only in the internal language then you can just use a proof assistant. There is a minor technicality of having or not having powersets, since proof assistants are typically ...
Andrej Bauer's user avatar
  • 28.9k
5 votes

What logic correponds via Curry-Howard to a Monad?

I'll add this in addition to Neel Krishnaswami's answer. The article he refers to A Judgemental Reconstruction of Modal Logic cites the article by Satoshi Kobayashi Monad As Modality which I had come ...
Henry Story's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible