FacMikCharacterization.tex

% !TEX root = FacMik.tex
\section{A characterization of languages of uncountable degree}
\subsubsection*{Games on types and strategy trees.}
%We recall that, given a language $L$, the set $H_L$ is the set of tree types, and the set $V_L$ of context types of $L$. Both are finite when $L$ is regular. 
Following \cite{bp}, for a given regular language of trees $L$, a prefix $p$ and types $h_i\in H_L$ ($i=1,2,\dots$) we define games on types $\mathcal{H}^p_k(h_1,\dots,h_k)$ and $\mathcal{H}^p_\infty(h_1,h_2,\dots)$. The Constrainer plays as in the simple and infinite cutting games and the task of the Alternator is to play in the $i$--th round a tree of type $h_i$, that is an element of $\alpha_L^{-1}(h_i)$. % If the prefix $p$ is empty we just write $\mathcal{H}_\infty(h_1,h_2,\dots)$ and $\mathcal{H}(h_1, \dots, h_k)$ respectively.

A type tree for $L$ is a tree over the finite alphabet $H_L$. For a given tree $t$, there is a type tree $\sigma_t$ induced by $t$ such that for every node $w \in \dom(\sigma_t)$, 
\begin{equation}
\label{formula:sigmat}
\sigma_t(w)\ \mbox{is the type of the tree}\ t.w.
\end{equation}
Let $\sigma$ be a type tree, and $t$ a tree. We say that a type tree $\sigma$ is \emph{locally consistent} with a tree $t$ if $\dom(\sigma)=\dom(t)$ and for every node $w \in \dom(t)$ such that $t(w)=a$, 
\begin{itemize}
\item if $w$ is a leaf, then $\sigma(w)$ is the type of $a$,
\item if $w$ has two children $m_\ell$ and $m_r$, then $\sigma(w)$ is the type obtained by applying $a$ to the pair $(\sigma(m_\ell), \sigma(m_r))$.
\end{itemize}
\begin{definition} A finite strategy tree is a tuple
$\mathfrak{s}=(t, \sigma_1, \dots, \sigma_k)$ where
\begin{itemize}
\item $t$ is a tree, the support of the strategy and $\sigma_1=\sigma_t$,
\item $\sigma_\ell$ is locally consistent with $t$, for each $\ell \leq k$,
\item for each $w \in \dom(t)$, Alternator has a winning strategy in $\mathcal{H}(\sigma_1(w), \dots, \sigma_k(w))$.
\end{itemize}
An  infinite strategy tree $\mathfrak{s}=(t, \sigma_1, \sigma_2, \dots )$ is defined analogously.
\end{definition}
The root sequence of a strategy tree $\mathfrak{s}=(t, \sigma_1, \sigma_2, \dots )$ is the sequence of types $(\sigma_1(\varepsilon), \sigma_2(\varepsilon), \dots)$.  We define the \emph{alternation} of a sequence $(h_1,\dots,h_\ell)$ of types as the cardinality of the set $\{ i: h_i\neq h_{i+1} \}$. The same definition applies to infinite sequences of types. Let $\mathfrak{s}$ be a finite strategy tree. The \emph{root alternation} of $\mathfrak{s}$ is the alternation of the root sequence, while the \emph{limit alternation} of $\mathfrak{s}$ is the maximal number $k$ such that infinitely many subtrees of $\mathfrak{s}$ have root alternation at least $k$. We say that a set  $\mathfrak{S}$ of finite strategy trees has \emph{bounded root alternation} if there is a  $k$ such that the root alternation of each $\mathfrak{s} \in \mathfrak{S}$ is at most $k$, unbounded otherwise. Analogously for limit alternation.

A finite or infinite strategy tree $\mathfrak{s}=(t, \sigma_1, \dots)$ is \emph{locally optimal} if for every strategy tree $\mathfrak{s}'=(t, \sigma'_1, \dots)$ with same root sequence, and every $i>1$, the depth at which $\sigma_i$ and $\sigma_{i+1}$ first differ is greater or equal than the depth at which $\sigma'_i$ and $\sigma'_{i+1}$ first differ.
The next Proposition is very important technical point of \cite{bp}. 
\begin{proposition}[\cite{bp}]\label{prop:locality}
 For a regular tree language $L$, if $\mathfrak{S}$ is a set of locally optimal finite strategy trees with both root and unbounded limit alternation, then the strategy graph $G_L$ is recursive.
 \end{proposition}
The next Proposition establishes an important link between infinite cutting games and strategy trees. % alternating between a language and its complement and infinite cutting games with infinite root alternation.
\begin{proposition}\label{prop:types}
 Assume Alternator has a winning strategy in  $\mathcal{H}^\varepsilon_\infty(L, L^\complement)$. Then there is an infinite strategy tree $\mathfrak{s}^\infty$ with infinite root alternation. 
\end{proposition} 
 \begin{proof} 
 Assume Alternator has a winning strategy $f$ in  $\mathcal{H}^\varepsilon_\infty(L, L^\complement)$. The infinite strategy tree $\mathfrak{s}^\infty$ is constructed as follows. First of all, we can represent $f$ as a tree satisfying the following properties:
\begin{itemize}
\item the root is labelled by $\varepsilon$, and its unique child is labelled by Alternator's move obtained by applying the winning strategy $f$ at the first round of the game,
\item if a node $v$ is labelled with a tree $t$, then for every prefix $p$ of $t$ there is a unique child of $v$ labelled by $p$,
\item if a node $v$ is labelled with a prefix $p$, then $v$ has a unique child, and such a child is labelled by the answer obtained by applying the winning strategy $f$ to the position in the cutting game given by the labels of the path from the root to $v$.
\end{itemize}
Notice, that nodes at odd depth represent Alternator's moves (according to $f$) and are therefore labelled by trees, while nodes at even depth represent Constrainer's move and are thus labelled by prefixes. From now on, we always identify $f$ and the aforementioned tree.
\begin{claim}\label{claim:strategy}
For every node $v$ of $f$ labelled by a prefix $p$, 
there is an infinite sequence of strategy trees $(\mathfrak{s}^v_\ell: \ell < \omega)$ such that for each $\ell$
\begin{enumerate}
\item $\mathfrak{s}^v_\ell=(t, \sigma_1, \dots, \sigma_\ell)$, with the type $\sigma_{2k+1}(\varepsilon)$ included in $L$ and the type  $\sigma_{2k}(\varepsilon)$ included  $L^\complement$ if $v$ is at depth $2i$ with $i$ even, else dually. In particular this means that  $\sigma_{2k+1}(\varepsilon) \neq \sigma_{2k}(\varepsilon)$;
\item $\mathfrak{s}^n_{\ell+1}$ extends $\mathfrak{s}^v_\ell$, that is  $\mathfrak{s}^v_{\ell+1}=(t, \sigma_1, \dots, \sigma_\ell, \sigma_{\ell+1})$ and $\mathfrak{s}^n_\ell=(t, \sigma_1, \dots, \sigma_\ell)$.
\end{enumerate}
\end{claim}
Given the Claim, from Property 1 we have that
for each node $v$ labelled by a prefix $p$, and each $\ell=1,2,\dots$, $\mathfrak{s}^v_\ell$ has root alternation $\ell$ and defines a winning strategy for Alternator in $\mathcal{H}^p_\ell(L, L^\complement)$ if $v$ is at depth $2i$ with $i$ even, in $\mathcal{H}^p_\ell(L^\complement, L)$ otherwise. 
Let \[ \mathfrak{s}^\varepsilon_\ell = (t, \sigma_1, \dots, \sigma_\ell)\ \mbox{for}\ \ell=1,2,\dots.\] The required   
infinite stategy tree is defined as 
%\[ 
$ \mathfrak{s}^\infty = (t, \sigma_1, \dots )$.% \]
It remains to prove the Claim.
Firstly, by induction with respect to $\ell=1,2,\dots$ we will assign a strategy tree $\mathfrak{s}^v_\ell$ to each node $v$ of $f$ labelled by a prefix. % We then verify that for each such node $v$ of $f$, the obtained sequence $(\mathfrak{s}^v_1, \mathfrak{s}^v_2, \dots)$ satisfy the properties of the Claim. 
In the process of inductive construction we will also verify that Property 1 of the Claim is satisfied. Verification of Property 2 will be done later. Let us start from a remark that given an infinite sequence of type trees $(\sigma_1, \dots)$, by compactness there is a converging subsequence $(\sigma'_1, \dots)$. We assume that every time we have to choose  
a converging subsequence $(\sigma'_1, \dots)$ of a given sequence $(\sigma_1, \dots)$, we always choose the same subsequence and denote it's limit as 
$\limit(\sigma_1, \dots)$. We also assume that given a tree $t$, we have fixed an enumeration $(p_1, \dots)$ of all its prefixes such 
that sequence $(p_k)_{k=1,2,\dots}$ converge to the tree $t$.
For $\ell=1$, 
it is enough to take for each node $v$  \[ \mathfrak{s}^v_1=(t, \sigma_t),\] where $t$ is given by applying $f$ to the considered position and $\sigma_t$ is defined by formula (\ref{formula:sigmat}) at the beggining of this Section. By choice of $\sigma_t$, Property 1 is satisfied. For $\ell>1$ we proceed as follows. We assume the construction performed for $\ell-1$. Fix any node $v$ labelled by a prefix $p$. Assume that a tree $t$ is the answer given by $f$  at the position in the game given by the path from the root to the node $v$. To every prefix $p$ of $t$ corresponds a child $w$ of $v$ to which we already associated a strategy tree $\mathfrak{s}^w_{\ell-1}=(t^p, \sigma^p_{2}, \dots, \sigma^p_{\ell})$. 
Let us thence consider the sequence $(p_1, \dots)$, with limit $t$ and the sequences
$(t^{p_1}, \dots)$, $(\sigma^{p_1}_2\dots)$, $\dots,$  $(\sigma^{p_1}_{\ell}\dots)$.  The limits $\limit(\sigma^{p_k}_2),\dots,
\limit(\sigma^{p_k}_{\ell})$ were chosen in advance and are equal $\sigma^*_2, \dots, \sigma^*_\ell$. Since each $t^{p_k}$ extends $p_k$, the limit $t^*$ of  $(t^{p_1},t^{p_2},\dots)$ is $t$.
Now, for each $p$, the type trees $(\sigma^p_{2}, \dots, \sigma^p_{\ell})$
are locally consistent with $t^p$. Furthermore, given a sequence of trees $(t_1, \dots)$  that converges to $t^*$ and a sequence of type trees $(\sigma_1, \dots)$  that converges to $\sigma^*$, if $\sigma_k$ is locally consistent with $t_k$ for every k, then $\sigma^*$ is locally consistent with $t^*$.
%Therefore, by Lemma \ref{lemma:limit} 
From this fact follows that the limits $\sigma^*_2, \dots, \sigma^*_k$ are locally consistent with $t$. Finally, define $\sigma^*_1$ to be $\sigma_t$ as in formula (\ref{formula:sigmat}). We have just proved that
$\mathfrak{s}^v_\ell = (t, \sigma^*_1, \dots, \sigma^*_\ell)$
is a strategy tree. From induction hypothesis together with definition of $\sigma_t$ and preservation of Property 1 under limits follows that $\mathfrak{s}^v_\ell$ also 
satisfies Property 1. 

We now verify that the described procedure preserves Property 2. For $\ell=1$ there is nothing to check. For the induction step, we reason as follows. Assume the Property holds for each node and for each $k<\ell$. Now, let us consider an arbitrary node $v$. We have to prove that $\mathfrak{s}^v_{\ell+1}$ extends $\mathfrak{s}^v_{\ell}$. 
By induction hypothesis,  $\mathfrak{s}^w_{\ell-1}=(t^p, \sigma^p_{2}, \dots, \sigma^p_{\ell})$ and
$\mathfrak{s}^w_{\ell}=(t^p, \sigma^p_{2}, \dots, \sigma^p_{\ell}, \sigma^p_{\ell+1})$, for every node $w$  in the described procedure. Since the limits have been fixed in advance, we have that $\mathfrak{s}^w_{\ell}=(t, \sigma_t, \sigma^*_2, \dots, \sigma^*_\ell)$ and $\mathfrak{s}^v_{\ell+1}=(t, \sigma_t, \sigma^*_2, \dots, \sigma^*_\ell, \sigma^*_{\ell+1})$, meaning that the latter extends the former. This concludes the proof of the Claim.
 \end{proof}
 
Using the above Proposition, we can generalize to infinite games Proposition 5.2 from \cite{bp}:
\begin{proposition}\label{prop:tree_to_types}
For a regular language $L$ 
%and any prefix $p$, 
the following conditions are equivalent.
 \begin{enumerate}
\item Alternator wins the game $\mathcal{H}^\varepsilon_\infty(L, L^\complement)$, 
 \item  There are tree types $h, g\in H_L$, such that $h\neq g$ and Alternator wins $\mathcal{H}^\varepsilon_\infty(h, g)$.
 \end{enumerate}
\end{proposition}
The proof of Proposition \ref{prop:tree_to_types} can be found in the Appendix.
We will use the following Lemma, presented in \cite{bp} for finite strategy trees, with proof extending straightforwardly to infinite strategy trees.
\begin{lemma}\label{lemma:locallyoptimal}
For every finite or infinite strategy tree, there is a locally optimal strategy tree with same root sequence.
\end{lemma}
The next Lemma  follows immediately from the definition of a strategy tree.
\begin{lemma}\label{lemma:short_strategy}
Let $\mathfrak{s}=(t, \sigma_1, \dots, \sigma_\ell)$ be a strategy tree. For the game $\mathcal{H}(\sigma_1(\varepsilon), \dots, \sigma_\ell(\varepsilon))$ and a strategy of Constrainer given by always cutting at level $i$, Alternator wins  by playing as follows:
\begin{itemize}
\item at first, Alternator plays $t$, then
\item for each port $w$ at level $i$ of the multi context given by Constrainer's move, Alternator plugs in the tree given by her winning strategy $\mathcal{H}(\sigma_1(w), \dots, \sigma_\ell(w))$.
\end{itemize}
In particular, if from a certain $j<\ell$ on $\sigma_k(w)=\sigma_{k+1}(w)$, $j\leq k < \ell$, then for each round $k$ such that $j< k < \ell$ Alternator always plugs in the same tree of type $\sigma_j(w)$ chosen at round $j$.
\end{lemma}
\subsubsection*{An Effective Characterization.}
\label{sec:the main result}
Everything now is ready to prove the main result of this paper.
\begin{theorem}\label{theorem:main}
Let $L$ be a regular tree language given by a non-deterministic tree automaton $\A$. The following conditions are equivalent:
\begin{enumerate}
%\item The following identity is not satisfied: $(u_2w_2^\omega v)^\omega u_1w_1^\infty = (u_2w_2^\omega v)^\infty$ if $(u_1, u_2) \in V_L$ and $(w_1, w_2) \in V_L$
%\item $L$ has unbounded limit alternation
\item The strategy graph $G_L$ is recursive.
\item $d_W(L) \geq \omega_1$
\end{enumerate}
In particular, since the graph $G_L$ is computable from the automaton $\A$, it is decidable whether the language accepted by $\A$ is of Wadge degree bigger or eqal than $\omega_1$.  
\end{theorem}
\begin{proof}
%The implication $(1) \Rightarrow (2)$ is proved in \cite{bp}.  
${\bf (1) \Rightarrow (2).}$  Assume the strategy graph is recursive. This means that there exists a strongly connected component that contains two nodes $(v, h)$ and $(v', h')$ with $h \neq h'$. 
Thanks to Proposition \ref{proposition:path to edge}, if there exists a path between $(v, h)$ and $(v', h')$, there is also an edge between $(v, h)$ and $(v', h')$. 
Moreover, for vertices $(v_1,h_1),(v_2,h_2),\dots$, if for every $i=1,2,\dots$ there is an edge from $(v_i, h_i)$ to $(v_{i+1}, h_{i+1})$, this means that Alternator has a winning strategy in $\mathcal{H}(h_1,h_2,\dots)$. So, take $(v_i, h_i)= (v,h)$ for $i$ even, and $(v_i, h_i)= (v',h')$ for $i$ odd. This shows that Alternator has a winning strategy in $\mathcal{H}^\varepsilon_\infty(h, h')$. By Proposition \ref{prop:tree_to_types}
Alternator has a winning strategy in  $\mathcal{H}^\varepsilon_\infty(L, L^\complement)$.


${\bf (2) \Rightarrow (1).}$ 
By Propositions \ref{prop:infinity}  and \ref{prop:locality}, it is enough to verify that 
 if Alternator has a winning strategy in $\mathcal{H}^\varepsilon_\infty(L, L^\complement)$ then there is a set $\mathfrak{S}$ of locally optimal finite strategy trees  with both root and limit unbounded alternation. 
Assume Alternator has a winning strategy $f$ in  $\mathcal{H}^\varepsilon_\infty(L, L^\complement)$. From Proposition \ref{prop:types} there is a strategy tree $\mathfrak{s}^\infty = (t,\sigma_1,\dots) $ with infinite root alternation. 
 By Lemma \ref{lemma:locallyoptimal} we can assume that $\mathfrak{s}^\infty$ is  locally optimal. Let us define 
\[ \mathfrak{S}= \{ (t,\sigma_1,\dots,\sigma_k): k=1,2,\dots\}. \]
Note that each element of $\mathfrak{S}$ is locally optimal.
Now, assume limit alternation of $\mathfrak{S}$ is bounded.
From this fact and since every element of $\mathfrak{S}$ is a prefix of $\mathfrak{s}^\infty$, it holds that with respect to $\mathfrak{s}^\infty$, the set of subtrees of $t$ with infinite root alternation has to be finite. This means that $\mathfrak{s}^\infty$ satisfies the following property:
\begin{description}
\item[(*)] 
there is a finite set $X$ of nodes of $t$ satisfying the following properties:
\begin{itemize}
%\item there is a node $n^* \in \{n_1, \dots, n_\ell\}$ with two children $m_1, m_2 \in \dom(t)|_i \setminus \{n_1, \dots, n_\ell\}$
\item the root is included in $X$, and each node of $X$ is at most at depth $i$ in $t$, 
\item $\sigma_k(v)\neq \sigma_{k'}(v)$, for every node $v$ in the set $X$, and $\sigma_k(w)= \sigma_{k'}(w)$, for every node $w$ of $t$ of depth $i+1$, for some $k, k'$ , with $k < k' \leq j$.
\end{itemize}
\end{description}
The strategy tree $\mathfrak{s}=(t, \sigma_1, \dots, \sigma_j)$ from $\mathfrak{S}$, where $j$ is given by the previous property, also satisfies the property (*) above (for the same $X$ and the same $k, k'$).

%This means that there is a strategy tree $\mathfrak{s}=(t, \sigma_1, \dots, \sigma_j)$ in  $ \mathfrak{S}$ and a finite set $X$ of nodes of $t$ satisfying the following properties:
%\begin{itemize}
%%\item there is a node $n^* \in \{n_1, \dots, n_\ell\}$ with two children $m_1, m_2 \in \dom(t)|_i \setminus \{n_1, \dots, n_\ell\}$
%\item the root is included in the set $X$,
%\item the set $X$ is included in the first $i$ levels of the tree $t$, 
%\item $\sigma_k(v)\neq \sigma_{k'}(v)$, for every node $v$ in the set $X$, $\sigma_k(v)= \sigma_{k'}(v)$, for every node $v$ not in the set $X$ for some $k, k'$ , with $k < k' \leq j$.
%\end{itemize}

Let us consider the game $\mathcal{H}( \sigma_1(\varepsilon), \dots, \sigma_j(\varepsilon))$ where at first Alternator plays $t$ and then Constrainer uses the strategy given by cutting always at level $i+1$. We can therefore apply Lemma \ref{lemma:short_strategy} and assume that Alternator plays the winning strategy described there. This implies that the trees played at round $k$ and $k'$ are the same, say $t'$ (from the root to level $i$ they are the same, because the Constrainer insists on this and below they are the same, because the Alternator plays the same answers in rounds $k$ and $k'$). But by local consistency, since $\sigma_k(\varepsilon)\neq \sigma_{k'}(\varepsilon)$, the two trees should have two different types, a contradiction. We therefore conclude that limit alternation of $\mathfrak{S}$ is unbounded. The method of proof is illustrated by Figure \ref{figure:consistency} in the Appendix .
\end{proof}