34
One is internal and the other is external.
A category $\mathcal{C}$ consists of objects and morphisms. When we write $f : A \to B$ we mean that $f$ is a morphism from object $A$ to object $B$. We may collect all morphisms from $A$ to $B$ into a set of morphisms $\mathrm{Hom}_{\mathcal{C}}(A,B)$, called the "hom-set". This set is not an object of $\mathcal{C}...
28
Grothendieck's inequality, from his days in functional analysis, was initially proved to relate fundamental norms on tensor product spaces. Grothendieck called the inequality "the fundamental theorem of the metric theory of tensor product spaces", and published it in a now famous paper in 1958, in French, in a limited circulation Brazilian journal. The paper ...
27
There have been recent developments in dependent type theory which relate type systems to homotopy types.
This is now a relatively small field, but there is a lot of exciting work being done right now, and potentially a lot of low hanging fruit, most notably in porting results from algebraic topology and homological algebra and formalizing the notion of ...
25
Algebraic geometry is used heavily in algebraic complexity theory and in particular in geometric complexity theory. Representation theory is also crucial for the latter, but it's even more useful when combined with algebraic geometry and homological algebra.
18
Semantically, a coercion $c : A \leq B$ is just a morphism $c : A \to B$, which gets added to the interpretation of terms at the appropriate points. The basic problem this creates is the issue of coherence: are you guaranteed that a term will have a unique meaning, given that the same term can potentially have coercions hidden in many possible places in the ...
18
Grothendieck's impact can be felt in type theory and logic. For instance, Bart Jacobs' 700+ page volume Categorical Logic and Type Theory gives a uniform treatment of various type theories ($X$-type theory, where $X\subseteq \{ \text{simple},$ $\text{dependent},$ $\text{polymorphic},$ $\text{higher-order}\}$) based on the categorical notion of Grothendieck ...
18
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, they didn't do all the work, but if you start with their papers and trace out the citation graph, you'll get pretty good coverage of the area.
The central ...
16
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 points that I am familiar with, others can chime in with their answers.
Specific examples of monads
You do not have to study super-general theory all the time. ...
16
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(a)$.
An element of $\Sigma (x : A) . \|P(x)\|$, where $\|{-}\|$ is propositional truncation, is a pair $(a, q)$ where $a : A$ and $q$ is an equivalence class ...
15
Your knowledge of field theory would be useful in cryptography, while category theory is heavily used in the research on programming languages and typing systems, both of which are closely related to the foundations of mathematics.
15
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 automata (maps between the alphabets and the states that are consistent with one another) which also either preserve the motions of the tape head(s), or exactly ...
14
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 theorem. (See comment section below for further discussion.)
Let $K(x)$ be the Kolmogorov complexity of string $x$.
lemma. $K$ is not computable.
Proof.
...
14
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-scripts as used by the UNIX diff.
In their sense, you have what you want. The objects are finite sequences of words over an alphabet $L$, seen as a mapping $A : [...
13
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 than "what is the categorical structure which underlies computation". Thus, Robin and Pieter identify a general kind of category that is suitable for developing ...
13
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 less on this topic than he does - but I was mentioned by name, as was my project.
When I gave a talk about agda-categories, I explained one thing about it that ...
12
Unfortunately, there are too many things are going on here. So, it is easy to mix things up. The use of "full" in "full completeness" and "full abstraction" refer to completely different ideas of fullness. But, there is also some vague connection between them. So, this is going to be a complicated answer.
Full completeness: "Sound and complete" is a ...
12
Any applications of $p$-adic cohomology, etale cohomology in point counting formulas for algebraic varieties has roots in his work.
I am guessing Mulmuley's vision of generalization of Riemann hypothesis over finite fields coming from the Weil conjectures can be thought of as asking questions which originally had fruitful results from Grothendieck's etale ...
12
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 very strong analogy between computability and topology. The intuition is that termination/nontermination is like the Sierpinski space, since termination is ...
11
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 structure and behavior in a synthetic manner.
The most apparent work I am aware of is the categorical semantics of UML, which is admittedly different from OOP ...
11
Field theory and algrebraic geometry would be useful in topics related to error correcting codes, both in the classical setting as well as in studying locally decodable codes and list decoding. I believe this goes back to work on the Reed-Solomon and Reed-Muller codes, which was then generalized to algebraic geometric codes. See for example, this book ...
11
I refer you to Chapter 9 of the HoTT book. In particular, a category is defined in such a way that isomorphic objects are equal, see Definition 9.1.6. As Example 9.1.15 points out, there really isn't a reasonable notion of "skeletality" in HoTT. This is so because equality is so weak that it already means "isomorphic".
Furthermore, Theorem 9.4.16 says
...
11
You can take a look to:
Peter Golbus, Robert W. McGrail, Tomasz Przytycki, Mary Sharac, and Aleksandar Chakarov. 2009. Tricolorable torus knots are NP-complete. In Proceedings of the 47th Annual Southeast Regional Conference (ACM-SE 47). ACM, New York, NY, USA, , Article 42 , 6 pages.
Abstract: This work presents a method for associating a class of ...
11
Applying higher homotopy-theoretic ideas to CS is still a very nascent field! My understanding is that it's not even that old as a mathematical field.
Certainly HoTT is the central impetus for such ideas. Even there though, there only have been few applications of category theory of "dimension" higher than 2.
One nice "computer science-y" one is ...
11
Theoretical computer scientists do many things, one of which is mathematical modeling of various computer-sciency things. For instance, we like to provide mathematical models of programming languages, so that people can actually prove things about programs (such as proving that the program does what it's supposed to). In this sense it is always good to have ...
11
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 fixpoints in a cartesian closed category. Theoretical Computer Science, 73:101–112, 1990.
However, I and (most of the other people I've met) learned about it ...
11
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 polymorphism or constrained genericity. Concepts themselves correspond to the constraints or bounds placed on a type.
A template is type-level function, parameterised ...
10
In this post on SO I found an interesting answer - decisive functors. If we replace () by Void, (,) by Either and reverse the arrows, we get:
class Functor f => Decisive f where
nogood :: f Void -> Void
orwell :: f (Either s t) -> Either (f s) (f t)
The blog post also gives some laws that decisive functors adhere to.
And, every Comonad is ...
10
The short answer is: they are not dual.
The Try[T] type is basically the sum type $T + E$, where $E$ is the type of exceptions.
A typical way of rendering a future Future[T] is via temporal logic. Here, a future can be understood as a "weak eventually" operator, $\Diamond T$, saying that at some point in the future you may receive a $T$. This can be ...
10
The following is an extended comment, it does not answer your question in the terms you posed it but does give a semantics for higher-order probabilistic calculi which you may find of interest.
In the past few years there has been a very active line of research around so-called quantitative denotational semantics of linear logic, based on the idea (...
10
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 Davies and Frank Pfenning's A Judgmental Reconstruction of Modal Logic, which gives a constructive proof theory for S4 modal logic with box and diamond, and ...
Only top voted, non community-wiki answers of a minimum length are eligible
