### Abstract

We formalize first-order query evaluation over an infinite domain with equality. We first define the syntax and semantics of first-order logic with equality. Next we define a locale eval_fo abstracting a representation of a potentially infinite set of tuples satisfying a first-order query over finite relations. Inside the locale, we define a function eval checking if the set of tuples satisfying a first-order 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 first-order logic with equality. We also use the function eval to prove a code equation for the semantics of first-order logic, i.e., the function checking if a first-order 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 first-order 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.

### License

BSD License

### Topics

- Computer science/Data management systems
- Logic/General logic/Classical first-order logic

### Session Eval_FO

- Infinite
- FO
- Eval_FO
- Mapping_Code
- Cluster
- Ailamazyan
- Ailamazyan_Code

### Depends on

- Light-weight Containers

## Cite

×

Eval_FO-AFP

    @article{Eval_FO-AFP,
      author  = {Martin Raszyk},
      title   = {First-Order Query Evaluation},
      journal = {Archive of Formal Proofs},
      month   = {February},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Eval_FO.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Feb 21, 2022 : Isabelle2021-1