7 Dec 2004 chalst   » (Master)

I've been spending a fair amount of time trying to improve the quality of the logic pages at wikipedia. I've just posted a slightly polemical comment in one of the talk pages about the name "Curry-Howard isomorophism":
I've got a long past with this topic, so much so that I probably can't be objective about certain details: my doctorate was on the so-called classical Curry-Howard correspondence and begins with a rant about the misleading way the topic is made use of in many works in the field. While the centre of the topic was Bill Howard's 1969 manuscript, which indeed presented an isomorphism between two formal systems, there are reasons to prefer not to call the topic the Curry-Howard isomorphism, and these are mine:
  • Howard's manuscript was called The formulae-as-types notion of construction, the terminology formulae-as-types correspondence is closest to the source;
  • The topic does not consist in the first place of showing an isomosophism, rather it consists of establishing first an intuitive observation of a correlation between certain notions of construction in type theory, and certain patterns of inference in logic; the presentation of an isomorphism is rather a virtuoso flourish that adds force to this observation. To insist on talk of isomorphism obscures the most important part, which is the intuitive and I think necessarily informal part;
  • There are many important aspects of the theory that cannot be put into isomorphism, because what would have to be regarded as the logical counterpart of the type theoretic construction makes no logical sense: the clearest development of this problem is in Zhaohui Luo's Computation and Reasoning, where he discusses the problems applying the formulae-as-types correspondence to the Extended Calculus of Constructions (essentially one cannot mix dependent sum with System F like polymorphism and expect the result to be entirely logic-like);
  • There's something artificial about Howard's isomorphism: while the simply-typed lambda calculus is a calculus of an obviously fundamental nature, there's something forced about the logical end, namely the idea of labelling assumptions and implies elimination rules. The labels are needed for the isomorphism to work, but before the work of Curry and Howard, no-one working with natural deduction thought to keep track of these; instead the assumption was simply that all assumptions matching the implies elimination rule are discharged.
As a last point, if I am convinced that 'Curry-Howard isomorphism' is the more widely used term, the people whose judgement I respect most, mostly prefer 'formulae-as-types correspondence'; and at the risk of sounding elitist, I think we should prefer the better term even when it is less popular. My preference for this page are:
  1. Formulae-as-types correspondence;
  2. Curry-Howard correspondence;
  3. Curry-Howard isomorphism;
with the latter only under sufferance; also note that the phrase 'Curry-Howard' is disrespectful to those logicians who contributed fundamental insights; I would particularly single out William Tait in this respect.

ncm's testimonial
A couple of days ago, a rather stressy morning was brightened by noticing that ncm posted a fun and mostly generous Orkut testimonial. But really, he's got my LISP infatuation all wrong! I guess I'll post something in my diary saying why I got into scheme/LISP...

Planet LISP ...which reminds me, this should be my first diary entry syndicated to the multitudes who read Planet LISP (though thanks to a comment of dan, maybe my last post counts as the first?). Well, hello there... A comment with my thoughts on Kent Pitman's idea of programming lamnguages as political parties and what Common LISP and Scheme can learn from each other is planned in the not too distant future.

LtU on types A lot of energy is being expended by Lambda the Ultimate regulars on various issues around type systems: not in itself surprising, but what I find a bit odd is how little this broad-minded group (my dogmatic self excluded, of course) are making contact on the fundamental issues. A list of some recent threads:

  1. Why type systems are interesting
  2. Why type systems are interesting - part II
  3. Why type systems are interesting - part III: latent types
  4. Looking for Classic Types Thread
  5. What's a definition of "type" that beginners can understand?
  6. Definition of Type

Latest blog entries     Older blog entries

New Advogato Features

New HTML Parser: The long-awaited libxml2 based HTML parser code is live. It needs further work but already handles most markup better than the original parser.

Keep up with the latest Advogato features by reading the Advogato status blog.

If you're a C programmer with some spare time, take a look at the mod_virgule project page and help us with one of the tasks on the ToDo list!