Classical lambda calculus in modern dress

(Link).

Author: Martin Hyland (University of Cambridge)

Reference: arXiv preprint arXiv:1211.5762v1 [math.CT], 2012.

Comments: For those reading this blog who aren't familiar with Google Scholar Updates, it might help to describe the format of this tool, because it is a little different from how search tools are usually set up. Instead of being ranked by relevance, my Updates page's 42 results, all presumably judged as crossing some threshold of relevancy, are ranked chronologically, so the most recently archived papers are at the top. The oldest paper is 326 days old; I do not know for sure if they will start dropping off the list, but I suspect they will once they get to a year old. I should say that the 42 results are from my list of 'top' recommendations, which I am using for this blog - there is also a less selective list of 'all' recommendations that currently has 99 results. In weeks where no new papers have been added I will go down the list till I get to my first unblogged paper; there hasn't been a lot of activity lately, so this week's paper is currently fifth.

This is another arXiv preprint (discussion here), but slightly unusually the author specifies which venue the paper is intended for - a 'festschrift' special issue of the journal Mathematical Structures in Computer Science in honour of the 90th birthday of Italian computer scientist Corrado Böhm (journal issues as 'birthday presents' to eminent scientists are a rather nice tradition in science, and quite common; one paper of mine is in a festschrift for Gordon Plotkin's 60th birthday, for example).

The subject of this paper is the λ (lambda) calculus, an area to which Böhm made important contributions. The λ-calculus is a mathematical formalism developed in the 1930s by Alonzo Church as a 'theory of functions'. The two basic constructions are application - given a function f and expression e, we get a new expression f(e) (usually written without brackets), and abstraction - given an expression e which may mention a fresh variable x, the function λx.e will evaluate by binding whatever argument it's given to x throughout e. For example, λx.x is the identity function that returns whatever it's given unchanged. Finally, raw λ-calculus expressions are considered to be equal if they differ only by certain variable renamings, or they can be simplified in the same way by evaluating them as functions. I should also note that the rhetorical distinction I'm making between 'functions' and 'expressions' is a bit misleading - in the pure λ-calculus, everything is a function, and functions happily take other functions as inputs and produce them as outputs.

Remarkably, the simple system I have sketched can be used to compute any function (on natural numbers) that it is possible to compute! This claim is called the Church–Turing thesis (where 'Turing' refers to the Turing machines of Alan Turing). So the λ-calculus is important and useful to people like me whose job it is to ponder the nature of computation all day.

It's one thing to define a formal system of rules and procedures, but it seems a bit like a pointless game if we don't have a precise understanding of what they all mean. After all, why these rules and not some others? This is a question of semantics, and in the case of the λ-calculus this question has, in the words of this paper, "proved vexed". The simplest interpretation - that λ-expressions correlate to ordinary functions - turns out not to work. Computer scientists have had 80-odd years to work on this problem, so of course there are now a number of answers on the market; this paper adds a new one, and shows that it is mathematically natural and yields some of the earlier approaches as special cases.

The semantics for the λ-calculus given by Hyland are category theoretic (an approach I discussed generally here). The basic concept is that of an 'operad', although it could also be given in the more familiar (to me, at least) guise of Lawvere theories. The general idea is that for every natural number n we have a set L(n) of all the λ-expressions with at most n free variables. This is the setting for ordinary equational logic (see here). To get to the λ-calculus we must also have functions L(n+1)→L(n) and L(n)→L(n+1), where the first corresponds to adding an abstraction, and the second to applying an expression to a fresh variable. These functions are related because doing the first, then the second, leaves you back where you started - e = (λx.e)x. Doing the second, then the first, need not leave you back where you started, but if we added the requirement that it did - that f = λx.(fx) - this is exactly η-equivalence, a common condition to add on to the basic λ-calculus.

This is attractive stuff if you are a computer science and category theory nerd - and I am! The rest of the paper is dedicated to showing that this construction, called a 'semi-closed structure' is indeed a good way to interpret the λ-calculus, by relating it to the syntax, and to some other notions of semantics. There's a lot in this paper and I couldn't absorb it all in one week - the 'Taylor Fibration' material went a bit over my head - but I still greatly enjoyed it.

Associahedra, Multiplihedra and units in A∞ form

(Link).

Author: Norio Iwase (Kyushu University)

Journal reference: arXiv preprint arXiv:1211.5741v6 [math.AT], 2013.

Comments: I should start by saying that this might very well be a fine paper. But then again, it might not. I simply have nowhere near the understanding of the area this paper covers (algebraic topology) necessary to make head or tails of it. While it's healthy to broaden my horizons by reading outside of my narrow field, there comes a point when so much study would be required to comprehend a paper that I, however reluctantly, have to put it on the 'too hard' pile.

So the question to address is this: why has Google Scholar Updates decided that this should be among the top papers archived in the last 300-odd days to recommend for me? One of the common deficiencies of this automated recommendation approach is that, unlike a recommendation from a human being, no reason is provided for why I might be interested in something, but scanning the paper provides a few clues. There are a couple of mathematical concepts in here which I have used in my publications (coalgebra, internal categories). Less helpfully, something called equivariance is used here, and I very frequently use the word 'equivariance' - but I mean a somewhat different thing by it than how it is used here. Has Updates been confused by a homonym? The paper also cites a PhD thesis by Marcelo Aguiar which I have cited before.

This is all very well and good, but a couple of mathematical concepts and one citation is just not enough of an 'in' when it comes to digesting a 53 page mathematical paper in an area for which I don't have anything close to the basic prerequisites. After two papers I've read and enjoyed, this is the experiment's first unambiguous failure. It will be interesting to see how often this happens as I continue.

Initial Semantics for Reduction Rules

(Link).

Author: Benedikt Ahrens (Université Nice Sophia-Antipolis)

Reference: arXiv preprint arXiv:1212.5668v1 [math.LO], 2012.

Comments: First, let's discuss the status of this paper. The arXiv is an internet archive for scientific 'preprints' (draft papers not yet published in any peer-reviewed outlet). As such, this paper is probably currently undergoing peer-review for some journal, so some care should be taken with the results as they have not yet withstood this process. The point of arXiv is to allow dissemination of results, and claims of priority, to be established more rapidly than the often ponderous publication process. This paper will undoubtedly be changed in some way as a response to reviewers' comments before it sees the 'official' light of day; it is an example of the 'grey literature' that Google Scholar tends to include that I mentioned in my mission statement post.

There are, however, two reasons to trust the results of this particular paper. First, they appeared in the author's PhD thesis, which has been examined and passed. Second, this paper is an extended version of the author's 2012 conference paper Initiality for Typed Syntax and Semantics, which was peer-reviewed before acceptance. This model of relatively rapid publication of a short paper in a conference, followed by the slower publication of a longer paper, covering similar territory in more depth, in a traditional journal, is very common in computer science (and much less so in other disciplines).

Considering the paper's contents, this is an application to computer science of an approach to mathematics called category theory. Categories provide a way of looking at mathematics where instead of taking mathematical 'objects' as the primary focus, as a conventional mathematician might, we focus on the interconnections between objects. Stated at that level of abstraction it might seem vaguely Eastern and mystical, but it's a completely formal way of building up mathematics that is exactly as powerful as set theoretic foundations. The advantage of this different angle on things is a bit like learning to speak a new language - different concepts tend to come to light. Category theory has been particularly widely applied in computer science, perhaps because computer scientists are quite comfortable thinking about dynamic transformations between objects, rather than the objects' static descriptions, as the most interesting thing.

The category theoretic concept that gets the most work in this paper is that of a monad. The definition of a monad is, like many things in category theory, relatively simple but so abstract that its utility is far from obvious. If we view a category as an area of mathematics (so we have a category for set theory, a category for group theory, or even go down the rabbit hole to define a category for category theory itself), then a monad can be thought of as a construction that allows you to do algebra within that area of mathematics. (In fact, monads have made a slightly surprising escape from the world of pure theory to become a useful tool in functional programming, but that is orthogonal to the interests of this paper.)

In fact, this paper doesn't use monads in the conventional sense, but rather the relative monads introduced by the 2010 paper Monads Need Not Be Endofunctors by Altenkirch et al. There, the monad is not defined on a category, but on a translation between (possibly different) categories (such a translation is called a functor). This generalisation collapses to the conventional definition if we set this functor to be the identity on some category. The impact of this generalisation when we use our monads to do algebra is that our variables may live in a different mathematical universe from our terms. In this paper, the variables reside in the category of sets, while the terms reside in the category of preorders (sets equipped with a reflexive and transitive relation).

Why pull this trick? The clue is in the 'reduction rules' of the paper's title. Ahrens looks at systems like the λ-calculus where some terms can be reduced, or simplified, to other terms; the reduction relation that holds across all the terms is a preorder. This motivates the setting of terms within the category of preorders. So why not work entirely within this category, using normal monads? This would mean that the variables would also live in the category of preorders, so we might be able to reduce some variables to others. But this is not the case for most applications - variables usually form a set only, in the sense that they have no non-trivial preorder definable on them. Therefore Ahrens keeps his variables in the category of sets, and injects them when needed into the category of preorders via the trivial embedding functor, here called Δ. Monads for systems like the λ-calculus can then defined on the functor Δ, and the 'algebraic' view that arises (via initiality; I'm afraid I'll have to beg off going into the details of that here) give rise to mathematical descriptions of syntax and reduction semantics, and a notion of reduction-preserving translation which is here used to map the programming language PCF into the simply typed λ-calculus.

The key word in the sentence above is 'typed'. In fact much of the development discussed above can be found in a 2011 paper be the same author, and the specific advance of this paper is to detail how (simple) types are incorporated into this view (types are essentially annotations on terms that restricts how they can be used, for example preventing you from applying an arithmetical operation to a string; most programming languages have them). Technically, it means shifting from categories of sets and preorders to categories of typed families of sets and preorders. This shift apparently introduces only "a minor complication" to the major theorem of the paper (Theorem 3.32), but it is a necessary one to talk sensibly about typed languages like PCF.

Finally, this work has been formalised and machine-checked with the proof assistant Coq. Such formalisation is an increasingly popular way to boost confidence in the correctness of mathematical results; perhaps unsurprisingly, computer scientists have been the most eager to adopt this technology. It's not something I've dealt with in much depth myself however, so I have no particular comments or insights into the final section of this paper, which details the formalisation process.