Category Theory
Zulip Server
Archive

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.

Stream: event: ACT20

Topic: July 9: Geoff Cruttwell et al.'s talk

Paolo Perrone (Jul 01 2020 at 20:38):

Hello all! This is the thread of discussion for the talk of Geoffrey Cruttwell, Jonathan Gallagher and Dorette Pronk, "Categorical semantics of a simple differential programming language".
Date and time: Thursday July 9, 21:10 UTC.
Zoom meeting: https://mit.zoom.us/j/7488874897
YouTube live stream: https://www.youtube.com/watch?v=F9Yxw_PlDfY&list=PLCOXjXDLt3pZDHGYOIqtg1m1lLOURjl1Q

Geoff Cruttwell (Jul 09 2020 at 10:27):

Jonathan Gallagher will be giving the talk. Some references:

The "simple differential programming language" (SDPL) referred to in the title is the one recently defined by Abadi and Plotkin (https://arxiv.org/pdf/1911.04523.pdf)
The "categorical semantics" are a combination of reverse differential categories (https://arxiv.org/pdf/1910.07065.pdf) and restriction categories (https://www.sciencedirect.com/science/article/pii/S0304397500003820)
The extended abstract of the talk is here: http://www.reluctantm.com/gcruttw/publications/rdrc-act-extended-abstract.pdf
Implementations of SDPL in Haskell (with some optimizations coming from the categorical semantics) can be found here: https://github.com/jonathan-ll/SDPL-Meta

Paolo Perrone (Jul 09 2020 at 19:45):

Please notice the new Zoom address!

Paolo Perrone (Jul 09 2020 at 21:00):

Hello! This talk will start in 10 minutes. Please notice the new Zoom address, https://mit.zoom.us/j/7488874897

Sam Staton (Jul 09 2020 at 21:41):

Hi Jonathan thanks for your nice talk. Out of interest did you see Gordon Plotkin's recent paper https://arxiv.org/abs/2006.06415 ? He gives an equational presentation of partial differentiation that is Hilbert-Post complete: there can be no other equations without inconsistency. Quite a strong and impressive result, I think. His presentation looks a bit like differential categories. If you've seen it, I wonder if you've thought about what it means for your categorical models.

Jules Hedges (Jul 09 2020 at 21:52):

Following Valeria's question, I also previously noticed dialectica categories show up in one of Gordon Plotkin's other papers, the differentiable curry. I was thinking to email him but never got around to it. Here's a thread I wrote about it at the time: https://twitter.com/_julesh_/status/1185506357748862976

Ideas that pop into my head while reading The Differentiable Curry (https://openreview.net/pdf?id=ryxuz9SzDB):

- julesh (@_julesh_)

Valeria de Paiva (Jul 09 2020 at 22:10):

Jules Hedges said:

Following Valeria's question, I also previously noticed dialectica categories show up in one of Gordon Plotkin's other papers, the differentiable curry. I was thinking to email him but never got around to it. Here's a thread I wrote about it at the time: https://twitter.com/_julesh_/status/1185506357748862976

Yes, nice talk Jonathan! and thanks for the new reference Jules, I had not heard about "the differentiable curry", but I did hear about the partial compilers paper "Mihai Budiu, Joel Galenson, and Gordon Plotkin The Compiler Forest, ESOP 2013, http://budiu.info/work/esop13.pdf slides https://jgalenson.github.io/papers/esop2013-talk.pdf"

Paolo Perrone (Jul 10 2020 at 10:19):

Morning! Here's the video.
https://www.youtube.com/watch?v=jqPgdpBp3QE&list=PLCOXjXDLt3pYot9VNdLlZqGajHyZUywdI

Geoff Cruttwell (Jul 10 2020 at 11:45):

@Jules Hedges, on your twitter, I noticed you said you were thinking about "automatic integration" (https://twitter.com/_julesh_/status/1232997000561463299) @JS Pacaud Lemay has developed notions of "integral category" (https://arxiv.org/abs/1707.08211, https://www.sciencedirect.com/science/article/pii/S1571066118300847). As we've seen in this talk, automatic differentation can be interpreted via (Cartesian reverse) differential categories. Similarly, could automatic integration be interpreted via integral categories? Without knowing the details of automatic integration, I don't know if this actually makes any sense, but thought I'd mention the possible connection to you both.

Just realised that one of the things I've been talking about this week can be summarised as: Like backpropagation, but for integration rather than differentiation

- julesh (@_julesh_)

Jules Hedges (Jul 10 2020 at 12:29):

So the context for this tweet is that I was visiting @Toby Smithe and talking about "bayesian updates compose optically" from his talk. (Cf. my UCR seminar where I proposed that optics are precisely a categorical axiomatisation of "things that look like the chain rule"). The jump from that to this is the (significant minority) view that "integration" and "bayesian inference" are different terms for the same thing