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 'A New Approach to Abstract Syntax with Variable Binding'

(Link).

Authors: Murdoch J. Gabbay and Andrew M. Pitts (University of Cambridge)

Reference: Formal Aspects of Computing Vol. 13(3-5), pp 341-363 (2002).

Why this paper? Cited by 9 (of a possible 29) of the papers in my Google Scholar Updates recommendations (where multiple citations from different papers by the same author(s) in my recommendations are disregarded).

Comments: My PhD and some of my subsequent research was built around something called nominal techniques; this is the journal version of the conference paper that introduced them (in fact the second author, Andrew Pitts, was my PhD supervisor). Already some clarification is necessary: computer science has for some reason developed an unusual publication culture in which peer-reviewed conferences, rather than journals, take center stage. But conference publication often imposes tight space limits on papers, which can force authors to tighten their prose, which I find no bad discpline, but more regrettably can mean some details or examples are omitted. Hence new research is often published twice, with a more detailed 'journal version' following the conference version, often years later because of the slowness of the journal review process (which itself is probably contributed to by so much work having to be reviewed twice!). Another clarification to my first sentence is that the word 'nominal', which has become the brand name under which all developments of this work by Gabbay and Pitts are grouped, does not appear in this paper. I believe it was introduced by Pitts in his 'Nominal logic' paper, which was published before this paper but written after it, thanks again to the vagaries of academic publication.

The problem this paper addresses is that of reasoning formally in the presence of names and binding, ubiquitous features of computer science applications and other formal settings like mathematics. Of course names are everywhere - think of variable names in programs, or the identifiers like x and y we use when we do maths. The precise names we use is at some level arbitrary; while we're doing our mathematical manipulations we better keep track of our xs and ys, but 'from the outside' it obviously wouldn't have mattered if we'd called our variables foo and bar instead. Binding (sometimes, scope) is simply the point where this 'outside' versus 'inside' distinction is made: some operations have the property that the choices of names inside the operation's domain are irrelevant to anything outside that operation's domain. Such structure is vital in software engineering applications where people worry about encapsulation, but is in fact virtually unavoidable in any sufficiently interesting formal setting.

Anyone with a passing interest in computing, or even logic or mathematics, would nod along to most of the previous paragraph, but perhaps would not become greatly interested. Names and binding are basic machinery, and there is no reason to spend time thinking about them, as opposed to getting on with using them! The twist comes when one tries to reason fully formally, for example to convince a computer that a certain program has a certain desirable property. This sort of reasoning, if successful, can yield guarantees about software far more robust than mere testing, but it is not easy, and names and binding structure turns out to be be one of the (many) barriers to doing this successfully. In particular, proofs involving structural induction, which are vital to programming languages applications in particular, do not play well with bound names. So there is a problem to be solved.

The solution proposed by Gabbay and Pitts (I should note that other candidate solutions exist, but I will not discuss them here) is to change the set theoretic foundations on which we build our mathematics, from the standard one to an alternative framework developed by Fraenkel and Mostowski in the 1930s for reasons completely unrelated to computer science. In this framework certain elements called atoms claim a privileged place, giving mathematics in this universe a slightly different flavour. This paper adapts this work in (to me) wildly surprising fashion to show that if we view these atoms as our names then we have just the right 'universe' in which to model, and reason in a reasonably intuitive way about, binding, up to and including the structural induction I mentioned earlier.

It should be acknowledged, of course, that doing mathematics in a 'different universe' sounds like an cumbersome (and possibly eccentric!) move. For this stuff to actually be used, the esoteric set theory needs to be at least partially hidden, and subsequent work, most notably the 'nominal logic' paper I mentioned above, has helped to do this. Still, all of the many subsequent applications of Gabbay and Pitts's work can be seen to rest on some of the most abstruse mathematics you can imagine, a story that must gladden the heart of any working theoretician!