21
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(...
- 28.1k
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, ...
- 32.3k
17
votes
Status quo of category theory and monads in theoretical computer science research?
There have been a number of developments with regards to the use of monads in the theory of computation since Eugenio Moggi's work. I am not able to give a comprehensive account, but here are some ...
- 28.1k
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 ...
- 28.1k
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 ...
- 36.7k
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 ...
- 9,595
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 ...
- 1,530
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 ...
- 32.3k
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-...
- 146
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 ...
- 32.3k
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 ...
- 32.3k
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 ...
- 16.7k
11
votes
What's the relation between OOP and category theory?
There are absolutely some relationships between the semantics and practice of OOP and category theory. This is somewhat unsurprising since both fields attempt to give a principled generic account of ...
- 13.7k
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. ...
- 11.3k
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 ...
- 32.3k
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 ...
- 28.1k
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 ...
- 2,030
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 ...
- 32.3k
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.
...
- 32.3k
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 ...
- 28.1k
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)...
- 1,638
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 ...
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 ...
- 668
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 ...
- 32.3k
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 ...
- 28.1k
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 ...
- 1,530
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 ...
- 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 ...
- 633
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 ...
- 2,017
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 ...
- 28.1k
Only top scored, non community-wiki answers of a minimum length are eligible