After 30 years of bad luck, Australia has finally qualified for next year's World Cup in Germany after beating Uruguay in a dramatic penalty shoot-out at Sydney's Telstra Stadium, Australia.
Sunday, November 27, 2005
Australia qualified for the World Cup 2006 in Germany
After 30 years of bad luck, Australia has finally qualified for next year's World Cup in Germany after beating Uruguay in a dramatic penalty shoot-out at Sydney's Telstra Stadium, Australia.
Sunday, November 20, 2005
XML = Automata + Logic + Database
What do you get when you mix automata theory, mathematical logic, and database theory in a big bowl, and stir it vigorously? The answer is foundations of XML. In the past 7 - 8 years, the study of XML has generated a large number of elegant and unexpected connections between the three aforementioned areas. How so? Answer: we can view XML documents as labeled unranked trees, and we have numerous formalisms in (tree) automata theory and mathematical logic for querying and manipulating tree-like structures.
I presume you all know a little bit about HTML. XML is just like HTML but you have to define your own tags (e.g. <tag> ... </tag>). According to W3C XML tutorial, unlike HTML, whose primary goal is to display data focusing on how it looks, XML was designed to describe data and to focus on what data is. Well, then, what can you use XML for? Primarily, for information exchange on the web. In fact, one of the greatest promises of XML is to serve as the lingua franca in information exchange. Without further ado, let's look at an example of XML documents:
One can view this document as a labeled unranked tree:
When we study foundations of XML, we care only about the structure of the tree. Consequently, we omitted the texts within the innermost tags. By definition, this tree is different from the tree that you get from exchanging the two children of "books". That is, a sibling ordering is assumed. Also, note that a node in an XML tree may have an arbitrarily large number of children. This is why the tree is said to be unranked.
We are interested in both procedural formalisms (i.e. automata) and logical formalisms (i.e. logical languages) for querying unranked trees. The intention is that we express the query in a logical language, which will then be converted to an automaton that one can run to compute the query against the XML document.
Of course, we should ask why we want to have query languages in the first place. Some answers are:
For validation, the yardstick logic is monadic second-order logic (MSO). This is because MSO is essentially equivalent to XSD (XML Schema Definition) which people use for validation in practice. For navigation, the yardstick logic is first-order logic (FO). This is because FO and its fragments is closely connected to XPath, a practical XML navigational language which people use.
What kind of procedural formalisms do we have for validation and navigation? For validation, we have what we call nondeterministic unranked tree automaton (NUTA). Its connection to MSO is very tight:
Theorem: A set of unranked trees (over a fixed finite set of labels) is recognizable by a NUTA iff it is definable in MSO.
What about navigation? This is still open.
Another research direction in foundations of XML concerns finding logics, which are equivalent to the yardstick logics, whose model-checking/query evaluation is polynomial in the size of the formula and tree. It is known that both MSO and FO have horrible complexity for model-checking over trees. Research in this direction often requires one to use some kinds of modal logics. For example, we know that CTL* (Computational Tree Logic*) with past operator, which researchers in model-checking community love, is equivalent to FO over unranked trees. There are also other research directions with a plethora of interesting open problems (such as streaming XML documents). If the reader is interested, I will further elaborate on foundations of XML.
I presume you all know a little bit about HTML. XML is just like HTML but you have to define your own tags (e.g. <tag> ... </tag>). According to W3C XML tutorial, unlike HTML, whose primary goal is to display data focusing on how it looks, XML was designed to describe data and to focus on what data is. Well, then, what can you use XML for? Primarily, for information exchange on the web. In fact, one of the greatest promises of XML is to serve as the lingua franca in information exchange. Without further ado, let's look at an example of XML documents:
<books>
<book>
<title>Elements of Finite Model Theory</title>
<author>Leonid Libkin</author>
<year>2004</year>
<publisher>Springer</publisher>
<rank>5/5</rank>
</book>
<book>
<title>Animal Farm</title>
<author>George Orwell</author>
<year>2003</year>
<publisher>Penguin Books</publisher>
</book>
</books>
One can view this document as a labeled unranked tree:
When we study foundations of XML, we care only about the structure of the tree. Consequently, we omitted the texts within the innermost tags. By definition, this tree is different from the tree that you get from exchanging the two children of "books". That is, a sibling ordering is assumed. Also, note that a node in an XML tree may have an arbitrarily large number of children. This is why the tree is said to be unranked.
We are interested in both procedural formalisms (i.e. automata) and logical formalisms (i.e. logical languages) for querying unranked trees. The intention is that we express the query in a logical language, which will then be converted to an automaton that one can run to compute the query against the XML document.
Of course, we should ask why we want to have query languages in the first place. Some answers are:
- Validation - we wish to distinguish XML documents that make sense and those that don't. A common example arises when two parties want to exchange some information using XML documents. They of course have to agree on the formatting of the documents that they accept. Elaborating on the example above, one may insist that "books" have zero or more children with tags "book", each of which must have four children with tags (in order) "title", "author", "year", and "publisher", and one optional child with tags "rank".
- Navigation. For example, one may want to ask for all nodes in the document that are tagged "book" and have a child tagged "rank".
For validation, the yardstick logic is monadic second-order logic (MSO). This is because MSO is essentially equivalent to XSD (XML Schema Definition) which people use for validation in practice. For navigation, the yardstick logic is first-order logic (FO). This is because FO and its fragments is closely connected to XPath, a practical XML navigational language which people use.
What kind of procedural formalisms do we have for validation and navigation? For validation, we have what we call nondeterministic unranked tree automaton (NUTA). Its connection to MSO is very tight:
Theorem: A set of unranked trees (over a fixed finite set of labels) is recognizable by a NUTA iff it is definable in MSO.
What about navigation? This is still open.
Another research direction in foundations of XML concerns finding logics, which are equivalent to the yardstick logics, whose model-checking/query evaluation is polynomial in the size of the formula and tree. It is known that both MSO and FO have horrible complexity for model-checking over trees. Research in this direction often requires one to use some kinds of modal logics. For example, we know that CTL* (Computational Tree Logic*) with past operator, which researchers in model-checking community love, is equivalent to FO over unranked trees. There are also other research directions with a plethora of interesting open problems (such as streaming XML documents). If the reader is interested, I will further elaborate on foundations of XML.
Saturday, November 12, 2005
Upcoming theory talk at UofT
For those of you in Toronto, you might want to stop by at UofT next Friday for a talk on P vs. NP. Here is the description:
Title: Can the P vs NP question be independent of the axioms of mathematical reasoning?
Speaker: Shai Ben-David, University of Waterloo
Venue: Galbraith Bld, Rm. 248
Time: 18 November, 11.10 AM
Abstract:
I'll discuss the possibility that the failure to resolve basic complexity theoretic statements stems from these statements being independent of the logical theories that underly our mathematical reasoning. In the first part of the talk, I shall briefly survey independence (from the axioms of set theory) of questions in various areas of mathematics. I shall then go on to discuss independence results that seem relevant to the P vs NP question. Finally, I shall outline some results of myself and Shai Halevi that imply that, as far as current proof techniques for such questions go, the task of proving that P vs NP is independent of Peano Arithmetic is as hard as proving very strong upper bounds on the (deterministic) complexity of the SAT problem.
Title: Can the P vs NP question be independent of the axioms of mathematical reasoning?
Speaker: Shai Ben-David, University of Waterloo
Venue: Galbraith Bld, Rm. 248
Time: 18 November, 11.10 AM
Abstract:
I'll discuss the possibility that the failure to resolve basic complexity theoretic statements stems from these statements being independent of the logical theories that underly our mathematical reasoning. In the first part of the talk, I shall briefly survey independence (from the axioms of set theory) of questions in various areas of mathematics. I shall then go on to discuss independence results that seem relevant to the P vs NP question. Finally, I shall outline some results of myself and Shai Halevi that imply that, as far as current proof techniques for such questions go, the task of proving that P vs NP is independent of Peano Arithmetic is as hard as proving very strong upper bounds on the (deterministic) complexity of the SAT problem.
Monday, November 07, 2005
Favorite Logic of November 2005: Second-Order Logic
Last month we talked about monadic second-order logic (MSO). We now shall proceed to a more expressive logic: second-order logic (SO) and some of its fragments, such as existential second-order logic (ESO) and universal second-order logic (ASO). In fact, some of the most tantalizing open questions in complexity theory can be reduced to questions about the expressive power of the afore-mentioned logics. More precisely, ESO equals NP, whereas ASO equals coNP. Hence, to separate P from NP, it is sufficient to prove that ASO and ESO have different expressive power. Since we have numerous tools for proving inexpressibility results in finite model theory, it is natural to ask whether it is possible to separate NP from coNP using finite model theory. This, as you would have expected, is still open. However, we have managed to prove a weaker version: that Monadic NP is different from Monadic coNP.
So, what exactly is SO? MSO permits quantifications over sets (i.e. unary relations). SO is just a generalization of this idea: you are allowed to quantify over k-ary relations. So, formulas in SO will look like
ψ := Q1X1...QmXm φ
where Q ∈ {∃,∀}, Xi is a ki-ary "second-order variable" to be interpreted as a ki-ary relation, and φ is just a first-order (FO) formula that talks about these second-order variables as well as some relations in the given vocabulary. An example of a sentence in this logic has been given in here, in which case all second-order variables are unary. Another example that uses non-unary relations is hamiltonianicity:
∃ L ∃ S ( (L is a strict linear ordering over the vertices) and (S is L's successor relation) and ∀ x ∀ y( S(x,y) -> E(x,y) ) )
A graph is hamiltonian iff there exists a path that visits every vertex in the graph. You can think of L as the transitive closure of the path P that witnesses the hamiltonianicity of the graph, and of S as the path P. [Example: a strict linear ordering on {1,2,3} is the binary relation ≤ = {(1,2),(1,3),(2,3)}, while its successor relation is the binary relation {(1,2),(2,3)}. Perhaps, it is more descriptive to say "immediate successor" than just "successor".] Notice that in these two examples we only used ∃ quantifiers for the second-order variables. We use ESO (read: existential second-order logic) to denote all formulas in SO of this kind, i.e., where all the Qi is ∃. We use ASO (read: universal second-order logic) to denote formulas in SO where Qi equals ∀.
Theorem (Fagin 1974): ESO captures NP. ASO captures coNP.
The notion of "capture" here has been defined in a previous post. The examples above give two concrete NP properties (hamiltonianicity, and 3-colorability) that you can express in ESO. How do you express non-hamiltonianicity in ASO? It's simple: just negate the formula above and use the fact that "not ∃ Xi ψ" is equivalent to "∃ Xi not &psi". This can easily be generalized to other coNP properties. Let's summarize the results.
Theorem: NP = coNP iff ESO = ASO iff 3-colorability is expressible in ASO.
What complexity class does SO correspond to?
Theorem (Stockmeyer 1977) SO captures PH.
Actually, Stockmeyer proved a much stronger result relating the kth level in the hierarchy to an SO fragment that contains formulas with k second-order quantifier alternation.
Of course, we have not been successful in proving that ESO != ASO. However, a weaker version has been proven in the literature.
Theorem (Fagin 1975) Monadic NP is different from Monadic coNP.
By monadic NP, we mean ESO formulas all of whose second-order variables are unary. The same goes for monadic coNP. So, monadic NP is just existential monadic second-order logic (EMSO), while monadic coNP is universal MSO (AMSO). The separation query given in Fagin's proof was "graph connectivity"; it is expressible in AMSO, but not in EMSO. A simplified version of this proof has been given in a paper by Ajtai, Fagin, and Stockmeyer (AFS) in 1995. [Correction: the paper is by Fagin, Stockmeyer, and Vardi (FSV) instead. Thanks to Ron Fagin for pointing this out.] In my opinion, this is also the most beatiful proof I have ever seen in finite model theory: simple, but extremely powerful. In a nutshell, this proof cleverly employs hanf-locality (which I have discussed here) which gives us a way of easily providing a winning strategy in "Ehrenfeucht-Fraisse games", which can be used to prove inexpressibility results. Is it possible to generalize the proof technique to ESO? Unfortunately no: Hanf-locality is not useful as soon as we permit binary second-order variables. On the other hand, we still have Ehrenfeucht-Fraisse games, which are in general hard to play. So, FSV proposed the following project: develop tools to easily establish a winning strategy in Ehrenfeucht-Fraisse games! Thus far, most tools of this kind uses some notions of locality, which is only useful for "sparse" structures. I hope that a more powerful tool can be discovered some time in the near future to prove a separation of ESO from ASO, although it seems that we are far from it.
The best way to learn AFS techniques for separating NP and coNP is to read Ron Fagin's
Easier ways to win logical games, DIMACS 1997
It is available from his website. A more complete reference is Leonid Libkin's excellent textbook titled Elements of Finite Model Theory (see chapter (3,4, and) 7).
So, what exactly is SO? MSO permits quantifications over sets (i.e. unary relations). SO is just a generalization of this idea: you are allowed to quantify over k-ary relations. So, formulas in SO will look like
ψ := Q1X1...QmXm φ
where Q ∈ {∃,∀}, Xi is a ki-ary "second-order variable" to be interpreted as a ki-ary relation, and φ is just a first-order (FO) formula that talks about these second-order variables as well as some relations in the given vocabulary. An example of a sentence in this logic has been given in here, in which case all second-order variables are unary. Another example that uses non-unary relations is hamiltonianicity:
∃ L ∃ S ( (L is a strict linear ordering over the vertices) and (S is L's successor relation) and ∀ x ∀ y( S(x,y) -> E(x,y) ) )
A graph is hamiltonian iff there exists a path that visits every vertex in the graph. You can think of L as the transitive closure of the path P that witnesses the hamiltonianicity of the graph, and of S as the path P. [Example: a strict linear ordering on {1,2,3} is the binary relation ≤ = {(1,2),(1,3),(2,3)}, while its successor relation is the binary relation {(1,2),(2,3)}. Perhaps, it is more descriptive to say "immediate successor" than just "successor".] Notice that in these two examples we only used ∃ quantifiers for the second-order variables. We use ESO (read: existential second-order logic) to denote all formulas in SO of this kind, i.e., where all the Qi is ∃. We use ASO (read: universal second-order logic) to denote formulas in SO where Qi equals ∀.
Theorem (Fagin 1974): ESO captures NP. ASO captures coNP.
The notion of "capture" here has been defined in a previous post. The examples above give two concrete NP properties (hamiltonianicity, and 3-colorability) that you can express in ESO. How do you express non-hamiltonianicity in ASO? It's simple: just negate the formula above and use the fact that "not ∃ Xi ψ" is equivalent to "∃ Xi not &psi". This can easily be generalized to other coNP properties. Let's summarize the results.
Theorem: NP = coNP iff ESO = ASO iff 3-colorability is expressible in ASO.
What complexity class does SO correspond to?
Theorem (Stockmeyer 1977) SO captures PH.
Actually, Stockmeyer proved a much stronger result relating the kth level in the hierarchy to an SO fragment that contains formulas with k second-order quantifier alternation.
Of course, we have not been successful in proving that ESO != ASO. However, a weaker version has been proven in the literature.
Theorem (Fagin 1975) Monadic NP is different from Monadic coNP.
By monadic NP, we mean ESO formulas all of whose second-order variables are unary. The same goes for monadic coNP. So, monadic NP is just existential monadic second-order logic (EMSO), while monadic coNP is universal MSO (AMSO). The separation query given in Fagin's proof was "graph connectivity"; it is expressible in AMSO, but not in EMSO. A simplified version of this proof has been given in a paper by Ajtai, Fagin, and Stockmeyer (AFS) in 1995. [Correction: the paper is by Fagin, Stockmeyer, and Vardi (FSV) instead. Thanks to Ron Fagin for pointing this out.] In my opinion, this is also the most beatiful proof I have ever seen in finite model theory: simple, but extremely powerful. In a nutshell, this proof cleverly employs hanf-locality (which I have discussed here) which gives us a way of easily providing a winning strategy in "Ehrenfeucht-Fraisse games", which can be used to prove inexpressibility results. Is it possible to generalize the proof technique to ESO? Unfortunately no: Hanf-locality is not useful as soon as we permit binary second-order variables. On the other hand, we still have Ehrenfeucht-Fraisse games, which are in general hard to play. So, FSV proposed the following project: develop tools to easily establish a winning strategy in Ehrenfeucht-Fraisse games! Thus far, most tools of this kind uses some notions of locality, which is only useful for "sparse" structures. I hope that a more powerful tool can be discovered some time in the near future to prove a separation of ESO from ASO, although it seems that we are far from it.
The best way to learn AFS techniques for separating NP and coNP is to read Ron Fagin's
Easier ways to win logical games, DIMACS 1997
It is available from his website. A more complete reference is Leonid Libkin's excellent textbook titled Elements of Finite Model Theory (see chapter (3,4, and) 7).
Lance Fortnow's ComplexityCast
Check out Lance Fortnow's ComplexityCast, in which he and Bill Gasarch engaged in an after-dinner talk about P vs. NP. I think it's really fun!
Friday, November 04, 2005
NL != P?
Howdy! It's been some time since I posted last. Being a graduate student, I don't think it is possible for me to post 3 - 4 times per week without sacrificing the quality of the posts. [Maybe, successful bloggers, like Professor Lance Fortnow, would care to tell me how they manage to cope well with both blogging and academic life.] However, my dear readers, rest assured! I do love posting here, and will try to post at least once a week.
Anyway, I just remembered that Stephen Cook told me some time ago that Michael Taitslin claimed to have a proof that NL is different from P, and at that time Steve was checking his proof. His paper can be found here. I am not quite sure of the progress. Incidentally, when I was in Los Alamos a couple of months back, a complexity theorist briefly looked at the paper and told me that it looks "fishy". Of course, in view of the many fallacious proofs that P != NP claimed by some novices (as discussed in here, people often tend to avoid reading "proofs" of this type of statements. Again, I am not sure of Taitslin's "proof". I read the first few pages, and all I can say is that he definitely uses some logic. One thing I can say though is that he has published some nice results in the areas of database theory and finite model theory in well-known journals and conference proceedings. This gives him some credentials, which perhaps will attract some of the readers to read his manuscript and find subtle bugs in his proof or verify the validity of his proof. In any case, if you decide to do so, please keep me informed :-)
Anyway, I just remembered that Stephen Cook told me some time ago that Michael Taitslin claimed to have a proof that NL is different from P, and at that time Steve was checking his proof. His paper can be found here. I am not quite sure of the progress. Incidentally, when I was in Los Alamos a couple of months back, a complexity theorist briefly looked at the paper and told me that it looks "fishy". Of course, in view of the many fallacious proofs that P != NP claimed by some novices (as discussed in here, people often tend to avoid reading "proofs" of this type of statements. Again, I am not sure of Taitslin's "proof". I read the first few pages, and all I can say is that he definitely uses some logic. One thing I can say though is that he has published some nice results in the areas of database theory and finite model theory in well-known journals and conference proceedings. This gives him some credentials, which perhaps will attract some of the readers to read his manuscript and find subtle bugs in his proof or verify the validity of his proof. In any case, if you decide to do so, please keep me informed :-)
Subscribe to:
Posts (Atom)