Existential Change Verbs?

If you find a sentence like "Our reservations were cancelled by the hotel computing system" you need to know that, whether you name them or not, whether you're using bag-of-words or not, someone's reservations do not exist anymore in that hotel.

Patricia Amaral, Cleo Condoravdi, Annie Zaenen and I worked a little on the problem of classifying verbs that exhibit this "existential change" effect. We submitted a paper to a context workshop in 2008, it was accepted, but no one had time to travel for that conference. Now we submitted it again to ONTOBRAS-MOST 2012 in Recife.

OpenWN-PT is online!!

Together with Alexandre Rademaker and Gerard de Melo I have been working on a version of WordNet for Portuguese that is open, downloadable and modifiable by all. The paper was called "Revisiting a Brazilian WordNet" and it appeared in the Proceedings of Global Wordnet Conference.

We call it OpenWN-PT because there are some other efforts at Portuguese WordNets, including the MultiWordNet-Portuguese, the Portuguese Wordnet of P. Marrafa and the Brazilian Portuguese WordNet of Bento Dias-da-Silva. Ours is small, but downloadable and improvable.

This week we heard from Francis Bond that this has been incorporated into Francis' project,  Open Multilingual Wordnet (link below) which makes it online, searchable and "linked" to SUMO, which I worked on with  Adam Pease.

YAY!!! Great news guys, many thanks!!!

Open Multilingual Wordnet

 

Language and Natural Reasoning

Annie has created a new group in CSLI, Language and Natural Reasoning.

I guess I need to justify my participation, so I need to write up my RAIN (Reasoning and Interaction as NASSLLI) talk: Little engines of Inference: Contexts for Quantification.

Women in Logic? Yes!

Catarina Dutilh Novaes had the clever  idea of making a list of women working in logic.

But the list was not alphabetical (which made it difficult to know if you were in there) and it had no webpages for the women there (which made it difficult to read their work).

So I've asked Anna Crouch to find out the webpages for the women in the list and to make it  alphabetical. 

Ruth Barcan Marcus in 1943 and a "year of zipping and unzipping snowsuits" to illustrate.

Fuzzy Sets in Brazil

Apostolos Syropoulos and I have managed to submit a paper  on (Dialectica-style) Fuzzy Topological Systems for the

II CBSF - Second Brazilian Congress on Fuzzy Systems

 

Thanks Elaine Pimentel for the photo of Natal!

Computing in Tunisia?

 Prof. Fairouz Kamareddine (Heriot-Watt University, Edinburgh, UK) invited me to the program committee of this new conference in Tunisia,

International Symposium on Symbolic Computation in Software Science,
December 15-17 2012
Gammarth, Tunisia

I sure would like to go to Tunisia.

IMPORTANTS DATES:
August 23, 2012: Paper title and abstract deadline
August 30, 2012: Full paper deadline (firm)
October 30, 2012: Author notification
November 30, 2012: Final version deadline (firm)
December 15-17, 2012: Symposium

Lambek Calculus and Dialectica Categories

Many years ago I wrote a short note on a categorical model of the Lambek Calculus using the Dialectica construction. The note is imaginatively called A Dialectica Model of the Lambek Calculus.

This is interesting for a couple of reasons. First because the original dialectica constructions are all commutative and the Lambek calculus is definitely not commutative.
Second because the route I took to start from the Lambek calculus and end up in classical propositional logic, I have not seen taken since. It was based on previous work of Yetter and independently Morrill-Hepple-Moortgat and it's surprising to me that others have not decided to use it.

 I talked about it at both the Durham Symposium and the Amsterdam Colloquium. But with job moves, house moves,  broken computers and passwords-that-don't-work, I had not a single copy of my own paper. So I wrote to the nice guys in Amsterdam and thanks to wonderful Peter van Ormondt, Paul Dekker, Maria Aloni and Johan van Benthem I now have at least a scanned copy of  Peter's volume. Thank you guys!

So if like me, you want to read it, you can check it out at the place provided by the also nice guys  at Slideshare. Google Docs doesn't allow you to upload a 3.5MB scanned file, but Slideshare does. On the other hand, I did have a postscript/pdf  draft version that might be easier to read.

Kinds of Categorical Fuzzy Sets

In the logic seminar in Stanford sometimes people are asked to present papers. That's how I ended up reading Takeuti and Titani on fuzzy sets, which turned to be very interesting.

Now I'm reading Gottwald on "Universes of Fuzzy Sets and Axiomatizations of Fuzzy Set Theory. Part II: Category Theoretic Approaches" and this is very interesting too, for the same reason.

I have known since around  1990 that I can construct a "fuzzy" version of dialectica categories.  I know that this construction gives us a symmetric monoidal closed category with products and coproducts, with a (admittedly complicated) linear exponential comonad, hence is a model of Linear Logic. I know that there are other fuzzy sets that are also models of Linear Logic. Presumably I can relate these models via functors.

 I have not managed, so far,   to discover what makes fuzzy logic such a "crowd-puller", such a strong favorite. so I have no idea if this attractiveness will hold for the linear logic models. Or not.

Reading about Univalent Foundations

Voevodsky’s proposal to the NSF and IAS(2010) consists of 13 pages. The slides from his talk in Goteborg (Sept 2011) are easier to understand. Both can be found  in the univalent foundations page.

There is also the page on Homotopy Type Theory tout court, with more information on other researchers' views. 

Homotopy Type Theory refers to a new interpretation of Martin-Löf’s system of intensional, constructive type theory into abstract homotopy theory.  Propositional equality is interpreted as homotopy and type isomorphism as homotopy equivalence. Logical constructions in type theory then correspond to homotopy-invariant constructions on spaces, while theorems and even proofs in the logical system inherit a homotopical meaning. Slides from Thierry Coquand following this kind of explanation in Oberwolfach are  linked from here.

The original work that is the basis of this stuff is the groupoid model of Martin-Loeuf's CTT by Thomas Streicher and Martin Hofmann, here.

The broad motivation behind univalent foundations is a desire to have a system in which mathematics can be formalised in a manner which is as natural as possible. Whilst it is possible to encode all of mathematics into Zermelo-Fraenkel set theory, the manner in which this is done is frequently ugly; worse, when one does so, there remain many statements of ZF which are mathematically meaningless. This problem becomes particularly pressing in attempting a computer formalisation of mathematics; in the standard foundations, to write down in full even the most basic definitions—of isomorphism between sets, or of group structure on a set—requires many pages of symbols.

Univalent foundations seeks to improve on this situation by providing a system, based on Martin-Loef’s dependent type theory, whose syntax is tightly wedded to the intended semantical interpretation in the world of everyday mathematics. In particular, it allows the direct formalisation
of the world of homotopy types; indeed, these are the basic entities dealt with.

Constructing a model of the univalent foundations in the category of simplicial sets Voevodsky shows the consistency of these foundations relative to the usual ones. But this is just a first sanity check, if the new foundations are to be used, what do we need to know about them?

Some highlights of the Voevodsky proposal (first pages only).

1. We're close to "a new era which will be characterized by the widespread use of automated tools for proof construction and verification". yeah.
2. V came up with "a new semantics for dependent type theories - the class of formal systems which are widely used in the theory of programming languages"    Cool about the new semantics. I wish the bit about 'widely used' was true.
3.  "univalent semantics" interprets types as homotopy types. "the key property of the univalent interpretation is that it satisfies the univalence axiom a new axiom which makes it possible to automatically transport constructions and proofs between types which are connected by appropriately defined weak equivalences."    ok, need definitions...
4.  The key features of  "univalent foundations":

•  axiomatization of n-categorical structure
•  language is dependent type theory
•  based on homotopy types, not sets
•  both constructive and non-constructive maths

Univalent Foundations? Go Voevodsky!

 I should be an awful lot better at explaining hard stuff than I am.  This is because before starting mathematics I had one year of journalism and half a year of law in college. Long story, don't ask.(oddly enough, this hasn't helped me much.)

But since I am not good at explanations and I would like to improve, I've decided to write down (over)simplified versions of ideas to see if "practice makes perfect". I've decided to start with Vladimir Voevodsky's programme on Univalent Foundations for Mathematics.

There is a couple of reasons for that. First it's one of the more interest-generating new ideas in Category Theory. Some of it it's just because Voevodsky is a Fields medallist and all that. Some is because category theorists have a "chip on their shoulder" as far as other branches of mathematics are concerned. Despite claims in Wikipedia (of all places) that  abstract nonsense is a term of endearment, true category theorists know that it's not. It's an insult where more established branches of mathematics want to say that what we do is just dress up old concepts in new language. But thirdly and far more importantly the reason for trying to explain (to myself) what Univalent Foundations is about is that fact that this is the first serious attempt to extract new mathematics from the Curry-Howard isomorphism.

Why does this matter, do you ask? Well, the Curry-Howard iso is something that I've been trying to explain (to myself and others) for the last twenty years and I still haven't got a good way of doing it. So I wanted to use this non-serious medium (I cannot be corrupting the youth or damaging anyone else's reputation in a blog post) to try out a few off the wall ideas.

One of the things that makes explaining other people's work hard is that your own work and ideas keep trying to introduce themselves into the explanation. One has to fight to keep them off. The case of univalent foundations is slightly easier for me, as my own work is very marginally related to them. 

More on why Infinite Possibilities was so cool..

The Infinite Possibilities Conference (IPC) is a national conference that is designed to promote, educate, encourage and support minority women interested in mathematics and statistics.

The conference is important because African-American, Hispanic/Latina, and American Indian women have been historically underrepresented in mathematics. In 2002, less than 1% of the doctoral degrees in the mathematical sciences were awarded to American women from underrepresented minority groups. Even professionals who have succeeded in completing advanced degree programs in science and engineering fields can face inequities within their professional lives with respect to advancement and salaries. 

 In 2012 IPC was called "Building Diversity in Science and Mathematics", it happened 30-31st March at the University of Maryland, Baltimore County, Baltimore, MD and I had the honor of being one of the two keynote speakers. Many of the mathematicians I met there seemed to be working with mathematical Biology,  I was the only speaker talking from a Computer Science,  programming languages perspective.

My talk was entitled ``Edwardian Proofs for Futuristic Programs" and besides the required description of my career path so far,  talked about the birth of Mathematical Logic in the early years on the 20th century and how Proof Theory, one of the main strands of Mathematical Logic got a big impulse via the advent of Computing for all, through the (still today!) poorly recognized Curry-Howard Isomorphism and its more mathematical incarnations. 

This is a difficult talk to give, even for people interested in Computer Science, let alone for a generic mathematical audience. So I reckon I need to keep working on making it more accessible. It's a tall order, as Category Theory seems to scare people off, even mathematicians. The slides are available here, if you want to have a look.

Paraty 2012

I've been invited to give a talk at
Proof Theory: Linear Logic, Ludics and Geometry of Interaction. 

yay!!!

The link is here, but I don't think there's much information there, yet.

Intuitionistic Modal Logic and Applications 2011 Nancy, France

Natasha Alechina and I organized this meeting on

Intuitionistic Modal Logics and Applications Workshop (IMLA'11)

as part of the 14th Congress of Logic, Methdology and Philosophy of Science in Nancy, France, 25 July 2011.

The webpage is in the Agents Lab in the University of Nottingham and the call for papers for the publication after the meeting is here.

 

Party at NASSLLI?

GetFUN good news

So I have been helping to write a twinning logic research project between Brazil and Europe, in the shape of Portugal, Italy, Romania and Israel(!?...).

Just heard that it has been accepted, yay!
Great job Carlos Caleiro and Joao Marcos!

A week of intense work...

Bit of good news, Cristina Sernadas invited me to the editorial board of Cadernos de Lógica e Computação College Publications.