You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Todd Trimble (Aug 29 2023 at 19:34):Steve Huntsman said:
John Baez said:
I think any branch of math you're just learning seems to have an annoyingly large amount of jargon. Later, once you've mastered a lot of the jargon and are digging deeper, you discover it has an annoyingly large number of theorems. :upside_down:
I have never felt this in disciplines wherein one actually computes things. Take enumerative combinatorics as an extreme opposite case: there are certainly a lot of concepts and terms, but at a basic level there are not many definitions to wade through for any particular sort of problem. If I want to enumerate all the Dyck paths of a certain size then there are quite a few ways to do it, and perhaps some machinery to learn (say a generating function), but not a lot of concepts without associated machinery, results, or examples.
You don't think CT-ists actually compute things?
I don't know about others, but I feel that I compute things all the time as I work in category theory. One example that came up not so long ago was to compute the set of natural transformations from one functor Vect --> Set to another, where the first takes a vector space to its n-fold tensor power and the other was some other functor. "Compute" here means to characterize these things in simple concrete terms. For example, if the second functor is the same as the first here, then natural transformations are tantamount to (are in natural bijection with) elements of the group algebra of kS_n, where k is the ground field.
If one's idea of computing or calculating is relegated to computing numbers, then I don't know what to say. That would be a limited meaning. I would naturally use the word "compute" to describe what I was doing, and wouldn't know what else to call it. I think a lot of category theorists engage in this sort of humble but honest activity, routinely.
Patrick Nicodemus (Aug 29 2023 at 20:00):I feel that there is a notion of computing a colimit which amounts to giving an explicit and compact/tangible description of the equivalence classes in the quotient.
Often I find this goes as follows: Given F : D -> Sets a functor, find a reasonably small/workable subcategory A : C -> D and a functor T : C -> Sets such that F is the left Kan extension of T along A and thus has the same colimit.
Patrick Nicodemus (Aug 29 2023 at 20:01):Certainly most of the things I do when manipulating simplicial set could be called computing. it is highly combinatorial.
Steve Huntsman (Aug 29 2023 at 20:09):Todd Trimble said:
You don't think CT-ists actually compute things?
... "Compute" here means to characterize these things in simple concrete terms. ...
If one's idea of computing or calculating is relegated to computing numbers, then I don't know what to say. That would be a limited meaning.
I do in fact mean that. I think "characterize" is a fine word for the CT-oriented activities you described.
Steve Huntsman (Aug 29 2023 at 20:12):One minor caveat here: I would also think of "computing" data structures that are conveniently encoded with numbers. A homology group (which I can exhibit by a matrix indexed by generators that are themselves conveniently encoded with numbers) would fit this bill for any fans of categorifying things.
Mike Shulman (Aug 29 2023 at 20:13):What about a homology group that is infinitely generated?
Steve Huntsman (Aug 29 2023 at 20:14):Well I guess I would have to do some LISPy things then.
Mike Shulman (Aug 29 2023 at 20:15):?
Steve Huntsman (Aug 29 2023 at 20:17):Like a stream (a source or sink for characters) or some other data structure that doesn't "terminate."
Todd Trimble (Aug 29 2023 at 20:17):Hm. So if the question were changed to: find the number of natural transformations, that would count?
Since you brought up enumerative combinatorics, I'll say that a lot of time-tested ways to calculate numbers of structures -- bijective proofs -- typically involve proving two functors are isomorphic (Joyal species). I would call computing the number of structures of one type by bijecting them with another easy-to-count type of structure just that, a computation. Examples from q-mathematics pop to mind.
Mike Shulman (Aug 29 2023 at 20:17):How about a homology group that is uncountably generated?
Steve Huntsman (Aug 29 2023 at 20:18):Todd Trimble said:
Hm. So if the question were changed to: find the number of natural transformations, that would count?
Yes. But people doing that would probably tend to describe their work as combinatorics and not CT.
Mike Shulman (Aug 29 2023 at 20:19):I would find it curious to describe one activity as "computing" and another activity that gives strictly more information than the first (describing a set rather than just its cardinality) as not "computing".
Todd Trimble (Aug 29 2023 at 20:19):You said areas in which one (as in, person) computes things. I used categorical reasoning to count the number of natural transformations.
Steve Huntsman (Aug 29 2023 at 20:20):@Mike Shulman I'm not trying to advocate some detailed philosophical view of computation here, I know you'll run rings around me lol. But there is a notion of computation that boils down to some process that takes numbers in and spits numbers out. It doesnt have to be a finitary process.
Mike Shulman (Aug 29 2023 at 20:20):There is?
Todd Trimble (Aug 29 2023 at 20:22):There's also a point of view from type theory (proof relevance) where proofs are viewed as computations of a sort, i.e., as a process that takes data in and spits data out.
Mike Shulman (Aug 29 2023 at 20:22):Ordinary Turing-computation is finitary. It has variants relative to oracles or other PCAs, but I don't think "computing a homology group" (e.g. by a spectral sequence argument) can be reduced to any sort of formal computability of that kind.
Steve Huntsman (Aug 29 2023 at 20:23):Todd Trimble said:
You said areas in which one (as in, person) computes things. I used categorical reasoning to count the number of natural transformations.
Yes and I think that is not a common activity for folks when studying CT as a discipline. I use CT only as a tool not as an object of study in its own right. Folks can do both but many seem not to very much.
Mike Shulman (Aug 29 2023 at 20:24):Don't take this the wrong way, but if you personally use CT only as a tool, maybe you aren't the best-equipped to judge what the common activities are for folks who study it as a discipline?
Mike Shulman (Aug 29 2023 at 20:25):(As a sort of converse to Tim's point above about perceptions...)
Todd Trimble (Aug 29 2023 at 20:27):Steve Huntsman said:
Todd Trimble said:
You said areas in which one (as in, person) computes things. I used categorical reasoning to count the number of natural transformations.
Yes and I think that is not a common activity for folks when studying CT as a discipline. I use CT only as a tool not as an object of study in its own right. Folks can do both but many seem not to very much.
Eh, don't be too sure of that. I think maybe you don't fully realize what many category theorists do in their work (and yes, I study CT as a discipline). I think a lot of us practitioners calculate -- and I wouldn't think it natural to phrase it as "a lot of us practitioners characterize".
People like Lawvere and Schanuel calculated all the time, on small humble finite structures.
Steve Huntsman (Aug 29 2023 at 20:28):Mike Shulman said:
Don't take this the wrong way, but if you personally use CT only as a tool, maybe you aren't the best-equipped to judge what the common activities are for folks who study it as a discipline?
I certainly am not. But I am pretty sure they "compute" less on average than in "meat and potatoes math" because the formal manipulations are further removed from numbers where I can put an actual "=" at the end of a computation.
Steve Huntsman (Aug 29 2023 at 20:30):Todd Trimble said:
Steve Huntsman said:
Todd Trimble said:
You said areas in which one (as in, person) computes things. I used categorical reasoning to count the number of natural transformations.
Yes and I think that is not a common activity for folks when studying CT as a discipline. I use CT only as a tool not as an object of study in its own right. Folks can do both but many seem not to very much.
Eh, don't be too sure of that. I think maybe you don't fully realize what many category theorists do in their work (and yes, I study CT as a discipline). I think a lot of us practitioners calculate -- and I wouldn't think it natural to phrase it as "a lot of us practitioners characterize".
People like Lawvere and Schanuel calculated all the time, on small humble finite structures.
It is entirely possible that I am mistaken here. But the observations I have been able to make over the years support the conclusion I've reached. Happy to be disabused of it but anecdotes of "someone computed something once" or "here's a equals sign I can point to in a paper" have a lot of inertia to counter in my case.
Mike Shulman (Aug 29 2023 at 20:30):I put an actual "=" at the end of a computation all the time too. It just happens to be an equality in the type of sets, i.e. an isomorphism. (-:O
Steve Huntsman (Aug 29 2023 at 20:31):At the end of the day I think of computing as being about numbers. Call me crazy.
Steve Huntsman (Aug 29 2023 at 20:33):Mike Shulman said:
There is?
Sure. https://en.wikipedia.org/wiki/Hypercomputation#Uncomputable_inputs_or_black-box_components
I think of mathematicians as being nominally more powerful than Turing machines too.
Mike Shulman (Aug 29 2023 at 20:33):I won't call you crazy, I'll just say you haven't yet understood how general computation can be.
Mike Shulman (Aug 29 2023 at 20:35):Yes, I think that falls under the same general heading as oracle computation, which I mentioned. As I said, I doubt there is a kind of computation of that sort that describes what we do when "computing" a homology group. And if you are supposing an informal notion of "computation" that just means "anything a mathematician can do," then there's no reason that would be restricted to numbers at all.
Steve Huntsman (Aug 29 2023 at 20:35):I would call
Mike Shulman said:
I won't call you crazy, I'll just say you haven't yet understood how general computation can be.
Could be. I think it's mere nomenclature. I would call a lot of things "characterizations" (say) that it seems y'all might call "computations"
James Deikun (Aug 29 2023 at 20:36):For a data point, as someone making a living as a computer scientist in industry, I don't think of computing, in either the automated or manual sense, as being about numbers.
Mike Shulman (Aug 29 2023 at 20:36):Probably this thread has about reached the limit of its usefulness and we should knock it off, but I'll just mention that in dependent type theory one certainly has "computations", in any meaningful sense of the word, which evaluate (in a real programming language implemented on a computer) to sets rather than numbers.
Steve Huntsman (Aug 29 2023 at 20:49):OK so I figured I'd exhibit some examples (nuts I know) of things that folks "compute compute" in various areas as delineated by the arXiv. It's hacky but please fill in blanks/educate me.
AG- cohomology groups
AT- ibid.
AP- solutions to PDEs
CT- ???
CA- solutions to ODEs
CO- number of structures
AC- bases; generators
CV- residues
DG- curvatures
DS- entropies; recurrences
FA- integral transforms
GM- whatever
GN- topologies on finite sets
GT- Godbillon-Vey invariants
GR- character tables
HO- ...
IT- entropies
KT- K-groups
LO- ???
MP- instanton numbers
MG- Hadwiger's constant
NT- lots of numbers
NA- ibid.
OA- spectral things
OC- optima
PR- probabilities
QA- invariants
RT- character tables
SP- spectra
ST- statistics
SG- symplectic capacities, Floer stuff
Mike Shulman (Aug 29 2023 at 20:51):Is the fact that you don't want to talk about "computing a set" related to the fact that such computations usually only determine the set up to unique isomorphism?
Steve Huntsman (Aug 29 2023 at 20:52):You mean a number?
Steve Huntsman (Aug 29 2023 at 20:52):Honestly not trying to be obtuse here
Mike Shulman (Aug 29 2023 at 20:53):Do I mean what is a number?
James Deikun (Aug 29 2023 at 20:54):A number is a set determined up to isomorphism, but not up to unique isomorphism.
Mike Shulman (Aug 29 2023 at 20:54):I mean the sort of computation that Todd described:
natural transformations are tantamount to (are in natural bijection with) elements of the group algebra of kS_n, where k is the ground field
You don't want to call this a computation. I was asking whether your reluctance is related to the parenthetical "are in natural bijection with", as opposed to how computing a number traditionally says "is equal to".
James Deikun (Aug 29 2023 at 20:56):In particular, the information that you throw away when you reduce a computation of a set to a computation of a number, is which isomorphism is the "canonical" or "natural" one.
Steve Huntsman (Aug 29 2023 at 20:57):Oh I see. I blew past this part of the discussion but quoting myself: "I would also think of "computing" data structures that are conveniently encoded with numbers."
Todd Trimble (Aug 29 2023 at 20:58):Mike Shulman said:
Probably this thread has about reached the limit of its usefulness and we should knock it off, but I'll just mention that in dependent type theory one certainly has "computations", in any meaningful sense of the word, which evaluate (in a real programming language implemented on a computer) to sets rather than numbers.
Probably wise, we should knock it off soon.
Now I'm not saying I think Steve thinks this, but -- since we're sharing personal impressions -- I've long gotten the sense that people think of "soft" (conceptual) mathematics or mathematicians as something less than red-blooded or doing "real stuff". Some people I've observed crow how they do "hard analysis", and the way they say it, it sounds like a thing that manly men should be doing. The hard stuff.
So the idea that CT-ists are some sort or arty, airy bunch who love to engage in sophisticated jargon-laden discussions, who are not down-to-earth types, like those hard analysts -- well, surely some of that may be true, but I think it's largely a caricature and isn't in tune with the multi-faceted reality of what committed category theorists really do. I think I can end on that thought.
Mike Shulman (Aug 29 2023 at 21:00):Steve Huntsman said:
Oh I see. I blew past this part of the discussion but quoting myself: "I would also think of "computing" data structures that are conveniently encoded with numbers."
I was enquiring about the reasons for this preference of yours.
Steve Huntsman (Aug 29 2023 at 21:02):Todd Trimble said:
Now I'm not saying I think Steve thinks this, but -- since we're sharing personal impressions -- I've long gotten the sense that people think of "soft" (conceptual) mathematics or mathematicians as something less than red-blooded or doing "real stuff".
I don't think that but I have gotten that sense too, and have even been on the receiving end of that sense.
On certain rare and specific occasions I have felt that it was even true in that instance, like the joke that some AG/CT type person said an equation was like GRR because there was an equals sign in it.
Steve Huntsman (Aug 29 2023 at 21:05):Mike Shulman said:
I was enquiring about the reasons for this preference of yours.
Well my actual jobs since 2010 have mostly consisted of designing algorithms and computing data that I have to represent as numbers in some way on an actual computer using inputs also represented as numbers in some way on an actual computer. There can be lots of syntactic sugar.
Ryan Wisnesky (Aug 29 2023 at 22:25):fwiw, I think there is a blind spot in applied category theory re: computation, that needs to be further developed, and I commend the HoTT community for doing work in this area. in particular, I claim that in many ways, applied category theory "should be" the same thing as computer algebra; but whereas in e.g. the group theory community there is a lot discussion about algorithms and how to solve word problems and what to do with software packages like Mathematica, in applied category theory, most work is still done on paper, and I'm not sure why there's such a divergence from group theory in that regard.
Steve Huntsman (Aug 29 2023 at 23:30):Steve Huntsman said:
OK so I figured I'd exhibit some examples (nuts I know) of things that folks "compute compute" in various areas as delineated by the arXiv. It's hacky but please fill in blanks/educate me.
…
LO- ???
Embarrassed to have not thought of satisfying assignments to SMT problems here.
Maybe for CT the answer of what gets computed is a diagram?
Steve Huntsman (Aug 29 2023 at 23:31):Or “an” answer I guess
Notification Bot (Aug 30 2023 at 13:06):48 messages were moved here from #practice: communication > CT representation online by Matteo Capucci (he/him).
Steve Huntsman (Aug 30 2023 at 13:31):OK so I'm leaning towards the notion, anticipated and expressed by @Ryan Wisnesky in a paper (and business!) if not here, that a (if not "the principal" or even just "the") computational objective of CT is Kan extensions per https://www.epatters.org/wiki/algebra/computational-category-theory.html.
Steve Huntsman (Aug 30 2023 at 13:34):Are there other computational objectives that are "internal" to category theory?
Todd Trimble (Aug 30 2023 at 13:39):Steve Huntsman said:
OK so I'm leaning towards the notion, anticipated and expressed by Ryan Wisnesky in a paper (and business!) if not here, that a (if not "the principal" or even just "the") computational objective of CT is Kan extensions per https://www.epatters.org/wiki/algebra/computational-category-theory.html.
Ah, yes. I think Fong and Spivak allude to this sort of thing in papers and in their Seven Sketches (see the chapter on databases and database migration), don't they?
Steve Huntsman (Aug 30 2023 at 13:48):It is embarrassing (but maybe not just to me?) that identifying a computational objective of CT didn't seem obvious to me despite the fact that I was aware of this particular work.
Steve Huntsman (Aug 30 2023 at 13:50):To clarify, I mean maybe not just to me but perhaps also to the field.
Steve Huntsman (Aug 30 2023 at 13:51):The idea that 'computing' is in quotes in the thread title is another indication of this--computing is seen as something uncommon enough to be described in such a way. By comparison computations of logical objectives were familiar to Aristotle.
Steve Huntsman (Aug 30 2023 at 14:47):Todd Trimble said:
Hm. So if the question were changed to: find the number of natural transformations, that would count?
Looking back on this, I see that you were under the impression that I a) thought CT-ists didn't actually compute and that b) your set of natural transformations gizmo didn't count as a computation. I want to clarify these, because neither was or is the case. a) I think CT-ists don't compute many things in CT versus using CT, with Kan extensions being now an (or the) obvious counterexample. b) could be called a computation versus a characterization (not sure I would feel comfortable eliding such a distinction but OK), and it can clearly be encoded numerically: take a basis as a matrix, form its tensor powers, and encode the algebraic operations. But insofar as there is computation here, there isn't much of a CT-ish computational objective--it is a group-theoretical one, and the computations are only "in" CT insofar as the problem has been translated there: this strikes me as more fairly called "using" CT than "in" CT. Now it is a CT-ish objective to characterize this gizmo "in" CT, and you've done that by construction. Fair enough?
Steve Huntsman (Aug 30 2023 at 14:48):Todd Trimble said:
Since you brought up enumerative combinatorics, I'll say that a lot of time-tested ways to calculate numbers of structures -- bijective proofs -- typically involve proving two functors are isomorphic (Joyal species). I would call computing the number of structures of one type by bijecting them with another easy-to-count type of structure just that, a computation. Examples from q-mathematics pop to mind.
This is what I'd call "using" CT not "in" CT. The computational objective is more combinatorial than categorical.
Josselin Poiret (Aug 30 2023 at 14:49):huh, I thought for sure Yoneda was pure computation, guess it's not then
Steve Huntsman (Aug 30 2023 at 14:50):Mike Shulman said:
I would find it curious to describe one activity as "computing" and another activity that gives strictly more information than the first (describing a set rather than just its cardinality) as not "computing".
I would say the computation is all concentrated in the numerics and the rest is characterization. I see now that not talking to Todd's earlier point at the time seemed to convey a rather different impression.
Steve Huntsman (Aug 30 2023 at 14:56):Mike Shulman said:
I doubt there is a kind of computation of that sort that describes what we do when "computing" a homology group.
I don't understand this. I might characterize a space as equivalent to one that has a representation admitting computation, e.g., a triangulation. Then I would compute on the triangulation and do linear algebra. Or I might have a theorem that allows me to compute some equivalence between different spaces, one of which I've already computed a result for. Do you mean something else?
Steve Huntsman (Aug 30 2023 at 15:00):Josselin Poiret said:
huh, I thought for sure Yoneda was pure computation, guess it's not then
Good point, it can be
Steve Huntsman (Aug 30 2023 at 15:02):But (again please correct me) Yoneda seems more commonly used to characterize things than to compute as part of an algorithm. Now I know we aren't gonna be able to define that because as Yanofsky showed any meaningful notion of algorithm has an undecidable equality predicate, but like Potter Stewart I know an algorithm when I see one.
Ryan Wisnesky (Aug 30 2023 at 15:04):For anyone interested, our latest thinking about how to implement kan extensions rapidly using existing "chase" algorithms already developed in computer science is here: https://arxiv.org/abs/2205.02425 . There are enough applications of this to automated reasoning that we were able to publish in the journal of automated reasoning itself, not in a category theory journal. I think that is another under appreciated point - I'm not convinced applied category theory results are of interest to domain experts, unless they are published in domain-specific journals, rather than math ones.
Todd Trimble (Aug 30 2023 at 15:25):Steve Huntsman said:
Mike Shulman said:
I would find it curious to describe one activity as "computing" and another activity that gives strictly more information than the first (describing a set rather than just its cardinality) as not "computing".
I would say the computation is all concentrated in the numerics and the rest is characterization. I see now that not talking to Todd's earlier point at the time seemed to convey a rather different impression.
It's no problem, and I'd be glad to be move on from the nomenclatural debate, now that I see better what you're after. (And I appreciate your efforts to clarify; I'm going to read what you wrote a few more times to be absolutely sure.) If I may say, "I have never felt this in disciplines wherein one actually computes things" sounded more aggressive at the time than it does with the benefit of hindsight.
Anyhow, as you surely perceive, I'm more of a pure guy. I've notified someone I know about this thread, who may be able to give more examples of computation in CT.
Steve Huntsman (Aug 30 2023 at 16:12):Todd Trimble said:
If I may say, "I have never felt this in disciplines wherein one actually computes things" sounded more aggressive at the time than it does with the benefit of hindsight.
Not sure it wasn't aggressive--I am an aggressive interlocutor in person and online--but it wasn't intended to be very aggressive.
Indeed except for the Kan stuff, which I didn't think of previously, I'm still not sure I've spotted another class of computations, and I suspect the generality of Kan things might even subsume vast swathes of algorithms/computations that aren't generally thought of in that idiom.
Regarding Yoneda, I've used Cayley's theorem (hence Yoneda) in service of explicit computations such as this but don't think of that as _part_ of the computation.
Mike Shulman (Aug 30 2023 at 16:21):I'm about done with this conversation, but just to clarify this:
Steve Huntsman said:
Mike Shulman said:
I doubt there is a kind of computation of that sort that describes what we do when "computing" a homology group.
I don't understand this. I might characterize a space as equivalent to one that has a representation admitting computation, e.g., a triangulation. Then I would compute on the triangulation and do linear algebra. Or I might have a theorem that allows me to compute some equivalence between different spaces, one of which I've already computed a result for. Do you mean something else?
The point I was making was about terminology. Everyone in the world (at least, everyone who does it) talks about "computing" a homology group when they do, for instance, spectral sequence calculations, which are not (at least, not a priori) reducible to first characterizing something in "numerical" terms and then running an algorithm. So I was saying that this use of "computing" (which, again, is utterly standard in the field of algebraic topology, not category theory) doesn't fit in your (in my view, overly narrow) meaning of "computation".
Steve Huntsman (Aug 30 2023 at 16:42):Mike Shulman said:
I'm about done with this conversation, but just to clarify this:
Steve Huntsman said:Mike Shulman said:
I doubt there is a kind of computation of that sort that describes what we do when "computing" a homology group.
I don't understand this. I might characterize a space as equivalent to one that has a representation admitting computation, e.g., a triangulation. Then I would compute on the triangulation and do linear algebra. Or I might have a theorem that allows me to compute some equivalence between different spaces, one of which I've already computed a result for. Do you mean something else?
The point I was making was about terminology. Everyone in the world (at least, everyone who does it) talks about "computing" a homology group when they do, for instance, spectral sequence calculations, which are not (at least, not a priori) reducible to first characterizing something in "numerical" terms and then running an algorithm. So I was saying that this use of "computing" (which, again, is utterly standard in the field of algebraic topology, not category theory) doesn't fit in your (in my view, overly narrow) meaning of "computation".
Fair enough. Whenever I computed something I've been able to look back and seen how in principle it could have been done on a computer, and usually in practice I actually try to prove things by writing code in a poor man's Curry-Howard mindset and writing things up in natural language afterwards.
Often I thought (and think) of my work as a composition of preparatory work ("characterization") with a "mechanical process" a la Turing ("computation"). I need to do the former but in principle only to understand the latter because it can be outsourced to silicon (even though paper is often faster and more useful in practice). My impression has been (and apart from the Kan extension algorithm stuff still is) that CT is more focused on characterization than any other field of mathematics and that this is its nature and intent. A lot of the time (maybe every time?) mathematicians say "is just" they are channeling this, but they are not computing.
BTW can you comment on https://arxiv.org/abs/1610.05338? I get that it doesn't compute everything.
Mike Shulman (Aug 30 2023 at 16:44):I didn't mean there aren't algorithms, just that what mathematicians do isn't a priori just running an algorithm.
Steve Huntsman (Aug 30 2023 at 16:48):Right and I think that CT folks generally do less algorithmic stuff (when wearing the CT hat) than other folks. Maybe this is broadly unfair/inaccurate (certainly doesn't fit Ryan W!) but it's not an indictment to begin with.
Mike Shulman (Aug 30 2023 at 16:51):I'm not convinced of that, but I agree it's not an indictment. If it has any moral value, I would say it would be a good thing, as it would mean we're less likely to be replaced by computers. (-: I'm glad we reached the actual point eventually, even if we have to agree to disagree about terminology.
Ryan Wisnesky (Aug 30 2023 at 17:45):you know what they say - it won't be AI that replaces people, but people using AI that replace people ;-)
David Michael Roberts (Sep 02 2023 at 06:32):Here's an example of what people in CT compute, from an example I saw yesterday, I think: given that some object exists by some universal property (it was an exponential in some (2-)category, in what I saw), what actually is that object? In the sense of being able to say concretely what the elements are (if this were a concrete category) or what the objects are (if this was an exponential in some 2-category of structured categories, asy), and in a way whose definition is independent of the characterisation by that universal property. Even better if you can give a concrete isomorphism to a priori known and understood object/categories whose objects are a priori known.
Perhaps this falls under the banner of "computing Kan extensions", but this way of looking at it unpacks the actual output of the computation (what even does it mean to "compute a Kan extension" anyway?).
The computation process often involves chaining together known CT theorems, other "calculated" universal objects (i.e. they have a concrete description, but have been shown to satisfy a universal property) and taking advantage of their abstract CT properties and/or some concrete fact to arrive at some concrete description of what the universal object of interest is.
I'm put in mind of the whole Schur functor story that @John Baez and @Todd Trimble and collaborator(s) have worked out. There's some abstract 2-rig stuff, but it comes down to computing the "solution" to be a specific known thing.
John Baez (Sep 02 2023 at 10:01):There's also another sense of of computing, which matters a lot to me. To me it means working in a situation where I know a bunch of rules for manipulating symbols and I'm applying these rules to:
There is often a lot of exploration and blundering around, not only because I make actual errors but also because I don't know which rule to apply when - and there may also be missing rules that I discover I need, and have to prove. I have a personal feeling for when I'm "computing" something in this sense, and it's different than "proving" someting, though it may be used to prove something.
I did a bunch of computing - in this sense - to prove Lemma 15 on Kaehler differentials here. By the final writeup there was not much computing left, and I pushed it into Lemma 16. But this is the distilled result of a lot of blundering about, which was at times rather frustrating since Lemma 15 has a superficially much more elegant proof on Wikipedia. However, on Wikipedia all the "computation" is packed into the last sentence:
Taking the quotient by precisely imposes the Leibniz rule.
John Baez (Sep 02 2023 at 10:04):Ultimately I feel Wikipedia didn't really prove that has the universal property of Kaehler differentials, while my superficially more grungy proof does, and also reveals more.
John Baez (Sep 02 2023 at 10:10):I don't feel I did a lot of "computing" in this sense in my part of proving the theorems in the paper on Schur functors. Maybe @Todd Trimble did. There is, however, a lot of computing to be done in this subject - the Littlewood-Richardson rules for tensoring Schur functors, and plethysm for composing Schur functors (where no practical algorithm is known even today!).
Ryan Wisnesky (Sep 02 2023 at 14:13):Maybe whether or not something is computation has to do with whether it is done on paper vs on a computer, rather than about what is being computed. Like, sure, I can compute Kan extensions by hand, but not on terabytes of data - I need a computer for that. Or sure, I can write a proof by hand, but sometimes need an automated theorem prover to solve the word problem for some category presentation for me, because I need to prove millions of expressions equal or not. Although they are the same activity, the way they are engineered into existence is a lot different
John Baez (Sep 02 2023 at 16:27):By hand versus computer is a really important distinction, but people were computing by hand long before investigations in mathematical logic revealed the possibility of automated mechanical computation, so personally I'm not going to stop using "computation" in a way that includes computation by hand. Especially since that's the main kind I do. :upside_down:
Mike Shulman (Sep 02 2023 at 16:27):And, of course, before electronic computers, the people who computed were called "computers".
Jean-Baptiste Vienney (Sep 02 2023 at 19:26):It always annoys me when people try to defend human mathematicians vs. computers which would remplace them. Because making mathematics understanble by computers is equal to making mathematics better, both for humans and computers. I know an example where such a thing happened. There is a field in algebraic topology which is named Functor calculus, or Goodwillie calculus. It is named calculus because it looks like calculus but it is clearly not the same thing. Investigation in computer science led to linear logic, twenty years later, differential linear logic was invented, then differential categories, then cartesian differential categories and then in 2018, in this paper Directional derivatives and higher order chain rules for abelian functor calculus they found that functor calculus gives an example of cartesian differential category.
So, here progress in pure mathematics came from research in logic and an aera of logic which is tightely linked with the theory of programming languages. So, please, yes people were doing computations before computers exist, but what computers are doing is closer to what computation is really: a completely mechanical process. So it is the computers which are really doing computations. And helping them to do these computations, is a good thing for everybody. Being against the mechanization of mathematics is being against progress in mathematics.
Jean-Baptiste Vienney (Sep 02 2023 at 19:29):Everything is good in replacing computations by human through random intuitive thinking by a clear theory that allows things to be computed by computers.
Jean-Baptiste Vienney (Sep 02 2023 at 19:30):Humans can also use this clear theory after it has been found.
Jean-Baptiste Vienney (Sep 02 2023 at 19:32):The example of categorical database theory is good also. It is a progress which makes the theory much more beautiful for humans while being something easily implementable on computers because of this same clarity/beauty which comes from the use of category theory.
Jean-Baptiste Vienney (Sep 02 2023 at 19:34):It is presented in this paper: Algebraic Databases.
Jean-Baptiste Vienney (Sep 02 2023 at 19:35):You can see that both of the two papers I linked have in their authors people which are widely known in the community of category theory (two of thems are on Wikipedia). And they are not affraid by computers.
Jean-Baptiste Vienney (Sep 02 2023 at 19:38):I'm deeply convinced that very very good things happen when you try to help computers understand mathematics.
John Baez (Sep 02 2023 at 21:17):Jean-Baptiste Vienney said:
. So, please, yes people were doing computations before computers exist, but what computers are doing is closer to what computation is really: a completely mechanical process. So it is the computers which are really doing computations.
As I tried to explain, I don't use "computation" in that sense when I talk about the computations I'm doing. If you want me to use a different term when taking to you, like "calculation", that's fine. I don't like arguing about words.
But whatever you call it, I am not seeking to carry out a completely mechanical process. I could only do that after I figured out the things I'm trying to figure out. Instead, I'm manipulating symbols, following rules, but with a free choice of which rule I apply at each time - and sometimes adding new rules:
John Baez (Sep 02 2023 at 21:17):John Baez said:
There's also another sense of of computing, which matters a lot to me. To me it means working in a situation where I know a bunch of rules for manipulating symbols and I'm applying these rules to:
- prove two expressions are equal,
- reduce an expression to some sort of desired form, the details of which I don't know ahead of time,
- find patterns that may lead to theorems,
- etc.
There is often a lot of exploration and blundering around, not only because I make actual errors but also because I don't know which rule to apply when - and there may also be missing rules that I discover I need, and have to prove.
Jean-Baptiste Vienney (Sep 02 2023 at 21:40):I think that for you computing is thus the manipulation of formal rules, once you have specified what are the rules of the game ie. you have chosen the axioms and then you want to manipulate them to try proving something.
A stronger form a computation would be to have an algorithm which when you give him what you want to prove, give you a proof, ie. a way to apply the rules of the game to prove what you want to prove.
Jean-Baptiste Vienney (Sep 02 2023 at 21:41):But I think that finding such an algorithm would be very difficult and maybe impossible with most of the sets of axioms.
Mike Shulman (Sep 02 2023 at 21:43):Jean-Baptiste Vienney said:
the manipulation of formal rules, once you have specified what are the rules of the game ie. you have chosen the axioms and then you want to manipulate them to try proving something.
That sounds to me like a description of mathematics.
Jean-Baptiste Vienney (Sep 02 2023 at 21:47):I think in mathematics you can either:
This second activity is very difficult to formalize and it is difficult to link it to any kind of computation.
Jean-Baptiste Vienney (Sep 02 2023 at 21:49):Formalizing this second activity would be creating a very powerful AI that can do everything a human is capable of whereas the first one is more related to classical mathematical logic / computer science.
Jean-Baptiste Vienney (Sep 02 2023 at 21:57):ie. you can hope to find deterministic algorithms as opposed to the statiscal aspect of AI to help you somehow in the first activity.
Jean-Baptiste Vienney (Sep 02 2023 at 22:02):Honnestly, I'm very far from understanding what is computation. I find it very intriguing that category theory seems more related to computation than set theory -- I say that because of all the work in computer science which uses category theory, whereas at the same time it looks also more abstract, and thus makes you think that you're not going to produce an algorithm with some pratical application from it.
Jean-Baptiste Vienney (Sep 02 2023 at 22:06):I'm completely lost today on what is the meaning of words like "abstract", "concrete", "computation", "reasoning" and how to link each of this words to mathematics and computer science. I'm no longer able to define any of this in a good way.
Mike Shulman (Sep 02 2023 at 22:11):Sure, fair enough, there is more to mathematics than proving things. But I don't think any activity of "searching for a proof" can be described as "computation".
Jean-Baptiste Vienney (Sep 02 2023 at 22:26):I was just trying to give a more formal definition of what John B was talking about.
John Baez (Sep 02 2023 at 22:38):Jean-Baptiste Vienney said:
I'm completely lost today on what is the meaning of words like "abstract", "concrete", "computation", "reasoning" and how to link each of this words to mathematics and computer science. I'm no longer able to define any of this in a good way.
Luckily that's okay: we don't need to define these things very precisely.
Jean-Baptiste Vienney (Sep 02 2023 at 22:47):That's painful for my mind. The more I progress in life, the more I realize that everything is complicated and that you can't explain anything in a short and simple way, like it would be in my dreams.
Jean-Baptiste Vienney (Sep 02 2023 at 22:48):I would love everything to be super simple and very organized, in math or anywhere else.
John Baez (Sep 02 2023 at 23:20):I once was like that, but I no longer think it's bad that the world is more complicated than we can possibly understand. For one thing, it would get boring if I understood it well.
Patrick Nicodemus (Sep 03 2023 at 20:01):Mike Shulman said:
Sure, fair enough, there is more to mathematics than proving things. But I don't think any activity of "searching for a proof" can be described as "computation".
To be fair, the whole field of logic programming is based on the insight that much kind of computation can be recast as proof search, and conversely.
Mike Shulman (Sep 04 2023 at 01:07):Sure, but very little of what mathematicians do when searching for a proof falls under the formal heading of algorithmic "proof search".
Ryan Wisnesky (Sep 05 2023 at 17:14):To elaborate on what Mike is saying, one of the failure modes for programmers working in proof assistants is to try to "game" the proof assistant and produce a proof without understanding why it is true. Even with automation, this doesn't work well - we teach that it is a sign to do more math and less programming. So I absolutely agree that proof search in the sense of logic programming or automated theorem moving is usually at a lower level of abstraction that what mathematicians are doing in practice. I don't expect machines to replace mathematicians, but I would like mathematicians to get as much as possible out of machines. I think there's a lot computers have to offer mathematicians, but the best is yet to come- it will no doubt go beyond proof search
Steve Huntsman (Sep 05 2023 at 17:32):I imagine proof search is gonna become more of a thing as AI/ML stuff gets to the point where it impedance matches with tactics better than neophyte users do
Mike Shulman (Sep 05 2023 at 17:36):That's also a failure mode for mathematicians using a proof assistant! I've done it myself. It's tempting because occasionally it does work...
John Baez (Sep 05 2023 at 18:08):@Ryan Wisnesky wrote:
I would like mathematicians to get as much as possible out of machines.
I've gotten out of programming as much as possible, but that's probably not what you meant.