
FirstOrder
Query
Evaluation
Title: 
FirstOrder Query Evaluation 
Author:

Martin Raszyk (martin /dot/ raszyk /at/ inf /dot/ ethz /dot/ ch)

Submission date: 
20220215 
Abstract: 
We formalize firstorder query evaluation over an infinite domain with
equality. We first define the syntax and semantics of firstorder
logic with equality. Next we define a locale
eval_fo abstracting a representation of
a potentially infinite set of tuples satisfying a firstorder query
over finite relations. Inside the locale, we define a function
eval checking if the set of tuples satisfying a
firstorder query over a database (an interpretation of the
query's predicates) is finite (i.e., deciding relative
safety) and computing the set of satisfying tuples if it is
finite. Altogether the function eval solves
capturability (Avron and Hirshfeld, 1991) of
firstorder logic with equality. We also use the function
eval to prove a code equation for the semantics of
firstorder logic, i.e., the function checking if a firstorder query
over a database is satisfied by a variable assignment. We provide an
interpretation of the locale eval_fo
based on the approach by Ailamazyan et al. A core notion in the
interpretation is the active domain of a query and a database that
contains all domain elements that occur in the database or interpret
the query's constants. We prove the main theorem of Ailamazyan et
al. relating the satisfaction of a firstorder query over an infinite
domain to the satisfaction of this query over a finite domain
consisting of the active domain and a few additional domain elements
(outside the active domain) whose number only depends on the query. In
our interpretation of the locale
eval_fo, we use a potentially higher
number of the additional domain elements, but their number still only
depends on the query and thus has no effect on the data complexity
(Vardi, 1982) of query evaluation. Our interpretation yields an
executable function eval. The
time complexity of eval on a query is linear in the
total number of tuples in the intermediate relations for the
subqueries. Specifically, we build a database index to evaluate a
conjunction. We also optimize the case of a negated subquery in a
conjunction. Finally, we export code for the infinite domain of
natural numbers. 
BibTeX: 
@article{Eval_FOAFP,
author = {Martin Raszyk},
title = {FirstOrder Query Evaluation},
journal = {Archive of Formal Proofs},
month = feb,
year = 2022,
note = {\url{https://isaafp.org/entries/Eval_FO.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
Depends on: 
Containers 
Status: [ok] 
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.

