Sunday, January 22, 2006
How much damage can be caused by a peer reviewer having a bad day?
Check out this cool article! You will find some hilarious reviews for award-winning papers authored by Dijkstra, Codd, Shannon, etc.
Saturday, January 21, 2006
Almost sure theory
We all know that the Hilbert's Enstceidungsproblem, i.e. deciding whether a first-order sentence is true, is undecidable. Church, Turing, and others proved it. Recall that first-order logic admits the 0-1 law, i.e., every FO sentence is almost surely true (AST) or almost surely false (ASF). So, what about the problem of deciding whether an FO sentence be AST? It turns out that this is decidable. I shall outline some important ideas for proving this statement.
Let us restrict ourselves to graphs as before. In proving that FO admits the 0-1 law, we mentioned the extension axioms EA = {Pk}k ∈ N, where N is the set of all natural numbers. Extension axioms are nothing more than graph properties. In our case, Pks are FO-expressible. Although for the purpose of this post we need not understand what our extension axioms are, I will just define it for future reference:
∀x1, ..., x2k( ∧i ≠ j xi &ne xj ->
∃z( ∧1 ≤ i ≤ 2k z ≠ xi
∧i ≤ k E(z,xi)
∧i > k ¬E(z,xi)))
Recall that a theory T is a set of sentences. A model of T is a structure that satisfies all sentences of T. The theory T is consistent if it has a model, and it is complete iff for each sentence f (of the same vocabulary), we have either T |= f, i.e. every model of T is a model of f, or T |= ¬ f. A consistent and complete theory T is decidable if it is possible to decide whether T |= f, for any given sentence f.
Theorem: EA is consistent (and has a unique countable model), complete, and decidable
We will not prove the first two statements, as we will need more model theory (see Libkin's "Elements of Finite Model Theory" for more details). To prove that EA is decidable, we need only invoke an old result from recursive theory that every recursively axiomatizable theory is decidable. The above definition of Pk gives us a recursive enumeration of the axioms.
The unique countable model for EA, denoted RG, is called the random graph, as its probabilistic construction is often emphasized in the literature. Using the above theorem, we derive an easy corollary:
Corollary: For any FO sentence f, RG |= f iff μ(f) = 1.
With these results, it is a breeze to conclude that deciding whether an FO sentence be AST is computable. To determine the exact complexity of the problem, one needs a more hairy analysis, which we will not do here. It turns out that the problem is PSPACE-complete, the proof of which can be found in
E. Granjean. Complexity of the first-order theory of almost all finite structures, Information and Control, Volume 57, 1983.
Recent work in this area mostly deals with determining fragments of second-order logic that admits the 0-1 law, and whether the almost sure theory with respect to the fragment be decidable. [It is easy to see that SO in its full power does not admit the 0-1 law.] This, however, lies outside the scope of our current discussion.
Let us restrict ourselves to graphs as before. In proving that FO admits the 0-1 law, we mentioned the extension axioms EA = {Pk}k ∈ N, where N is the set of all natural numbers. Extension axioms are nothing more than graph properties. In our case, Pks are FO-expressible. Although for the purpose of this post we need not understand what our extension axioms are, I will just define it for future reference:
∀x1, ..., x2k( ∧i ≠ j xi &ne xj ->
∃z( ∧1 ≤ i ≤ 2k z ≠ xi
∧i ≤ k E(z,xi)
∧i > k ¬E(z,xi)))
Recall that a theory T is a set of sentences. A model of T is a structure that satisfies all sentences of T. The theory T is consistent if it has a model, and it is complete iff for each sentence f (of the same vocabulary), we have either T |= f, i.e. every model of T is a model of f, or T |= ¬ f. A consistent and complete theory T is decidable if it is possible to decide whether T |= f, for any given sentence f.
Theorem: EA is consistent (and has a unique countable model), complete, and decidable
We will not prove the first two statements, as we will need more model theory (see Libkin's "Elements of Finite Model Theory" for more details). To prove that EA is decidable, we need only invoke an old result from recursive theory that every recursively axiomatizable theory is decidable. The above definition of Pk gives us a recursive enumeration of the axioms.
The unique countable model for EA, denoted RG, is called the random graph, as its probabilistic construction is often emphasized in the literature. Using the above theorem, we derive an easy corollary:
Corollary: For any FO sentence f, RG |= f iff μ(f) = 1.
With these results, it is a breeze to conclude that deciding whether an FO sentence be AST is computable. To determine the exact complexity of the problem, one needs a more hairy analysis, which we will not do here. It turns out that the problem is PSPACE-complete, the proof of which can be found in
E. Granjean. Complexity of the first-order theory of almost all finite structures, Information and Control, Volume 57, 1983.
Recent work in this area mostly deals with determining fragments of second-order logic that admits the 0-1 law, and whether the almost sure theory with respect to the fragment be decidable. [It is easy to see that SO in its full power does not admit the 0-1 law.] This, however, lies outside the scope of our current discussion.
Saturday, January 07, 2006
The 0-1 Law
To start off the year 2006, I want to talk about the 0-1 law, which is an extremely important and elegant topic in finite model theory. A logic L (over a fixed vocabulary σ) is said to admit the 0-1 law if, for any sentence f of L, the fraction of σ-structures with universe {0,...,n-1} that satisfy the sentence f converges to either 0 or 1 as n approaches infinity. We denote this fraction by μn(f) and the limit, if exists, by μ(f). [Of course, this means that μ and μn ranges between 0 and 1.] In other words, every sentence f is almost surely false or almost surely true. For simplicity, let us restrict our attention to undirected loopless graphs, i.e., σ contains only one binary relation E which is both symmetric and irreflexive. Below is perhaps the most fundamental theorem about the 0-1 law.
Theorem (Fagin 1976, Glebskii et al. 1969): First-order logic admits the 0-1 law
Most finite model theorists equate the admission of 0-1 law with the inability to do "counting". Consider the following properties EVEN = { G : G has even number of vertices }. We see that μn(EVEN) = 1 iff n is even, and hence μ(EVEN) does not exist. I am yet to see a property whose asymptotic probability μ converges to something other than 0 or 1, or diverges, but has nothing to do with counting. Consider the following properties:
On the other hand, if you admit constant or function symbols, it is possible to have first-order properties whose asymptotic probability converges to something other than 0 or 1. So, it is crucial to assume that our vocabulary σ be purely relational.
What is the use of 0-1 law in finite model theory apart from the amusement of some theoreticians? [I will have to confess many proofs about the 0-1 law, including Fagin's proof of the above theorem, are usually of great beauty.] Well, a primary concern of finite model theory is to determine how expressive a logic is over a given class of finite structures. By proving that a logic admits the 0-1 law, we show that any property whose asymptotic probability does not converge to either 0 or 1 is not expressible in the logic. For example, an immediate corollary of the above theorem is that first-order logic cannot express EVEN.
Let me briefly outline the proof ideas of the above theorem which recurs in 0-1 law proofs. We only need to show that, for each natural number k, there exists a property Pk of graphs such that
Why is this sufficient? Let f be a first-order sentence of quantifier rank k. There are two cases. First, there exists a model of Pk that is also a model of f. In this case, it is not hard to show that any model of Pk is also a model of f, which implies that μ(f) ≥ μ(Pk) = 1. The second case is that all models of Pk are not models of f, i.e., they are models of "not f". Therefore, μ("not f") ≥ μ(Pk) = 1. That is, we have μ(f) = 0.
The property Pk is commonly referred to as an extension axiom. Note that Pk does not have to be L-definable (where L is the logic that is to admit 0-1 law).
Two excellent expositions of the basics of 0-1 laws include Leonid Libkin's Elements of Finite Model Theory chapter 12, and James Lynch DIMACS 1995-1996 Tutorial notes on "Random Finite Models".
Theorem (Fagin 1976, Glebskii et al. 1969): First-order logic admits the 0-1 law
Most finite model theorists equate the admission of 0-1 law with the inability to do "counting". Consider the following properties EVEN = { G : G has even number of vertices }. We see that μn(EVEN) = 1 iff n is even, and hence μ(EVEN) does not exist. I am yet to see a property whose asymptotic probability μ converges to something other than 0 or 1, or diverges, but has nothing to do with counting. Consider the following properties:
- μ(BIPARTITE) = 0
- μ(HAMILTONIAN) = 1
- μ(CONNECTED) = 1
- μ(TREE) = 0
On the other hand, if you admit constant or function symbols, it is possible to have first-order properties whose asymptotic probability converges to something other than 0 or 1. So, it is crucial to assume that our vocabulary σ be purely relational.
What is the use of 0-1 law in finite model theory apart from the amusement of some theoreticians? [I will have to confess many proofs about the 0-1 law, including Fagin's proof of the above theorem, are usually of great beauty.] Well, a primary concern of finite model theory is to determine how expressive a logic is over a given class of finite structures. By proving that a logic admits the 0-1 law, we show that any property whose asymptotic probability does not converge to either 0 or 1 is not expressible in the logic. For example, an immediate corollary of the above theorem is that first-order logic cannot express EVEN.
Let me briefly outline the proof ideas of the above theorem which recurs in 0-1 law proofs. We only need to show that, for each natural number k, there exists a property Pk of graphs such that
- μ(Pk) = 1, and
- Any two models of Pk cannot be distinguished by a first-order sentence of quantifier rank k. [Recall that the quantifier rank of a first-order sentence is the maximum depth of any nesting of quantifiers of the sentence.]
Why is this sufficient? Let f be a first-order sentence of quantifier rank k. There are two cases. First, there exists a model of Pk that is also a model of f. In this case, it is not hard to show that any model of Pk is also a model of f, which implies that μ(f) ≥ μ(Pk) = 1. The second case is that all models of Pk are not models of f, i.e., they are models of "not f". Therefore, μ("not f") ≥ μ(Pk) = 1. That is, we have μ(f) = 0.
The property Pk is commonly referred to as an extension axiom. Note that Pk does not have to be L-definable (where L is the logic that is to admit 0-1 law).
Two excellent expositions of the basics of 0-1 laws include Leonid Libkin's Elements of Finite Model Theory chapter 12, and James Lynch DIMACS 1995-1996 Tutorial notes on "Random Finite Models".
Starting the year 2006
Sorry for having been silent for quite a while. This winter "break" turned out to be quite a busy one for me, with quite a bit of homework and research to do. Anyway, belated happy new year! I hope that this will be a great and productive year for all of us.
I just resumed reading the lattest on the blogsphere, with still quite a bit of catching up to do. For now, I will mention mention a couple of noteworthy things that happened:
I just resumed reading the lattest on the blogsphere, with still quite a bit of catching up to do. For now, I will mention mention a couple of noteworthy things that happened:
- Kenny Easwaran wrote an introductory article on "forcing", a well-known technique in set theory for proving independence results. I will write more on it when I finish reading the article.
- Igor Naverniouk, a PhD student from University of Toronto, just started a new blog on True Artificial Intelligence. The first couple of entries look quite interesting.
Monday, December 19, 2005
Immerman's descriptive complexity survey
The most recent issue of SIGACT Newsletter (vol. 36, number 4) contains a guest column concerning progress in descriptive complexity by Neil Immerman. [Thanks to Kurt for making me aware of this article.] The article concisely surveys some recent progress in finite model theory with an emphasis on descriptive complexity. The style is extremely informal, and I believe is a perfect weekend read. I highly recommend the article to anybody interested in logic or computational complexity.
Let me say a little bit about the content of the article (no spoiler!). It starts by motivating the study of descriptive complexity. Then, it moves on to the spectrum problem and Fagin's theorem (that NP = existential second-order logic), which marked the beginning of descriptive complexity. We then see some other capturing results in descriptive complexity (e.g. characterizations of P, PSPACE, etc.). My favorite capturing result mentioned here is DSPACE[nv] = VAR[v+1], where VAR[k] denotes the set of problems expressible by a sequence of first-order sentences using at most k variables. And so forth ... but let me mention another interesting thing written in the article. We notice that most of the capturing results use a linear ordering on the universe. [In fact, a linear ordering is necessary for these results to work.] For example, Immerman-Vardi theorem says that FO(LFP) captures PTIME over the class of ordered structures. However, FO(LFP) does not capture PTIME over the class of all structures. In fact, a long-standing open problem in finite model theory is whether there exists a logic capturing order-independent PTIME problems. The article nicely surveys our progress towards resolving this problem. Another interesting thing that you will get to know a bit about is the phenomenon that one logic may be exponentially more "succinct" than another logic with the same expressive power.
A fair question to ask now is to what extent has descriptive complexity has helped us to answer structural complexity questions such as separating two complexity classes. Let me try to provide some answers to this question. I believe that the first switching lemma, which separates AC0 from LOGSPACE, was proved by Miklos Ajtai using finite model theory. This result was independently discovered by Saxe, Sipser, and Furst around the same time using combinatorics. Most people, even finite model theorists, think that the combinatorial proof provided by Saxe et al. is easier to understand than Ajtai's proof. [Of course, we now have Hastad's switching lemma with some elegant proofs.] Next I will mention Immerman-Szelepscenyi theorem that NSPACE(f(n)) is closed under complementation. Immerman proved this by appealing to descriptive complexity, while Szelepscenyi by using some elementary combinatorics. In this sense, a skeptic might say that descriptive complexity has not really helped structural complexity theory. But, what has? Nothing much really, with expander graphs as one only exception (recall Reingold's recently proved theorem that L = SL). On the other hand, I believe that descriptive complexity helps us understand computational complexity. Many problems or classes in complexity theory have simple and elegant correspondence in descriptive complexity theory. In fact, some logical characterizations of complexity classes are commonly used by computational complexity theorists (e.g. logical characterizations of each level in the poly-time hierarchy). In this sense, I am positive that one day somebody who understands computational complexity, with some help from descriptive complexity, will resolve some of the most tantalizing open problems in structural complexity.
Let me say a little bit about the content of the article (no spoiler!). It starts by motivating the study of descriptive complexity. Then, it moves on to the spectrum problem and Fagin's theorem (that NP = existential second-order logic), which marked the beginning of descriptive complexity. We then see some other capturing results in descriptive complexity (e.g. characterizations of P, PSPACE, etc.). My favorite capturing result mentioned here is DSPACE[nv] = VAR[v+1], where VAR[k] denotes the set of problems expressible by a sequence of first-order sentences using at most k variables. And so forth ... but let me mention another interesting thing written in the article. We notice that most of the capturing results use a linear ordering on the universe. [In fact, a linear ordering is necessary for these results to work.] For example, Immerman-Vardi theorem says that FO(LFP) captures PTIME over the class of ordered structures. However, FO(LFP) does not capture PTIME over the class of all structures. In fact, a long-standing open problem in finite model theory is whether there exists a logic capturing order-independent PTIME problems. The article nicely surveys our progress towards resolving this problem. Another interesting thing that you will get to know a bit about is the phenomenon that one logic may be exponentially more "succinct" than another logic with the same expressive power.
A fair question to ask now is to what extent has descriptive complexity has helped us to answer structural complexity questions such as separating two complexity classes. Let me try to provide some answers to this question. I believe that the first switching lemma, which separates AC0 from LOGSPACE, was proved by Miklos Ajtai using finite model theory. This result was independently discovered by Saxe, Sipser, and Furst around the same time using combinatorics. Most people, even finite model theorists, think that the combinatorial proof provided by Saxe et al. is easier to understand than Ajtai's proof. [Of course, we now have Hastad's switching lemma with some elegant proofs.] Next I will mention Immerman-Szelepscenyi theorem that NSPACE(f(n)) is closed under complementation. Immerman proved this by appealing to descriptive complexity, while Szelepscenyi by using some elementary combinatorics. In this sense, a skeptic might say that descriptive complexity has not really helped structural complexity theory. But, what has? Nothing much really, with expander graphs as one only exception (recall Reingold's recently proved theorem that L = SL). On the other hand, I believe that descriptive complexity helps us understand computational complexity. Many problems or classes in complexity theory have simple and elegant correspondence in descriptive complexity theory. In fact, some logical characterizations of complexity classes are commonly used by computational complexity theorists (e.g. logical characterizations of each level in the poly-time hierarchy). In this sense, I am positive that one day somebody who understands computational complexity, with some help from descriptive complexity, will resolve some of the most tantalizing open problems in structural complexity.
Subscribe to:
Posts (Atom)