I just recently stumbled upon the "univalent foundations" approach to mathematics, i.e. homotopy type theory (HoTT), and holy schnikes this is a deep rabbit hole to fall into. It would appear that category theory and set theory can both be represented in HoTT.
I think the world is not going to reap the true benefits of computers for scientific progress until we systematize formal knowledge within a single shared syntactical universe. Open science means nothing if it has become so siloed and complex that results are largely unverified and frequently unverifiable.
It's not really a matter of what formal system is most powerful. It's a matter of what formal system can represent ordinary math in the simplest and clearest fashion. I think this what proponents of category theory argue. Basically, category theory lets one take many standard mathematical theorems and generalize them widely - ie, lot of standard math theories can be seen as theories about categories and when you see them that way, the generality of a category means the theorem applies broadly.
This kind of foundational (ZFC,CT,HTT) stuff is pretty niche in mathematics.
Set theory, though touted as the foundation of math, isn't really used to its full extremes (HOD, etc) by anyone but set theorists. Its more like... A common datatype?
And while CT could also be a foundation, as far as im aware its only practical uses as a tool are found in commutative algebra.
I think the truth is that most math is pretty simple to describe and doesn't require a grand framework to formalize.
All formal systems have their limitations as far as what is provable.
Example:, for any statement
A
unprovable in a particular formal system
F
, there are, trivially, other formal systems in which
A
is provable (take
A
as an axiom). On the other hand, there is the extremely powerful standard axiom system of Zermelo-Fraenkel set theory (denoted as ZF, or, with the axiom of choice, ZFC), which is more than sufficient for the derivation of all ordinary mathematics. Now there are, by Gödel’s first theorem, arithmetical truths that are not provable even in ZFC. Proving them would thus require a formal system that incorporates methods going beyond ZFC. There is thus a sense in which such truths are not provable using today’s “ordinary” mathematical methods and axioms, nor can they be proved in a way that mathematicians would today regard as unproblematic and conclusive.
An interesting thing happened when category theory was used to model sets. It turned out set membership was problematic. When wearing your category theory glasses "parameterized elements" (subobject classifier) were the natural thing. Think tangent planes to a sphere instead of points on a sphere.
Naive outsider intuition is that you can encode all category theorems as graphs, but only because you can encode anything as a graph, and the property of category theory that could make it a universal modelling language is really just an artifact of it being a way to talk about things that can be encoded as graphs.
At best, perception may be graphs all the way down. As though we were living in a simulation specified by a Matrix of adjacencies.
The main thing categories add to graphs is identifications of paths. Every pair of edges f: A -> B and g : B -> C generates a third edge g.f, and we identify the path (g)(f) with the new edge (g.f). Not only that, we add h.(g.f) = (h.g).f for any h: C -> D, which basically says that "." acts like concatenation of paths (it doesn't matter how you group the edges in a path, you get the same thing).
Those are the basic axioms to say you're working with a nice operation that turns paths into edges in a reasonable way. It gets interesting when you add more identifications (commutative diagrams) and operations (functors). Prototypical example: vertices are sets, edges are functions, you get identification of paths (sequential compositions of functions) whenever the underlying composite functions are pointwise equal.
Categories aren't just graphs; they have additional properties, the most important of which is composition (ex. function composition). They can also be thought of as a type algebra, like groups or rings, but again with different properties.
Edit: these extra properties allow you to reason about a wide class of problems when they're represented as categories, not just round trip them from unencoded to encoded to unencoded. For example, Pijul uses a category of patches to model file patching and prove certain properties of the version control system.
While Category Theory does make an extensive use of the language of diagrams, this in no way implies that it can be reduced to them. Category Theory is much deeper than graph theory. In fact, the very notion of a category should be seen as ancillary to the much more important concept of a functor (which, in turn, if you believe the word of the founders, was only needed to provide a base for a rigorous definition of natural equivalence).
Visual perception and perhaps touch because there is a general mutual exclusivity of visual and tactile 'things' (once you draw a boundary around them.)
But taste, smell, and sound ... you can't so readily and purely taxonomize these...
As an engineer looking in from the outside of academia, all of the discussion I see pop up around Category Theory seems hauntingly similar to ideas discussed when producing SQL schemas in well-normalized databases.
Is 3NF/BCNF something that can be described in terms of Category Theory?
I always felt like there was some super deep & fundamental link between these mathematical concepts and relational modeling ideas. Reading "Out of the Tar Pit" was a big trigger for me on connecting dots between imperative/functional/relational programming as well as implications that a good combination of these things would have positive impact on domain modeling.
The answer is yes. There's even a notion of 'categorical normal form' that extends 3NF that guarantees the direct representability of such relational databases as set-valued functors. Spivak talks about it in e.g. http://math.mit.edu/~dspivak/informatics/FunctorialDataMigra...
That's precisely what it is. Homotopy/Category theory is strongly-normalising.
Which is roughly what the Univalence axiom tells us: identity is equivalent to equivalence.
The identity type is the normal/canonical/unique form for all object of a particular type.
Yet another perspective is the question "Do A and B have the same structure? Are they isomorphic?". When you are dealing with finite data types the answer to such questions is inevitably in the domain of Finite Model Theory ( https://en.wikipedia.org/wiki/Finite_model_theory ). Finite categories are the same sort objects as DB schemas.
> I always felt like there was some super deep & fundamental link between these mathematical concepts and relational modeling ideas.
The relational model is relies on set theory (more specifically relational algebra). An alternative view on data and data modeling is based on 1) sets, and 2) functions, and is called the concept-oriented model [1, 2]. It is actually quite similar to category theory and maybe even could be described in terms of category theory. It is also quite useful for data processing and there is one possible implementation which is an alternative to map-reduce and join-groupby approaches [3].
[3] https://github.com/asavinov/prosto Prosto is a data processing toolkit radically changing how data is processed by heavily relying on functions and operations with functions - an alternative to map-reduce and join-groupby
The categorical databases formalism is also known as 'sketches'. For example, here are some slides from NASA et al that connect to David's work but use this alternative phrasing. It shows how to use category theory to 'align' ontologies, with an example about voting. https://www.nasa.gov/sites/default/files/ivv_wojtowicz_sketc...
What's the tradeoff? I mean, how smart you need to be to produce/understand something useful.
Modelling is about communication and understanding, if the language is expressive, precise and utterly abstruse for most people, it's a niche application at most (and it's likely very valuable in its niche).
There's a reason most informal methods become more popular.
I can imagine that there is some theorem that says Category theory is a universal modeling language in some sense. For example, it includes all of set theory, so it "includes" everything classical math can model.
But the real question is whether it is a _useful_ modeling language for everything. Engineers know everything has a tradeoff, and category theorists would do well to recognize the limitations of their tools or risk turning people (like me) away after years of study.
The trade-off has to do with computability: because (finitely presented) categories can express so much, reasoning about them (for example, the 'word problem' for them) is undecidable. So to use CT as a modeling language requires automated theorem proving techniques, which are computationally expensive, and fast reasoning is a large part of what we're commercializing.
> But the real question is whether it is a _useful_ modeling language for everything.
Category theory is definitely not useful for modeling everything. However, it's useful for modeling a whole lot. Categories have few axoims, and those they do have align well with how humans break down complex problems, so a lot of systems can be modeled neatly with categories. And category models are useful for proving existence, uniqueness, and notions of "maximum" and "minimum" for their "arrows", which are often useful things people try to prove about systems.
It's a really nice framework though, but there's plenty (pleeeeenty!) of things that lie beyond its scope.
Idealizing CT and its applications only does more harm than good to the field.
Edit: Sure, I'll be glad to talk about it. Have plenty of experience doing (also, avoiding doing) things w/ CT. Just drop me an email (see profile), you're always welcome.
Isn't there supposed to be a nice three-way equivalence between certain systems of logic, category theory, and lambda calculus? Presumably something that lies beyond the scope of CT also lies beyond the scope of those other systems.
The problem is that RDBMS do not structure information as humans do, making them very bad at modeling and working with information as we humans do. We think in a graph of relationships which we recurse through constantly. These are the two worst things that RDBMS do, so the architecture of data is simply wrong for the job.
Relational databases as introduced by Codd AFAIK are pretty much just storages for Prolog's fact statements: they map exactly one-to-one. The underlying data structures used for implementation (B-trees etc.) may or may not be optimal for the Prolog-style queries, of course.
Sure, but Category theory can handle recursion. See Section "6.6 Application: Primitive Recursion" of "OLOGS: A CATEGORICAL FRAMEWORK FOR KNOWLEDGE REPRESENTATION" (http://math.mit.edu/~dspivak/informatics/olog.pdf).
Are there any prominent category theorists who are not “characters” and present it in a humble / conventional style of mathematical exposition? A lot of the style of presentation of CT is off-putting.
I got into informatics and ontology because I stumble across David's paper on ologs. Years later and I'm still waiting for someone to implement a knowledge representation system that uses them, and hoping that it won't end up being me.
I have learned enough Category theory to realise that it isn’t helpful in solving any software design/programming problems I care about. And also that Type theory is a much simpler and cleaner foundation for math than Category theory.
The formalization of what it means for modules to exist and compose with each other is valuable, but learning category theory as a mathematician would is not sufficient for grokking this. Category theory's insights are often obscured by terminology that fails to reify the abstractions at a level where its wide scope becomes clear.
The candidate I would push forward as the proper reification would be Mark Burgess' Promise Theory. Mark's starting point isn't, "what's the most general algebra I can form for encoding mathematical objects", but "what happens if I generalize points in spacetime to be a special case of any kind of graph". When you do this, you make each point in space responsible for either promising information to another point, or accepting the outcome of a promise, as bidirectionality cannot be directly inferred.
So if every point in spacetime cannot be assumed to be connected both ways, then you have to explicitly define the communication channels that exist between points. This idea unifies both physical and digital "spaces", as everything is now modeled as a communications network from atoms up. Thus, Promise Theory makes the connection between compositionality and information and the rest of reality more clear than categories alone.
Mark acknowledges that Category Theory and Promise Theory are both similar and related. For instance, they both deal with notions of interiority. And Mark encodes his axioms with categories. He's written several books on the topic, like "In Search of Certainty" and "Smart Spacetime", and has published papers on arxiv. I recommend "Smart Spacetime" to see how powerful this kind of semantics can get.
[+] [-] jkhdigital|4 years ago|reply
I think the world is not going to reap the true benefits of computers for scientific progress until we systematize formal knowledge within a single shared syntactical universe. Open science means nothing if it has become so siloed and complex that results are largely unverified and frequently unverifiable.
[+] [-] joe_the_user|4 years ago|reply
[+] [-] chobytes|4 years ago|reply
I think the truth is that most math is pretty simple to describe and doesn't require a grand framework to formalize.
[+] [-] weatherlight|4 years ago|reply
Example:, for any statement A unprovable in a particular formal system F , there are, trivially, other formal systems in which A is provable (take A as an axiom). On the other hand, there is the extremely powerful standard axiom system of Zermelo-Fraenkel set theory (denoted as ZF, or, with the axiom of choice, ZFC), which is more than sufficient for the derivation of all ordinary mathematics. Now there are, by Gödel’s first theorem, arithmetical truths that are not provable even in ZFC. Proving them would thus require a formal system that incorporates methods going beyond ZFC. There is thus a sense in which such truths are not provable using today’s “ordinary” mathematical methods and axioms, nor can they be proved in a way that mathematicians would today regard as unproblematic and conclusive.
[+] [-] keithalewis|4 years ago|reply
[+] [-] beaconstudios|4 years ago|reply
[+] [-] motohagiography|4 years ago|reply
At best, perception may be graphs all the way down. As though we were living in a simulation specified by a Matrix of adjacencies.
[+] [-] pgustafs|4 years ago|reply
Those are the basic axioms to say you're working with a nice operation that turns paths into edges in a reasonable way. It gets interesting when you add more identifications (commutative diagrams) and operations (functors). Prototypical example: vertices are sets, edges are functions, you get identification of paths (sequential compositions of functions) whenever the underlying composite functions are pointwise equal.
[+] [-] RacfeelBudkind|4 years ago|reply
Edit: these extra properties allow you to reason about a wide class of problems when they're represented as categories, not just round trip them from unencoded to encoded to unencoded. For example, Pijul uses a category of patches to model file patching and prove certain properties of the version control system.
[+] [-] Koshkin|4 years ago|reply
[+] [-] wellpast|4 years ago|reply
But taste, smell, and sound ... you can't so readily and purely taxonomize these...
[+] [-] wisnesky|4 years ago|reply
[+] [-] bob1029|4 years ago|reply
Is 3NF/BCNF something that can be described in terms of Category Theory?
I always felt like there was some super deep & fundamental link between these mathematical concepts and relational modeling ideas. Reading "Out of the Tar Pit" was a big trigger for me on connecting dots between imperative/functional/relational programming as well as implications that a good combination of these things would have positive impact on domain modeling.
[+] [-] wisnesky|4 years ago|reply
[+] [-] ukj|4 years ago|reply
Which is roughly what the Univalence axiom tells us: identity is equivalent to equivalence.
The identity type is the normal/canonical/unique form for all object of a particular type.
Yet another perspective is the question "Do A and B have the same structure? Are they isomorphic?". When you are dealing with finite data types the answer to such questions is inevitably in the domain of Finite Model Theory ( https://en.wikipedia.org/wiki/Finite_model_theory ). Finite categories are the same sort objects as DB schemas.
[+] [-] asavinov|4 years ago|reply
The relational model is relies on set theory (more specifically relational algebra). An alternative view on data and data modeling is based on 1) sets, and 2) functions, and is called the concept-oriented model [1, 2]. It is actually quite similar to category theory and maybe even could be described in terms of category theory. It is also quite useful for data processing and there is one possible implementation which is an alternative to map-reduce and join-groupby approaches [3].
[1] A. Savinov, On the importance of functions in data modeling https://www.researchgate.net/publication/348079767_On_the_im...
[2] A. Savinov, Concept-oriented model: Modeling and processing data using functions https://www.researchgate.net/publication/337336089_Concept-o...
[3] https://github.com/asavinov/prosto Prosto is a data processing toolkit radically changing how data is processed by heavily relying on functions and operations with functions - an alternative to map-reduce and join-groupby
[+] [-] wisnesky|4 years ago|reply
[+] [-] juancn|4 years ago|reply
Modelling is about communication and understanding, if the language is expressive, precise and utterly abstruse for most people, it's a niche application at most (and it's likely very valuable in its niche).
There's a reason most informal methods become more popular.
[+] [-] j2kun|4 years ago|reply
But the real question is whether it is a _useful_ modeling language for everything. Engineers know everything has a tradeoff, and category theorists would do well to recognize the limitations of their tools or risk turning people (like me) away after years of study.
[+] [-] wisnesky|4 years ago|reply
[+] [-] RacfeelBudkind|4 years ago|reply
Category theory is definitely not useful for modeling everything. However, it's useful for modeling a whole lot. Categories have few axoims, and those they do have align well with how humans break down complex problems, so a lot of systems can be modeled neatly with categories. And category models are useful for proving existence, uniqueness, and notions of "maximum" and "minimum" for their "arrows", which are often useful things people try to prove about systems.
[+] [-] moralestapia|4 years ago|reply
It's a really nice framework though, but there's plenty (pleeeeenty!) of things that lie beyond its scope.
Idealizing CT and its applications only does more harm than good to the field.
Edit: Sure, I'll be glad to talk about it. Have plenty of experience doing (also, avoiding doing) things w/ CT. Just drop me an email (see profile), you're always welcome.
[+] [-] meowkit|4 years ago|reply
[+] [-] nerdponx|4 years ago|reply
[+] [-] weatherlight|4 years ago|reply
[+] [-] random3|4 years ago|reply
[+] [-] unknown|4 years ago|reply
[deleted]
[+] [-] notslow|4 years ago|reply
https://conexus.com/
[+] [-] unknown|4 years ago|reply
[deleted]
[+] [-] 6gvONxR4sf7o|4 years ago|reply
[+] [-] zozbot234|4 years ago|reply
[+] [-] weatherlight|4 years ago|reply
https://mitpress.mit.edu/books/category-theory-sciences
[+] [-] gibsonf1|4 years ago|reply
[+] [-] Joker_vD|4 years ago|reply
[+] [-] haskellandchill|4 years ago|reply
[+] [-] RacfeelBudkind|4 years ago|reply
[+] [-] Koshkin|4 years ago|reply
[+] [-] da39a3ee|4 years ago|reply
[+] [-] tgbugs|4 years ago|reply
[+] [-] mbrodersen|4 years ago|reply
[+] [-] bordercases|4 years ago|reply
The candidate I would push forward as the proper reification would be Mark Burgess' Promise Theory. Mark's starting point isn't, "what's the most general algebra I can form for encoding mathematical objects", but "what happens if I generalize points in spacetime to be a special case of any kind of graph". When you do this, you make each point in space responsible for either promising information to another point, or accepting the outcome of a promise, as bidirectionality cannot be directly inferred.
So if every point in spacetime cannot be assumed to be connected both ways, then you have to explicitly define the communication channels that exist between points. This idea unifies both physical and digital "spaces", as everything is now modeled as a communications network from atoms up. Thus, Promise Theory makes the connection between compositionality and information and the rest of reality more clear than categories alone.
Mark acknowledges that Category Theory and Promise Theory are both similar and related. For instance, they both deal with notions of interiority. And Mark encodes his axioms with categories. He's written several books on the topic, like "In Search of Certainty" and "Smart Spacetime", and has published papers on arxiv. I recommend "Smart Spacetime" to see how powerful this kind of semantics can get.
https://arxiv.org/abs/1411.5563
[+] [-] grouphugs|4 years ago|reply
[deleted]