Ecumenical Negation at LC2021

 My friend Tim cannot hear me talking about Ecumenical Logic without thinking of Father Ted (below). For friends not from the UK, Father Ted was a very successful comedy series a long, long time ago. They had three seasons, the last one finished the year we came to California, 1998. Apparently, it became a cult series since then, every year they have a Ted Fest and several slogans from the series entered the common spoken language, as Wikipedia tells me. I thought it was funny, but the same kind of funny of Fawlty Towers which is so embarrassing that you have to laugh. I don't like this kind of stuff much, but yes, the family says that I lack a sense of humour altogether.

Anyways, the ecumenical in Ecumenical Logic has nothing to do with priests or religion, funny or non-funny. But it has to do with friends Elaine Pimentel and Luiz Carlos Pereira pictured above. Ecumenical logic is about accepting in the same framework logic systems that tend to be considered exclusive alternatives, like intuitionistic and classical logic. Actually, the label 'ecumenical' is supposed to generalize from this setting, but in reality, this is the case that counts. 

Thus the idea is that we want a system where classical and intuitionistic theorems can be proved and disproved in the respective cases, satisfying as many good proof-theoretical properties as we can have. The issue is of course *which* good properties can we have and how to optimize rules to get as many of these properties, with the most perspicuous rules.

Dag Prawitz approached this problem from a philosophical point of view in his article "Classical versus intuitionistic logic", in the book `Why is this a Proof?' a Festschrift for Luiz Carlos Pereira in 2015. Pereira and Rodriguez proved the normalization of the propositional fragment of Prawitz's system and  provided a possible-worlds semantics for it, proved sound and complete in Normalization, Soundness and Completeness for the Propositional Fragment of Prawitz’ Ecumenical System. Elaine, Luiz Carlos and I have provided sequent calculi for Prawitz's system, which  allows us  a deeper investigation of its proof theoretical properties in An ecumenical notion of entailment. Elaine and Luiz Carlos, together with Sonia Marin and Emerson Sales produced a version of the system extended with constructive Simpson-style modalities  in A pure view of ecumenical modalities.

Now recently we have been discussing the role of negation in the ecumenical system. Luiz Carlos just presented this really nice deck at the Logic Colloquium 2021 in Poland. Now we're working on the paper, which I hope will hit the arXiv soon.

(the cast of Father Ted)

AplicAi! Matching students and researchers

 

Sometimes, when walking in the park near my house, I think about big ideas, like AI for Good. It should be much easier to think about small kinds of good ideas, that actually help people, instead of being simply boring exercises for young programmers. But it isn't very easy to find small projects that are helpful to society, stretch and showcase a student's competence, and are also fun to deal with! yeah, I know I am asking for much, but really? It ought to be simple!

I have come up with a few ideas, but mostly things work the other way round. Students have their own ideas of what they want to do, we discuss issues -- sometimes quite a bit -- and sometimes things emerge that work nicely. One of these examples was Hugo Machado's app AplicAi! Hugo just finished his undergrad degree at  Dept of Informatica at PUC-Rio and this app was his end of course project and thesis.

Hugo came up with a very interesting idea. He noticed that students at PUC-Rio tend to be worried about not knowing enough about new technologies and about not being ready for the market when they finish their degrees. He thought these students might want to do "tasks" for employers, to add to their resumes some professional experience. Clearly this is a good deal for employers (e.g. start-up workers or researchers) who might get extremely clever and dedicated workers  for no money at all. Hugo wanted to create an app to match students and their competencies to employers and their proposed tasks.

This is an interesting AI task in itself, recommender systems are used everywhere, from big places like Netflix (who wants to serve you the best films for you) to small outlets who need to know where to spend their restricted sales budget. Because Hugo wanted to do a mobile app he actually could showcase his coding abilities with Flutter, BLOC, Flask and Firebase. And he could showcase his abilities with AI technologies like word embeddings, word2vec, word distance mover, etc. Together with Hugo's advisor, Prof Markus Endler, I worked on getting his recommender system as good as we could and showing (through evaluation) that his system worked as well as the ones we were  emulating.

Hugo was very lucky to be able to find cleaned up data of a reasonable size to bootstrap his recommender system: an employment agency had collected data about 50K job offers and respective developer profiles. We would have preferred data about a wider range of jobs and profiles, but the data about developers should be able to get us a baseline for many technical areas. 

This is a socially useful project, as the demand from PUC students for 'internships' is real. It is also extremely helpful to both small companies or researchers within the University, who can count on specific help for their projects, from the students with the requested competencies. Of course, a prototype for an undergraduate thesis can only do so much, but since the code is open (https://github.com/hugomachado93/aplicai) and based on open data, it can be re-used with newer NLP technology (perhaps BERT instead of word2vec), and hopefully more data (to extend it to other domains of skills besides software development).

Hugo's thesis was a fun project for all, I think. More importantly, it has many possible developments, so I hope the video  about it will appear soon. And I'm looking forward to the writing of our joint paper!

Main sources:

1. @article{DBLP:journals/corr/LeQA17,

  author    = {Van{-}Duyet Le and
               Vo Minh Quan and
               Dang Quang An},
  title     = {Skill2vec: Machine Learning Approaches for Determining the Relevant
               Skill from Job Description},
  journal   = {CoRR},
  volume    = {abs/1707.09751},
  year      = {2017},
  url       = {http://arxiv.org/abs/1707.09751},
  archivePrefix = {arXiv},
  eprint    = {1707.09751},
  timestamp = {Mon, 13 Aug 2018 16:47:57 +0200},
  biburl    = {https://dblp.org/rec/journals/corr/LeQA17.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

2. Simon Hughes. How We Data-Mine Related Tech Skills.
2015. URL: http : / / insights . dice . com /
2015/03/16/how-we-data-mine-related-tech-skills/ (visited on 09/12/2017)

Hypatia

 

 

In 1996 Edmund Robinson wrote to the Types mailing list the message below. I have found the message while looking for something else and it has been sitting in my blog posts drafts folder since Dec 2014. 

It is amazing how Hypatia was such  a clever idea, but it disappeared without trace!

 

You can read about Hypatia, the philosopher and mathematician, in Wikipedia, like I just did. Again. But I find most of the literature about famous women written by man tend to go on and on about how exaggerated the claims about their cleverness were. They say the same about Ada Lovelace, about Emmy Noether, about Marie Curie. oh well.

Dear Colleagues,

This is to tell you about the new electronic library, Hypatia,
which has been implemented by my colleagues at QMW.
(Apologies for duplicate copies of this message.)

     HH   HH                                   ii
     HH   HH                           tt
     HHHHHHH  yy  yy  p ppp    aaaa    tttt    ii   aaaa
     HH   HH  yy  yy  pp  pp  aa  aa   tt      ii  aa  aa
     HH   HH   yy yy  pp  pp  aa  aa   tt  tt  ii  aa  aa
     HH   HH     yy   ppppp    aaa aa   tttt   ii   aaa aa
                yy    pp
             yyyy     pp      http://hypatia.dcs.qmw.ac.uk

Hypatia is at Queen Mary and Westfield College in London's East End.

Hypatia is a directory of research workers in computer science and
mathematics, and a library of their papers. It contains material which
has been published by placing it on a publicly accessible web or ftp
site, and a certain amount of "public domain" information about
authors (name, affiliation, email address and phone number, etc).
It also assembles bibliographic information.

Hypatia is not a web crawler, but a mirrored archive with a web
interface.  The archive is indexed by author and by research group,
and is equipped with a search engine.

Hypatia works by having a database of registered authors. Many of the
readers of this message will already be on the database. You can find
out if you are on our database simply by searching for yourself in
Hypatia. If you are not, then you can register and ensure that your
papers are lodged in Hypatia simply by filling in an electronic form,
which you can obtain via the Hypatia home page. If you are already
registered, then you can use the same form to correct any incorrect or
out of date information we have about you. (Inevitably, and despite
our best efforts, not all the information on Hypatia's database will
be correct.)

You can use the same form on behalf of your colleagues to help expand
Hypatia's coverage.

Hypatia would also like to encourage you to compile a BibTeX-format
database of your own papers. We hope that this will help people to
cite accurately the definitive versions of your work. On-line help for
this is available.

Hypatia has been implemented by Mark Dawson, who set up and ran the
popular mirrored archive at theory,doc.ic.ac.uk.  Mark has benefited
from discussions with Paul Taylor.

Hypatia is still under development and welcomes your comments,
suggestions, requests for help, and corrections to
<hypatia@dcs.qmw.ac.uk>.

Edmund Robinson,
Department of Computer Science,
Queen Mary and Westfield College,
University of London,
London E1 4NS

Kolmogorov-Veloso Problems

 This paper (now in the arXiv)  Kolgomorov-Veloso Problems and Dialectica Categories was written last year for a book for Paulo Augusto Veloso, a friend, teacher and colleague at the Dept of Informatica, PUC-RJ in the 80s. The book appeared this year, A Question is More Illuminating than an Answer. A Festschrift for Paulo A. S. Veloso – February 15, 2021, edited by E. Hermann Haeusler, Luiz Carlos Pereira, and J. Petrucio Viana. 

 Samuel Gomes da Silva and I have been working for several years now on applications of the Dialectica construction to Set Theory (which is Samuel's speciality) and hearing Wagner Sanz talk about Veloso's Theory of Problems, we realized that Kolmogorov's problems were another case of the Dialectica construction. The examples from undergraduate/graduate mathematics that Samuel described to explain the connection are just beautiful!

Both Kolmogorov and Veloso had extremely general theories of problems that get much more concrete when we introduce the morphisms of category theory. I have given two talks about this work, one in the meeting called Finding the Right Abstractions and one more recently in the Logic Colloquium, organized in Poland.

Dialectica Petri Nets

 

This beautiful poster presented by Elena at the ACT poster session is a great summary of the work that went into the arXiv preprint of ours Dialectica Petri Nets  (Elena di Lavore, Wilmer Leal, Valeria de Paiva). But a 2 min presentation, even if impeccably given, like Elena did it at the Applied Category Theory Conference, does not do justice to the work.

This work started  for the ACT Summer School last year. Summer Schools can be fraught with difficulties, as people do not know what to expect from them. I had decided to play it safe and to have a few meetings before the official start of the School, so Jade Master, Elena di Lavore, Xiaoyan Li  and I met a few times to talk about the readings. I had a great time with these meetings and only realized later on that two other members of the team (Wilmer Leal and Eigil Rischel) were missing!

The School itself was complicated by COVID-19 and the first "Shelter in place" or "LockDown" or whatever you want to call it. Also because the School had a team in Australia the logistics were more complicated, as covering West Coast, Europe and Australia is complicated. Both West Coast and Europe and West Coast and Australia are ok, but the three together does not seem to work very well. Someone has to suffer in the middle of the night.

Elena Di Lavore and Xiaoyan Li wrote their piece Linear Logic Flavoured Composition of Petri Nets as a guest post for The n-Category Café and some good  discussion happened. I must confess that this work went into a different direction than the one I had envisaged. Which is great, this is why we have collaborations. But I had imagined that we would do much work connecting this LL-based version of Petri nets to other categories of Petri nets, trying to suss out advantages and disadvantages of different categorical models. Instead the group seemed much more interested in discussing different kinds of connections or edges in a given Petri Net (namely probabilistic edges, multiple-valued logic edges, multiplicity enhanced edges, etc..) and how we could put these kinds of links together. This was caused by the disposition of actually using these nets in Chemistry and Bioinformatics and these proposed applications are extremely cool!