Dichotomy 2

This post is a sort of continuation of my previous ramblings about dichotomy theorems.

Recall that Schaefer's Theorem essentially says that every boolean constraint satisfaction problem (CSP) is either in P or NP-Complete. Is there any real content to this? That is, if P is not equal to NP, then is there anything in between? The answer to this question is given by a famous result due to Richard Ladner - if P is not NP, then there is an incomplete set in NP - P. That is, there is a problem which is in NP, but in neither P nor NP-Complete. This result is contained in:

On the Structure of Polynomial Time Reducibility; Richard E. Ladner

A nice follow-up paper, which includes a succint account of two proofs of Ladner's Theorem in an appendix is:

Uniformly Hard Languages; Rod Downey and Lance Fortnow

Actually, Ladner's Theorem says that there would be a dense hierarchy of sets between P and NP. So, somehow Schaefer managed to home in on a large piece of NP that skips out anything in between P and NP, whether there is anything there or not. I previously pointed to some articles that look to extend Schaefer's theroem to broader classes of CSP's by translating everything into universal algebra.

Another approach is given in the following remarkable paper (with an unfortunately long title!):

The Computational Structure of Monotone Monadic SNP and Constraint Satisfiaction: A Study Through Datalog and Group Theory; Tomas Feder and Moshe Vardi

Their approach is to start from Fagin's Theorem, which says that NP is precisely the class of languages expressible in existensial second order logic. By placing increasingly many syntactic restrictions on the language they use, they eventually end up with a logic which does not seem to fall prey to Ladner's Theorem. This logic then turns out to be equivalent to the class of CSP problems, though one direction of the equivalence uses a randomised reduction (it is an enticing open problem to derandomise this).

The article does not really succeed in identifying a large subclass of NP that has a dichotomy theorem. What it does do, however, is to explain the various cases of Schaefer's theorem and why each of them are polynomial, in a manner which facilitates generalisation. What they discovered is that "linear equations mod 2" is polynomial for a very different reason to the other cases. Rather than summarise their results (of which there are many!), I'll just point you to slides for a talk that I gave recently on the topic:

Deeper into Dichotomy: Splitting the Computational Universe; Jon Cohen

I tend to say a lot more in a talk than is on my slides and this talk was no exception. One thing I mentioned that is not on the slides is a neat dichotomy result from combinatorics. Consider the problem of deciding whether it is possible to colour the vertices of a graph with three or fewer colours in such a way that no two adjacent vertices have the same colour (that is, the 3-colourability problem). If you squint a bit, then you'l see that this is the same as asking if there is a homomorphism from the graph you are interested in, to the complete graph on three vertices, K3. To see this, just paint each vertex of K3 with a different colour and remember that there are no self-loops.

So, we have turned the colourability problem into a homomorphism problem. Now, there is nothing wrong with varying the target graph. What you get is the H-colouring problem. If the target graph is a complete graph, then you just get the standard k-colourability problem. It turns out that, depending upon the type of the target graph, we get a dichotomy! That is, if the target graph is bipartite, then the H-Colourability problem is in P, otherwise it is NP-Complete. This result is contained in:

On the Complexity of H-Coloring; P. Hell and J. Nesetril, J. Combin. Theory Ser. B, 48 (1990) pp. 92--110.

Anyway, there is loads of interesting stuff in Feder and Vardi's paper and it is well worth checking out if you are interested in the interaction between logic, complexity theory and group theory!

Typesetting

I am busy writing a longish paper on some proof theoretic mumbo jumbo. As such, I probably won't post much until the blasted thing is finished (writing about logic is not a very efficacious way to have a break from writing about logic :). But, that is not the point of this post.

Typesetting a logic paper, especially a structural proof theory one, can be quite tedious. I am aware of the Latex for Logicians page and am using the bussproofs package for typesetting formal proofs and calculi and such. Later on, I will probably need to typeset some proof nets also. For this, I am thinking of using the XY-Pic package, which I have used in the past for drawing simple diagrams.

Does anyone with experience typesetting this sort of thing have any helpful suggestions? In particular, if you have hacked up some macros or parsers or such that make the job a little easier, I'd be most grateful if you would pass it on! Even some code snippets of good ways to typeset stuff like proof nets would be handy, so that I don't need to reinvent the wheel. Thanks!

Labelled Tableux

Yes, I know that Greg scooped me on this one, but Thomas Sutton has started a blog charting his development of a modal logic theorem prover written in Haskell and based around labelled tableaux. I point you to: Labelled Tableaux.

Labelled what you ask? A tableau is a proof theoretic gadget that looks and feels much like a collection of "uspide down sequent rules". The idea of tableaux is that instead of proving a formula, we show that its negation is inconsistent with the logic. This works especially well in the case of modal logic, since the tableau rules tend to match the frame semantics quite closely. Moreover, if the statement is not a theorem, then we can extract a countermodel from the failed proof search. This is quite dandy! For an introduction to tableau calculi for modal logic, including as much modal logic as is required, see:

Tableau Methods for Modal and Temporal Logic, Rajeev Gore'

(Full disclosure: Raj is one of my PhD supervisors. Of course, I give the article three thumbs up :)

So, what is all this labelling about then? Well, modal proof theory is a tricky thing to get right. In order to avoid nasty things such as infinite looping during proof search, many people have incorporated "labels" into their tableau calculi. This is not so nice from a theoretical point of view, since it obfuscates the essence of the logic and has a very "hacky" feel to it. Of course, if you are actually building a theorem prover, then labels are very handy!

A question that occurs to me is whether anyone has beaten semantic tableaux into providing systems for paraconsistent logics. This is a family of logics where an inconsitency does not necessarily trivialise the theory. Or, alternatively, where both a statement and its negation can be theorems! The basic strategy of attacking the negation of a formula seems, at first glance, to be at odds with this property. I'd be interested in any work that proves me otherwise.

Anyway, I'll be interested to see how the project turns out for Thomas. Maybe he'll let me play around with it when he is done... :)

To Categories!

One hot area of proof theory research is categorical semantics of proofs. For some, this abstraction may seem like needless faffing about. I'll admit that I used to think that myself. I'll try to convey the intuitions that led me to change my mind.

Traditionally, the way in which one obtains an algebraic model of a logic is to pass to the so-called Lindenbaum algebra of the logic. Let's look at that process for classical logic. The first step is to define an equivalence relation on the set of well formed formulas (wff's). If x and y are wff's then define the equivalence relation ~ by saying that x ~ y iff |- x <-> y. Letting [x] denote the equivalence class of x under this relation, we define a partial order on the set of equivalence relations by saying that [x] <= [y] iff x |- y. So we have a poset, which we can turn into a lattice in the obvious way by defining [x]&[y] = [x&y] and [x]v[y] = [x v y]. Why might this not be a good enough semantics for us? Well, the point is that the partial order only records the fact that there is some proof of x |- y -- that is, some deduction from x to y. Thinking topologically for a moment, suppose we have two points in a topological space. Then, the equivalent notion would be to say that there is a path from x to y. But, whether or not all paths are "equivalent" depends on the space!

Recall that given two paths f,g from x to y in some space, f and g are homotopic if they can be continuously deformed into each other. This is not possible if, for example, there is a hole between them. Merely recording the fact that there is a path does not capture this information.

So, one might try to do the same thing for logic. If you try to do it concretely, by defining actual topologies on the logic, then you'll find yourself getting into a bit of a tangle. In fact, I tried to do this for a while, before caving in and doing it via categories. Categories work much smoother!

The idea is that we build a category C whose objects are formulae and whose arrows are "equivalence classes of proofs" between formulae. Defining the equivalence relation in a reasonable manner is a tricky business. Looking a bit closer, take two formulae x and y and consider the set of all proofs from x to y (for the finicky category people out there, there is no real loss in making the category locally small). This is denoted Hom(x,y). If this is nonempty, then we can "look inside" and consider how the equivalence relation works out. One usually does this by proving cut elimination and then looking at cut-free proofs. I'll discuss a logic where this procedure works out in a really cool way from a mathematical standpoint in a later post.

But, why stop there? We may delve deeper into Hom(x,y) and look at procedures for sending one proof to another, just like a homotopy! In the current set up, this means that we would have a bunch of what are called 2-morphisms. These are fella's that send morphisms to morphisms. Sound heady? It's not. What we have done is to form a category whose objects are the sets Hom(x,y) and whose arrows are transformations of proofs. Thinking about this more would take us deep into the waters of n-categories, so I will leave that for another post.

Taking a step back and having a look at what we have done, we see that categorical semantics focus on proofs whereas traditional algebraic semantics focus on "mere" provability. There are some nice theorems that go via category theory to derive models for a logic which are complete in a very strong sense. That is, if two proofs are equivalent, then they are equivalent in every model and if they are not equivalent, then there is some model in which they are not equivalent. These "models" are usually built from some heavy duty mathematical gadgets.

Anyway, for those looking for a good survey of category theory as it applies to logic, check out:

Category theory for linear logicians. R. Blute, P. Scott.

Logic Down Under

The deadline is fast approaching for submissions to this year's Australasian Association for Logic Conference. Paper abstracts need to be in by July 24, with the conference being held September 24 -- 25 in Perth (my home town!). The early deadline is partly because the conference is sponsored by the ASL, with abstracts appearling in the Bulletin of Symbolic Logic. This also means that I need to decide what I want to speak on pretty soon!

This conference immediately precedes the Australian Mathematical Society Annual Conference. Among the special sessions this year are three of interest to the logically minded: Logic, Algebra and Mathematics of Computation. Abstract deadlines for the AustMS meeting are not available yet, but will most likely be late August.

It is a pity that this year's Victorian Algebra Conference has been scheduled to coincide with the AAL conference, so I won't be able to attend both. Monday of this conference does not clash with the AAL though and has the theme of groups and combinatorics, which was lots of fun last year.

However, with the coupling of the AAL and AustMS meetings, it means that the organisers have been able to pursuade some international speakers to come along, including Heinrich Wansing, Michael Zakharyaschev, Andreas Weiermann and Angus MacIntyre.