connected grammar ${\mathcal{G}}$ is _periodic_ in the sense that there is a
constant $c$ (that depends on ${\mathcal{G}})$ and a family of constants
$d_{N,N^{\prime}}$ such that, for each
$N,N^{\prime}\in{{\mathcal{N}}}^{\mathrm{inf}}$, and sufficiently large $n$,
${\mathcal{L}}_{n}\\!\left({\mathcal{G}},N{\Rightarrow}N^{\prime}\right)\neq\emptyset$
if and only if $n\equiv d_{N,N^{\prime}}\mod c$.

######  Lemma 37.

Let ${\mathcal{G}}=(\Sigma,{\mathcal{N}},{\mathcal{R}})$ be a regular tree
grammar. Assume that ${\mathcal{G}}$ is essentially strongly-connected and
$\\#\\!\left({\mathcal{L}}\\!\left({\mathcal{G}}\right)\right)=\infty$. Then
there exist constants $n_{0},c>0$ and a family
$(d_{N,N^{\prime}})_{N,N^{\prime}\in{{\mathcal{N}}}^{\mathrm{inf}}}$ of
natural numbers $0\leq d_{N,N^{\prime}}<c$ that satisfy the following
conditions:

  1. (1)

For every $N,N^{\prime}\in{{\mathcal{N}}}^{\mathrm{inf}}$, if
${\mathcal{L}}_{n}\\!\left({\mathcal{G}},N{\Rightarrow}N^{\prime}\right)\neq\emptyset$,
then $n\equiv d_{N,N^{\prime}}\mod c$.

  2. (2)

The converse of (1) holds for sufficiently large $n$: for any
$N,N^{\prime}\in{{\mathcal{N}}}^{\mathrm{inf}}$ and $n\geq n_{0}$, if $n\equiv
d_{N,N^{\prime}}\mod c$ then
${\mathcal{L}}_{n}\\!\left({\mathcal{G}},N{\Rightarrow}N^{\prime}\right)\neq\emptyset$.

  3. (3)

$d_{N,N}=0$ for every $N\in{{\mathcal{N}}}^{\mathrm{inf}}$.

  4. (4)

$d_{N,N^{\prime}}+d_{N^{\prime},N^{\prime\prime}}\equiv
d_{N,N^{\prime\prime}}\mod c$ for every
$N,N^{\prime},N^{\prime\prime}\in{{\mathcal{N}}}^{\mathrm{inf}}$.

The proof of the above lemma is rather involved; we defer it to Appendix C. We
give some examples below, to clarify what the lemma means. Consider the
grammar ${\mathcal{G}}_{1}$ consisting of the following rewriting rules:

$A\longrightarrow\mathtt{a}(B)\qquad B\longrightarrow\mathtt{b}(A)\qquad
A\longrightarrow\mathtt{c}(C)\qquad C\longrightarrow\mathtt{c}$

Then ${{\mathcal{N}}}^{\mathrm{inf}}=\\{A,B\\}$ and the conditions of the
lemma above hold for:

$n_{0}=0\qquad c=2\qquad d_{A,A}=d_{B,B}=0\qquad d_{A,B}=d_{B,A}=1.$

In fact,
${\mathcal{L}}\\!\left({\mathcal{G}}_{1},A{\Rightarrow}A\right)=\\{(\mathtt{a}\mathtt{b})^{k}[\,]\mid
k\geq 0\\}$,
${\mathcal{L}}\\!\left({\mathcal{G}}_{1},B{\Rightarrow}B\right)=\\{(\mathtt{b}\mathtt{a})^{k}[\,]\mid
k\geq 0\\}$,
${\mathcal{L}}\\!\left({\mathcal{G}}_{1},B{\Rightarrow}A\right)=\\{(\mathtt{a}\mathtt{b})^{k}\mathtt{a}[\,]\mid
k\geq 0\\}$, and
${\mathcal{L}}\\!\left({\mathcal{G}}_{1},A{\Rightarrow}B\right)=\\{(\mathtt{b}\mathtt{a})^{k}\mathtt{b}[\,]\mid
k\geq 0\\}$. Here, since the arities of $\mathtt{a}$ and $\mathtt{b}$ are $1$,
we have used regular expressions to denote linear contexts.

Consider the grammar ${\mathcal{G}}_{2}$, obtained by adding the following
rules to the grammar above.

$A\longrightarrow\mathtt{a}(A_{1})\qquad
A_{1}\longrightarrow\mathtt{a}(A_{2})\qquad
A_{2}\longrightarrow\mathtt{a}(A).$

Then, the conditions of the lemma above holds for $n=6$, $c=1$,
$d_{N,N^{\prime}}=0$ for $N,N^{\prime}\in\\{A,A_{1},A_{2},B\\}$. Note that
${\mathcal{L}}\\!\left({\mathcal{G}}_{2},A_{2}{\Rightarrow}A_{1}\right)=\\{\mathtt{a}^{2}(\mathtt{a}^{3}|\mathtt{a}\mathtt{b})^{k}\mathtt{a}^{2}[\,]\mid
k\geq 0\\}$. ∎

######  Remark 38.

With some additional assumptions on a grammar, Lemma 37 above can be easily
proved. For example, consider a canonical, unambiguous and essentially
strongly-connected grammar ${\mathcal{G}}$ and assume that (i) ${\mathcal{G}}$
is $N$-aperiodic for some $N$ and (ii) there exist a $2$-context $C$ and
nonterminals $N,N_{1},N_{2}\in{{\mathcal{N}}}^{\mathrm{inf}}$ such that
$N\longrightarrow_{{\mathcal{G}}}^{*}C[N_{1},N_{2}]$. Then Lemma 37 for the
grammar ${\mathcal{G}}$ trivially holds with $c=1$. In fact, this simpler
approach is essentially what we adopted in the conference version [18] of this
article.

Using the lemma above, we prove that for every
$S\in{\mathcal{S}}^{\mathrm{inf}}({\mathcal{G}})$ and any sufficiently large
$n$ such that
${\mathcal{L}}_{n}\\!\left({\mathcal{G}},\kappa\right)\neq\emptyset$, we can
find a context $U\in{\mathcal{L}}_{n}\\!\left({\mathcal{G}},\kappa\right)$
such that $S\preceq U$ (Lemma 39 below).

######  Lemma 39.

Let ${\mathcal{G}}=(\Sigma,{\mathcal{N}},{\mathcal{R}})$ be a regular tree
grammar in canonical form. Assume that ${\mathcal{G}}$ is unambiguous and
essentially strongly-connected and
$\\#\\!\left({\mathcal{L}}\\!\left({\mathcal{G}}\right)\right)=\infty$. Then
there exists a constant $n_{0}\in{\rm Nature}$ that satisfies the following
condition: For every

  * •

$S\in{\mathcal{S}}^{\mathrm{inf}}({\mathcal{G}})$,

  * •

$n\geq n_{0}+|S|$, and

  * •

$\kappa=({}{\Rightarrow}N^{\prime})$ or $(N{\Rightarrow}N^{\prime})$ where
$N,N^{\prime}\in{{\mathcal{N}}}^{\mathrm{inf}}$,

if ${\mathcal{L}}_{n}\\!\left({\mathcal{G}},\kappa\right)\neq\emptyset$, then
there exists $U\in{\mathcal{L}}_{n}\\!\left({\mathcal{G}},\kappa\right)$ with
$S\preceq U$.

######  Proof 3.20.

First, let us choose the following constants:

  * •

$m_{0}\in{\rm Nature}$ such that, for every
$N,N^{\prime}\in{\mathcal{N}}^{\mathrm{inf}}$, there exists
$S_{N,N^{\prime}}\in{\mathcal{L}}\\!\left({\mathcal{G}},N{\Rightarrow}N^{\prime}\right)$
with $|S_{N,N^{\prime}}|\leq m_{0}$. The existence of $m_{0}$ is a consequence
of essential strong-connectivity and of finiteness of ${\mathcal{N}}$.

  * •

$m_{1}$ which is the constant $n_{0}$ of Lemma 37.

  * •

$m_{2}\in{\rm Nature}$ such that, for every
$N\in{\mathcal{N}}\backslash{\mathcal{N}}^{\mathrm{inf}}$ and every
$T\in{\mathcal{L}}\\!\left({\mathcal{G}},N\right)$, we have $|T|<m_{2}$. The
existence of $m_{2}$ follows from the fact that
$\bigcup_{N\in{\mathcal{N}}\backslash{\mathcal{N}}^{\mathrm{inf}}}{\mathcal{L}}\\!\left({\mathcal{G}},N\right)$
is a finite set.

Let $c$ and $(d_{N,N^{\prime}})_{N,N^{\prime}\in{\mathcal{N}}^{\mathrm{inf}}}$
be the constant and the family obtained by Lemma 37.

We define $n_{1}\triangleq m_{0}+m_{1}$ and $n_{2}\triangleq
m_{0}+m_{1}+rm_{2}+1$, where
$r\triangleq\max(\mathrm{Im}\left(\Sigma\right))$. Below we shall show: (i)
the current lemma for the case $\kappa=(N{\Rightarrow}N^{\prime})$, by setting
$n_{0}\triangleq n_{1}$ and then (ii) the lemma for the case
$\kappa=({\Rightarrow}N^{\prime})$, by setting $n_{0}\triangleq n_{2}$; we use
(i) to show (ii). The whole lemma then follows immediately from (i) and (ii)
with $n_{0}\triangleq\max\\{n_{1},n_{2}\\}\,(=n_{2})$.

  * •

Case (i): We define $n_{0}\triangleq n_{1}=m_{0}+m_{1}$. Assume that:
$S\in{\mathcal{L}}\\!\left({\mathcal{G}},N_{1}{\Rightarrow}N_{2}\right)$ where
$N_{1},N_{2}\in{\mathcal{N}}^{\mathrm{inf}}$; $n\geq n_{0}+|S|$;
$\kappa=(N{\Rightarrow}N^{\prime})$ where
$N,N^{\prime}\in{\mathcal{N}}^{\mathrm{inf}}$; and
${\mathcal{L}}_{n}\\!\left({\mathcal{G}},\kappa\right)\neq\emptyset$. Let
$S_{1}\in{\mathcal{L}}\\!\left({\mathcal{G}},N_{2}{\Rightarrow}N^{\prime}\right)$
with $|S_{1}|\leq m_{0}$. Then
$S_{1}[S]\in{\mathcal{L}}\\!\left({\mathcal{G}},N_{1}{\Rightarrow}N^{\prime}\right)$.
It suffices to show that
${\mathcal{L}}_{n-|S_{1}[S]|}\\!\left({\mathcal{G}},N{\Rightarrow}N_{1}\right)\neq\emptyset$.
By Lemma 37(1)(4),

$\mspace{20.0mu}\begin{aligned} n&\equiv d_{N,N^{\prime}}\equiv
d_{N,N_{1}}+d_{N_{1},N_{2}}+d_{N_{2},N^{\prime}}&&\bmod
c&&(\because{\mathcal{L}}_{n}\\!\left({\mathcal{G}},\kappa\right)={\mathcal{L}}_{n}\\!\left({\mathcal{G}},N{\Rightarrow}N^{\prime}\right)\neq\emptyset)\\\
|S_{1}|&\equiv d_{N_{2},N^{\prime}}&&\bmod
c&&(\because(S_{1}\in)\,{\mathcal{L}}_{|S_{1}|}\\!\left({\mathcal{G}},N_{2}{\Rightarrow}N^{\prime}\right)\neq\emptyset)\\\
|S|&\equiv d_{N_{1},N_{2}}&&\bmod
c&&(\because(S\in)\,{\mathcal{L}}_{|S|}\\!\left({\mathcal{G}},N_{1}{\Rightarrow}N_{2}\right)\neq\emptyset)\end{aligned}$

and thus

$n-|S_{1}[S]|\equiv d_{N,N_{1}}\mod c.$

Since $n\geq m_{0}+m_{1}+|S|$, we have $n-|S_{1}[S]|\geq m_{1}$, and hence by
Lemma 37(2), we have
${\mathcal{L}}_{n-|S_{1}[S]|}\\!\left({\mathcal{G}},N{\Rightarrow}N_{1}\right)\neq\emptyset$.

  * •

Case (ii): We define $n_{0}\triangleq n_{2}=m_{0}+m_{1}+rm_{2}+1$. Assume
that: $S\in{\mathcal{L}}\\!\left({\mathcal{G}},N_{1}{\Rightarrow}N_{2}\right)$
where $N_{1},N_{2}\in{\mathcal{N}}^{\mathrm{inf}}$; $n\geq n_{0}+|S|$;
$\kappa=({}{\Rightarrow}N^{\prime})$ where
$N^{\prime}\in{\mathcal{N}}^{\mathrm{inf}}$; and
${\mathcal{L}}_{n}\\!\left({\mathcal{G}},\kappa\right)\neq\emptyset$. Let
$T\in{\mathcal{L}}_{n}\\!\left({\mathcal{G}},\kappa\right)$. Since the arity
of terminal symbols are bounded by $r$ and $|T|\geq rm_{2}+1$, there exists a
subtree $T_{0}\preceq T$ such that $m_{2}\leq|T_{0}|\leq rm_{2}+1$, which can
be shown by induction on tree $T$. Let $U$ be a linear context such that
$T=U[T_{0}]$. Since ${\mathcal{G}}$ is canonical and unambiguous, by Lemma 30,
$U\in{\mathcal{L}}\\!\left({\mathcal{G}},N{\Rightarrow}N^{\prime}\right)$ and
$T_{0}\in{\mathcal{L}}\\!\left({\mathcal{G}},N\right)$ for some
$N\in{\mathcal{N}}$. Since $m_{2}\leq|T_{0}|\leq rm_{2}+1$, we have
$N\in{\mathcal{N}}^{\mathrm{inf}}$ and $|U|\geq m_{0}+m_{1}+|S|$. By using the
case $(1)$, since
$(U\in)\,{\mathcal{L}}_{|U|}\\!\left({\mathcal{G}},N{\Rightarrow}N^{\prime}\right)\neq\emptyset$,
there exists
$U^{\prime}\in{\mathcal{L}}_{|U|}\\!\left({\mathcal{G}},N{\Rightarrow}N^{\prime}\right)$
with $S\preceq U^{\prime}$. Let $T^{\prime}\triangleq U^{\prime}[T_{0}]$; then
$T^{\prime}\in{\mathcal{L}}_{n}\\!\left({\mathcal{G}},{\Rightarrow}N^{\prime}\right)$
and $S\preceq T^{\prime}$.

We prepare another lemma.

######  Lemma 40.

If $\Phi_{m}(T)=(U,E,P)$, $\ell\in\\{1,\dots,\mathtt{shn}(E)\\}$,
$P{\centerdot}\ell$ is a linear context, and the second-order hole
$E{\centerdot}\ell$ occurs in $E$ in the form
$(E{\centerdot}\ell)[E^{\prime}]$, then $|E^{\prime}|\geq m$.

######  Proof 3.21.

By straightforward induction on $|T|$ and case analysis of Equation (2) in the
definition of $\Phi_{m}$. We can use Lemma 19 in the second case of Equation
(2) when $\ell=1$; all the other cases immediately follow from induction
hypothesis.

We are now ready to prove the main lemma of this subsection.

######  Proof 3.22 (Proof of Lemma 36).

Since $S_{0}\in{\mathcal{S}}^{\mathrm{inf}}({\mathcal{G}})$, we have
${{\mathcal{N}}}^{\mathrm{inf}}\neq\emptyset$ and hence
$\\#\\!\left({\mathcal{L}}\\!\left({\mathcal{G}}\right)\right)=\infty$. Let
$n_{0}$ be the constant of Lemma 39. Let $c_{1}$ be a positive integer such
that $|S_{n}|\leq c_{1}n$ for every $n\in{\rm Nature}$. We define
$c\triangleq(2r+1)c_{1}$ (recall that $r$ is the largest arity of $\Sigma$)
and choose $b$ so that $b\geq n_{0}$ and $b>|T|$ for any
$T\in\bigcup_{N\in{\mathcal{N}}\backslash{{\mathcal{N}}}^{\mathrm{inf}}}{\mathcal{L}}\\!\left({\mathcal{G}},N\right)$.

Assume that $N\in{{\mathcal{N}}}^{\mathrm{inf}}$, $n\geq 1$, $m\geq b$,
$\widetilde{E}\in\widetilde{\mathcal{E}}_{n}^{cm}({\mathcal{G}},N)$ and
$i\in\\{1,\dots,\mathtt{shn}(\widetilde{E})\\}$. Let
$\widetilde{E}{\centerdot}i=\llbracket\,\rrbracket^{n^{\prime}}_{\kappa^{\prime}}$.
We need to show that there exists
$U\in\widetilde{\mathcal{U}}^{cm}_{\llbracket\,\rrbracket^{n^{\prime}}_{\kappa^{\prime}}}({\mathcal{G}})$
such that $S_{m}\preceq U$.

Since $\widetilde{E}\in\widetilde{\mathcal{E}}_{n}^{cm}({\mathcal{G}},N)$,
there exist $T\in{\mathcal{L}}_{n}\\!\left({\mathcal{G}},N\right)$ and $P$
such that
$(\widetilde{E},P)=\widetilde{\Phi}_{cm}^{\bullet,{\mathcal{G}}}(T,N)$; hence
$P{\centerdot}i\in\widetilde{\mathcal{U}}^{cm}_{\widetilde{E}{\centerdot}i}({\mathcal{G}})=\widetilde{\mathcal{U}}^{cm}_{\llbracket\,\rrbracket^{n^{\prime}}_{\kappa^{\prime}}}({\mathcal{G}})$.
The affine context $P{\centerdot}i$ must be of the form
$a(U_{1},\dots,U_{\Sigma(a)})$. Since $P{\centerdot}i$ is good for $cm$, we
have $|P{\centerdot}i|\geq cm=(2r+1)c_{1}m\geq 2rc_{1}m+1$. Since
$\Sigma(a)\leq r$, there exists $j\leq\Sigma(a)$ such that $|U_{j}|\geq
2c_{1}m$. We have $\kappa^{\prime}=(N^{\prime}{\Rightarrow}N^{\prime\prime})$
or $({\Rightarrow}N^{\prime\prime})$ for some
$N^{\prime},N^{\prime\prime}\in{\mathcal{N}}$. Since
$P.i=a(U_{1},\dots,U_{\Sigma(a)})\in{\mathcal{L}}\\!\left({\mathcal{G}},\kappa^{\prime}\right)$,
there exist $N_{1},\dots,N_{\Sigma(a)}\in{\mathcal{N}}$ such that

$N^{\prime\prime}\longrightarrow
a(N_{1},\dots,N_{\Sigma(a)})\longrightarrow^{*}T^{\prime}$

where $T^{\prime}=P.i[N^{\prime}]$ if
$\kappa^{\prime}=(N^{\prime}{\Rightarrow}N^{\prime\prime})$, and
$T^{\prime}=P.i$ if $\kappa^{\prime}=({\Rightarrow}N^{\prime\prime})$. Let
$\kappa$ be $N^{\prime}{\Rightarrow}N_{j}$ if $U_{j}$ is a linear context, and
${\Rightarrow}N_{j}$ otherwise. Then
$U_{j}\in{\mathcal{L}}_{|U_{j}|}\\!\left({\mathcal{G}},\kappa\right)\neq\emptyset$.
In order to apply Lemma 39 (for $S=S_{m}$ and $n=|U_{j}|$), we need to check
the conditions: (i) $|U_{j}|\geq n_{0}+|S_{m}|$ and (ii) $\kappa$ consists of
only nonterminals in ${{\mathcal{N}}}^{\mathrm{inf}}$. Condition (i) follows
immediately from $|U_{j}|\geq 2c_{1}m\geq m+c_{1}m\geq n_{0}+|S_{m}|$. As for
(ii), it suffices to check that
${\mathcal{L}}\\!\left({\mathcal{G}},N_{j}\right)$ and
${\mathcal{L}}\\!\left({\mathcal{G}},N^{\prime}\right)$ contain a tree whose
size is no less than $b$ (where the condition on
${\mathcal{L}}\\!\left({\mathcal{G}},N^{\prime}\right)$ is required only if
$U_{j}$ is a linear context). The condition on
${\mathcal{L}}\\!\left({\mathcal{G}},N_{j}\right)$ follows from $|U_{j}|\geq
2c_{1}m\geq m\geq b$. If $U_{j}$ is a linear context, by Lemma 40, there exist
$S$ and $T^{\prime\prime}$ such that:

$T=S[(P{\centerdot}i)[T^{\prime\prime}]]\qquad|T^{\prime\prime}|\geq cm\geq
b\qquad
T^{\prime\prime}\in{\mathcal{L}}\\!\left({\mathcal{G}},N^{\prime}\right)$

as required.

Thus, we can apply Lemma 39 and obtain
$U_{j}^{\prime}\in{\mathcal{L}}\\!\left({\mathcal{G}},\kappa\right)$ such that
$S_{m}\preceq U_{j}^{\prime}$ and $|U_{j}^{\prime}|=|U_{j}|$. Since
$P.i=a(U_{1},\ldots,U_{\Sigma(a)})$ is good for $cm$, $U\triangleq
a(U_{1},\dots,U_{j-1},U^{\prime}_{j},U_{j+1},\dots,U_{\Sigma(a)})$ is also
good for $cm$. Obviously $|U|=|P.i|$ and thus
$U\in\widetilde{\mathcal{U}}^{cm}_{\llbracket\,\rrbracket^{n^{\prime}}_{\kappa^{\prime}}}({\mathcal{G}})$.
Since $S_{m}\preceq U_{j}^{\prime}$ and $U_{j}^{\prime}\preceq U$, we have
$S_{m}\preceq U$ as required.

###  3.6. Main Proof

Here, we give a proof of Theorem 6. Before the proof, we prepare a simple
lemma. We write $\mathcal{U}_{\leq n}({\Sigma})$ for the set of affine
contexts over $\Sigma$ of size at most $n$. Lemma 41 below gives an upper
bound of $\\#\\!\left(\mathcal{U}_{\leq n}({\Sigma})\right)$. A more precise
bound can be obtained by using a technique of analytic combinatorics such as
Drmota–Lalley–Woods theorem (cf. [5], Theorem VII.6), but the rough bound
provided by the lemma below is sufficient for our purpose.

######  Lemma 41.

For every ranked alphabet $\Sigma$, there exists a real constant $\gamma>1$
such that

$\\#\\!\left(\mathcal{U}_{\leq n}({\Sigma})\right)\leq\gamma^{n}$

for every $n\geq 0$.

######  Proof 3.23.

Let $A$ be the set of symbols: $\\{\grave{a},\acute{a}\mid
a\in\mathop{\mathrm{Dom}}(\Sigma)\\}\cup\\{\,\square\\}$. Intuitively
$\grave{a}$ and $\acute{a}$ are opening and closing tags of an XML-like
language.

We can transform an affine context $U$ to its XML-like string representation
$U^{\dagger}\in A^{*}$ by:

$\displaystyle(a(U_{1},\dots,U_{\Sigma(a)}))^{\dagger}$
$\displaystyle\triangleq\grave{a}\,U_{1}^{\dagger}\cdots
U_{\Sigma(a)}^{\dagger}\,\acute{a}$ $\displaystyle[\,]^{\dagger}$
$\displaystyle\triangleq\square.$

Obviously, $(\cdot)^{\dagger}$ is injective. Furthermore, $|U^{\dagger}|=2|U|$
if $U$ is a $0$-context (i.e., a tree), and $|U^{\dagger}|=2|U|+1$ if $U$ is a
linear context (note that the size of the hole $[\,]$ is zero, but its word
representation is of length $1$). Thus, for $n>0$, we have

$\\#\\!\left(\mathcal{U}_{\leq
n}({\Sigma})\right)\leq\sum_{i=0}^{2n+1}(\\#\\!\left(A\right))^{i}\leq\sum_{i=0}^{3n}(\\#\\!\left(A\right))^{i}\leq(\\#\\!\left(A\right)+1)^{3n}=((\\#\\!\left(A\right)+1)^{3})^{n}.$

If $n=0$, then $\\#\\!\left(\mathcal{U}_{\leq
n}({\Sigma})\right)=1=((\\#\\!\left(A\right)+1)^{3})^{n}$, as
$\mathcal{U}_{\leq n}({\Sigma})$ is the singleton set $\\{[\,]\\}$. Thus, the
required result holds for $\gamma=(\\#\\!\left(A\right)+1)^{3}$.

The following lemma is a variant of Theorem 6, specialized to a canonical
grammar.

######  Lemma 42.

Let ${\mathcal{G}}=(\Sigma,{\mathcal{N}},{\mathcal{R}})$ be a canonical,
unambiguous, and essentially strongly-connected regular tree grammar such that
$\\#\\!\left({\mathcal{L}}\\!\left({\mathcal{G}}\right)\right)=\infty$, and
$(S_{n})_{n\in{\rm Nature}}$ be a family of linear contexts in
${\mathcal{S}}^{\mathrm{inf}}({\mathcal{G}})$ such that
$|S_{n}|=\mathrm{O}(n)$. Then there exists a real constant $p>0$ such that for
any $N\in{{\mathcal{N}}}^{\mathrm{inf}}$,

$\operatorname*{limdef}_{n\rightarrow\infty}\frac{\\#\\!\left(\\{T\in{\mathcal{L}}_{n}\\!\left({\mathcal{G}},N\right)\mid
S_{\lceil p\log n\rceil}\preceq
T\\}\right)}{\\#\\!\left({\mathcal{L}}_{n}\\!\left({\mathcal{G}},N\right)\right)}=1.$

######  Proof 3.24.

The overall structure of the proof is the same as that of Proposition 12. Let
$Z_{n}$ be

$1-\frac{\\#\\!\left(\\{T\in{\mathcal{L}}_{n}\\!\left({\mathcal{G}},N\right)\mid
S_{\lceil p\log n\rceil}\preceq
T\\}\right)}{\\#\\!\left({\mathcal{L}}_{n}\\!\left({\mathcal{G}},N\right)\right)}=\frac{\\#\\!\left(\\{T\in{\mathcal{L}}_{n}\\!\left({\mathcal{G}},N\right)\mid
S_{\lceil p\log n\rceil}\not\preceq
T\\}\right)}{\\#\\!\left({\mathcal{L}}_{n}\\!\left({\mathcal{G}},N\right)\right)}.$

It suffices to show that $Z_{n}$ converges to $0$.

By Lemma 32, we have

${\mathcal{L}}_{n}\\!\left({\mathcal{G}},N\right)\cong\coprod_{\widetilde{E}\in\widetilde{\mathcal{E}}_{n}^{m}({\mathcal{G}},N)}\prod_{i=1}^{\mathtt{shn}(\widetilde{E})}\widetilde{\mathcal{U}}^{m}_{\widetilde{E}{\centerdot}i}({\mathcal{G}})$

for any $m>0$. Thus, we have

$Z_{n}\leq\frac{\sum_{\widetilde{E}\in\widetilde{\mathcal{E}}_{n}^{m}({\mathcal{G}},N)}\prod_{i=1}^{\mathtt{shn}(\widetilde{E})}\\#\\!\left(\\{U\in\widetilde{\mathcal{U}}^{m}_{\widetilde{E}{\centerdot}i}({\mathcal{G}})\mid
S_{\lceil p\log n\rceil}\not\preceq
U\\}\right)}{\sum_{\widetilde{E}\in\widetilde{\mathcal{E}}_{n}^{m(n)}({\mathcal{G}},N)}\prod_{i=1}^{\mathtt{shn}(\widetilde{E})}\\#\\!\left(\widetilde{\mathcal{U}}^{m}_{\widetilde{E}{\centerdot}i}({\mathcal{G}})\right)}.$
(4)

Let $b,c\geq 1$ be the numbers in Lemma 36. Then, by the lemma, for any $n$
and $p$ such that $\lceil p\log n\rceil\geq b$, each
$\widetilde{\mathcal{U}}^{c\lceil p\log
n\rceil}_{\widetilde{E}{\centerdot}i}({\mathcal{G}})$ contains at least one
$U$ that has $S_{\lceil p\log n\rceil}$ as a subcontext. Thus, for $m=c\lceil
p\log n\rceil$,
$\\#\\!\left(\\{U\in\widetilde{\mathcal{U}}^{m}_{\widetilde{E}{\centerdot}i}({\mathcal{G}})\mid
S_{\lceil p\log n\rceil}\not\preceq U\\}\right)$ is bounded above by:

$\begin{array}[]{ll}\\#\\!\left(\widetilde{\mathcal{U}}^{m}_{\widetilde{E}{\centerdot}i}({\mathcal{G}})\right)-1=(1-\displaystyle\frac{1}{\\#\\!\left(\widetilde{\mathcal{U}}^{m}_{\widetilde{E}{\centerdot}i}({\mathcal{G}})\right)})\\#\\!\left(\widetilde{\mathcal{U}}^{m}_{\widetilde{E}{\centerdot}i}({\mathcal{G}})\right)\leq(1-\displaystyle\frac{1}{\gamma^{rm}})\\#\\!\left(\widetilde{\mathcal{U}}^{m}_{\widetilde{E}{\centerdot}i}({\mathcal{G}})\right).\end{array}$

Here $\gamma$ is the constant (that only depends on $\Sigma$) of Lemma 41, and
$r$ is the largest arity of $\Sigma$. In the last inequality, we have used the
fact that
$\widetilde{\mathcal{U}}^{m}_{\widetilde{E}{\centerdot}i}({\mathcal{G}})\subseteq\mathcal{U}_{\leq
rm}({\Sigma})$.

By using the upper-bound above, Equation (4), and
$\mathtt{shn}(\widetilde{E})\geq\frac{n}{2rm}$ (Lemma 15), we have:

$\begin{array}[]{l}Z_{n}\leq\dfrac{\sum_{\widetilde{E}\in\widetilde{\mathcal{E}}_{n}^{m}({\mathcal{G}},N)}\prod_{i=1}^{\mathtt{shn}(\widetilde{E})}(1-\displaystyle\frac{1}{\gamma^{rm}})\\#\\!\left(\widetilde{\mathcal{U}}^{m}_{\widetilde{E}{\centerdot}i}({\mathcal{G}})\right)}{\sum_{\widetilde{E}\in\widetilde{\mathcal{E}}_{n}^{m(n)}({\mathcal{G}},N)}\prod_{i=1}^{\mathtt{shn}(\widetilde{E})}\\#\\!\left(\widetilde{\mathcal{U}}^{m}_{\widetilde{E}{\centerdot}i}({\mathcal{G}})\right)}\\\
=\dfrac{\sum_{\widetilde{E}\in\widetilde{\mathcal{E}}_{n}^{m}({\mathcal{G}},N)}(1-\displaystyle\frac{1}{\gamma^{rm}})^{\mathtt{shn}(\widetilde{E})}\prod_{i=1}^{\mathtt{shn}(\widetilde{E})}\\#\\!\left(\widetilde{\mathcal{U}}^{m}_{\widetilde{E}{\centerdot}i}({\mathcal{G}})\right)}{\sum_{\widetilde{E}\in\widetilde{\mathcal{E}}_{n}^{m(n)}({\mathcal{G}},N)}\prod_{i=1}^{\mathtt{shn}(\widetilde{E})}\\#\\!\left(\widetilde{\mathcal{U}}^{m}_{\widetilde{E}{\centerdot}i}({\mathcal{G}})\right)}\\\
\leq\dfrac{\sum_{\widetilde{E}\in\widetilde{\mathcal{E}}_{n}^{m}({\mathcal{G}},N)}(1-\displaystyle\frac{1}{\gamma^{rm}})^{\frac{n}{2rm}}\prod_{i=1}^{\mathtt{shn}(\widetilde{E})}\\#\\!\left(\widetilde{\mathcal{U}}^{m}_{\widetilde{E}{\centerdot}i}({\mathcal{G}})\right)}{\sum_{\widetilde{E}\in\widetilde{\mathcal{E}}_{n}^{m(n)}({\mathcal{G}},N)}\prod_{i=1}^{\mathtt{shn}(\widetilde{E})}\\#\\!\left(\widetilde{\mathcal{U}}^{m}_{\widetilde{E}{\centerdot}i}({\mathcal{G}})\right)}=(1-\dfrac{1}{\gamma^{rm}})^{\frac{n}{2rm}}\end{array}$

for any $n$ and $p$ such that $\lceil p\log n\rceil\geq b$ and $m=c\lceil
p\log n\rceil$.

It remains to choose $p$ so that
$(1-\dfrac{1}{\gamma^{rm}})^{\frac{n}{2rm}}=(1-\dfrac{1}{\gamma^{rc\lceil
p\log n\rceil}})^{\frac{n}{2rc\lceil p\log n\rceil}}$ converges to $0$. Let us
choose positive real numbers $a$, $p$, and $q$ so that $p$ and $q$ satisfy the
following conditions for every $n\geq a$:

$\displaystyle{p\log n}$ $\displaystyle\geq b$ (5)
$\displaystyle\gamma^{rc\lceil p\log n\rceil}$ $\displaystyle\leq n^{q}$ (6)
$\displaystyle q$ $\displaystyle<1.$ (7)

For example, we can choose $a,\,p,\,q$ as follows:

$\displaystyle a=\max\\{\gamma^{b({rc+2})},\gamma^{rc({rc+2})}\\}\qquad
p=\frac{\mathchoice{1}{1}{1}{{\scriptstyle
1}}}{\mathchoice{(rc+2)\log\gamma}{(rc+2)\log\gamma}{(rc+2)\log\gamma}{{\scriptstyle(rc+2)\log\gamma}}}\qquad
q=\frac{\mathchoice{rc+1}{rc+1}{rc+1}{{\scriptstyle
rc+1}}}{\mathchoice{rc+2}{rc+2}{rc+2}{{\scriptstyle rc+2}}}$

In fact, condition (6) follows from:

$\begin{array}[]{l}rc\lceil p\log n\rceil-\log_{\gamma}n^{q}\leq
rc(\frac{\mathchoice{1}{1}{1}{{\scriptstyle
1}}}{\mathchoice{(rc+2)\log\gamma}{(rc+2)\log\gamma}{(rc+2)\log\gamma}{{\scriptstyle(rc+2)\log\gamma}}}\log
n+1)-\frac{\mathchoice{rc+1}{rc+1}{rc+1}{{\scriptstyle
rc+1}}}{\mathchoice{rc+2}{rc+2}{rc+2}{{\scriptstyle rc+2}}}\frac{\log
n}{\log{\gamma}}\\\ =\frac{1}{(rc+2)\log\gamma}(rc\log
n+rc(rc+2)\log\gamma-(rc+1)\log n)\\\
=\frac{1}{(rc+2)\log\gamma}(rc(rc+2)\log\gamma-\log n)\\\
\leq\frac{1}{(rc+2)\log\gamma}(rc(rc+2)\log\gamma-\log a)\leq 0.\\\
\end{array}$

Thus, for $n\geq a$, we have:

$(1-\dfrac{1}{\gamma^{rc\lceil p\log n\rceil}})^{\frac{n}{2rc\lceil p\log
n\rceil}}\leq(1-\dfrac{1}{n^{q}})^{\frac{n}{2rc\lceil p\log
n\rceil}}\leq\left(\left(1-\frac{\mathchoice{1}{1}{1}{{\scriptstyle
1}}}{\mathchoice{n^{q}}{n^{q}}{n^{q}}{{\scriptstyle
n^{q}}}}\right)^{\frac{\mathchoice{n}{n}{n}{{\scriptstyle
n}}}{\mathchoice{\log n}{\log n}{\log n}{{\scriptstyle\log
n}}}}\right)^{\frac{\mathchoice{1}{1}{1}{{\scriptstyle
1}}}{\mathchoice{3rcp}{3rcp}{3rcp}{{\scriptstyle 3rcp}}}}.$

Since
$\lim_{n\rightarrow\infty}\left(1-\frac{\mathchoice{1}{1}{1}{{\scriptstyle
1}}}{\mathchoice{n^{q}}{n^{q}}{n^{q}}{{\scriptstyle
n^{q}}}}\right)^{\frac{\mathchoice{n}{n}{n}{{\scriptstyle
n}}}{\mathchoice{\log n}{\log n}{\log n}{{\scriptstyle\log n}}}}=0$, we have
$\operatorname*{limdef}\limits_{n\rightarrow\infty}Z_{n}=0$ as required.

######  Remark 43.

In the proof above, we used the fact that if $0<q<1$ then

$\lim_{n\rightarrow\infty}\left(1-\frac{\mathchoice{1}{1}{1}{{\scriptstyle
1}}}{\mathchoice{n^{q}}{n^{q}}{n^{q}}{{\scriptstyle
n^{q}}}}\right)^{\frac{\mathchoice{n}{n}{n}{{\scriptstyle
n}}}{\mathchoice{\log n}{\log n}{\log n}{{\scriptstyle\log n}}}}=0.$

We also remark that if $q\geq 1$ then

$\lim_{n\rightarrow\infty}\left(1-\frac{\mathchoice{1}{1}{1}{{\scriptstyle
1}}}{\mathchoice{n^{q}}{n^{q}}{n^{q}}{{\scriptstyle
n^{q}}}}\right)^{\frac{\mathchoice{n}{n}{n}{{\scriptstyle
n}}}{\mathchoice{\log n}{\log n}{\log n}{{\scriptstyle\log n}}}}=1.$

Thus, $p$ should be chosen to be sufficiently small so that Equation (6) in
the proof holds for some $q<1$.

We are now ready to prove Theorem 6. We restate the theorem.

######  Theorem 6 (Parameterized Infinite Monkey Theorem for Regular Tree
Languages).

Let ${\mathcal{G}}=(\Sigma,{\mathcal{N}},{\mathcal{R}})$ be an unambiguous and
strongly-connected regular tree grammar such that
$\\#\\!\left({\mathcal{L}}\\!\left({\mathcal{G}}\right)\right)=\infty$, and
$(S_{n})_{n\in{\rm Nature}}$ be a family of linear contexts in
${\mathcal{S}}({\mathcal{G}})$ such that $|S_{n}|=\mathrm{O}(n)$. Then there
exists a real constant $p>0$ such that for any $N\in{\mathcal{N}}$ the
following equation holds:

$\operatorname*{limdef}_{n\rightarrow\infty}\frac{\\#\\!\left(\\{T\in{\mathcal{L}}_{n}\\!\left({\mathcal{G}},N\right)\mid
S_{\lceil p\log n\rceil}\preceq
T\\}\right)}{\\#\\!\left({\mathcal{L}}_{n}\\!\left({\mathcal{G}},N\right)\right)}=1.$

######  Proof 3.25.

By Lemma 25, there exists a canonical, unambiguous and essentially strongly-
connected grammar
${\mathcal{G}}^{\prime}=(\Sigma,{\mathcal{N}}^{\prime},{\mathcal{R}}^{\prime})$
and a family $(\mathcal{I}_{N})_{N\in{\mathcal{N}}}$ of subsets
$\mathcal{I}_{N}\subseteq{\mathcal{N}}^{\prime}$ such that
${\mathcal{L}}\\!\left({\mathcal{G}},N\right)=\biguplus_{N^{\prime}\in\mathcal{I}_{N}}{\mathcal{L}}\\!\left({\mathcal{G}}^{\prime},N^{\prime}\right)$
for every $N\in{\mathcal{N}}$ and
${\mathcal{S}}({\mathcal{G}})\subseteq{\mathcal{S}}^{\mathrm{inf}}({\mathcal{G}}^{\prime})$.
Let
$\mathcal{I}^{\prime}_{N}\triangleq\mathcal{I}_{N}\cap{{\mathcal{N}}^{\prime}}^{\mathrm{inf}}=\\{N^{\prime}\in\mathcal{I}_{N}\mid{\mathcal{L}}\\!\left({\mathcal{G}}^{\prime},N^{\prime}\right)=\infty\\}$.
For any $N\in{\mathcal{N}}$, since
${\mathcal{L}}\\!\left({\mathcal{G}}\right)=\infty$ and ${\mathcal{G}}$ is
strongly connected, we have
${\mathcal{L}}\\!\left({\mathcal{G}},N\right)=\infty$, and hence
$\mathcal{I}^{\prime}_{N}\neq\emptyset$. By Lemma 42, there exists a real
constant $p>0$ such that, for each $N^{\prime}\in\mathcal{I}^{\prime}_{N}$,

$\displaystyle\operatorname*{limdef}_{n\rightarrow\infty}\frac{\\#\\!\left(\\{T\in{\mathcal{L}}_{n}\\!\left({\mathcal{G}}^{\prime},N^{\prime}\right)\mid
S_{\lceil p\log n\rceil}\preceq
T\\}\right)}{\\#\\!\left({\mathcal{L}}_{n}\\!\left({\mathcal{G}}^{\prime},N^{\prime}\right)\right)}=1.$
(8)

Thus, we have

$\displaystyle\
\operatorname*{limdef}\limits_{n\rightarrow\infty}\frac{\\#\\!\left(\\{T\in{\mathcal{L}}_{n}\\!\left({\mathcal{G}},N\right)\mid
S_{\lceil p\log n\rceil}\preceq
T\\}\right)}{\\#\\!\left({\mathcal{L}}_{n}\\!\left({\mathcal{G}},N\right)\right)}$
$\displaystyle=$ $\displaystyle\
\operatorname*{limdef}\limits_{n\rightarrow\infty}\frac{\sum_{N^{\prime}\in\mathcal{I}_{N}}\\#\\!\left(\\{T\in{\mathcal{L}}_{n}\\!\left({\mathcal{G}}^{\prime},N^{\prime}\right)\mid
S_{\lceil p\log n\rceil}\preceq
T\\}\right)}{\sum_{N^{\prime}\in\mathcal{I}_{N}}\\#\\!\left({\mathcal{L}}_{n}\\!\left({\mathcal{G}}^{\prime},N^{\prime}\right)\right)}$
$\displaystyle=$ $\displaystyle\
\operatorname*{limdef}\limits_{n\rightarrow\infty}\frac{\sum_{N^{\prime}\in\mathcal{I}^{\prime}_{N}}\\#\\!\left(\\{T\in{\mathcal{L}}_{n}\\!\left({\mathcal{G}}^{\prime},N^{\prime}\right)\mid
S_{\lceil p\log n\rceil}\preceq
T\\}\right)}{\sum_{N^{\prime}\in\mathcal{I}^{\prime}_{N}}\\#\\!\left({\mathcal{L}}_{n}\\!\left({\mathcal{G}}^{\prime},N^{\prime}\right)\right)}$
$\displaystyle=$ $\displaystyle\ 1$

as required; we have used Lemma 5 and Equation (8) in the last step.

##  4\. Proof of the Main Theorem on $\lambda$-calculus

This section proves our main theorem (Theorem 2). We first prepare a regular
tree grammar that generates the set of tree representations of elements of
${\iota}{\xi}$ in Section 4.1, and then apply Corollary 9 to obtain Theorem 2,
where $(T_{n})_{n\in{\rm Nature}}$ in the corollary are set to (the tree
representations of) the terms in the introduction that have long
$\beta$-reduction sequences.

###  4.1. Regular Tree Grammar ${\mathcal{G}}{(\delta,\iota,\xi)}$ of
${\iota}{\xi}$

Recall that ${\iota}{\xi}$ is the set of ($\alpha$-equivalence classes of)
closed well-typed terms, whose order, internal arity, and number of variables
are bounded above by $\delta$, $\iota$, and $\xi$ (consult Definition 1 for
the precise definition). The set ${\iota}{\xi}$ can be generated by the
following grammar (up to isomorphism). [grammar of ${\iota}{\xi}$] Let
$\delta,\iota,\xi\geq 0$ be integers and $X_{\xi}=\\{x_{1},\ldots,x_{\xi}\\}$
be a subset of $V$. The regular tree grammar
${\mathcal{G}}{(\delta,\iota,\xi)}$ is defined as
$(\Sigma{(\delta,\iota,\xi)},{\mathcal{N}}{(\delta,\iota,\xi)},{\mathcal{R}}{(\delta,\iota,\xi)})$
where:

$\displaystyle\Sigma{(\delta,\iota,\xi)}\triangleq$ $\displaystyle\
\\{x\mapsto 0\mid x\in X_{\xi}\\}\cup\\{@\mapsto 2\\}$ $\displaystyle\cup$
$\displaystyle\ \\{\lambda\overline{x}^{\tau}\mapsto
1\mid\overline{x}\in\\{{\ast}\\}\cup X_{\xi},\
\tau\in\mathrm{Types}(\delta-1,\iota)\\}$
$\displaystyle{\mathcal{N}}{(\delta,\iota,\xi)}\triangleq$ $\displaystyle\
\\{N_{\langle\Gamma;\tau\rangle}\mid\tau\in\mathrm{Types}(\delta,\iota),\mathop{\mathrm{Dom}}(\Gamma)\subseteq
X_{\xi},\
\mathrm{Im}\left(\Gamma\right)\subseteq\mathrm{Types}(\delta-1,\iota),$
$\displaystyle\
\qquad\qquad\Lambda(\langle\Gamma;\tau\rangle,\delta,\iota,\xi)\neq\emptyset\\}$
$\displaystyle{\mathcal{R}}{(\delta,\iota,\xi)}\triangleq$ $\displaystyle\
\\{N_{\langle\\{x_{i}:\tau\\};\tau\rangle}\longrightarrow
x_{i}\\}\cup\\{N_{\langle\Gamma;\sigma{\rightarrow}\tau\rangle}\longrightarrow\lambda{\ast}^{\sigma}(N_{\langle\Gamma;\tau\rangle})\\}$
$\displaystyle\cup$ $\displaystyle\
\\{N_{\langle\Gamma;\sigma{\rightarrow}\tau\rangle}\longrightarrow\lambda
x_{i}^{\sigma}(N_{\langle\Gamma\cup\\{x_{i}:\sigma\\};\tau\rangle})\mid
i=\min\\{j\mid x_{j}\in X_{\xi}\setminus\mathop{\mathrm{Dom}}(\Gamma)\\}\\}$
$\displaystyle\cup$ $\displaystyle\
\\{N_{\langle\Gamma;\tau\rangle}\longrightarrow@(N_{\langle\Gamma_{1};\sigma{\rightarrow}\tau\rangle},N_{\langle\Gamma_{2};\sigma\rangle})\mid\Gamma=\Gamma_{1}\cup\Gamma_{2}\\}$

The grammar above generates the tree representations of elements of
${\iota}{\xi}$, where a variable $x$, a lambda-abstraction, and an application
are represented respectively as the nullary tree constructor $x$, unary tree
constructor $\lambda\overline{x}$, and binary tree constructor $@$. The
nonterminal $N_{\langle\Gamma;\tau\rangle}$ is used to generate (the tree
representations of) the elements of
$\Lambda(\langle\Gamma;\tau\rangle,\delta,\iota,\xi)$; the condition
$\Lambda(\langle\Gamma;\tau\rangle,\delta,\iota,\xi)\neq\emptyset$ on
nonterminal $N_{\langle\Gamma;\tau\rangle}$ ensures that every nonterminal
generates at least one tree. To guarantee that the grammar generates at most
one tree for each $\alpha$-equivalence class $[t]_{\alpha}$, (i) variables are
chosen from the fixed set $X_{\xi}$, and (ii) in the rule for generating a
$\lambda$-abstraction, a variable is chosen in a deterministic manner. Note
that $\Sigma{(\delta,\iota,\xi)}$, ${\mathcal{N}}{(\delta,\iota,\xi)}$ and
${\mathcal{R}}{(\delta,\iota,\xi)}$ are finite. The finiteness of
${\mathcal{N}}{(\delta,\iota,\xi)}$ follows from that of $X_{\xi}$,
$\mathrm{Types}(\delta-1,\iota)$, and
$\\{\Gamma\mid\mathop{\mathrm{Dom}}(\Gamma)\subseteq X_{\xi},\
\mathrm{Im}\left(\Gamma\right)\subseteq\mathrm{Types}(\delta-1,\iota)\\}$. The
finiteness of ${\mathcal{R}}{(\delta,\iota,\xi)}$ also follows immediately
from that of ${\mathcal{N}}{(\delta,\iota,\xi)}$.

Let us consider the case where $\delta=\iota=\xi=1$. The grammar
${\mathcal{G}}{(1,1,1)}$ consists of the following components.

$\displaystyle\Sigma{(1,1,1)}$ $\displaystyle=\\{x_{1},@,\lambda
x_{1}^{\mathtt{o}},\lambda{\ast}^{\mathtt{o}}\\}\qquad{\mathcal{N}}{(1,1,1)}=\\{N_{\langle\emptyset;\mathtt{o}{\rightarrow}\mathtt{o}\rangle},N_{\langle\\{x_{1}:\mathtt{o}\\};\mathtt{o}\rangle},N_{\langle\\{x_{1}:\mathtt{o}\\};\mathtt{o}{\rightarrow}\mathtt{o}\rangle}\\}$
$\displaystyle{\mathcal{R}}{(1,1,1)}$
$\displaystyle=\begin{cases}N_{\langle\emptyset;\mathtt{o}{\rightarrow}\mathtt{o}\rangle}\longrightarrow\lambda
x_{1}^{\mathtt{o}}(N_{\langle\\{x_{1}:\mathtt{o}\\};\mathtt{o}\rangle})\\\
N_{\langle\\{x_{1}:\mathtt{o}\\};\mathtt{o}\rangle}\longrightarrow
x_{1}\mid@(N_{\langle\\{x_{1}:\mathtt{o}\\};{\mathtt{o}{\rightarrow}\mathtt{o}}\rangle},N_{\langle\\{x_{1}:\mathtt{o}\\};\mathtt{o}\rangle})\mid@(N_{\langle\emptyset;\mathtt{o}{\rightarrow}\mathtt{o}\rangle},N_{\langle\\{x_{1}:\mathtt{o}\\};\mathtt{o}\rangle})\\\
N_{\langle\\{x_{1}:\mathtt{o}\\};\mathtt{o}{\rightarrow}\mathtt{o}\rangle}\longrightarrow\lambda{\ast}^{\mathtt{o}}(N_{\langle\\{x_{1}:\mathtt{o}\\};\mathtt{o}\rangle}).\end{cases}$

There is an obvious embedding $e^{(\delta,\iota,\xi)}$ ($e$ for short) from
trees in ${\mathcal{T}}(\Sigma{(\delta,\iota,\xi)})$ into (not necessarily
well-typed) $\lambda$-terms. For
$N_{\langle\Gamma;\tau\rangle}\in{\mathcal{N}}{(\delta,\iota,\xi)}$ we define

$\pi^{(\delta,\iota,\xi)}_{\langle\Gamma;\tau\rangle}\triangleq[-]_{\alpha}\circ
e:{\mathcal{L}}\\!\left(N_{\langle\Gamma;\tau\rangle}\right)\rightarrow\Lambda(\langle\Gamma;\tau\rangle,\delta,\iota,\xi)$

where $[-]_{\alpha}$ maps a term to its $\alpha$-equivalence class. We
sometimes omit the superscript and/or the subscript and may write just $\pi$
for $\pi^{(\delta,\iota,\xi)}_{\langle\Gamma;\tau\rangle}$.

The following lemma says that ${\mathcal{G}}{(\delta,\iota,\xi)}$ gives a
complete representation system of the $\alpha$-equivalence classes.

######  Lemma 44.

For $\delta,\iota,\xi\geq 0$, $\
\pi^{(\delta,\iota,\xi)}_{\langle\Gamma;\tau\rangle}:{\mathcal{L}}\\!\left({\mathcal{G}}{(\delta,\iota,\xi)},N_{\langle\Gamma;\tau\rangle}\right)\rightarrow\Lambda(\langle\Gamma;\tau\rangle,\delta,\iota,\xi)$
is a size-preserving bijection.

######  Proof 4.1.

It is trivial that the image of $\pi_{\langle\Gamma;\tau\rangle}$ is contained
in $\Lambda(\langle\Gamma;\tau\rangle,\delta,\iota,\xi)$ and $\pi$ preserves
the size.

The injectivity, i.e., $e(T)\sim_{\alpha}e(T^{\prime})$ implies $T=T^{\prime}$
for
$T,T^{\prime}\in{\mathcal{L}}\\!\left(N_{\langle\Gamma;\tau\rangle}\right)$,
is shown by induction on the length of the leftmost rewriting sequence
$N_{\langle\Gamma;\tau\rangle}\longrightarrow^{*}T$ and by case analysis of
the rewriting rule used in the first step of the reduction sequence. In the
case analysis below, we use the fact that if
$T\in{\mathcal{L}}\\!\left(N_{\langle\Gamma;\tau\rangle}\right)$, then
$\mathbf{FV}(e(T))=\mathop{\mathrm{Dom}}(\Gamma)$, which can be proved by
straightforward induction.

  * •

Case for the rule $N_{\langle\\{x_{i}:\tau\\};\tau\rangle}\longrightarrow
x_{i}$: In this case, $T=x_{i}$. By the assumption
$e(T)\sim_{\alpha}e(T^{\prime})$, $T=T^{\prime}$ follows immediately.

  * •

Case for the rule
$N_{\langle\Gamma;\sigma{\rightarrow}\tau\rangle}\longrightarrow\lambda{\ast}^{\sigma}(N_{\langle\Gamma;\tau\rangle})$:
In this case, $T=\lambda{\ast}^{\sigma}(T_{1})$ with
$N_{\langle\Gamma;\tau\rangle}\longrightarrow^{*}T_{1}$. By the assumption
$e(T)\sim_{\alpha}e(T^{\prime})$, $T^{\prime}$ must be of the form
$\lambda\overline{x}^{\sigma}(T_{1}^{\prime})$ where (i) $\overline{x}$ does
not occur free in $e(T_{1}^{\prime})$, and (ii)
$e(T_{1})\sim_{\alpha}e(T_{1}^{\prime})$. Then $\overline{x}={\ast}$ and hence
we have
$N_{\langle\Gamma;\sigma{\rightarrow}\tau\rangle}\longrightarrow\lambda{\ast}^{\sigma}(N_{\langle\Gamma;\tau\rangle})$
with $N_{\langle\Gamma;\tau\rangle}\longrightarrow^{*}T_{1}^{\prime}$,
because, if $\overline{x}\neq{\ast}$, we have
$N_{\langle\Gamma;\sigma{\rightarrow}\tau\rangle}\longrightarrow\lambda\overline{x}^{\sigma}(N_{\langle\Gamma\cup\\{\overline{x}:\sigma\\};\tau\rangle})$
with
$N_{\langle\Gamma\cup\\{\overline{x}:\sigma\\};\tau\rangle}\longrightarrow^{*}T_{1}^{\prime}$,
and hence
$\mathbf{FV}(e(T^{\prime}_{1}))=\mathop{\mathrm{Dom}}(\Gamma\cup\\{\overline{x}:\sigma\\})$,
which contradicts the condition (i). Therefore, by the induction hypothesis,
we have $T_{1}=T_{1}^{\prime}$, which implies $T=T^{\prime}$ as required.

  * •

Case for the rule:
$N_{\langle\Gamma;\sigma{\rightarrow}\tau\rangle}\longrightarrow\lambda
x_{i}^{\sigma}(N_{\langle\Gamma\cup\\{x_{i}:\sigma\\};\tau\rangle})$, where
$i=\min\\{j\mid x_{j}\in X_{\xi}\setminus\mathop{\mathrm{Dom}}(\Gamma)\\}$. By
the assumption $e(T)\sim_{\alpha}e(T^{\prime})$, $T^{\prime}$ must be of the
form $\lambda x^{\sigma}(T_{1}^{\prime})$ where $x$ occurs free in
$e(T_{1}^{\prime})$, and
$[x^{\prime}/x_{i}]e(T_{1})\sim_{\alpha}[x^{\prime}/x]e(T_{1}^{\prime})$ for a
fresh variable $x^{\prime}$. Thus, by the definition of
${\mathcal{R}}{(\delta,\iota,\xi)}$, $T^{\prime}$ must have also been
generated by the same rule, i.e., $T^{\prime}=\lambda
x_{i}^{\sigma}(T_{1}^{\prime})$ with
$N_{\langle\Gamma\cup\\{x_{i}:\sigma\\};\tau\rangle}\longrightarrow^{*}T_{1}^{\prime}$.
By the induction hypothesis, we have $T_{1}=T_{1}^{\prime}$, which also
implies $T=T^{\prime}$ as required.

  * •

Case for the rule:
$N_{\langle\Gamma;\tau\rangle}\longrightarrow@(N_{\langle\Gamma_{1};\sigma{\rightarrow}\tau\rangle},N_{\langle\Gamma_{2};\sigma\rangle})$
where $\Gamma=\Gamma_{1}\cup\Gamma_{2}$. Then $T=@(T_{1},T_{2})$ with
$N_{\langle\Gamma_{1};\sigma{\rightarrow}\tau\rangle}\longrightarrow^{*}T_{1}$
and $N_{\langle\Gamma_{2};\sigma\rangle}\longrightarrow^{*}T_{2}$. By the
assumption $e(T)\sim_{\alpha}e(T^{\prime})$, $T^{\prime}$ must also be of the
form $@(T_{1}^{\prime},T_{2}^{\prime})$, with
$e(T_{1})\sim_{\alpha}e(T_{1}^{\prime})$ and
$e(T_{2})\sim_{\alpha}e(T_{2}^{\prime})$. Therefore, $T^{\prime}$ must also
have been generated by a rule for applications; hence
$N_{\langle\Gamma^{\prime}_{1};\sigma^{\prime}{\rightarrow}\tau\rangle}\longrightarrow^{*}T_{1}^{\prime}$
and
$N_{\langle\Gamma^{\prime}_{2};\sigma^{\prime}\rangle}\longrightarrow^{*}T_{2}^{\prime}$
for some $\Gamma_{1}^{\prime},\Gamma_{2}^{\prime},\sigma^{\prime}$ such that
$\Gamma=\Gamma^{\prime}_{1}\cup\Gamma^{\prime}_{2}$. By the condition
$e(T_{i})\sim_{\alpha}e(T_{i}^{\prime})$,
$\mathop{\mathrm{Dom}}(\Gamma_{i})=\mathbf{FV}(e(T_{i}))=\mathbf{FV}(e(T_{i}^{\prime}))=\mathop{\mathrm{Dom}}(\Gamma^{\prime}_{i})$
for each $i\in\\{1,2\\}$. Thus, since
$\Gamma_{1}\cup\Gamma_{2}=\Gamma^{\prime}_{1}\cup\Gamma^{\prime}_{2}$, we have
$\Gamma_{i}=\Gamma_{i}^{\prime}$, which also implies $\sigma=\sigma^{\prime}$
(since the type of a simply-typed $\lambda$-term is uniquely determined by the
term and the type environment). Therefore, by the induction hypothesis, we
have $T_{i}=T_{i}^{\prime}$ for each $i\in\\{1,2\\}$, which implies
$T=T^{\prime}$ as required.

Next we show the surjectivity, i.e., for any
$[t]_{\alpha}\in\Lambda(\langle\Gamma;\tau\rangle,\delta,\iota,\xi)$ there
exists $T\in{\mathcal{L}}\\!\left(N_{\langle\Gamma;\tau\rangle}\right)$ such
that $e(T)\sim_{\alpha}t$. For $\delta,\iota,\xi$ with
$X_{\xi}=\\{x_{1},\ldots,x_{\xi}\\}$ and
$N_{\langle\Gamma;\tau\rangle}\in{\mathcal{N}}{(\delta,\iota,\xi)}$, we define
a “renaming” function $\rho^{(\delta,\iota,\xi)}_{\langle\Gamma;\tau\rangle}$
($\rho_{\langle\Gamma;\tau\rangle}$ or $\rho$ for short) from
$\\{t\mid[t]_{\alpha}\in\Lambda(\langle\Gamma;\tau\rangle,\delta,\iota,\xi)\\}$
to ${\mathcal{L}}\\!\left(N_{\langle\Gamma;\tau\rangle}\right)$ by induction
on the size of $t$, so that $\pi{}(\rho(t))=[t]_{\alpha}$ holds.

$\begin{array}[]{ll}\rho_{\langle\\{x:\tau\\};\tau\rangle}(x)&\triangleq x\\\
\rho_{\langle\Gamma;\sigma{\rightarrow}\tau\rangle}(\lambda{\ast}^{\sigma}\\!.t)&\triangleq\lambda{\ast}^{\sigma}(\rho_{\langle\Gamma;\tau\rangle}(t))\\\
\rho_{\langle\Gamma;\sigma{\rightarrow}\tau\rangle}(\lambda
x^{\sigma}\\!.t)&\triangleq\lambda{\ast}^{\sigma}(\rho_{\langle\Gamma;\tau\rangle}(t))\qquad\qquad\hfill(\text{if
}x\notin\mathbf{FV}(t))\\\
\rho_{\langle\Gamma;\sigma{\rightarrow}\tau\rangle}(\lambda
x^{\sigma}\\!.t)&\triangleq\lambda
x_{i}^{\sigma}(\rho_{\langle\Gamma\cup\\{x_{i}:\sigma\\};\tau\rangle}([x_{i}\leftrightarrow
x]t))\text{ where $i\triangleq\min\\{j\mid x_{j}\in
X_{\xi}\setminus\mathop{\mathrm{Dom}}(\Gamma)\\}$}\\\ &\hfill(\text{if
}x\in\mathbf{FV}(t))\\\
\rho_{\langle\Gamma_{1}\cup\Gamma_{2};\tau\rangle}(t_{1}t_{2})&\triangleq@(\rho_{\langle\Gamma_{1};\sigma{\rightarrow}\tau\rangle}(t_{1}),\rho_{\langle\Gamma_{2};\sigma\rangle}(t_{2}))\hfill(\text{if
}\Gamma_{1}\vdash t_{1}:\sigma{\rightarrow}\tau\text{ and }\Gamma_{2}\vdash
t_{2}:\sigma)\end{array}$

Here, $[x\leftrightarrow y]t$ represents the term obtained by swapping every
occurrence of $x$ with that of $y$; for example, $[x\leftrightarrow y](\lambda
x.xy)=\lambda y.yx$. Note that in the last clause, if $\Gamma\vdash
t_{1}t_{2}:\tau$, then there exists a unique triple
$(\Gamma_{1},\Gamma_{2},\sigma)$ such that $\Gamma=\Gamma_{1}\cup\Gamma_{2}$,
$\Gamma_{1}\vdash t_{1}:\sigma{\rightarrow}\tau$, and $\Gamma_{2}\vdash
t_{2}:\sigma$. We can prove that $\pi{}(\rho(t))=[t]_{\alpha}$ holds for every
$\lambda$-term $t$ such that
$[t]_{\alpha}\in\Lambda(\langle\Gamma;\tau\rangle,\delta,\iota,\xi)$, by
straightforward induction on the size of $t$.

######  Lemma 45.

For $\delta,\iota,\xi\geq 0$, ${\mathcal{G}}{(\delta,\iota,\xi)}$ is
unambiguous.

######  Proof 4.2.

The proof is similar to that of the injectivity of Lemma 44. We show that, for
any $N_{\langle\Gamma;\tau\rangle}\in{\mathcal{N}}{(\delta,\iota,\xi)}$,
$T\in{\mathcal{T}}(\Sigma{(\delta,\iota,\xi)})$, and two leftmost rewriting
sequences of the form

$\displaystyle N_{\langle\Gamma;\tau\rangle}\longrightarrow
T^{(1)}\longrightarrow\dots\longrightarrow T^{(n)}=T\qquad(n\geq 1)$
$\displaystyle N_{\langle\Gamma;\tau\rangle}\longrightarrow
T^{\prime(1)}\longrightarrow\dots\longrightarrow
T^{\prime(n^{\prime})}=T\qquad(n^{\prime}\geq 1),$

$n=n^{\prime}$ and $T^{(k)}=T^{\prime(k)}$ hold for $1\leq k<n$. The proof
proceeds by induction on $n$, with case analysis on the rule
$N_{\langle\Gamma;\tau\rangle}\longrightarrow T^{(1)}$. As in the proof of
Lemma 44, we use the fact that if
$T\in{\mathcal{L}}\\!\left(N_{\langle\Gamma;\tau\rangle}\right)$, then
$\mathbf{FV}(e(T))=\mathop{\mathrm{Dom}}(\Gamma)$.

  * •

Case for the rule $N_{\langle\\{x_{i}:\tau\\};\tau\rangle}\longrightarrow
x_{i}$: In this case, $T=x_{i}$ and $n=1$. Since the root of $T^{\prime(1)}$
must be $x_{i}$, we have $T^{\prime(1)}=T$ and $n^{\prime}=1=n$.

  * •

Case for the rule
$N_{\langle\Gamma;\sigma{\rightarrow}\tau^{\prime}\rangle}\longrightarrow\lambda{\ast}^{\sigma}(N_{\langle\Gamma;\tau^{\prime}\rangle})$:
In this case, $n\geq 2$, $T^{(k)}=\lambda{\ast}^{\sigma}(T^{(k)}_{1})$ ($k\leq
n$), $T=\lambda{\ast}^{\sigma}(T_{1})$, and we have the following leftmost
rewriting sequences:

$N_{\langle\Gamma;\tau^{\prime}\rangle}=T^{(1)}_{1}\longrightarrow\dots\longrightarrow
T^{(n)}_{1}=T_{1}.$

Since the root of $T^{\prime(k)}$ is the same as that of $T$,
$T^{\prime(k)}=\lambda{\ast}^{\sigma}(T^{\prime(k)}_{1})$ for $k\leq
n^{\prime}$, and we have the following leftmost rewriting sequence:

$T^{\prime(1)}_{1}\longrightarrow\dots\longrightarrow
T^{\prime(n^{\prime})}_{1}=T_{1}.$

By the definition of rules, $T^{\prime(1)}$ must be of the form
$\lambda{\ast}^{\sigma}(N_{\langle\Gamma;\tau\rangle})$ and so
$T^{\prime(1)}_{1}=N_{\langle\Gamma;\tau\rangle}$. By the induction hypothesis
for $N_{\langle\Gamma;\tau\rangle}\longrightarrow T^{(2)}_{1}$, we have
$n=n^{\prime}$ and $T^{(k)}_{1}=T^{\prime(k)}_{1}$ for $2\leq k<n$. Thus we
have also $T^{(k)}=T^{\prime(k)}$ for $1\leq k<n$, as required.

  * •

Case for the rule:
$N_{\langle\Gamma;\sigma{\rightarrow}\tau^{\prime}\rangle}\longrightarrow\lambda
x_{i}^{\sigma}(N_{\langle\Gamma\cup\\{x_{i}:\sigma\\};\tau^{\prime}\rangle})$,
where $i=\min\\{j\mid x_{j}\in
X_{\xi}\setminus\mathop{\mathrm{Dom}}(\Gamma)\\}$. In this case, $n\geq 2$,
$T^{(k)}=\lambda x_{i}^{\sigma}(T^{(k)}_{1})$ ($k\leq n$), $T=\lambda
x_{i}^{\sigma}(T_{1})$, and we have the following leftmost rewriting
sequences:

$N_{\langle\Gamma\cup\\{x_{i}:\sigma\\};\tau^{\prime}\rangle}=T^{(1)}_{1}\longrightarrow\dots\longrightarrow
T^{(n)}_{1}=T_{1}.$

Since the root of $T^{\prime(k)}$ are the same as that of $T$,
$T^{\prime(k)}=\lambda x_{i}^{\sigma}(T^{\prime(k)}_{1})$ ($k\leq
n^{\prime}$), and we have the leftmost rewriting sequence:

$T^{\prime(1)}_{1}\longrightarrow\dots\longrightarrow
T^{\prime(n^{\prime})}_{1}=T_{1}.$

By the definition of rules,
$N_{\langle\Gamma;\sigma{\rightarrow}\tau^{\prime}\rangle}\longrightarrow\lambda
x_{i}^{\sigma}(T^{\prime(1)}_{1})$ implies that
$T^{\prime(1)}_{1}=N_{\langle\Gamma\cup\\{x_{i}:\sigma\\};\tau^{\prime}\rangle}$.
Hence by the induction hypothesis for
$N_{\langle\Gamma\cup\\{x_{i}:\sigma\\};\tau\rangle}\longrightarrow
T^{(2)}_{1}$, we have $n=n^{\prime}$ and $T^{(k)}_{1}=T^{\prime(k)}_{1}$ for
$2\leq k<n$. Thus we also have $T^{(k)}=T^{\prime(k)}$ for $1\leq k<n$.

  * •

Case for the rule:
$N_{\langle\Gamma;\tau\rangle}\longrightarrow@(N_{\langle\Gamma_{1};\sigma{\rightarrow}\tau\rangle},N_{\langle\Gamma_{2};\sigma\rangle})$
where $\Gamma=\Gamma_{1}\cup\Gamma_{2}$. In this case, $n=n_{1}+n_{2}-1$,
$n_{1},n_{2}\geq 2$, $T=@(T_{1},T_{2})$,

$\displaystyle T^{(k)}$
$\displaystyle=@(T^{(k)}_{1},N_{\langle\Gamma_{2};\sigma\rangle})$
$\displaystyle(1\leq k\leq n_{1})$ $\displaystyle T^{(n_{1}-1+k)}$
$\displaystyle=@(T_{1},T^{(k)}_{2})$ $\displaystyle(1\leq k\leq n_{2}),$

and we have the following leftmost rewriting sequences:

$\displaystyle N_{\langle\Gamma_{1};\sigma{\rightarrow}\tau\rangle}$
$\displaystyle=T^{(1)}_{1}\longrightarrow\dots\longrightarrow
T^{(n_{1})}_{1}=T_{1}$ $\displaystyle N_{\langle\Gamma_{2};\sigma\rangle}$
$\displaystyle=T^{(1)}_{2}\longrightarrow\dots\longrightarrow
T^{(n_{2})}_{2}=T_{2}.$

Since the root of $T^{\prime(1)}$ is $@$, $T^{\prime(1)}$ must be of the form
$@(N_{\langle\Gamma^{\prime}_{1};\sigma^{\prime}{\rightarrow}\tau\rangle},N_{\langle\Gamma^{\prime}_{2};\sigma^{\prime}\rangle})$
with $\Gamma^{\prime}_{1}\cup\Gamma^{\prime}_{2}=\Gamma$. Also let us consider
$T^{\prime(k)}$: we have $n=n^{\prime}_{1}+n^{\prime}_{2}-1$,
$n^{\prime}_{1},n^{\prime}_{2}\geq 2$,

$\displaystyle T^{\prime(k)}$
$\displaystyle=@(T^{\prime(k)}_{1},N_{\langle\Gamma^{\prime}_{2};\sigma^{\prime}\rangle})$
$\displaystyle(1\leq k\leq n^{\prime}_{1})$ $\displaystyle
T^{\prime(n^{\prime}_{1}-1+k)}$ $\displaystyle=@(T_{1},T^{\prime(k)}_{2})$
$\displaystyle(1\leq k\leq n^{\prime}_{2}),$

and we have the following leftmost rewriting sequences:

$\displaystyle
N_{\langle\Gamma^{\prime}_{1};\sigma^{\prime}{\rightarrow}\tau\rangle}$
$\displaystyle=T^{\prime(1)}_{1}\longrightarrow\dots\longrightarrow
T^{\prime(n^{\prime}_{1})}_{1}=T_{1}$ $\displaystyle
N_{\langle\Gamma^{\prime}_{2};\sigma^{\prime}\rangle}$
$\displaystyle=T^{\prime(1)}_{2}\longrightarrow\dots\longrightarrow
T^{\prime(n^{\prime}_{2})}_{2}=T_{2}.$

Since
$\mathop{\mathrm{Dom}}(\Gamma_{i})=\mathbf{FV}(e(T_{i}))=\mathop{\mathrm{Dom}}(\Gamma^{\prime}_{i})$
for each $i\in\\{1,2\\}$ and
$\Gamma_{1}\cup\Gamma_{2}=\Gamma^{\prime}_{1}\cup\Gamma^{\prime}_{2}$, we have
$\Gamma_{i}=\Gamma^{\prime}_{i}$, which also implies $\sigma=\sigma^{\prime}$.
Hence by the induction hypothesis for
$N_{\langle\Gamma_{1};\sigma{\rightarrow}\tau\rangle}\longrightarrow
T^{(2)}_{1}$ and for $N_{\langle\Gamma_{2};\sigma\rangle}\longrightarrow
T^{(2)}_{2}$, we have $n_{i}=n^{\prime}_{i}$ and
$T^{(k)}_{i}=T^{\prime(k)}_{i}$ for each $i\in\\{1,2\\}$ and $2\leq k<n_{i}$.
Thus we also have $T^{(k)}=T^{\prime(k)}$ for $1\leq k<n$.

###  4.2. Strong Connectivity and Aperiodicity

In this section, we restrict the grammar ${\mathcal{G}}{(\delta,\iota,\xi)}$
to ${\mathcal{G}}^{\emptyset}{(\delta,\iota,\xi)}$ by removing unnecessary
nonterminals, and show the strong connectivity and aperiodicity of
${\mathcal{G}}^{\emptyset}{(\delta,\iota,\xi)}$ for $\delta,\iota,\xi\geq 2$
(Lemma 49 below). Recall that the strong connectivity and aperiodicity is
required to apply Corollary 9 and Remark 10, respectively.

We define the restricted grammar
${\mathcal{G}}^{\emptyset}{(\delta,\iota,\xi)}$ by:

$\displaystyle{\mathcal{N}}^{\emptyset}{(\delta,\iota,\xi)}$
$\displaystyle\triangleq\\{N\in{\mathcal{N}}{(\delta,\iota,\xi)}\mid\text{$N$
is reachable n ${\mathcal{G}}{(\delta,\iota,\xi)}$ from some
$N_{\langle\emptyset;\sigma\rangle}\in{\mathcal{N}}{(\delta,\iota,\xi)}$}\\}$
$\displaystyle{\mathcal{R}}^{\emptyset}{(\delta,\iota,\xi)}$
$\displaystyle\triangleq\\{N\longrightarrow
T\in{\mathcal{R}}{(\delta,\iota,\xi)}\mid
N\in{\mathcal{N}}^{\emptyset}{(\delta,\iota,\xi)}\\}$
$\displaystyle{\mathcal{G}}^{\emptyset}{(\delta,\iota,\xi)}$
$\displaystyle\triangleq(\Sigma{(\delta,\iota,\xi)},{\mathcal{N}}^{\emptyset}{(\delta,\iota,\xi)},{\mathcal{R}}^{\emptyset}{(\delta,\iota,\xi)}).$

For $N\in{\mathcal{N}}^{\emptyset}{(\delta,\iota,\xi)}$, clearly
${\mathcal{L}}\\!\left({\mathcal{G}}^{\emptyset}{(\delta,\iota,\xi)},N\right)={\mathcal{L}}\\!\left({\mathcal{G}}{(\delta,\iota,\xi)},N\right)$.
Through the bijection $\pi$, we can show that, for any
$N_{\langle\Gamma;\tau\rangle}\in{\mathcal{N}}{(\delta,\iota,\xi)}$,
$N_{\langle\Gamma;\tau\rangle}$ also belongs to
${\mathcal{N}}^{\emptyset}{(\delta,\iota,\xi)}$ if and only if there exists a
term in ${\iota}{\xi}$ whose type derivation contains a type judgment of the
form $\Gamma\vdash t:\tau$.

The strong connectivity of ${\mathcal{G}}^{\emptyset}{(\delta,\iota,\xi)}$
follows from the following facts: (i) each
$N_{\langle\Gamma;\tau\rangle}\in{\mathcal{N}}^{\emptyset}{(\delta,\iota,\xi)}$
is reachable from some
$N_{\langle\emptyset;\tau^{\prime}\rangle}\in{\mathcal{N}}^{\emptyset}{(\delta,\iota,\xi)}$
(by the definition of ${\mathcal{G}}^{\emptyset}{(\delta,\iota,\xi)}$ above),
(ii) each
$N_{\langle\emptyset;\tau\rangle}\in{\mathcal{N}}^{\emptyset}{(\delta,\iota,\xi)}$
is reachable from
$N_{\langle\emptyset;\mathtt{o}{\rightarrow}\mathtt{o}\rangle}$ (Lemma 46
below), and (iii)
$N_{\langle\emptyset;\mathtt{o}{\rightarrow}\mathtt{o}\rangle}$ is reachable
from every
$N_{\langle\Gamma;\tau\rangle}\in{\mathcal{N}}^{\emptyset}{(\delta,\iota,\xi)}$
(Lemma 47 below).

######  Lemma 46.

Let $\delta,\iota\geq 2$ and $\xi\geq 1$ be integers. Then for any nonterminal
$N_{\langle\emptyset;\tau\rangle}\in{\mathcal{N}}^{\emptyset}{(\delta,\iota,\xi)}$,
$N_{\langle\emptyset;\tau\rangle}$ is reachable from
$N_{\langle\emptyset;\mathtt{o}{\rightarrow}\mathtt{o}\rangle}$.

######  Proof 4.3.

Let
$\tau=\tau_{1}{\rightarrow}\dots\rightarrow\tau_{n}{\rightarrow}\mathtt{o}$
and
$\tau_{i}=\tau^{i}_{1}{\rightarrow}\dots\rightarrow\tau^{i}_{\ell_{i}}{\rightarrow}\mathtt{o}$
for $i=1,\dots,n$. For $i=1,\dots,n$, let
$T_{\tau_{i}}\triangleq\lambda*^{\tau^{i}_{1}}(\dots\lambda*^{\tau^{i}_{\ell_{i}}}(x_{1})\dots)$.
Then, we have:

$\displaystyle N_{\langle
x_{1}:\mathtt{o};\tau_{i}\rangle}\longrightarrow\lambda*^{\tau^{i}_{1}}(N_{\langle
x_{1}:\mathtt{o};\tau^{i}_{2}{\rightarrow}\dots\rightarrow\tau^{i}_{\ell_{i}}{\rightarrow}\mathtt{o}\rangle})$
$\displaystyle\longrightarrow^{*}\lambda*^{\tau^{i}_{1}}(\dots\lambda*^{\tau^{i}_{\ell_{i}}}(N_{\langle
x_{1}:\mathtt{o};\mathtt{o}\rangle})\dots)$
$\displaystyle\longrightarrow\lambda*^{\tau^{i}_{1}}(\dots\lambda*^{\tau^{i}_{\ell_{i}}}(x_{1})\dots)=T_{\tau_{i}}$

and hence

$\displaystyle N_{\langle\emptyset;\mathtt{o}{\rightarrow}\mathtt{o}\rangle}$
$\displaystyle\longrightarrow\phantom{{}^{*}}\lambda
x_{1}^{\mathtt{o}}(N_{\langle x_{1}:\mathtt{o};\mathtt{o}\rangle})$
$\displaystyle\longrightarrow\phantom{{}^{*}}\lambda
x_{1}^{\mathtt{o}}(@(N_{\langle
x_{1}:\mathtt{o};\tau_{n}{\rightarrow}\mathtt{o}\rangle},N_{\langle
x_{1}:\mathtt{o};\tau_{n}\rangle}))\longrightarrow^{*}\lambda
x_{1}^{\mathtt{o}}(@(N_{\langle
x_{1}:\mathtt{o};\tau_{n}{\rightarrow}\mathtt{o}\rangle},T_{\tau_{n}}))$
$\displaystyle\longrightarrow^{*}\lambda
x_{1}^{\mathtt{o}}(@({@(\dots@(N_{\langle
x_{1}:\mathtt{o};\tau_{2}{\rightarrow}\cdots{\rightarrow}\tau_{n}{\rightarrow}\mathtt{o}\rangle},T_{\tau_{2}}),\dots)},T_{\tau_{n}}))$
$\displaystyle\longrightarrow\phantom{{}^{*}}\lambda
x_{1}^{\mathtt{o}}(@({@(\dots@(@(N_{\langle\emptyset;\tau_{1}{\rightarrow}\tau_{2}{\rightarrow}\cdots{\rightarrow}\tau_{n}{\rightarrow}\mathtt{o}\rangle},N_{\langle
x_{1}:\mathtt{o};\tau_{1}\rangle}),T_{\tau_{2}}),\dots)},T_{\tau_{n}}))$
$\displaystyle\longrightarrow^{*}\lambda
x_{1}^{\mathtt{o}}(@({@(\dots@(@(N_{\langle\emptyset;\tau\rangle},T_{\tau_{1}}),T_{\tau_{2}}),\dots)},T_{\tau_{n}})).$

######  Lemma 47.

Let $\delta,\iota,\xi\geq 2$ be integers. Then for any nonterminal
$N_{\langle\Gamma;\tau\rangle}\in{\mathcal{N}}^{\emptyset}{(\delta,\iota,\xi)}$,
$N_{\langle\emptyset;\mathtt{o}{\rightarrow}\mathtt{o}\rangle}$ is reachable
from $N_{\langle\Gamma;\tau\rangle}$.

######  Proof 4.4.

Suppose
$N_{\langle\Gamma;\tau\rangle}\in{\mathcal{N}}^{\emptyset}{(\delta,\iota,\xi)}$.
By the definition of ${\mathcal{N}}^{\emptyset}{(\delta,\iota,\xi)}$ (and
${\mathcal{N}}{(\delta,\iota,\xi)}$), there exists $t$ such that
$[t]_{\alpha}\in\Lambda(\langle\Gamma;\tau\rangle,\delta,\iota,\xi)$. Let
$T\triangleq\pi^{-1}([t]_{\alpha})\in{\mathcal{L}}\\!\left(N_{\langle\Gamma;\tau\rangle}\right)$.
Now $T$ contains at least one (possibly bound) variable, say $x$, and let
$\sigma$ be the type of $x$. Since
$T\in{\mathcal{L}}\\!\left(N_{\langle\Gamma;\tau\rangle}\right)$, there exists
a linear context $C$ such that

$N_{\langle\Gamma;\tau\rangle}\longrightarrow^{*}C[N_{\langle\\{x:\sigma\\};\sigma\rangle}]\longrightarrow
C[x]=T.$

We show, by the induction on the structure of $\sigma$, that
$N_{\langle\\{x:\sigma\\};\sigma\rangle}\longrightarrow^{*}C^{\prime}[N_{\langle\\{y:\mathtt{o}\\};y\rangle}]$
for some $y$ and linear context $C^{\prime}$. The case for $\sigma=\mathtt{o}$
is obvious. If $\sigma=\sigma^{\prime}\to\tau^{\prime}$, then since $\xi\geq
2$, we obtain:

$\begin{array}[]{l}N_{\langle\\{x:\sigma\\};\sigma\rangle}\longrightarrow\lambda
x_{i}^{\sigma^{\prime}}N_{\langle\\{x:\sigma,x_{i}:\sigma^{\prime}\\};\tau^{\prime}\rangle}\longrightarrow\lambda
x_{i}^{\sigma^{\prime}}(@(N_{\langle\\{x:\sigma\\};\sigma\rangle},N_{\langle\\{x_{i}:\sigma^{\prime}\\};\sigma^{\prime}\rangle}))\\\
\longrightarrow\lambda
x_{i}^{\sigma^{\prime}}(@(x,N_{\langle\\{x_{i}:\sigma^{\prime}\\};\sigma^{\prime}\rangle}))\end{array}$

by “$\eta$-expansion”. By the induction hypothesis, we have
$N_{\langle\\{x_{i}:\sigma^{\prime}\\};\sigma^{\prime}\rangle}\longrightarrow^{*}C^{\prime\prime}[N_{\langle\\{y:\mathtt{o}\\};\mathtt{o}\rangle}]$
for some $y$ and 1-context $C^{\prime\prime}$. Thus, the result holds for
$C^{\prime}=\lambda x_{i}^{\sigma^{\prime}}(@(x,C^{\prime\prime}))$.

By using the property above, we obtain

$\begin{array}[]{l}N_{\langle\Gamma;\tau\rangle}\longrightarrow^{*}C[N_{\langle\\{x:\sigma\\};\sigma\rangle}]\longrightarrow^{*}C[C^{\prime}[N_{\langle\\{y:\mathtt{o}\\};\mathtt{o}\rangle}]]\\\
\longrightarrow
C[C^{\prime}[@(N_{\langle\emptyset;\mathtt{o}\to\mathtt{o}\rangle},N_{\langle\\{y:\mathtt{o}\\};\mathtt{o}\rangle})]]\longrightarrow
C[C^{\prime}[@(N_{\langle\emptyset;\mathtt{o}\to\mathtt{o}\rangle},y)]].\end{array}$

Thus, $N_{\langle\emptyset;\mathtt{o}{\rightarrow}\mathtt{o}\rangle}$ is
reachable from $N_{\langle\Gamma;\tau\rangle}$.

######  Lemma 48.

Let $\delta,\iota\geq 2$ and $\xi\geq 1$ be integers. Then for any integer
$n\geq 5$, the nonterminal
$N_{\langle\emptyset;\mathtt{o}{\rightarrow}\mathtt{o}\rangle}$ of
${\mathcal{G}}^{\emptyset}{(\delta,\iota,\xi)}$ satisfies
${\mathcal{L}}_{n}\\!\left(N_{\langle\emptyset;\mathtt{o}{\rightarrow}\mathtt{o}\rangle}\right)\neq\emptyset$.

######  Proof 4.5.

For simplicity of the presentation, here we identify trees with terms by the
size-preserving bijection $\pi$. The proof proceeds by induction on $n$. For
$n=5,6,7$, the following terms

$\displaystyle\lambda x^{\mathtt{o}}\\!.(\lambda{\ast}^{\mathtt{o}}\\!.x)x$
$\displaystyle\lambda
x^{\mathtt{o}}\\!.(\lambda{\ast}^{\mathtt{o}{\rightarrow}\mathtt{o}}\\!.x)(\lambda{\ast}^{\mathtt{o}}\\!.x)$
$\displaystyle\lambda
x^{\mathtt{o}}\\!.(\lambda{\ast}^{\mathtt{o}{\rightarrow}\mathtt{o}{\rightarrow}\mathtt{o}}\\!.x)\lambda{\ast}^{\mathtt{o}}\\!.\lambda{\ast}^{\mathtt{o}}\\!.x$

belong to
${\mathcal{L}}_{n}\\!\left(N_{\langle\emptyset;\mathtt{o}{\rightarrow}\mathtt{o}\rangle}\right)$,
respectively. For $n\geq 8$, by the induction hypothesis, there exists
$t\in{\mathcal{L}}_{n-3}\\!\left(N_{\langle\emptyset;\mathtt{o}{\rightarrow}\mathtt{o}\rangle}\right)$.
Thus we have $\lambda
x.tx\in{\mathcal{L}}_{n}\\!\left(N_{\langle\emptyset;\mathtt{o}{\rightarrow}\mathtt{o}\rangle}\right)$
as required.

The following is the main result of this subsection.

######  Lemma 49.

${\mathcal{G}}^{\emptyset}{(\delta,\iota,\xi)}$ is strongly connected and
aperiodic for any $\delta,\iota,\xi\geq 2$.

######  Proof 4.6.

Strong connectivity follows from Lemmas 46 and 47, and the definition of
${\mathcal{G}}^{\emptyset}{(\delta,\iota,\xi)}$ (as stated at the beginning of
this subsection). The aperiodicity follows from Lemma 48 and strong
connectivity. (Note that for every nonterminal $N$, there exists a linear
context
$U\in{\mathcal{L}}\\!\left({\mathcal{G}},N_{\langle\emptyset;\mathtt{o}{\rightarrow}\mathtt{o}\rangle}{\Rightarrow}N\right)$.
Thus, for any $n\geq|U|+5$,
${\mathcal{L}}_{n}\\!\left({\mathcal{G}},N\right)\supseteq\\{U[T]\mid
T\in{\mathcal{L}}_{n-|U|}\\!\left({\mathcal{G}},N_{\langle\emptyset;\mathtt{o}{\rightarrow}\mathtt{o}\rangle}\right)\\}\neq\emptyset$.)

###  4.3. Explosive Terms

In this section, we define a family $(\mathit{Expl}_{n}^{k})_{n}$ of
$\lambda$-terms, which have long $\beta$-reduction sequences. They play the
role of $(T_{n})_{n}$ in Corollary 9.

We define a “duplicating term” $\mathit{Dup}\triangleq\lambda
x^{\mathtt{o}}.(\lambda x^{\mathtt{o}}.\lambda{\ast}^{\mathtt{o}}.x)x\,x$, and
$\mathit{Id}\triangleq\lambda x^{\mathtt{o}}.x$. For two terms $t$,
$t^{\prime}$ and integer $n\geq 1$, we define the “$n$-fold application”
operation $\mathop{{\uparrow}^{n}}$ by
$t\mathop{{\uparrow}^{0}}t^{\prime}\triangleq t^{\prime}$ and
$t\mathop{{\uparrow}^{n}}t^{\prime}\triangleq
t(t\mathop{{\uparrow}^{n-1}}t^{\prime})$. For an integer $k\geq 2$, we define
an order-$k$ term

$\overline{2}_{k}\triangleq\lambda f^{\tau^{(k-1)}}.\lambda
x^{\tau^{(k-2)}}.f(fx)$

where $\tau^{(i)}$ is defined by $\tau^{(0)}\triangleq\mathtt{o}$ and
$\tau^{(i+1)}\triangleq\tau^{(i)}{\rightarrow}\tau^{(i)}$.

[explosive terms] Let $m\geq 1$ and $k\geq 2$ be integers. We define the
_explosive term $\mathit{Expl}_{m}^{k}$_ by:

$\mathit{Expl}_{m}^{k}\triangleq\lambda
x^{\mathtt{o}}.\bigl{(}(\overline{2}_{k}\mathop{{\uparrow}^{m}}\overline{2}_{k-1})\overline{2}_{k-2}\cdots\overline{2}_{2}\,\mathit{Dup}(\mathit{Id}\,x)\bigr{)}.$

We state key properties of $\mathit{Expl}_{m}^{k}$ below.

######  Lemma 50 (explosive).

  1. (1)

$\emptyset\vdash\mathit{Expl}_{m}^{k}:\mathtt{o}{\rightarrow}\mathtt{o}$ is
derivable.

  2. (2)

$\mathtt{ord}(\mathit{Expl}_{m}^{k})=k$,
$\mathtt{iar}(\mathit{Expl}_{m}^{k})=k$ and
$\\#\\!\left(\smash{\mathbf{V}(\mathit{Expl}_{m}^{k})}\right)=2$.

  3. (3)

$|\mathit{Expl}_{m}^{k}|=8m+8k-2$.

  4. (4)

$[\mathit{Expl}_{m}^{k}]_{\alpha}\in\Lambda(\langle\emptyset;\mathtt{o}{\rightarrow}\mathtt{o}\rangle,\delta,\iota,\xi)$
if $\delta$, $\iota\geq k$ and $\xi\geq 2$.

  5. (5)

If a term $t$ satisfies $\mathit{Expl}_{m}^{k}\preceq t$, then
$\beta(t)\geq{\mathbf{exp}_{k}(m)}$ holds.

######  Proof 4.7.

First, observe that by the definition of $\overline{2}_{k}$, we have:

$|\overline{2}_{k}|=7,\quad\vdash\overline{2}_{k}:\tau^{(k)},\quad\mathtt{ord}(\overline{2}_{k})=k,\quad\mathtt{iar}(\overline{2}_{k})=k.$

(1) is obvious, and in the derivation of
$\emptyset\vdash\mathit{Expl}_{m}^{k}:\mathtt{o}{\rightarrow}\mathtt{o}$,
$\overline{2}_{k}$ is a subterm that has a type of the largest order and
internal arity. Thus, (2) follows also immediately from
$\mathtt{ord}(\overline{2}_{k})=\mathtt{iar}(\overline{2}_{k})=k$, and
$\smash{\mathbf{V}(\mathit{Expl}_{m}^{k})}=\\{f,x\\}$.

(3) follows from the following calculation.

$\begin{array}[]{ll}|\mathit{Expl}_{m}^{k}|&=1+|\overline{2}_{k}\mathop{{\uparrow}^{m}}\overline{2}_{k-1}|+\Sigma_{i=2}^{k-2}(1+|\overline{2}_{i}|)+(1+|\mathit{Dup}|)+(1+|\mathit{Id}\,x|)\\\
&\hfill\mbox{(by $|t_{0}t_{1}\cdots
t_{n}|=|t_{0}|+\Sigma_{i=1}^{n}(1+|t_{i}|)$)}\\\
&=1+((|\overline{2}_{k}|+1)m+|\overline{2}_{k-1}|)+\Sigma_{i=2}^{k-2}(1+|\overline{2}_{i}|)+(1+|\mathit{Dup}|)+(1+|\mathit{Id}\,x|)\\\
&=1+(8m+7)+8(k-3)+9+5=8m+8k-2.\end{array}$

(4) follows from (1) and (2).

The proof for (5) is the same as the corresponding proof in [1].

###  4.4. Proof of the Main Theorem

We are now ready to prove Theorem 2.

######  Proof 4.8 (Proof of Theorem 2).

We apply Corollary 9 with Remark 10 to the grammar
${\mathcal{G}}^{\emptyset}{(\delta,\iota,\xi)}$, which is unambiguous by Lemma
45, and aperiodic and strongly connected by Lemma 49. We define
$T_{n}\triangleq\pi^{-1}([\mathit{Expl}_{n}^{k}]_{\alpha})$; then by Lemma
50(3), we have $|T_{n}|=8n+8k-2=\mathrm{O}(n)$. Thus, by Corollary 9 (with
Remark 10, which allows us to replace
$\operatorname*{limdef}_{n\rightarrow\infty}$ with
$\lim_{n\rightarrow\infty}$), there exists $p>0$ such that, for
$\mathcal{I}\triangleq\\{N_{\langle\emptyset;\tau\rangle}\mid\tau\in\mathrm{Types}(\delta,\iota)\\}$,

$\lim_{n\rightarrow\infty}\frac{\\#\\!\left(\\{(N,T)\in\coprod_{N\in\mathcal{I}}{\mathcal{L}}_{n}\\!\left({\mathcal{G}}^{\emptyset}{(\delta,\iota,\xi)},N\right)\mid
T_{\lceil p\log n\rceil}\preceq
T\\}\right)}{\\#\\!\left(\coprod_{N\in\mathcal{I}}{\mathcal{L}}_{n}\\!\left({\mathcal{G}}^{\emptyset}{(\delta,\iota,\xi)},N\right)\right)}=1.$
(9)

For $n\in{\rm Nature}$, we have

$\\{[t]_{\alpha}\in\Lambda_{n}(\delta,\iota,\xi)\mid\mathit{Expl}_{\lceil
p\log n\rceil}^{k}\preceq
t\\}\subseteq\\{[t]_{\alpha}\in\Lambda_{n}(\delta,\iota,\xi)\mid\beta(t)\geq{\mathbf{exp}_{k-1}(n^{p})}\\}$
(10)

by Lemma 50(5), and

$\Lambda_{n}(\delta,\iota,\xi)\ =\
\,\biguplus_{\mathclap{\tau\in\mathrm{Types}(\delta,\iota)}}\,\Lambda_{n}(\langle\emptyset;\tau\rangle,\delta,\iota,\xi)\
\cong\
\,\coprod_{\mathclap{N\in\mathcal{I}}}\,{\mathcal{L}}_{n}\\!\left({\mathcal{G}}^{\emptyset}{(\delta,\iota,\xi)},N\right)$
(11)

by Lemma 44.

Therefore, we have:

$\displaystyle 1\geq\ $
$\displaystyle\frac{\\#\\!\left(\\{[t]_{\alpha}\in\Lambda_{n}(\delta,\iota,\xi)\mid\beta(t)\geq{\mathbf{exp}_{k-1}(n^{p})}\\}\right)}{\\#\\!\left(\Lambda_{n}(\delta,\iota,\xi)\right)}$
$\displaystyle\geq\ $
$\displaystyle\frac{\\#\\!\left(\\{[t]_{\alpha}\in\Lambda_{n}(\delta,\iota,\xi)\mid\mathit{Expl}_{\lceil
p\log n\rceil}^{k}\preceq
t\\}\right)}{\\#\\!\left(\Lambda_{n}(\delta,\iota,\xi)\right)}$ ($\because$ by
(10)) $\displaystyle=\ $
$\displaystyle\frac{\\#\\!\left(\\{(N,T)\in\coprod_{N\in\mathcal{I}}\,{\mathcal{L}}_{n}\\!\left({\mathcal{G}}^{\emptyset}{(\delta,\iota,\xi)},N\right)\mid
T_{\lceil p\log n\rceil}\preceq
T\\}\right)}{\\#\\!\left(\coprod_{N\in\mathcal{I}}\,{\mathcal{L}}_{n}\\!\left({\mathcal{G}}^{\emptyset}{(\delta,\iota,\xi)},N\right)\right)}$
($\because$ by (11))

Since the right hand side converges to $1$ by (9), we have

$\lim_{n\rightarrow\infty}\frac{\\#\\!\left(\\{[t]_{\alpha}\in\Lambda_{n}(\delta,\iota,\xi)\mid\beta(t)\geq{\mathbf{exp}_{k-1}(n^{p})}\\}\right)}{\\#\\!\left(\Lambda_{n}(\delta,\iota,\xi)\right)}=1$

as required.

##  5\. Related Work

As mentioned in Section 1, there are several pieces of work on probabilistic
properties of untyped $\lambda$-terms [2, 3, 4]. David et al. [2] have shown
that almost all untyped $\lambda$-terms are strongly normalizing, whereas the
result is opposite for terms expressed in SK combinators (the latter result
has later been generalized for arbitrary Turing complete combinator bases
[24]). Their former result implies that untyped $\lambda$-terms do _not_
satisfy the infinite monkey theorem, i.e., for any term $t$, the probability
that a randomly chosen term of size $n$ contains $t$ as a subterm tends to
_zero_.

Bendkowski et al. [4] proved that almost all terms in de Brujin representation
are not strongly normalizing, by regarding the size of an index $i$ is $i+1$,
instead of the constant $1$. The discrepancies among those results suggest
that this kind of probabilistic property is quite fragile and depends on the
definition of the syntax and the size of terms. Thus, the setting of our
paper, especially the assumption on the boundedness of internal arities and
the number of variables is a matter of debate, and it would be interesting to
study how the result changes for different assumptions.

We are not aware of similar studies on _typed_ $\lambda$-terms. In fact, in
their paper about combinatorial aspects of $\lambda$-terms, Grygiel and
Lescanne [3] pointed out that the combinatorial study of typed $\lambda$-terms
is difficult, due to the lack of (simple) recursive definition of typed terms.
In the present paper, we have avoided the difficulty by making the assumption
on the boundedness of internal arities and the number of variables (which is,
as mentioned above, subject to a debate though).

Choppy et al. [25] proposed a method to evaluate the average number of
reduction steps for a restricted class of term rewriting systems called
_regular_ rewriting systems. In our context, the average number of reduction
steps is not of much interest; note that, as the worst-case number of
reduction steps is $k$-fold exponential for order-$k$ terms, the average is
also $k$-fold exponential, even if it were the case that the number of
reduction steps is small for almost all terms.

In a larger context, our work may be viewed as an instance of the studies of
average-case complexity [26, Chapter 10], which discusses “typical-case
feasibility”. We are not aware of much work on the average-case complexity of
problems with hyper-exponential complexity.

As a result related to our parameterized infinite monkey theorem for trees
(Theorem 6), Steyaert and Flajolet [27] studied the probability that a given
pattern (which is, in our terminology, a tree context of which every leaf is a
hole) occurs at a randomly chosen node of a randomly chosen tree. Their result
immediately yields a _non-parameterized_ infinite monkey theorem for trees
(which says that the probability that a given pattern occurs in a sufficiently
large tree tends to $1$), but their technique does not seem directly
applicable to obtain our _parameterized_ version.

##  6\. Conclusion

We have shown that almost every simply-typed $\lambda$-term of order $k$ has a
$\beta$-reduction sequence as long as $(k-1)$-fold exponential in the term
size, under a certain assumption. To our knowledge, this is the first result
of this kind for typed $\lambda$-terms. We obtained the result through the
parameterized infinite monkey theorem for regular tree grammars, which may be
of independent interest.

A lot of questions are left for future work, such as (i) whether our
assumption (on the boundedness of arities and the number of variables) is
reasonable, and how the result changes for different assumptions, (ii) whether
our result is optimal (e.g., whether almost every term has a $k$-fold
exponentially long reduction sequence), and (iii) whether similar results hold
for Terui’s decision problems [15] and/or the higher-order model checking
problem [7]. To resolve the question (ii) above, it may be useful to conduct
experiments to count the number of reduction steps for randomly generated
terms.

#### Acknowledgment

We would like to thank anonymous referees for useful comments. This work was
supported by JSPS KAKENHI Grant Number JP15H05706.

## References

  * [1] Beckmann, A.:  Exact bounds for lengths of reductions in typed lambda-calculus.  Journal of Symbolic Logic 66(3) (2001) 1277–1285
  * [2] David, R., Grygiel, K., Kozik, J., Raffalli, C., Theyssier, G., Zaionc, M.:  Asymptotically almost all $\lambda$-terms are strongly normalizing.  Logical Methods in Computer Science 9(1) (2013)
  * [3] Grygiel, K., Lescanne, P.:  Counting and generating lambda terms.  Journal of Functional Programming 23(05) (2013) 594–628
  * [4] Bendkowski, M., Grygiel, K., Lescanne, P., Zaionc, M.:  A Natural Counting of Lambda Terms.  In: SOFSEM 2016: Theory and Practice of Computer Science: 42nd International Conference on Current Trends in Theory and Practice of Computer Science, Harrachov, Czech Republic, January 23-28, 2016, Proceedings. Springer Berlin Heidelberg, Berlin, Heidelberg (2016) 183–194
  * [5] Flajolet, P., Sedgewick, R.:  Analytic Combinatorics. 1 edn.  Cambridge University Press, New York, NY, USA (2009)
  * [6] Knapik, T., Niwinski, D., Urzyczyn, P.:  Higher-order pushdown trees are easy.  In: Foundations of Software Science and Computation Structures, 5th International Conference, FOSSACS 2002. Volume 2303 of Lecture Notes in Computer Science., Springer (2002) 205–222
  * [7] Ong, C.H.L.:  On model-checking trees generated by higher-order recursion schemes.  In: 21th IEEE Symposium on Logic in Computer Science (LICS 2006), IEEE Computer Society Press (2006) 81–90
  * [8] Kobayashi, N.:  Model checking higher-order programs.  Journal of the ACM 60(3) (2013)
  * [9] Broadbent, C.H., Kobayashi, N.:  Saturation-based model checking of higher-order recursion schemes.  In: Proceedings of CSL 2013. Volume 23 of LIPIcs. (2013) 129–148
  * [10] Ramsay, S., Neatherway, R., Ong, C.H.L.:  An abstraction refinement approach to higher-order model checking.  In: Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages (POPL). (2014)
  * [11] Kobayashi, N.:  Types and higher-order recursion schemes for verification of higher-order programs.  In: Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages (POPL), ACM Press (2009) 416–428
  * [12] Kobayashi, N., Sato, R., Unno, H.:  Predicate abstraction and CEGAR for higher-order model checking.  In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), ACM Press (2011) 222–233
  * [13] Ong, C.H.L., Ramsay, S.:  Verifying higher-order programs with pattern-matching algebraic data types.  In: Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages (POPL), ACM Press (2011) 587–598
  * [14] Sato, R., Unno, H., Kobayashi, N.:  Towards a scalable software model checker for higher-order programs.  In: Proceedings of the ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation, PEPM 2013, ACM Press (2013) 53–62
  * [15] Terui, K.:  Semantic evaluation, intersection types and complexity of simply typed lambda calculus.  In: 23rd International Conference on Rewriting Techniques and Applications (RTA’12). Volume 15 of LIPIcs., Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2012) 323–338
  * [16] Mairson, H.G.:  Deciding ML typability is complete for deterministic exponential time.  In: Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages (POPL), ACM Press (1990) 382–401
  * [17] Kfoury, A.J., Tiuryn, J., Urzyczyn, P.:  ML typability is DEXTIME-complete.  In: Proceedings of CAAP ’90. Volume 431 of Lecture Notes in Computer Science., Springer (1990) 206–220
  * [18] Sin’ya, R., Asada, K., Kobayashi, N., Tsukada, T.:  Almost every simply typed $\lambda$-term has a long $\beta$-reduction sequence.  In: Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings. Volume 10203 of Lecture Notes in Computer Science. (2017) 53–68
  * [19] Barendregt, H., Dekkers, W., Statman, R.:  Lambda Calculus with Types.  Cambridge University Press (2013)
  * [20] Saoudi, A.:  Rational and recognizable infinite tree sets.  In Nivat, M., Podelski, A., eds.: Tree Automata and Languages.  North-Holland, Amsterdam (1992) 225–234
  * [21] Comon, H., Dauchet, M., Gilleron, R., Löding, C., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.:  Tree automata techniques and applications.  Available on: http://www.grappa.univ-lille3.fr/tata (2007) release October, 12th 2007.
  * [22] Heintze, N., McAllester, D.A.:  Linear-time subtransitive control flow analysis.  In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). (1997) 261–272
  * [23] Mureşan, M.:  A concrete approach to classical analysis.  CMS books in mathematics. Springer (2009)
  * [24] Bendkowski, M., Grygiel, K., Zaionc, M.:  On the likelihood of normalization in combinatory logic.  J. Log. Comput. 27(7) (2017) 2251–2269
  * [25] Choppy, C., Kaplan, S., Soria, M.:  Complexity analysis of term-rewriting systems.  Theor. Comput. Sci. 67(2&3) (1989) 261–282
  * [26] Goldreich, O.:  Computational Complexity: A Conceptual Perspective.  Cambridge University Press (2008)
  * [27] Steyaert, J.M., Flajolet, P.:  Patterns and pattern-matching in trees: An analysis.  Information and Control 58(1) (1983) 19 – 58

##  Appendix A A List of Notations

notation | explanation | introduced at:
---|---|---
$\\#\\!\left(X\right)$ | the cardinality of set $X$, or the length of sequence $X$ | Section 2.1
$s.i$ | the $i$-th element of sequence $s$ | Section 2.1
$\mathop{\mathrm{Dom}}(f)$ | the domain of function $f$ | Section 2.1
$\mathrm{Im}\left(f\right)$ | the image of function $f$ | Section 2.1
$\tau$ | a type (of a simply-typed $\lambda$-term); | Section 2.1
$\mathtt{ord}(\tau)$ | the order of type $\tau$ | Section 2.1
$\mathtt{iar}(\tau)$ | the internal arity of type $\tau$ | Section 2.1
$\mathrm{Types}(\delta,\iota)$ |  the set of types whose order and internal arity are bounded by $\delta$ and $\iota$ respectively | Section 2.1
$t$ | a $\lambda$-term | Section 2.1
$\beta(t)$ | the maximal length of $\beta$-reduction sequences of $t$ | Section 2.1
$\delta$ | a bound on the order of $\lambda$-terms | Section 2.1
$\iota$ | a bound on the arity of $\lambda$-terms | Section 2.1
$\xi$ | a bound on the number of variables used in $\lambda$-terms | Section 2.1
$\Lambda(\langle\Gamma;\tau\rangle,\delta,\iota,\xi)$ |  the set of $\alpha$-equivalence classes of terms $t$ such that $\Gamma\vdash t:\tau$, with the given bounds | Section 2.1
$\Lambda_{n}(\langle\Gamma;\tau\rangle,\delta,\iota,\xi)$ |  Like $\Lambda(\langle\Gamma;\tau\rangle,\delta,\iota,\xi)$, but the term size is restricted to $n$ | Section 2.1
${\iota}{\xi}$ |  the set of $\alpha$-equivalence classes of closed well-typed terms, with the given bounds | Section 2.1
$\Lambda_{n}(\delta,\iota,\xi)$ |  Like ${\iota}{\xi}$, but the term size is restricted to $n$ | Section 2.1
$T$ | a tree | Section 2.2
$|T|$ | the size of tree $T$ | Section 2.2
$C$ | a tree context | Section 2.2
$|C|$ | the size of context $C$ | Section 2.2
$C\preceq C^{\prime}$ |  $C$ is a subcontext of $C^{\prime}$ | Section 2.2
$S$ | a linear context | Section 2.2
$U$ | an affine context | Section 2.2
$N$ | a nonterminal | Section 2.2
$a$ | a terminal symbol | Section 2.2
${\mathcal{G}}$ | a grammar | Section 2.2
$\kappa$ | a context type | Section 2.2
${\mathcal{L}}\\!\left({\mathcal{G}},N\right)$ | the set of trees generated by $N$ | Section 2.2
${\mathcal{L}}_{n}\\!\left({\mathcal{G}},N\right)$ |  Like ${\mathcal{L}}\\!\left({\mathcal{G}},N\right)$, but the tree size is restricted to $n$ | Section 2.2
${\mathcal{L}}\\!\left({\mathcal{G}},\kappa\right)$ |  the set of contexts $C$ such that $N\longrightarrow^{*}C[N_{1},\ldots,N_{k}]$ where $\kappa=N_{1}\cdots N_{k}{\Rightarrow}N$ | Section 2.2
${\mathcal{L}}_{n}\\!\left({\mathcal{G}},\kappa\right)$ |  Like ${\mathcal{L}}\\!\left({\mathcal{G}},\kappa\right)$, but the context size is restricted to $n$ | Section 2.2

notation | explanation | introduced at:
---|---|---
${\mathcal{L}}\\!\left({\mathcal{G}}\right)$ |  the set of trees generated from some nonterminals | Section 2.2
${\mathcal{L}}_{n}\\!\left({\mathcal{G}}\right)$ |  Like ${\mathcal{L}}_{n}\\!\left({\mathcal{G}}\right)$, but the tree size is restricted to $n$ | Section 2.2
${\mathcal{S}}({\mathcal{G}})$ |  the set of linear contexts generated from some nonterminals | Section 2.2
${\mathcal{S}}_{n}({\mathcal{G}})$ |  Like ${\mathcal{S}}_{n}({\mathcal{G}})$, but the size is restricted to $n$ | Section 2.2
${\mathcal{U}}({\mathcal{G}})$ |  the set of affine contexts generated from some nonterminals | Section 2.2
${\mathcal{U}}_{n}({\mathcal{G}})$ |  Like ${\mathcal{U}}_{n}({\mathcal{G}})$, but the size is restricted to $n$ | Section 2.2
$E$ | a second-order context | Section 3.2
$\mathtt{shn}(E)$ | the number of second-order holes of $E$ | Section 3.2
$P$ | a sequences of affine contexts | Section 3.2
$\\#\\!\left(P\right)$ | the length of the sequence $P$ of affine contexts | Section 3.2
$r$ | the largest arity of symbols in $\Sigma$ | Section 3.2.2
$\Phi_{m}^{\bullet}$ |  grammar-independent decomposition function | Section 3.2.2
$\Phi_{m}$ | an auxiliary decomposition function | Section 3.2.2
$\mathcal{E}_{n}^{m}$ |  the set of second-order contexts obtained by decomposing trees of size $n$ | Section 3.2.4
$\mathcal{U}^{m}_{\llbracket\,\rrbracket_{k}^{n}}$ |  the set of affine contexts that match the hole $\llbracket\,\rrbracket_{k}^{n}$ | Section 3.2.4
$\mathcal{P}_{E}^{m}$ |  the set of sequence $P$ of affine contexts that match the second-order context $E$ | Section 3.2.4
$\widetilde{E}$ | a typed second order context | Section 3.4
$\llbracket\,\rrbracket_{\kappa}^{n}$ | a second-order hole | Section 3.4
$\mathtt{shn}(\widetilde{E})$ | the number of second-order holes in $\widetilde{E}$ | Section 3.4
$\widetilde{E}{\centerdot}i$ | the $i$-th second-order hole of $\widetilde{E}$ | Section 3.4
$\widetilde{\Phi}_{m}^{\bullet,{\mathcal{G}}}$ | grammar-respecting decomposition function for trees | Section 3.4.2
$\widetilde{\mathcal{E}}_{n}^{m}({\mathcal{G}},N)$ | typed-version of $\mathcal{E}_{n}^{m}$ | Section 3.4.3
$\widetilde{\mathcal{U}}^{m}_{\llbracket\,\rrbracket_{\kappa}^{n}}({\mathcal{G}})$ | typed-version of $\mathcal{U}^{m}_{\llbracket\,\rrbracket_{k}^{n}}$ | Section 3.4.3
$\widetilde{\mathcal{P}}_{\widetilde{E}}^{m}({\mathcal{G}},N)$ | typed-version of $\mathcal{P}_{E}^{m}$ | Section 3.4.3
$\Sigma{(\delta,\iota,\xi)}$ | the set of terminals of the grammar for $\lambda$-terms | Section 4.1
${\mathcal{N}}{(\delta,\iota,\xi)}$ | the set of nonterminals of the grammar for $\lambda$-terms | Section 4.1
${\mathcal{R}}{(\delta,\iota,\xi)}$ | the set of rules of the grammar for $\lambda$-terms | Section 4.1
$\mathit{Expl}_{m}^{k}$ | an explosive term | Section 4.3

##  Appendix B Proof of Canonical Form Lemma

This section proves Lemma 25 in Section 3.3. We describe the required
transformation as the composite of two transformations. In the first step, we
transform a grammar to _semi-canonical_ one: [Semi-Canonical Grammar] A
rewriting rule is in _semi-canonical form_ if it is in canonical form or of
the form

$N\longrightarrow_{\mathcal{G}}N^{\prime}.$

A grammar ${\mathcal{G}}=(\Sigma,{\mathcal{N}},{\mathcal{R}})$ is _semi-
canonical_ if every rewriting rule is in semi-canonical form.

Lemma 25 will be shown by the next two lemmas.

######  Lemma 51.

Let ${\mathcal{G}}=(\Sigma,{\mathcal{N}},{\mathcal{R}})$ be a regular tree
grammar that is unambiguous and essentially strongly-connected. Then one can
(effectively) construct a grammar
${\mathcal{G}}^{\prime}=(\Sigma,{\mathcal{N}}^{\prime},{\mathcal{R}}^{\prime})$
with ${\mathcal{N}}\subseteq{\mathcal{N}}^{\prime}$ that satisfies the
following conditions:

  * •

${\mathcal{G}}^{\prime}$ is semi-canonical, unambiguous and essentially
strongly-connected.

  * •

${\mathcal{L}}\\!\left({\mathcal{G}},N\right)={\mathcal{L}}\\!\left({\mathcal{G}}^{\prime},N\right)$
for every $N\in{\mathcal{N}}$.

  * •

${\mathcal{S}}^{\mathrm{inf}}({\mathcal{G}})\subseteq{\mathcal{S}}^{\mathrm{inf}}({\mathcal{G}}^{\prime})$.

######  Proof B.1.

Let ${\mathcal{G}}=(\Sigma,{\mathcal{N}},{\mathcal{R}})$ be a grammar that
satisfies the assumption. We can assume without loss of generality that
${\mathcal{L}}\\!\left({\mathcal{G}},N_{0}\right)\neq\emptyset$ for every
$N_{0}\in{\mathcal{N}}$.

Assume ${\mathcal{G}}$ has a rule of the form

$N^{\prime}\longrightarrow
a(T_{1},\dots,T_{n})\qquad\mbox{($T_{1},\dots,T_{n}$ are
$(\Sigma\cup{\mathcal{N}})$-trees)}$

such that $T_{i}\notin{\mathcal{N}}$ for some $i$. (If ${\mathcal{G}}$ does
not have a rule of this form, then ${\mathcal{G}}$ is already semi-canonical.)
Let $N^{\prime\prime}$ be a fresh nonterminal not in ${\mathcal{N}}$. Consider
the grammar
${\mathcal{G}}^{\prime\prime}=(\Sigma,{\mathcal{N}}\cup\\{N^{\prime\prime}\\},{\mathcal{R}}^{\prime\prime})$
where

$\displaystyle{\mathcal{R}}^{\prime\prime}=({\mathcal{R}}\;\setminus$
$\displaystyle\;\\{\;N^{\prime}\longrightarrow a(T_{1},\dots,T_{n})\;\\})$
$\displaystyle\cup$ $\displaystyle\;\\{\;N^{\prime}\longrightarrow
a(T_{1},\dots,T_{i-1},N^{\prime\prime},T_{i+1},\dots,T_{n}),\quad
N^{\prime\prime}\longrightarrow T_{i}\;\\}.$

Then we can show the following claim by induction on the length of rewriting
sequences.

> Claim For every $N\in{\mathcal{N}}$ and $(\Sigma\cup{\mathcal{N}})$-tree
> $T$,
>
>   * •
>
> $N\longrightarrow_{{\mathcal{G}}}^{*}T$ if and only if
> $N\longrightarrow_{{\mathcal{G}}^{\prime\prime}}^{*}T$, and
>
>   * •
>
> $N\longrightarrow_{{\mathcal{G}},\ell}^{*}T$ if and only if
> $N\longrightarrow_{{\mathcal{G}}^{\prime\prime},\ell}^{*}T$.
>
>

This claim implies that ${\mathcal{G}}^{\prime\prime}$ is unambiguous and
${\mathcal{L}}\\!\left({\mathcal{G}},N\right)={\mathcal{L}}\\!\left({\mathcal{G}}^{\prime\prime},N\right)$
for every $N\in{\mathcal{N}}$.

We show that ${\mathcal{G}}^{\prime\prime}$ is essentially strongly-connected.
Let $N_{1},N_{2}\in{\mathcal{N}}\cup\\{N^{\prime\prime}\\}$ and assume
$\\#\\!\left({\mathcal{L}}\\!\left({\mathcal{G}}^{\prime\prime},N_{1}\right)\right)=\\#\\!\left({\mathcal{L}}\\!\left({\mathcal{G}}^{\prime\prime},N_{2}\right)\right)=\infty$.
We should show that $N_{2}$ is reachable from $N_{1}$. We can assume without
loss of generality that $N_{1}\neq N^{\prime\prime}$ and $N_{2}\neq
N^{\prime\prime}$ by the following argument:

  * •

If $N_{1}=N^{\prime\prime}$, then $T_{i}$ must contain a nonterminal
$N_{1}^{\prime}\in{\mathcal{N}}$ with
$\\#\\!\left({\mathcal{L}}\\!\left({\mathcal{G}}^{\prime\prime},N_{1}^{\prime}\right)\right)=\infty$.
Since $N^{\prime\prime}\longrightarrow_{{\mathcal{G}}^{\prime\prime}}T_{i}$ is
the unique rule for $N^{\prime\prime}$ and
$\\#\\!\left({\mathcal{L}}\\!\left({\mathcal{G}}^{\prime\prime},N^{\prime\prime}\right)\right)=\infty$,
we have ${\mathcal{L}}\\!\left({\mathcal{G}},N_{0}\right)\neq\emptyset$ for
each nonterminal $N_{0}$ appearing in $T_{i}$. Hence
$N^{\prime\prime}\longrightarrow_{{\mathcal{G}}^{\prime\prime}}T_{i}\longrightarrow_{{\mathcal{G}}^{\prime\prime}}^{*}S[N_{1}^{\prime}]$
for some linear context $S$ over $\Sigma$ by rewriting each occurrence of a
nonterminal $N_{0}$ in $T_{i}$ (except for one occurrence of $N_{1}^{\prime}$)
with an element of
${\mathcal{L}}\\!\left({\mathcal{G}}^{\prime\prime},N_{0}\right)$. So
$N_{1}^{\prime}$ is reachable from $N^{\prime\prime}$ in
${\mathcal{G}}^{\prime\prime}$. Since the reachability relation is transitive,
it suffices to show that $N_{2}$ is reachable from
$N_{1}^{\prime}\in{\mathcal{N}}$, which satisfies
$\\#\\!\left({\mathcal{L}}\\!\left({\mathcal{G}}^{\prime\prime},N_{1}^{\prime}\right)\right)=\infty$.

  * •

If $N_{2}=N^{\prime\prime}$, then
${\mathcal{L}}\\!\left({\mathcal{G}}^{\prime\prime},N^{\prime}\right)$ is
infinite and $N^{\prime\prime}$ is reachable from $N^{\prime}$. (Here we use
the assumption that
${\mathcal{L}}\\!\left({\mathcal{G}},N_{0}\right)\neq\emptyset$ for every
$N_{0}\in{\mathcal{N}}$.) Hence it suffices to show that $N^{\prime}$ is
reachable from $N_{1}$.

Since
${\mathcal{L}}\\!\left({\mathcal{G}}^{\prime\prime},N_{i}\right)={\mathcal{L}}\\!\left({\mathcal{G}},N_{i}\right)$
($i=1,2$), both ${\mathcal{L}}\\!\left({\mathcal{G}},N_{1}\right)$ and
${\mathcal{L}}\\!\left({\mathcal{G}},N_{2}\right)$ are infinite. Since
${\mathcal{G}}$ is essentially strongly-connected, there exists a $1$-context
$S$ such that $N_{1}\longrightarrow_{{\mathcal{G}}}^{*}S[N_{2}]$. Since
$S[N_{2}]$ is a $(\Sigma\cup{\mathcal{N}})$-tree, by the above claim,
$N_{1}\longrightarrow_{{\mathcal{G}}^{\prime\prime}}^{*}S[N_{2}]$ and thus
$N_{2}$ is reachable from $N_{1}$ in ${\mathcal{G}}^{\prime\prime}$.

We show that
${\mathcal{S}}^{\mathrm{inf}}({\mathcal{G}})\subseteq{\mathcal{S}}^{\mathrm{inf}}({\mathcal{G}}^{\prime\prime})$.
Suppose that
$S\in{\mathcal{L}}\\!\left({\mathcal{G}},N{\Rightarrow}N^{\prime}\right)$ with
$\\#\\!\left({\mathcal{L}}\\!\left({\mathcal{G}},N\right)\right)=\\#\\!\left({\mathcal{L}}\\!\left({\mathcal{G}},N^{\prime}\right)\right)=\infty$.
By definition, $N^{\prime}\longrightarrow_{{\mathcal{G}}}^{*}S[N]$. By the
above claim,
$N^{\prime}\longrightarrow_{{\mathcal{G}}^{\prime\prime}}^{*}S[N]$. Hence
$S\in{\mathcal{L}}\\!\left({\mathcal{G}}^{\prime\prime},N{\Rightarrow}N^{\prime}\right)$.
Since
${\mathcal{L}}\\!\left({\mathcal{G}},N\right)={\mathcal{L}}\\!\left({\mathcal{G}}^{\prime\prime},N\right)$
and
${\mathcal{L}}\\!\left({\mathcal{G}},N^{\prime}\right)={\mathcal{L}}\\!\left({\mathcal{G}}^{\prime\prime},N^{\prime}\right)$,
we have
$\\#\\!\left({\mathcal{L}}\\!\left({\mathcal{G}}^{\prime\prime},N\right)\right)=\\#\\!\left({\mathcal{L}}\\!\left({\mathcal{G}}^{\prime\prime},N^{\prime}\right)\right)=\infty$.

By applying the above transformation as much as needed, we obtain a grammar
that satisfies the requirements. What remains is to show the termination of
the iterated application of the above transformation. A termination measure
can be given as follows: the measure of a rule $N\longrightarrow
C[N_{1},\dots,N_{k}]$ is defined as $\max(|C|-1,0)$ and the measure of a
grammar is the sum of the measures of rules. The measure is by definition a
non-negative integer and decreases by $1$ by the above transformation.

######  Lemma 52.

Let ${\mathcal{G}}=(\Sigma,{\mathcal{N}},{\mathcal{R}})$ be a regular tree
grammar that is semi-canonical, unambiguous and essentially strongly-
connected. Then one can (effectively) construct a grammar
${\mathcal{G}}^{\prime}=(\Sigma,{\mathcal{N}}^{\prime},{\mathcal{R}}^{\prime})$
and a family $(\mathcal{I}_{N})_{N\in{\mathcal{N}}}$ of subsets
$\mathcal{I}_{N}\subseteq{\mathcal{N}}^{\prime}$ that satisfy the following
conditions:

  * •

${\mathcal{G}}^{\prime}$ is canonical, unambiguous and essentially strongly-
connected.

  * •

${\mathcal{L}}\\!\left({\mathcal{G}},N\right)=\biguplus_{N^{\prime}\in\mathcal{I}_{N}}{\mathcal{L}}\\!\left({\mathcal{G}}^{\prime},N^{\prime}\right)$
for every $N\in{\mathcal{N}}$.

  * •

${\mathcal{S}}^{\mathrm{inf}}({\mathcal{G}})\subseteq{\mathcal{S}}^{\mathrm{inf}}({\mathcal{G}}^{\prime})$.

######  Proof B.2.

Let ${\mathcal{G}}=(\Sigma,{\mathcal{N}},{\mathcal{R}})$ be a grammar that
satisfies the assumption. Let ${\mathcal{N}}^{\prime}$ be the subset of
${\mathcal{N}}$ defined by

$N_{0}\in{\mathcal{N}}^{\prime}\;\Leftrightarrow\;(N_{0}\longrightarrow
a(N_{1},\dots,N_{\Sigma(a)}))\in{\mathcal{R}}\;\;\mbox{for some
$a,N_{1},\dots,N_{\Sigma(a)}$}.$

The rewriting rule ${\mathcal{R}}^{\prime}$ is defined by

$\displaystyle{\mathcal{R}}^{\prime}:=\\{N_{0}\longrightarrow
a(N_{1}^{\prime},\dots,N_{\Sigma(a)}^{\prime})\mid~{}$ $\displaystyle
N_{0},N^{\prime}_{1},\dots,N^{\prime}_{\Sigma(a)}\in{\mathcal{N}}^{\prime},$
$\displaystyle
N_{0}\longrightarrow_{{\mathcal{G}}}a(N_{1},\dots,N_{\Sigma(a)})\longrightarrow_{{\mathcal{G}}}^{*}a(N^{\prime}_{1},\dots,N^{\prime}_{\Sigma(a)})\\}.$

In other words, $N_{0}\longrightarrow
a(N_{1}^{\prime},\dots,N_{\Sigma(a)}^{\prime})$ is in ${\mathcal{R}}^{\prime}$
if and only if there exists a rule $N_{0}\longrightarrow
a(N_{1},\dots,N_{\Sigma(a)})$ in ${\mathcal{R}}$ with
$N_{i}\longrightarrow_{{\mathcal{G}}}^{*}N^{\prime}_{i}$ for each
$i=1,\dots,\Sigma(a)$. Given a nonterminal $N\in{\mathcal{N}}$, let
$\mathcal{I}_{N}\subseteq{\mathcal{N}}^{\prime}$ be the subset given by

$\mathcal{I}_{N}\triangleq\\{N^{\prime}\in{\mathcal{N}}^{\prime}\mid
N\longrightarrow_{\mathcal{G}}^{*}N^{\prime}\\}.$

We show that the grammar
${\mathcal{G}}^{\prime}\triangleq(\Sigma,{\mathcal{N}}^{\prime},{\mathcal{R}}^{\prime})$
together with $(\mathcal{I}_{N})_{N\in{\mathcal{N}}}$ satisfies the
requirement.

We can prove the following claims by induction on the length of rewriting
sequences:

  1. (1)

For $N\in{\mathcal{N}}$ and
$T\in{\mathcal{T}}(\Sigma\cup{\mathcal{N}}^{\prime})$, if
$N\longrightarrow_{{\mathcal{G}}}^{*}T$, then
$N^{\prime}\longrightarrow_{{\mathcal{G}}^{\prime}}^{*}T$ for some
$N^{\prime}\in\mathcal{I}_{N}$.

  2. (2)

For $N^{\prime}\in{\mathcal{N}}^{\prime}$ and
$T\in{\mathcal{T}}(\Sigma\cup{\mathcal{N}}^{\prime})$, if
$N^{\prime}\longrightarrow_{{\mathcal{G}}^{\prime}}^{*}T$, then
$N^{\prime}\longrightarrow_{{\mathcal{G}}}^{*}T$.

We show that
${\mathcal{L}}\\!\left({\mathcal{G}},N\right)=\bigcup_{N^{\prime}\in\mathcal{I}_{N}}{\mathcal{L}}\\!\left({\mathcal{G}}^{\prime},N^{\prime}\right)$.
The above $(1)$ shows that
${\mathcal{L}}\\!\left({\mathcal{G}},N\right)\subseteq\bigcup_{N^{\prime}\in\mathcal{I}_{N}}{\mathcal{L}}\\!\left({\mathcal{G}}^{\prime},N^{\prime}\right)$.
The above $(2)$ shows that
${\mathcal{L}}\\!\left({\mathcal{G}}^{\prime},N^{\prime}\right)\subseteq{\mathcal{L}}\\!\left({\mathcal{G}},N^{\prime}\right)$
for every $N^{\prime}\in\mathcal{I}_{N}$. By definition of $\mathcal{I}_{N}$,
we have $N\longrightarrow_{{\mathcal{G}}}^{*}N^{\prime}$ and thus
${\mathcal{L}}\\!\left({\mathcal{G}},N^{\prime}\right)\subseteq{\mathcal{L}}\\!\left({\mathcal{G}},N\right)$
for every $N^{\prime}\in\mathcal{I}_{N}$. So
$\bigcup_{N^{\prime}\in\mathcal{I}_{N}}{\mathcal{L}}\\!\left({\mathcal{G}}^{\prime},N^{\prime}\right)\subseteq{\mathcal{L}}\\!\left({\mathcal{G}},N\right)$.

We prove by contraposition that, for $N_{1},N_{2}\in\mathcal{I}_{N}$, if
$N_{1}\neq N_{2}$, then
${\mathcal{L}}\\!\left({\mathcal{G}}^{\prime},N_{1}\right)\cap{\mathcal{L}}\\!\left({\mathcal{G}}^{\prime},N_{2}\right)=\emptyset$.
Suppose that
$T\in{\mathcal{L}}\\!\left({\mathcal{G}}^{\prime},N_{1}\right)\cap{\mathcal{L}}\\!\left({\mathcal{G}}^{\prime},N_{2}\right)$.
Then we have

$N_{i}\longrightarrow_{{\mathcal{G}}^{\prime}}a(N^{\prime}_{i,1},\dots,N^{\prime}_{i,\Sigma(a)})\longrightarrow_{{\mathcal{G}}^{\prime}}^{*}T\qquad(i=1,2)$

for some $N^{\prime}_{i,j}\in{\mathcal{N}}^{\prime}$. By the definition of
${\mathcal{R}}^{\prime}$, we have

$N_{i}\longrightarrow_{{\mathcal{G}}}a(N_{i,1},\dots,N_{i,\Sigma(a)})\longrightarrow_{{\mathcal{G}}}^{*}a(N^{\prime}_{i,1},\dots,N^{\prime}_{i,\Sigma(a)})\longrightarrow_{{\mathcal{G}}^{\prime}}^{*}T\qquad(i=1,2).$

Because $N_{i}\in\mathcal{I}_{N}$, we have
$N\longrightarrow_{{\mathcal{G}}}^{*}N_{i}$, for $i=1,2$. By the claim $(2)$,
we have

$N\longrightarrow_{{\mathcal{G}}}^{*}N_{i}\longrightarrow_{{\mathcal{G}}}a(N_{i,1},\dots,N_{i,\Sigma(a)})\longrightarrow_{{\mathcal{G}}}^{*}a(N^{\prime}_{i,1},\dots,N^{\prime}_{i,\Sigma(a)})\longrightarrow_{{\mathcal{G}}}^{*}T\qquad(i=1,2).$

The above two rewriting sequences of ${\mathcal{G}}$ induce the following two
leftmost rewriting sequences:

$N\longrightarrow_{{\mathcal{G}},\ell}^{*}N_{i}\longrightarrow_{{\mathcal{G}},\ell}a(N_{i,1},\dots,N_{i,\Sigma(a)})\longrightarrow_{{\mathcal{G}},\ell}^{*}T\qquad(i=1,2),$

which are the same by the unambiguity of ${\mathcal{G}}$. Then the length of
the sequence $N\longrightarrow_{{\mathcal{G}},\ell}^{*}N_{1}$ and that of
$N\longrightarrow_{{\mathcal{G}},\ell}^{*}N_{2}$ are the same since just after
them the root terminal $a$ occurs, and hence $N_{1}=N_{2}$, as required. Next
we prove the unambiguity of ${\mathcal{G}}^{\prime}$, by contradiction: we
assume that ${\mathcal{G}}^{\prime}$ is not unambiguous, and show that
${\mathcal{G}}$ is not unambiguous, which is a contradiction. Let
$N_{0}^{\prime}\in{\mathcal{N}}^{\prime}$ and $T\in{\mathcal{T}}(\Sigma)$ be a
pair of a nonterminal and a tree such that there exist two leftmost rewriting
sequences from $N_{0}^{\prime}$ to $T$ in ${\mathcal{G}}^{\prime}$. We can
assume without loss of generality that the leftmost rewriting sequences differ
on the first step. Assume that the two rewriting sequences are

$N_{0}^{\prime}\longrightarrow_{{\mathcal{G}}^{\prime},\ell}a(N_{1,1}^{\prime},\dots,N_{1,\Sigma(a)}^{\prime})\longrightarrow_{{\mathcal{G}}^{\prime},\ell}^{*}a(T_{1},\dots,T_{\Sigma(a)})=T$

and

$N_{0}^{\prime}\longrightarrow_{{\mathcal{G}}^{\prime},\ell}a(N_{2,1}^{\prime},\dots,N_{2,\Sigma(a)}^{\prime})\longrightarrow_{{\mathcal{G}}^{\prime},\ell}^{*}a(T_{1},\dots,T_{\Sigma(a)})=T.$

We have $N_{1,j}^{\prime}\neq N_{2,j}^{\prime}$ for some $j$. By the
definition of ${\mathcal{R}}^{\prime}$, there are rules

$N_{0}^{\prime}\longrightarrow_{{\mathcal{G}}}a(N_{1,1},\dots,N_{1,\Sigma(a)})\qquad\mbox{and}\qquad
N_{0}^{\prime}\longrightarrow_{{\mathcal{G}}}a(N_{2,1},\dots,N_{2,\Sigma(a)})$

with $N_{i,j}\longrightarrow_{{\mathcal{G}}}^{*}N_{i,j}^{\prime}$ for every
$(i,j)\in\\{1,2\\}\times\\{1,\dots,\Sigma(a)\\}$. There are two cases:

  * •

Case $N_{1,j}\neq N_{2,j}$ for some $j\in\\{1,\dots,\Sigma(a)\\}$: By the
rewriting sequences above and the claim $(2)$, we have two sequences

$N_{0}^{\prime}\longrightarrow_{{\mathcal{G}}}a(N_{i,1},\dots,N_{i,\Sigma(a)})\longrightarrow_{{\mathcal{G}}}^{*}a(N_{i,1}^{\prime},\dots,N_{i,\Sigma(a)}^{\prime})\longrightarrow_{{\mathcal{G}}}^{*}a(T_{1},\dots,T_{\Sigma(a)})$

for $i=1,2$. The corresponding leftmost rewriting sequences differ at the
first step. So ${\mathcal{G}}$ is unambiguous.

  * •

Case $N_{1,j}=N_{2,j}$ for every $j\in\\{1,\dots,\Sigma(a)\\}$: Let $j$ be an
index such that $N_{1,j}^{\prime}\neq N_{2,j}^{\prime}$ and $N_{j}\triangleq
N_{1,j}=N_{2,j}$. Then
$N_{j}\longrightarrow_{{\mathcal{G}}}^{*}N_{1,j}^{\prime}\longrightarrow_{{\mathcal{G}}^{\prime}}^{*}T_{j}$
and
$N_{j}\longrightarrow_{{\mathcal{G}}}^{*}N_{2,j}^{\prime}\longrightarrow_{{\mathcal{G}}^{\prime}}^{*}T_{j}$.
By the definition of ${\mathcal{R}}^{\prime}$ and the claim $(2)$, we have

$N_{j}\longrightarrow_{{\mathcal{G}}}^{*}N_{i,j}^{\prime}\longrightarrow_{{\mathcal{G}}}b(N_{i,1}^{\prime\prime},\dots,N_{i,\Sigma(b)}^{\prime\prime})\longrightarrow_{{\mathcal{G}}}^{*}T_{j}\qquad(i=1,2)$

with $N_{1,j}^{\prime}\neq N_{2,j}^{\prime}$. Hence ${\mathcal{G}}$ is not
unambiguous.

We show that ${\mathcal{G}}^{\prime}$ is essentially strongly-connected. Let
$N_{1},N_{2}\in{\mathcal{N}}^{\prime}$ such that
$\\#\\!\left({\mathcal{L}}\\!\left({\mathcal{G}}^{\prime},N_{1}\right)\right)=\\#\\!\left({\mathcal{L}}\\!\left({\mathcal{G}}^{\prime},N_{2}\right)\right)=\infty$.
We show that $N_{2}$ is reachable from $N_{1}$ in ${\mathcal{G}}^{\prime}$. By
the claim $(2)$,
${\mathcal{L}}\\!\left({\mathcal{G}},N_{2}\right)\supseteq{\mathcal{L}}\\!\left({\mathcal{G}}^{\prime},N_{2}\right)$
is infinite. Since ${\mathcal{L}}\\!\left({\mathcal{G}}^{\prime},N_{1}\right)$
is infinite, we have a rule

$N_{1}\longrightarrow_{{\mathcal{G}}^{\prime}}a(N_{1,1},\dots,N_{1,\Sigma(a)})$

in ${\mathcal{R}}^{\prime}$ such that
${\mathcal{L}}\\!\left({\mathcal{G}}^{\prime},N_{1,i}\right)$ is infinite for
some $i$ and
${\mathcal{L}}\\!\left({\mathcal{G}}^{\prime},N_{1,j}\right)\neq\emptyset$ for
every $j=1,\dots,\Sigma(a)$. Again, by the claim $(2)$,
${\mathcal{L}}\\!\left({\mathcal{G}},N_{1,i}\right)\supseteq{\mathcal{L}}\\!\left({\mathcal{G}}^{\prime},N_{1,i}\right)$
is infinite. Since ${\mathcal{G}}$ is essentially strongly-connected, there
exists a linear context $S$ such that
$N_{1,i}\longrightarrow_{{\mathcal{G}}}^{*}S[N_{2}]$. By the claim $(1)$,
there exists $N_{1,i}^{\prime}\in\mathcal{I}_{N_{1,i}}$ such that
$N_{1,i}^{\prime}\longrightarrow_{{\mathcal{G}}^{\prime}}^{*}S[N_{2}]$. Since
$N^{\prime}_{1,i}\in\mathcal{I}_{N_{1,i}}$, we have
$N_{1,i}\longrightarrow^{*}_{{\mathcal{G}}}N^{\prime}_{1,i}$, and hence by the
definition of ${\mathcal{R}}^{\prime}$, we find that

$N_{1}\longrightarrow_{{\mathcal{G}}^{\prime}}a(N_{1,1},\dots,N_{1,i-1},N_{1,i}^{\prime},N_{1,i+1},\dots,N_{1,\Sigma(a)})$

is in ${\mathcal{R}}^{\prime}$. Let us pick
$T_{1,j}\in{\mathcal{L}}\\!\left({\mathcal{G}}^{\prime},N_{1,j}\right)$ for
each $j\neq i$; then we have:

$\displaystyle N_{1}$
$\displaystyle\longrightarrow_{{\mathcal{G}}^{\prime}}a(N_{1,1},\dots,N_{1,i-1},N_{1,i}^{\prime},N_{1,i+1},\dots,N_{1,\Sigma(a)})$
$\displaystyle\longrightarrow_{{\mathcal{G}}^{\prime}}^{*}a(N_{1,1},\dots,N_{1,i-1},S[N_{2}],N_{1,i+1},\dots,N_{1,\Sigma(a)})$
$\displaystyle\longrightarrow_{{\mathcal{G}}^{\prime}}^{*}a(T_{1,1},\dots,T_{1,i-1},S[N_{2}],T_{1,i+1},\dots,T_{1,\Sigma(a)}).$

Thus $N_{2}$ is reachable from $N_{1}$ in ${\mathcal{G}}^{\prime}$.

Lastly, we show that
${\mathcal{S}}^{\mathrm{inf}}({\mathcal{G}})\subseteq{\mathcal{S}}^{\mathrm{inf}}({\mathcal{G}}^{\prime})$.
Assume that
$S\in{\mathcal{L}}\\!\left({\mathcal{G}},N_{1}{\Rightarrow}N_{2}\right)$ and
$\\#\\!\left({\mathcal{L}}\\!\left({\mathcal{G}},N_{1}\right)\right)=\\#\\!\left({\mathcal{L}}\\!\left({\mathcal{G}},N_{2}\right)\right)=\infty$.
Since
${\mathcal{L}}\\!\left({\mathcal{G}},N_{1}\right)=\bigcup_{N_{1}^{\prime}\in\mathcal{I}_{N_{1}}}{\mathcal{L}}\\!\left({\mathcal{G}}^{\prime},N_{1}^{\prime}\right)$,
there exists $N_{1}^{\prime}\in\mathcal{I}_{N_{1}}$ such that
$\\#\\!\left({\mathcal{L}}\\!\left({\mathcal{G}}^{\prime},N_{1}^{\prime}\right)\right)=\infty$.
Since $N_{2}\longrightarrow_{{\mathcal{G}}}^{*}S[N_{1}]$ and
$N_{1}\longrightarrow_{{\mathcal{G}}}^{*}N_{1}^{\prime}$, we have
$N_{2}\longrightarrow_{{\mathcal{G}}}^{*}S[N_{1}^{\prime}]$. By the claim
$(1)$, there exists $N_{2}^{\prime}\in\mathcal{I}_{N_{2}}$ such that
$N_{2}^{\prime}\longrightarrow_{{\mathcal{G}}^{\prime}}^{*}S[N_{1}^{\prime}]$.
Hence
$S\in{\mathcal{L}}\\!\left({\mathcal{G}}^{\prime},N_{1}^{\prime}{\Rightarrow}N_{2}^{\prime}\right)$.
Since
$\\#\\!\left({\mathcal{L}}\\!\left({\mathcal{G}}^{\prime},N_{1}^{\prime}\right)\right)=\infty$,
we have
$\\#\\!\left({\mathcal{L}}\\!\left({\mathcal{G}}^{\prime},N_{2}^{\prime}\right)\right)=\infty$
as well.

######  Proof B.3 (Proof of Lemma 25).

Let ${\mathcal{G}}$ be a regular tree grammar that is unambiguous and strongly
connected. Then ${\mathcal{G}}$ is essentially strongly-connected. So by
applying Lemmas 51 and 52, we obtain a grammar ${\mathcal{G}}^{\prime}$ and a
family $(\mathcal{I}_{N})_{N\in{\mathcal{N}}}$ that satisfy the following
conditions:

  * •

${\mathcal{G}}^{\prime}$ is canonical, unambiguous and essentially strongly-
connected.

  * •

${\mathcal{L}}\\!\left({\mathcal{G}},N\right)=\biguplus_{N^{\prime}\in\mathcal{I}_{N}}{\mathcal{L}}\\!\left({\mathcal{G}}^{\prime},N^{\prime}\right)$
for every $N\in{\mathcal{N}}$.

  * •

${\mathcal{S}}^{\mathrm{inf}}({\mathcal{G}})\subseteq{\mathcal{S}}^{\mathrm{inf}}({\mathcal{G}}^{\prime})$.

The grammar ${\mathcal{G}}^{\prime}$ and a family
$(\mathcal{I}_{N})_{N\in{\mathcal{N}}}$ satisfy the first and second
requirements of Lemma 25. We show that
$\\#\\!\left({\mathcal{L}}\\!\left({\mathcal{G}}\right)\right)=\infty$ implies
${\mathcal{S}}({\mathcal{G}})\subseteq{\mathcal{S}}^{\mathrm{inf}}({\mathcal{G}}^{\prime})$.

Suppose that
$\\#\\!\left({\mathcal{L}}\\!\left({\mathcal{G}}\right)\right)=\infty$. Since
${\mathcal{L}}\\!\left({\mathcal{G}}\right)=\bigcup_{N\in{\mathcal{N}}}{\mathcal{L}}\\!\left({\mathcal{G}},N\right)$
and ${\mathcal{N}}$ is finite, there exists $N_{0}\in{\mathcal{N}}$ such that
$\\#\\!\left({\mathcal{L}}\\!\left({\mathcal{G}},N_{0}\right)\right)=\infty$.
By strong connectivity of ${\mathcal{G}}$, we have
$\\#\\!\left({\mathcal{L}}\\!\left({\mathcal{G}},N\right)\right)=\infty$ for
every $N\in{\mathcal{N}}$. Hence
${{\mathcal{N}}}^{\mathrm{inf}}={\mathcal{N}}$, and thus
${\mathcal{S}}({\mathcal{G}})={\mathcal{S}}^{\mathrm{inf}}({\mathcal{G}})$. We
have
${\mathcal{S}}({\mathcal{G}})={\mathcal{S}}^{\mathrm{inf}}({\mathcal{G}})\subseteq{\mathcal{S}}^{\mathrm{inf}}({\mathcal{G}}^{\prime})$
as required.

##  Appendix C Proof of Lemma 37

We start from the formal definition of periodicity and its basic properties.
[period, basic period] Let $X\subseteq{\rm Nature}$ be a subset of natural
numbers. We say $X$ is _periodic_ with _period $c$_ ($c\in{\rm
Nature}\backslash\\{0\\}$) if

$\exists n_{0}\in{\rm Nature}.\;\forall n\geq n_{0}.\;\forall k\in{\rm
Nature}.\quad n\in X\Leftrightarrow(n+ck)\in X.$

If $X$ is periodic, we call the minimum period the _basic period_.

Let ${\mathcal{G}}$ be a regular tree grammar and $\kappa=(N_{1}\dots
N_{k}{\Rightarrow}N)$ be a context type of ${\mathcal{G}}$. We say $\kappa$ is
_periodic with period $c$_ if so is the subset of natural numbers

$\\{n\in{\rm
Nature}\mid{\mathcal{L}}_{n}\\!\left({\mathcal{G}},\kappa\right)\neq\emptyset\\},$

and call the minimum period the _basic period_.

######  Lemma 53.

Let $X\subseteq{\rm Nature}$ be a subset of natural numbers and $c\in{\rm
Nature}\backslash\\{0\\}$.

  1. (1)

Suppose that

$\exists n_{0}\in{\rm Nature}.\;\forall n\geq n_{0}.\quad n\in X\Rightarrow
n+c\in X.$

Then $X$ is periodic with period $c$.

  2. (2)

Suppose that

$\exists n_{0}\in{\rm Nature}.\;\exists k_{0}\in{\rm Nature}.\;\forall n\geq
n_{0}.\;\forall k\geq k_{0}.\quad n\in X\Rightarrow n+ck\in X.$

Then $X$ is periodic with period $c$.

  3. (3)

Suppose that $c$ and $c^{\prime}$ are periods of $X$. Then
$\gcd(c,c^{\prime})$ is also a period of $X$, where $\gcd(c,c^{\prime})$ is
the greatest common divisor.

######  Proof C.1.

(1) Let $n_{0}\in{\rm Nature}$ be a witness of the assumption. Then for every
$n\geq n_{0}$ and $k\geq 0$, we have $n\in X\Rightarrow(n+ck)\in X$, by
induction on $k$. Let $Y\subseteq{\rm Nature}$ be the set of counterexamples
of $n+c\in X\Rightarrow n\in X$, namely,

$Y\triangleq\\{n\in{\rm Nature}\mid n+c\in X\;\wedge\;n\notin X\\}.$

Then $Y$ has at most $n_{0}+c$ elements because, for every $n\geq n_{0}$ and
$k\geq 1$,

$n\in Y\quad\Rightarrow\quad n+c\in X\quad\Rightarrow\quad n+ck\in
X\quad\Rightarrow\quad n+ck\notin Y.$

Let $n_{0}^{\prime}\geq n_{0}$ be a natural number that is (strictly) greater
than all elements of $Y$. Then for every $n\geq n_{0}^{\prime}$,

$n\in X\quad\Leftrightarrow\quad n+c\in X.$

By induction on $k\geq 0$, we conclude that $n\in X\Leftrightarrow n+kd\in X$
for every $n\geq n_{0}^{\prime}$.

(2) Let $n_{0}$ and $k_{0}$ be witnesses of the assumption and $Y\subseteq{\rm
Nature}$ be the set of counterexamples of $n\in X\Rightarrow n+c\in X$, i.e.,

$Y\triangleq\\{n\in{\rm Nature}\mid n\in X\;\wedge\;n+c\notin X\\}.$

Then $Y$ has at most $n_{0}+ck_{0}$ elements because, for every $n\geq n_{0}$
and $k\geq k_{0}$,

$n\in Y\quad\Rightarrow\quad n\in X\quad\Rightarrow\quad n+c(k+1)\in
X\quad\Rightarrow\quad n+ck\notin Y.$

Let $n_{0}^{\prime}$ be a natural number that is (strictly) greater than all
elements of $Y$. Then for every $n\geq n_{0}^{\prime}$,

$n\in X\quad\Rightarrow\quad n+c\in X.$

Hence by item (1), $X$ is periodic with period $c$.

(3) The claim trivially holds if $\gcd(c,c^{\prime})=c$ or $c^{\prime}$. We
assume that $\gcd(c,c^{\prime})<c,c^{\prime}$. Let $d=\gcd(c,c^{\prime})$.
There exist integers $a,b$ such that $ac+bc^{\prime}=d$ (by Bézout’s lemma).
Since $0<d<c,c^{\prime}$, exactly one of $a$ and $b$ is negative. Suppose that
$a>0$ and $b<0$.

Let $n_{0}$ be a constant such that

$\forall n\geq n_{0}.\;\forall k\in{\rm Nature}.\quad n\in
X\Leftrightarrow(n+ck)\in X$

and $n_{0}^{\prime}$ be a constant for a similar condition for $c^{\prime}$.
Let $n_{0}^{\prime\prime}=\max(n_{0},n_{0}^{\prime})-bc^{\prime}$. Then, for
every $n\geq n_{0}^{\prime\prime}$,

$\displaystyle n\in X$ $\displaystyle\quad\Leftrightarrow\quad
n+bc^{\prime}\in X$ (since $n+bc^{\prime}\geq n_{0}^{\prime}$ and $b<0$)
$\displaystyle\quad\Leftrightarrow\quad n+bc^{\prime}+ac\in X$ (since
$n+bc^{\prime}\geq n_{0}$ and $a>0$) $\displaystyle\quad\Leftrightarrow\quad
n+d\in X.$

By induction on $k\geq 0$, we conclude that $n\in X\Leftrightarrow n+kd\in X$
for every $n\geq n_{0}^{\prime\prime}$.

We show that $N{\Rightarrow}N^{\prime}$ is periodic for every
$N,N^{\prime}\in{{\mathcal{N}}}^{\mathrm{inf}}$ and its basic period is
independent of the choice of $N$ and $N^{\prime}$. We call the basic period of
$N{\Rightarrow}N^{\prime}$, which is independent of $N$ and $N^{\prime}$, the
_basic period of the grammar ${\mathcal{G}}$_. Further we show that
$U,U^{\prime}\in{\mathcal{L}}\\!\left({\mathcal{G}},N{\Rightarrow}N^{\prime}\right)$
implies $|U|\equiv|U^{\prime}|\mod c$, where $c$ is the basic period of the
grammar ${\mathcal{G}}$.

######  Lemma 54.

Let ${\mathcal{G}}=(\Sigma,{\mathcal{N}},{\mathcal{R}})$ be a regular tree
grammar. Assume that ${\mathcal{G}}$ is essentially strongly-connected and
$\\#\\!\left({\mathcal{L}}\\!\left({\mathcal{G}}\right)\right)=\infty$.

  1. (1)

${\mathcal{L}}\\!\left({\mathcal{G}},N{\Rightarrow}N^{\prime}\right)$ is
infinite for every $N,N^{\prime}\in{{\mathcal{N}}}^{\mathrm{inf}}$.

  2. (2)

$N{\Rightarrow}N$ is periodic for every $N\in{{\mathcal{N}}}^{\mathrm{inf}}$.

  3. (3)

Let $N\in{{\mathcal{N}}}^{\mathrm{inf}}$ and $c_{N}$ be the basic period of
$N{\Rightarrow}N$. Then
${\mathcal{L}}_{n}\\!\left({\mathcal{G}},N{\Rightarrow}N\right)\neq\emptyset$
implies $n\equiv 0\mod c_{N}$.

  4. (4)

The basic period $c_{N}$ of $N{\Rightarrow}N$ is independent of
$N\in{{\mathcal{N}}}^{\mathrm{inf}}$. Let $c=c_{N}$.

  5. (5)

For every $N,N^{\prime}\in{{\mathcal{N}}}^{\mathrm{inf}}$, if
$U_{1},U_{2}\in{\mathcal{L}}\\!\left({\mathcal{G}},N{\Rightarrow}N^{\prime}\right)$,
then $|U_{1}|\equiv|U_{2}|\mod c$.

  6. (6)

For every $N,N^{\prime}\in{{\mathcal{N}}}^{\mathrm{inf}}$,
$N{\Rightarrow}N^{\prime}$ has the basic period $c$.

######  Proof C.2.

(1) There exist $N_{1},N_{2}\in{{\mathcal{N}}}^{\mathrm{inf}}$ such that
${\mathcal{L}}\\!\left({\mathcal{G}},N_{1}{\Rightarrow}N_{2}\right)$ contains
a context of size greater than $0$, because there exists
$N_{2}\in{\mathcal{N}}$ with
${\mathcal{L}}\\!\left({\mathcal{G}},N_{2}\right)=\infty$ due to
$\\#\\!\left({\mathcal{L}}\\!\left({\mathcal{G}}\right)\right)=\infty$. Let
$U\in{\mathcal{L}}\\!\left({\mathcal{G}},N_{1}{\Rightarrow}N_{2}\right)$ be a
context with $|U|>0$. Let $N\in{{\mathcal{N}}}^{\mathrm{inf}}$. By essential
strong-connectivity there exist
$S_{N}\in{\mathcal{L}}\\!\left({\mathcal{G}},N{\Rightarrow}N_{1}\right)$ and
$S^{\prime}_{N}\in{\mathcal{L}}\\!\left({\mathcal{G}},N_{2}{\Rightarrow}N\right)$,
and then $U_{N}\triangleq
S^{\prime}_{N}[U[S_{N}]]\in{\mathcal{L}}\\!\left({\mathcal{G}},N{\Rightarrow}N\right)$
with $|U_{N}|>0$. Let $U^{n}_{N}$ be the context defined by $U^{0}_{N}=[\,]$
and $U^{n+1}_{N}=U_{N}[U_{N}^{n}]$. Then
$U^{n}_{N}\in{\mathcal{L}}\\!\left({\mathcal{G}},N{\Rightarrow}N\right)$ for
every $n$ and $|U^{n}|\geq n$; hence
${\mathcal{L}}\\!\left({\mathcal{G}},N{\Rightarrow}N\right)$ is an infinite
set. Let $N^{\prime}\in{{\mathcal{N}}}^{\mathrm{inf}}$. By essential strong-
connectivity there exists
$S_{N,N^{\prime}}\in{\mathcal{L}}\\!\left({\mathcal{G}},N{\Rightarrow}N^{\prime}\right)$,
which implies
${\mathcal{L}}\\!\left({\mathcal{G}},N{\Rightarrow}N^{\prime}\right)$ is also
infinite.

(2) Let $N\in{{\mathcal{N}}}^{\mathrm{inf}}$. By (1),
${\mathcal{L}}\\!\left({\mathcal{G}},N{\Rightarrow}N\right)$ is an infinite
set. In particular, there exists
$U_{N}\in{\mathcal{L}}\\!\left({\mathcal{G}},N{\Rightarrow}N\right)$ with
$|U_{N}|>0$. Let $n\in{\rm Nature}$ and assume that
${\mathcal{L}}_{n}\\!\left({\mathcal{G}},N{\Rightarrow}N\right)\neq\emptyset$.
Then $U\in{\mathcal{L}}_{n}\\!\left({\mathcal{G}},N{\Rightarrow}N\right)$ for
some $U$ and thus
$U[U_{N}]\in{\mathcal{L}}_{n+|U_{N}|}\\!\left({\mathcal{G}},N{\Rightarrow}N\right)$.
Therefore
${\mathcal{L}}_{n}\\!\left({\mathcal{G}},N{\Rightarrow}N\right)\neq\emptyset$
implies
${\mathcal{L}}_{n+|U_{N}|}\\!\left({\mathcal{G}},N{\Rightarrow}N\right)\neq\emptyset$.
By applying Lemma 53(1), $N{\Rightarrow}N$ is periodic with period $|U_{N}|$.

(3) Let $N\in{{\mathcal{N}}}^{\mathrm{inf}}$ and $c_{N}$ be the basic period
of $N{\Rightarrow}N$, and suppose that
${\mathcal{L}}_{n}\\!\left({\mathcal{G}},N{\Rightarrow}N\right)\neq\emptyset$.
If $n=0$, then the claim trivially holds. Suppose that $n>0$ and let
$U\in{\mathcal{L}}_{n}\\!\left({\mathcal{G}},N{\Rightarrow}N\right)$. Then by
the argument of the proof of (1), $N{\Rightarrow}N$ has period $|U|=n$. By
Lemma 53(3), $N{\Rightarrow}N$ has period $\gcd(c_{N},n)$, which is smaller
than or equal to $c_{N}$. Since $c_{N}$ is basic, this implies
$c_{N}=\gcd(c_{N},n)$, i.e., $n\equiv 0\mod c_{N}$.

(4) Let $N_{1},N_{2}\in{{\mathcal{N}}}^{\mathrm{inf}}$ and $c_{1}$ and $c_{2}$
be the basic periods of $N_{1}{\Rightarrow}N_{1}$ and of
$N_{2}{\Rightarrow}N_{2}$, respectively. We show that $c_{1}\equiv 0\mod
c_{2}$. By essential strong-connectivity, there exist
$S_{1,2}\in{\mathcal{L}}\\!\left({\mathcal{G}},N_{1}{\Rightarrow}N_{2}\right)$
and
$S_{2,1}\in{\mathcal{L}}\\!\left({\mathcal{G}},N_{2}{\Rightarrow}N_{1}\right)$.
Since ${\mathcal{L}}\\!\left({\mathcal{G}},N_{1}{\Rightarrow}N_{1}\right)$ is
infinite (by (1)) and $N_{1}{\Rightarrow}N_{1}$ has period $c_{1}$, there
exist contexts
$U,U^{\prime}\in{\mathcal{L}}\\!\left({\mathcal{G}},N_{1}{\Rightarrow}N_{1}\right)$
such that $|U^{\prime}|=|U|+c_{1}$. Let $n=|S_{1,2}[U[S_{2,1}]]|$ and
$n^{\prime}=|S_{1,2}[U^{\prime}[S_{2,1}]]|$; then $n^{\prime}=n+c_{1}$. Then
both ${\mathcal{L}}_{n}\\!\left({\mathcal{G}},N_{2}{\Rightarrow}N_{2}\right)$
and
${\mathcal{L}}_{n^{\prime}}\\!\left({\mathcal{G}},N_{2}{\Rightarrow}N_{2}\right)$
are non-empty. Hence $n\equiv 0\mod c_{2}$ and $n^{\prime}\equiv 0\mod c_{2}$
by (3). Therefore $c_{1}\equiv n^{\prime}-n\equiv 0\mod c_{2}$.

(5) Let $N,N^{\prime}\in{{\mathcal{N}}}^{\mathrm{inf}}$ and assume that
$U_{1},U_{2}\in{\mathcal{L}}\\!\left({\mathcal{G}},N{\Rightarrow}N^{\prime}\right)$.
By essential strong-connectivity, there exists
$S\in{\mathcal{L}}\\!\left({\mathcal{G}},N^{\prime}{\Rightarrow}N\right)$.
Then
$S[U_{1}],S[U_{2}]\in{\mathcal{L}}\\!\left({\mathcal{G}},N{\Rightarrow}N\right)$.
By (3),

$|S|+|U_{1}|\equiv|S[U_{1}]|\equiv|S[U_{2}]|\equiv|S|+|U_{2}|\mod c.$

Hence $|U_{1}|\equiv|U_{2}|\mod c$.

(6) Let $N,N^{\prime}\in{{\mathcal{N}}}^{\mathrm{inf}}$. Recall that $c$ is
the basic period of $N{\Rightarrow}N$. Since $c$ is a period of
$N{\Rightarrow}N$ and by (3), there exists $k_{0}\geq 0$ such that, for every
$k\geq k_{0}$, we have
${\mathcal{L}}_{ck}\\!\left({\mathcal{G}},N{\Rightarrow}N\right)\neq\emptyset$.
Let $(U_{k})_{k\geq k_{0}}$ be a family such that
$U_{k}\in{\mathcal{L}}_{ck}\\!\left({\mathcal{G}},N{\Rightarrow}N\right)$. Now
${\mathcal{L}}_{n}\\!\left({\mathcal{G}},N{\Rightarrow}N^{\prime}\right)\neq\emptyset$
implies
${\mathcal{L}}_{n+ck}\\!\left({\mathcal{G}},N{\Rightarrow}N^{\prime}\right)\neq\emptyset$
for every $k\geq k_{0}$, since
$U^{\prime}\in{\mathcal{L}}_{n}\\!\left({\mathcal{G}},N{\Rightarrow}N^{\prime}\right)$
implies
$U^{\prime}[U_{k}]\in{\mathcal{L}}_{n+ck}\\!\left({\mathcal{G}},N{\Rightarrow}N^{\prime}\right)$.
By Lemma 53(2), $N{\Rightarrow}N^{\prime}$ has period $c$.

Conversely assume that $N{\Rightarrow}N^{\prime}$ has period $c^{\prime}$.
Since ${\mathcal{L}}\\!\left({\mathcal{G}},N{\Rightarrow}N^{\prime}\right)$ is
an infinite set by (1), we have
$U_{1},U_{2}\in{\mathcal{L}}\\!\left({\mathcal{G}},N{\Rightarrow}N^{\prime}\right)$
such that $|U_{2}|=|U_{1}|+c^{\prime}$. By (5), we have
$|U_{1}|\equiv|U_{2}|\mod c$, which implies $c^{\prime}\equiv 0\mod c$.

We are now ready to prove Lemma 37.

######  Proof C.3 (Proof of Lemma 37).

Let $c$ be the basic period of ${\mathcal{G}}$. We first define
$d_{N,N^{\prime}}$ for each $N,N^{\prime}\in{{\mathcal{N}}}^{\mathrm{inf}}$.
Since ${\mathcal{L}}\\!\left({\mathcal{G}},N{\Rightarrow}N^{\prime}\right)$ is
infinite (Lemma 54(1)), there exists
$U_{N,N^{\prime}}\in{\mathcal{L}}\\!\left({\mathcal{G}},N{\Rightarrow}N^{\prime}\right)$.
Let $d_{N,N^{\prime}}$ be the unique natural number $0\leq d_{N,N^{\prime}}<c$
such that $|U_{N,N^{\prime}}|\equiv d_{N,N^{\prime}}\mod c$. This definition
of $d_{N,N^{\prime}}$ does not depend on the choice of $U_{N,N^{\prime}}$, by
Lemma 54(5).

We define $n_{0}$. For every $N,N^{\prime}\in{{\mathcal{N}}}^{\mathrm{inf}}$,
since $c$ is a period of
${\mathcal{L}}\\!\left({\mathcal{G}},N{\Rightarrow}N^{\prime}\right)$, there
exists $n_{0}^{N,N^{\prime}}$ such that:

$\forall n\geq n_{0}^{N,N^{\prime}}.\;\forall k\in{\rm
Nature}.\quad{\mathcal{L}}_{n}\\!\left({\mathcal{G}},N{\Rightarrow}N^{\prime}\right)\neq\emptyset\
\Leftrightarrow\
{\mathcal{L}}_{n+ck}\\!\left({\mathcal{G}},N{\Rightarrow}N^{\prime}\right)\neq\emptyset.$

Let $n_{0}\triangleq\max\\{n_{0}^{N,N^{\prime}}\mid
N,N^{\prime}\in{{\mathcal{N}}}^{\mathrm{inf}}\\}$.

Then:

  * •

(1) follows from Lemma 54(5).

  * •

(2) follows from the definition of $n_{0}$, infinity of
${\mathcal{L}}\\!\left({\mathcal{G}},N{\Rightarrow}N^{\prime}\right)$ (Lemma
54(1)), and Lemma 54(5) (given $n\geq n_{0}$, pick
$U\in{\mathcal{L}}\\!\left({\mathcal{G}},N{\Rightarrow}N^{\prime}\right)$ such
that $|U|\geq n$; then $|U|=n+ck$ for some $k\geq 0$).

  * •

(3) follows from Lemma 54(3).

  * •

(4) follows from
$U_{N^{\prime},N^{\prime\prime}}[U_{N,N^{\prime}}]\in{\mathcal{L}}\\!\left({\mathcal{G}},N{\Rightarrow}N^{\prime\prime}\right)$
and Lemma 54(5).