On Quasi Ordinal Diagram Systems

TL;DR

This paper generalizes ordinal diagram systems using recent tree embedding theorems and explores their application in proving termination of complex term rewriting systems, including second-order systems.

Contribution

It extends Okada-Takeuti's ordinal diagram theory with modern embedding results and discusses their potential for termination proofs in advanced rewriting systems.

Findings

Generalization of ordinal diagram systems using Dershowitz-Tzameret's theorem

Application of ordinal notation to termination proofs for second-order rewriting

Potential for ordinal systems to improve termination analysis methods

Abstract

The purposes of this note are the following two; we first generalize Okada-Takeuti's well quasi ordinal diagram theory, utilizing the recent result of Dershowitz-Tzameret's version of tree embedding theorem with gap conditions. Second, we discuss possible use of such strong ordinal notation systems for the purpose of a typical traditional termination proof method for term rewriting systems, especially for second-order (pattern-matching-based) rewriting systems including a rewrite-theoretic version of Buchholz's hydra game.

Equations

$$I:=$$

$$(0,0^{\prime \prime }\#0^{\prime \prime })\#(2^{\prime },(2^{\prime },1^{\prime \prime \prime })\#(1^{\prime },1^{\prime \prime }))\#(1,0^{\prime \prime }\#(1,2^{\prime \prime }\#0^{\prime \prime }))$$

$$\bullet$$

Full text

1 Introduction

Dershowitz and Tzameret extended the Friedman-Kříž-Gordeev’s tree embedding theorem with gap conditions by relaxing the well orderedness condition for the labels of tree-nodes to a well quasi orderedness condition. The first purpose of our paper is to generalize Okada-Takeuti’s quasi ordinal diagram systems ([14, 13]) using this Dershowitz-Tzameret’s result. The second purpose is to analyze to which extent such a non-simplification ordering could be used as an extension of the typical termination proof method based on simplification orderings. We especially consider a “second-order (pattern-matching-based) rewrite rule” version of Buchholz’s hydra game.

A typical termination proof method for first-order term rewriting systems is to show the termination of a term rewriting system $R$ by verifying that for each rewrite rule $l(\vec{x})\to r(\vec{x})$ of $R$, $f(l(\vec{x})>f(r(\vec{x}))$ holds, where $f$ is a strictly order-preserving mapping and $<$ is a well founded ordering with the substitution property and the monotonicity property. Here, the substitution property and the monotonicity property mean (i) for any substitution (for the list of variables) $\sigma$, if $\alpha<\beta$ holds then $\alpha\sigma<\beta\sigma$ holds, and (ii) for any context $u[\ast]$, if $\alpha<\beta$ holds then $u[\alpha]<u[\beta]$ holds, respectively. The properties (i) and (ii) guarantee the termination of the whole $R$ because any application of (first-order) rewrite rule $l(\vec{x})\to r(\vec{x})$ has a form $u[l\sigma]\to u[r\sigma]$ for some context $u[\ast]$ and some substitution $\sigma$. In this note, we restrict our attention to the identity $f$ for our basic argument.

The method has been widely used for termination proofs as well as a tool for Knuth-Bendix completion. The method itself would be attractive not only for the traditional first-order rewriting but also for higher-order or graphic-pattern-matching-based rewriting. One could expect that strong and general ordering structures in proof theory would be useful for this termination proof method of higher-order pattern-matching-based rewrite systems.

However, the use of strong orderings such as $<_{\_}i$ on Takeuti’s ordinal diagram systems, which is a non-simplification ordering, cannot satisfy the two basic properties (i) and (ii). Because of this difficulty, instead of the traditional termination proof method, various different techniques for the termination of higher-order rewriting systems have been utilized; for example, Jouannaud and Okada ([10]) introduced a generalized form of Tait-Girard’s reducibility candidates method (cf. also [2, 3] with Blanqui).

Hence at a first look, it seems hard to adapt ordinal diagram systems to the traditional termination method. It is a natural question how we could adapt them to the termination proof method especially for higher-order rewriting systems. We aim to answer this question in the present paper.

This paper is structured as follows. We first define our generalized quasi ordinal diagram systems $\mathsf{GQ}(I,A)$ (§2.1), then prove the well quasi orderedness of these systems as a corollary of the Dershowitz-Tzameret’s version of tree embedding theorem (§2.2). Next, we propose a termination proof method induced by the monotonicity property and a restricted substitution property of $\mathsf{GQ}(I,A)$ (§3.1). Finally, we take a version of Buchholz game as an example of pattern-matching-based second-order rewrite systems and show its termination by another termination proof method in terms of $\mathsf{GQ}(I,A)$ (§3.2). Note that the termination of the original version and its variants of Kirby-Paris’s hydra game could be proved in the traditional termination method of simplification orderings (cf. [9]).

2 Well quasi ordered systems of generalized quasi ordinal diagrams

In this section, we first generalize quasi ordinal diagram systems $(\mathsf{Q}(I,A),\leq_{\_}i)$ of Okada-Takeuti ([13, 14]) by using an arbitrary well partial ordering $I$ as the inner node labels (§2.1). Next, we prove the well quasi orderedness of these generalized systems as a direct corollary of the Dershowitz-Tzameret’s version ([7]) of tree embedding theorem with gap condition (§2.2).

2.1 Formulation of generalized quasi ordinal diagram systems

A quasi ordering is a pair $(D,\leq)$ of a set $D$ and a binary relation $\leq$ such that for any $a\in D$, $a\leq a$ holds (reflexivity) and for any $a,b,c\in D$, if $a\leq b$ and $b\leq c$ hold then $a\leq c$ holds (transitivity). A partial ordering is a quasi ordering $(D,\leq)$ with the antisymmetry: For any $a,b\in D$, if $a\leq b$ and $b\leq a$ hold then $a=b$ holds. A linear ordering is a partial ordering $(D,\leq)$ with the linearity: For any $a,b\in D$, $a\leq b$ or $b\leq a$ holds. A well quasi ordering is a quasi ordering $(D,\leq)$ such that for any infinite sequence $a_{\_}0,a_{\_}1,\ldots$ from $D$, there are numbers $n$ and $m$ such that $n<m$ and $a_{\_}n\leq a_{\_}m$ holds. A well partial ordering is a partial ordering that is a well quasi ordering. For a quasi ordering $(D,\leq)$, we use abbreviation “$a<b$” for “$a\leq b$ and $b\not\leq a$.” Note that the well quasi orderedness has a weaker definition saying that for any infinite $\leq$-decreasing sequence $a_{\_}0\geq a_{\_}1\geq\ldots$ from $D$, there are numbers $n$ and $m$ such that $n<m$ and $a_{\_}n\leq a_{\_}m$ holds. A weak well quasi ordering is a quasi ordering $(D,\leq)$ satisfying this condition. In this paper, we show the stronger version of well quasi orderedness of our quasi ordinal diagram systems.

Let $(I,\leq_{\_}I)$ be a well partial ordering and $(A,\leq_{\_}A)$ be a well quasi ordering. We define the set $\mathcal{F}_{\_}0$ of constants and the set $\mathcal{F}_{\_}1$ of unary function symbols as follows: $\mathcal{F}_{\_}0:=A$, $\mathcal{F}_{\_}1:=\{f_{\_}i\mid i\in I\}$. Let $\mathcal{F}$ be a signature defined as the union of $\mathcal{F}_{\_}0$, $\mathcal{F}_{\_}1$ and $\{\#\}$ with a varyadic function symbol $\#$.

The pre-domain $\mathsf{preGQ}(I,A)$ of generalized quasi ordinal diagrams on $(I,\leq_{\_}I)$ and $(A,\leq_{\_}A)$ is the set $\mathcal{T}(\mathcal{F})$ of all terms constructed from symbols in $\mathcal{F}$. To follow the notation in [13, 14], we denote terms of $\mathsf{preGQ}(I,A)$ by $\alpha,\beta,\gamma,\ldots$ and adopt the following abbreviations: $(i,\alpha):=f_{\_}i(\alpha)$, $\alpha_{\_}1\#\cdots\#\alpha_{\_}n:=\#(\alpha_{\_}1,\ldots,\alpha_{\_}n)$. We call a term that belongs to $\mathcal{F}_{\_}0$ or has the form of $(i,\alpha)$ a connected term of $\mathsf{preGQ}(I,A)$, and a term that has the form $\alpha_{\_}1\#\cdots\#\alpha_{\_}n$ an unconnected term of $\mathsf{preGQ}(I,A)$. When an unconnected term $\alpha$ is indicated as $\alpha\equiv\alpha_{\_}1\#\cdots\#\alpha_{\_}n$, we assume that all of $\alpha_{\_}1,\ldots,\alpha_{\_}n$ are connected. For a connected term $\alpha$, a term $\beta$ is a component of $\alpha$ if and only if $\beta\equiv\alpha$ holds. For an unconnected term $\alpha\equiv\alpha_{\_}1\#\cdots\#\alpha_{\_}n$, a term $\beta$ is a component of $\alpha$ if and only if for some $k$ with $1\leq k\leq n$, $\beta\equiv\alpha_{\_}k$ holds.

Definition 2.1** (Labeled Finite Trees).**

Labeled finite trees are defined as follows.

A finite tree is a partial ordering $(T,\leq_{\_}T)$ such that $T$ is a finite set with the $\leq_{\_}T$-least element called the root, and for any $a\in T$, the set $\{b\in T\mid b\leq_{\_}Ta\}$ is linearly ordered with respect to $\leq_{\_}T$. 2. 2.

Let $(I,\leq_{\_}I)$ be a quasi ordering. A $I$-labeled finite tree is a pair of a finite tree $(T,\leq_{\_}T)$ and a mapping $l:T\to I$.

Let $(T,\leq_{\_}T)$ be a finite tree. For any $a\in T$, if the set $\{b\in T\mid b<_{\_}Ta\}$ is non-empty, then we call its greatest element the immediate lower node of $a$. We call $\leq_{\_}T$-maximal elements of $T$ leaves of $T$. The $\leq_{\_}T$-greatest lower bound of $\{a,b\}$ is denoted by $a\land b$.

Example 2.2**.**

Let $I$ and $A$ be the following well partial ordering and well quasi ordering, respectively, where the arrow $i\rightarrow j$ means $i<_{\_}Ij$ and $a\rightsquigarrow b$ means $a\leq_{\_}Ab$.

[TABLE]

In addition, we stipulate that for any $i\in I$ and any $a\in A$, $a<_{\_}{I}i$ hold. Here we use the symbol $\omega^{\prime}$ since $I$ is similar to the ordinal $\omega$. An example of forest representation are as follows.

[TABLE]

Note that $\#$ is represented by tree’s sum and branching. By the definition of the identity below, $\#$ denotes the associative-commutative sum of connected terms, which is called “natural sum.” In term rewrite orderings such as the recursive path ordering, $\alpha_{\_}1\#\cdots\#\alpha_{\_}n$ is often represented as $\langle\alpha_{\_}1,\ldots,\alpha_{\_}n\rangle$.

Definition 2.3** (Identity on $\mathsf{preGQ}(I,A)$).**

For any two terms $\alpha$ and $\beta$ of $\mathsf{preGQ}(I,A)$, the identity relation $\alpha=\beta$ holds if and only if either (1) both of $\alpha$ and $\beta$ are elements of $A$, and $\alpha$ is identical with $\beta$ in the sense of $A$, or (2) $\alpha\equiv(i,\alpha^{\prime})$, $\beta\equiv(i,\beta^{\prime})$ and $\alpha^{\prime}=\beta^{\prime}$ hold, or (3) $\alpha\equiv\alpha_{\_}1\#\cdots\#\alpha_{\_}n$ and $\beta\equiv\beta_{\_}1\#\cdots\#\beta_{\_}n$ hold with $n>1$ and there is a permutation $p$ of $\{1,\ldots,n\}$ such that $\alpha_{\_}i=\beta_{\_}{p(i)}$ holds for any $i$.

Definition 2.4** ($i$-sections).**

For any two terms $\alpha$ and $\beta$ of $\mathsf{preGQ}(I,A)$ and any element $i$ of $I$, the relation $\alpha\subset_{\_}i\beta$, which we call “$\alpha$ is an $i$-section of $\beta$”, is defined as follows.

If $\beta$ is an element of $A$, then $\alpha\subset_{\_}i\beta$ never holds. 2. 2.

If $\beta\equiv(j,\beta^{\prime})$ holds, then

1. (a)

when $i=j$ holds, $\alpha\subset_{\_}i\beta$ if and only if $\alpha=\beta^{\prime}$ or $\alpha\subset_{\_}i\beta^{\prime}$, 2. (b)

when $i<j$ holds, $\alpha\subset_{\_}i\beta$ if and only if $\alpha\subset_{\_}i\beta^{\prime}$, 3. (c)

when $i\not\leq j$ holds, $\alpha\subset_{\_}i\beta$ never holds. 3. 3.

If $\beta\equiv\beta_{\_}1\#\ldots\#\beta_{\_}m$ holds with $m>1$, then $\alpha\subset_{\_}i\beta$ if and only if for some $\beta_{\_}l\;(1\leq l\leq m)$, $\alpha\subset_{\_}i\beta_{\_}l$.

Example 2.5** (An example of an $i$-section).**

Consider the domain $\mathsf{preGQ}(I,A)$ defined in Example 2.2.

\textstyle{\bullet}$$\textstyle{5}$$\textstyle{\bullet}$$\textstyle{\omega^{\prime}}$$\textstyle{\bullet}$$\textstyle{3}$$\textstyle{\bullet}$$\textstyle{2}$$\textstyle{\alpha}$$\textstyle{\beta:=}Here $3,\omega^{\prime},5$ appears as labels, in this order, below $(2,\alpha)$.Since $3,\omega^{\prime},5$ are greater than or equal to $2$, $\alpha\subset_{\_}2\beta$ holds by definition,$\textstyle{\text{where }\beta\equiv(5,\cdots\#(\omega^{\prime},\cdots\#(3,\cdots\#(2,\alpha)\#\cdots)\#\cdots)\#\cdots).}$

An element $i$ of $I$ is an index of $\alpha$ if and only if there is a $\beta$ such that $\beta$ is an $i$-section of $\alpha$. Set $\tilde{I}:=I\cup\{\infty\}$. For any $i\in I$ and any finite set $\{\alpha_{\_}0,\ldots,\alpha_{\_}n\}$ of terms, define $\mathsf{idx}_{i}\{\alpha_{\_}0,\ldots,\alpha_{\_}n\}:=\{j\mid i<j,\;j\text{ is an index of }\alpha_{\_}0\text{ or }\ldots\text{ or }\alpha_{\_}n\}$. We denote the cardinality of $\mathsf{idx}_{i}\{\alpha_{\_}0,\ldots,\alpha_{\_}n\}$ by $\#\mathsf{idx}_{i}\{\alpha_{\_}0,\ldots,\alpha_{\_}n\}$. For any finite set $\{\alpha_{\_}0,\ldots,\alpha_{\_}n\}$ of terms, the total number of all occurrences of $(,)$ and $\#$ in $\alpha_{\_}0,\ldots,\alpha_{\_}n$ is denoted by $l(\alpha_{\_}0,\ldots,\alpha_{\_}n)$.

Definition 2.6** (Ordering $\leq^{\mathsf{q}}_{\_}i$ on $\mathsf{preGQ}(I,A)$).**

For any element $i$ of $\tilde{I}$, the relation $\leq^{\mathsf{q}}_{\_}i$ on $\mathsf{preGQ}(I,A)$ is defined by double induction on (1) $l(\alpha,\beta)$ and (2) $\#\mathsf{idx}_{i}\{\alpha,\beta\}$, in this order.

If both of $\alpha$ and $\beta$ are elements of $A$, then for any element $i$ of $\tilde{I}$, $\alpha\leq^{\mathsf{q}}_{\_}i\beta$ if and only if $\alpha\leq_{\_}A\beta$. 2. 2.

If $\alpha$ is an element of $A$ and $\beta$ is not, then for any element $i$ of $\tilde{I}$, both $\alpha\leq^{\mathsf{q}}_{\_}i\beta$ and $\beta\not\leq^{\mathsf{q}}_{\_}i\alpha$ hold. 3. 3.

If $\alpha\equiv\alpha_{\_}1\#\ldots\#\alpha_{\_}n$ and $\beta\equiv\beta_{\_}1\#\ldots\#\beta_{\_}m$ hold with $n+m>2$, then for any element $i$ of $\tilde{I}$, $\alpha\leq^{\mathsf{q}}_{\_}i\beta$ if and only if one of the following conditions holds:

1. (a)

there is a $\beta_{\_}l\;(1\leq l\leq m)$ such that for any $k\;(1\leq k\leq n)$, $\alpha_{\_}k\leq^{\mathsf{q}}_{\_}i\beta_{\_}l$ and $\beta_{\_}l\not\leq^{\mathsf{q}}_{\_}i\alpha_{\_}k$ hold, 2. (b)

there is a $\beta_{\_}l\;(1\leq l\leq m)$ such that $\alpha_{\_}1\leq^{\mathsf{q}}_{\_}i\beta_{\_}l$, and if $n\geq 2$ then the following holds.

$\alpha_{\_}2\#\ldots\#\alpha_{\_}{n}\leq^{\mathsf{q}}_{\_}i\beta_{\_}1\#\ldots\#\beta_{\_}{l-1}\#\beta_{\_}{l+1}\#\ldots\#\beta_{\_}{m}$ 4. 4.

If $\alpha\equiv(j,\alpha_{\_}0)$, $\beta\equiv(j^{\prime},\beta_{\_}0)$ and $i=\infty$ hold, then $\alpha\leq^{\mathsf{q}}_{\_}{\infty}\beta$ if and only if either $j<j^{\prime}$ holds or both $j=j^{\prime}$ and $\alpha_{\_}0\leq^{\mathsf{q}}_{\_}j\beta_{\_}0$ hold. 5. 5.

If $\alpha\equiv(j,\alpha_{\_}0)$ and $\beta\equiv(j^{\prime},\beta_{\_}0)$ hold and $i$ is an element of $I$, then $\alpha\leq^{\mathsf{q}}_{\_}i\beta$ if and only if either

1. ($\exists$)

there is a $\beta^{\prime}\subset_{\_}i\beta$ such that $\alpha\leq^{\mathsf{q}}_{\_}i\beta^{\prime}$, or 2. ($\forall$)

for any $\alpha^{\prime}\subset_{\_}i\alpha$, both of $\alpha^{\prime}\leq^{\mathsf{q}}_{\_}i\beta$ and $\beta\not\leq^{\mathsf{q}}_{\_}i\alpha^{\prime}$ hold, and if $\mathsf{idx}_{i}\{\alpha,\beta\}\neq\emptyset$ holds then $\alpha\leq^{\mathsf{q}}_{\_}{j}\beta$ holds for any minimal element $j$ of $\mathsf{idx}_{i}\{\alpha,\beta\}$, otherwise $\alpha\leq^{\mathsf{q}}_{\_}{\infty}\beta$ holds.

We say $\alpha\leq^{\mathsf{q}}_{\_}i\beta$ holds by $\exists$-condition, when the condition ($\exists$) above holds. Similarly, we say $\alpha\leq^{\mathsf{q}}_{\_}i\beta$ holds by $\forall$-condition, when the condition ($\forall$) above holds. Note that if $I$ is a finite set, $j$ in the condition ($\forall$) can be taken as a $\leq_{\_}I$-maximal element of $\{h\mid h>_{\_}Ii\}$, and the resulting ordering $\leq^{\mathsf{q}}_{\_}i$ becomes the same as the one defined above.

Remark 2.7**.**

Consider $\mathsf{preGQ}(I,A)$ defined in Example 2.2. For the readers familiar to the recursive path ordering $\geq_{\_}{rpo}$ (cf. [5]), the table below suggests some similarity of $\geq_{\_}{i}^{\mathsf{q}}$ to $\geq_{\_}{rpo}$ and the richness of $\geq_{\_}{i}^{\mathsf{q}}$ in the sense that $\geq_{\_}{i}^{\mathsf{q}}$ for some $i\in I$ depends on $\geq_{\_}{j}^{\mathsf{q}}$ for another $j\in I$. When we stipulate that $i>\#$ holds for any $i\in I$, we have the following table:

[TABLE]

Lemma 2.8**.**

For any well partial ordering $I$, any well quasi ordering $A$ and any element $i$ of $\tilde{I}$,

$(\mathsf{preGQ}(I,A),\leq^{\mathsf{q}}_{\_}i)$ is a quasi ordering.

Proof.

Prove the following sublemmas (1) and (2) by double induction on $\langle l(\alpha,\beta,\gamma),\#\mathsf{idx}_{i}\{\alpha,\beta,\gamma\}\rangle$ and double induction on $\langle l(\alpha),\#\mathsf{idx}_{i}\{\alpha\}\rangle$, respectively. (1) (Transitivity) For every $\alpha,\beta,\gamma\in\mathsf{preGQ}(I,A)$ and every $i\in\tilde{I}$, if $\alpha\leq^{\mathsf{q}}_{\_}i\beta$ and $\beta\leq^{\mathsf{q}}_{\_}i\gamma$ hold then $\alpha\leq^{\mathsf{q}}_{\_}i\gamma$ holds. (2) (Reflexivity) For every $\alpha\in\mathsf{preGQ}(I,A)$ and every $i\in\tilde{I}$, the following two hold: $\alpha\leq^{\mathsf{q}}_{\_}{i}\alpha$ holds, and if $i\in I$ holds then for any $\beta\in\mathsf{preGQ}(I,A)$ with $\alpha\subset_{\_}i\beta$, $\alpha\leq^{\mathsf{q}}_{\_}{i}\beta$ and $\beta\not\leq^{\mathsf{q}}_{\_}{i}\alpha$ hold. ∎

Remark 2.9**.**

Let us comment on the definitions of $i$-sections (Definition 2.4) and $\leq^{\mathsf{q}}_{\_}i$ (Definition 2.6).

• •

If we replace “$i\not\leq j$” in Definition 2.4.2.(c) with “$i>j$”, then we obtain the definition of $i$-sections in [13, 14].

• •

We defined $\mathsf{preGQ}(I,A)$ by taking $I$ as not a well quasi ordering but a well partial ordering. The antisymmetry of $I$ is needed to verify the transitivity of $\leq^{\mathsf{q}}_{\_}{\infty}$. In addition, note that the proof for the lemma above neither depends on the well quasi orderedness of $I$ nor the one of $A$. If we take $I$ as a well ordering, then in Definition 2.6.5.($\forall$) there always exists the least element of $\mathsf{idx}_{i}\{\alpha,\beta\}$ if it is non-empty. This is the only difference of our orderings $\leq^{\mathsf{q}}_{\_}i$ from the ones in [13, 14].

The central quasi ordering $\lll$ in this paper is a generalization of the linear ordering appeared in [12], which satisfies the monotonicity property. We will show in Section 3.1 that our ordering $\lll$ satisfies the monotonicity property as well (cf. Lemma 3.1).

Definition 2.10** (Ordering $\alpha\lll\beta$).**

For any two terms $\alpha,\beta$ of $\mathsf{preGQ}(I,A)$, $\alpha\lll\beta$ holds if and only if $\alpha<^{\mathsf{q}}_{\_}i\beta$ holds for any element $i$ of $\tilde{I}$.

Let $\lll^{=}$ be the reflexive closure of $\lll$. It is obvious that $(\mathsf{preGQ}(I,A),\lll^{=})$ is a quasi ordering and that for any $\alpha$ and $\beta$, $\alpha\lll\beta$ holds if and only if both $\alpha\lll^{=}\beta$ and $\beta\not\lll^{=}\alpha$ holds.

Next, we restrict the pre-domains $\mathsf{preGQ}(I,A)$ to the path comparable tree-domain $\mathsf{GQ}(I,A)$, since there is a counterexample for the well quasi orderedness of $(\mathsf{preGQ}(I,A),\lll^{=})$. In fact, we have a counterexample for its weak well quasi orderedness.

Example 2.11**.**

A counterexample for the weak well quasi orderedness of $(\mathsf{preGQ}(I,A),\lll^{=})$ is as follows: Let $I$ be $\{0,a_{\_}1,a_{\_}2,b_{\_}1,b_{\_}2\}$ and $A$ be $\{0\}$, where $0<_{\_}Ia_{\_}1<_{\_}Ib_{\_}1$, $0<_{\_}Ia_{\_}2<_{\_}Ib_{\_}2$ and for any $c\in\{a_{\_}1,b_{\_}1\}$ and $d\in\{a_{\_}2,b_{\_}2\}$, neither $c\leq_{\_}Id$ nor $d\leq_{\_}Ic$ holds. Then, we have the following infinite sequence.

$(a_{\_}1,(b_{\_}2,0))\ggg(a_{\_}1,(a_{\_}2,(b_{\_}1,0)))\ggg(a_{\_}1,(a_{\_}2,(a_{\_}1,(b_{\_}2,0))))\ggg(a_{\_}1,(a_{\_}2,(a_{\_}1,(a_{\_}2,(b_{\_}1,0)))))\ggg\ldots$

This kind of counterexamples is blocked if we restrict the pre-domains $\mathsf{preGQ}(I,A)$ to the path comparable tree-domains $\mathsf{GQ}(I,A)$. In the rest of this subsection and the next subsection, we assume that pre-domains $\mathsf{preGQ}(I,A)$ satisfy the following conditions: $I\cap A=\emptyset$ and $a<_{\_}{I}i$ holds for any $i\in I$ and any $a\in A$. In addition, we identify a connected term $\alpha$ of $\mathsf{preGQ}(I,A)$ with a labeled finite tree $((T,\leq_{\_}T),l_{\_}T)$ in the manner of Example 2.2. For any quasi ordering $(A,\leq_{\_}A)$ and any two elements $a_{\_}1,a_{\_}2$ of $A$, we say $a_{\_}1$ is comparable with $a_{\_}2$ if and only if $a_{\_}1\leq_{\_}Aa_{\_}2$ or $a_{\_}2\leq_{\_}Aa_{\_}1$ holds.

Definition 2.12** (Path comparable tree-domains $\mathsf{GQ}(I,A)$ of $\mathsf{preGQ}(I,A)$, cf. [7]).**

The path comparable tree-domain $\mathsf{GQ}(I,A)$ of $\mathsf{preGQ}(I,A)$ is defined as follows:

If $a\in A$ holds, then $a$ is a connected term of $\mathsf{GQ}(I,A)$. 2. 2.

Let $\alpha_{\_}1,\ldots,\alpha_{\_}n$ be connected terms of $\mathsf{GQ}(I,A)$ with $\alpha_{\_}1=((T_{\_}1,\leq_{\_}1),l_{\_}1),\ldots,\alpha_{\_}n=((T_{\_}n,\leq_{\_}n),l_{\_}n)$. If $i$ is comparable with $l_{\_}k(a)$ for any $k$ $(1\leq k\leq n)$ and any $a\in T_{\_}k$, then $(i,\alpha_{\_}1\#\cdots\#\alpha_{\_}n)$ is a connected term of $\mathsf{GQ}(I,A)$. 3. 3.

If $\alpha_{\_}1,\ldots,\alpha_{\_}n$ are connected terms of $\mathsf{GQ}(I,A)$, then $\alpha_{\_}1\#\ldots\#\alpha_{\_}n$ is an unconnected term of $\mathsf{GQ}(I,A)$.

A generalized quasi ordinal diagram system is a pair $(\mathsf{GQ}(I,A),\lll^{=})$ of a path comparable tree-domain $\mathsf{GQ}(I,A)$ and the quasi ordering $\lll^{=}$ on this domain. We often abbreviate $(\mathsf{GQ}(I,A),\lll^{=})$ as $\mathsf{GQ}(I,A)$. Hereafter, we call a connected term (resp. an unconnected term) of $\mathsf{GQ}(I,A)$ a connected gqod (resp. an unconnected gqod). For $\mathsf{GQ}(I,A)$, we have the following lemma by induction on $l(\alpha)$.

Lemma 2.13**.**

For any element $(i,\alpha)$ of $\mathsf{GQ}(I,A)$, $\alpha<^{\mathsf{q}}_{\_}j(i,\alpha)$ holds for any element $j$ of $I$ with $j\leq i$.

2.2 Well quasi ordering proof for $(\mathsf{GQ}(I,A),\lll^{=})$ via Dershowitz and Tzameret’s tree embedding theorem

We first recall Dershowitz-Tzameret’s tree embedding with gap condition (cf. [7, Definition 3.3]).

Definition 2.14** (Tree Embedding $\hookrightarrow$).**

For any two connected gqod’s $\alpha=((T_{\_}1,\leq_{\_}1),l_{\_}1)$ and

$\beta=((T_{\_}2,\leq_{\_}2),l_{\_}2)$, $\alpha\hookrightarrow\beta$ holds if and only if there is an injection $\iota:T_{\_}1\to T_{\_}2$ such that

(Node condition 1) for any $a\in T_{\_}1$, $l_{\_}1(a)\leq_{\_}{I}l_{\_}2(\iota(a))$ holds, 2. 2.

(Node condition 2) for any $a_{\_}1,a_{\_}2\in T_{\_}1$, $\iota(a_{\_}1\wedge a_{\_}2)=\iota(a_{\_}1)\wedge\iota(a_{\_}2)$ holds, 3. 3.

(Edge condition) if $a_{\_}1$ is an element of $T_{\_}1$ with its immediate lower node $a_{\_}2$ in $T_{\_}1$, then for any $b\in T_{\_}2$ with $\iota(a_{\_}2)<_{\_}2b<_{\_}2\iota(a_{\_}1)$, $l_{\_}1(a_{\_}1)\leq_{\_}Il_{\_}2(b)$ holds, and 4. 4.

(Root condition) if $a$ is the root of $T_{\_}1$, then for any $b\in T_{\_}2$ with $b<_{\_}2\iota(a)$, $l_{\_}1(a)\leq_{\_}Il_{\_}2(b)$ holds.

Example 2.15**.**

The following is an example of Dershowitz-Tzameret’s tree embedding (cf. [7, p.87]).

[TABLE]

Theorem 2.16** (Theorem 3.1 in [7]).**

Let $\mathsf{GQ}^{ctd}(I,A)$ be the set of all connected gqod’s from $\mathsf{GQ}(I,A)$. Then, $(\mathsf{GQ}^{ctd}(I,A),\hookrightarrow)$ is a well quasi ordering.

Next, we extend this tree embedding to forests, namely, unconnected gqod’s and show that $\alpha\lll^{=}\beta$ holds whenever $\alpha$ is embedded into $\beta$ in the sense of this forest embedding.

Definition 2.17** (Forest Embedding $\hookrightarrow^{\#}$).**

For any two terms $\alpha$ and $\beta$ of $\mathsf{GQ}(I,A)$ with $\alpha\equiv\alpha_{\_}1\#\cdots\#\alpha_{\_}n$ and $\beta\equiv\beta_{\_}1\#\cdots\#\beta_{\_}m$ ($n,m>0$), $\alpha\hookrightarrow^{\#}\beta$ holds if and only if $n\leq m$ and there is a permutation $p$ of $\{1,\ldots,n\}$ such that $\alpha_{\_}i\hookrightarrow\beta_{\_}{p(i)}$ for any $i$ with $1\leq i\leq n$.

Proposition 2.18**.**

For every $\alpha,\beta\in\mathsf{GQ}(I,A)$, if $\alpha\hookrightarrow^{\#}\beta$ holds, then $\alpha\lll^{=}\beta$ holds.

Proof.

By Lemma 2.13, one can prove the following sublemma (1) and (2). For every $\alpha,\beta\in\mathsf{GQ}(I,A)$ and every $i,j\in I$ with $i\leq j$, (1) if $\beta$ is connected and $(i,\alpha)\lll^{=}\beta$ holds, then $(i,\alpha)\lll(j,\beta)$ holds, and (2) if $\beta\equiv\beta_{\_}1\#\cdots\#\beta_{\_}n\;(n>1)$ and for some $m\;(1\leq m\leq n)$, $(i,\alpha)\lll^{=}\beta_{\_}m$ hold, then $(i,\alpha)\lll(j,\beta)$ holds.

We prove Proposition 2.18 by induction on $l(\alpha)$. The base case is obvious. If $\alpha$ is unconnected, then the proposition immediately follows from IH. Suppose that $\alpha\equiv(i_{\_}1,\alpha^{\prime})$ holds. By the definition of $\hookrightarrow^{\#}$, it suffices to prove the proposition when $\beta$ is a connected gqod $(i_{\_}2,\beta^{\prime})$. In this case, the proposition follows from the following two claims: For any $i\in I$ and any $\delta\subset_{\_}i\alpha$, $\delta<^{\mathsf{q}}_{\_}i\beta$ holds, and $\alpha\leq^{\mathsf{q}}_{\_}{\infty}\beta$ holds.

First, we show that for any $i\in I$ and any $\delta\subset_{\_}i\alpha$, $\delta<^{\mathsf{q}}_{\_}i\beta$ holds. Consider a gqod $\delta$ with $\delta\subset_{\_}i\alpha$ and put $\delta\equiv\delta_{\_}1\#\cdots\#\delta_{\_}n\;(n\geq 1)$. We show that $\delta_{\_}k<^{\mathsf{q}}_{\_}i\beta$ for any $k$ with $1\leq k\leq n$. If $\delta_{\_}k\in A$ holds then $\delta_{\_}k<^{\mathsf{q}}_{\_}i\beta$ obviously holds, so we assume that $\delta_{\_}k$ is of the form $(i_{\_}k,\delta_{\_}k^{\prime})$. Let us denote this outermost occurrence of $i_{\_}k$ in $\delta_{\_}k$ by $i_{\_}k^{*}$. Suppose that the embedding $\alpha\hookrightarrow^{\#}\beta$ maps $i_{\_}k^{*}$ to the outermost occurrence of $j_{\_}k$ in a sub-gqod $(j_{\_}k,\beta_{\_}k)$ of $\beta$. We denote this outermost occurrence of $j_{\_}k$ in $(j_{\_}k,\beta_{\_}k)$ by $j_{\_}k^{*}$. Since $\delta_{\_}k\hookrightarrow^{\#}(j_{\_}k,\beta_{\_}k)$ holds, we have by IH $\delta_{\_}k\lll^{=}(j_{\_}k,\beta_{\_}k)$ for any $k$. On the other hand, $\alpha$ has a sub-gqod $(i,\delta)$ because $\delta\subset_{\_}i\alpha$ holds. Denote this occurrence of $i$ in $\alpha$ by $i^{*}$ and suppose that the embedding $\alpha\hookrightarrow^{\#}\beta$ maps $i^{*}$ to the outermost occurrence $j^{*}$ of $j$ in a sub-gqod $(j,\gamma_{\_}1\#\cdots\#\gamma_{\_}m)$ of $\beta$ ($m\geq 1$), as the following figure.

[TABLE]

Because of the gap condition of $\hookrightarrow^{\#}$, we have $\delta_{\_}k\lll\gamma_{\_}1\#\cdots\#\gamma_{\_}m$ for any $k$ by using sublemmas (1) and (2) above repeatedly. For example, if $(j_{\_}1^{*},\beta_{\_}1)$ is subsumed by $(h,\eta_{\_}1\#(j_{\_}1^{*},\beta_{\_}1)\#\eta_{\_}2)$ and $h\neq j^{*}$, then $h\geq i_{\_}1$ holds by the gap condition. Therefore, we have $\delta_{\_}1\lll(h,\eta_{\_}1\#(j_{\_}1^{*},\beta_{\_}1)\#\eta_{\_}2)$ by the sublemma (2). By repeating this argument, we have $\delta_{\_}k\lll\gamma_{\_}l$ for some $l$ with $1\leq l\leq m$. Since $\gamma_{\_}1\#\cdots\#\gamma_{\_}m<^{\mathsf{q}}_{\_}i(j,\gamma_{\_}1\#\cdots\#\gamma_{\_}m)$ by Lemma 2.13, $\delta_{\_}k<^{\mathsf{q}}_{\_}i(j,\gamma_{\_}1\#\cdots\#\gamma_{\_}m)$ holds for any $k$. Therefore, $\delta<^{\mathsf{q}}_{\_}i(j,\gamma_{\_}1\#\cdots\#\gamma_{\_}m)$ holds. Note that $i\leq h$ holds for any $h$ occurring in the path from $j^{*}$ to the root of $\beta$ because of the gap condition and the fact that $\delta$ is an $i$-section of $\alpha$. Therefore, by Lemma 2.13, we have $\delta<^{\mathsf{q}}_{\_}i\beta$.

By an argument similar to the one above, one can verify that $\alpha\leq^{\mathsf{q}}_{\_}{\infty}\beta$ holds. ∎

Theorem 2.19**.**

The system $(\mathsf{GQ}(I,A),\hookrightarrow^{\#})$ is a well quasi ordering.

Proof.

Let $\{\alpha_{\_}i\}$ and $\{\beta_{\_}i\}$ be infinite sequences of gqod’s. We say $\{\alpha_{\_}i\}$ is a component subsequence of $\{\beta_{\_}i\}$ if and only if there is a monotone function $f:\mathbb{N}\to\mathbb{N}$ such that for any $i\in\mathbb{N}$, $\alpha_{\_}i$ is a component of $\beta_{\_}{f(i)}$. In addition, an infinite sequence $\{a_{\_}i\}$ from a quasi ordering $(A,\leq)$ is $\leq$-bad if and only if there is no pair $i,j$ of natural numbers such that both $i<j$ and $a_{\_}i\leq a_{\_}j$ hold.

In a way similar to the proof of [13, Lemma 17], one can prove the following claim. Let $\{\alpha_{\_}i\}$ be an infinite sequence from $\mathsf{GQ}(I,A)$. If there is no $\hookrightarrow$-bad component subsequence $\{\beta_{\_}i\}$ of $\{\alpha_{\_}i\}$, then $\{\alpha_{\_}i\}$ is $\hookrightarrow^{\#}$-good, that is, $\{\alpha_{\_}i\}$ is not $\hookrightarrow^{\#}$-bad. By this claim and Theorem 2.16, we have the theorem. ∎

Corollary 2.20**.**

The system $(\mathsf{GQ}(I,A),\lll^{=})$ is a well quasi ordering.

3 Discussion of generalized quasi ordinal diagram systems from the viewpoint of termination proof methods

In this section, we apply the well quasi orderedness of $(\mathsf{GQ}(I,A),\lll^{=})$ to termination proof methods for second-order pattern-matching-based rewriting systems. First, we propose a termination proof method induced by the monotonicity property and a restricted substitution property of $(\mathsf{GQ}(I,A),\lll^{=})$ (§3.1). Next, we consider Buchholz-style hydra game as an example (cf. [4, 8]), and show the termination of a rewriting system in this game by another termination proof method in terms of $(\mathsf{GQ}(I,A),\lll^{=})$ (§3.2).

3.1 Application of $(\mathsf{GQ}(I,A),\lll^{=})$ to the termination proof method

Let $V$ be a finite set of variables. In this and next subsections, we consider an arbitrary system $\mathsf{GQ}(I,A)$ satisfying the following conditions: (1) $A=V\cup\{\rho\}$ holds, and neither $x\leq_{\_}Ay$ nor $y\leq_{\_}Ax$ holds for any $x,y\in V$, and $\rho$ is the $\leq_{\_}A$-minimum element of $A$, and (2) $\rho\in I$ and $I\cap V=\emptyset$ hold, and $\rho<_{\_}Ix<_{\_}Ii$ holds for any $x\in V$ and any $i\in I\setminus\{\rho\}$. We denote the set of all contexts from $\mathsf{GQ}(I,A)$ by $\mathcal{C}$.

A numeral substitution $\sigma$ for a gqod $\alpha$ is a substitution assigning a numeral term to each variable in $\alpha$, where a numeral term is a connected gqod that consists of $\rho$’s only. Note that the numeral terms are generalization of the numerals represented by no $\#$-branching trees $\rho-\rho-\cdots-\rho$; the numeral terms correspond to the ordinals up to $\varepsilon_{\_}0$.

As we will see below, the system $(\mathsf{GQ}(I,A),\lll^{=})$ satisfies not only the monotonicity property (Lemma 3.1) but also the following restricted substitution property (Lemma 3.2): For any connected terms $\alpha$ and $\beta$ of $\mathsf{GQ}(I,A)$ with $\alpha,\beta\not\in A$, if $\alpha\lll\beta$ holds then $\alpha\sigma\lll\beta\sigma$ holds for any numeral substitution $\sigma$. Therefore, if $l\ggg r$ holds for any rule $l\rhd r$ of a rewriting system $R$, then we immediately obtain the termination of the $R$-rewrite relation $\to$ defined as follows: $\alpha\to\beta$ holds if and only if $\alpha\equiv(i,u[l])\sigma$ and $\beta\equiv(i,u[r])\sigma$ for some context $u[\ast]$ and some numeral substitution $\sigma$.

Lemma 3.1** (The monotonicity property lemma).**

Let $\alpha$ and $\beta$ be gqod’s with $u[\alpha]\in\mathsf{GQ}(I,A)$ and $u[\beta]\in\mathsf{GQ}(I,A)$. If $\alpha\lll\beta$ holds, then $u[\alpha]\lll u[\beta]$ holds.

Proof.

We easily obtain $\gamma_{\_}1\#\cdots\#\gamma_{\_}k\#\alpha\#\gamma_{\_}{k+1}\#\cdots\#\gamma_{\_}n\lll\gamma_{\_}1\#\cdots\#\gamma_{\_}k\#\beta\#\gamma_{\_}{k+1}\#\cdots\#\gamma_{\_}n$ if $\alpha\lll\beta$ holds. Therefore, it suffices to show that for any two gqod’s $\alpha$ and $\beta$ with $(i,\alpha)\in\mathsf{GQ}(I,A)$ and $(i,\beta)\in\mathsf{GQ}(I,A)$, if $\alpha\lll\beta$ holds then $(i,\alpha)\lll(i,\beta)$ holds.

Assume that $\alpha\lll\beta$ holds, then it is obvious that $(i,\alpha)<^{\mathsf{q}}_{\_}{\infty}(i,\beta)$ holds. We show that $(i,\alpha)<^{\mathsf{q}}_{\_}j(i,\beta)$ holds for any $j$ with $j\not\leq i$. In this case, neither $(i,\alpha)$ nor $(i,\beta)$ has a $j^{\prime}$-section for any $j^{\prime}$ with $j^{\prime}\geq j$, so $(i,\alpha)\leq^{\mathsf{q}}_{\_}j(i,\beta)$ holds by $\forall$-condition, since we already have $(i,\alpha)\leq^{\mathsf{q}}_{\_}{\infty}(i,\beta)$. In the present case, it is easy to verify that $(i,\beta)\not\leq^{\mathsf{q}}_{\_}{j}(i,\alpha)$ holds.

Finally, we show that $(i,\alpha)<^{\mathsf{q}}_{\_}j(i,\beta)$ holds for any $j$ with $j\leq i$ by induction on $\#\mathsf{idx}_{j}\{(i,\alpha),(i,\beta)\}$. Consider the base case, where $\#\mathsf{idx}_{j}\{(i,\alpha),(i,\beta)\}=0$ holds, that is, $j=i$ holds. In the base case, we have $(i,\alpha)\leq^{\mathsf{q}}_{\_}i(i,\beta)$ by $\forall$-condition, since $(i,\alpha)\leq^{\mathsf{q}}_{\_}{\infty}(i,\beta)$ holds and for any $\gamma\subset_{\_}i(i,\alpha)$, $\gamma\leq^{\mathsf{q}}_{\_}i\alpha<^{\mathsf{q}}_{\_}{i}\beta<^{\mathsf{q}}_{\_}i(i,\beta)$ holds. Suppose that $(i,\beta)\leq^{\mathsf{q}}_{\_}i(i,\alpha)$ holds. If $(i,\beta)\leq^{\mathsf{q}}_{\_}i(i,\alpha)$ holds by $\exists$-condition, there is a gqod $\gamma\subset_{\_}i(i,\alpha)$ such that $(i,\beta)\leq^{\mathsf{q}}_{\_}i\gamma\leq^{\mathsf{q}}_{\_}i\alpha$ holds. Then, we have $\beta<^{\mathsf{q}}_{\_}i\alpha$, contradiction. We have a contradiction as well, if $(i,\beta)\leq^{\mathsf{q}}_{\_}i(i,\alpha)$ holds by $\forall$-condition. Therefore, $(i,\beta)\not\leq^{\mathsf{q}}_{\_}{i}(i,\alpha)$ holds.

Consider the induction step. In a way similar to the base case, we have $\gamma<^{\mathsf{q}}_{\_}j(i,\beta)$ for any $\gamma\subset_{\_}j(i,\alpha)$. Note that we have $\beta<^{\mathsf{q}}_{\_}j(i,\beta)$ by Lemma 2.13 because $(i,\beta)\in\mathsf{GQ}(I,A)$ holds. Let $j^{\prime}$ be a minimal element of $\mathsf{idx}_{j}\{(i,\alpha),(i,\beta)\}$. Since $j^{\prime}$ is an index of $(i,\alpha)$ or $(i,\beta)$, $j^{\prime}\leq i$ holds. By IH, we have $(i,\alpha)\leq^{\mathsf{q}}_{\_}{j^{\prime}}(i,\beta)$. If $(i,\beta)\leq^{\mathsf{q}}_{\_}j(i,\alpha)$ holds then we obtain a contradiction, so $(i,\alpha)<^{\mathsf{q}}_{\_}j(i,\beta)$ holds. ∎

As stated above, we have the following restricted substitution property. Note that we cannot have the full substitution property of $(\mathsf{GQ}(I,A),\lll^{=})$ because there is a counterexample. Take a substitution $\sigma$ assigning $(\rho,\rho)$ to $x$. Then, we have both $x\#x\lll(\rho,\rho)\#x$ and $(x\#x)\sigma\not\lll((\rho,\rho)\#x)\sigma$.

Lemma 3.2** (The numeral substitution property lemma).**

For any connected gqod’s $\alpha$ and $\beta$ of $\mathsf{GQ}(I,A)$ with $\alpha,\beta\not\in A$, if $\alpha\lll\beta$ holds then $\alpha\sigma\lll\beta\sigma$ holds for any numeral substitution $\sigma$.

Proof.

Verify the following by double induction on $\langle l(\alpha,\beta),\#\mathsf{idx}_{i}\{\alpha,\beta\}\rangle$: For any $i\in\tilde{I}$, any connected terms $\alpha$ and $\beta$ with $\alpha,\beta\not\in A$, if $\alpha<^{\mathsf{q}}_{\_}i\beta$ holds then $\alpha\sigma<^{\mathsf{q}}_{\_}i\beta\sigma$ holds for any numeral substitution $\sigma$. ∎

Proposition 3.3**.**

Let $l\rhd r$ be an arbitrary rule of a rewriting system $R$. For any $i\in I$ and any context $u[\ast]$, if both of $(i,u[l])$ and $(i,u[r])$ are terms of $\mathsf{GQ}(I,A)$ and $l\ggg r$ holds, then $(i,u[l])\sigma\ggg(i,u[r])\sigma$ holds for any numeral substitution $\sigma$.

Proof.

By Lemma 3.1 and Lemma 3.2. ∎

3.2 A case study with the rewrite system of Buchholz-style hydra game

Below we study the termination proof of a rewrite system version of Buchholz-style hydra game, by using our generalized quasi ordinal diagram systems. Instead of the general method for termination proofs proposed in the last subsection, we use the method relative to a given rewriting system.

The set $\mathcal{C}_{\_}i$ of contexts for any $i\in I$ is defined as follows:

$\ast$ is a connected term of $\mathcal{C}_{\_}i$. 2. 2.

if $u_{\_}i[\ast]$ is a connected term of $\mathcal{C}_{\_}i$ and $\alpha_{\_}1,\ldots,\alpha_{\_}n,\beta_{\_}1,\ldots,\beta_{\_}m$ are connected gqod’s in $\mathsf{GQ}(I,A)$, then $u_{\_}i^{\prime}[\ast]\equiv\alpha_{\_}1\#\cdots\#\alpha_{\_}n\#u_{\_}i[\ast]\#\beta_{\_}1\#\cdots\#\beta_{\_}m$ is an unconnected term of $\mathcal{C}_{\_}i$. 3. 3.

if $u_{\_}i[\ast]$ is a term of $\mathcal{C}_{\_}i$ and $(j,u_{\_}i[\rho])\in\mathsf{GQ}(I,A)$ holds with $j\geq i$, then $(j,u_{\_}i[\ast])$ is a connected term of $\mathcal{C}_{\_}i$.

Note that $u[\alpha]$ and $u_{\_}i[\alpha]$ may not be path comparable trees even if $u[\ast]$, $u_{\_}i[\ast]$ and $\alpha$ are.

An element $i$ of $I$ is a successor if the set of all $I$-elements smaller than $i$ has a maximal element. An element $\lambda$ of $I$ is a limit element if the set of all $I$-elements smaller than $\lambda$ is non-empty and does not have a maximal element.

To formulate Buchholz-style hydra game, we define the notion of segments.

Definition 3.4** (Segments).**

For any connected gqod $\alpha$ in $\mathsf{GQ}(I,A)$ and any finite subset $J$ of $I$, the segment $\alpha\upharpoonright J$ of $\alpha$ on $J$ is defined as follows: If $J$ is empty, $\alpha\upharpoonright J:=\alpha$. Assume that $J$ is not empty.

If $\alpha\in A$ holds, then $\alpha\upharpoonright J:=\alpha$. 2. 2.

Suppose that $\alpha$ is of the form $(i,\alpha_{\_}1\#\cdots\#\alpha_{\_}n)$ with $\alpha_{\_}1,\cdots,\alpha_{\_}n$ connected. If there is an element of $J$ that is not comparable with $i$ then $\alpha\upharpoonright J:=\rho$, otherwise $\alpha\upharpoonright J:=(i,\alpha_{\_}1\upharpoonright J\#\cdots\#\alpha_{\_}n\upharpoonright J)$.

For any $n\in\mathbb{N}$, let $\alpha\cdot(n+1)$ be \underbrace{\alpha\#\cdots\#\alpha}_{\_}{\text{n+1 times}}. We define $I\upharpoonright i:=\{j\in I\mid j<i\}$. A substitution $\sigma$ is a mapping from $V$ to $\mathsf{GQ}(I,A)$.

Definition 3.5** (Buchholz-style hydra game rules).**

Buchholz-style hydra game rules on $\mathsf{GQ}(I,A)$ are the following rules (1), (1)’, (2) and (3):

1. (1)

$(i,\alpha_{\_}1\#\cdots\#\alpha_{\_}n\#(\rho,\rho)\#\beta_{\_}1\#\cdots\#\beta_{\_}m)\rhd((i,\alpha_{\_}1\#\cdots\#\alpha_{\_}n\#\beta_{\_}1\#\cdots\#\beta_{\_}m)\cdot(k+1))\#\rho\cdot 2$, where $k$ is an arbitrarily chosen natural number and $n+m>0$ holds. 2. (1)’

(i,(\rho,\rho)\bigr{)}\rhd\bigl{(}(i,\rho)\cdot(k+1))\#\rho, where $k$ is an arbitrarily chosen natural number. 3. (2)

(j,\alpha_{\_}1\#\cdots\#\alpha_{\_}n\#u_{\_}i[(i,a)]\#\beta_{\_}1\#\cdots\#\beta_{\_}m)\rhd\Biggl{(}j,\alpha_{\_}1\#\cdots\#\alpha_{\_}n\#u_{\_}i\biggl{[}\Bigl{(}i^{-},u_{\_}i[(\rho,a)]\Bigr{)}\upharpoonright J\biggr{]}\#\beta_{\_}1\#\cdots\#\beta_{\_}m\Biggr{)}\#\rho,

where $a\in A$ and $j<i$ hold, $i$ is a successor, $i^{-}$ is an arbitrarily chosen maximal element of $I\upharpoonright i$, $u_{\_}i[\ast]$ is a connected term of $\mathcal{C}_{\_}i$ and $J:=\emptyset$ if $u_{\_}i[\ast]=\ast$, otherwise

J:=\{j,i^{-}\}\cup\{h\in I\mid\text{h$is a label occurring in the path between$\ast$and the root of$u_{_}i[\ast]}\}. 4. (3)

$(\lambda,a)\rhd(i,a)\#\rho$, where $\lambda$ is a limit element and $i$ is an arbitrarily chosen element of $I\upharpoonright\lambda$.

Remark 3.6**.**

Let us comment on the definition above.

• •

Choices in each of the rules are, intuitively, made by hydras after Heracles’s attacks.

• •

By restricting the initial states of hydras to the form $(\rho,\alpha_{\_}1)\#\cdots\#(\rho,\alpha_{\_}n)$, one can guarantee that at least one rule applies to the initial hydras of the games. Moreover, if rewriting in these games terminates, then the final hydra is a forest of numeral terms that have at most the depth $2$.

• •

The reason we attached one or two $\rho$’s to the right gqod’s of the rules above is that we indicate by the number of the occurrences of $\rho$’s at leaves how many times at most we applied the rules.

• •

We take the segment \Bigl{(}i^{-},u_{\_}i[(\rho,a)]\Bigr{)}\upharpoonright J at RHS in the rule (2) to make sure that the right gqod in the rule (2) belongs to $\mathsf{GQ}(I,A)$, since u_{\_}i\Bigl{[}\Bigl{(}i^{-},u_{\_}i[(\rho,a)]\Bigr{)}\Bigr{]} is not always a path comparable tree.

• •

Our hydras have labels from the well partial ordering $I$, while Buchholz’s original hydras ([4]) have labels from $\mathbb{N}\cup\{\omega\}$. Moreover, our rule (3) is more liberal than Buchholz’s corresponding rule. On the other hand, the duplication in the rule (2) of our hydra game is more restricted than the one in Buchholz’s corresponding rule. Because of this restriction, we have Lemma 3.9 below.

Definition 3.7** (Rewrite relation for Buchholz-style hydra game).**

For any two terms $\alpha$ and $\beta$ of $\mathsf{GQ}(I,A)$, $\alpha\to\beta$ holds if and only if $\alpha\equiv u[l\sigma]$ and $\beta\equiv u[r\sigma]$ hold for some context $u[\ast]$, some substitution $\sigma$ and some $l,r\in\mathsf{GQ}(I,A)$ with $l\rhd r$.

Example 3.8**.**

Consider $\mathsf{GQ}(I,V\cup\{0\})$ with $I$ defined in Example 2.2. Then, a play runs as follows.

[TABLE]

The termination proof method in this subsection consists in the following substitution property.

Lemma 3.9** (The relative substitution property lemma).**

For any substitution $\sigma$ and any two gqod’s $l$ and $r$, if both of $l\sigma$ and $r\sigma$ belong to $\mathsf{GQ}(I,A)$ and $l\rhd r$ holds, then $l\sigma\ggg r\sigma$ holds.

Proof.

We consider the rule (2) only, since the cases of the other rules are obvious. For any substitution $\sigma$ satisfying the conditions of the lemma, we show

(j,\vec{\alpha\sigma}\#u_{\_}i\sigma[(i,a\sigma)]\#\vec{\beta\sigma}\rhd\Bigl{(}j,\vec{\alpha\sigma}\#u_{\_}i\sigma\Bigl{[}\Bigl{(}\bigl{(}i^{-},u_{\_}i[(\rho,a)]\bigr{)}\upharpoonright J\Bigr{)}\sigma\Bigr{]}\#\vec{\beta\sigma}\Bigr{)}\#\rho,

where we abbreviate $\alpha_{\_}1\sigma\#\cdots\#\alpha_{\_}n\sigma$ and $\beta_{\_}1\sigma\#\cdots\#\beta_{\_}m\sigma$ as $\vec{\alpha\sigma}$ and $\vec{\beta\sigma}$, respectively. We verify the claim above by proving the following two sublemmas. The lemma follows from these sublemmas by the monotonicity. Note that one easily obtains $(\alpha\upharpoonright J)\sigma\lll^{=}\alpha\sigma$ by induction on $l(\alpha)$.

Sublemma 1. u_{\_}i\sigma\Bigl{[}\Bigl{(}\bigl{(}i^{-},u_{\_}i[(\rho,a)]\bigr{)}\upharpoonright J\Bigr{)}\sigma\Bigr{]}<^{\mathsf{q}}_{\_}hu_{\_}i\sigma[(i,a\sigma)] holds for any $h$ with $h\not\leq i^{-}$ or $h=\infty$.

By induction on the built-up of $u_{\_}i\sigma[\ast]$. If $u_{\_}i\sigma[\ast]$ is $\ast$, then one can prove this sublemma by subinduction on $\#\mathsf{idx}_{h}\{((i^{-},u_{\_}i[(\rho,a)])\upharpoonright J)\sigma,(i,a\sigma)\}$.

Suppose that $u_{\_}i\sigma[\ast]$ is $(k,\gamma_{\_}1\#\cdots\#\gamma_{\_}l\#u_{\_}i^{\prime}[\ast]\#\delta_{\_}1\#\cdots\#\delta_{\_}{l^{\prime}})$ with $u_{\_}i^{\prime}[\ast]$ connected. We abbreviate $\gamma_{\_}1\#\cdots\#\gamma_{\_}l$ and $\delta_{\_}1\#\cdots\#\delta_{\_}{l^{\prime}}$ as $\vec{\gamma}$ and $\vec{\delta}$, respectively. In addition, we set

\alpha:\equiv(k,\vec{\gamma}\#u_{\_}i^{\prime}\Bigl{[}\Bigl{(}\bigl{(}i^{-},u_{\_}i[(\rho,a)]\bigr{)}\upharpoonright J\Bigr{)}\sigma\Bigr{]}\#\vec{\delta}),\quad\beta:\equiv(k,\vec{\gamma}\#u_{\_}i^{\prime}[(i,a\sigma)]\#\vec{\delta}).

By IH, we have u_{\_}i^{\prime}\Bigl{[}\Bigl{(}\bigl{(}i^{-},u_{\_}i[(\rho,a)]\bigr{)}\upharpoonright J\Bigr{)}\sigma\Bigr{]}<^{\mathsf{q}}_{\_}hu_{\_}i^{\prime}[(i,a\sigma)] for any $h\not\leq i^{-}$. Therefore, we in particular have u_{\_}i^{\prime}\Bigl{[}\Bigl{(}\bigl{(}i^{-},u_{\_}i[(\rho,a)]\bigr{)}\upharpoonright J\Bigr{)}\sigma\Bigr{]}<^{\mathsf{q}}_{\_}ku_{\_}i^{\prime}[(i,a\sigma)], so $\alpha<^{\mathsf{q}}_{\_}{\infty}\beta$ holds. Then, it follows that $\alpha<^{\mathsf{q}}_{\_}{h}\beta$ holds for any $h\not\leq i^{-}$ with $h\not\leq k$. Since $\alpha^{\prime}<^{\mathsf{q}}_{\_}k\beta$ holds for any $\alpha^{\prime}\subset_{\_}k\alpha$, we also have $\alpha<^{\mathsf{q}}_{\_}k\beta$ by $\forall$-condition. Finally, consider $h\in I$ with $h\not\leq i^{-}$ and $h<k$. Then, for any $\alpha^{\prime}\subset_{\_}h\alpha$, we have $\alpha^{\prime}<^{\mathsf{q}}_{\_}h\beta$ also in this case. Then, by subinduction on $\#\mathsf{idx}_{h}\{\alpha,\beta\}$, it follows that $\alpha<^{\mathsf{q}}_{\_}h\beta$ holds.

Sublemma 2. u_{\_}i\sigma\Bigl{[}\Bigl{(}\bigl{(}i^{-},u_{\_}i[(\rho,a)]\bigr{)}\upharpoonright J\Bigr{)}\sigma\Bigr{]}<^{\mathsf{q}}_{\_}hu_{\_}i\sigma[(i,a\sigma)] holds for any $h\leq i^{-}$.

Take a gqod \gamma\subset_{\_}hu_{\_}i\sigma\Bigl{[}\Bigl{(}\bigl{(}i^{-},u_{\_}i[(\rho,a)]\bigr{)}\upharpoonright J\Bigr{)}\sigma\Bigr{]} with $h\leq i^{-}$ and consider the key case, where \gamma\subset_{\_}h\Bigl{(}\bigl{(}i^{-},u_{\_}i[(\rho,a)]\bigr{)}\upharpoonright J\Bigr{)}\sigma holds. Then, there is a gqod $\alpha^{\prime}$ such that $\gamma\equiv(\alpha^{\prime}\upharpoonright J)\sigma$ holds. Since we have

$(\alpha^{\prime}\upharpoonright J)\sigma\lll\alpha^{\prime}\sigma\leq_{\_}h(u_{\_}i[(\rho,a)])\sigma=u_{\_}i\sigma[(\rho,a\sigma)]\lll u_{\_}i\sigma[(i,a\sigma)]$,

$\gamma<^{\mathsf{q}}_{\_}hu_{\_}i\sigma[(i,a\sigma)]$ holds. In the other cases, one easily see $\gamma<^{\mathsf{q}}_{\_}hu_{\_}i\sigma[(i,a\sigma)]$. We obtain the present sublemma by induction on \#\mathsf{idx}_{h}\{u_{\_}i\sigma\Bigl{[}\Bigl{(}\bigl{(}i^{-},u_{\_}i[(\rho,a)]\bigr{)}\upharpoonright J\Bigr{)}\sigma\Bigr{]},u_{\_}i\sigma[(i,a\sigma)]\} and Sublemma 1. ∎

Proposition 3.10** (Termination of $\to$).**

For any substitution $\sigma$, any context $u[\ast]$ and any two gqod’s $l$ and $r$, if both of $u[l\sigma]$ and $u[r\sigma]$ belong to $\mathsf{GQ}(I,A)$ and $l\rhd r$ holds, then $u[l\sigma]\ggg u[r\sigma]$ holds.

Proof.

By Lemma 3.9 and Lemma 3.1. ∎

4 Concluding discussion and future work

We have generalized Okada-Takeuti’s quasi ordinal diagram systems and proved the well quasi orderedness of the generalized systems $(\mathsf{GQ}(I,A),\lll^{=})$, using Dershowitz-Tzameret’s tree embedding theorem with gap conditions. This gives one example of usefulness of Dershowitz-Tzameret’s tree embedding theorem. We also have examined to which extent $(\mathsf{GQ}(I,A),\lll^{=})$ can be used for termination proof methods for higher-order rewrite systems, by proposing two termination proof methods. First, it has been shown that $(\mathsf{GQ}(I,A),\lll^{=})$ satisfies not only the monotonicity property but also the numeral substitution property, which holds for the substitutions of numeral trees. Next, we have formulated the termination proof method relative to a given higher-order rewrite system, taking Buchholz-style hydra game as an example.

We conjecture that the order on $\mathsf{GQ}(I,A)$ decreases even if Buchholz-style hydra game allows to move a subtree on several leave nodes of another subtree at once. This might lead us to investigate an alternative substitution property, rather than the numeral substitution property reported in this paper. These computational phenomena will be examined in our future work. We also investigate further how to use our results of generalized quasi ordinal diagram systems for another pattern-matching-based rewrite programming. In addition, we are working on more graphic (non-tree) versions of quasi ordinal diagrams, based on the current results.