Quasivarieties and Varieties of Ordered Algebras: Regularity and Exactness

(Link - pdf).

Authors: Alexander Kurz (University of Leicester) and Jiří Velebil (Czech Technical University in Prague).

Reference: Retrieved from Alexander Kurz's homepage, 24 July 2013.

Comments: After last week's paper, which could only have been recommended to me based on my most recent publication, this week's paper seems to hark back to the very first paper I published back in 2005 when I was doing (more or less) pure mathematics for my Masters degree. That paper looked at coalgebra, which I have previously discussed in a post about a paper which shares an author with this one. This week's paper looks at the categorically dual (and perhaps more familiar) notion of algebra.

This paper fits within (or perhaps just to one side of) the mathematical field of universal algebra, which very broadly is the study of mathematics specified by equations. The power of equations is a theme I've come back to a few times on this blog, e.g. here. A class of mathematical structures, called algebras, that are specified by a certain set of equations is called a variety. For example, the class of all groups is a variety. A quasivariety is similar except that it is specified by conditional equations where each equation is conditioned by a list of equations. For example if we wanted to require that a symbol f be interpreted as an injective function then we do this by writing

(fx = fy) implies x=y.

The really interesting results in universal algebra involve describing (quasi)varieties in ways that are apparently unconnected to their definition by (quasi)equational logic. The one I'm most familiar with is Birkhoff's HSP theorem, which characterises (quasi)varieties by certain 'closure' conditions; this paper concerns an alternative characterisation where varieties are interpreted as categories, and we then enquire what structure such a category should possess.

So much for the standard picture; this paper picks up the suggestion of the 1976 paper Varieties of ordered algebras by Bloom which replaces equations, =, by inequations, ≤. That paper gave a Birkhoff-style characterisation of such 'ordered' (quasi)varieties; this paper gives these classes their categorical characterisation. For this to happen we need to relax our idea of what a category is; normal categories have a set of arrows between any two objects, called a hom-set, but the categories of this paper have a partial order on their hom-sets. This is a particular manifestation of a general idea called enriched category theory, where hom-sets can be replaced by objects from (almost) any category.

NOTE: Because of leave my next post will be in a fortnight.

Correspondence between Modal Hilbert Axioms and Sequent Rules with an Application to S5

(Link).

Authors: Björn Lellmann (Imperial College London) and Dirk Pattinson (Imperial College London / Australian National University).

Conference: Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux 2013), Nancy, France, 16-19 September, 2013.

Journal reference: Lecture Notes in Computer Science, to appear.

Comments: This is a paper that Google Scholar Updates surely wouldn't have recommended to me a couple of weeks ago; recall that Updates uses one's papers as 'search terms' to direct its recommendations of new work to you. This paper has little in common with most of my existing papers, but it has clear (albeit somewhat shallow) similarities with my brand new paper 'Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic' (pdf), co-authored with Jeremy Dawson, Rajeev Goré, and Alwen Tiu, which I will be presenting at the conference CSL 2013 in September. I also must note that one of the authors of this paper, Dirk Pattinson, has an office in the same corridor as me at Australian National University; in this new world we apparently need big data algorithms to tell us to read the work of our colleagues next door!

A mathematical proof involves starting with agreed-upon axioms, applying agreed-upon inference rules, and reaching a conclusion; this is a rather basic definition, but leads us to the really important questions for a logician - what axioms? And what inference rules? One broad approach, called Hilbert calculi, require that only an extremely small and fixed set of inference rules be used: in the simplest systems the single rule Modus Ponens alone suffices, although with modal logic, the topic of this week's paper, a couple more are needed. All the action with Hilbert calculi is in their axioms, in the sense that many different logics developed for all sorts of different purposes may have the same inference rule(s) but very different axioms. Hilbert calculi have their charms - they can be a very concise way to present a logic, for example - but they are not much fun to construct actual proofs with, as proofs of even apparently simple tautologies can be lengthy and highly unintuitive.

To get a more structured proof system that helps both humans and machines to generate proofs, the opposite approach tends to be more helpful: more structured proof systems tend to have very few axioms - often the fact that every proposition entails itself is enough - but many inference rules. Such structured proof systems come in various styles, including natural deduction, tableau, and sequent calculus, the topic of this paper, and also of my CSL paper which has surely prompted this recommendation (broadly, these proof systems differ in the style in which the inference rules are designed and organised).

One last piece of preamble is needed before we consider this week's paper; modal logic refers to any logic involving 'modalities' that modify propositions. For example, if 'p' is a statement that might be true or false ("it is raining"), we can preface it with a range of modalities: "it is possible that", "I believe that", "I know that", "in the future it will hold that", and so on. If such modalities have any plausible logical content - e.g. you can form a deductive argument in which "it is possible that" forms an important part - then we can design a modal logic that captures this logical content, via Hilbert axioms, sequent calculus, or whatever other proof style appears most suited.

This paper concerns the translation back and forth between Hilbert calculi axioms and sequent calculi rules for modal logic. The details of this translation are far too involved to summarise adequately in this blog post, but a key wrinkle in the development is to precisely identify certain classes of axioms with certain classes of rules; these classes relate to how many modalities must be piled up on top of one proposition to describe the logic. These distinctions support the 'limitative' results of the final section of the paper, which uses the translation to show that certain modal logics (defined via Hilbert calculi) cannot be captured by certain types of sequent calculus.

A Confluent Pattern Calculus with Hedge Variables

(Link).

Authors: Sandra Alves (University of Porto), Besik Dundua (Porto / Ivane Javakhishvili Tbilisi State University), Mário Florido (Porto), and Temur Kutsia (Johannes Kepler University).

Workshop: 2nd International Workshop on Confluence (IWC 2013), 28 June 2013, Eindhoven, The Netherlands.

Reference: Retrieved from workshop website, 8 July 2013.

Comments: This week's paper is certainly the shortest I've looked at for this blog - no bad thing in a week I've been wrestling with a conference deadline - at just 4 pages plus a half page of references. But this it isn't a formally `published' paper at all, although it has been reviewed; rather, it is a short communication to the specialist workshop IWC 2013, and ideas in here will probably form part of some bigger published paper in the future. Like many such workshops, IWC is a satellite orbiting a bigger event, the International Conference on Rewriting, Deduction, and Programming (RDP 2013), whose main events are two conferences, RTA and TLCA, that do have formally published proceedings (last week's paper hailed from one of those conferences).

The topic of the workshop IWC is confluence. Some computational systems are non-deterministic - at certain points their next steps may not be completely determined, like a Choose Your Own Adventure book. A non-deterministic system is confluent if those 'choices' don't really matter in the end - whenever possible paths diverge, they must always be able to converge again. In a Choose Your Own Adventure book this would imply that there was at most one accessible ending (there could be loops in the book, and hence perhaps no ending at all; confluence says nothing about termination, but rather says you can never make a choice that closes off where you would have gone if you'd made a different choice). In such a book confluence would be a bit of a rip-off, but for a computational system it is highly desirable, because it means the overall behaviour of the system is predictable without going to the trouble of specifying a totally deterministic strategy.

A class of computational systems for which confluence is highly prized are formal calculi, among which the λ (lambda) calculus is king. Here computation is expressed as the simplification, or reduction, of a term, and confluence corresponds to the notion that it doesn't matter which part of the term you choose to reduce first. While the λ-calculus is powerful enough to model any and all computations, there is good reason why most programmers use languages with many more built-in commands - just because you can use the λ-calculus for something like complex data structures doesn't mean it's easy to do so, so ready-to-hand support for them is to be desired. However even with such 'higher' commands the λ-calculus comes in useful, as by bolting them directly on to the basic calculus we can study their behaviour, including how they effect confluence.

One such 'extension' to the λ-calculus known to cause problems with confluence is pattern matching, the process of comparing a term with some pattern, attempting to unify them (as discussed last week), then proceeding to compute using that unification somehow. I'm being intentionally vague here - there are many notions of pattern matching, differing for example in their choice of what constitutes a 'pattern', and a whole host of them have been added to the λ-calculus. The most important reference for this work is the dynamic pattern λ-calculus of Cirstea and Faure, itself an attempt to unify various other calculi with similar intent. This workshop paper extends the dynamic pattern λ-calculus with hedge variables, which instead of being substituted for by terms, may be substituted for by lists of terms, and discusses how such a calculus can be constrained to get the desired confluence property.

Unifying Nominal Unification

(Link).

Author: Christophe Calvès (Université de Lorraine, Centre National de la Recherche Scientifique)

Conference: 24th International Conference on Rewriting Techniques and Applications (RTA 2013), 24-26 June, 2013, Eindhoven, The Netherlands.

Journal reference: Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, Femke van Raamsdonk (Ed.), pp 143-157 (2013).

Comments: Many algorithms in computer science involve some sort of pattern matching which involves, at its most abstract level, working out whether two different terms can be forced to be equal by an appropriate choice of substitutions of their variables. This process is called unification and is best understood by simple examples - given the terms f(c,x) and f(y,d), where f is a binary function, x and y are variables, and c and d are constants that may not vary, we can unify them by mapping x to c and y to d, to get the new term f(c,d). On the other hand the terms f(x,x) and f(c,d) cannot be unified - there is nothing we can substitute for x that will make the terms equal.

In its simplest form, as in the examples above, unification is frequently useful but basically trivial - unifiers (more precisely the best, or 'most general' unifiers) can be computed in linear time. One way to make the problem harder is to relax the definition of equal from 'literally equal' to 'equal with respect to some equational theory', which creates a unification problem that is in general undecidable - working out whether f(x,x) and f(c,d) are unifiable now necessitates determining if there exists any term t such that f(t,t) and f(c,d) are provably equal, which involves a possibly infinite search through all possible terms t, not to mention the difficulty of proving the equality holds when a candidate term t is found.

Another way that unification can become more difficult is to enrich the syntax that is used to define terms - here, we consider variable binding, a frequent concern of my research, and this blog. Conceptually, this is not too different from the 'equational unification' of the paragraph above - terms can be considered equal despite being not literally equal, in this case because they differ only uniformly in their bound names. Fortunately the equality theory of binding is not difficult enough to lead to uncomputability: so-called nominal unification was proved to be decidable in at least exponential time in the original 2003 paper of that name by Urban, Pitts and Gabbay. Exponential time algorithms are rather slow so are of limited practical use; the picture was improved in 2008 by Levy and Villaret who gave a quadratic time algorithm for nominal unification, based on a detour via 'higher-order' syntax. Calvès, this week's author, in 2011 published a paper with Fernández presenting a different quadratic time algorithm, based on a detour via first-order syntax. The point of this paper is to show that, despite the differences between the approaches of Levy-Villaret and Calvès-Fernández, the algorithms are in a certain sense mathematically identical; both rely implicitly on a concept Calvès calls nominal modalities.