Instances of computational effects: an algebraic perspective

(Link).

Authors: Sam Staton (University of Cambridge)

Conference: Twenty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2013), June 25-28, 2013, New Orleans, USA.

Journal reference: Proceedings to appear.

Comments: Google Scholar Updates's top recommendation this week was something a bit different - my old PhD supervisor Andrew Pitts has just released the first full book ever published on the relatively new field of nominal sets, titled Nominal Sets: Names and Symmetry in Computer Science. As a recommendation to read it is of course very much in line with my interests, but as a recommendation to write about on this blog within a week's notice it is not so realistic (Google Books offer a preview if you're curious).

Let's turn instead to the second recommendation in my queue, which happens to also stem from Cambridge. In fact it is a sequel to the Staton paper I wrote about four months ago, continuing his development of parameterized algebra. Please refer to my earlier post for a reminder of what that is.

In this paper parameterized algebra is put to work to talk about computational effects. If we think of a computer program as a process that, after some computation, returns a result, a (side) effect refers to things the computer does while that result is being produced. For example, the computer might write something on the screen, or change something in memory. Less obviously, if the program can accept user input this is also a sort of side effect. Whether such events are treated as side effects or as part of the value returned is somewhat flexible, and can differ by programming paradigm or language, but separating computations into the values they calculate and the effects they produce en route is hard to avoid entirely, even in the relatively 'pure' world of functional programming.

A big development in functional programming that allowed effects to be handled more transparently came with Moggi's 1991 paper Notions of computation and monads. Monads are a concept we've encountered a few times on this blog, most extensively here, and essentially give a concise category theoretic way to describe equationally defined, or algebraic, models. Monads are a core concept of category theory because of their relationship to the basic idea of adjunctions, but hardly seem candidates to impact the working practices of your average Haskell programmer. And yet, Moggi and later authors showed that monads are a nice way to 'package up' effects in functional programs to make effectful programs more structured.

The next big milestone in the intellectual history behind this paper is Plotkin and Power's 2002 Notions of computation determine monads, deliberately titled as a sequel to Moggi's classic. This paper essentially dialed the practical issue - effects - back to the original theory - equational definitions - and asked how the monads used to handle effects can be defined equationally. This work was in a sense experimental, as it gave a few examples of how such definitions were both possible and illuminating without building any sort of general theory. Staton to an extent follows this example-driven approach, looking at computational effects that can be thought of as multiple instances of a general concept, such as writing to a specific memory bit being an instance of the general idea of writing to memory. However he moves beyond the examples to argue that the effects in question are correctly captured by his theory of parameterized algebra, which hence provides a syntactic and semantic framework through which many interesting side effects can be defined, categorised, and studied.

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.