3 ms·

Is there really any substantial relationship between differential calculus and sequent calculus? You might get the impression there's a unity because different

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.

StandardFuture 6y ago
> any thread unifying these things 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: https://www.youtube.com/watch?v=xLRUofFSq5Y https://www.youtube.com/watch?v=xLRUofFSq5Y Recommended watching! 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.
- bmc7505 6y ago
  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. [1]: https://www.youtube.com/channel/UCDe6N9R7U-RYWA57wzJQ2SQ https://www.youtube.com/channel/UCDe6N9R7U-RYWA57wzJQ2SQ
bmc7505 6y ago
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? [1]: https://arxiv.org/pdf/1606.01642.pdf https://arxiv.org/pdf/1606.01642.pdf [2]: https://lipn.univ-paris13.fr/~kerjean/papers/EDP18.pdf https://lipn.univ-paris13.fr/~kerjean/papers/EDP18.pdf [3]: https://en.wikipedia.org/wiki/Brzozowski_derivative https://en.wikipedia.org/wiki/Brzozowski_derivative [4]: https://dl.acm.org/doi/10.1145/2034773.2034801 https://dl.acm.org/doi/10.1145/2034773.2034801 [5]: http://strictlypositive.org/diff.pdf http://strictlypositive.org/diff.pdf [6]: https://en.wikipedia.org/wiki/Boolean_differential_calculus https://en.wikipedia.org/wiki/Boolean_differential_calculus
- domnomnom 6y ago
  This looks really cool.
- deleted 6y ago
  [deleted]
tmerr 6y ago
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.
- rsj_hn 6y ago
  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.

StandardFuture 6y ago

> any thread unifying these things 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: https://www.youtube.com/watch?v=xLRUofFSq5Y https://www.youtube.com/watch?v=xLRUofFSq5Y Recommended watching! 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.

bmc7505 6y ago
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. [1]: https://www.youtube.com/channel/UCDe6N9R7U-RYWA57wzJQ2SQ https://www.youtube.com/channel/UCDe6N9R7U-RYWA57wzJQ2SQ

bmc7505 6y ago

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? [1]: https://arxiv.org/pdf/1606.01642.pdf https://arxiv.org/pdf/1606.01642.pdf [2]: https://lipn.univ-paris13.fr/~kerjean/papers/EDP18.pdf https://lipn.univ-paris13.fr/~kerjean/papers/EDP18.pdf [3]: https://en.wikipedia.org/wiki/Brzozowski_derivative https://en.wikipedia.org/wiki/Brzozowski_derivative [4]: https://dl.acm.org/doi/10.1145/2034773.2034801 https://dl.acm.org/doi/10.1145/2034773.2034801 [5]: http://strictlypositive.org/diff.pdf http://strictlypositive.org/diff.pdf [6]: https://en.wikipedia.org/wiki/Boolean_differential_calculus https://en.wikipedia.org/wiki/Boolean_differential_calculus

domnomnom 6y ago
This looks really cool.
deleted 6y ago
[deleted]

tmerr 6y ago

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.

rsj_hn 6y ago
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.