Authors: Nick Benton (Microsoft Research Cambridge), Martin Hofmann (LMU Munich), and Vivek Nigam (Federal University of Paraíba)
Reference: Retrieved from third author's homepage, 11 Feb 2013.
Comments: It's an interesting and perhaps underappreciated fact that where you do your earliest research can typecast you for some time - perhaps a whole career - into a certain 'school' of researchers who look at similar problems, and use similar techniques to solve them. This notion of a school of thought is perhaps most known in the humanities, and particularly philosophy, but it's just as true in science, I think. For this reason, perhaps it's not surprising that this is the third paper in four weeks that Google Scholar Updates has served up that hails from Cambridge, where I did my PhD (although Benton works at Microsoft Research Cambridge, rather than the university's Computer Laboratory, that doesn't really diminish the point - the buildings are after all right next door to each other).
I should be completely clear by saying that this paper hails only in part from Cambridge, as this is a truly international collaboration, with the England-based researcher joined by one in Germany and another in Brazil. The paper is described on Nigam's website as a "conference submission", so the usual health warnings about grey literature apply - the paper has not been peer reviewed, is very likely to change between now and publication as a result of reviewers' comments, and of course may not appear at all if rejected.
This paper is yet another to look at my favourite topic of nominal sets (see here for discussion), albeit in rather disguised fashion. It's well known (although I don't know that the result has ever been published) that nominal sets have an equivalent formulation called the Schanuel topos, where instead of taking sets with certain structure as primary, we take certain homomorphisms between categories, called functors, as our objects. The intuition is that these functors map finite sets of names to the sets of elements that are 'supported by them', so the functors map into the category of sets. We then throw out all the functors that don't have a certain property called pullback-preservation. It's fair to say that this formulation of nominal sets isn't so simple to understand for most, but it's natural from the point of view of category theory, and that point of view can be useful, as I discussed here.
The move taken in this paper is to consider the pullback-preserving functors that start in the same category as the Schanuel topos, but map into the category of setoids, not sets. I should say that there seems to exist a reasonably widely used definition of 'setoid' (see e.g. here) which the authors are not cohering to, which is confusing, but these things happen (and Humpty Dumpty would urge us to be philosophical about it). The essential notion is that a setoid is a collection of 'types' equipped with explicit 'proofs' that some of these types are equal to others. I found myself wondering whether a set theoretic version of this paper could have been written that starts with the usual definition of nominal sets and adds structure to define 'nominal setoids'; this is not discussed in the paper, and perhaps such a construction wouldn't work, or would work but not be so natural for the applications that the authors have in mind.
What applications of this setoid version of Schanuel topos do the authors present? In a related and longer arXiv paper they discuss a range, but this paper looks as a case study at reasoning about the ν (nu) calculus, a formal calculus developed by Andrew Pitts and Ian Stark in a 1993 paper, and in particular the equationally specified semantics for the observable behaviour of the ν-calculus, first studied by Stark in 1996. The ν-calculus is an extension of the λ-calculus with explicit support for the generation of new 'names' encapsulated within a given scope (a common feature of programming languages). This paper shows that the setoid-Schanuel view can support a definition of the operators of the ν-calculus (to be precise, a 'metalanguage' for reasoning about the ν-calculus) which validates the equations for semantics that Stark gave in his 1996 paper.
No comments:
Post a Comment