Computing with First-Order Logic

摘要

We study two important extensions of first-order logic (FO) with iteration, the fixpoint and while queries. The main result of the paper concerns the open problem of the relationship between fixpoint and while: they are the same iff PTIME = PSPACE. These and other expressibility results are obtained using a powerful normal form for while which shows that each while computation over an unordered domain can be reduced to a while computation over an ordered domain via a fixpoint query. The fixpoint query computes an equivalence relation on tuples which is a congruence with respect to the rest of the computation. The same technique is used to show that equivalence of tuples and structures with respect to FO formulas with bounded number of variables is definable in fixpoint. Generalizing fixpoint and while, we consider more powerful languages which model arbitrary computation interacting with a database using a finite set of FO queries. Such computation is modeled by a relational machine called loosely coupled generic machine, GMloose. GMloose consists of a Turing machine augmented with a finite set of fixed-arity relations forming a relational store. The connection with while is emphasised by a result showing that GMloose is equivalent to while augmented with integer variables and arithmetic. The normal form for while extends to these languages. We study the expressive power of GMloose and its PTIME and PSPACE restrictions. We argue that complexity measures based on the size of the input may not be best suited for database computation. Instead, we suggest an alternative measure based on the discerning power of the machine, i.e., its ability to distinguish between tuples given its input. With this measure of the input, it is shown that fixpoint and while are the PTIME and PSPACE restrictions of GMloose.