
\section{Proofs for \cref{sec:main}}
\subsection{Proof of \cref{lemma:next}}
We first observe the following helpful result:
\begin{lemma}\label{obs:nextins}
	Let $\partial = \ins{\zeta}{u}$ and let $x \leadsto_{w} y$ for $x,y \in D$. We have that $x \not\leadsto_{w'} y$ if and only if $x<u<y$.
\end{lemma}
\begin{proof}
	Let $\zeta \in \Sigma$, if we perform the update $\ins{\zeta}{u}$ on $\mathcal{W}$ where $x<u<y$ then it follows that there exists some $z$ such that $w'(z) \neq \varepsilon$ and $x<z<y$. Therefore it cannot be the case that $x \leadsto_{w'} y$, so $x \not\leadsto_{w'} y$.
	
	If it is not the case that $x<u<y$ then it cannot be that there exists some $z \in D$ such that $x<z<y$ where $w'(z) \neq \varepsilon$. Therefore, if $x \leadsto_{w} y$ and $\partial = \ins{\zeta}{u}$ then $x \not\leadsto_{w'} y$ if and only if $x<u<y$.
\end{proof}
\subsubsection{Actual proof of \cref{lemma:next}}
\input{proof-nextsymbol.tex}



\subsection{Proof of \cref{lemma:eqsubstr}}
We first observe two results which help us in the actual proof of \cref{lemma:eqsubstr}:


\begin{lemma}
\label{obs:next}
If $y \leadsto_{w} z$ then $w[x,y] \cdot w[z,v] = w[x,v]$ where $x,y,z,v \in D$.
\end{lemma}
\begin{proof}
Because $y \leadsto_{w} z$ it follows that $w[y+1,z-1] = \varepsilon$. Since we can write $w[x,v]$ as $w[x,y] \cdot w[y+1,z-1] \cdot w[z,v]$ and because $w[y+1,z-1] = \varepsilon$, it follows that $w[x,y] \cdot w[z,v] = w[x,v]$.
\end{proof}

\begin{lemma}
\label{obs:insert}
If $w[x_1,y_1] = w[x_2,y_2]$ and we perform $\ins{\zeta}{u}$ then $w'[x_1,y_1] \neq w'[x_2,y_2]$ if $x_1 < u < y_1$ or $x_2 < u < y_2$.
\end{lemma}
\begin{proof}
If $x_1 < u < y_1$ then it follows that $|w'[x_1,y_1]| = |w[x_1,y_1]| + 1$ but since $w'[x_2,y_2]| = |w[x_2,y_2]|$ it follows that $w'[x_1,y_1] \neq w'[x_2,y_2]$. The reasoning for when $x_2 < u < y_2$ is analogous.

There is the case when $w(u) \neq \varepsilon$ and $x_1 < u < y_1$ or $x_2 < u < y_2$. However since we have the restriction that an update \emph{must} change the word (i.\,e.\xspace we cannot perform $\ins{\zeta}{u}$ if $w(u) = \zeta$), this case is trivial.
\end{proof}

\subsubsection{Actual proof of \cref{lemma:eqsubstr}}
\input{proof-equalsubstr.tex}












\section{Proofs for \cref{sec:main}}
\subsection{Proof of \cref{lemma:next}}
We first observe the following helpful result:
\begin{lemma}\label{obs:nextins}
	Let $\partial = \ins{\zeta}{u}$ and let $x \leadsto_{w} y$ for $x,y \in D$. We have that $x \not\leadsto_{w'} y$ if and only if $x<u<y$.
\end{lemma}
\begin{proof}
	Let $\zeta \in \Sigma$, if we perform the update $\ins{\zeta}{u}$ on $\mathcal{W}$ where $x<u<y$ then it follows that there exists some $z$ such that $w'(z) \neq \varepsilon$ and $x<z<y$. Therefore it cannot be the case that $x \leadsto_{w'} y$, so $x \not\leadsto_{w'} y$.
	
	If it is not the case that $x<u<y$ then it cannot be that there exists some $z \in D$ such that $x<z<y$ where $w'(z) \neq \varepsilon$. Therefore, if $x \leadsto_{w} y$ and $\partial = \ins{\zeta}{u}$ then $x \not\leadsto_{w'} y$ if and only if $x<u<y$.
\end{proof}
\subsubsection{Actual proof of \cref{lemma:next}}
\input{proof-nextsymbol.tex}



\subsection{Proof of \cref{lemma:eqsubstr}}
We first observe two results which help us in the actual proof of \cref{lemma:eqsubstr}:


\begin{lemma}
\label{obs:next}
If $y \leadsto_{w} z$ then $w[x,y] \cdot w[z,v] = w[x,v]$ where $x,y,z,v \in D$.
\end{lemma}
\begin{proof}
Because $y \leadsto_{w} z$ it follows that $w[y+1,z-1] = \varepsilon$. Since we can write $w[x,v]$ as $w[x,y] \cdot w[y+1,z-1] \cdot w[z,v]$ and because $w[y+1,z-1] = \varepsilon$, it follows that $w[x,y] \cdot w[z,v] = w[x,v]$.
\end{proof}

\begin{lemma}
\label{obs:insert}
If $w[x_1,y_1] = w[x_2,y_2]$ and we perform $\ins{\zeta}{u}$ then $w'[x_1,y_1] \neq w'[x_2,y_2]$ if $x_1 < u < y_1$ or $x_2 < u < y_2$.
\end{lemma}
\begin{proof}
If $x_1 < u < y_1$ then it follows that $|w'[x_1,y_1]| = |w[x_1,y_1]| + 1$ but since $w'[x_2,y_2]| = |w[x_2,y_2]|$ it follows that $w'[x_1,y_1] \neq w'[x_2,y_2]$. The reasoning for when $x_2 < u < y_2$ is analogous.

There is the case when $w(u) \neq \varepsilon$ and $x_1 < u < y_1$ or $x_2 < u < y_2$. However since we have the restriction that an update \emph{must} change the word (i.\,e.\xspace we cannot perform $\ins{\zeta}{u}$ if $w(u) = \zeta$), this case is trivial.
\end{proof}

\subsubsection{Actual proof of \cref{lemma:eqsubstr}}
\input{proof-equalsubstr.tex}











\section{Introduction}\label{sec:intro}
\input{sec-intro}
\section{Preliminaries}\label{sec:prelim}
\input{sec-prelim}
\section{Core Spanners are in \ifmmode{\mathsf{DynCQ}}\else{\textsf{DynCQ}}\xspace\fi}\label{sec:main}
\input{sec-main}
\section{Relations in \ifmmode{\mathsf{SpLog}}\else{\textsf{SpLog}}\xspace\fi and \ifmmode{\mathsf{DynCQ}}\else{\textsf{DynCQ}}\xspace\fi}\label{sec:rel}
\input{sec-rel}
\section{Conclusions}\label{sec:conc}
\input{sec-conc}

\newpage














\subsection{Document Spanners and Spanner Algebra}\label{sec:spanners}

\input{sec-prelim-spanners}

\subsection{Spanner Logic}\label{sec:splog}

\input{sec-prelim-splog}

\subsection{Dynamic complexity}\label{sec:dyn}

\input{sec-prelim-dyn}



\subsubsection{Primitive Spanner Representations}\label{sec:spanner-rep}
Let $w := a_1 \cdot a_2 \cdots a_n$ be a word, where $n \geq 0$ and $a_1,\dots,a_n \in \Sigma$. A \emph{span} of $w$ is an interval $\spn{i,j}$ with $1 \leq i \leq j \leq n+1$ and $i,j \geq 0$. Given a span $\spn{i,j}$ of a word $w$, we define the subword $w_{\spn{i,j}}$ as $a_i \cdot a_{i+1} \cdots a_{j-1}$.
\begin{example}
Consider the word 
$w:= \mathtt{banana}$.	As $|w|=6$, the spans of $w$ are the $\spn{i,j}$ with $1\leq i \leq j\leq 7$. For example, we have $w_{\spn{1,2}}=\mathtt{b}$ and $w_{\spn{2,4}}=w_{\spn{4,6}}=\mathtt{an}$. Although both spans describe the same subword \texttt{an}, the two occurrences are at different locations (and, thus, at different spans). Analogously, we have $w_{\spn{1,1}}=w_{\spn{2,2}}=\cdots=w_{\spn{7,7}}=\varepsilon$, but $\spn{i,i}\neq \spn{i',i'}$ for all distinct $1\leq i,i'\leq 7$.
\end{example}

Let  $V \subseteq \Xi$ and  $w \in \Sigma^*$. A $(V,w)$\emph{-tuple} is a function $\mu$ that maps each  $x\in V$ to a span $\mu(x)$ of $w$. A set of $(V,w)$-tuples is called a  $(V,w)$\emph{-relation}. A \emph{spanner} P is a function that maps every $w \in \Sigma^*$ to a $(V,w)$-relation~$P(w)$. 
We write $\SVars{P}$ to denote the set of variables $V$ of a spanner~$P$. 
Two spanners $P_1$ and $P_2$ are \emph{equivalent} if $\SVars{P_1} = \SVars{P_2}$ and  $P_1(w) = P_2(w)$ holds for all $w \in \Sigma^*$.

In the usual applications of spans and spanners, the word $w$ is some type of text. Hence, we can view a spanner $P$ as mapping an input text $w$ to a $(V,w)$-relation  $P(w)$, which can be understood as a table of spans of $w$. 

To define spanners, we use two types of \emph{primitive spanner representations}, the so-called \emph{regex formulas} and \emph{variable-set automata}. Both extend classical mechanisms for regular languages (regular expressions and NFAs, respectively) with variables.  
\subparagraph*{Regex formulas:}
The syntax of regex formulas is defined by the following
$\alpha := \emptyset \mid \varepsilon \mid a \mid (\alpha \lor \alpha) \mid (\alpha \cdot \alpha) \mid (\alpha)^* \mid x \{ \alpha \}, $
where $a \in \Sigma$ and $x \in \Xi$. We use $\alpha^+$ to denote $\alpha \cdot \alpha^*$. 

Like~\cite{fre:splog}, we define the  semantics of regex formulas using two step-semantics with  \emph{ref-words} (originally introduced by Schmid~\cite{sch:cha} in a different context). A ref-word is a word over the extended alphabet $(\Sigma \cup \Gamma)$ where $\Gamma := \{ \openvar{x}, \closevar{x} \mid x \in \Xi \}$. The symbols $\openvar{x}$ and $\closevar{x}$ represent the beginning and end of the span for the variable $x$. 
The first step in the definition of semantics is treating each regex formula $\alpha$ as generators of languages of ref-words $\rlang(\alpha)\subseteq (\Sigma \cup \Gamma)^*$, which  is defined by $\rlang(\emptyset) := \emptyset$, $\rlang(a) := \{ a \}$ where $a \in \Sigma \cup \{ \varepsilon \}$, $\rlang(\alpha_1 \lor \alpha_2) := \rlang(\alpha_1) \cup \rlang(\alpha_2)$, $\rlang(\alpha_1 \cdot \alpha_2) := \rlang(\alpha_1) \cdot \rlang(\alpha_2)$, $\rlang(\alpha^*) := \rlang(\alpha)^*$, and $\rlang(x\{ \alpha \}) := \openvar{x} \rlang(\alpha) \closevar{x}$.

Let $\SVars{\alpha}$ be the set of all $x \in \Xi$ such that $x\{ \}$ occurs somewhere in $\alpha$. A ref-word $r \in \rlang(\alpha)$ is \emph{valid} if for all $x \in \SVars{\alpha}$, we have that $|r|_{\openvar{x}} = 1$. 
We denote the set of valid ref-words in $\rlang(\alpha)$ as $\validr{\alpha}$ and say that 
a regex formula is \emph{functional} if $\rlang(\alpha) = \validr{\alpha}$. 
We write $\mathsf{RGX}$ for the set of all functional regex formulas. 
By definition,  for  every $\alpha\in\mathsf{RGX}$, every $r \in \validr{\alpha}$, and  every $x \in \SVars{\alpha}$, there is  a unique factorization $r = r_1 \openvar{x} r_2 \closevar{x} r_3$. 

This allows us to define the second step of the semantics, which turns such a  factorization for some variable $x$ into a span $\mu(x)$. To this end, we define a morphism $\mathsf{clr} \colon (\Sigma \cup \Gamma)^* \rightarrow \Sigma^*$ by $\mathsf{clr}(a) := a $ for $a \in \Sigma$ and $\mathsf{clr}(g) = \varepsilon$ for all $g \in \Gamma$. 
For a  factorization $r = r_1 \openvar{x} r_2 \closevar{x} r_3$, $\mathsf{clr}(r_1)$ is the substring of $w$ that appears before $\mu(x)$ and $\mathsf{clr}(r_2)$ is the substring $w_{\mu(x)}$.

We use this for the definition of the semantics as follows: 
For $\alpha \in \mathsf{RGX}$ and $w \in \Sigma^*$, let $V := \SVars{\alpha}$ and (more importantly) $\validr{\alpha, w} := \{ r \in \validr{\alpha} \mid \mathsf{clr}(r)=w \}$.

Every $r \in \validr{\alpha,w}$ defines a $(V,w)$-tuple $\mu^r$ in the following way: For every $x \in \SVars{\alpha}$, we use  the unique factorization $r = r_1 \openvar{x} r_2 \closevar{x} r_3$ to define $\mu^r(x) := \spn{|\mathsf{clr}(r_1)|+1, |\mathsf{clr}(r_1 r_2)|+1	}$. 
The spanner $\spanner{\alpha}$ is then defined by $\spanner{\alpha}(w) := \{ \mu^r \mid r \in \validr{\alpha,w} \} $ for all $w\in\Sigma^*$.

\subparagraph*{Variable-set automata:} Variable-set automata (short: \emph{vset-automata}) are NFAs that may use variable operations $\openvar{x}$ and $\closevar{x}$ as  transitions. More formally, let  $V \subset \Xi$ be a finite set of variables. 
 A variable-set automaton over $\Sigma$ with variables $V$ is a tuple $A = (Q, q_0, q_f , \delta)$, where $Q$ is the set of states, $q_0 \in Q$ is the initial state, $q_f \in Q$ is the accepting state, and $\delta \colon Q \times (\Sigma \cup \{ \varepsilon \} \cup \Gamma_V) \rightarrow \powerset{Q}$ is the transition function with $\Gamma_V := \{ \openvar{x}, \closevar{x} \mid x \in V \}$. 
 
We define the semantics using a two-step approach analogous to the semantic definition of regex formulas. 
 Firstly, we treat $A$ as an NFA that defines the ref-language defined by $\rlang(A):=\{ r \in (\Sigma \cup \Gamma_V)^* \mid q_f \in \delta^*(q_0, r) \}$, where 
 the function $\delta^* \colon Q \times (\Sigma \cup \Gamma_V) \rightarrow \powerset{Q}$ is defined such that for all $p,q \in Q$ and $r \in (\Sigma \cup \Gamma_V)^*$, $q \in \delta^*(p,r)$ if and only if there exists a path in $A$ from $p$ to $q$ with the label $r$. 

Secondly, let $\SVars{A}$ be the set of $x \in V$ such that $\openvar{x}$ or $\closevar{x}$ appears in $A$. A ref-word $r \in \rlang(A)$ is \emph{valid} if for every $x \in \SVars{A}$, $|r|_{\openvar{x}} = |r|_{\closevar{x}}=1$, and $\openvar{x}$ always occurs to the left of $\closevar{x}$. Then $\validr{A}$, $\validr{A,w}$ and $\spanner{A}$ are defined analogously to regex formulas. We denote the set of all vset-automata using $\mathsf{VA_{set}}$. As for regex formulas, a vset-automaton $A\in\mathsf{VA_{set}}$ is called \emph{functional} if $\rlang(A)=\validr{A}$.

\begin{example}\label{ex:regexAutomaton}
We define the functional regex formula 
$\alpha:=\Sigma^*\cdot x\{(\mathtt{wine})\lor(\mathtt{cake})\}\cdot\Sigma^*$. We also define the functional vset-automaton~$A$ as follows:
\begin{center}
	\begin{tikzpicture}[on grid, node distance =12mm,every loop/.style={shorten >=0pt}, every state/.style={inner sep=0pt,minimum size=5mm}]
	\node[state,initial text=,initial by arrow] (q0) {};
	\node[state, right= of q0] (q1) {};
	\node[state, above right=of q1] (b1) {};
	\node[state, right=of b1] (b2) {};
	\node[state, right=of b2] (b3) {};

	\node[state, below right=of q1] (c1) {};
		\node[state, right=of c1] (c2) {};
		\node[state, right=of c2] (c3) {};
	\node[state, below right=of b3] (q3) {};
	\node[state,accepting,right=of q3] (q4) {};	\path[->]
	(q0) edge [loop above] node {$\Sigma$} (q0)
	(q0) edge node[above] {$\openvar{x}$} (q1)
	(q1) edge[pos=0.2] node[above] {$\mathtt{w}$} (b1)
	(b1) edge[] node[above] {$\mathtt{i}$} (b2)
	(b2) edge[] node[above] {$\mathtt{n}$} (b3)
	(b3) edge[] node[above] {$\mathtt{e}$} (q3)
	(q1) edge[pos=0.2] node[below] {$\mathtt{c}$} (c1)
(c1) edge[] node[below] {$\mathtt{a}$} (c2)
(c2) edge[] node[below] {$\mathtt{k}$} (c3)
(c3) edge[] node[below] {$\mathtt{e}$} (q3)
	(q3) edge node[above] {$\closevar{x}$} (q4)
(q4) edge [loop above] node {$\Sigma$} (q4)
	;
	\end{tikzpicture}
\end{center}  
For all $w\in\Sigma^*$, we have that $\spanner{\alpha}(w)=\spanner{A}(w)$ contains exactly those $(\{x\},w)$-tuples $\mu$ that have $w_{\mu(x)}=\mathtt{wine}$ or $w_{\mu(x)}=\mathtt{cake}$.
\end{example}

\subsubsection{Spanner Algebra}\label{sec:spannerAlgebra}
We now introduce an algebra on spanners in order to construct more complex spanners.

\begin{definition}
Two spanners $P_1$ and $P_2$ are \emph{compatible} if $\SVars{P_1}=\SVars{P_2}$.
We define  the following algebraic operators for all spanners $P, P_1, P_2$:
\begin{itemize}
	\item If $P_1$ and $P_2$ are compatible, their \emph{union} $(P_1 \cup P_2)$ and their \emph{difference} $(P_1\setminus P_2)$ are defined by $(P_1 \cup P_2)(w) := P_1(w) \cup P_2(w)$ and $(P_1 \setminus P_2)(w) := P_1(w) \setminus P_2(w)$.
	\item The \emph{projection} $\pi_Y P$ for $Y \subseteq \SVars{P}$ is defined by $\pi_Y P(w) := P|_Y(w)$, where $P|_Y(w)$ is the restriction of all $\mu \in P(w)$ to~$Y$.
	\item The \emph{natural join} $P_1 \bowtie P_2$ is obtained by defining each $(P_1 \bowtie P_2)(w)$ as the set of all  $(V_1 \cup V_2,w)$-tuples $\mu$ for which there exists $\mu_1 \in P_1(w)$ and $\mu_2 \in P_2(w)$ with $\mu|_{V_1}(w) = \mu_1(w)$ and $\mu|_{V_2}(w) = \mu_2(w)$, where $V_i := \SVars{P_i}$ for $i \in \{ 1,2 \}$.   
	\item For every  $k$-ary relation $R \subseteq (\Sigma^*)^k$ and variables $x_1, \dots, x_k \in \SVars{P}$, the \emph{selection}  $\upxi^R_{x_1 \dots x_k}P$ is defined by
	$\upxi^R_{x_1 \dots x_k} P(w):= \{\mu \in P(w) \mid (w_{\mu(x_1)} , \dots , w_{\mu(x_k)}) \in R\}$ for $w\in\Sigma^*$.
\end{itemize}
Let  $\SVars{P_1 \cup P_2} := \SVars{P_1\setminus P_2}:=\SVars{P_1}=\SVars{P_2}$,   $\SVars{\pi_Y P} := Y$,  $\SVars{P_1 \bowtie P_2} := \SVars{P_1} \cup \SVars{P_2}$, and $\SVars{\upxi^R_{x_1 \dots x_k}} := \SVars{P}$.
\end{definition}

 Note that the relations $R$ in the selection are usually infinite; and they are never considered part of the input.

Let $O$ be a spanner algebra and let $C$ be a class of primitive spanner representations, then we use $C^O$ to denote the set of all spanner representations that can be constructed by repeated combinations of the symbols for the operators from $O$ with the spanner representation from~$C$. We denote the closure of $\spanner{C}$ under the spanner operators $O$ as $\spanner{C^O}$. 
\begin{example}

Let $\alpha_1:= \Sigma^*x\{\Sigma^*\}\Sigma^*y\{\Sigma^*\}\Sigma^*$ and $\alpha_2:=\Sigma^*\cdot x\{(\mathtt{wine})\lor(\mathtt{cake})\}\cdot\Sigma^*$ (recall Example~\ref{ex:regexAutomaton}). We combine the two regex formulas into a core spanner $P := \pi_{x}\upxi^=_{x,y} (\alpha_1\bowtie\alpha_2)$. Then $\spanner{P}(w)$ contains all $(\{x\},w)$-tuples $\mu$ such that $w_{\mu(x)}$ is an occurrence of \texttt{wine} or \texttt{cake} in $w$ that is followed by another occurrence of the same word.
\end{example}

Like  Fagin et al. \cite{fag:spa}, we are mostly concerned with string equality selections $\upxi^=$. Following~$\cite{fag:spa,pet:rec}$, we focus on the class  of \emph{regular spanners} $\spanner{\rgx^{\spanreg}}$, the class of  \emph{core spanners}\footnote{As this class captures the core functionality of SystemT.}  $\spanner{\rgx^{\core}}$ 
and the class of \emph{generalized core spanners}  $\spanner{\rgx^{\cored}}$, where 
$\mathsf{reg}:=\{\pi,\cup,\bowtie\}$ and  $\mathsf{core} := \{ \pi, \upxi^=, \cup, \bowtie\}$. 
As shown in~\cite{fag:spa}, we have
\[ \spanner{\rgx^{\spanreg}}=\spanner{\mathsf{VA}_{\mathsf{set}}^{\spanreg}} =\spanner{\mathsf{VA_{set}}}  \subset  \spanner{\rgx^{\core}}=\spanner{\mathsf{VA}_{\mathsf{set}}^{\core}}\subset \spanner{\rgx^{\cored}}=\spanner{\mathsf{VA}_{\mathsf{set}}^{\cored}}. \]
In other words, there is a proper hierarchy of regular, core, and generalized core spanners; and for each of the classes, we can choose regex formulas or vset-automata as primitive spanner representations. As shown in~\cite{fre:splog}, functional vset-automata have the same expressive power as vset-automata in general. The size difference can be exponential, but this does not matter for the purpose of the present paper.




\section{Introduction}\label{sec:intro}
\input{sec-intro}
\section{Preliminaries}\label{sec:prelim}
\input{sec-prelim}
\section{Core Spanners are in \ifmmode{\mathsf{DynCQ}}\else{\textsf{DynCQ}}\xspace\fi}\label{sec:main}
\input{sec-main}
\section{Relations in \ifmmode{\mathsf{SpLog}}\else{\textsf{SpLog}}\xspace\fi and \ifmmode{\mathsf{DynCQ}}\else{\textsf{DynCQ}}\xspace\fi}\label{sec:rel}
\input{sec-rel}
\section{Conclusions}\label{sec:conc}
\input{sec-conc}

\newpage















\subsubsection{Primitive Spanner Representations}\label{sec:spanner-rep}
Let $w := a_1 \cdot a_2 \cdots a_n$ be a word, where $n \geq 0$ and $a_1,\dots,a_n \in \Sigma$. A \emph{span} of $w$ is an interval $\spn{i,j}$ with $1 \leq i \leq j \leq n+1$ and $i,j \geq 0$. Given a span $\spn{i,j}$ of a word $w$, we define the subword $w_{\spn{i,j}}$ as $a_i \cdot a_{i+1} \cdots a_{j-1}$.
\begin{example}
Consider the word 
$w:= \mathtt{banana}$.	As $|w|=6$, the spans of $w$ are the $\spn{i,j}$ with $1\leq i \leq j\leq 7$. For example, we have $w_{\spn{1,2}}=\mathtt{b}$ and $w_{\spn{2,4}}=w_{\spn{4,6}}=\mathtt{an}$. Although both spans describe the same subword \texttt{an}, the two occurrences are at different locations (and, thus, at different spans). Analogously, we have $w_{\spn{1,1}}=w_{\spn{2,2}}=\cdots=w_{\spn{7,7}}=\varepsilon$, but $\spn{i,i}\neq \spn{i',i'}$ for all distinct $1\leq i,i'\leq 7$.
\end{example}

Let  $V \subseteq \Xi$ and  $w \in \Sigma^*$. A $(V,w)$\emph{-tuple} is a function $\mu$ that maps each  $x\in V$ to a span $\mu(x)$ of $w$. A set of $(V,w)$-tuples is called a  $(V,w)$\emph{-relation}. A \emph{spanner} P is a function that maps every $w \in \Sigma^*$ to a $(V,w)$-relation~$P(w)$. 
We write $\SVars{P}$ to denote the set of variables $V$ of a spanner~$P$. 
Two spanners $P_1$ and $P_2$ are \emph{equivalent} if $\SVars{P_1} = \SVars{P_2}$ and  $P_1(w) = P_2(w)$ holds for all $w \in \Sigma^*$.

In the usual applications of spans and spanners, the word $w$ is some type of text. Hence, we can view a spanner $P$ as mapping an input text $w$ to a $(V,w)$-relation  $P(w)$, which can be understood as a table of spans of $w$. 

To define spanners, we use two types of \emph{primitive spanner representations}, the so-called \emph{regex formulas} and \emph{variable-set automata}. Both extend classical mechanisms for regular languages (regular expressions and NFAs, respectively) with variables.  
\subparagraph*{Regex formulas:}
The syntax of regex formulas is defined by the following
$\alpha := \emptyset \mid \varepsilon \mid a \mid (\alpha \lor \alpha) \mid (\alpha \cdot \alpha) \mid (\alpha)^* \mid x \{ \alpha \}, $
where $a \in \Sigma$ and $x \in \Xi$. We use $\alpha^+$ to denote $\alpha \cdot \alpha^*$. 

Like~\cite{fre:splog}, we define the  semantics of regex formulas using two step-semantics with  \emph{ref-words} (originally introduced by Schmid~\cite{sch:cha} in a different context). A ref-word is a word over the extended alphabet $(\Sigma \cup \Gamma)$ where $\Gamma := \{ \openvar{x}, \closevar{x} \mid x \in \Xi \}$. The symbols $\openvar{x}$ and $\closevar{x}$ represent the beginning and end of the span for the variable $x$. 
The first step in the definition of semantics is treating each regex formula $\alpha$ as generators of languages of ref-words $\rlang(\alpha)\subseteq (\Sigma \cup \Gamma)^*$, which  is defined by $\rlang(\emptyset) := \emptyset$, $\rlang(a) := \{ a \}$ where $a \in \Sigma \cup \{ \varepsilon \}$, $\rlang(\alpha_1 \lor \alpha_2) := \rlang(\alpha_1) \cup \rlang(\alpha_2)$, $\rlang(\alpha_1 \cdot \alpha_2) := \rlang(\alpha_1) \cdot \rlang(\alpha_2)$, $\rlang(\alpha^*) := \rlang(\alpha)^*$, and $\rlang(x\{ \alpha \}) := \openvar{x} \rlang(\alpha) \closevar{x}$.

Let $\SVars{\alpha}$ be the set of all $x \in \Xi$ such that $x\{ \}$ occurs somewhere in $\alpha$. A ref-word $r \in \rlang(\alpha)$ is \emph{valid} if for all $x \in \SVars{\alpha}$, we have that $|r|_{\openvar{x}} = 1$. 
We denote the set of valid ref-words in $\rlang(\alpha)$ as $\validr{\alpha}$ and say that 
a regex formula is \emph{functional} if $\rlang(\alpha) = \validr{\alpha}$. 
We write $\mathsf{RGX}$ for the set of all functional regex formulas. 
By definition,  for  every $\alpha\in\mathsf{RGX}$, every $r \in \validr{\alpha}$, and  every $x \in \SVars{\alpha}$, there is  a unique factorization $r = r_1 \openvar{x} r_2 \closevar{x} r_3$. 

This allows us to define the second step of the semantics, which turns such a  factorization for some variable $x$ into a span $\mu(x)$. To this end, we define a morphism $\mathsf{clr} \colon (\Sigma \cup \Gamma)^* \rightarrow \Sigma^*$ by $\mathsf{clr}(a) := a $ for $a \in \Sigma$ and $\mathsf{clr}(g) = \varepsilon$ for all $g \in \Gamma$. 
For a  factorization $r = r_1 \openvar{x} r_2 \closevar{x} r_3$, $\mathsf{clr}(r_1)$ is the substring of $w$ that appears before $\mu(x)$ and $\mathsf{clr}(r_2)$ is the substring $w_{\mu(x)}$.

We use this for the definition of the semantics as follows: 
For $\alpha \in \mathsf{RGX}$ and $w \in \Sigma^*$, let $V := \SVars{\alpha}$ and (more importantly) $\validr{\alpha, w} := \{ r \in \validr{\alpha} \mid \mathsf{clr}(r)=w \}$.

Every $r \in \validr{\alpha,w}$ defines a $(V,w)$-tuple $\mu^r$ in the following way: For every $x \in \SVars{\alpha}$, we use  the unique factorization $r = r_1 \openvar{x} r_2 \closevar{x} r_3$ to define $\mu^r(x) := \spn{|\mathsf{clr}(r_1)|+1, |\mathsf{clr}(r_1 r_2)|+1	}$. 
The spanner $\spanner{\alpha}$ is then defined by $\spanner{\alpha}(w) := \{ \mu^r \mid r \in \validr{\alpha,w} \} $ for all $w\in\Sigma^*$.

\subparagraph*{Variable-set automata:} Variable-set automata (short: \emph{vset-automata}) are NFAs that may use variable operations $\openvar{x}$ and $\closevar{x}$ as  transitions. More formally, let  $V \subset \Xi$ be a finite set of variables. 
 A variable-set automaton over $\Sigma$ with variables $V$ is a tuple $A = (Q, q_0, q_f , \delta)$, where $Q$ is the set of states, $q_0 \in Q$ is the initial state, $q_f \in Q$ is the accepting state, and $\delta \colon Q \times (\Sigma \cup \{ \varepsilon \} \cup \Gamma_V) \rightarrow \powerset{Q}$ is the transition function with $\Gamma_V := \{ \openvar{x}, \closevar{x} \mid x \in V \}$. 
 
We define the semantics using a two-step approach analogous to the semantic definition of regex formulas. 
 Firstly, we treat $A$ as an NFA that defines the ref-language defined by $\rlang(A):=\{ r \in (\Sigma \cup \Gamma_V)^* \mid q_f \in \delta^*(q_0, r) \}$, where 
 the function $\delta^* \colon Q \times (\Sigma \cup \Gamma_V) \rightarrow \powerset{Q}$ is defined such that for all $p,q \in Q$ and $r \in (\Sigma \cup \Gamma_V)^*$, $q \in \delta^*(p,r)$ if and only if there exists a path in $A$ from $p$ to $q$ with the label $r$. 

Secondly, let $\SVars{A}$ be the set of $x \in V$ such that $\openvar{x}$ or $\closevar{x}$ appears in $A$. A ref-word $r \in \rlang(A)$ is \emph{valid} if for every $x \in \SVars{A}$, $|r|_{\openvar{x}} = |r|_{\closevar{x}}=1$, and $\openvar{x}$ always occurs to the left of $\closevar{x}$. Then $\validr{A}$, $\validr{A,w}$ and $\spanner{A}$ are defined analogously to regex formulas. We denote the set of all vset-automata using $\mathsf{VA_{set}}$. As for regex formulas, a vset-automaton $A\in\mathsf{VA_{set}}$ is called \emph{functional} if $\rlang(A)=\validr{A}$.

\begin{example}\label{ex:regexAutomaton}
We define the functional regex formula 
$\alpha:=\Sigma^*\cdot x\{(\mathtt{wine})\lor(\mathtt{cake})\}\cdot\Sigma^*$. We also define the functional vset-automaton~$A$ as follows:
\begin{center}
	\begin{tikzpicture}[on grid, node distance =12mm,every loop/.style={shorten >=0pt}, every state/.style={inner sep=0pt,minimum size=5mm}]
	\node[state,initial text=,initial by arrow] (q0) {};
	\node[state, right= of q0] (q1) {};
	\node[state, above right=of q1] (b1) {};
	\node[state, right=of b1] (b2) {};
	\node[state, right=of b2] (b3) {};

	\node[state, below right=of q1] (c1) {};
		\node[state, right=of c1] (c2) {};
		\node[state, right=of c2] (c3) {};
	\node[state, below right=of b3] (q3) {};
	\node[state,accepting,right=of q3] (q4) {};	\path[->]
	(q0) edge [loop above] node {$\Sigma$} (q0)
	(q0) edge node[above] {$\openvar{x}$} (q1)
	(q1) edge[pos=0.2] node[above] {$\mathtt{w}$} (b1)
	(b1) edge[] node[above] {$\mathtt{i}$} (b2)
	(b2) edge[] node[above] {$\mathtt{n}$} (b3)
	(b3) edge[] node[above] {$\mathtt{e}$} (q3)
	(q1) edge[pos=0.2] node[below] {$\mathtt{c}$} (c1)
(c1) edge[] node[below] {$\mathtt{a}$} (c2)
(c2) edge[] node[below] {$\mathtt{k}$} (c3)
(c3) edge[] node[below] {$\mathtt{e}$} (q3)
	(q3) edge node[above] {$\closevar{x}$} (q4)
(q4) edge [loop above] node {$\Sigma$} (q4)
	;
	\end{tikzpicture}
\end{center}  
For all $w\in\Sigma^*$, we have that $\spanner{\alpha}(w)=\spanner{A}(w)$ contains exactly those $(\{x\},w)$-tuples $\mu$ that have $w_{\mu(x)}=\mathtt{wine}$ or $w_{\mu(x)}=\mathtt{cake}$.
\end{example}

\subsubsection{Spanner Algebra}\label{sec:spannerAlgebra}
We now introduce an algebra on spanners in order to construct more complex spanners.

\begin{definition}
Two spanners $P_1$ and $P_2$ are \emph{compatible} if $\SVars{P_1}=\SVars{P_2}$.
We define  the following algebraic operators for all spanners $P, P_1, P_2$:
\begin{itemize}
	\item If $P_1$ and $P_2$ are compatible, their \emph{union} $(P_1 \cup P_2)$ and their \emph{difference} $(P_1\setminus P_2)$ are defined by $(P_1 \cup P_2)(w) := P_1(w) \cup P_2(w)$ and $(P_1 \setminus P_2)(w) := P_1(w) \setminus P_2(w)$.
	\item The \emph{projection} $\pi_Y P$ for $Y \subseteq \SVars{P}$ is defined by $\pi_Y P(w) := P|_Y(w)$, where $P|_Y(w)$ is the restriction of all $\mu \in P(w)$ to~$Y$.
	\item The \emph{natural join} $P_1 \bowtie P_2$ is obtained by defining each $(P_1 \bowtie P_2)(w)$ as the set of all  $(V_1 \cup V_2,w)$-tuples $\mu$ for which there exists $\mu_1 \in P_1(w)$ and $\mu_2 \in P_2(w)$ with $\mu|_{V_1}(w) = \mu_1(w)$ and $\mu|_{V_2}(w) = \mu_2(w)$, where $V_i := \SVars{P_i}$ for $i \in \{ 1,2 \}$.   
	\item For every  $k$-ary relation $R \subseteq (\Sigma^*)^k$ and variables $x_1, \dots, x_k \in \SVars{P}$, the \emph{selection}  $\upxi^R_{x_1 \dots x_k}P$ is defined by
	$\upxi^R_{x_1 \dots x_k} P(w):= \{\mu \in P(w) \mid (w_{\mu(x_1)} , \dots , w_{\mu(x_k)}) \in R\}$ for $w\in\Sigma^*$.
\end{itemize}
Let  $\SVars{P_1 \cup P_2} := \SVars{P_1\setminus P_2}:=\SVars{P_1}=\SVars{P_2}$,   $\SVars{\pi_Y P} := Y$,  $\SVars{P_1 \bowtie P_2} := \SVars{P_1} \cup \SVars{P_2}$, and $\SVars{\upxi^R_{x_1 \dots x_k}} := \SVars{P}$.
\end{definition}

 Note that the relations $R$ in the selection are usually infinite; and they are never considered part of the input.

Let $O$ be a spanner algebra and let $C$ be a class of primitive spanner representations, then we use $C^O$ to denote the set of all spanner representations that can be constructed by repeated combinations of the symbols for the operators from $O$ with the spanner representation from~$C$. We denote the closure of $\spanner{C}$ under the spanner operators $O$ as $\spanner{C^O}$. 
\begin{example}

Let $\alpha_1:= \Sigma^*x\{\Sigma^*\}\Sigma^*y\{\Sigma^*\}\Sigma^*$ and $\alpha_2:=\Sigma^*\cdot x\{(\mathtt{wine})\lor(\mathtt{cake})\}\cdot\Sigma^*$ (recall Example~\ref{ex:regexAutomaton}). We combine the two regex formulas into a core spanner $P := \pi_{x}\upxi^=_{x,y} (\alpha_1\bowtie\alpha_2)$. Then $\spanner{P}(w)$ contains all $(\{x\},w)$-tuples $\mu$ such that $w_{\mu(x)}$ is an occurrence of \texttt{wine} or \texttt{cake} in $w$ that is followed by another occurrence of the same word.
\end{example}

Like  Fagin et al. \cite{fag:spa}, we are mostly concerned with string equality selections $\upxi^=$. Following~$\cite{fag:spa,pet:rec}$, we focus on the class  of \emph{regular spanners} $\spanner{\rgx^{\spanreg}}$, the class of  \emph{core spanners}\footnote{As this class captures the core functionality of SystemT.}  $\spanner{\rgx^{\core}}$ 
and the class of \emph{generalized core spanners}  $\spanner{\rgx^{\cored}}$, where 
$\mathsf{reg}:=\{\pi,\cup,\bowtie\}$ and  $\mathsf{core} := \{ \pi, \upxi^=, \cup, \bowtie\}$. 
As shown in~\cite{fag:spa}, we have
\[ \spanner{\rgx^{\spanreg}}=\spanner{\mathsf{VA}_{\mathsf{set}}^{\spanreg}} =\spanner{\mathsf{VA_{set}}}  \subset  \spanner{\rgx^{\core}}=\spanner{\mathsf{VA}_{\mathsf{set}}^{\core}}\subset \spanner{\rgx^{\cored}}=\spanner{\mathsf{VA}_{\mathsf{set}}^{\cored}}. \]
In other words, there is a proper hierarchy of regular, core, and generalized core spanners; and for each of the classes, we can choose regex formulas or vset-automata as primitive spanner representations. As shown in~\cite{fre:splog}, functional vset-automata have the same expressive power as vset-automata in general. The size difference can be exponential, but this does not matter for the purpose of the present paper.


\subsection{Document Spanners and Spanner Algebra}\label{sec:spanners}

\input{sec-prelim-spanners}

\subsection{Spanner Logic}\label{sec:splog}

\input{sec-prelim-splog}

\subsection{Dynamic complexity}\label{sec:dyn}

\input{sec-prelim-dyn}



