We define a new kind of automata recognizing properties of data words or data
trees and prove that the automata capture all queries definable in Regular
XPath. We show that the automata-theoretic approach may be applied to answer
decidability and expressibility questions for XPath.
The Algebraic Dichotomy Conjecture states that the Constraint Satisfaction
Problem over a fixed template is solvable in polynomial time if the algebra of
polymorphisms associated to the template lies in a Taylor variety, and is
NP-complete otherwise. This paper provides two new characterizations of
finitely generated Taylor varieties. The first characterization is using
absorbing subalgebras and the second one cyclic terms. These new conditions
allow us to reprove the conjecture of Bang-Jensen and Hell (proved by the
authors) and the characterization of locally finite Taylor varieties using weak
near-unanimity terms (proved by McKenzie and Maróti) in an elementary and
self-contained way.
Is there any Cartesian-closed category of continuous domains that would be
closed under Jones and Plotkin's probabilistic powerdomain construction? This
is a major open problem in the area of denotational semantics of probabilistic
higher-order languages. We relax the question, and look for quasi-continuous
dcpos instead. We introduce a natural class of such quasi-continuous dcpos, the
omega-QRB-domains. We show that they form a category omega-QRB with pleasing
properties: omega-QRB is closed under the probabilistic powerdomain functor,
under finite products, under taking bilimits of expanding sequences, under
retracts, and even under so-called quasi-retracts. But... omega-QRB is not
Cartesian closed. We conclude by showing that the QRB domains are just one half
of an FS-domain, merely lacking control.
The universal-algebraic approach has proved a powerful tool in the study of
the complexity of CSPs. This approach has previously been applied to the study
of CSPs with finite or (infinite) omega-categorical templates, and relies on
two facts. The first is that in finite or omega-categorical structures A, a
relation is primitive positive definable if and only if it is preserved by the
polymorphisms of A. The second is that every finite or omega-categorical
structure is homomorphically equivalent to a core structure. In this paper, we
present generalizations of these facts to infinite structures that are not
necessarily omega-categorical. (This abstract has been severely curtailed by
the space constraints of arXiv -- please read the full abstract in the
article.) Finally, we present applications of our general results to the
description and analysis of the complexity of CSPs. In particular, we give
general hardness criteria based on the absence of polymorphisms that depend on
more than one argument, and we present a polymorphism-based description of
those CSPs that are first-order definable (and therefore can be solved in
polynomial time).
Evaluating a Boolean conjunctive query Q against a guarded first-order theory
F is equivalent to checking whether "F and not Q" is unsatisfiable. This
problem is relevant to the areas of database theory and description logic.
Since Q may not be guarded, well known results about the decidability,
complexity, and finite-model property of the guarded fragment do not obviously
carry over to conjunctive query answering over guarded theories, and had been
left open in general. By investigating finite guarded bisimilar covers of
hypergraphs and relational structures, and by substantially generalising
Rosati's finite chase, we prove for guarded theories F and (unions of)
conjunctive queries Q that (i) Q is true in each model of F iff Q is true in
each finite model of F and (ii) determining whether F implies Q is
2EXPTIME-complete. We further show the following results: (iii) the existence
of polynomial-size conformal covers of arbitrary hypergraphs; (iv) a new proof
of the finite model property of the clique-guarded fragment; (v) the small
model property of the guarded fragment with optimal bounds; (vi) a
polynomial-time solution to the canonisation problem modulo guarded
bisimulation, which yields (vii) a capturing result for guarded bisimulation
invariant PTIME.
As observed by Intrigila, there are hardly techniques available in the
lambda-calculus to prove that two lambda-terms are not beta-convertible.
Techniques employing the usual Boehm Trees are inadequate when we deal with
terms having the same Boehm Tree (BT). This is the case in particular for fixed
point combinators, as they all have the same BT. Another interesting equation,
whose consideration was suggested by Scott, is BY = BYS, an equation valid in
the classical model P-omega of lambda-calculus, and hence valid with respect to
BT-equality but nevertheless the terms are beta-inconvertible. To prove such
beta-inconvertibilities, we employ `clocked' BT's, with annotations that convey
information of the tempo in which the data in the BT are produced. Boehm Trees
are thus enriched with an intrinsic clock behaviour, leading to a refined
discrimination method for lambda-terms. The corresponding equality is strictly
intermediate between beta-convertibility and Boehm Tree equality, the equality
in the model P-omega. An analogous approach pertains to Levy-Longo and
Berarducci Trees. Our refined Boehm Trees find in particular an application in
beta-discriminating fixed point combinators (fpc's). It turns out that Scott's
equation BY = BYS is the key to unlocking a plethora of fpc's, generated by a
variety of production schemes of which the simplest was found by Boehm, stating
that new fpc's are obtained by postfixing the term SI, also known as Smullyan's
Owl. We prove that all these […]
We study a natural hierarchy in first-order logic, namely the quantifier
structure hierarchy, which gives a systematic classification of first-order
formulas based on structural quantifier resource. We define a variant of
Ehrenfeucht-Fraisse games that characterizes quantifier classes and use it to
prove that this hierarchy is strict over finite structures, using strategy
compositions. Moreover, we prove that this hierarchy is strict even over
ordered finite structures, which is interesting in the context of descriptive
complexity.
