Discussing "First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees"

(Link). Slightly confusingly, the authors earlier published a shorter conference article with the same name.

Authors: Lars Birkedal (IT University of Copenhagen), Rasmus Ejlers Møgelberg (IT University of Copenhagen), Jan Schwinghammer (Saarland University), and Kristian Støvring (University of Copenhagen)

Reference: Birkedal, L., Møgelberg, R. E., Schwinghammer, J., & Støvring, K. (2012). First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Logical Methods in Computer Science, 8.

Why this paper? Cited by A Formal Logic for Formal Category Theory, Classifying topoi in synthetic guarded domain theory, and A metalanguage for cost-aware denotational semantics

This paper, which has been very influential on a chunk of my career, nicely pieces together some practically minded applications in program verification with the more abstract world of category theory.

The practical motivations are very similar to the step-indexing paper I discussed a few weeks ago, namely type systems with recursive features that appear difficult to reason about without getting trapped in unsolvable circularities. In the key example of this paper, a programming language with higher-order store (i.e. the ability to store typed programs in memory) forces one to define the meaning of types in terms of the meaning of the store, but also to define the meaning of the store in terms of the meanings of types! In the step-indexing approach, one works around these circularities by invoking a natural number that decreases towards zero as the program computes; this paper does something quite similar, but in the name of “avoiding tedious calculations with step indices” it instead asks us to work in a topos which naturally supports this sort of notion of steps.

A topos is, very roughly, a ‘mathematical universe’ (or category) which contains the mathematical machinery one would expect to have in set theory. For example, a subobject classifier is an object of truth values. We might expect to have just the two values, True and False – and indeed there are toposes for which this is so – but in the topos of this paper, the topos of trees, one can see the subobject classifier as the set of all natural numbers, along with the infinite value ω. One can consider 0 as False, ω as True, and each positive integer n as ‘not falsified by the first n steps of computation’ (this is not quite how this paper presents things, but is the point of view taken for example by a later paper of mine). This is quite a nice way to think about computations that unfold over time: consider two streams (infinite lists); they are 1-equal if their first elements agree, 2-equal if their first two elements agree, and so on to only reach ω, or ‘true’, equality if there is no index on which they will ever be unequal. In other words, working inside the topos of trees gives you access to a logic that allows you to talk about certain aspects of computer programs that are harder to describe with more conventional logic. In particular, instead of working directly with the indices, one instead can do a lot with a modality (new logical connective) called ‘later’ than helps hide those details away while preserving the ability to make the sort of arguments for which one would otherwise explicitly involve step indices.

As well as the logical point of view which comes from working with the subobject classifier, one can also use the topos of trees as a denotational semantics (mathematical meaning) for types in various ways, whether one is reasoning about a typed programming language, or using dependent type theory to construct a formal mathematical argument. Looked at through this prism, instead of viewing a type as standing in for its set of elements, one can view types as an infinite series of sets that become more and more precise or informative over time. For example, the type of streams is not merely the set of infinite sequences, but instead an infinite string of sets that at step 1 reveal only their first elements, at step 2 reveal their first two elements, and so on. The modality `later’ now reappears in slightly different guise as a type-former; one needs to check that self-references are guarded by later in order to ensure one has a meaningful recursive type definition. This idea of checking syntax for guardedness in order to ensure that recursive definitions are good is quite old, but usually takes place at the level of the syntax of terms. By lifting this check to the level of types we get the advantages that well-behaved type systems usually confer, particularly modularity – the ability to stick any two good programs together, provided their types agree, without their combination going wrong.

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.

Nominal Event Structures

(Link).

Authors: Andrei Alexandru and Gabriel Ciobanu (Institute of Computer Science Iași)

Journal reference: Romanian Journal of Information Science and Technology, Volume 15, Number 2, pp. 79-90 (2012).

Comments: I must admit that this paper hailing from the 'Romanian Journal of Information Science and Technology' (ROMJIST) didn't exactly fill me with confidence. My scepticism was not primarily driven by the 'Romanian' in the title - many journals and conferences are sponsored by scientific societies linked to specific countries or regions, and not necessarily the 'obvious' countries either - the conference WoLLIC, through which I have published, has significant sponsorship from Brazil, for example.

Rather, it's the 'Information Science and Technology' in the title that set off alarm bells. How does a journal ensure high quality and credible reviewing when their remit covers the entire field of computer science? If you're the Journal of the ACM that's possible because you've set yourself up as a flagship journal for the whole subject, with a seriously high powered and diverse board of editors (Nature is a more famous and even more wide-ranging example of this sort of model). But for less high profile journals (a category in which ROMJIST obviously sits) a larger degree of specialisation seems essential if quality is to be maintained.

Setting that aside, Google Scholar has recommended this paper to me, and so I read it with an open mind. The reason for the recommendation is clear enough, as it deals my speciality of nominal sets, a variant of set theory in which each element is linked to a 'finite support' of names. I discussed the computational applications of this model in my first article on this blog. It's a natural and common move to reinterpret mathematical concepts from 'ordinary' set theory into nominal set theory - my own work on equational logic, which I discussed briefly last week, can be seen in this light. This paper makes this move on event structures, abstract structures in which causality and conflict between events can be modelled.

Here's the problem though - nowhere in this paper is it explained why creating a nominal variant of event structures might be a good idea. No examples are given of these new nominal event structures, no problems are solved using them, no 'further work' section suggests what might be done with them next, and no interesting theoretical or mathematical issues are brought to light. The small number of novel proofs in this paper are all completely routine checks that finite (or sometimes empty) support properties are not violated by the new definitions. I don't intend this blog to be a space where I 'review' papers in the academic sense, with all the controversy that process inevitably generates, but I can't report on the usefulness of Google Scholar Updates without indicating where the papers I read are not useful, and this is certainly such an instance.

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.

Imperative Programming in Sets with Atoms

(Link).

Authors: Mikołaj Bojańczyk and Szymon Toruńczyk (University of Warsaw).

Conference: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012), December 15-17 2012, Hyderabad, India (invited talk).

Journal reference: Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, Deepak D'Souza, Telikepalli Kavitha and Jaikumar Radhakrishnan (Eds.), pp 4-15 (2012).

Comments: All but one of the papers I've published have been on nominal sets, so it is hardly surprising that Google Scholar Updates have started me off with something in this vein, although I had not read this particular paper.

Nominal sets are a mathematical model in which each set-element is 'supported by' finite sets of atoms. What are atoms? In the original theory, developed in the 30s by the set theorists Abraham Fraenkel and Andrzej Mostowski, they were simply elements of an infinite set with no particular structure. This paper, and other recent papers by Bojańczyk and various co-authors, takes a more expansive view of what an atom might be, but first we will consider this unstructured case.

Frankel-Mostowski set theory was imported from the abstruse world of foundational set theory into the apparently more grounded domain of computer science by Murdoch Gabbay and Andrew Pitts, in their 1999 paper A new approach to abstract syntax involving binders, where it was used to model the syntax of computer programs and formal calculi. The problem the Gabbay-Pitts paper addressed was the syntactic construct of names, such as variable names in a program, which were and are a continual source of error and irritation to those who trying to reason formally about computation. The atoms of the old set theory played the role of names in various applications, and provided a model in which we can reason about names with rather less headaches than before. The label 'nominal sets', and more broadly 'nominal techniques', were (later) coined for this approach - not the only approach on the market for dealing with names, but certainly one of the most prominent and successful.

This paper is a companion piece to Bojańczyk et al's 2012 Towards Nominal Computation, in which a functional programming language Nλ was presented to support computation in nominal sets. I should note that Nλ is by no means the first example of the application of nominal sets to the design of programming languages, and some of these languages have actually been implemented while Nλ has not; in the last paragraph we will discuss what makes Bojańczyk et al's research programme truly distinctive. But setting that aside, in Imperative Programming in Sets with Atoms we see a language based on the same principles as Nλ, but in the imperative style. The distinctive construct of this language is the command

for x in X do I

where x is a variable, X is a set possibly containing some atoms, and I is a code fragment. This command triggers a parallel execution in which x is bound to every (correctly typed) element of X and I is executed accordingly. If any such run of I fails to terminate, then this code fails to terminate. What if they all do terminate? Suppose y is some variable that has an expression assigned to it in the code fragment I. If y is of type atom then every run of I must agree on y's value, regardless of the value of x, or we get a run-time error. But if y is of type set, the final value of y will be the union of all the runs of I.

The most interesting aspect of Bojańczyk et al's research direction (initiated by the 2011 Automata with Group Actions) is that they have substantially generalised the definition of nominal sets to accommodate various structure, such as orderings, on their atoms. Their claim is that these generalised nominal sets are useful not merely for 'dealing with names', but also for reasoning about and computing with a variety of infinite computational phenomena (if this sounds paradoxical, it isn't; the set of integers is infinite but no one objects to programs that manipulate them). For example, the semantics I have sketched above for the command 'for x in X do I' seems to require that X be finite to work in the real world, as we obviously cannot compute infinitely many parallel branches. However, some sets that are infinite but have a finite 'recipe' (technically, finitely many orbits) can be sensibly computed within the framework defined in this paper. The big application of the generalisation at this stage is a model of computation called finite-memory automata, but it's a pretty new direction, so there may well be more value to be found in this relaxation of the normal definition of nominal sets.