Nominal Coalgebraic Data Types with Applications to Lambda Calculus

(Link).

Authors: Alexander Kurz, Daniela Petrişan, Paula Severi, and Fer-Jan de Vries (University of Leicester)

Reference: Retrieved from Fer-Jan de Vries's homepage, 22 April 2013.

Comments: The topic of this unpublished paper is infinitary syntax, for which terms need not be finite, but rather can extend to the horizon. The key example is the infinitary λ (lambda) calculus, which I have previously discussed, and this paper is a sequel of sorts to a 2012 conference paper that focused purely on this example.

At first glance infinitary syntax might seem an abstruse thing to study, but consider the λ-calculus. This is an abstract model for all computation, but not all computation terminates, and nor is all computation supposed to terminate. We therefore need to think infinitely if we are to reason about the behaviour of non-terminating computation. But how can this infinity be 'tamed' so we can reason about it with our finite minds? There are two techniques. One is to start with the finite terms (over some signature) and extend them to infinity with a procedure called 'metric completion'. The other uses a category theoretic notion called final coalgebra.

I discussed category theory at some length here. Recall that category theorists describe mathematical structure by the transitions, or arrows, between objects. These definitions are often presented as diagrams. One of the truly cool things about category theory is that given such an arrow-theoretic definition, we can turn all the arrows in the diagram around and we get a new definition of something different, but related and often interesting in its own right - what category theorists call dual. So the dual of (the abstract arrow-theoretic definition of) zero is one, the dual of addition is multiplication, and so on. The notion of a set of finite terms can be defined with arrows as what is called an initial algebra; turn the arrows around and you get a final coalgebra, which gives you the set of infinitary terms, equipped with helpful techniques for reasoning about them (coinduction instead of induction).

The move this paper makes is to look at syntax with names that can be free or bound, a major focus of my own research and hence, unsurprisingly, of the recommendations of Google Scholar Updates. To get final coalgebra for this sort of structure we move from the category of sets to the category of nominal sets, which I gave an introduction to here.

At first blush, however, the marriage of infinitary syntax and nominal sets looks like it might be an unhappy one, because the machinery of nominal sets crucially requires a finiteness condition - only finitely many free names. Indeed, the metric completion notion of infinitary syntax and the final coalgebra notion no longer coincide in this setting, as the former happily accommodates infinitely many free names. The authors argue that the more restricted nominal sets setting is the more useful, given that it supports coinduction. This certainly accords with intuition, as if we think of infinite terms as non-terminating 'unfoldings' of programs that started out finite, and impose the reasonable requirement that such unfoldings can not generate new free names, then the infinite unfoldings will only have at most the names of the original finite program.

For those applications where infinite numbers of free names truly are necessary, the authors communicate an idea from nominal sets co-creator Andrew Pitts that replaces free names with constants. I'm not sure how flexible this idea is - we can't bind a constant - but it may be sufficient for some purposes.