02:44:31 ahmad: to professor Bob my SV Hishamuddin Zainuddin from Malaysia say Hi 02:46:20 Jules Hedges: and this is why Girard invented string diagrams to replace proof trees..... 02:46:46 David Spivak: how does one discover the type of a word in a sentence, e.g. “that” 02:47:13 coecke: Ahmad, pass on my best wishes to Hisham! A few years ago I he invited me over to talk about this line of work. 02:47:51 coecke: David, use a parser; they work very well. 02:48:15 David Spivak: thanks! 02:50:42 David Spivak: did he say what “restricted symmetry” is? 02:50:59 David Jaz: Question 02:51:41 David Jaz: Are the morphisms the derivations, or is this an order where a morphism is the fact that such a sequent is deriveable 02:52:40 Mehrnoosh Sadrzadeh: Derivations corresponds to morphisms 02:53:07 Mehrnoosh Sadrzadeh: David, restricted symmetry just means only banged objects !A can be permuted. 02:53:23 David Spivak: thanks! 02:53:43 David Jaz: Thanks 02:56:04 bob coecke in the Black Pub: Did anyone ever proof completeness/coherence for the clisp in the diagrammatic calc? 02:56:25 Mehrnoosh Sadrzadeh: Gijs did it for the non banged version in WoLLIC 2017. 02:56:40 Nicolas Blanco: Is there weakening for ! 02:56:43 Mehrnoosh Sadrzadeh: The proof for this banged version is still in progress ,,, 02:56:52 Mehrnoosh Sadrzadeh: there is no weakening for ! 02:57:23 bob coecke in the Black Pub: [thumbs up!] 02:57:29 Nicolas Blanco: Thanks 02:59:29 David Jaz: Is this anti-symmetry justified semantically? 03:01:03 David Spivak: yeah, what does it say? 03:02:09 David Spivak: is it as simple as “happy spider” = -“spider happy”? 03:02:52 Aleks Kissinger: for a good ! modality, doesn't !(f) need to be natural w.r.t. to the comonoid? it doesn't seem like the identity comonad has this property 03:03:00 David Jaz: https://youtu.be/5CjSu5hLtcw Mike Shulman has an embedding into *-autonomous categories that allows you to avoid the clasp. I don’t remember the precise statement, but I learned of it in the linked talk 03:06:11 Giovanni de Felice: Does BERT give subject and object vectors for each verb? 03:06:31 Martha Lewis: Do you take BERT sentence embeddings or word embeddings? 03:06:38 Georgios Bakirtzis: What do these numbers mean? 03:06:53 Mehrnoosh Sadrzadeh: It inputs a context, e.g. a subject-verb-object sentence and then gives vectors for the words in there 03:07:09 Georgios Bakirtzis: What does 0.65 mean compared to 0.45 03:07:11 Mehrnoosh Sadrzadeh: The numbers are degrees of precision of the performance of the models 03:07:34 Mehrnoosh Sadrzadeh: 0.65 means in 65 % of times that model was correct 03:07:50 Mehrnoosh Sadrzadeh: 0.45 means in 45% of the times that model was correct 03:08:02 Georgios Bakirtzis: Is the implementation open source? 03:08:06 Mehrnoosh Sadrzadeh: Not yet 03:08:12 Carl Stuendel: Thank you, Lachlan and Hadi. 03:08:16 Martha Lewis: clap clap! 03:08:17 Georgios Bakirtzis: Thanks! 03:08:18 Martha Lewis: Thanks! 03:08:23 Sophie El Agami: Thanks! 03:08:28 Anna Matsui: thanks! 03:08:29 Nicolas Blanco: Great talk, thanks! 03:10:00 Michael Moortgat: Why ! as a relevant modality? It has been claimed that for the linguistic applications something weaker is already enough: the bang of *soft* linear logic (which has !A \vdash A \otimes A, but not !A \vdash !A \otimes !A) 03:10:56 Mehrnoosh Sadrzadeh: Ah Michael, is there a cut-free proof system for that? 03:11:16 Michael Moortgat: sure - see Retore&Moot in JoLLI 03:11:40 Mehrnoosh Sadrzadeh: I guess soft linear logic is cut-free, but would it still be if one adds it to the Lambek Calculus? 03:11:44 Mehrnoosh Sadrzadeh: I will check the paper … 03:11:45 Mehrnoosh Sadrzadeh: thanks 03:11:46 Aleksandar Makelov: so if I understand correctly, BERT provides context-aware embeddings, whereas the word2vec and the other model (don't remember the name) do not take into account the context of the word when providing the embedding. And the categorical approach presented here gives you a way to combine word embeddings in a smarter way than just e.g. adding embeddings? 03:11:47 Michael Moortgat: Journal of Logic, Language and Information (2019) 28:287–307 03:13:03 Mehrnoosh Sadrzadeh: Thanks a lot, we will definitely look at it 03:15:08 Bruno Gavranovic: Fun fact: the original paper that had the king-queen=man-woman interpretation has been shown to be very misleading and doesn't seem to happen at all with these trained word2vec databases 03:15:28 Bruno Gavranovic: I'll try to find a reference 03:15:47 Bruno Gavranovic: https://twitter.com/goodfellow_ian/status/1133528189651677184?lang=en 03:16:14 David Spivak: wow, that’s an important thing to know… 03:16:51 Mehrnoosh Sadrzadeh: But that property was not the most important property of Word2Vec embeddings 03:17:11 Aleksandar Makelov: in general you never get king - queen = man - woman exactly - you instead find a closest embedding to a linear combination of the three words 03:17:20 Bruno Gavranovic: I'm not saying it was, I'm merely remarking on the question from David 03:17:28 Aleksandar Makelov: and yes you might have to "help" this "closest embedding search" 03:17:57 Abel Jansma: People are also trying this latent space arithmetic with latent representation of biological cells now, and the same reproducibility discussion is happening there. 03:18:16 Aleksandar Makelov: still, the fact that word2vec and related models are useful for word analogy tasks suggests that there is *some* way to extract information along those lines from the models 03:19:07 Bruno Gavranovic: @Aleksandar, yeah you are finding the closest embedding, but the issue is that the closest embedding was always one of the other words and they had to hardcode the model not to pick that word 03:19:23 bob coecke in the Black Pub: In all fairness, my main contribution was to put capitals in the name DisCoPy, otherwise it read dis-copy. 03:21:44 Eran Meir: :) 03:26:31 David Spivak: does anyone know a reference for the box product of cats? 03:27:29 Giovanni de Felice: https://ncatlab.org/nlab/show/funny+tensor+product 03:27:58 David Spivak: François Foltz, Christian Lair, and GM Kelly. Algebraic categories with few monoidal biclosed structures or none. Journal of Pure and Applied Algebra, 17(2):171–177, 1980. maybe too 03:28:08 Aleks Kissinger: are there normal forms, modulo interchange in your representation? 03:28:35 Giovanni de Felice: Also this paper on premonoidal categories: 03:28:38 Giovanni de Felice: John Power and Edmund Robinson. Premonoidal categories and notions of computation. 03:29:35 David Spivak: thanks all 03:30:05 Juan Orendain Almada: Thank you for the references 03:31:01 Giovanni de Felice: @Aleks we implemented a normal form method for diagrams that allows to check equality up to interchangers 03:31:03 bob coecke in the Black Pub: So this toolbox was initially produced for our implementation of DisCoCat on a quantum computer (QNLP). I talked about that at the MIT CT seminar. 03:31:30 Giovanni de Felice: The normalisation is based on this paper by Vicary and Delpeuch 03:31:31 Giovanni de Felice: Antonin Delpeuch and Jamie Vicary. Normalization for planar string diagrams and a quadratic equivalence algorithm. arXiv:1804.07832 [cs], April 2018. 03:34:24 Aleks Kissinger: nice. does this rely on the fact that you don't deal w symmetries? 03:35:27 Giovanni de Felice: Yes the Diagram class in miscopy corresponds to planar diagrams, we also implemented a normal form for rigid planar diagrams, I.e. with cups and caps and the snake equation 03:37:18 David Spivak: wow! 03:37:26 Aleks Kissinger: thanks! very cool 03:37:31 Eswaran Subrahmanian: very nice! 03:37:35 Martha Lewis: clap clap! 03:37:35 Carl Stuendel: clap clap clap 03:37:40 Sophie El Agami: Thanks 03:37:41 Nicolas Blanco: clap! 03:37:45 Luca Bonavita: Very cool 03:39:31 Joao Paixão: What is the reference for the polynomial time algorithm? 03:40:02 Paolo Perrone: By the way, if anyone wants to try to make crema di mascarpone now, make sure that you beat the egg white at the very last moment, right before you mix it with the rest - otherwise it loses its texture. Monoidal categories don't tell you that :p 03:40:15 Luca Bonavita: aha 03:40:22 Fabrizio Romano Genovese: Amen to that 03:40:52 Giovanni de Felice: Monoidal categories don’t tell you about that but premonoidal categories do 03:41:20 Fabrizio Romano Genovese: Which makes sense, since egg white loosing texture is a side effect due to time 03:41:33 Giovanni de Felice: You need to interchange the egg beating to the end of the diagram 03:41:39 Paolo Perrone: @giovanni: right! haha 03:41:50 Bruno Gavranovic: I think Aleks was saying to take an off-the-shelf _machine learning_ solution to do that? 03:41:50 Abel Jansma: This reminds me of this package that can turn screenshots of latex TikZ images into valid TikZ code. 03:42:11 Matt Roberts: Interesting talk! 03:42:33 Adittya Chaudhuri: Thanks! 03:44:37 Aleks Kissinger: @A+G: did you guys play with hooking this up to pyzx already? it would be nice, especially for ZX-calculus tutorials to have monoidal-category type notation for creating ZX-diagrams from generators 03:45:30 Aleks Kissinger: currently, there is only QASM and friends, as well as a sortof hack called SQASM (spider-QASM) which does some automatic post-selection 04:00:18 David Jaz: what os special about Bool here? 04:00:43 Jules Hedges: Nothing, we can and do replace that with other things 04:00:50 David Spivak: things of what type? 04:01:13 Jules Hedges: Any commutative monoid works, and I think you can go more general. Maybe Jérémy will talk about that 04:01:39 Bruno Gavranovic: You can replace Bool with any monoid 04:01:41 David Jaz: Thanksgivings 04:01:46 David Jaz: Thanks* 04:01:47 David Spivak: thanks 04:03:24 Toby Smithe: I'm really enjoying this, by the way. It's much neater than all the complicated nonsense I waded through! I'm going to go away and simplify my variant of statistical games, I think 04:06:26 Adittya Chaudhuri: Thanks for the talk. 04:06:47 Jules Hedges: Hm, I don’t know about this….. 04:06:53 Viktor Winschel: So, could we compose different equilibrium concepts, like Nash for some part of the game and Minimax for other parts (regardless of what it means economically) 04:07:30 Toby Smithe: Is there a category of categories of open games? 04:07:38 Bruno Gavranovic: what does it mean to "compose different equilibrium concepts"? 04:09:09 Viktor Winschel: Ok, thanks 04:09:37 Jules Hedges: I suspect there is probably a mixed variance problem 04:09:46 Bruno Gavranovic: Yeah I was asking Viktor 04:10:24 Juan Meleiro: It could mean expressing the two equilibrium conceptz in a more general kind of equilibrium 04:10:41 Juan Meleiro: A sort of poset of equilibrium concepts 04:16:52 Joshua Meyers: try clicking on the X? 04:17:23 Paolo Perrone: nope, that's likely to end the presentation 04:19:26 Juan Meleiro: From listening to you at previous times, I had the impression you already had a working diagram interpreter 04:20:58 David Jaz: not *yet* 04:21:09 Harny Wang: Your goal is a kind of abstract. 04:21:43 Sophie El Agami: Hm the goal seems tangible from a design perspective 04:22:50 Toby Smithe: Question (maybe something that the quantum people might know about): earlier Jules mentioned a thing called a double optic. When I was preparing the diagrams for my paper, I noticed that "double optics" look a lot like the doubling construction from CQM. Does anyone know if this is right? You can see a quick sketch at https://tsmithe.net/misc/doubling-optics.png for the case where the "double optic" is an optical "context", that is, a state in the double optic category. 04:23:26 Toby Smithe: (sorry, the question isn't really related to the content of the talk...) 04:24:02 David Jaz: How does this dsl differ from arrow do notation, other than the missing “prop”? 04:24:10 Viktor Winschel: Statebox has a text-to-string-diagram rendering code called KD editor which produces string diagrams but also Arrow-Haskell code. This might be a visualisation tool for otherwise textual specification of games. However this code might still lacks (not sure) a covariant arrow one needs for the coutility direction of arrows in open games. 04:24:11 David Jaz: “proc” 04:24:33 Bruno Gavranovic: @Toby, do you have a reference for the doubling construction in CQM? 04:24:37 Toby Smithe: er yes 04:24:51 Toby Smithe: i wrote the observation in my extended abstract, let me dig out the reference from there 04:25:51 Aleks Kissinger: @Bruno: https://arxiv.org/pdf/1510.05468.pdf 04:25:57 Toby Smithe: ah thanks aleks 04:26:07 Toby Smithe: yes that's the paper i cited 04:27:02 Aleks Kissinger: its also in Picturing Quantum Processes, with much more explanation and context 04:27:51 Aleks Kissinger: but the "Categorical Quantum Mechanics" papers are meant to be compressed (and free) versions of the material in the book, for people with a bit more CT background 04:28:57 Toby Smithe: the conjecture is 'conjecture 3.3' in my extended abstract, but i don't say much more there than I did here already (and i had to cut the figure i linked above for the EPTCS submission) 04:30:28 David Jaz: Wait, I thought the equilibria were built up compositionally? 04:30:48 Elena Di Lavore: built but not computed I think 04:31:34 Philipp Zahn: representation is compositional; concrete computation (of a compositionally represented game) is not 04:32:05 Toby Smithe: can it not be? at least for my statistical games, the computation of the equilibria was compositoinal as well 04:32:10 Viktor Winschel: I doubt that it is true that equilibrium analysis is economics and not interesting for CT. after all we might use algebraic geometry for example for analysing equilibria defined in polynomials. Actually we do that in economics already with homotopy continuation theory in “computational/numerical economics”. 04:32:13 Bruno Gavranovic: My understanding is that you build up a bigger game from smaller atomic games whose equilibria you know. But mostly in real life you don't know what the equilibrium is of smaller games. I'm not entirely sure, though, what "computation" means here 04:32:17 Toby Smithe: *compositional 04:32:36 Elena Di Lavore: it's not going to be more efficient than a global computation 04:33:05 Philipp Zahn: @toby: there might be cases where this is true but not in general 04:33:34 David Jaz: There is probably some curve. If we have a lot of small games which are the same then it might surpass the whole computation, no? 04:33:42 Viktor Winschel: CT might be help full to advance “compositional numerics” 04:34:02 Toby Smithe: @David, like your dream for your dynamical systems, that is? 04:34:18 David Jaz: Yes haha, I do hope this works 04:34:41 Toby Smithe: @Philipp, yes, I think I can see that: because of the interaction in the best-responses (ie, what player A do might depend on what player B does?) 04:34:58 Toby Smithe: I think all my games were "atomic" so that wasn't an issue 04:35:33 Philipp Zahn: @toby: yes 04:35:50 Toby Smithe: I need to think more about non-atomic statistical games (which of course do crop up when you have interacting cybernetic systems). I have some ideas about that but not particularly well-formed yet 04:36:12 Matthew Di Meglio: The DSL looks very similar to Haskell do-notation, what do you get in the DSL that you couldn’t get from do-notation? Could this be used as a language for building string diagrams, say for typesetting purposes? 04:39:20 Paolo Perrone: Zulip: https://categorytheory.zulipchat.com/#narrow/stream/243068-ACT-2020/topic/July.208.3A.20Jules.20Hedges.20et.20al.2E's.20talk 04:39:26 Bruno Gavranovic: Thanks! 04:39:35 Aleks Kissinger: thanks jules! 04:39:40 Sophie El Agami: Thanks, Jules! 04:39:41 Toby Smithe: thanks jules! 04:39:52 Adittya Chaudhuri: Thanks for the talk! 04:39:55 Abel Jansma: Thanks! 04:40:44 James Fairbanks: Thanks