COMPUTING WITH INFINITARY LOGIC

Most recursive extensions of the first-order queries converge around t wo central classes of queries: fixpoint and while. Infinitary logic (w ith finitely many variables) is a very powerful extension of these lan guages which provides an elegant unifying formalism for a wide variety of query languages. However, neither the syntax nor the semantics of infinitary logic are effective, and its connection to practical query languages has been largely unexplored, We relate infinitary logic to a nother powerful extension of fixpoint and while, called relational mac hine, which highlights the computational style of these languages, Rel ational machines capture the kind of computation occurring when a quer y language is embedded in a host programming language, as in C+SQL. Th e main result of this paper is that relational machines correspond to the natural effective fragment of infinitary logic. Other well-known q uery languages are related to infinitary logic using syntactic restric tions formulated in language-theoretic terms. For example, it is shown that while corresponds to infinitary logic formulas which can be desc ribed by a regular language. As a side effect to these results, we obt ain interesting normal forms for effective infinitary logic formulas.