Is there really any substantial relationship between differential calculus and sequent calculus?
You might get the impression there's a unity because differential calculus has been generalized to functions of many things - calculus on metrices or tensors is analogous to calculus on functions of a real variable. But my impression is the term "calculus" overall, when use in something like sequent calculus or lambda calculus, is just a term for a calculation system. IE, Whether a system is called an "algebra", a "calculus" or something else is more historical accident than any thread unifying these things. But maybe there is such a thread and I just don't know about it.
Surprisingly, there is an interesting proof-theoretic connection between differential and sequent calculus! For a more detailed account of differential linear logic (DiLL), see Erhard [1] and Kerjean [2].
More generally, the same rules from differential calculus have reappeared in strange and marvelous places throughout computer science, including formal language theory [3], parsing [4], type theory [5] and automata theory [6].
We do not attempt to cover all these topics, research is just beginning to understand how they are related. The general theme seems to be, how do you propagate local changes through a computation? Can you compute changes incrementally without restarting from scratch?
Yes, this is the critical question. And I think the authors of this "reading group" answer that in this really smooth introduction to sequent calculus:
The summary (explained in the video) is that these three areas: differential programming, probabilistic programming, and logic programming are all just programming language semantics that are more specifically "languages for calculating" and thus "calculi" languages.
These three areas are also all linked to historical and current AI research. And I think AI research is the primary motivation (another underlying thread) for this collection.
Thank you for your kind remarks! As you mentioned, a better name might have been "languages for calculation". In French these subjects are all "calcul". Personally, I would skip the first few and listen to the guest speakers, who have spent a lot more time thinking about these topics. You might also enjoy the lectures from OPLSS, where I learned about many of these ideas. [1]
These three areas are also all linked to historical and current AI research.
Indeed, they all seem to have some fascinating connections to symbolic and connectionist learning. I think the symbolists were originally on the right track, but they were too preoccupied with expert systems when they should have been working at a much lower level of representation. One way to view the current wave of deep learning is as a form of symbolic differentiation with a special order of evaluation corresponding to reverse-mode AD.
Not a mathematician but every use of the term algebra I have seen has some way related back to what I learned in grade school about sets of real numbers, operations, properties, and how to solve equations. It's the same thing with linear algebra, they just put restrictions on the kinds of equations to solve. Then more ... abstract there is abstract algebra that goes beyond real numbers and looks at other kinds of sets & operations and classifies them as fields, rings, and more. I wonder if there are examples of the term "algebra" that are unrelated to this. If not that might be one difference between algebra and "a calculus" which as you said seems to refer to any system for formal calculation/reasoning.
When most mathematicians use the world "algebra", they mean abstract algebra. It's not so much a research area in itself but there are many interesting subfields. For example, algebraic geometry is in some sense just the study of solutions of polynomials, but there are algebraic analogues of many interesting geometric notions you encounter in plain old Riemmannian geometry. Then there is algebraic number theory, the studies of modules (generalizations of linear algebra), and then you have questions about representation theory, you can ask questions about moduli spaces of curves defined over a field, of vector bundles (or rather "coherent sheaves") defined over a field, classification of m-dimensional algebraic structure up to birational equivalence, resolution of singularities, etc. All of these have purely algebraic analogues and are topics of interest without needing to resort to the real numbers or any analytical techniques. Talking about "algebra" is a bit like talking about "analysis". It's more of a dividing line of techniques than a specific field.
Off topic, but this looks like a well organised, independent learning network. Where can I find others, on serious topics, that are independent of platforms or publishers? Is there an 'awesome' list of topic-based reading groups (not book clubs) for interested learners?
I don't know of a single resource, but I would search for "X [reading group OR journal club]".
Also, many academic associations, like ACM, have Special Interest Groups (SIG). Some SIGs have journal clubs but you might need to become a member or ask someone to add you to their Slack, Discord, etc.
thanks, this helps. i've tried different search terms with little success (descriptors for resource-based independent learning in groups are hard to refine). i'm retired so my professional affiliations have lapsed. and, with the freedom to pursue my interests, the possible topics are all over the place. but i'll look for some SIGs that might work (cultivating Australian native plants, tiny compiler design, etc).
I'm part of a math one, where each individual goes through books in their interest with the guidance of a person who has a PhD. He checks our proofs for us, which is super useful when learning, and is constantly learning new math (and physics) himself. It's platformed in on Discord, though, as that's where we meet. Sadly, I dunno if we'd be able to recreate it if Discord were to close down tomorrow, though we're also all on Reddit.
Just because I'm not the owner of the server, though I have been given permission to ask, look through my comments. I've mentioned it before, and mentioned who to contact on Reddit for it. Just mention you came from hackernews and he'll know it was me.
We have an analytic number theory book club at https://antmeet.github.io/. The reading sessions occur at 18:00 UTC from Monday to Friday. This is a book club though, not a reading group. We meet online and go through each page of the chosen book together. During the meetings, we illustrate the theorems with concrete examples, work out the intermediate steps not explicitly specified in the book, and then discuss any additional insight the club members may have to offer. See https://antmeet.github.io/boards/ for notes from the previous meetings.
You might get the impression there's a unity because differential calculus has been generalized to functions of many things - calculus on metrices or tensors is analogous to calculus on functions of a real variable. But my impression is the term "calculus" overall, when use in something like sequent calculus or lambda calculus, is just a term for a calculation system. IE, Whether a system is called an "algebra", a "calculus" or something else is more historical accident than any thread unifying these things. But maybe there is such a thread and I just don't know about it.