Automated Query Equivalence Solver (MongoDB)

Question

The query-equivalence problem is undecidable. However there are theorem provers that attempt to solve instances of undecidable problems. I am curious how I could go about using an automatic theorem prover (or other solvers) to prove that one MongoDB query is equivalent to another. The MongoDB query language is large, so I will focus on a small subset in the aggregation language.

Although my target is the MongoDB aggregation language, I think advice for query equivalence for SQL would be helpful too.

For example let's say I want to prove [$match: {...}, $sort: {...}] is equivalent to [$sort: {...}, $match: {...}]. \$match and \$sort pass documents from the previous pipeline stage to the next. \$match is a filter that only passes on documents where its predicate argument evaluate to true, and \$sort takes all documents given and sorts them on a field, then returns all documents. Essentially these are SQL WHERE and ORDER BY on a particular collection.

I understand why these queries produce the same result but I do not know how to prove it, or how to encode queries to allow a theorem prover to attempt to solve the problem.

How do I encode a query for a solver? It seems like I would need to communicate the behavior of different operators to it, like for example expressing that sorting an array leads to an array with the same elements but in increasing order. Thank you!

Answer 1

I'm not an expert on formal verification, so I'll share a non-expert perspective.

A general approach is: formalize the semantics of each operation (in whatever logic is accepted by your chosen theorem prover), then formulate the theorem you are trying to prove (that both queries yield the same results for all possible databases), then ask the theorem prover to prove it.

The details of how you go about that will depend a lot on the particular theorem prover you have chosen, the set of operations you want to support, how you formalize the semantics of each operation mathematically, and how much human assistance you want to provide the theorem prover.

There are a wide range of theorem provers, which strike different points in the tradeoff between automated proving (without human assistance) vs expressivity and based on different mathematical logics.

There are also likely to be multiple ways to formulate the semantics of the operations mathematically. For instance, suppose you know that all of your operations will only select some of the rows of input and/or re-order them, but will not produce new rows not found in the input or modify existing rows. Then the output of an operation could be represented by a sequence $(r_1,r_2,\dots,r_k)$ of indices, where $r_i$ is the index of a row in the input (namely, the $i$th row returned by the operation). Then each operation becomes a function $f$ that maps from an input to a sequence $r$; you can formulate the semantics of the composition of operations; and proving the equivalence of operations amounts to proving that they represent the same function.

Another approach, instead of formulating this as theorem proving of mathematical statements, would be to formulate this as formal verification of programs. You can view an operation as a program that takes an array as input (the database is an array of rows), and produces an array as output (an array of rows). You can write down code that implements the sort operation, and code that implements the match operation. So, now you can write down two subroutines: one that sorts then matches; and one that matches then sorts. Finally, you can try to use formal verification to prove that both subroutines yield the same output, on all possible inputs.

If you try to do this in practice, you'll probably quickly run into the limitations of the current state of the art in automated theorem proving and program verification. Theorem provers generally require a lot of hand-holding to prove non-trivial mathematical statements (they may require you to specify statements of lemmas that are useful to proof, or give hints on how to prove a statement). Program verification tools also generally require a lot of hand-holding to verify non-trivial programs correct (for instance, they may require you to specify many loop invariants). They are getting better, but it's still a non-trivial effort.

To learn more, you might start by looking at how to formally verify a sorting algorithm correct. That will give you ideas on possible ways you could formulate the kinds of properties you want to prove.

See also A general picture of formal verification in software.