Monday, September 3, 2018

Mirantão and Linear Dependencies

Mirantão, or actually the `Pensão Renascer' in Mirantão is very pretty.  Rustic, with delicious food, very nice people and landscapes to remind you of a Minas Gerais that only exists in the old songs of Milton Nascimento and Fernando Brant.

But Jornadas Mirantão is not about Club de Esquina nor about the world of Guimarães Rosa, re-inventing o sertão. Jornadas Mirantão are about logic and proof theory in beautiful places. So I talked about an old work with Torben Bra\"u ner that I would like to go back to. This is about using linear dependencies between formulas to describe precisely (and without the support of terms) the system called Full Intuitionistic Linear Logic. The slides are in slideshare and the technical report in Cut-Elimination for Full Intuitionistic Linear Logic. (with Brauner). Technical Report 395 from Computer Laboratory, University of Cambridge and BRICS, Denmark. May 1996.

Sunday, August 26, 2018

Playing Mathematician at ICM2018

I am just back from Niteroi, Brazil, where I was Invited Speaker at Logic Satellite event for the International Congress of Mathematicians 2018 (ICM2018) co-organised by the Sociedade Brasileira de Lógica and  DLMPST/IUHPST. This

Division for Logic, Methodology, and Philosophy of Science and Technology

is an alphabet soup that no one can remember properly. The ICM is the  main meeting of  Mathematics around the world, where the Fields Medal, sometimes called the Nobel of Mathematics, is presented every four years. (a bit like the Olympics, really.) I had meant to go for the whole thing, since I have never been to one of these before and since this is the first time it has happened in the Southern Hemisphere, but ended up only being able to go for the Logic event.

The picture of me  comes from Twitter, courtesy of Benedikt Lowe, the Secretary of  the DLMPST 
and one of the main organizers of the logic satellite event. Thanks Benedikt!
I  talked about Relevant Dialectica Categories, which maybe I should talk about in the Nuance NAIL seminar too.

It was very nice of the people in Brazil (especially Bruno Lopes and Samuel Gomes da Silva) to invite me and pay for my trip! and very nice of my manager Charles Ortiz to authorize my PTO. Thank you!
icm2018

Saturday, August 4, 2018

Invited Talks are Fun. Maybe.

I like talking. About work, about politics, about friendship, chit-chat or deep-issues, all are welcome and part of my repertoire.

But yeah, it's especially nice when people ask you to talk about your work. You don't have to submit something and wait for others to decide whether they like it or not, whether they think it's important or not. It's your invited talk, you can do whatever you want. Or so I say.

I feel very lucky to have been invited to talk about my work in a series of occasions. I have a very non-linear working career, with lots of  chop and changing along the way, which, I hope, makes for interesting talks. But clearly also means I don't have all the accolades of the profession. I am, in some sense, still a junior, still hungry to do more work, still not established enough. sigh..

But I digress: the reason I wanted to write this blog post was to remind myself of the other invited talks I've given, to make sure the message I really think it's important is not getting lost in the middle of my own confused mind. That place is a jungle, everything gets lost in there.

I notice that in the curriculum vitae in my webpage from 2016, I kind of list the following invited talks:
  1. Weapons of Math Construction, LICS Logic Mentoring Workshop,  Iceland, 2017.
  2. Intuitionistic Modal Logic: a personal view, Stanford Logic Seminar, Stanford, CA, USA, 2016
  3. Modal Type Theory, Logical and Semantic Frameworks with Applications (LSFA) 2015, Natal, Brazil.
  4. Lean Logic for Lean Times: Varieties of Natural Logic, Conference on Computing Natural Reasoning (CoCoNat), Bloomington, Indiana, US, 2015
  5. Lean Logic for Lean times: Entailment and Contradiction (ECD) Revisited, 4th CSLI Workshop on Logic, Rationality & Intelligent Interaction, Stanford, CA, US.
  6. Intuitionistic Modal Logic: 15 years later, Berkeley Logic ColloquiumBerkeley, CA, USA, 2015.
  7. Edwardian Proofs for Futuristic Programs and Personal Assistants,  Plenary Talk, North American Annual Meeting of the Association for Symbolic Logic, Boulder, CO, USA, 2014.
  8. Dialectica categories’ surprising application – mapping cardinal invariants, XV Latin American Symposium on Mathematical Logic (SLALM 2012), Bogotá, Colômbia, 2012
  9. Edwardian Proofs for Futuristic Programs, Invited Plenary Talk at Infinite Possibilities Conference, IPC2012, Baltimore, Maryland, 2012.
  10. A Bridge not too far, SRI AI Seminar, Menlo Park, CA, 2010. 
  11. Fibrational Versions of Dialectica Categories.Talk at Stanford Logic Seminar, 2010
  12. CLiCS: Categorical Logic in Computer Science, Talk at  M*A*T*H Colloquium, Sonoma State University, 2009.
  13. Adventures in SearchLand, PARC Forum, Palo Alto, CA, 2009
  14. Constructive Hybrid Logics and Contexts, Hybrid Logic, Seattle, WA, 2006.
  15. Dialectica Categories: a survey Logic Lunch Stanford, 1999.
  16. Explicit Linear Substitutions,  WoLLIC Sao Paulo, Brazil,  1998. 

Some are more prestigious than others.
I am very proud of having spoken at Infinity Possibilities and the two ASL meetings (Boulder and Bogota). and also especially of the Berkeley Logic Colloquium, where I wanted to ask autographs of the guys in the audience: William Craig, Dana Scott, Paolo Mancuso, John Steel,...
But the hardest was definitely talking about Dialectica categories to Sol Feferman and Grisha Mints when I first arrived in the Bay Area. I miss them!

Friday, August 3, 2018

Old Technical Reports

Nice to find this page from the Computer Lab in Cambridge with my old technical reports, neatly listed, with dates and sizes. This is very helpful, since I was trying to find the original version of the work on Logical Dependencies in Linear Logic, with Torben Brauner.

My Amazon Author page also looks nice, I think.
The only bad thing is the price of the book for Prawitz.
And the stuff not done, yet.
But my page of publications while at PARC disappeared completely. Even from the Wayback Machine, sniff, sniff.

Just as well that Susie Mulhern, a friend that still works for PARC Communications, I think, was able to produce the picture below. I need to do something about it.






Moon over Mongolia and Lexical Resources?

Yep, one has nothing to do with the other. It's just a very pretty picture. I love the fact that the person who took it decided to tell us it's Mongolia. I want to visit China and maybe Mongolia too. Soon. But this post is about Lexical Resources for Portuguese.

It is an awful lot of work to deal with linguistic data. (ok, it can a bit easier than doing mathematics, as everything you do, gets you more data, so it's worth doing it...unlike maths when sometimes it really does not work. ) But we do it! And at least you can look back and see, not only the huge number of things you still want to do, but the fairly large number of works you have already done.

This was the spirit of the note "OWN-PT: Taking Stock", which we submitted to NLCS 2018. Alexandre Rademaker gave the talk and had his own slides, which I hope are already the FLoC site. But I produced mine first, so while we think what to do next and how, here they are.

Friday, July 27, 2018

Oxford and FLoC


I admit it: I bit more than I could chew, when I decided to organize three workshops, on different subjects, as part of FLoC2018 (the Federated Logic Conference) in Oxford this July. Sure, I did not know they would be all scheduled for the same weekend. I assumed they wouldn't, but still everything worked fine, mostly.

The picture above is from the dining hall of Wadham College, right after the Workshop Women in Logic 2018. We had a very good workshop and a spirited discussion, "Priorities for Diversity in Logic for Computer Science". Not absolutely clear how we will implement our ideas, but we're working on it.

Then we had Natural Language in Computer Science NLCS2018.  This is the 5th NLCS that  Larry Moss and myself organized, this time we had Ash Asudeh helping us out and the meeting was great! The program is available from FLoC here. Unfortunately I forgot to take pictures during the talks, a real shame! I thought  I had some pictures of the dinner  after NLCS2018 but I cannot found them now...

 Oxford is of course super photogenic... it is difficult to choose which pictures to post.










Finally,  I also also invited by Maribel Fernández, Thomas Ehrhard and Lorenzo Tortora de Falco to help organize the Linearity/TLLA workshop.

The talks were super interesting, but I could not attend. I had several `spies' there, though.  Harley Eades III and Jiaming Jiang, talked about the "Lambek Calculus with an Exchange Modality". Elaine Pimentel   talked about our joint work with Carlos Olarte and Giselle Reis on "Benchmarking Linear Logic Translation". This to the right is a chapel, that is, apparently a library, "where you can work", someone said...

Many intense and productive discussions were had. It was very nice to see good friends that I had not seen for many years.

But there was a big knot on our collective throat: we missed Mike Gordon a lot. As Sara put it, he brought us together once again.




Wednesday, July 25, 2018

Party in New Orleans

NAACL and *SEM happened in New Orleans this year.  Since the husband wanted to go, and had two papers on the program with Katerina, I decided to tag along and we all had a great time! Livy submitted a poster of our work on SICK-BR and the party was really fun! Danced so much, the calves were complaining the next day...yay!!

But the conference was also serious business, lots to learn, lots to take in.
Had extreme interesting serious conversations with Reuben Cohen-Gordon, Chris Potts, Ido Dagan and Ben van Durme, amongst others. Now the challenge is to transform all those clever conversations into serious, coded up and latexed work. oh boy, there's lots to do...

Thursday, June 21, 2018

Fjords and Semantics

 

Meaningful Work: Advancing Computational Semantics  is the  Centre for Advanced Study of the Norwegian Academy of Science and Letters'  write up on the meeting Dick and I went to, at the end of May, near Oslo, Norway. The program of the meeting is in SynSem/MeaningRepresentation - Deep Linguistic Processing with HPSG (DELPH-IN).

The meeting was super fun and we spent many hours talking about issues that we care about. Many thanks to Cleo Condoravdi and Stephan Oepen for the invitation!

Saturday, May 19, 2018

Coming up for Air

Once again, I bit more than I could chew. I thought I could organize, or help organize, three workshops as part of FLoC 2018 (Women in Logic, Natural Language in Computer Science and Linearity/LTTA) and I have spent the last six weeks, drowning in overdue papers, overdue reviews, overdue comments, overdue any kind of stuff. So much so that I haven't be able to even sit in the garden or watch stupid television for a while. What's the point of living in sunny California if you can't even sit in the garden, one may ask...

But today I think things might be getting better, touch wood. Still lots of to-dos undone, but  papers have been chosen, workshops are going ahead, they have preliminary programs, authors have been told. There might be a lull on the incessant pounding of "being late". So maybe one can sit on the garden, with a lemonade and try to think through the rest of what needs doing. After all the point of being a researcher is presumably researching stuff that you find interesting, not doing bureaucratic stuff non-stop. Maybe I can ponder one or two or ten conversations that were left hanging in the middle. One or two urgent emails that are now so old  that it will be surprising if they still matter. Worth a go, anyways.

Friday, May 4, 2018

Surely you're joking, Mr Martin-Löf?...

Many, many years ago, when I was a young postdoc I gave a talk in Uppsala about Dialectica categories and Full Intuitionistic Linear Logic. I was pretty pleased with how the mathematics of my thesis had panned out and when question time came and I had a question from a distinguished Swedish professor, I thought I was on safe grounds. He asked "ok, this is all very well, the categorical constructions are nice, I can see why you might want to consider a more intuitionisitic version of a multiplicative disjunction, but...what does it all mean? How do you tell a man in the street what you do?" And yes, the distinguished professor whom I had not met till then, was prof Per Martin-Löf (second from the right in the picture above) and it took me several years to get at least preliminary answers to his (very reasonable we all agree) questions.

Now the question is in Twitter, pestering me again, and I still do not have a proper answer. But I have a suggestion, given to me by Luiz Carlos Pereira, a good friend and collaborator. (It took me more than 3 hours ransacking my old notebooks to find it, so I feel that I should write it down, as well as I can, in this week of drowning-by-reviews...)

Now, everyone knows and some of us do enjoy shopping. The earlier Linear Logic examples were all about Camels and Malborough packets. Some people decided to change them to chocolate and coffee, but the vending machines stayed. Now in this era of Amazon and Walmart, let us describe a "FashionMall Semantics". (In Rio, "fashion mall" is not a common noun compound, but a proper noun. It's a sophisticated shopping center in one of the most unequal, on your face, terrible, parts of town, where the `favela'  and the uber-consumption face each other, in threatening ways. still...)
Anyways the FashionMall in Sao Conrado has all kinds of stores you might want to buy nice things from. So if the mall issued tickets for shopping, you could think of these tickets as ways of satisfying consumers' orders:

  •  If the mall gave you a ticket marked A\otimes B, then the mall has to have both A and B in stock and when you use your ticket, you  take both A and B  home.
  • If the mall gave you a ticket marked A&B, their stock has to have both, but you, the customer, can only take one of them home. You can choose which one A or B  you take home.
  • If the mall gave you a ticket marked A\oplus B, the stock only has to have one of A or B and the seller will choose which one it will give you. 

So far so good and similar to other explanations of Linear Logic using commercial transactions. But what can we say about A\par B?  Well, if the mall gives you a ticket marked A\par B they must have both in their stock,  you, the customer can only take one home, but you can take it back to the mall and swap it for the other one, if you want to do it. (The par operator is commutative, in the way that linear implication is not...)You do have to keep one of the two (A or B), though.

So more interesting still, if the mall gave you a ticket marked A\lollipop B what can we say?  Then we have a complicated transaction: if the buying of the antecedent  A is satisfied, then the buying of the consequent B has to be satisfied, whatever these buyings may be.  (some might use  "higher-order rule" to describe this transaction, but this  is somewhat familiar from  BHK-style interpretations.) Following this line of reasoning, a transaction A\lollipop \bot could be a transaction that cannot be satisfied.

And the units of Linear Logic, what happens to them? Well some "buys" cannot be satisfied, because the mall does not have the required stock. Other buys cannot be satisfied independently of the stock, just relating to what the costumer and the seller want to do.

There is much more that we need to work out to make  sure these intuitive notions  agree with the mathematics of Full Intuitionistic Linear Logic, but I hope this is enough to start the conversation. (and it gives me the chance to post a picture of friends Per, Steve and Richard, as well as the late Vladimir Voevodsky whom I had never had the pleasure of meeting: he really seemed a nice guy.)