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.

A Sorted Semantic Framework for Applied Process Calculi

(Link).

Authors: Johannes Borgström, Ramūnas Gutkovas, Joachim Parrow, Björn Victor and Johannes Åman Pohjola (Uppsala University)

Reference: Retrieved from Joachim Parrow's homepage, 16 April 2013.

Comments: After some time away from the blog due first to conference travel, then to the next round of conference submission, a number of papers have collected in my Google Scholar Updates in-tray. This week sees an unpublished paper that, judging from its length of exactly 15 pages (not counting appendices) must also be a conference submission - wrestling scientific work to exactly fit the page length requirements of this or that venue is one of the necessary frustrations of being a researcher.

A very common mode of research in theoretical computer science is to study formal calculi, which are often best seen as idealised programming languages, usually with a very simple syntax and set of operations. These calculi allow various aspects of computation to be formalised and studied without all the impurities and hacks that go along with a 'real' programming language intended to be conveniently usable. The most famous and important such calculus is the λ (lambda) calculus, which I discussed a few posts back.

Almost as important are the calculi known collectively as the process calculi, which are intended for the formalisation and study of concurrent computation - computation that runs in parallel (perhaps simultaneously) in different threads, occasionally interacting. This is an important topic because computers - even home PCs - are increasingly multiplying the number of separate 'cores' in their hardware, not to mention the use of massively distributed computation across the internet; yet what the best programming languages, methodologies, and theory should be for this sort of architecture remains very much up for grabs.

The process calculi best known to me is the π (pi) calculus, introduced by Robin Milner, Joachim Parrow (one of the authors of this paper), and David Walker here. This notion of process calculus alone has produced dozens of offshoots and modifications, often aimed at some specific application. To name just one important example, the spi calculus is used to formalise cryptographic protocols.

At one level this paper merely adds to the arguably overstocked zoo of process calculi, by making modifications to the existing psi-calculus by adding a sort system (a concept I discussed, in a rather different setting, here) and more flexible pattern matching. At another level, this paper is intended to be a unifying and clarifying contribution to the zoo, by setting the augmented psi-calculus up as a system that captures many other process calculi. By this the authors don't mean that the new and improved psi-calculus makes systems like the spi calculus practically redundant; rather, the spi calculus can be seen in a some relatively natural way as a particular instantiation of the psi-calculus. The advantage of this, as posited in the introduction, is that basic theoretical proofs about process calculi only need to be 'done once', for the very general psi-calculus, and then can be exported 'for free' to hold for the many process calculi that are examples of the psi-calculus. With these basic correctness proofs out the way, people can then direct their attention to what really is unique, interesting or useful about the calculus they are particularly interested in.