39
There are actually two uses of the word "strength" in play here.
A strong endofunctor $F : C \to C$ over a monoidal category $(C, \otimes, I)$ is one which comes with a natural transformation $\sigma : A \otimes F(B) \to F(A \otimes B)$, satisfying some coherence conditions with respect to the associator which I will gloss over. This condition is sometimes ...
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
As it happens, I'm writing a paper about this now. IMO, a good way to think about futures or promises is in terms of the Curry-Howard correspondence for temporal logic.
Basically, the idea behind futures is that it is a data structure representing a computation that is in progress, and upon which you can synchronize. In terms of temporal logic, this is the ...
24
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
How do type classes fit in this model?
The short answer is: they don't.
Whenever you introduce coercions, type classes, or other mechanisms for ad-hoc polymorphism into a language, the main design issue you face is coherence.
Basically, you need to ensure that typeclass resolution is deterministic, so that a well-typed program has a single ...
18
There has been a lot done applying category theory to regular languages and automata. One starting point is the recent papers:
Bialgebraic Review of Deterministic Automata, Regular Expressions and Languages
by Bart Jacobs
A Bialgebraic Approach to Automata and Formal Language Theory by James Worthington.
In the first of these papers, the structure of ...
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 ...
17
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 ...
16
There is not a canonical such category, for the same reason there is no canonical category of computations. However, there are large and useful algebraic structures on data structures.
One of the more general such structures, which is still nevertheless useful, is the theory of combinatorial species. A species is a functor $F : B \to B$, where $B$ is the ...
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. ...
15
Indeed, there is a different notion than isomorphism which is more useful in programming. It is called "behavioural equivalence" (sometimes called "observational equivalence") and it is established by giving a "simulation relation" between data structures rather than bijections. Algebraists came in and established an area called "algebraic data types" in ...
15
First of all:
Any monad is also an applicative functor and any applicative functor is a functor.
This is true in the context of Haskell, but (reading Applicative as "strong lax monoidal functor") not in general, for the rather trivial reason that you can have "applicative" functors between different monoidal categories, whereas monads (and comonads) are ...
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
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 : [...
14
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
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 ...
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 ...
12
Actually, I think what you're looking for is Kleene algebra. See Dexter Kozen's classic article. He gives an axiomatization of Kleene-star. I assume this is the very first step you're interested in.
A completeness theorem for Kleene algebras and the algebra of regular events. Information and Computation, 110(2):366-390, May 1994.
That article does not ...
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 ...
11
I think you are asking two questions about applicability, type A and type B separately.
As you note, there are many substantive applications of category theory to type B topics: semantics of programming languages (monads, cartesian closed categories), logic and provability (topoi, varieties of linear logic).
However, there seems to be little substantive ...
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 ...
Only top voted, non community-wiki answers of a minimum length are eligible
