From Quirky Case to Representing Space: AnnieFest one year later...

AnnieFest was almost a year ago and I'm pleased to report that because Tracy H. King is such a powerhouse of organization all is well with the volume arising from it.

Listing here the talks, as PARC doesn't keep its pages going for very long...

• Danny Bobrow, PARC Host
• Joan Bresnan, Stanford University and CSLI
• Anette Frank, Heidelberg University
• Joan M. Maling, Brandeis University and U.S. National Science Foundation
• Geoffrey Nunberg, University of California at Berkeley
• Livia Polanyi, Microsoft Corporation
• Hans Uszkoreit, DFKI and Saarland University

5 October 2011
2:00-5:30pm
George E. Pake Auditorium, PARC, 3333 Coyote Hill Road, Palo Alto, California

description

This symposium is being held on the occasion of Annie Zaenen's retirement from PARC to honor her significant contributions to theoretical and computational linguistics over a long and distinguished career.
The symposium features speakers who have collaborated closely with Annie at different times and on different topics, representing the broad sweep of her theoretical and practical concerns. The talks and discussion will reflect on their collaborations with Annie and offer new perspectives on language issues of current interest.
Speakers:
Joan Maling, Brandeis University and U.S. National Science Foundation
Chapter 1. Iceland: Is Icelandic a natural language
Joan Bresnan, Stanford University and CSLI
The evolution of syntax in the time of Annie
Hans Uszkoreit, DFKI and Saarland University
NLP is OOG?
Anette Frank, Heidelberg University
Diving into semantics -- and getting hidden meanings out
Livia Polanyi, Microsoft Corporation
Sentiment Analysis and the linguistic structure of Discourse
Geoffrey Nunberg, University of California at Berkeley
L'avis des mots
Organizers:
Danny Bobrow, PARC
Ron Kaplan, Microsoft
Tracy King, eBay
Valeria de Paiva, Rearden Commerce
Sponsored by PARC.

Constructive modal logics? in the plural?

(picture by Eric Volpe, check his flickr stream)

A long time ago I started compiling a bibliography of work on constructive modal logics. Now I've decided to make it a Google Docs so that people can help me improve it,  adding and correcting things.

Online bibliographies seem to me  a sensible idea.

Where's the meeting that was cancelled?

When I was still at PARC -- 2008 seems an awful long time ago now -- I invited Patricia Amaral, then a recently graduated research student to come and visit us for a short while. She was applying to be a research assistant in Linguistics, Stanford and being in Palo Alto a little earlier was a good idea. It was lucky that the Gulbekian Foundation agreed too. We wanted to work on improving the system Bridge (about which I will write informally some other day, but an official description can be found in PARC's Bridge and Question Answering System and a personal preliminary take can be found here).

Being a latecomer to computational linguistics and perhaps a bit too optimistic about research, I always have dozens of ideas of things I want to get done, but little ability to predict the time that it takes to get those things done. In this case, however, everything worked well. Patricia got the hang of the system very quickly and soon enough made gigantic progress on the issue I wanted to deal with.

Despite our claims in Preventing Existence (and despite the beautiful algorithm that Rowan, Cleo and Lauri described in Computing Relative Polarity for Textual Inference) the Bridge system could, at that stage, only deal with logical contexts introduced by verbs with a full complement phrase. So something like Ed knew that Mary arrived  would be fine, a logical context would be created with the right polarity, but Ed knew of Mary's arrival  would not create a logical context. (The Bridge system works with full deep LFG parses of sentences and it easier to mark the complemented verbs.)

Thus my goal for the work with Patricia was the extension of the marking of verbs that introduce context, from the ones with full complement to ones that were simply directly transitive.  As usual the problem was much harder than I expected and Patricia, at the end of her stay, gave us a huge presentation with millions of issues and a possible classification that would be a first stab at solving the original problem.

This was written up in a paper  (by Patricia, myself, Cleo Condoravdi and Annie Zaenen) submitted to the workshop on contexts associated with ECAI2008. The paper accepted, but none of us could attend. So we withdraw the paper, hoping to improve it.

Very recently I took the initiative of re-submitting the paper to ONTOBRAS2012 in Recife, Brazil, as I had hoped to go visit some  friends there. But this was not possible, so the paper, again accepted,  had to be withdrawn. Again.

The newly named Where's the meeting that was cancelled? paper seems a bit unlucky, but the work is very cool. Patricia came up with this idea of treating verbs that change  existential commitments as pre and post conditions reminiscent of Hoare's logic. This connection is hinted at in the paper, but not pursued, as the need for classification large-scale was definitely more important then. Someone should work on this, though.

(Meanwhile together with Lottie Price and Tracy King, I worked a little on nouns that introduce logical contexts, cf. Contexts Inducing Nouns.)

Why Constructive Modal Logics?

I guess the question can be taken as both why constructive?, if we like modal logics, but also as why modal?, if we favor constructive logic. (some might even ask why logic at all?, but we won't go there...)

I will try to outline my answers to both forms of the question.

To my functional programming friends, the answer to why modal? goes via extending the  Curry-Howard paradigm to deal with effects, exceptions, I/O and other non-pure features of real-life computations. Despite all the excellent work in this area in the last thirty years or so, the models and tools we have still seem to work best for sequential, effect-free functional programming. The hope is that extending the Curry-Howard to more modal systems will allow us to deal with more of the computing we already do, but are not able to model accurately.

To my modal logicians friends, the answer to why constructive? goes via pointing out the affordances of Curry-Howard as well as the niceties of having an amenable proof-theory with explicit computational content.

 I still believe what we wrote in the preface of the special issue devoted to IMLA in 2004, viz.   `Proofs carry concrete intensional information over and above the fact that a formula is valid. From this point of view modalities come in naturally, viz.\ as syntactic reflections of this underlying intensional level hidden in the proof theory of a constructive logic. A constructive modal logic might arise in an attempt to handle the intensional dimension, or parameter, of modalities (time, nondeterminism, security margin, knowledge, beliefs, etc.) in a computational way at the level of the proof theory. It seems obvious that such a program has much to offer not only from a computer science perspective.'

However I will freely admit that putting together constructivity and intensionality in the guise of constructive modal logics is not an easy task, as there are many design decisions to take and these do not seem clear cut to me. Even the definitions of systems are up for grabs, so there is very little known about semantics and/or complexity results, for instance. Worse still I cannot point out at huge successes in the form of logically-based systems being used in real applications. The best I seem to be able to do is point out at (many though!) systems that use ideas from the Curry-Howard correspondence...

Intuitionistic Modal Logics and Applications (IMLA2013)

For a fair number of years now I have been working on modalities in constructive logics and type theories. This started with the  realization that the Linear Logic "of course" exponential connective corresponds to an S4-box operator (1992), which became my paper with Gavin Bierman On an Intuitionistic Modal Logic, Studia Logica (65):383-416, 2000.

And it has continued ever since in an informal project with many collaborators including Nick Benton, Torben Brauner, Gianluigi Bellin, Eike Ritter, Michael Mendler, Rajeev Gore, Natasha Alechina, Neil Ghani, Milly Maietti, etc.  The main outcome of this project has been the organization of Intuitionistic Modal Logic and Applications (IMLA) workshops and the journal special issues that came from them.

So far there have been 5 such workshops. Now the 6th Workshop on Intuitionistic Modal Logic and Applications (IMLA2013) will be held in association with Unilog2013,  in March-April, 2013 in Rio de Janeiro, Brazil.

Previous workshops were part of FLoC1999, Trento, Italy, of FLoC2002, Copenhagen, Denmark, part of LiCS2005, Chicago, USA, part of LiCS2008, Pittsburgh, USA and part of the 14th Congress of Logic, Methdology and Philosophy of Science, Nancy, France, 25 July, 2011.

I wasn't much associated with the first workshop in Trento, but have been involved in all the others. Three special issues of journals have been published from IMLA workshops so far (a fourth is being produced, editors Natasha Alechina and me):

1. M. Fairtlough, M. Mendler, E. Moggi (eds.): Modalities in Type Theory. Mathematical Structures in Computer Science, Vol. 11, No. 4, August 2001.
2. V. De Paiva, R. Gore, M. Mendler (eds.): Modalities in Constructive Modal Logics and Type Theories. Special issue of the Journal Logic and Computation, editorial pp. 439-446, Vol. 14, No. 4, Oxford University Press, August 2004.
3. Valeria de Paiva, Brigitte Pientka (eds.): Intuitionistic Modal Logic and Applications (IMLA 2008). Inf. Comput. 209(12): 1435-1436 (2011).

Ideas to discuss with Elaine?

Elaine wanted to discuss some more mathematical ideas that she might (or not) want to talk to her students about. Sitting in the several planes that it took me to get home, I made a preliminary list of things that I wanted to talk to her about.

#1. Dialectica categories relationship to Milner's "tacticals", in Budiu et al's partial compilers paper. Also relationship to sub-exponentials, as Dialectica categories have three notions of modalities.
#2. Hopf (co)-algebras in Dialectica categories (Blute/Majid?).
#3. Prove (using TATU perhaps?) cut-elimination for FILL. I guess this is hard, given what she said about multiple-conclusion versions of IL.
#4. Proof-theoretical institutions. Why my work with Rabe et al  is not good enough. as far as I'm concerned, that is.