Saturday, March 12, 2016

Late with Women's International Day 2016

Someone I don't know personally yet (Evangelia Antonakos)
posted this in the Facebook group Women in Logic
List of women in mathematics - Wikipedia, the free encyclopedia
and guess what? I am there!!!

As Grouch Marx would've said things are really wrong if I'm invited to this party. Still a party is a party, might as well enjoy it.

Thank you Evangelia, this was a super present!

Monday, February 22, 2016

Bridges and all that

I talked  on October 26th 2012 in the Nuance NLU Seminar organized by Mark Fanty,
(NLP Research: Bridges from Language to Logic)
about my work on Natural Language-based Knowledge Representations at PARC and how I wanted to improve it.

I first gave a talk similar to this in Feb 2010 at SRI (slides in slideshare).

Then I tried to think a bit more along the lines of expressivity vs. complexity, following the work of Larry Moss and others. First at Stanford Workshop on Natural Logic, Proof Theory, and Computational Semantics, March 2011 and  then at RAIN in Austin, Texas, June 2011, when I called it Little Engines of Inference.

Now this work is stopped for lack of computational power. I need to decide how to continue it, but am drawing a blank right now.

(picture of Via Lactea in the Appalachian mountains by Lam, CUNY 2015 photo contest)

Sunday, February 21, 2016

Gentle with Gentilics

(photo of Yosemite Firefall by Sangeeta Dey via National Geographic)

Yesterday Livy submitted a joint paper on gentilics on the OpenWordNet-PT. This is good, as she reminded me, this work has been kicking around for quite a while.

This also reminds me that the work on NomLex-PT needs tidying up. Will write more about it later on. There is a paper in e.g. here.

Sunday, February 14, 2016

Bauer and Banach-Tarski

Dan Piponi had a short and thought-provoking post in G+ the other day. To me the best bit was
"Conversations between people who view mathematics as being about beliefs, and people who view mathematics as being about practices, can often be at cross purposes.
I think I am firmly on the side of the ones who think that it's about practices, not beliefs. One thing that surprises me about Philosophy and philosophical questions is the notion of cross-purposed-ness, how one can be interested in a subject, yet, totally not engage with certain questions and manners of approaching it.

The whole Piponi's post is below. In response to an ensuing discussion with Rodrigo Freire on  whether intuitionistic practices of Mathematics are self-contradictory, given that the majority of the mathematicians do believe in Excluded Middle and Choice, Victor Botelho posted the link to the following video from Andrej Bauer talking in Princeton in 2013.

Five Stages of Accepting Constructive Mathematics

I loved it!! If you haven't seen it yet, do yourself a favour and have a look. It touches on lots of the questions that aren't at cross-purposes for me. Says some things I'd say too, but it has much more than I know, so I learned lots, and hope to follow up with some more learning on the subject of constructive mathematics. Including some on what to do with Banach-Tarski and the constructive "theorem" that every function is continuous. 

Philosophy is hard, I don't want to venture there much, but it would be nice to get enough od a feeling for the place, to avoid it.

Dan Piponi on Beliefs vs Practices in Mathematics
Many people think of religions primarily as systems of belief. I think this may be a skewed view because of the predominance of Christianity and Islam, both of which make creeds prominent. For example, although Judaism does have something like a creed, it tends to place more emphasis on practice than belief.

This reflects my view of mathematics. I think that for many, mathematics is a matter of belief. For them, mathematics is a way to find out what is and isn't true. I tend to see mathematics as a set of practices. As a result, I find myself bemused by debates over whether 2 really exists, or whether infinite sets exist, whether the continuum really is an infinite collection of points, whether infinitesimals exist, whether the axiom of choice is true, and so on. I find some ultrafinitists particularly confusing. They seem to believe themselves to be expressing skepticism of some sort, whereas to me, expressing skepticism about mathematical constructions is a category error. So to me, these ultrafinitists are surprising because of what they believe, not because of what they don't. This doesn't just apply to ultrafinitists. In an essay by Boolos [1], he seems confident in the self-evident truth of the existence of integers, say, but expresses more and more doubt as he considers larger and larger cardinals. Many mathematicians seem to have a scale of believability, and ultrafinitists just draw the scale differently.

Conversations between people who view mathematics (or religion) as being about beliefs, and people who view mathematics (or religion) as being about practices, can often be at cross purposes. And members of one group can often find themselves dragged into debates that they don't care for because of the framing of questions. (I don't want to debate the existence infinite sets, not because I can't justify my beliefs, but because I'm more interested in how to use such sets. I don't think belief is a precondition for use.)

Of course you can't completely separate belief and practice and I certainly do have some mathematical beliefs. For example I put a certain amount of trust in mathematics in my daily job because I believe certain practices will allow me to achieve certain goals.

[1] Must we believe in Set Theory? (I hope I'm not mischaracterizing this essay, but even if I am, the point still stands.)

Friday, February 12, 2016

Billy Goats Gruff

In 2009 Ruy de Queiroz first asked his logician friends, me included, about Rolf Schock Prize nominations.

I think it's very nice that Ruy gets asked this kind of question. So I tried to help in 2009 with a tale of Bills.

I'd like to nominate Three Bills: William A. Howard, William W. Tait and F. William Lavwere. No, it's not a kid's story, even if the three Billy Goats Gruff come to mind. The reason I think this is a sensible nomination is that the three are involved in the project that came to be known as the Curry-Howard Correspondence. The Curry-Howard correspondence is one of the big forces behind the advancement of logic and philosophy as   engines of Computer Science in the last fifty years.

The Curry-Howard correspondence asserts that propositions in (certain systems of) logic correspond to types in (certain kinds of) programming languages, that proofs in those logics correspond to terms in the these programming languages and that simplification of proofs correspond to computation in the related  languages. As can be easily seen even in this oversimplified description, the correspondence has far-reaching consequences for both logic and programming. In particular it allows for results in either area to be exploit in the other--a hallmark of a deep result in Mathematics.

Howard is already, together with H. Curry named in the the correspondence, which wouldn't have the impact it has without the work of Tait and Lawvere. Tait is responsible to the part of the correspondence that relates proof simplification to computation, possibly the most important component of the correspondence. And Lawvere (together with Lambek and many other category theorists) is the one that made it all beautiful mathematics, by relating it to the Theory of Categories. Lawvere showed in his thesis (1968) that the correspondence could be  extended to (special classes of) categories and that, once again, results in pure category theory correspond to logical (and hence also programming) results, so that one can work in whichever field there are tools available and then transfer the results to the other fields. It's remarkable and very beautiful, albeit still hard to explain without the full mathematical apparatus.

Nonetheless given the Rolf's prize interest in making sure that society in general is aware of the importance of philosophy  and logic matters for humanity, and given the importance of computing and its understanding for society as a whole, the nomination of the three Bills seems to me a sensible option.

Wednesday, February 3, 2016

Feminism 2016

I have to learn a thing or two from the girls writing for Buzzfeed. 
First I loved this
Here's How To Have A Panel About Women At Davos

Check it out, it's hilarious!

Then there's tumblr with
Congrats, you have an all male panel!
(shame I cannot find the post from the (male) statistician which showed that these things do not happen by chance!)

Most recently I loved the great
If Male Scientists were written about like women

«He had the body of an athlete and the face of a movie star. But Oliver Sacks chose science over glamour.»


Monday, January 18, 2016

Our Grant Money of Every Day

I have a long history of getting grant money that I cannot use, because I have moved, or because the partner changed his/her mind, etc.

It started with the project "Authentication Logics", which I mostly wrote for co-P.I's Larry Paulson and Roger M. Needham in 1995. Larry had been my sponsor in the previous project on "Evaluation Logic" with Andrew Pitts and I was really grateful when he accepted the idea of a project on authentication logics and invited Prof. Needham. I was also grateful to Kim Wagner, who stepped in to be the RA, when I was offered a proper lectureship in Birmingham and moved there in January 1996.

Of course they changed completely the direction of the project, which was about theory and implementation in Isabelle and ended up being about a new method in Isabelle, i.e. a totally different, but quite interesting new theory and mostly its implementation.

Larry's project  page, linked above, says:

Authentication Logics:
New Theory and Implementations

Lawrence C. Paulson and Roger M. Needham (with thanks to Valeria de Paiva)
Research associates: Kim Wagner (to 31 March 1997), Katherine Eastaughffe
EPSRC logo
Funded by the EPSRC (1 Jan 1996 to 30 June 1999). Grant reference GR/K77051. Value £157,244
This project developed the inductive approach to verifying cryptographic protocols. The key paper has been cited over 1100 times.
In distributed computing systems, components of the system (people, computers, services: usually called principals) must satisfy themselves mutually that they are who they say they are. This is the reason for authentication protocols. Formal analysis of these protocols is highly desirable for discovering flaws and omissions.
This proposal concerns the study of authentication logics, a widespread formal method used in the verification of security protocols. We make a case for a deeper theoretical analysis of the method, as well as for implementations of the resulting logics in the generic theorem prover Isabelle. In the course of the work, attention has shifted from authentication logics to new methods based upon operational models and inductive proofs.