#HornSAT is not in $\Sigma{\rm QSO}(\Sigma_{2}\textsc{-Horn})$.

Next we show that $\Sigma{\rm QSO}(\Sigma_{2}\textsc{-Horn})$ is the class we
were looking for, as not only every function in $\Sigma{\rm
QSO}(\Sigma_{2}\textsc{-Horn})$ has an easy decision counterpart, but also
$\Sigma{\rm QSO}(\Sigma_{2}\textsc{-Horn})$ admits a natural complete problem
under parsimonious reductions. More precisely, define #DisjHornSAT as the
problem of counting the satisfying assignments of a formula $\Phi$ that is a
disjunction of Horn formulae. Then we have that:

######  Theorem 18.

#DisjHornSAT is $\Sigma{\rm QSO}(\Sigma_{2}\textsc{-Horn})$-complete under
parsimonious reductions.

######  Proof 5.12.

First we prove that #DisjHornSAT is in $\Sigma{\rm
QSO}(\Sigma_{2}\textsc{-Horn})$. Recall that each instance of #DisjHornSAT is
a disjunction of Horn formulae. Let $\mathbf{R}$ be a relational signature
such that
$\mathbf{R}=\\{\textit{P}(\cdot,\cdot),\textit{N}(\cdot,\cdot),\textit{V}(\cdot),\textit{NC}(\cdot),\textit{D}(\cdot,\cdot)\\}$.
Each symbol in this vocabulary is used to indicate the same as in Example 5.3,
with the addition of $\textit{D}(d,c)$ which indicates that $c$ is a clause in
the formula $d$. Define $\psi$ as in Example 5.3 such that
$\Sigma{\textit{T}}.\,\Sigma{\textit{A}}.\,\psi(\textit{T},\textit{A})$
defines #HornSAT. In order to encode #DisjHornSAT, we extend
$\psi(\textit{T},\textit{A})$ by adding the information of $\textit{D}(d,c)$
as follows:

$\displaystyle\psi^{\prime}(T,A)\ :=\ \exists{d}.\>\big{[}\ $
$\displaystyle\forall{x}.\>(\neg\textit{T}(x)\vee\textit{V}(x))\ \wedge$
$\displaystyle\forall{c}.\>(\neg\textit{D}(c,d)\vee\neg\textit{NC}(c)\vee\exists{x}.\>\neg\textit{A}(c,x))\
\wedge$
$\displaystyle\forall{c}.\>\forall{x}.\>(\neg\textit{D}(c,d)\vee\neg\textit{P}(c,x)\vee\exists{y}.\>\neg\textit{A}(c,y)\vee\textit{T}(x))\
\wedge$
$\displaystyle\forall{c}.\>\forall{x}.\>(\neg\textit{D}(c,d)\vee\neg\textit{N}(c,x)\vee\textit{T}(x)\vee\neg\textit{A}(c,x))\
\wedge$
$\displaystyle\forall{c}.\>\forall{x}.\>(\neg\textit{D}(c,d)\vee\textit{A}(c,x)\vee\textit{N}(c,x))\
\wedge$
$\displaystyle\forall{c}.\>\forall{x}.\>(\neg\textit{D}(c,d)\vee\textit{A}(c,x)\vee\neg\textit{T}(x))\
\big{]}.$

One can check that $\psi^{\prime}(T,A)$ effectively defines #DisjHornSAT as
for every disjunction of Horn formulae
$\theta=\theta_{1}\vee\cdots\vee\theta_{m}$ encoded by an
$\mathbf{R}$-structure $\mathfrak{A}$, the number of satisfying assignments of
$\theta$ is equal to
${\llbracket{}{\Sigma{\textit{T}}.\,\Sigma{\textit{A}}.\,\psi^{\prime}(\textit{T},\textit{A})}\rrbracket}(\mathfrak{A})$.
Therefore, we conclude that $\textsc{\\#DisjHornSAT}\in\Sigma{\rm
QSO}(\Sigma_{2}\textsc{-Horn})$.

Next, we prove that #DisjHornSAT is hard for $\Sigma{\rm
QSO}(\Sigma_{2}\textsc{-Horn})$ over each signature $\mathbf{R}$ under
parsimonious reductions. For each $\Sigma{\rm QSO}(\Sigma_{2}\textsc{-Horn})$
formula $\alpha$ over $\mathbf{R}$, we define a polynomial-time function
$g_{\alpha}$ that receives an $\mathbf{R}$-structure $\mathfrak{A}$ and
outputs an instance of #DisjHornSAT such that
${\llbracket{}{\alpha}\rrbracket}(\mathfrak{A})=\textsc{\\#DisjHornSAT}(g_{\alpha}(\mathfrak{A}))$.
By Proposition 8, we can assume that $\alpha$ is of the form:

$\alpha\ =\
\sum_{i=1}^{m}\Sigma{\bar{X}_{i}}.\,\Sigma{\bar{x}}.\,\exists{\bar{y}}.\>\bigwedge_{j=1}^{n}\forall{\bar{z}}.\>\varphi^{i}_{j}(\bar{X}_{i},\bar{x},\bar{y},\bar{z}),$

where each $\varphi^{i}_{j}$ is a Horn clause, and each $\bar{X}_{i}$ is a
sequence of second-order variables. Consider $\bar{X}$ as the union of all
$\bar{X}_{i}$. We replace each of the $m$ summands in $\alpha$ with

$\Sigma{\bar{X}}.\,\Sigma{\bar{x}}.\,\exists{\bar{y}}.\>\bigg{(}\bigwedge_{j=1}^{n}\forall{\bar{z}}.\>\varphi^{i}_{j}(\bar{X}_{i},\bar{x},\bar{y},\bar{z})\wedge\bigwedge_{X\not\in\bar{X}_{i}}\\!\\!\forall{\bar{u}}.\>X(\bar{u})\bigg{)},$

whose sum is equivalent to $\alpha$. Now, consider a finite
$\mathbf{R}$-structure $\mathfrak{A}$ with domain $A$. The next transformation
of $\alpha$ and $\mathfrak{A}$ towards a disjunction of Horn-formulae is to
expand each first-order quantifier (i.e. $\Sigma{\bar{x}}$, $\exists\bar{y}$,
and $\forall\bar{z}$) by replacing variables with constants. More
specifically, we obtain the following formula that defines the same function
as $\alpha$, and it is of polynomial size in the size of $\mathfrak{A}$
(recall that $\alpha$ is fixed):

$\alpha_{\mathfrak{A}}\ =\ \sum_{i=1}^{m}\sum_{\bar{a}\,\in
A^{|\bar{x}|}}\Sigma{\bar{X}}.\,\bigvee_{\bar{b}\,\in
A^{|\bar{y}|}}\bigg{(}\bigwedge_{j=1}^{n}\bigwedge_{\bar{c}\,\in
A^{|\bar{z}|}}\varphi^{i}_{j}(\bar{X}_{i},\bar{a},\bar{b},\bar{c})\wedge\bigwedge_{X\not\in\bar{X}_{i}}\bigwedge_{\bar{e}\,\in
A^{{\rm arity}(X)}}\\!\\!\\!\\!\\!\\!\\!X(\bar{e})\bigg{)}.$

Notice that each first-order subformula in
$\varphi^{i}_{j}(\bar{X}_{i},\bar{a},\bar{b},\bar{c})$ has no free variables
and, therefore, we can evaluate each of them in polynomial time and easily
rewrite $\alpha_{\mathfrak{A}}$ to an equivalent formula that does not have
any first-order subformula. In other words, in polynomial time we can replace
$\varphi^{i}_{j}$ with a disjunction of negative literals of the form $\neg
X_{\ell}(\bar{d})$ and at most one positive literal of the form
$X_{\ell}(\bar{d})$, where $\bar{d}$ is a tuple of constants. After
simplifying, grouping and reordering the previous formula, we can obtain an
equivalent formula $\alpha_{\mathfrak{A}}^{\prime}$ of the form:

$\alpha_{\mathfrak{A}}^{\prime}\ =\
\sum_{i=1}^{m^{\prime}}\Sigma{\bar{X}}.\,\bigvee_{j=1}^{n_{1}^{\prime}}\bigwedge_{k=1}^{n_{2}^{\prime}}\psi^{i}_{j,k}(\bar{X}),$

where every $\psi^{i}_{j,k}(\bar{X})$ is a disjunction of negative literals of
the form $\neg X_{\ell}(\bar{d})$ and at most one positive literal of the form
$X_{\ell}(\bar{d})$, where $\bar{d}$ is a tuple of constants.

The idea for the rest of the proof is to show how to obtain
$g_{\alpha}(\mathfrak{A})$, i.e. an instance of #DisjHornSAT, from
$\alpha_{\mathfrak{A}}^{\prime}$. First, if $m^{\prime}=1$ and
$\alpha_{\mathfrak{A}}^{\prime}=\Sigma{\bar{X}}.\,\bigvee_{j=1}^{n_{1}^{\prime}}\bigwedge_{k=1}^{n_{2}^{\prime}}\psi_{j,k}(\bar{X})$,
then we can define $g_{\alpha}(\mathfrak{A})$ as the propositional formula
$\bigvee_{j=1}^{n_{1}^{\prime}}\bigwedge_{k=1}^{n_{2}^{\prime}}\psi_{j,k}(\bar{X})$
over the propositional alphabet $\\{X(\bar{e})\mid X\in\bar{X}\text{ and
}\bar{e}\in A^{{\rm arity}(X)}\\}$. It is straightforward to see that
$\bigvee_{j=1}^{n_{1}^{\prime}}\bigwedge_{k=1}^{n_{2}^{\prime}}\psi_{j,k}(\bar{X})$
is a disjunction of Horn formulae, and its number of satisfying assignments is
exactly ${\llbracket{}{\alpha}\rrbracket}(\mathfrak{A})$. Otherwise, if
$m^{\prime}>1$, then we can use $m^{\prime}$ fresh new variables
$t_{1},\ldots,t_{m^{\prime}}$ and define:

$g_{\alpha}(\mathfrak{A})\ :=\
\bigvee_{i=1}^{m^{\prime}}\,\bigvee_{j=1}^{n_{1}^{\prime}}\,\bigwedge_{k=1}^{n_{2}^{\prime}}\,\psi^{i}_{j,k}(\bar{X})\wedge
t_{i}\wedge\bigwedge_{\ell\neq i}\neg t_{\ell}$

over the propositional alphabet $\\{X(\bar{e})\mid X\in\bar{X}\text{ and
}\bar{e}\in A^{{\rm arity}(X)}\\}\cup\\{t_{1},\ldots,t_{m^{\prime}}\\}$.
Variables $t_{1},\ldots,t_{m^{\prime}}$ are used to have disjoint sets of
propositional assignments for the different disjuncts of the outermost
disjunction, which correspond to the summands in the original formula. One can
easily check that $g_{\alpha}(\mathfrak{A})$ is a disjunction of Horn
formulae, and that the number of satisfying assignments of
$g_{\alpha}(\mathfrak{A})$ is exactly
${\llbracket{}{\alpha}\rrbracket}(\mathfrak{A})$. This covers all possible
cases for $\alpha$, and the entire procedure takes polynomial time.

Now that we have a complete problem for $\Sigma{\rm
QSO}(\Sigma_{2}\textsc{-Horn})$, we can provide a simple proof of Proposition
16.

_Proof of Proposition 16._ As we mentioned before, TotP is closed under
parsimonious reductions, so we only need to show that #DisjHornSAT is in TotP.
For this consider a non-deterministic procedure that receives a DisjHornSAT
formula $\Phi$ as input and does the following. First it checks whether $\Phi$
is satisfiable. If it is not, then it stops; otherwise, it creates a dummy
branch that simply stops, and continues in the main branch. More precisely, it
picks in the main branch a propositional variable $x$ in $\Phi$ and creates
two formulae $\Phi_{0}$ and $\Phi_{1}$, where $x$ has been replaced by $\perp$
and $\top$, respectively. If only one of these is satisfiable, it continues on
this branch with the respective $\Phi_{i}$, and if both are satisfiable, then
it creates a new branch for $\Phi_{1}$ and continues on this branch with
$\Phi_{0}$. On each branch, it repeats the same instructions until no
variables are left to replace. Since DisjHornSAT is in P, all the
aforementioned checks can be done in polynomial time, so that the procedure
takes at most $h(n)$ steps in each branch, where $n$ is the size of $\Phi$ and
$h$ is some fixed polynomial. Moreover, the algorithm produces exactly
$\textsc{\\#DisjHornSAT}(\Phi)+1$ branches, from which we conclude that
#DisjHornSAT is in TotP. ∎

Finally, it is important to mention that from the previous proof one can
easily derive that $\Sigma{\rm
QSO}(\Sigma_{2}\textsc{-Horn})\equiv\\#(\Sigma_{2}\textsc{-Horn})$. Therefore,
the framework in [SST95] is enough for defining the class of problems in
$\Sigma{\rm QSO}(\Sigma_{2}\textsc{-Horn})$.

##  6\. Adding recursion to QSO

We have used weighted logics to give a framework for descriptive complexity of
counting complexity classes. Here, we go beyond weighted logics and give the
first steps on defining recursion at the quantitative level. This goal is not
trivial not only because we want to add recursion over functions, but also
because it is not clear what could be the right notion of “fixed point”. To
this end, we show first how to extend ${\rm QSO}$ with function symbols that
are later used to define a natural generalization of LFP to functions. As a
proof of concept, we show that this notion can be used to capture FP.
Moreover, we use this concept to define an operator for counting paths in a
graph, a natural generalization of the transitive closure operator [Imm99],
and show that this gives rise to a logic that captures #L.

We start by defining an extension of ${\rm QSO}$ with function symbols. Assume
that $\mathbf{FS}$ is an infinite set of function symbols, where each
$h\in\mathbf{FS}$ has an associated arity denoted by ${\rm arity}(h)$. Then
the set of ${\rm FQSO}$ formulae over a signature $\mathbf{R}$ is defined by
the following grammar:

$\alpha\ :=\ \varphi\ \mid\ s\ \mid\ h(x_{1},\ldots,x_{\ell})\ \mid\
(\alpha+\alpha)\ \mid\ (\alpha\cdot\alpha)\ \mid\\\ \Sigma{x}.\,\alpha\ \mid\
\Pi{x}.\,\alpha\ \mid\ \Sigma{X}.\,\alpha\ \mid\ \Pi{X}.\,\alpha,$ (9)

where $h\in\mathbf{FS}$, ${\rm arity}(h)=\ell$ and $x_{1},\ldots,x_{\ell}$ is
a sequence of (not necessarily distinct) first-order variables. Given an
$\mathbf{R}$-structure $\mathfrak{A}$ with domain $A$, we say that $F$ is a
_function assignment_ for $\mathfrak{A}$ if for every $h\in\mathbf{FS}$ with
${\rm arity}(h)=\ell$, we have that $F(h)\colon A^{\ell}\to\mathbb{N}$. The
notion of function assignment is used to extend the semantics of ${\rm QSO}$
to the case of a quantitative formula of the form $h(x_{1},\ldots,x_{\ell})$.
More precisely, given first-order and second-order assignments $v$ and $V$ for
$\mathfrak{A}$, respectively, we have that:

$\displaystyle{\llbracket{}{h(x_{1},\ldots,x_{\ell})}\rrbracket}(\mathfrak{A},v,V,F)$
$\displaystyle=F(h)(v(x_{1}),\ldots,v(x_{\ell})).$

As for the case of ${\rm QFO}$, we define ${\rm FQFO}$ disallowing quantifiers
$\Sigma X$ and $\Pi X$ in (9).

It is worth noting that function symbols in ${\rm FQSO}$ represent functions
from tuples to natural numbers, so they are different from the classical
notion of function symbol in ${\rm FO}$ [Lib04]. Furthermore, a function
symbol can be seen as an “oracle” that is instantiated by the function
assignment. To the best of our knowledge, this is the first article to propose
this extension on weighted logics, which we think should be further
investigated.

We define an extension of LFP [Imm86, Var82] to allow counting. More
precisely, the set of ${\rm RQFO}({\rm FO})$ formulae over a signature
$\mathbf{R}$, where ${\rm RQFO}$ stands for recursive ${\rm QFO}$, is defined
as an extension of ${\rm QFO}({\rm FO})$ that includes the formula $[{\bf
lsfp}\,\beta(\bar{x},h)]$, where (1) $\bar{x}=(x_{1},\ldots,x_{\ell})$ is a
sequence of $\ell$ distinct first-order variables, (2) $\beta(\bar{x},h)$ is
an ${\rm FQFO}({\rm FO})$-formula over $\mathbf{R}$ whose only function symbol
is $h$, and (3) ${\rm arity}(h)=\ell$. The free variables of the formula
$[{\bf lsfp}\,\beta(\bar{x},h)]$ are $x_{1},\ldots,x_{\ell}$; in particular,
$h$ is not considered to be free.

Fix an $\mathbf{R}$-structure with domain $A$ and a quantitative formula
$[{\bf lsfp}\,\beta(\bar{x},h)]$ with ${\rm arity}(h)=\ell$, and assume that
$\mathcal{F}$ is the set of functions $f\colon A^{\ell}\to\mathbb{N}$. To
define the semantics of $[{\bf lsfp}\,\beta(\bar{x},h)]$, we first show how
$\beta(\bar{x},h)$ can be interpreted as an operator $T_{\beta}$ on
$\mathcal{F}$. More precisely, for every $f\in\mathcal{F}$ and tuple
$\bar{a}=(a_{1},\ldots,a_{\ell})\in A^{\ell}$, the function $T_{\beta}(f)$
satisfies that:

$\displaystyle T_{\beta}(f)(\bar{a})$
$\displaystyle={\llbracket{}{\beta(\bar{x},h)}\rrbracket}(\mathfrak{A},v,F),$

where $v$ is a first-order assignment for $\mathfrak{A}$ such that
$v(x_{i})=a_{i}$ for every $i\in\\{1,\ldots,\ell\\}$, and $F$ is a function
assignment for $\mathfrak{A}$ such that $F(h)=f$.

As for the case of LFP, it would be natural to consider the point-wise partial
order $\leq$ on $\mathcal{F}$ defined as $f\leq g$ if, and only if,
$f(\bar{a})\leq g(\bar{a})$ for every $\bar{a}\in A^{\ell}$, and let the
semantics of $[{\bf lsfp}\,\beta(\bar{x},h)]$ be the least fixed point of the
operator $T_{\beta}$. However, $(\mathcal{F},\leq)$ is not a complete lattice,
so we do not have a Knaster-Tarski Theorem ensuring that such a fixed point
exists. Instead, we generalize the semantics of LFP as follows. In the
definition of the semantics of LFP, an operator $T$ on relations is
considered, and the semantics is defined in terms of the least fixed point of
$T$, that is, a relation $R$ such that [Imm86, Var82]: (a) $T(R)=R$, and (b)
$R\subseteq S$ for every $S$ such that $T(S)=S$. We can view $T$ as an
operator on functions if we consider the characteristic function of a
relation. Given a relation $R\subseteq A^{\ell}$, let $\chi_{R}$ be its
characteristic function, that is $\chi_{R}(\bar{a})=1$ if $\bar{a}\in R$, and
$\chi_{R}(\bar{a})=0$ otherwise. Then define an operator $T^{\star}$ on
characteristic functions as $T^{\star}(\chi_{R})=\chi_{T(R)}$. Moreover, we
can rewrite the conditions defining a least fixed point of $T$ in terms of the
operator $T^{\star}$ if we consider the notion of support of a function. Given
a function $f\in\mathcal{F}$, define the support of $f$, denoted by $\text{\rm
supp}(f)$, as $\\{\bar{a}\in A^{\ell}\mid f(\bar{a})>0\\}$. Then given that
$\text{\rm supp}(\chi_{R})=R$, we have that the conditions (a) and (b) are
equivalent to the following conditions on $T^{\star}$: (a) $\text{\rm
supp}(T^{\star}(\chi_{R}))=\text{\rm supp}(\chi_{R})$, and (b) $\text{\rm
supp}(\chi_{R})\subseteq\text{\rm supp}(\chi_{S})$ for every $S$ such that
$\text{\rm supp}(T^{\star}(\chi_{S}))=\text{\rm supp}(\chi_{S})$. To define a
notion of fixed point for $T_{\beta}$ we simply generalize these conditions.
More precisely, a function $f\in\mathcal{F}$ is a s-fixed point of $T_{\beta}$
if $\text{\rm supp}(T_{\beta}(f))=\text{\rm supp}(f)$, and $f$ is a least
s-fixed point of $T_{\beta}$ if $f$ is a s-fixed point of $T_{\beta}$ and for
every s-fixed point $g$ of $T_{\beta}$ it holds that $\text{\rm
supp}(f)\subseteq\text{\rm supp}(g)$. The existence of such fixed point is
ensured by the following lemma:

######  Lemma 19.

Let $h\in\mathbf{FS}$ such that ${\rm arity}(h)=\ell$, and $\beta$ be an ${\rm
FQFO}({\rm FO})$-formula over a signature $\mathbf{R}$ such that if a function
symbol occurs in $\beta$, then this function symbol is $h$. Moreover, let
$\mathfrak{A}$ be an $\mathbf{R}$-structure with domain $A$, $f,g\colon
A^{\ell}\to\mathbb{N}$ and $F,G$ be function assignments such that $F(h)=f$
and $F(h)=g$. If $\text{\rm supp}(f)\subseteq\text{\rm supp}(g)$, then for
every first-order and second-order assignments $v$ and $V$, respectively, it
holds that:

if ${\llbracket{}{\beta}\rrbracket}(\mathfrak{A},v,V,F)>0$, then
${\llbracket{}{\beta}\rrbracket}(\mathfrak{A},v,V,G)>0$.

######  Proof 6.1.

We prove the lemma by induction on the structure of $\beta$. First we need to
consider the base cases.

  1. (1)

Assume that $\beta$ is either a constant $s\in\mathbb{N}$ or an ${\rm
FO}$-formula $\varphi$. In both cases, function symbol $h$ is not mentioned,
so
${\llbracket{}{\beta}\rrbracket}(\mathfrak{A},v,V,F)={\llbracket{}{\beta}\rrbracket}(\mathfrak{A},v,V,G)$
and it trivially holds that if
${\llbracket{}{\beta}\rrbracket}(\mathfrak{A},v,V,F)>0$, then
${\llbracket{}{\beta}\rrbracket}(\mathfrak{A},v,V,G)>0$.

  2. (2)

Assume that $\beta$ is equal to $h(y_{1},\ldots,y_{\ell})$, where $y_{1}$,
$\ldots$, $y_{\ell}$ is a sequence of (non-necessarily pairwise distinct)
variables. Let $\bar{a}=(v(y_{1}),\ldots,v(y_{\ell}))$. Then we have that
${\llbracket{}{\beta}\rrbracket}(\mathfrak{A},v,V,F)=F(h)(v(y_{1}),\ldots,v(y_{\ell}))=f(\bar{a})$
and ${\llbracket{}{\beta}\rrbracket}(\mathfrak{A},v,V,G)=g(\bar{a})$. Given
that $\text{\rm supp}(f)\subseteq\text{\rm supp}(g)$, if $f(\bar{a})>0$, then
$g(\bar{a})>0$. Hence, we conclude that if
${\llbracket{}{\beta}\rrbracket}(\mathfrak{A},v,V,F)>0$, then
${\llbracket{}{\beta}\rrbracket}(\mathfrak{A},v,V,G)>0$.

We now consider the inductive steps. Assume that the property holds for ${\rm
FQFO}({\rm FO})$-formulae $\beta_{1}$, $\beta_{2}$ and $\delta$

  1. (3)

Assume that $\beta=(\beta_{1}+\beta_{2})$. If
${\llbracket{}{\beta}\rrbracket}(\mathfrak{A},v,V,F)>0$, then
${\llbracket{}{\beta_{1}}\rrbracket}(\mathfrak{A},v,V,F)>0$ or
${\llbracket{}{\beta_{2}}\rrbracket}(\mathfrak{A},v,V,F)>0$. Thus, by
induction hypothesis we conclude that
${\llbracket{}{\beta_{1}}\rrbracket}(\mathfrak{A},v,V,G)>0$ or
${\llbracket{}{\beta_{2}}\rrbracket}(\mathfrak{A},v,V,G)>0$. Hence, we have
that ${\llbracket{}{\beta}\rrbracket}(\mathfrak{A},v,V,G)>0$.

  2. (4)

Assume that $\beta=(\beta_{1}\cdot\beta_{2})$. If
${\llbracket{}{\beta}\rrbracket}(\mathfrak{A},v,V,F)>0$, then
${\llbracket{}{\beta_{1}}\rrbracket}(\mathfrak{A},v,V,F)>0$ and
${\llbracket{}{\beta_{2}}\rrbracket}(\mathfrak{A},v,V,F)>0$. Thus, by
induction hypothesis we conclude that
${\llbracket{}{\beta_{1}}\rrbracket}(\mathfrak{A},v,V,G)>0$ and
${\llbracket{}{\beta_{2}}\rrbracket}(\mathfrak{A},v,V,G)>0$. Hence, we have
that ${\llbracket{}{\beta}\rrbracket}(\mathfrak{A},v,V,G)>0$.

  3. (5)

Suppose that $\beta=\Sigma{x}.\,\delta$. Then we have that
${\llbracket{}{\beta}\rrbracket}(\mathfrak{A},v,V,F)=\sum_{a\in
A}{\llbracket{}{\delta}\rrbracket}(\mathfrak{A},v[a/x],V,F)$ and
${\llbracket{}{\beta}\rrbracket}(\mathfrak{A},v,V,G)=\sum_{a\in
A}{\llbracket{}{\delta}\rrbracket}(\mathfrak{A},v[a/x],V,G)$. Thus, if we
assume that ${\llbracket{}{\beta}\rrbracket}(\mathfrak{A},v,V,F)>0$, then
there exists $a\in A$ such that
${\llbracket{}{\delta}\rrbracket}(\mathfrak{A},v[a/x],V,F)>0$. Hence, by
induction hypothesis we have that
${\llbracket{}{\delta}\rrbracket}(\mathfrak{A},v[a/x],V,G)>0$ and, therefore,
we conclude that ${\llbracket{}{\beta}\rrbracket}(\mathfrak{A},v,V,G)>0$.

  4. (6)

Suppose that $\beta=\Pi{x}.\,\delta$. Then we have that
${\llbracket{}{\beta}\rrbracket}(\mathfrak{A},v,V,F)=\prod_{a\in
A}{\llbracket{}{\delta}\rrbracket}(\mathfrak{A},v[a/x],V,F)$ and
${\llbracket{}{\beta}\rrbracket}(\mathfrak{A},v,V,G)=\prod_{a\in
A}{\llbracket{}{\delta}\rrbracket}(\mathfrak{A},v[a/x],V,G)$. Thus, if we
assume that ${\llbracket{}{\beta}\rrbracket}(\mathfrak{A},v,V,F)>0$, then
${\llbracket{}{\delta}\rrbracket}(\mathfrak{A},v[a/x],V,F)>0$ for every $a\in
A$. Hence, by induction hypothesis we have that
${\llbracket{}{\delta}\rrbracket}(\mathfrak{A},v[a/x],V,G)>0$ for every $a\in
A$, and, therefore, we conclude that
${\llbracket{}{\beta}\rrbracket}(\mathfrak{A},v,V,G)>0$.

In the particular case of an ${\rm RQFO}({\rm FO})$-formula $[{\bf
lsfp}\,\beta(\bar{x},h)]$, Lemma 19 tell us that if $f,g\in\mathcal{F}$ and
$\text{\rm supp}(f)\subseteq\text{\rm supp}(g)$, then $\text{\rm
supp}(T_{\beta}(f))\subseteq\text{\rm supp}(T_{\beta}(g))$. Hence, as for the
case of LFP, this lemma gives us a simple way to compute a least s-fixed point
of $T_{\beta}$. Let $f_{0}\in\mathcal{F}$ be a function such that
$f_{0}(\bar{a})=0$ for every $\bar{a}\in A^{\ell}$ (i.e. $f_{0}$ is the only
function with empty support), and let function $f_{i+1}$ be defined as
$T_{\beta}(f_{i})$ for every $i\in\mathbb{N}$. Then there exists $j\geq 0$
such that $\text{\rm supp}(f_{j})=\text{\rm supp}(T_{\beta}(f_{j}))$. Let $k$
be the smallest natural number such that $\text{\rm supp}(f_{k})=\text{\rm
supp}(T_{\beta}(f_{k}))$. We have that $f_{k}$ is a least s-fixed point of
$T_{\beta}$, which is used to define the semantics of $[{\bf
lsfp}\,\beta(\bar{x},h)]$. More specifically, for an arbitrary first-order
assignment $v$ for $\mathfrak{A}$:

$\displaystyle{\llbracket{}{[{\bf
lsfp}\,\beta(\bar{x},h)]}\rrbracket}(\mathfrak{A},v)$
$\displaystyle=f_{k}(v(\bar{x})).$

We would like to define an ${\rm RQFO}({\rm FO})$-formula that, given a
directed acyclic graph $G$ with $n$ nodes and a pair of nodes $b$, $c$ in $G$,
counts the number of paths of length less than $n$ from $b$ to $c$ in $G$. To
this end, assume that graphs are encoded using the signature
$\mathbf{R}=\\{E(\cdot,\cdot),<\\}$, and then define formula $\alpha(x,y,f)$
as follows:

$\displaystyle E(x,y)+\Sigma{z}.\,f(x,z)\cdot E(z,y).$ (10)

We have that $[{\bf lsfp}\,\alpha(x,y,f)]$ defines our counting function. In
fact, assume that $\mathfrak{A}$ is an $\mathbf{R}$-structure with $n$
elements in its domain encoding an acyclic directed graph. Moreover, assume
that $b,c$ are elements of $\mathfrak{A}$ and $v$ is a first-order assignment
over $\mathfrak{A}$ such that $v(x)=b$ and $v(y)=c$. Then we have that
${\llbracket{}{[{\bf lsfp}\,\alpha(x,y,f)]}\rrbracket}(\mathfrak{A},v)$ is
equal to the number of paths in $\mathfrak{A}$ from $b$ to $c$ of length at
most $n-1$.

Assume now that we need to count the number of paths of length less than $n$
from a node $b$ to a node $c$ in a directed graph that is not necessarily
acyclic. Then we cannot use formula (10), as the fixed point could be reached
too soon without counting all paths of length at most $n-1$. The fixed point
of (10) is always reached after $k$ steps, where $k$ is the size of the
maximum shortest path between two vertices in the graph. If the graph has a
cycle in it, there might be paths of size $k^{\prime}\in\\{k+1,\ldots,n-1\\}$
that would not be counted because the fixed point was reached earlier. Thus,
we need a more involved formula in the general case, which is given below.

Suppose that $\varphi_{\text{\rm first}}(x)$ and $\varphi_{\text{succ}}(x,y)$
are ${\rm FO}$-formulae defining the first element of $<$ and the successor
relation associated to $<$, respectively. Moreover, define formula
$\beta(x,y,t,g)$ as follows:

$\displaystyle(E(x,y)+\Sigma{z}.\,g(x,z,t)\cdot E(z,y))\cdot\varphi_{\text{\rm
first}}(t)\
+\Sigma{t^{\prime}}.\,\varphi_{\text{succ}}(t^{\prime},t)\cdot\left(\Sigma{x^{\prime}}.\,\Sigma{y^{\prime}}.\,g(x^{\prime},y^{\prime},t^{\prime})\right)$

Then our extended counting function is defined by:

$\Sigma{t}.\,(\varphi_{\text{\rm first}}(t)\cdot[{\bf
lsfp}\,\beta(x,y,t,g)]).$

In fact, the number of paths of length at most $n$ from a node $x$ to a node
$y$ is recursively computed by using the formula
$(E(x,y)+\Sigma{z}.\,g(x,z,t)\cdot E(z,y))\cdot\varphi_{\text{\rm first}}(t)$,
which stores this value in $g(x,y,t)$ with $t$ the first element in the
domain. The other formula
$\Sigma{t^{\prime}}.\,\varphi_{\text{succ}}(t^{\prime},t)\cdot\left(\Sigma{x^{\prime}}.\,\Sigma{y^{\prime}}.\,g(x^{\prime},y^{\prime},t^{\prime})\right)$
is just an auxiliary artifact that is used as a counter to allow reaching a
fixed point in the support of $g$ in $n$ steps. Notice that the use of the
filter $\varphi_{\text{succ}}(t^{\prime},t)$ prevents this formula for
incrementing the value of $g(x,y,t)$ when $t$ is the first element in the
domain. ∎

In contrast to ${\rm LFP}$, to reach a fixed point we do not need to impose
any positive restriction on the formula $\beta(\bar{x},h)$. In fact, since
$\beta$ is constructed from monotone operations (sum and product) over the
natural numbers, the resulting operator $T_{\beta}$ is monotone as well.

Now that a least fixed point operator over functions is defined, the next step
is to understand its expressive power. In the following theorem, we show that
this operator can be used to capture FP.

######  Theorem 20.

${\rm RQFO}({\rm FO})$ captures FP over ordered structures.

######  Proof 6.2.

Given the definition of the semantics of ${\rm RQFO}({\rm FO})$, it is clear
that a fixed formula $[{\bf lsfp}\,\beta(\bar{x},h)]$ can be evaluated in
polynomial time, from which it is possible to conclude that each fixed formula
in ${\rm RQFO}({\rm FO})$ can be evaluated in polynomial time. Thus, to prove
that ${\rm RQFO}({\rm FO})$ captures FP, we only need to prove the second
condition in Definition 4.

Let $f$ be a function in FP. We address the case when $f$ is defined for the
encodings of the structures of a relational signature
$\mathbf{R}=\\{E(\cdot,\cdot)\\}$, as the proof for an arbitrary signature is
analogous. Let $M$ be a deterministic polynomial-time TM with a working tape
and an output tape, such that the output of $M$ on input ${\rm
enc}(\mathfrak{A})$ is $f({\rm enc}(\mathfrak{A}))$ for each
$\mathbf{R}$-structure $\mathfrak{A}$. We assume that
$M=(Q,\\{0,1\\},q_{0},\delta)$, where $Q=\\{q_{0},\ldots,q_{\ell}\\}$, and
$\delta\colon Q\times\\{0,1,\mathtt{B},\vdash\\}\to
Q\times\\{0,1,\mathtt{B},\vdash\\}\times\\{\leftarrow,\rightarrow\\}\times\\{0,1,\emptyset\\}$
is a partial function. In particular, the tapes of $M$ are infinite to the
right so the symbol $\vdash$ is used to indicate the first position in each
tape, and $M$ does not have any final states, as it produces an output for
each input. Moreover, the only allowed operations in the output tape are: (1)
writing 0 and moving the head one cell to the right, (2) writing 1 and moving
the head one cell to the right, or (3) doing nothing. These operations are
represented by 0, 1, and $\emptyset$, respectively. Finally, assume that $M$,
on input ${\rm enc}(\mathfrak{A})$ with domain $A=\\{1,\dots,n\\}$, executes
exactly $n^{k}$ steps on large inputs for a fixed $k\geq 1$. We ignore small
inputs since they can be handled separately.

We construct a formula $\alpha$ in an extension of the grammar of ${\rm
RQFO}({\rm FO})$ such that
${\llbracket{}{\alpha}\rrbracket}(\mathfrak{A})=f({\rm enc}(\mathfrak{A}))$
for each $\mathbf{R}$-structure $\mathfrak{A}$. This extension allows defining
the operator ${\bf lsfp}$ for multiple functions, analogously to the notion of
simultaneous LFP [Lib04]. Let $\bar{x}=(x_{1},\ldots,x_{k})$ and
$\bar{t}=(t_{1},\ldots,t_{k})$. Then $\alpha$ is defined as:

$\displaystyle\alpha\ =\ \Sigma{\bar{t}}.\,[{\bf lsfp}\,\text{\it
out}(\bar{t}):\,$
$\displaystyle\alpha_{T_{0}}(\bar{t},\bar{x},T_{0},T_{1},T_{\mathtt{B}},T_{\vdash},h,\hat{h},s_{q_{0}},\ldots,s_{q_{\ell}},\text{\it
out}),$
$\displaystyle\alpha_{T_{1}}(\bar{t},\bar{x},T_{0},T_{1},T_{\mathtt{B}},T_{\vdash},h,\hat{h},s_{q_{0}},\ldots,s_{q_{\ell}},\text{\it
out}),$
$\displaystyle\alpha_{T_{\mathtt{B}}}(\bar{t},\bar{x},T_{0},T_{1},T_{\mathtt{B}},T_{\vdash},h,\hat{h},s_{q_{0}},\ldots,s_{q_{\ell}},\text{\it
out}),$
$\displaystyle\alpha_{T_{\vdash}}(\bar{t},\bar{x},T_{0},T_{1},T_{\mathtt{B}},T_{\vdash},h,\hat{h},s_{q_{0}},\ldots,s_{q_{\ell}},\text{\it
out}),$
$\displaystyle\alpha_{h}(\bar{t},\bar{x},T_{0},T_{1},T_{\mathtt{B}},T_{\vdash},h,\hat{h},s_{q_{0}},\ldots,s_{q_{\ell}},\text{\it
out}),$
$\displaystyle\alpha_{\hat{h}}(\bar{t},\bar{x},T_{0},T_{1},T_{\mathtt{B}},T_{\vdash},h,\hat{h},s_{q_{0}},\ldots,s_{q_{\ell}},\text{\it
out}),$
$\displaystyle\alpha_{s_{q_{0}}}(\bar{t},T_{0},T_{1},T_{\mathtt{B}},T_{\vdash},h,\hat{h},s_{q_{0}},\ldots,s_{q_{\ell}},\text{\it
out}),$ $\displaystyle\vdots$
$\displaystyle\alpha_{s_{q_{\ell}}}(\bar{t},T_{0},T_{1},T_{\mathtt{B}},T_{\vdash},h,\hat{h},s_{q_{0}},\ldots,s_{q_{\ell}},\text{\it
out}),$ $\displaystyle\alpha_{\text{\it
out}}(\bar{t},T_{0},T_{1},T_{\mathtt{B}},T_{\vdash},h,\hat{h},s_{q_{0}},\ldots,s_{q_{\ell}},\text{\it
out})]\cdot\operatorname{last}(\bar{t}).$

In this formula, $T_{0},T_{1},T_{\mathtt{B}},T_{\vdash},h,\hat{h}$ are
functions symbols of arity $2\cdot k$, while
$s_{q_{0}},\ldots,s_{q_{\ell}},\text{\it out}$ are function symbols of arity
$k$. For each one of these function symbols $f$, there is a formula
$\alpha_{f}$ defining how the values of $f$ are updated when computing the
fixed point. For example, $\alpha_{T_{0}}$ is used to define the values of
function $T_{0}$. Notice that the values of each function in $\alpha$ depend
on the values of the other functions, which is why we talk about a
simultaneous computation. Besides, notice that the notation $[{\bf
lsfp}\,\text{\it out}(\bar{t}):\ldots]$ is used to indicate that (1) the free
variables of the formula are $\bar{t}=(t_{1},\ldots,t_{k})$, and (2) once the
least fixed point has been computed, the value of $[{\bf lsfp}\,\text{\it
out}(\bar{t}):\ldots]$ for an assignment $\bar{a}$ to $\bar{t}$ is given by
the value (in the fixed point) of function out on $\bar{a}$. Finally, it is
important to notice that $\alpha$ can be transformed into a proper ${\rm
RQFO}({\rm FO})$ formula by using the same techniques used to prove that
simultaneous LFP has the same expressiveness as LFP [Lib04]; in particular,
functions symbols
$T_{0},T_{1},T_{\mathtt{B}},T_{\vdash},h,\hat{h},s_{q_{0}},\ldots,s_{q_{\ell}},\text{\it
out}$ are replaced by a single function $f$ of arity $6\cdot 2\cdot
k+(\ell+1)\cdot k+k=(\ell+14)\cdot k$.

In the formula $\alpha$, function $T_{0}$ is used to indicate whether the
content of a cell of the working tape is 0 at a certain point of time, that
is, $T_{0}(\bar{t},\bar{x})>0$ if the cell at position $\bar{x}$ of the
working tape contains the symbol 0 at step $\bar{t}$, and
$T_{0}(\bar{t},\bar{x})=0$ otherwise. Functions $T_{1}$, $T_{\mathtt{B}}$ and
$T_{\vdash}$ are defined analogously. Function $h$ is used to indicate whether
the head of the working tape is in a specific position at a certain point of
time, that is, $h(\bar{t},\bar{x})>0$ if the head of the working tape is at
position $\bar{x}$ at step $\bar{t}$, and $h(\bar{t},\bar{x})=0$ otherwise.
Function $\hat{h}$ is used to indicate whether the head of the working tape is
not in a position at a particular point of time, that is,
$\hat{h}(\bar{t},\bar{x})>0$ if the head of the working tape is not at
position $\bar{x}$ at step $\bar{t}$, and $\hat{h}(\bar{t},\bar{x})=0$
otherwise. For each $i\in\\{0,\ldots,\ell\\}$, function $s_{q_{i}}$ is used to
indicate whether the TM $M$ is in state $q_{i}$ at a certain point of time,
that is, $s_{q_{i}}(\bar{t})>0$ if the TM $M$ is in state $q_{i}$ at step
$\bar{t}$, and $s_{q_{i}}(\bar{t})=0$ otherwise. Function out stores the
output of the TM $M$; in particular, $\text{\it out}(\bar{t})$ is the value
returned by $M$ when $\bar{t}$ is the last step. Finally, assuming that
$\varphi_{\text{\rm last}}(x)$ is an ${\rm FO}$-formula defining the last
element of $<$, we have that
$\operatorname{last}(\bar{t})=\bigwedge_{i=1}^{k}\varphi_{\text{\rm
last}}(t_{i})$, that is, $\operatorname{last}(\bar{t})$ holds if $\bar{t}$ is
the last step. Therefore, the use of $\operatorname{last}(\bar{t})$ in
$\alpha$ allows us to return the output of the TM $M$.

As in Example 6, assume that $\varphi_{\text{\rm first}}(x)$ is an ${\rm
FO}$-formula defining the first element of $<$. Moreover, assume that
$\operatorname{first}(\bar{t})$ and
$\operatorname{succ}(\bar{t},\bar{t^{\prime}})$ are ${\rm FO}$-formulae such
that $\operatorname{first}(\bar{t})$ holds if $\bar{t}$ is the first step and
$\operatorname{succ}(\bar{t},\bar{t^{\prime}})$ holds if $\bar{t}^{\prime}$ is
the successor step of $\bar{t}$ (that is, $\operatorname{succ}(\cdot,\cdot)$
is the successor relation associated to the lexicographical order induced by
$<$ on the tuples with $k$ elements). Then formula $\alpha_{T_{\vdash}}$ is
defined as follows:

$\alpha_{T_{\vdash}}(\bar{t},\bar{x},T_{0},T_{1},T_{\mathtt{B}},T_{\vdash},h,\hat{h},s_{q_{0}},\ldots,s_{q_{\ell}},\text{\it
out})=\\\
(\operatorname{first}(\bar{t})\wedge\operatorname{first}(\bar{x}))+\Sigma{\bar{t}^{\prime}}.\,(\text{succ}(\bar{t}^{\prime},\bar{t})\cdot\hat{h}(\bar{t}^{\prime},\bar{x})\cdot
T_{\vdash}(\bar{t}^{\prime},\bar{x}))\ +\\\
\sum_{(q,a)\,:\,\delta(q,a)=(\\_,\vdash,\\_,\\_)}\Sigma{\bar{t}^{\prime}}.\,(\text{succ}(\bar{t}^{\prime},\bar{t})\cdot
h(\bar{t}^{\prime},\bar{x})\cdot T_{a}(\bar{t}^{\prime},\bar{x})\cdot
s_{q}(\bar{t}^{\prime})).$

Notation $\sum_{(q,a)\,:\,\delta(q,a)=(\\_,\vdash,\\_,\\_)}$ in this formula
is used to indicate that we are considering a sum over all pairs $(q,a)\in
Q\times\\{0,1,\mathtt{B},\vdash\\}$ such that
$\delta(q,a)=(q^{\prime},\vdash,u,v)$ for some $q^{\prime}\in Q$,
$u\in\\{\leftarrow,\rightarrow\\}$ and $v\in\\{0,1,\emptyset\\}$. Formulae
$\alpha_{T_{0}}$, $\alpha_{T_{1}}$ and $\alpha_{T_{\mathtt{B}}}$ are defined
analogously; for the sake of presentation, we only show here how
$\alpha_{T_{0}}$ is defined, assuming that $\bar{y}=(y_{1},\ldots,y_{k})$:

$\alpha_{T_{0}}(\bar{t},\bar{x},T_{0},T_{1},T_{\mathtt{B}},T_{\vdash},h,\hat{h},s_{q_{0}},\ldots,s_{q_{\ell}},\text{\it
out})=\\\
(\operatorname{first}(\bar{t})\wedge\exists\bar{y}(\varphi_{\text{\rm
first}}(y_{1})\wedge\cdots\wedge\varphi_{\text{\rm first}}(y_{k-2})\wedge\neg
E(y_{k-1},y_{k})\wedge\text{succ}(\bar{y},\bar{x})))\ +\\\
\Sigma{\bar{t}^{\prime}}.\,(\text{succ}(\bar{t}^{\prime},\bar{t})\cdot\hat{h}(\bar{t}^{\prime},\bar{x})\cdot
T_{0}(\bar{t}^{\prime},\bar{x}))+\\\
\sum_{(q,a)\,:\,\delta(q,a)=(\\_,0,\\_,\\_)}\Sigma{\bar{t}^{\prime}}.\,(\text{succ}(\bar{t}^{\prime},\bar{t})\cdot
h(\bar{t}^{\prime},\bar{x})\cdot T_{a}(\bar{t}^{\prime},\bar{x})\cdot
s_{q}(\bar{t}^{\prime})).$

Notice that in the initial step, the encoding of the structure $\mathfrak{A}$
has to be placed on the working tape of $M$ from the second position since the
symbol $\vdash$ is placed in the first position. This is the reason why we use
tuple $\bar{y}$ and define $\bar{x}$ as the successor of $\bar{y}$. Formula
$\alpha_{h}$ is defined as follows:

$\displaystyle\alpha_{h}(\bar{t},\bar{x},$ $\displaystyle
T_{0},T_{1},T_{\mathtt{B}},T_{\vdash},h,\hat{h},s_{q_{0}},\ldots,s_{q_{\ell}},\text{\it
out})=$
$\displaystyle(\operatorname{first}(\bar{t})\wedge\text{succ}(\bar{t},\bar{x}))+$
$\displaystyle\sum_{(q,a)\,:\,\delta(q,a)=(\\_,\\_,\leftarrow,\\_)}\Sigma{\bar{t}^{\prime}}.\,\Sigma{\bar{x}^{\prime}}.\,(\text{succ}(\bar{t}^{\prime},\bar{t})\cdot\text{succ}(\bar{x},\bar{x}^{\prime})\cdot
h(\bar{t}^{\prime},\bar{x}^{\prime})\cdot
T_{a}(\bar{t}^{\prime},\bar{x}^{\prime})\cdot s_{q}(\bar{t}^{\prime}))\ +$
$\displaystyle\sum_{(q,a)\,:\,\delta(q,a)=(\\_,\\_,\rightarrow,\\_)}\Sigma{\bar{t}^{\prime}}.\,\Sigma{\bar{x}^{\prime}}.\,(\text{succ}(\bar{t}^{\prime},\bar{t})\cdot\text{succ}(\bar{x}^{\prime},\bar{x})\cdot
h(\bar{t}^{\prime},\bar{x}^{\prime})\cdot
T_{a}(\bar{t}^{\prime},\bar{x}^{\prime})\cdot s_{q}(\bar{t}^{\prime})).$

Similarly, formula $\alpha_{\hat{h}}$ is defined as follows:

$\displaystyle\alpha_{\hat{h}}(\bar{t},\bar{x},$ $\displaystyle
T_{0},T_{1},T_{\mathtt{B}},T_{\vdash},h,\hat{h},s_{q_{0}},\ldots,s_{q_{\ell}},\text{\it
out})=$
$\displaystyle(\operatorname{first}(\bar{t})\wedge\neg\text{succ}(\bar{t},\bar{x}))+$
$\displaystyle\sum_{(q,a)\,:\,\delta(q,a)=(\\_,\\_,\leftarrow,\\_)}\Sigma{\bar{t}^{\prime}}.\,\Sigma{\bar{x}^{\prime}}.\,\Sigma{\bar{x}^{\prime\prime}}.\,(\text{succ}(\bar{t}^{\prime},\bar{t})\cdot
h(\bar{t}^{\prime},\bar{x}^{\prime})\cdot
T_{a}(\bar{t}^{\prime},\bar{x}^{\prime})\cdot s_{q}(\bar{t}^{\prime})\,\cdot$
$\displaystyle\hskip
250.0pt\text{succ}(\bar{x}^{\prime\prime},\bar{x}^{\prime})\cdot(\bar{x}\neq\bar{x}^{\prime\prime}))\
+$
$\displaystyle\sum_{(q,a)\,:\,\delta(q,a)=(\\_,\\_,\rightarrow,\\_)}\Sigma{\bar{t}^{\prime}}.\,\Sigma{\bar{x}^{\prime}}.\,\Sigma{\bar{x}^{\prime\prime}}.\,(\text{succ}(\bar{t}^{\prime},\bar{t})\cdot
h(\bar{t}^{\prime},\bar{x}^{\prime})\cdot
T_{a}(\bar{t}^{\prime},\bar{x}^{\prime})\cdot s_{q}(\bar{t}^{\prime})\,\cdot$
$\displaystyle\hskip
250.0pt\text{succ}(\bar{x}^{\prime},\bar{x}^{\prime\prime})\cdot(\bar{x}\neq\bar{x}^{\prime\prime})).$

Notice that in the definition of $\alpha_{\hat{h}}$, ${\rm FO}$-formula
$\bar{x}\neq\bar{x}^{\prime\prime}$ is used to indicate that tuples $\bar{x}$
and $\bar{x}^{\prime\prime}$ are distinct (that is, there exists
$i\in\\{1,\ldots,k\\}$ such that the $i$-th components of $\bar{x}$ and
$\bar{x}^{\prime\prime}$ are distinct). Formula $\alpha_{s_{q_{0}}}$ is
defined as:

$\alpha_{s_{q_{0}}}(\bar{t},T_{0},T_{1},T_{\mathtt{B}},T_{\vdash},h,\hat{h},s_{q_{0}},\ldots,s_{q_{\ell}},\text{\it
out})\ =\\\ \operatorname{first}(\bar{t})\ +\
\sum_{(q,a)\,:\,\delta(q,a)=(q_{0},\\_,\\_,\\_)}\Sigma{\bar{t}^{\prime}}.\,\Sigma{\bar{x}^{\prime}}.\,(\text{succ}(\bar{t}^{\prime},\bar{t})\cdot
h(\bar{t}^{\prime},\bar{x}^{\prime})\cdot
T_{a}(\bar{t}^{\prime},\bar{x}^{\prime})\cdot s_{q}(\bar{t}^{\prime})).$

Moreover, for every $i\in\\{1,\ldots,\ell\\}$, formula $\alpha_{s_{q_{i}}}$ is
defined analogously. Finally, formula $\alpha_{\text{\it out}}$ is defined as:

$\displaystyle\alpha_{\text{\it out}}($
$\displaystyle\bar{t},T_{0},T_{1},T_{\mathtt{B}},T_{\vdash},h,\hat{h},s_{q_{0}},\ldots,s_{q_{\ell}},\text{\it
out})=$
$\displaystyle\sum_{(q,a)\,:\,\delta(q,a)=(\\_,\\_,\\_,0)}\Sigma{\bar{t}^{\prime}}.\,\Sigma{\bar{x}^{\prime}}.\,(\text{succ}(\bar{t}^{\prime},\bar{t})\cdot
h(\bar{t}^{\prime},\bar{x}^{\prime})\cdot
T_{a}(\bar{t}^{\prime},\bar{x}^{\prime})\cdot s_{q}(\bar{t}^{\prime})\cdot
2\cdot\text{\it out}(\bar{t}^{\prime}))\ +$
$\displaystyle\sum_{(q,a)\,:\,\delta(q,a)=(\\_,\\_,\\_,1)}\Sigma{\bar{t}^{\prime}}.\,\Sigma{\bar{x}^{\prime}}.\,(\text{succ}(\bar{t}^{\prime},\bar{t})\cdot
h(\bar{t}^{\prime},\bar{x}^{\prime})\cdot
T_{a}(\bar{t}^{\prime},\bar{x}^{\prime})\cdot
s_{q}(\bar{t}^{\prime})\cdot(2\cdot\text{\it out}(\bar{t}^{\prime})+1))\ +$
$\displaystyle\sum_{(q,a)\,:\,\delta(q,a)=(\\_,\\_,\\_,\emptyset)}\Sigma{\bar{t}^{\prime}}.\,\Sigma{\bar{x}^{\prime}}.\,(\text{succ}(\bar{t}^{\prime},\bar{t})\cdot
h(\bar{t}^{\prime},\bar{x}^{\prime})\cdot
T_{a}(\bar{t}^{\prime},\bar{x}^{\prime})\cdot
s_{q}(\bar{t}^{\prime})\cdot\text{\it out}(\bar{t}^{\prime})).$

Clearly, tuple $\bar{t}$ encodes the number of steps the machine has done and
in each iteration of the fixed point operator, one timestep of the machine is
executed. Assume that $\bar{a}$, $\bar{a}^{\prime}$ are tuples with $k$
elements such that $\bar{a}^{\prime}$ is the successor of $\bar{a}$. From the
construction of the formula, and since the machine is deterministic, it can be
seen that for each function
$f\in\\{T_{0},T_{1},T_{\mathtt{B}},T_{\vdash},h,\hat{h}\\}$, at the
$\bar{a}$-th iteration of the fixed point operator, it holds that
$f(\bar{a},\bar{b})\leq 1$ and $f(\bar{a}^{\prime},\bar{b})=0$ for every
$\bar{b}\in A^{k}$. In the same way, it can be seen that (1) for each function
$g\in\\{s_{q_{1}},\ldots,s_{q_{\ell}}\\}$, at the $\bar{a}$-th iteration of
the fixed point operator, it holds that $g(\bar{a})\leq 1$ and
$g(\bar{a}^{\prime})=0$, that (2) for each $\bar{b}$, only one of the
functions $T_{0}$,$T_{1}$,$T_{B}$,$T_{\vdash}$ outputs 1 on input
($\bar{a},\bar{b})$, (3) for each $\bar{b}$, only one of the functions
$h,\hat{h}$ outputs 1 on input $(\bar{a},\bar{b})$, (4) there is exactly one
$\bar{b}$ with $h(\bar{a},\bar{b})=1$, and (5) there is exactly one $i$ such
that $s_{q_{i}}(\bar{a})=1$. From this, we have that at the iteration
$\bar{a}^{\prime}$ of the fixed point operator, $\text{\it
out}(\bar{a}^{\prime})$ is equal to either $2\cdot\text{\it out}(\bar{a})$,
$2\cdot\text{\it out}(\bar{a})+1$, or $\text{\it out}(\bar{a})$, which
represents precisely the value in the output tape at each step of $M$ running
on the input ${\rm enc}(\mathfrak{A})$. From this argument, it can be seen
that ${\llbracket{}{\alpha}\rrbracket}(\mathfrak{A})=f({\rm
enc}(\mathfrak{A}))$, which concludes the proof of the theorem.

Our last goal in this section is to use the new characterization of FP to
explore classes below it. It was shown in [Imm86, Imm88] that ${\rm FO}$
extended with a transitive closure operator captures NL. Inspired by this
work, we show that a restricted version of ${\rm RQFO}$ can be used to capture
#L, the counting version of NL. Specifically, we use ${\rm RQFO}$ to define an
operator for counting the number of paths in a directed graph, which is what
is needed to capture #L.

Given a relational signature $\mathbf{R}$, the set of transitive ${\rm QFO}$
formulae (${\rm TQFO}$-formulae) is defined as the extension of ${\rm QFO}$ by
the additional operator $[{\bf path}\,\,\psi(\bar{x},\bar{y})]$, where
$\psi(\bar{x},\bar{y})$ is an ${\rm FO}$-formula over $\mathbf{R}$, and
$\bar{x}=(x_{1},\ldots,x_{k})$, $\bar{y}=(y_{1},\ldots,y_{k})$ are tuples of
pairwise distinct first-order variables. The semantics of $[{\bf
path}\,\,\psi(\bar{x},\bar{y})]$ can easily be defined in terms of ${\rm
RQFO}({\rm FO})$ as follows. Given an $\mathbf{R}$-structure $\mathfrak{A}$
with domain $A$, define a (directed) graph
$\mathcal{G}_{\psi}(\mathfrak{A})=(N,E)$ such that $N=A^{k}$ and for every
pair $\bar{b},\bar{c}\in N$, it holds that $(\bar{b},\bar{c})\in E$ if, and
only if, $\mathfrak{A}\models\psi(\bar{b},\bar{c})$. As was the case for
Example 6, we can count the paths of length at most $|A^{k}|$ in
$\mathcal{G}_{\psi}(\mathfrak{A})$ with the formula
$\beta_{\psi(\bar{x},\bar{y})}(\bar{x},\bar{y},\bar{t},g)$:

$\displaystyle(\psi(\bar{x},\bar{y})+\Sigma{\bar{z}}.\,g(\bar{x},\bar{z},\bar{t})\cdot\psi(\bar{z},\bar{y}))\cdot\varphi_{\text{\rm
first-lex}}(\bar{t})\ +\Sigma{\bar{t}^{\prime}}.\,\varphi_{\text{succ-
lex}}(\bar{t}^{\prime},\bar{t})\cdot\left(\Sigma{\bar{x}^{\prime}}.\,\Sigma{\bar{y}^{\prime}}.\,g(\bar{x}^{\prime},\bar{y}^{\prime},\bar{t}^{\prime})\right),$

where $\varphi_{\text{\rm first-lex}}$ and $\varphi_{\text{succ-lex}}$ are
${\rm FO}$-formulae defining the first and successor predicates over tuples in
$A^{k}$, following the lexicographic order induced by $<$. Then the semantics
of the path operator can be defined by using the following definition of
$[{\bf path}\,\,\psi(\bar{x},\bar{y})]$ in ${\rm RQFO}$:

$\displaystyle[{\bf path}\,\,\psi(\bar{x},\bar{y})]$ $\displaystyle:=$
$\displaystyle\Sigma{\bar{t}}.\,(\varphi_{\text{\rm first}}(\bar{t})\cdot[{\bf
lsfp}\,\beta_{\psi(\bar{x},\bar{y})}(\bar{x},\bar{y},\bar{t},g)]).$

In other words, ${\llbracket{}{[{\bf
path}\,\,\psi(\bar{x},\bar{y})]}\rrbracket}(\mathfrak{A},v)$ counts the number
of paths from $v(\bar{x})$ to $v(\bar{y})$ in the graph
$\mathcal{G}_{\psi}(\mathfrak{A})$ whose length is at most $|A^{k}|$. As
mentioned before, the operator for counting paths is exactly what we need to
capture #L.

######  Theorem 21.

${\rm TQFO}({\rm FO})$ captures #L over ordered structures.

######  Proof 6.3.

First, we show that every formula in ${\rm TQFO}({\rm FO})$ defines a function
that is in #L. Let $\mathbf{R}$ be a relational signature and $\alpha$ a
formula over $\mathbf{R}$ in ${\rm TQFO}({\rm FO})$. We construct a
logarithmic-space nondeterministic Turing Machine $M_{\alpha}$ that on input
$({\rm enc}(\mathfrak{A}),v)$, where $\mathfrak{A}$ is an
$\mathbf{R}$-structure and $v$ is a first-order assignment for $\mathfrak{A}$,
has ${\llbracket{}{\alpha}\rrbracket}(\mathfrak{A},v)$ accepting runs (so that
we can conclude that the function defined by $\alpha$ is in #L). Suppose that
the domain of $\mathfrak{A}$ is $A=\\{1,\ldots,n\\}$. The TM $M_{\alpha}$
needs $\ell\cdot\log_{2}(n)$ bits of memory to store the first-order variables
that appear in $\alpha$, where $\ell$ is the number of different variables in
this formula (and also the size of the domain of $v$). If $\alpha=\varphi$,
where $\varphi$ is an ${\rm FO}$-formula, then we check if
$(\mathfrak{A},v)\models\varphi$ in deterministic logarithmic space, and
accept if and only if this condition holds. If $\alpha=s$, where $s$ is a
fixed natural number, then we generate $s$ branches and accept in all of them.
If $\alpha=(\alpha_{1}+\alpha_{2})$, we simulate $M_{\alpha_{1}}$ and
$M_{\alpha_{2}}$ on separate branches. If
$\alpha=(\alpha_{1}\cdot\alpha_{2})$, we simulate $M_{\alpha_{1}}$ and if it
accepts, then instead of accepting we simulate $M_{\alpha_{2}}$. If
$\alpha=\Sigma{x}.\,\beta$, for each $a\in A$ we generate a different branch
where we simulate $M_{\beta}$ with input $v[a/x]$. If $\alpha=\Pi{x}.\,\beta$,
we simulate $M_{\beta}$ with input $v[1/x]$, and on each accepting run,
instead of accepting we simulate $M_{\beta}$ with input $v[2/x]$, and so on.
If $\alpha=[{\bf path}\,\,\varphi(\bar{x},\bar{y})]$, where $\varphi$ is an
${\rm FO}$-formula, we simulate the #L procedure that counts the number of
paths of a given length from a source to a target node in an input graph
(where the length is at most the number of nodes in the graph).

Second, we show that every function in #L can be encoded by a formula in ${\rm
TQFO}({\rm FO})$. Let $f$ be a function in #L and $M$ a logarithmic-space
nondeterministic Turing Machine such that $\text{\rm\\#accept}_{M}({\rm
enc}(\mathfrak{A}))=f({\rm enc}(\mathfrak{A}))$. We assume that $M$ has only
one accepting state, and that no transition is defined for this state.
Moreover, we assume that there exists only one accepting configuration. We
make use of transitive closure logic (${\rm TC}$) to simplify our proof
[Grä07]. We have that ${\rm TC}$ captures NL[Imm83], so that there exists a
formula $\varphi$ in ${\rm TC}$ such that $\mathfrak{A}\models\varphi$ if and
only if $M$ accepts ${\rm enc}(\mathfrak{A})$. This formula can be expressed
as:

$\varphi=\exists\bar{u}\exists\bar{z}(\psi_{\text{initial}}(\bar{u})\wedge\psi_{\text{acc}}(\bar{z})\wedge[{\bf
tc}_{\bar{x},\bar{y}}\,\psi_{\text{next}}(\bar{x},\bar{y})](\bar{u},\bar{z})),$

where $\psi_{\text{initial}}(\bar{u})$ is an ${\rm FO}$-formula that indicates
that $\bar{u}$ is the initial configuration, $\psi_{\text{acc}}(\bar{z})$ is
an ${\rm FO}$-formula that indicates that $\bar{z}$ is an accepting
configuration, and $\psi_{\text{next}}(\bar{x},\bar{y})$ is an ${\rm
FO}$-formula that indicates that $\bar{y}$ is a successor configuration of
$\bar{x}$ [Grä07]. Here, there is a one-to-one correspondence between
configurations of $M$ and assignments to $\bar{z}$. As a consequence, given a
structure $\mathfrak{A}$ and a first-order assignment $v$ for $\mathfrak{A}$,
where $v(\bar{x})$ is the starting configuration and $v(\bar{y})$ is the sole
accepting configuration, the value of ${\llbracket{}{[{\bf
path}\,\,\psi_{\text{next}}(\bar{x},\bar{y})]}\rrbracket}(\mathfrak{A},v)$ is
equal to $\text{\rm\\#accept}_{M}({\rm enc}(\mathfrak{A}))$. Therefore, the
${\rm TQFO}({\rm FO})$-formula
$\alpha=\Sigma{\bar{u}}.\,\Sigma{\bar{z}}.\,(\psi_{\text{initial}}(\bar{u})\cdot\psi_{\text{acc}}(\bar{z})\cdot[{\bf
path}\,\,\psi_{\text{next}}(\bar{u},\bar{z})])$ satisfies that
${\llbracket{}{\alpha}\rrbracket}(\mathfrak{A})=f({\rm enc}(\mathfrak{A}))$.
This concludes the proof of the theorem.

This last result perfectly illustrates the benefits of our logical framework
for the development of descriptive complexity for counting complexity classes.
The distinction in the language between the Boolean and the quantitative level
allows us to define operators at the latter level that cannot be defined at
the former. As an example showing how fundamental this separation is, consider
the issue of extending ${\rm QFO}({\rm FO})$ at the Boolean level in order to
capture #L. The natural alternative to do this is to use ${\rm FO}$ extended
with a transitive closure operator, which is denoted by ${\rm TC}$. But then
the problem is that for every language $L\in\text{\sc NL}$, it holds that its
characteristic function $\chi_{L}$ is in ${\rm QFO}({\rm TC})$, where
$\chi_{L}(x)=1$ if $x\in L$, and $\chi_{L}(x)=0$ otherwise. Thus, if we assume
that ${\rm QFO}({\rm TC})$ captures #L (over ordered structures), then we have
that $\chi_{L}\in\text{\sc\\#L}$ for every $L\in\text{\sc NL}$. This would
imply that $\text{\sc NL}=\text{\sc UL}$,555A decision language $L$ is in UL
is there exists a logarithmic-space NTM $M$ accepting $L$ and satisfying that
$\text{\rm\\#accept}_{M}(x)=1$ for every $x\in L$. solving an outstanding open
problem [RA97].

##  7\. Concluding remarks and future work

We proposed a framework based on Weighted Logics to develop a descriptive
complexity theory for complexity classes of functions. We consider the results
of this paper as a first step in this direction. Consequently, there are
several directions for future research, some of which are mentioned here. TotP
is an interesting counting complexity class as it naturally defines a class of
functions in #P with easy decision counterparts. However, we do not have a
logical characterization of this class. Similarly, we are missing logical
characterizations of other fundamental complexity classes such as SpanL
[ÀJ93]. We would also like to define a larger syntactic subclass of #P where
each function admits an FPRAS; notice that #PerfectMatching is an important
problem admitting an FPRAS[JSV04] that is not included in the classes defined
in Section 5.2. Moreover, by following the approach proposed in [Imm83], we
would like to include second-order free variables in the operator for counting
paths introduced in Section 6, in order to have alternative ways to capture
FPSPACE and even #P.

Finally, an open problem is to understand the connection of this framework
with enumeration complexity classes. For example, in [DS11] the enumeration of
assignments for first-order formulas was studied following the $\\#{\rm
FO}$-hierarchy, and in [ABJM17] the efficient enumeration (i.e. constant delay
enumeration [Seg13]) was shown for a particular class of circuits. It would be
interesting then to adapt the $\Sigma{\rm QSO}({\rm FO})$-hierarchy for the
context of enumeration and identify subclasses that also admit good properties
in terms of enumeration.

##  8\. Acknowledgements

The authors are grateful to Luis Alberto Croquevielle for providing the proof
of Proposition 17. This research has been supported by the Fondecyt grant
1161473 and the Millennium Institute for Foundational Research on Data.

## References

  * [AB09] Sanjeev Arora and Boaz Barak.  Computational complexity: a modern approach.  Cambridge University Press, 2009.
  * [ABJM17] Antoine Amarilli, Pierre Bourhis, Louis Jachiet, and Stefan Mengel.  A circuit-based approach to efficient enumeration.  In 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, pages 111:1–111:15, 2017.
  * [ÀJ93] Carme Àlvarez and Birgit Jenner.  A very hard log-space counting class.  Theor. Comput. Sci., 107(1):3–30, 1993.
  * [ALM+98] Sanjeev Arora, Carsten Lund, Rajeev Motwani, Madhu Sudan, and Mario Szegedy.  Proof verification and the hardness of approximation problems.  J. ACM, 45(3):501–555, 1998.
  * [AMR17] Marcelo Arenas, Martin Muñoz, and Cristian Riveros.  Descriptive complexity for counting complexity classes.  In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1–12, 2017\.
  * [AV89] Serge Abiteboul and Victor Vianu.  Fixpoint extensions of first-order logic and datalog-like languages.  In Proceedings of LICS’89, pages 71–79, 1989.
  * [BCP+17] Eleni Bakali, Aggeliki Chalki, Aris Pagourtzis, Petros Pantavos, and Stathis Zachos.  Completeness results for counting problems with easy decision.  In Algorithms and Complexity - 10th International Conference, CIAC 2017, Athens, Greece, May 24-26, 2017, Proceedings, pages 55–66, 2017\.
  * [CG96] Kevin J. Compton and Erich Grädel.  Logical definability of counting functions.  J. Comput. Syst. Sci., 53(2):283–297, 1996.
  * [DFJ02] Martin E. Dyer, Alan M. Frieze, and Mark Jerrum.  On counting independent sets in sparse graphs.  SIAM J. Comput., 31(5):1527–1541, 2002.
  * [DG07] Manfred Droste and Paul Gastin.  Weighted automata and weighted logics.  Theor. Comput. Sci., 380(1-2):69–86, 2007.
  * [DHK05] Arnaud Durand, Miki Hermann, and Phokion G. Kolaitis.  Subtractive reductions and complete problems for counting complexity classes.  Theor. Comput. Sci., 340(3):496–513, 2005.
  * [DHKV16] Arnaud Durand, Anselm Haak, Juha Kontinen, and Heribert Vollmer.  Descriptive complexity of #ac0 functions.  In 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France, pages 20:1–20:16, 2016.
  * [DKV09] Manfred Droste, Werner Kuich, and Heiko Vogler.  Handbook of weighted automata.  Springer Science & Business Media, 2009.
  * [DS11] Arnaud Durand and Yann Strozecki.  Enumeration Complexity of Logical Query Problems with Second-order Variables.  In Marc Bezem, editor, Computer Science Logic (CSL’11) - 25th International Workshop/20th Annual Conference of the EACSL, volume 12 of Leibniz International Proceedings in Informatics (LIPIcs), pages 189–202, Dagstuhl, Germany, 2011. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.
  * [Ete97] Kousha Etessami.  Counting quantifiers, successor relations, and logarithmic space.  J. Comput. Syst. Sci., 54(3):400–411, 1997.
  * [Fag74] Ronald Fagin.  Generalized first-order spectra and polynomial-time recognizable sets.  Complexity of Computation, SIAM-AMS Proceedings, (7):43–73, 1974\.
  * [Fag75] Ronald Fagin.  Monadic generalized spectra.  Math. Log. Q., 21(1):89–96, 1975.
  * [FFK94] Stephen A. Fenner, Lance Fortnow, and Stuart A. Kurtz.  Gap-definable counting classes.  J. Comput. Syst. Sci., 48(1):116–148, 1994.
  * [FH08] Piotr Faliszewski and Lane A. Hemaspaandra.  The consequences of eliminating NP solutions.  Comp. Sci. Review, 2(1):40–54, 2008.
  * [For97] Lance Fortnow.  Counting complexity.  In Complexity Theory Retrospective II, pages 81–107. Springer, 1997\.
  * [GG98] Erich Grädel and Yuri Gurevich.  Metafinite model theory.  Inf. Comput., 140(1):26–81, 1998.
  * [Gil77] John Gill.  Computational complexity of probabilistic turing machines.  SIAM J. Comput., 6(4):675–695, 1977.
  * [Grä92] Erich Grädel.  Capturing complexity classes by fragments of second-order logic.  Theor. Comput. Sci., 101(1):35–57, 1992.
  * [Grä07] Erich Grädel.  Finite model theory and descriptive complexity.  In Finite Model Theory and Its Applications, pages 125–230. Springer, 2007.
  * [GS90] Michelangelo Grigni and Michael Sipser.  Monotone complexity.  In Proceedings of LMS Workshop on Boolean Function Complexity, 1990\.
  * [HO13] Lane Hemaspaandra and Mitsunori Ogihara.  The complexity theory companion.  Springer Science & Business Media, 2013.
  * [HV95] Lane A. Hemaspaandra and Heribert Vollmer.  The satanic notations: counting classes beyond #P and other definitional adventures.  SIGACT News, 26(1):2–13, 1995.
  * [IL90] Neil Immerman and Eric Lander.  Describing graphs: a first order approach to graph canonization.  In Alan L. Selman, editor, Complexity Theory Retrospective, pages 59–81. Springer-Verlag, 1990.
  * [Imm82] Neil Immerman.  Relational queries computable in polynomial time (extended abstract).  In Proceedings of the fourteenth annual ACM symposium on Theory of computing, pages 147–152, 1982.
  * [Imm83] Neil Immerman.  Languages which capture complexity classes (preliminary report).  In Proceedings of STOC’83, pages 347–354, 1983.
  * [Imm86] Neil Immerman.  Relational queries computable in polynomial time.  Information and Control, 68(1-3):86–104, 1986.
  * [Imm88] Neil Immerman.  Nondeterministic space is closed under complementation.  SIAM J. Comput., 17(5):935–938, 1988.
  * [Imm99] Neil Immerman.  Descriptive complexity.  Graduate texts in computer science. Springer, 1999.
  * [JSV04] Mark Jerrum, Alistair Sinclair, and Eric Vigoda.  A polynomial-time approximation algorithm for the permanent of a matrix with nonnegative entries.  J. ACM, 51(4):671–697, 2004.
  * [KL83] Richard M. Karp and Michael Luby.  Monte-carlo algorithms for enumeration and reliability problems.  In Proceedings of FOCS’83, pages 56–64, 1983.
  * [Kre88] Mark W Krentel.  The complexity of optimization problems.  Journal of computer and system sciences, 36(3):490–509, 1988.
  * [KT94] Phokion G Kolaitis and Madhukar N Thakur.  Logical definability of NP optimization problems.  Information and Computation, 115(2):321–353, 1994.
  * [Lad89] Richard E. Ladner.  Polynomial space counting problems.  SIAM J. Comput., 18(6):1087–1097, 1989.
  * [Lib04] Leonid Libkin.  Elements of Finite Model Theory.  Springer, 2004.
  * [OH93] Mitsunori Ogiwara and Lane A. Hemachandra.  A complexity theory for feasible closure properties.  J. Comput. Syst. Sci., 46(3):295–325, 1993.
  * [Pap94] Christos H. Papadimitriou.  Computational complexity.  Addison-Wesley, 1994.
  * [PY91] Christos H. Papadimitriou and Mihalis Yannakakis.  Optimization, approximation, and complexity classes.  J. Comput. Syst. Sci., 43(3):425–440, 1991.
  * [PZ06] Aris Pagourtzis and Stathis Zachos.  The complexity of counting functions with easy decision version.  In Proceedings of MFCS’06, pages 741–752, 2006.
  * [RA97] Klaus Reinhardt and Eric Allender.  Making nondeterminism unambiguous.  Electronic Colloquium on Computational Complexity (ECCC), 4(14), 1997.
  * [Seg13] Luc Segoufin.  Enumerating with constant delay the answers to a query.  In Joint 2013 EDBT/ICDT Conferences, ICDT ’13 Proceedings, Genoa, Italy, March 18-22, 2013, pages 10–20, 2013.
  * [SST95] Sanjeev Saluja, K. V. Subrahmanyam, and Madhukar N. Thakur.  Descriptive Complexity of #P Functions.  J. Comput. Syst. Sci., 50(3):493–505, 1995.
  * [Val79a] Leslie G. Valiant.  The complexity of computing the permanent.  Theor. Comput. Sci., 8:189–201, 1979.
  * [Val79b] Leslie G. Valiant.  The complexity of enumeration and reliability problems.  SIAM J. Comput., 8(3):410–421, 1979.
  * [Var82] Moshe Vardi.  The complexity of relational query languages.  In Proceedings of STOC’82, pages 137–146, 1982.
  * [VW95] Heribert Vollmer and Klaus W Wagner.  Complexity classes of optimization functions.  Inf. and Comp., 120(2):198–219, 1995.