[HN Gopher] Category theory is a universal modeling language
___________________________________________________________________
Category theory is a universal modeling language
Author : bmc7505
Score : 126 points
Date : 2021-04-29 16:28 UTC (6 hours ago)
(HTM) web link (math.mit.edu)
(TXT) w3m dump (math.mit.edu)
| notslow wrote:
| I'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/
| 6gvONxR4sf7o wrote:
| I'll second that. Not a mathematician either, and I liked that
| book too.
| jkhdigital wrote:
| 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.
| beaconstudios wrote:
| Isn't that a similar idea to the Hilbert program, which failed
| due to godel's incompleteness theorem?
| Twisol wrote:
| Hilbert's program was about whether every statement could be
| proved _ab nihilo_ either true or false. The question
| remains: _given_ a proof, can we _verify_ it? Arguably, any
| proof conceived by a human mind should be verifiable in
| principle. So the Incompleteness Theorem doesn 't really
| apply, either formally or morally.
|
| A more interesting argument could be made on the basis of
| Rice's Theorem: for a Turing-complete language, the only non-
| trivial properties provable about a program are fundamentally
| syntactic. (Type systems can be seen as a way of elaborating
| your syntax to capture finer-grained details of your
| semantics). Here we have a richer and nearer-to-hand
| collection of programs whose properties are inaccessible --
| take, for instance, whether the 3n+1 algorithm halts on all
| inputs. Again, though, if we _have_ a proof of some property,
| we still ought to be able to verify it.
| tshaddox wrote:
| Isn't verifying a proof equivalent to determining whether a
| certain computer program halts?
| Twisol wrote:
| No, but it would be equivalent to verifying that a given
| computer program halts on a specified N steps.
|
| This is the same distinction between (among other things)
| P and NP problems. For any problem in P, given an
| instance of the problem I can produce a solution in
| polynomial time. For any problem in NP, given an instance
| of the problem _and a candidate solution_ , I can
| determine whether the solution is _valid_ in polynomial
| time.
|
| Determining whether a certain computer program halts
| would be equivalent to _producing_ a proof, not
| _verifying_ an existing one.
|
| Verifying a proof is, in principle, only a matter of
| making sure that each step of the proof is valid. Coming
| up with the right steps is a creative endeavor.
| Certainly, coming up with the right set of allowable
| steps is a creative endeavor, and proving that your
| system is expressive enough for interesting proofs is a
| creative endeavor. But once given a proof, verifying that
| it legally applies legal steeps is a purely mechanical
| endeavor.
| nicklecompte wrote:
| Parent is referring to something a bit different - Hilbert's
| program was about all of mathematics, even that which hadn't
| been discovered yet, whereas the parent is talking about
| formalizing existing mathematical knowledge in some HoTT-
| enabled programming language or proof-checker (hence the
| emphasis on verifying and the problem of siloed knowledge).
|
| Obviously true theorems with _existing_ proofs don't apply to
| Godelian incompleteness.
| joe_the_user wrote:
| 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.
| keithalewis wrote:
| 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.
| weatherlight wrote:
| 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 Godel'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 wrote:
| This 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?
| chobytes wrote:
| 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.
| chas wrote:
| In addition to CT's application to commutative algebra, it's
| pretty nice for reasoning about programs and logic.
|
| Programs: http://cseweb.ucsd.edu/~rtate/publications/proofgen
| /proofgen...,
| https://blog.sumtypeofway.com/posts/introduction-to-
| recursio..., the Functor/Applicative/Monad hierarchy in
| Haskell et al
|
| Logic: https://publish.uwo.ca/~jbell/catlogprime.pdf
|
| CT as a bridge between programs and logic:
| https://existentialtype.wordpress.com/2011/03/27/the-holy-
| tr...
| Twisol wrote:
| > I think the truth is that most math is pretty simple to
| describe and doesn't require a grand framework to formalize.
|
| I agree -- most fields of math are happy to establish their
| own axioms, and leave the reducibility of those axioms to
| some "foundations" as an exercise -- an important one, but
| not one that necessarily furthers the field itself.
|
| However, Voevodsky's stated aim for his Univalent Foundations
| project was _not_ to formalize everything under a grand
| theory of everything. He got the bejeebus scared out of him
| when one of his results was very, very subtly wrong, in a way
| that was difficult for mathematicians to verify for years,
| even given a reasonable inkling of a counterexample. So he
| sought to improve the state of the art in proof verification.
|
| You might argue, it's better to produce a verification tool
| for one field of mathematics than all of them at once. But
| you'll have a hard time finding any significantly complex
| theorem that doesn't draw insight from multiple places.
| (Arguably, that's why they're significantly complex in the
| first place). And all fields of mathematics have some basic
| elements in common. So, I'd argue, you're unlikely to do a
| good job for any but the most narrow domains of mathematics
| without seeking some level of generality.
|
| Any "foundation of mathematics" can be used for this purpose,
| and plenty of theorem provers have been built on each (Twelf,
| PVS, Agda). The draw of category theory is that it seems to
| capture at a fundamental level many of the basic conceptual
| elements we see across mathematics. (Homomorphisms are so
| universal it's not even funny.) It seems reasonable to pick
| something that starts us closer to where we want to be; the
| difficulties we encounter are more likely to be fundamental
| problems and not issues of encoding.
| chobytes wrote:
| Im not opposed to the use of proof assistant software for
| difficult theorems. And if one foundation or another is
| more applicable to that software, then thats fine.
|
| Its more the narrative of the grand unification of
| mathematics thats spun around 'foundational theories' that
| irks me. In reality its just various emulation schemes.
|
| Rephrasing other mathematicians work and claiming
| fundamental status, while not producing many novel
| theorems... just strikes me as very distasteful.
| weatherlight wrote:
| Theres a physical book as well. (It's nice!)
|
| https://mitpress.mit.edu/books/category-theory-sciences
| motohagiography wrote:
| 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.
| RacfeelBudkind wrote:
| 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.
| Koshkin wrote:
| 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).
| pgustafs wrote:
| 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.
| Twisol wrote:
| > The main thing categories add to graphs is identifications
| of paths.
|
| There's another, very different way to describe
| "identification of paths", although I agree that both are
| fundamental to categories.
|
| What you've described is better known in graph theory as the
| "transitive closure" of a graph. Indeed, every graph (and
| even every multigraph, with multiple edges between two nodes)
| gives a category via its transitive closure. But this
| category is the _free_ category on a graph, and there are
| many categories that are not "free", so there is still
| something missing.
|
| What categories add on top of the transitive closure is the
| ability to say that two paths between the same nodes are
| fundamentally _equivalent_. (In other words, you are
| identifying two paths -- see the confusion?) If those paths
| could be further composed with other paths, then the
| resulting composites are also equivalent (i.e. if a = b then
| ac = bc); proceeding in this way gets you a new category.
|
| It's the ability to say that two distinct "paths" (lists of
| edges) give you the same "edge" (single step) that really
| distinguishes category theory from graph theory. Commutative
| diagrams are popular in category theory precisely because
| they graphically display which paths produce equivalent
| edges.
| motohagiography wrote:
| > It's the ability to say that two distinct "paths" (lists
| of edges) give you the same "edge" (single step) that
| really distinguishes category theory from graph theory.
| Commutative diagrams are popular in category theory
| precisely because they graphically display which paths
| produce equivalent edges.
|
| It's the idea of graph isomorphism that confuses me about
| this, because I have trouble separating it from recognizing
| two equivalent paths as a type. The main reason is I don't
| have depth in the concepts at all, but the secondary one is
| that di-graphs with attributes seem to provide a covering
| abstraction for this. I should probably RTFM, (or more
| accurately, Do-TF-Graduate-Degree) but every time I read an
| explanation it creates a curiosity I can't leave alone.
| nicoburns wrote:
| I've never studied categories, but my reading of the
| parent comment was that a category was the combination of
| a graph and a seperate identification of paths within the
| graph in addition to the bare graph. Thus having
| isomorphic graphs would be necessary but not sufficient
| for two categories to be equivalent.
|
| I guess you could represent that as an extra complex
| graph, but I'm guessing that would be unwieldly, and may
| not actually be useful for analysos.
| Twisol wrote:
| I'm nervous that there might be a confusion between
| levels of abstraction here. Let me try to ground the
| terminology a bit, and see if that helps first.
|
| As a recognized term, "graph isomorphism" would lift to
| category theory as "category isomorphism". These are not
| entities _within_ a category (uh, _per se_ ), but they're
| relationships _about_ and _between_ categories. A graph
| /category isomorphism describes how two graphs/categories
| can be equivalently described in terms of each other.
|
| In graph theory, a _bidirectional path_ is a pair of
| paths _within_ a graph. Two nodes are part of the same
| _strongly-connected component_ if you can travel between
| them both ways. In the transitive closure of a graph, two
| nodes are in the same strongly-connected component if and
| only if the edges a- >b and b->a exist within the graph.
|
| In category theory, an _isomorphism of objects_ is a pair
| of arrows f, g _within_ a category between the same two
| objects -- such that their compositions fg and gf are
| both equivalent to the identity arrow. (In graphs, the
| paths fg and gf must be considered equivalent to the
| empty path.)
|
| In a graph, you might naturally think of isomorphic
| objects as those that "relate" the same way to all other
| objects -- that is, if you didn't already know which node
| you were looking at, you couldn't tell the two apart from
| a vantage point anywhere else in the graph. This
| intuition broadly carries into category theory, though
| you can have multiple edges betwen nodes -- that's why
| the `fg = gf = 1` rule needs to be added. The transitive
| closure guarantees that for any isomorphic objects A and
| B, any path entering (leaving) A (B) can be extended to
| enter (leave) B (A), and the identity condition
| guarantees that the extension we added to cross between
| the two objects didn't add or remove information.
|
| Put a slightly different way, if I have a path X -> Y
| that passes through either A or B, there is _no way_ to
| distinguish whether the path went through A or went
| through B.
| wellpast wrote:
| 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...
| moralestapia wrote:
| No, 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.
| meowkit wrote:
| You forgot the part where you explain <why>/point out/link to
| examples of things that lie beyond its scope.
| nerdponx wrote:
| 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.
| moralestapia wrote:
| I 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 wrote:
| Not 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]
| random3 wrote:
| It almost feels like your goal is to collect emails :). You
| made me curious. Please share your insights
| moralestapia wrote:
| >It almost feels like your goal is to collect emails
|
| Now that's a new one, keep going pal :)
| weatherlight wrote:
| Could you provide some examples where that this was the case?
| juancn wrote:
| 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.
| gibsonf1 wrote:
| 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.
| Joker_vD wrote:
| 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.
| haskellandchill wrote:
| 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).
| j2kun wrote:
| 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.
| RacfeelBudkind wrote:
| > 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.
| wisnesky wrote:
| 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.
| zozbot234 wrote:
| Newer work from the same author: Seven Sketches in
| Compositionality: An Invitation to Applied Category Theory
| https://arxiv.org/abs/1803.05316
| bordercases wrote:
| 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.
|
| https://arxiv.org/abs/1411.5563
| wisnesky wrote:
| 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...
| RacfeelBudkind wrote:
| For anyone interested in learning about category theory, this
| series is very good:
| https://www.youtube.com/playlist?list=PLbgaMIhjbmEnaH_LTkxLI...
| Koshkin wrote:
| To be honest, I liked _The Catsters_ better. Short and to the
| point.
| bob1029 wrote:
| 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.
| ukj wrote:
| 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.
| wisnesky wrote:
| 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...
| bob1029 wrote:
| Thank 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.
| wisnesky wrote:
| Welcome to the applied category theory community :-)
| gmfawcett wrote:
| > It would seem I should dive into category theory to see
| how far this rabbit hole goes.
|
| And that was the last we ever heard from bob1029.
| wisnesky wrote:
| Open source implementation and academic papers on using CT for
| databases: https://www.categoricaldata.net
___________________________________________________________________
(page generated 2021-04-29 23:01 UTC)