[//]: # (A rendered version of this review is available at https://hackmd.io/@remyw/rc2sql)
$$
\newcommand{\qryinqfin}{Q_{\not\infty}}
\newcommand{\qryrb}{\tilde{Q}}
\newcommand{\qryrbx}{\tilde{Q}'}
\newcommand{\varx}{x}
\newcommand{\fv}[1]{\mathsf{fv}(#1)}
\newcommand{\valsymb}{\alpha}
\newcommand{\oneatom}{Q_{\mathit{ap}}}
\newcommand{\apreds}{\mathcal{A}}
\newcommand{\fvseq}[1]{\vec{\mathsf{fv}}(#1)}
\newcommand{\ethz}{(VGT_1)}
\newcommand{\vgtrw}{(VGT_2)}
\newcommand{\tcov}[3]{\mathsf{cov}({#1},{#2},{#3})}
\newcommand{\cpreds}{\mathcal{G}}
\newcommand{\dom}{\mathcal{D}}
\newcommand{\transfree}{\faStarO}
\newcommand{\sconjtwo}[2]{\bigwedge\nolimits^\approx({#1},{#2})}
\newcommand{\eqconjqry}{R^\approx}
$$

## 2. Related Work

> In contrast, the question of whether a *fixed* structure satisfies the given RC query is decidable

What does it mean for a structure to *satisfy* an RC query, if the query has free variables?

The motivation of this paper is to decide if an arbitrary RC query is finite, and compute the finite result if so, given a fixed database and under the assumption of an infinite domain. The authors also refer to this problem as "Avron and Hirshfeld's capturability problem additionally assuming an infinite domain". In my understanding this paper is not the first one to achieve that, but rather the first one to achieve that with practical run time. If that is correct, then which paper was the first one to achieve that disregarding practical efficiency? Was it [AGSS86]? And does [HS94] also achieve the goal, albeit with impractical run time due to the use of the active domain?

[AGSS86] seems to be an important piece of work, but it's in Russian. Is it possible to add a section in the appendix to explain the main ideas of that paper? I hope that wouldn't be difficult since it's a short paper.

## 4. Query Translation

> $\qryrbx$ is a disjunction, $\varx$ is range restricted in the first disjunct,
and only occurs in the remaining disjuncts in subqueries of a special form
that are conjoined at the top-level to the disjuncts.

This is a very confusing sentence. Do you mean each such subquery appears as a conjunct at the top-level of each disjunct? Overall I find this second bullet confusing. After reading the remaining text, I think it can be more helpful to simply break down into three cases:

1. $x$ is range restricted
2. $x$ can be eliminated via equality to other variables
3. The previous cases do not hold

Is it true that the last case corresponds to "query satisfied by infinitely many values of $\varx$ for all values of the remaining free variables"?

> Let $\qryrb$ be a query with range-restricted bound variables, $\varx \in \fv{\qryrb}$.

I suggest to add "and" after the comma.

> $$
\begin{array}{@{}l@{\;}c@{\;}l@{\;\;}l@{\;\;\;\;}l@{}}
\valsymb\models\neg\bigvee_{\oneatom\in\apreds}\exists \fvseq{\oneatom}\setminus
\{\varx\}.\;\oneatom&\Longrightarrow&
(\valsymb\models\qryrb\Longleftrightarrow\valsymb\models \qryrb[\varx/\bot])&\ethz&\text{and}\\
\valsymb\models\qryrb[\varx/\bot]&\Longrightarrow& \valsymb\models\forall \varx.\,\qryrb&\vgtrw.
\end{array}
$$

$\vgtrw$ is not a property of $\apreds$ as it does not even mention $\apreds$. Therefore, the following sentence is also problematic: "In contrast to Van Gelder and Topor, we only require that $\apreds$ satisfies $\ethz$".

> We state the soundness and completeness of the relation $\tcov{\varx}{\qryrb}{\cpreds}$

Sound and complete with respect to what property?

In Example 4.4, the parentheses are very hard to match. Can you use different sizes?

> the query...is a tautology over $\dom$...This reasoning justifies

Can your translation algorithm detect tautologies?

> We remark that if we applied ($\faStarO$)
to the entire disjunct $\sconjtwo{\qryinqfin} {\eqconjqry}$,
the loop on Lines~\ref{alg:free:loopbeg}--\ref{alg:free:loopend} might not terminate.