10 ms·
Category theory is a universal modeling language
- notslow 5y agoI'm not a mathematician, but I found Spivak's book on the linked page to be very accessible. They've started a company as well. https://conexus.com/ https://conexus.com/
- 6gvONxR4sf7o 5y agoI'll second that. Not a mathematician either, and I liked that book too.
- deleted 5y ago[deleted]
- weatherlight 5y agoTheres a physical book as well. (It's nice!) https://mitpress.mit.edu/books/category-theory-sciences https://mitpress.mit.edu/books/category-theory-sciences
- moralestapia 5y agoNo, it isn't. 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.
- weatherlight 5y agoCould you provide some examples where that this was the case?
- meowkit 5y agoYou forgot the part where you explain <why>/point out/link to examples of things that lie beyond its scope.
- deleted 5y ago[deleted]
- random3 5y agoIt almost feels like your goal is to collect emails :). You made me curious. Please share your insights
- moralestapia 5y ago>It almost feels like your goal is to collect emails Now that's a new one, keep going pal :)
- nerdponx 5y agoIsn'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.
- moralestapia 5y agoI can see ways to represent lambda calculus constructs using CT and viceversa. I guess that 'systems of logic' includes lambda calculus, or systems with equivalent semantics; so yeah, I can believe there's a connection at some level. The (one?) problem with CT is that it, by definition, puts too much importance on the relation between things via composition, which is a powerful paradigm in itself, but also quite restrictive. 'Structure' is not usually encoded like that in a natural way. CT is just part of a larger framework that is currently being unveiled (!!!); but, to be quite frank, people who focus mostly on CT seem to be missing the forest for the trees.
- Koshkin 5y agoNot to disagree, I just would make a slight correction: in this case it is more like people seem to be missing the trees for the forest.
- deleted 5y ago[deleted]
- benrbray 5y agoSee e.g. Baez & Stay 2009, "Physics, Topology, Logic, and Computation: A Rosetta Stone". [1] [1] https://arxiv.org/abs/0903.0340 https://arxiv.org/abs/0903.0340
- gibsonf1 5y agoThe 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.
- Joker_vD 5y agoRelational 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.
- haskellandchill 5y agoSure, 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 http://math.mit.edu/~dspivak/informatics/olog.pdf).
- wisnesky 5y agoOpen source implementation and academic papers on using CT for databases: https://www.categoricaldata.net https://www.categoricaldata.net
- jkhdigital 5y agoI 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.
- weatherlight 5y agoAll 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.
- guerrilla 5y agoThis is well known. Type theories also do not assume the law of excluded middle. What's your point and it's relevance to the comment?
- jkhdigital 5y agoThe issue is not one of “power”—one can make almost any formal system sufficiently “powerful” by adding a few axioms that get you over the rough spots in your proofs. The problem is that the modern world increasingly relies on mathematics, in nearly all aspects of life, to make consequential decisions about how to interpret data and act on it. The challenge is not one of power, but of fidelity—using a mathematical structure that is a suitable abstraction for the real world situation. Use the wrong abstraction, and you end up with paradoxes like the incompleteness theorems. I believe a goal of univalent foundations is to make the abstract structure that one is working with absolutely explicit, evidenced by the (almost) total absence of axioms from the system. If you want to work in ZFC, you can add those axioms yourself.
- j2kun 5y agoI 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.
- wisnesky 5y agoThe 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.
- RacfeelBudkind 5y ago> 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.
- j2kun 5y agoI haven't seen any particularly convincing examples of this outside of pure math.
- zozbot234 5y agoNewer work from the same author: Seven Sketches in Compositionality: An Invitation to Applied Category Theory https://arxiv.org/abs/1803.05316 https://arxiv.org/abs/1803.05316
- juancn 5y agoWhat'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.
- bordercases 5y agoThe 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. https://arxiv.org/abs/1411.5563 https://arxiv.org/abs/1411.5563
- wisnesky 5y agoThe 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_sketch_theory_as_a_framework_for_knowledge_management_090214.pdf https://www.nasa.gov/sites/default/files/ivv_wojtowicz_sketc...
- bob1029 5y agoAs 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.
- wisnesky 5y agoThe 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/FunctorialDataMigration.pdf http://math.mit.edu/~dspivak/informatics/FunctorialDataMigra...
- bob1029 5y agoThank you for this. I was having a hard time finding Batman and Mr. Wayne in the same document at the same time. Definition 1.1.1 is blowing my mind right now. It would seem I should dive into category theory to see how far this rabbit hole goes. From a practical modeling perspective, there certainly feels like a "done/correct" point where any further normalization seems wrong, even if you ignore all the specific rules.
- motohagiography 5y agoNaive 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.
- wellpast 5y agoVisual 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...
- RacfeelBudkind 5y agoCategories 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.
- pgustafs 5y agoThe 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.
- RacfeelBudkind 5y agoFor anyone interested in learning about category theory, this series is very good: https://www.youtube.com/playlist?list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_ https://www.youtube.com/playlist?list=PLbgaMIhjbmEnaH_LTkxLI...
- grouphugs 5y agonope
- tgbugs 5y agoI 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.
- mbrodersen 5y agoI 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.