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.
Valeria de Paiva (May 22 2020 at 04:11):hey Rongmin, thanks for the nice message! feel free to ask. I've given several talks about the chops-and-changes of my career, the best one perhaps in the mentoring workshop at LICS2017 https://www.slideshare.net/valeria.depaiva/weapons-of-math-construction. but slides mostly don't have the narration of the story, so feel free to ask!
(=_=) (May 22 2020 at 04:46):What led you to study logic under Martin Hyland? Did you have a philosophical motivation, like John did initially? Or did you have a different motivation?
Valeria de Paiva (May 22 2020 at 05:02):Rongmin Lu said:
What led you to study logic under Martin Hyland? Did you have a philosophical motivation, like John did initially? Or did you have a different motivation?
well, I had done a master thesis in Algebra, (normed algebras, Hurwitz-Radon theorem) and I wanted to do something that was related to Computing, something that you could explain to your friends, something related to logic and mathematics. I had vaguely heard about toposes in the Handbook of Mathematical Logic. so I wrote to Robin Gandy, as a logician in Oxford and asked if he could be my supervisor, if I managed to get the money to attend Oxford. He wrote back a lovely hand-written letter saying he was about to retire in two years, so was not accepting new students and hence maybe I should go to Cambridge instead, and work with his ex-student, Martin Hyland. Robin died in 1995 and I wish I had been more confident to talk to him more before that. but I'm pleased to say that I managed to thank him for sending me to Martin, who is simply fantastic!
(=_=) (May 22 2020 at 05:04):Valeria de Paiva said:
I wanted to do something that was related to Computing, something that you could explain to your friends
Oh gosh, I can soooo relate to that. :sweat_smile:
Valeria de Paiva (May 22 2020 at 05:13):Rongmin Lu said:
Valeria de Paiva said:
I wanted to do something that was related to Computing, something that you could explain to your friends
Oh gosh, I can soooo relate to that. :sweat_smile:
well, during my masters I also spend most Sundays going up some slums in Rio, part of something called MUSP (Movement University at the Service of the People). we provided plans for sewage systems, for electricity, helped with the writing of petitions to the governor, the usual kind of stuff. I felt that my engineering friends had much more to offer.
(=_=) (May 22 2020 at 05:22):Valeria de Paiva said:
well, during my masters I also spend most Sundays going up some slums in Rio, part of something called MUSP (Movement University at the Service of the People). we provided plans for sewage systems, for electricity, helped with the writing of petitions to the governor, the usual kind of stuff. I felt that my engineering friends had much more to offer.
Back when I was in Adelaide doing my PhD, I used to know someone who was doing applied maths, but had also volunteered extensively with Engineers Without Borders. I'd never really felt that way about engineers, but as my research topic got more and more esoteric, it did start to feel more and more lonely.
John Baez (May 22 2020 at 05:34):When did you start work with Martin Hyland, Valeria?
(=_=) (May 22 2020 at 05:35):What was the idea that led to the work on Dialectica categories?
Valeria de Paiva (May 22 2020 at 05:39):John Baez said:
When did you start work with Martin Hyland, Valeria?
I got to Cambridge in 1984 and did the dreadful Part III of the Mathematical Tripos. (another messing up on my part, as I had hoped that I would not have to do qualifying exams in England, boy, how wrong I was!) Even Hardy thought PArt III was ghastly.
John Baez (May 22 2020 at 05:55):But presumably you survived this test well enough to proceed.
What sort of stuff did you learn from Hyland and/or Johnstone? I always wonder how their students actually learned category theory. (The British system is so different from the US one.)
Valeria de Paiva (May 22 2020 at 06:04):Rongmin Lu said:
What was the idea that led to the work on Dialectica categories?
oh cool, I almost missed this! When Dana Scott was visiting Cambridge, Martin thought he might as well give me a problem to work on, so we had one of our fun cake-and-tea meetings, with Dana, Pino Rosolini, Edmund Robinson. Martin described this category and asked me to prove that it was cartesian closed (like good type-theoretical cats ought to be). I tried, and tried, and finally had to come to Martin and say: sorry the best I can do is to prove it's monoidal closed. it has a tensor and internal-hom and the adjunction works. but the tensor is not a product! instead of being disappointed Martin looked and said, ah, I think Girard has been saying interesting things about situations like this. let us check it out! then when we went to
Categories in Computer Science and Logic: Proceedings of the AMS-IMS-SIAM Joint Summer Research Conference Held June 14-20, 1987 in Boulder, CO, Robert Seely was very generous and offered me his slot in the program to talk about this model of Linear Logic!
Valeria de Paiva (May 22 2020 at 06:17):John Baez said:
But presumably you survived this test well enough to proceed.
What sort of stuff did you learn from Hyland and/or Johnstone? I always wonder how their students actually learned category theory. (The British system is so different from the US one.)
yep, there were several courses of "Category Theory" in Part III. A bit like the "Homological Algebra" you've mentioned, they'd lecture on different subjects, under the same title. I had the serious difficulty of not speaking English very well. I had been planning (until I got Gandy's letter) to go to Paris, so I could read English, no problem, but understanding it was a different story. the situation was so bad that I thought the acronym TFAE (the following are equivalent) were the initials of some mathematicians and I thought oh my these guys are everywhere! The French red tape was slow, so I only got my acceptance from Paris 7 when I was already sitting in one of the Mill Lane Lecture rooms
John Baez (May 22 2020 at 06:22):Heh, that's great about TFAE.
John Baez (May 22 2020 at 06:25):I've heard about Part III and gotten the idea that this is where Cambridge mathematicians actually learn a lot of stuff. My student Aaron Lauda - an undergrad student of mine at U.C. Riverside - went to Cambridge for grad school to study with Hyland, and I think he took Part III and immersed himself in lots of courses.
John Baez (May 22 2020 at 06:26):Is this Part III at all related to the the Part III of the Mathematical Tripos? It's all so mysterious to me....
Valeria de Paiva (May 22 2020 at 06:27):John Baez said:
Heh, that's great about TFAE.
my first year in Cambridge Peter Johnstone also taught "Syntectic Differential Geometry" using Anders Kock book. again I worked like a horse to understand the lectures and was shocked to see a phd thesis two years later with some of the exercises that we were supposed to hand in.
Valeria de Paiva (May 22 2020 at 06:30):and yes, it's the Part III of the Mathematical Tripos, which has all sorts of funny traditions. my class had both Tim Gowers and Imre Leader!!
David Michael Roberts (May 22 2020 at 12:27):Heh, he's taught that again in the past decade, as a way of airing the material from the SDG chapter in Elephant part 3.
Morgan Rogers (he/him) (May 22 2020 at 12:42):I wish he'd done it for my class a few years back, but there aren't enough active category theorists in Cambridge any more for there to be more than an introductory CT course for Part III students...
Valeria de Paiva (May 22 2020 at 16:05):back to
What was the idea that led to the work on Dialectica categories?
I think Martin was thinking of internal versions of implications. Because there is Phil Scott's The ``Dialectica” Interpretation and Categories Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 24 (31-36):553-575 (1978). but this is purely syntactic, it's not Proof Theory in the Abstract, as in Martin's 2004 article for Troelstra's fest. what's exciting about dialectica categories is that all the action happens in the morphisms themselves.
John Baez (May 22 2020 at 23:35):I feel embarrassed that I don't understand Dialectica categories at all.
John Baez (May 22 2020 at 23:35):It's my fault for not studying them. And none of my students has explained them to me yet, either.
John Baez (May 22 2020 at 23:37):It it's not too annoying, could you say a bit to someone like me - someone who doesn't know what a dialectica category is - what's the key idea behind them?
John Baez (May 22 2020 at 23:38):I hear they give models of linear logic, so I don't need to hear that, I need to hear some idea about how you build them.
John Baez (May 22 2020 at 23:38):But only if you want to!
Alexander Kurz (May 23 2020 at 03:46):Thank you Valeria, and to John an Rongmin for asking the questions. I always thought mathematicians do not know enough about their history, so I thoroughly enjoy hearing about this.
(=_=) (May 23 2020 at 03:47):Alexander Kurz said:
Thank you Valeria, and to John an Rongmin for asking the questions. I always thought mathematicians do not know enough about their history, so I thoroughly enjoy hearing about this.
Thank you, Alexander, for your kind appreciation. I feel the same too, which is why I came up with this idea. It seems to be taking off quite nicely so far, fingers crossed. :sweat_smile:
Joachim Kock (May 23 2020 at 12:02):Hi Valéria,
thanks for this too. I too would like to hear about dialectica categories, what they are, and what they are good for, etc. If you feel like it.
Valeria de Paiva (May 23 2020 at 14:42):John Baez said:
I feel embarrassed that I don't understand Dialectica categories at all.
hey, so sorry I was making dinner, eating and drinking, and only saw this now. Sure! talking about dialectica cats is something I never get tired of. I am giving a purely mathematical talk, just going over definitions and theorems to Andres Villaveces undergrad students on the 8th june. but chatting about it is much much more fun.
there are by now several variations on the cats, but originally there were two classes DC and GC (where C a cartesian closed cat with some extra strux). DC was the original Martin suggestion (based on Goedel's interpretation of the implication) and when I presented it in Boulder, Girard suggested the categories GC, where the G is for him. both DC and GC have the same objects triples (U, X, alpha), where alpha is a relation between U and X. the important thing is (as usual) the morphisms. between (U, X, alpha) and (V, Y, beta), we have a pair of maps f:U-->V and F:Y-->X satisfying a logical condition (if alpha(u, Fy) then beta(fu,y)).
Now it is hard to say what's the key idea behind these definitions, because it depends on your perspective. but let me try this one on you: it's a model construction for several logics (ILL, CLL, syntactic calculus,IL): what makes it interesting is the feeling that the left-hand side of the maps is like proving a theorem, while the right-handed side is like trying to refute the theorem. So it is like a superpower game: you don't go through the rounds, prover and verifier lay down their full strategy and check what would've have happened, either prover wins, or they lose it--verifier wins or the game is undetermined.
there is a whole different story, if you prefer to compare dialectica categories to Chu spaces, but that it's kind of written down in TAC (DIALECTICA AND CHU CONSTRUCTIONS: COUSINS?). Ask more as questions are the best!
(=_=) (May 23 2020 at 14:54):Valeria de Paiva said:
hey, so sorry I was making dinner, eating and drinking, and only saw this now.
Glad to have you back! No need to apologise, John had excused himself for dinner and shopping, so it's no big deal. We'll just keep asking questions whenever we have some, and you can respond to those questions whenever you like.
(=_=) (May 23 2020 at 15:11):Valeria de Paiva said:
what makes it interesting is the feeling that the left-hand side of the maps is like proving a theorem, while the right-handed side is like trying to refute the theorem. So it is like a superpower game: you don't go through the rounds, prover and verifier lay down their full strategy and check what would've have happened, either prover wins, or they lose it--verifier wins or the game is undetermined.
So this sounds like something game-theoretic, but you're also saying that it's static, as in prover and verifier are able to check immediately whether or not they've won? How does this differ (or does it differ) from an iterated game like what happens, say, in GANs or reinforcement learning?
Henry Story (May 23 2020 at 15:14):Valeria de Paiva said:
So it is like a superpower game: you don't go through the rounds, prover and verifier lay down their full strategy and check what would've have happened, either prover wins, or they lose it--verifier wins or the game is undetermined.
Ah so it really is related to dialog in a way (I was wondering about the use of the word Dialectica).
Is it not about this time that Abramsky gave his Game Semantic analysis of Linear Logic too?
From what I understand from the above, you are looking at the whole game in one go. In the book I read recently "Immanent Reasoning or Equality in Action" that is considered the strategy level. Are there any other major differences? Advantages of using Dialectica over Game Semantics or Dialogical reasoning as in the book I just mentioned?
(=_=) (May 23 2020 at 15:19):Henry Story said:
Ah so it really is related to dialog in a way (I was wondering about the use of the word Dialectica).
Dialectica actually refers to the journal in which Gödel published his interpretation of Heyting arithmetic. It is kind of related, but perhaps one step removed.
Valeria de Paiva (May 23 2020 at 15:21):Rongmin Lu said:
Valeria de Paiva said:
what makes it interesting is the feeling that the left-hand side of the maps is like proving a theorem, while the right-handed side is like trying to refute the theorem. So it is like a superpower game: you don't go through the rounds, prover and verifier lay down their full strategy and check what would've have happened, either prover wins, or they lose it--verifier wins or the game is undetermined.
So this sounds like something game-theoretic, but you're also saying that it's static, as in prover and verifier are able to check immediately whether or not they've won? How does this differ (or does it differ) from an iterated game like what happens, say, in GANs or reinforcement learning?
yes, I say that's a strange approximation of a game, where the powerful don't have to play, they just say what they would do and everyone sees whether this means a win or not. (a win is just getting a 1 instead of a zero, after all in the basic version) what's is fun is that this kind of over-simplification can be used in so many directions, like "small cardinals of the continuum". but I have no idea how or if relates to GANs or reinforcement learning.
(=_=) (May 23 2020 at 15:25):Valeria de Paiva said:
yes, I say that's a strange approximation of a game, where the powerful don't have to play, they just say what they would do and everyone sees whether this means a win or not. (a win is just getting a 1 instead of a zero, after all in the basic version) what's is fun is that this kind of over-simplification can be used in so many directions, like "small cardinals of the continuum". but I have no idea how or if relates to GANs or reinforcement learning.
Right, it does sound like it's probably a different thing. GANs and reinforcement learning are iterated games, so they're dynamic in nature.
(=_=) (May 23 2020 at 15:27):How did that lead to your more recent work in NLP? I know from elsewhere that there are connections, but what was the path that you took?
Valeria de Paiva (May 23 2020 at 15:35):Henry Story said:
Valeria de Paiva said:
So it is like a superpower game: you don't go through the rounds, prover and verifier lay down their full strategy and check what would've have happened, either prover wins, or they lose it--verifier wins or the game is undetermined.
Ah so it really is related to dialog in a way (I was wondering about the use of the word Dialectica).
Is it not about this time that Abramsky gave his Game Semantic analysis of Linear Logic too?
From what I understand from the above, you are looking at the whole game in one go. In the book I read recently "Immanent Reasoning or Equality in Action" that is considered the strategy level. Are there any other major differences? Advantages of using Dialectica over Game Semantics or Dialogical reasoning as in the book I just mentioned?
well, as Rongmin explained the name is only about the journal. Mike Shulman finds this terrible, I think it's perfectly sensible. Goedel didn't give a name to his interpretation, people probably referred to it as the interpretation that Goedel published in Dialectica, from there to the Dialectica interpretation is an easy step.
this is long (5 years?) before Abramsky and Jagadeesan's game semantics, which was based on earlier work of Blass (in the 70s, if I remember what I read in Blass). I haven't seen the book you mentioned! but there are billions of books in games that I haven't read. I tried to write an EPSRC project to study the game aspects of Dialectica, but it was not accepted. I wish I could find it again.
(=_=) (May 23 2020 at 15:41):Unfortunately, it's late and getting cold here, so I'm going to bed for now, but I'll see if I have more questions after I wake up.
Henry Story (May 23 2020 at 15:46):That one step removed confused me, as I could not tell if it had something to do with Games. But it does, and it is an interpretation of Linear Logic. So that makes two interpretations of Linear Logic then. Now I know when I should look at Dialectica :-)
Valeria de Paiva (May 23 2020 at 15:49):Rongmin Lu said:
Unfortunately, it's late and getting cold here, so I'm going to bed for now, but I'll see if I have more questions after I wake up.
good night!!
Henry Story (May 23 2020 at 15:49):Where would one look to the Dialectica interpretation of Linear Logic rather than Abramsky's Game Semantics?
(a bit over 1½ years ago I came across Abramsky and Jagadeesan's work, and since then I have started seeing games appear everywhere)
Valeria de Paiva (May 23 2020 at 15:52):Henry Story said:
That one step removed confused me, as I could not tell if it had something to do with Games. But it does, and it is an interpretation of Linear Logic. So that makes two interpretations of Linear Logic then. Now I know when I should look at Dialectica :-)
two interpretations of Linear Logic? surely there are many many more?
you can find links to stuff I know about Dialectica categories in https://github.com/vcvpaiva/DialecticaCategories
and yes I agree that there are games everywhere!
(=_=) (May 23 2020 at 22:26):I'm up again, but I need to head out before the wild weather hits the city.
(=_=) (May 23 2020 at 22:36):@Joachim Kock said:
Hi Valéria,
thanks for this too. I too would like to hear about dialectica categories, what they are, and what they are good for, etc. If you feel like it.
Hi Joachim,
I'm glad you appreciate this, and would be honoured if you could also tell us about the ideas in your career as well. I believe you have an interesting story to tell, particularly since you've studied in Valeria's home country of Brazil.
This is strictly voluntary, so please feel free to accept the invitation when you're ready and have the time. I should remark that there should be no time pressure whatsoever in doing an AMA: we ask questions whenever we have them, and the people doing the AMA answer whenever they have the time.
(=_=) (May 23 2020 at 22:40):Valeria de Paiva said:
well, I had done a master thesis in Algebra, (normed algebras, Hurwitz-Radon theorem)
I forgot to ask, but who was your advisor for this, and what made this topic interesting for you at that time?
(=_=) (May 23 2020 at 22:45):Valeria de Paiva said:
you can find links to stuff I know about Dialectica categories in https://github.com/vcvpaiva/DialecticaCategories
Thank you, that's a nice list!
John Baez (May 23 2020 at 23:17):@Valeria de Paiva wrote:
Both DC and GC have the same objects triples , where alpha is a relation between and . the important thing is (as usual) the morphisms. between and , we have a pair of maps and satisfying a logical condition (if then .
John Baez (May 23 2020 at 23:24):Great, this is something I can sink my teeth into.
1) If your "if then" at the end were an "iff", this would remind me a lot of an adjunction. But you really want an "if then"? I guess so, since you said so.
2) How is this connected to your remark
the left-hand side of the maps is like proving a theorem, while the right-handed side is like trying to refute the theorem.
I must be dumb, but I don't see the connection, even vaguely. If we take that view of things, what are and ?
3) A complete digression. If we have poset-enriched categories and functors and we could talk about a "lax adjunction" where for all , we have
Does anyone think about these? I thought of this based on what you said.
Valeria de Paiva (May 24 2020 at 01:04):John Baez said:
Great, this is something I can sink my teeth into.
1) If your "if then" at the end were an "iff", this would remind me a lot of an adjunction. But you really want an "if then"? I guess so, since you said so.
2) How is this connected to your remark
the left-hand side of the maps is like proving a theorem, while the right-handed side is like trying to refute the theorem.
I must be dumb, but I don't see the connection, even vaguely. If we take that view of things, what are and ?
3) A complete digression. If we have poset-enriched categories and functors and we could talk about a "lax adjunction" where for all , we have
Does anyone think about these? I thought of this based on what you said.
hi,
about
But you really want an "if then"? I guess so, since you said so.
yes, I do want an "if-then", not an if and only if. If you take the (adjunction) "iff" you end up with a morphism like a Chu-morphism and eventually (depending on which calculations you want to do) you actually don't need "two-sides" of the world, only one, as by using the equality everything you do is dual.
I must be dumb, but I don't see the connection, even vaguely
I agree that this is not obvious at all, but the point is that the direction forward works like many categorical models would, it satisfies the laws you'd expect, like products allow for projections, coproducts for injections, realizability-like satisfaction of implication is ok, if you satisfy the antecedent, then you get the consequent, etc.
the right-hand side is not exactly an "op", but like it. and it's this (wrong) side of the world that enforces linearity of the constructions. so think of elements of U,V are proofs of alpha, beta
and elements of X,Y as refutations of alpha,beta. and think of the if-then condition as a lax form of the adjunction one you were expecting. the point is that when you move from the cartesian world to the monoidal world you also move from isos
F(A&B) = FA&F(B) to lax transformations F(A)\otimes F(B)--> F(A\otimes B) satisfying the required coherence.
Also one think that is important is that when you transpose one object you don't get its negation, you need to negate the relation too. so the negation of (U,X, alpha) is (X,U, not alpha) and this is not like classicla negation (not not A=A) but like intuitionistic negation A |- not not A, but not vice-versa.
and sure about lax adjunctions, this is exactly what's happening here. the same way Street wrote his seminal paper on the Formal theory of Monads and there were, if I remember correctly 16 possible categories of monads, depending on the directions you wanted to reverse, I think there are plenty of ways to weaken the adjunction categories. I have not tried to do it.
Valeria de Paiva (May 24 2020 at 02:43):Rongmin Lu said:
Valeria de Paiva said:
well, I had done a master thesis in Algebra, (normed algebras, Hurwitz-Radon theorem)
I forgot to ask, but who was your advisor for this, and what made this topic interesting for you at that time?
oops, missed this one. my Master's supervisor was Prof Duane Randall http://people.loyno.edu/~randall/#publications.
I had done some undergrad thinking about models of growth and PDEs, which I thought were boring. Prof Randall allowed me to think about lots of things, the theorem was neat and the mathematics needed to prove it was pretty advanced (fiber bundles in Husemoller's book). I struggled, as I wasn't sure I wanted to do mathematics. but since I had done one year of journalism, a half year of Law and one and a half years of Physics, I thought I will just finish this and see what comes next. I only fell in love with mathematics long after the trauma of Part III. maybe actually only when I moved to California and had been at Xerox PARC for a few years.
Valeria de Paiva (May 24 2020 at 03:45):Rongmin Lu said:
How did that lead to your more recent work in NLP? I know from elsewhere that there are connections, but what was the path that you took?
hey, keep missing things in this feed...
well, the connection between dialectica categories and NLP is via the work on Glue Semantics. Glue is a semantic interpretation of LFG (Lexical Functional Grammar), the grammatical theory that the work on the Xerox Language Engine (XLE) is based on.
https://en.wikipedia.org/wiki/Glue_semantics. Glue uses multiplicative linear logic as its basic mechanism for composition of meanings of bits of sentences. so I spend one year visiting PARC, before I joined in 2000, just talking and learning about glue. When I joined it was decided that Glue was very sophisticated and that the implemented system was going to use Transfer Semantics instead, easier and cheaper to implement. Transfer is the basis of what I am still using nowadays. if anyone feels like trying it out, our new semantic parser system is open source and has a demo at http://lap0973.sprachwiss.uni-konstanz.de:8080/sem.mapper/. it's the doctoral work of Katerina Kalouli (from Konstanz, Germany) and I am extremely proud of her work. a full implementation from scratch, with different grammar theory, different parser, but a similar logic to the PARC Bridge system that I worked on.
Valeria de Paiva (May 24 2020 at 04:16):Joachim Kock said:
Hi Valéria,
thanks for this too. I too would like to hear about dialectica categories, what they are, and what they are good for, etc. If you feel like it.
hey Joachim! assuming that you've got what are the dialectica cats (see above or below), two important points as far as the Dialectica and Linear Logic (LL) connections go. the first is that since I was doing it in 1987, more or less when LL was coming up, it actually gave it LL a bit more of a pedigree, as Goedel's name is still pretty powerful and LL seemed to some people very strange then. But more importantly, Girard's coherence spaces are a collapsed model of LL, dialectica categories keep structures apart: tensor and cartesian products are distinct, not equiprovable at all! at that stage many people thought only categorical products were worth some attention and the fact that linear logic insists on monoidal closed structures and not cartesian structures was a source of disbelief. the fact that the semantic model from where Girard abstracted away his logic did not satisfy the existence of the two monoidal structures was a minus. (even today reddit sent me a message of someone complaining how come there is a logic that is not monotonic? if a logic is not monotonic, how can it call itself logic? sigh!) but what was really neat and exciting about the first dialectica model was that I could provide a ! (an of course modality) that is co-free and that is not simply syntax in disguise. the proof that it generates a model of IL is a single line! I could and should've have written it in my paper from Boulder 87, in generic form, as Robert Seely did. but I only wrote the version I needed, the one for my own category DC. a rookie mistake for sure!
Valeria de Paiva (May 24 2020 at 04:34):Alexander Kurz said:
Thank you Valeria, and to John an Rongmin for asking the questions. I always thought mathematicians do not know enough about their history, so I thoroughly enjoy hearing about this.
Great that you're enjoying it Alexander! feel free to ask more questions. I agree that we don't write enough about our own history. I have only one more historical paper, Elements of categorical logic: fifty years later, V de Paiva, A Rodin, Logica Universalis 7 (3), 265-273, which counts the beginning of "categorical logic" from Bill Lawvere's seminal phd thesis written under Eilenberg in 1963. but I have many controversial opinions on the subject!
James Wood (May 24 2020 at 08:37):John Baez said:
2) How is this connected to your remark
the left-hand side of the maps is like proving a theorem, while the right-handed side is like trying to refute the theorem.
I must be dumb, but I don't see the connection, even vaguely. If we take that view of things, what are and ?
Am I right in thinking here that Dialectica categories (and similarly Chu spaces) are very big (informally), and when we use them to model linear logic, we actually only end up using much smaller full subcategories? I think this is part of what makes their reading unintuitive – in particular why the pairing relation feels very loose and difficult to pin to any specific idea.
Nikolaj Kuntner (May 24 2020 at 11:47):Bildschirmfoto-2020-05-24-um-13.42.04.png
My search results appear to be intimidating.
Valeria de Paiva (May 24 2020 at 15:11):James Wood said:
John Baez said:
2) How is this connected to your remark
the left-hand side of the maps is like proving a theorem, while the right-handed side is like trying to refute the theorem.
I must be dumb, but I don't see the connection, even vaguely. If we take that view of things, what are and ?
Am I right in thinking here that Dialectica categories (and similarly Chu spaces) are very big (informally), and when we use them to model linear logic, we actually only end up using much smaller full subcategories? I think this is part of what makes their reading unintuitive – in particular why the pairing relation feels very loose and difficult to pin to any specific idea.
I don't understand your question.
we actually only end up using much smaller full subcategories
I don't think so. Every object of DSets or GSets is a linear logic proposition. whether anyone needs that proposition or not. but even if this had been the case (i.e even if we only used smaller full subcategories), I wouldn't see why it would make them unintuitive. and of course, I don't think they're unintuitive.
as a definition they're as good or bad as any category like the comma categories or the categories of actions of a group or orbits of elements or any category where you have objects plus some some sort of map relating them. actually they're much easier than something as simple an "automaton".
the only thing that is unintuitive is the attempt to add to them an a posteriori logical explanation, more than the one that they naturally have, per their structure.
Valeria de Paiva (May 24 2020 at 15:14):Nikolaj Kuntner said:
Bildschirmfoto-2020-05-24-um-13.42.04.png
My search results appear to be intimidating.
why intimidating?
this is only one informal talk in a meet-up.
David Michael Roberts (May 25 2020 at 08:46):Well, since this is an 'ask anything session', and you seem to be in touch with British categorists (such as they are), do you have any inside rumours on Johnstone's progress through volume 3 of the Elephant?
(=_=) (May 25 2020 at 08:52):David Michael Roberts said:
Well, since this is an 'ask anything session'
This is a themed "ask anything" session. The theme is "history of ideas". Rumours are not history. Tsk tsk. :smiley:
I mean, you can ask, but they can also ignore.
David Michael Roberts (May 25 2020 at 08:58):Well, ok. It was a long shot, in any case :)
(=_=) (May 25 2020 at 08:59):Props to you for trying. I think this topic has come up somewhere before, and the response was inconclusive.
David Michael Roberts (May 25 2020 at 09:00):Yeah, it was me then, as well.
(=_=) (May 25 2020 at 09:13):Valeria de Paiva said:
I had done one year of journalism, a half year of Law and one and a half years of Physics
I'd have loved the chance to take some journalism classes, but unfortunately that wasn't on the menu. I did do an elective in business law and aced that, though, which made me question my choice of major. :sweat_smile:
Any recollection of what you'd studied in journalism, law and physics?
I only fell in love with mathematics long after the trauma of Part III. maybe actually only when I moved to California and had been at Xerox PARC for a few years.
You were at Birmingham when you got the visiting position at PARC. How did that come about?
Valeria de Paiva (May 25 2020 at 12:02):David Michael Roberts said:
Well, since this is an 'ask anything session', and you seem to be in touch with British categorists (such as they are), do you have any inside rumours on Johnstone's progress through volume 3 of the Elephant?
hi, no I'm afraid I do not.
but I do disapprove of
British categorists (such as they are)
there are plenty of very good British categorists
David Michael Roberts (May 25 2020 at 12:35):I mean: given their declining number! Not at all a reflection on their quality :embarrassed:
Valeria de Paiva (May 25 2020 at 12:58):Rongmin Lu said:
Any recollection of what you'd studied in journalism, law and physics?
Well, I didn't like the courses in the School of Communications at all. they were very superficial and I thought I was not learning anything. but I love the friends I made there and some I'm still in contact with. meanwhile, I still like the stuff about Law (I have two recent papers on using AI for law and one on the works) but I thought the course was too boring, I wasn't going to be learning stuff by rota when I was 17. so I took the big examination we have in Brazil to get into university again and moved on to Physics. but then I got very disappointed with Physics because one day they say friction is negligible, the next day is the only thing you need to consider! I didn't like that at all. and I hated that the physicists were always one semester ahead of the Calculus you were learning in school, so you had to unlearn the bad ways of the physicists, before you could really make some progress in Analysis! (yeah, I know this is not going to get me any friends in this crowd, but this was how I felt then). So I ended up doing mathematics not because I loved it, but because it was the less boring thing I tried. And I thought I'd do a phd, to travel the world, but that after that I would do something more interesting like History or Literature for a living. But as everyone around here knows, these interesting things are the hard ones, mathematics is by comparison very easy. and satisfying. your theorem might be in fashion or not, but with a bit of luck is always true, it doesn't stop being correct. and you put correct things together and they carry on being correct. they don't stop for no good reason. I love that about mathematics! and there is so much of it, so much to learn! I also love this!
I only fell in love with mathematics long after the trauma of Part III. maybe actually only when I moved to California and had been at Xerox PARC for a few years.
You were at Birmingham when you got the visiting position at PARC. How did that come about?
yeah, that. I had a two-body problem. I loved my job in Birmingham, my collaborators, and the research that we were doing.
But my husband commuted 3 hours a day to Nottingham where he worked. we had two tiny ones and Xerox made him an offer that we couldn't refuse. I was foolish enough to believe that because I had spent 5 years in the Computer Lab, Cambridge as a postdoc and had a permanent position in Birmigham that I would be able to find a job in the Bay Area. But in the Bay Area I fell between two stools: my work in Computing was too mathematical for the guys and my mathematical work was not good enough for the mathematicians. So I pivoted, as they do here, and became an AI person. had two great mentors for that: Danny Bobrow and Ron Kaplan, my managers at PARC.
(Sorry @Rongmin the formatting in zulip still defeating me!)
Fabrizio Genovese (May 25 2020 at 13:45):Valeria de Paiva said:
I still like the stuff about Law (I have two recent papers on using AI for law and one on the works)
This is interesting. I'm chatting quite a lot with Vlad Zamfir from ethereum later about law and governance issues. Are you aware of the work they are doing there?
Fabrizio Genovese (May 25 2020 at 13:46):Basically blockchain stuff is completely decentralized, stuff like "code is law" sucks and they need to implement trustless forms of governance/law. So there's definitely a lot to be said about this. I'd be glad to chat about this more in depth, I think we may have something worth collaborating on!
Valeria de Paiva (May 25 2020 at 14:01):Fabrizio Genovese said:
Valeria de Paiva said:
I still like the stuff about Law (I have two recent papers on using AI for law and one on the works)
This is interesting. I'm chatting quite a lot with Vlad Zamfir from ethereum later about law and governance issues. Are you aware of the work they are doing there?
Cool. and no, not aware of this work at all.
but I have a feeling we're talking at cross purposes as the work I'm referring to has to do with using NLP techniques to extract entities and relations and make middle-domain ontologies from law texts, decisions and regulations. (my basic idea is that reading law documents is really boring, but necessary. we need systems to help us decipher the essential bits.)
Henry Story (May 25 2020 at 14:43):Oh, interesting. I have been following a bit of law recently via Mireille Hildebrandt (Twitter), who has recently released the book Law for Computer Scientists and Other Folks. Perhaps you know her?
Valeria de Paiva (May 25 2020 at 14:55):Henry Story said:
Oh, interesting. I have been following a bit of law recently via Mireille Hildebrandt (Twitter), who has recently released the book Law for Computer Scientists and Other Folks. Perhaps you know her?
oh, thanks for the recommendation. the book looks like something I really should read. and no, I do not know her.
Henry Story (May 25 2020 at 15:12):I found the book very helpful coming from computer science.
I am getting to be interested in the law side, from thinking about Identity on the Web and Security. She pointed me to a paper on the relation between the territoriality of the law and the extraterritoriality of the internet. Extraterritorial Jurisdiction to Enforce in Cyberspace? Bodin, Schmitt, Grotius in Cyberspace from 2013, which explains the problem very well.
Thinking of the architecture of the web from Tim Berners-Lee's view there is actually a reasonably easy technical answer that one can put together by using Ontologies published as Linked Data so that they can be readable by browsers to inform people of what jurisdiction the web site they are dealing with is in. I called that the Web of Nations.
Perhaps there is work of yours I can draw on when thinking about this.
I think this project does not need much logic, not even deontic logics, but that has not stopped me looking that way too.
Valeria de Paiva (May 25 2020 at 16:25):Henry Story said:
I found the book very helpful coming from computer science.
I am getting to be interested in the law side, from thinking about Identity on the Web and Security. She pointed me to a paper on the relation between the territoriality of the law and the extraterritoriality of the internet. Extraterritorial Jurisdiction to Enforce in Cyberspace? Bodin, Schmitt, Grotius in Cyberspace from 2013, which explains the problem very well.
Thinking of the architecture of the web from Tim Berners-Lee's view there is actually a reasonably easy technical answer that one can put together by using Ontologies published as Linked Data so that they can be readable by browsers to inform people of what jurisdiction the web site they are dealing with is in. I called that the Web of Nations.Perhaps there is work of yours I can draw on when thinking about this.
I think this project does not need much logic, not even deontic logics, but that has not stopped me looking that way too.
Very interesting proposal. one of my collaborators Hermann Hausler in Rio wanted to use Hybrid Logic for the kinds of situation you're worrying about, I think. the original paper was
Edward Hermann Haeusler, Valeria de Paiva, Alexandre Rademaker. Using intuitionistic logic as a basis for legal ontologies. Proceedings of the 4th Workshop on Legal Ontologies and Artificial Intelligence Techniques. 2010
but I got a bit disheartened with this work, as I thought we needed to be able to do decent information extraction beforehand.
Henry Story (May 25 2020 at 16:58):Valeria de Paiva said:
The original paper was by Edward Hermann Haeusler, Valeria de Paiva, Alexandre Rademaker. Using intuitionistic logic as a basis for legal ontologies. Proceedings of the 4th Workshop on Legal Ontologies and Artificial Intelligence Techniques. 2010
but I got a bit disheartened with this work, as I thought we needed to be able to do decent information extraction
Interesting, I had not come across constructive description logics yet
(even if I had it is only recently that I would have understood what the advantages may be).
Henry Story (May 25 2020 at 17:16):The Web Of Nations would I think only need simple OWL ontologies, as one just wants to describe insititutions, companies, schools, ... in official registries, and relate those registries to the nations and then linke the nations in a web.
But once those web sites are tied to legal spaces like that one can do more interesting things. I put together 13 use cases of which the GDPR one is likely to need more deontic reasoning. The simple ideas is that web sites could publish machine readable GDPR policies, so that end users could set up their rules to automate the tasks of deciding when it is ok to accept a policy without always needing to ask the user to click "yes I accept your cookies".
So I think there are quite a few applications where one can get going without needing to do NLP on law (though that of course would be very useful too, for other applications). It would be interesting to plot out at what point one needs to go beyond simple boolean classical reasoning.
Valeria de Paiva (May 25 2020 at 17:37):Henry Story said:
Valeria de Paiva said:
The original paper was by Edward Hermann Haeusler, Valeria de Paiva, Alexandre Rademaker. Using intuitionistic logic as a basis for legal ontologies. Proceedings of the 4th Workshop on Legal Ontologies and Artificial Intelligence Techniques. 2010
but I got a bit disheartened with this work, as I thought we needed to be able to do decent information extractionInteresting, I had not come across constructive description logics yet
(even if I had it is only recently that I would have understood what the advantages may be).
well, thanks! Because I do think that constructive description logics are very interesting, and this was indeed my idea, one of those papers never properly written:
Constructive Description Logics: what, why and how. (extended draft) Presented at Context Representation and Reasoning, Riva del Garda, August 2006. available from https://www.cs.bham.ac.uk/%7Evdp/publications/papers.html. and yes I think you understand that the advantage would be to have a Curry-Howard and keep track of where the derivation is happening, right?
But Mendler's student Stephan Scheele used it for his phd thesis, so not so bad!
Henry Story (May 25 2020 at 17:56):Valeria de Paiva said:
I think you understand that the advantage would be to have a Curry-Howard and keep track of where the derivations is happening, right?
But Mendler's student Stephan Scheele used it for his phd thesis, so not so bad!
Thanks for the link!
I came across Curry-Howard programming in Scala, where Cats folks bring it up all the time, and indeed it is part ofwhat led me to study CT. (I started reading Lectures on the Curry Howard Isomorphism during X-mas but got sidetracked since then). But I had not seen it mentioned in the context of ontologies which is the other tool I use a lot.
For the moment the best CT description of the Semantic Community Work I have found was @Evan Patterson's Knowledge Representation in Bicategories of Relations which adapts Spivak's work to Relations and so is much closer to RDF.
What I have been looking for is a way to see if one can extend RDF to something that uses some form of light weight modal logic to better deal with contexts. RDF1.1 now has contexts in the form of DataSets, but they don't I think have a semantics for it, and a modal one seemed natural to me. (I see your paper mentions modal logic too).
Henry Story (May 26 2020 at 09:54):I read your two papers on constructive DL quickly, and will need to put time aside to read the thesis. This is very helpful for me, as I have been working with untyped DLs (OWL)as well as with programming strongly typed programming languages. This has led me to wondering how these two fit together. The relation to legal thinking is an extra bonus. :-)
Btw. these papers don't mention category theory. I guess being constructive there is a Topos hiding there. Is there some work there that helps make the connection in an interesting way? Perhaps it is just obvious, or there is not that much gained by looking at things the CT way here?
Valeria de Paiva (May 26 2020 at 18:16):Henry Story said:
This has led me to wondering how these two fit together. The relation to legal thinking is an extra bonus. :-)
oh, they don't fit together, yet. they might eventually.
Btw. these papers don't mention category theory. I guess being constructive there is a Topos hiding there. Is there some work there that helps make the connection in an interesting way? Perhaps it is just obvious, or there is not that much gained by looking at things the CT way quote
Most of my papers don't mention category theory, but it's always there in the background, in the way of thinking about stuff. and it does not need to be a topos, actually most of the time it ain't one. CCCs/simply typed lambda-calculus and extensions have an awful lot of offer, both in terms of constructive modal logic, constructive hybrid logic, constructive description logics, there's lots that we haven't done yet. but yeah, I think there's always lots to be gained by looking at it the CT way. it's just that many times it puts people off, so you don't have to mention it all the time.
let me know if you want to discuss any of this stuff, Scheele's thesis only scratched the surface of what I wanted to do with constructive description logics. (not a criticism of his work, just that thesis are time-bound!) thanks for reading!
Valeria de Paiva (May 28 2020 at 23:31):Rongmin Lu said:
What was the idea that led to the work on Dialectica categories?
@Rongmin Lu , I think we stopped with the questions, but I thought I wanted to say something more, a bit like @John Baez did.
so I did work on Dialectica categories for my thesis and I am still working on applications of that work, these many years later.
but that work moved on into a new logic FILL (full intuitionistic linear logic) and perhaps more importantly the working out the full Curry-Howard-Lambek-Tait correspondence for ILL/FILL/CLL (work with Gavin Bierman, Nick Benton, and Martin Hyland). and then because the difficulty with LL was always the modality !, that takes you back to normal (non-linear) logic, and this modality is the same as the traditional S4 one, this led to several works on Constructive Modal Logics (and the frontiers of categorical logic).
it also led, as you asked, to Natural Language semantics and the work at PARC, on the Bridge system. I've left PARC in 2008 to join the start-up, Cuil which failed 2 years later. and since then I have been working in real industry, as opposed to PARC, a research lab. I've worked both in the sweatshop kind of industry we have in here and in more refined research labs.
I always had this knack for being contrarian: my Linear Logic is different from others Linear Logic, my Linear Lambda-calculus is different from others' linear lambda-calculus, my constructive modal logic is different from (my good friend) Alex Simpson's constructive modal logic. My semantics of English is different from other categorical semantics of English you see around here.
Being a contrarian is hard work, I am very grateful to you for asking the original questions!
Gershom (May 29 2020 at 07:00):Can you explain what the "Tait" is in Curry-Howard-Lambek-Tait?
(=_=) (May 29 2020 at 07:10):Gershom said:
Can you explain what the "Tait" is in Curry-Howard-Lambek-Tait?
I was wondering about that as well. I think the Tait here is William W. Tait, who wrote a paper on Intensional interpretations of functionals of finite type.
(=_=) (May 29 2020 at 07:12):Valeria de Paiva said:
Being a contrarian is hard work, I am very grateful to you for asking the original questions!
What, me, original? Surely you jest! :upside_down:
(=_=) (May 29 2020 at 07:17):Valeria de Paiva said:
I've worked both in the sweatshop kind of industry we have in here and in more refined research labs.
In hindsight, what do you think are the clues you'd look for that'd tell you whether an employer is of the sweatshop kind or the refined kind?
Valeria de Paiva (May 29 2020 at 16:39):Gershom said:
Can you explain what the "Tait" is in Curry-Howard-Lambek-Tait?
Absolutely! Curry-Howard says that types correspond to propositions and terms to proofs of these propositions in ND. Lambek/Lawvere then adds that types correspond to objects in appropriate classes of categories and terms correspond to morphisms in these appropriate categories.
Tait (with this reducibility method) is the one who got the most important bit: that convertibility of lambda-terms really corresponds to simplifying the composition of morphisms, the "engine" of the correspondence, perhaps. check for instance https://www.semanticscholar.org/paper/Extending-the-Curry-Howard-Interpretation-to-and-Gabbay-Queiroz/a5652d3ba731c60321bf5ee799bdeee5b4e70cbc
Valeria de Paiva (May 29 2020 at 16:47):Rongmin Lu said:
Valeria de Paiva said:
I've worked both in the sweatshop kind of industry we have in here and in more refined research labs.
In hindsight, what do you think are the clues you'd look for that'd tell you whether an employer is of the sweatshop kind or the refined kind?
Hmm, it's not hard to tell the difference. it's hard to get jobs on refined research labs. in this industry we live for the stock changes every quarter, when stock tanks, the first thing to go is any kind of development, let alone research.