Discussing 'Nominal Unification'

UPDATE - Due to upcoming teaching commitments and, after that, paternity leave, this blog will not be updated again in the near future.

(Link).

Authors: Christian Urban (University of Cambridge), Andrew M. Pitts (University of Cambridge), and Murdoch J. Gabbay (INRIA).

Reference: Theoretical Computer Science vol. 323(1-3), pp. 473-497 (2004)

Why this paper? Cited by 4 (of a possible 28) of the papers in my Google Scholar Updates recommendations.

Comments: In the first iteration of this blog I reviewed recent papers recommended to me to by Google Scholar Updates; one of the reasons I abandoned this is that many of these new papers were quite strongly linked to older work, and I ended up having to explain all that older work before writing about the new. Note that being strongly linked to older work is no bad thing - on the contrary, such incremental research is the unglamorous but essential heart of scientific progress. But my new focus for this blog, on 'classic' (which is to say, highly cited) papers, allows me to focus more on foundational work, which tends to be more original and so may be described with less reference to prior literature.

The reason for this discussion is that I have already discussed this week's paper at some length in a post for the first iteration of this blog. Please feel free to look up the post; the only correction I'd make is that is that a quadratic time (which is to say, feasibly fast) algorithm for nominal unification is in fact sketched in the conclusion of this paper, whereas I had previously thought that credit for this should go to Levy and Villaret alone.

Let me instead discuss something slightly orthogonal to this paper. The phrase 'nominal techniques', which I discussed for example here, actually refers to two things - syntax and semantics. I have previously emphasised the semantical (which is to say, mathematical) side because that is where my interests lie; but here is a paper that is clearly nominal techniques yet makes explicit use of neither Fraenkel-Mostowski set theory nor nominal sets. What brings the syntactic and semantical work together under the heading 'nominal techniques' is their commonality of jargon and notation, their treatment of names as 'first-class' entities rather than as embarassments to be hidden away, and their use of name permutations (name-for-name swappings) as the main technical engine. These links mean that for a trained reader it is simple to see how this paper should be understood semantically, although my workshop paper 'Nominal Logic with Equations Only' is the only place I know of where this is done explicitly (see Section 6).

Discussing 'Linear Logic'

(Link).

Author: Jean-Yves Girard (Université Paris Diderot)

Reference: Theoretical Computer Science Vol. 50(1), pp 1-101 (1987).

Why this paper? Cited by 5 (of a possible 31) of the papers in my Google Scholar Updates recommendations.

Comments: This paper begins with an extraordinary disclaimer from the editor: "Because of its length and novelty this paper has not been subjected to the normal process of refereeing. The editor is prepared to share with the author any criticism that eventually will be expressed concerning this work." In other words, the paper was published in one of the top journals in theoretical computer science without review. With hindsight there is no doubt that this paper was worthy of publication - four and a half thousand citations speaks to that - but one wonders if a proper reviewing process could have helped point out Girard's rediscovery of much that was already known, particularly the work of the relevant logicians. Instead, only six papers are cited in this 101 page paper, 5 sole-authored by Girard himself! This matters for more than just the claiming of credit; for example Girard's notational innovations, which have stuck despite attempts at reform by the likes of Arnon Avron, have almost certainly harmed the ability of computer scientists and the broader logic community to communicate.

Linear logic is in part a substructural logic, meaning that less powerful 'structural rules' are available for reasoning than there would be for more standard logics. This is a technical concept, but can be explained by example: there is a substructural 'and', for which you cannot deduce 'A' from 'A and B' (weakening), nor 'A and A' from A (contraction). These are obviously not desirable restrictions to have if you really mean 'and'! But linear logic has the standard 'and' as well; the substructural one simply allows you to reason in a "resource conscious" way, in which propositions may not be thrown away with weakening, nor duplicated with contraction.

The insight that led to linear logic lay in Girard's study of coherent spaces, a mathematical model (or semantics) for intuitionistic logic (a standard logic which can be, but usually isn't, viewed as 'substructural'). In this model the meaning of the apparently basic logical notion of implication (if... then...) came apart into two. The denotation of "if A then B" involves (1) 'permission' to use A as many times as we might want to, and (2) some translation of however many As we fixed on, into a B. (2) is the the resource-conscious 'substructural' part, whereas (1) can be considered as a brand new logical connective, written !, which permits the throwing away or duplication of a proposition. Hence a new logic, expressive enough to encode intuitionistic logic (and via the well known encoding, or more directly) classical logic also.

As might be suggested by its 101 page length, there is a lot more to this paper, including an alternative semantics of 'phases', which look a lot like the 'ternary relations' already well known to relevance logicians, sequent calculus (which we discussed in general here), and 'proof nets', a style of deduction analogous in some ways to natural deduction. It is all quite engagingly written, thank goodness: necessary technical grinding is openly flagged as "boring", and the dedicated reader is rewarded on page 92 with "This paper has already been too long, and a reader not already dead at this point will have no trouble in finding out the details." Of course I already knew Girard as a flamboyant and humorous writer, exhibit A being his virtually indescribable Locus Solum, a 206 page paper that includes an almost 100 page long appendix titled 'A pure waste of paper', essentially amounting to his personal book of jokes and observations about logic ("The theory of free and bound variables is still a typical topic for the early morning lecture the day following a meeting banquet. But this is a deep subject..."). Strangely enough, that paper appears to have been reviewed in the usual way!