An algebraic presentation of predicate logic

(Link).

Author: Sam Staton (University of Cambridge).

Conference: 16th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2013), 18-20 March 2013, Rome, Italy.

Journal reference: Lecture Notes in Computer Science (to appear).

Comments: After last week's head-scratcher, Google Scholar Updates is back on firmer ground with a paper by somebody I know, from my old university, that cites one of my own papers. In fact, this paper is due to be presented at a conference later this year that I also have a paper at (pdf), so this is a chance to read something before I see it presented.

Equational logic is the logic that allows you to reason about systems that are defined with equations; its basic rules include facts such as "everything is equal to itself", and "if x is equal to y, then y is equal to x". This may not seem particularly deep, but in fact a vast number of mathematically significant systems are amenable to equational reasoning - groups, rings, Boolean algebras, and so on. I myself have conducted a short course of lectures on equational logic at the Australian National University's Logic Summer School - my slides can be found here.

For all the power of equational logic, both the demands of applications and pure curiousity have often lead people to tweak or extend the basic logic. The bulk of my own publications have looked at a certain tweak of equational logic, and this paper introduces another (my paper Nominal Equational Logic, with Andrew Pitts, is cited as related work for this reason).

Staton's new style of equational logic is called 'parameterized algebra'. In the standard equational setting, we start with a 'signature' of operation and constant symbols that can be used to build terms. For example, if we are interested in monoids we have an identity constant and a binary multiplication; if we move to groups we add a unary inverse operation, and so forth. With parameterized algebra we have two signatures - a main one, and an ancillary one that is used to define parameters. The difference between this and ordinary equational logic with two sorts is two-fold. First, parameter-sorted variables can be bound by the main signature's operations. Second, parameter terms can be appended to the main signature's variables. For example, the term

∃ a. P[a]

where a is a parameter-sorted variable and P is a main signature variable, indicates that a is bound by the existential quantifier ∃, and that P is 'standing in' for a predicate that may make some mention of a.

Once the new logic is defined, the paper goes in two directions: first, it develops the metatheory of the logic, first via Lawvere-style classifying categories, and then via monads (in fact, relative monads; this is the second paper of the four I have had recommended to me that has made use of this fairly recently developed notion). Second, a major example is developed of 'disjunctive predicate logic', a fragment of first order logic (lacking e.g. implication) that uses parameters. This example is considered as a small programming language, and it is shown that it has a mathematically natural description in the 'classifying category' setting.

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.

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.

Mission Statement

It's a bit hard to remember how keeping up with research was supposed to go before Google Scholar came along, despite the fairly brief time that it's been a fully developed tool for searching, and chasing forward-references, in the academic literature. Certainly, Google Scholar is much more comprehensive than any more established database like Scopus, and only slightly more noisy (your taste for Scholar probably depends largely on how you feel about the 'grey literature' it tends to include).

Despite worrying signs that Google may be de-emphasising Scholar in its interface, the search tool continues to be developed in interesting new ways. For example, publication and citation pages for individual researchers are now a great way to check a researcher out ‘at a glance’, and to show off to potential employers or other interested parties (examples: my page, or the Logic & Computation Group at ANU where I do my work).

Still, even with with this search engine it can be difficult to know that you're really keeping up with the advances in your field, let alone keeping up with any wider research that may have some serendipitous connection to your work. The new(ish) tool Scholar Updates is designed to help with this. If you have a Google Scholar profile, your papers can essentially be used as a giant search term to look through recent additions to the Scholar database, and those likely to be relevant to you are then compiled in an ever-updating list.

After seeing an enthusiastic user review of Updates, I decided to have a look myself, and was immediately impressed by the page of recent papers, many of which I was not aware of, which for the most part appeared to be highly relevant to my interests. But this a superficial first impression - would regular use of this tool really make me a better and more informed researcher? That calls for an (informal) experiment, and this experiment is this blog.

The rules are simple - every week (give or take) I'll pull the top recommendation from Updates that I have not previously read, write it up briefly on this blog, and comment on its relevance to my interests. I won't be 'reviewing', in the somewhat combative sense that that word takes on in academia, but rather trying to give a quick sense of a paper's contents from my perspective. After a while I'll report on the usefulness of the tool as a working aid to my work, and continue or discontinue the experiment, and the blog, as I see appropriate.

Why make this process public? After all, first and foremost this is about my self-improvement as a researcher, and exploring whether the tool works for me and me alone. One motivation is accountability - if the process is public (even if no one much is reading) I'll be ashamed not to keep to my schedule! The blog may also provide some interest to people interested in the tool, and in particular to those who share my corner of logic and theoretical computer science. If that sounds like you, read on!