1.2 Algebraic models of structured operational semantics and variable binding

The theory of binding algebras by Plotkin et al. (1998) was presented at the international conference on rewriting systems in 1998, RTA’98, the year before their LICS paper (Fiore et al. Reference Fiore, Plotkin and Turi1999). In this sense, a connection exists between the theory of binding algebras and rewriting systems on higher-order terms.

Plotkin’s work on binding algebras can be traced back to his algebraic work on the well-known operational semantics format structural operational semantics (SOS). SOS is a system for formally specifying the computation steps in programming languages and concurrent systems and has become a fundamentally important tool in the theoretical study of programming languages. Plotkin and Turi used the algebraic semantics of the SOS format to automatically derive a coincidence between the denotational semantics and the operational semantics of the language given by SOS. The language used in this study is the GSOS format of SOS, which is given by a first-order syntax and which contains no binding syntactic structures. Therefore, the structure of universal algebra and coalgebra was used. Extending this result to cover variable binding constructs is a necessary next step. It was mentioned as a plan in Turi and Plotkin (Reference Turi and Plotkin1997), because variable binding is an important syntactic construct in that programming languages and concurrent systems that are the main targets of SOS. Therefore, the theory of binding algebras by Plotkin et al. can be regarded as a preparatory step for the study of algebraic models of SOS that use expressions with variable binding. The present study can be regarded as one by which this idea is applied not to SOS but to rewriting systems. It becomes an appropriate algebraic model for rewriting systems on higher-order terms.

1.3 Rewriting systems and operational semantics

The operational semantics given by SOS and the theory of rewriting systems where the first-order term rewriting system (TRS) is the most common formalism have several similarities: they both give relations of computation steps. However, as research fields, their work has proceeded almost independently of each other without any close connection. One reason for their lack of connection is that SOS covers a wide variety of expressions, allowing variable binding and substitutions, whereas TRS is restricted to first-order terms.

The theory of rewriting has accumulated numerous useful concepts and results. If it can be applied directly to the study of operational semantics without complicated encoding, it will be useful as a foundational theory of computation and programming languages.

As well as the substantive aim of providing a complete model for the termination of second-order CSs, the more conceptual aim of this paper is to provide a step towards bringing the theory of TRS and the theory of SOS closer together by providing algebraic models of second-order CSs.

Contributions. This paper is the fully reworked and extended version of the conference paper (Hamana Reference Hamana2005). In this paper, we establish complete algebraic semantics of second-order rewriting systems called second-order CSs.

The complete characterisation of terminating CSs provides a method of proving the termination of CSs by algebraic interpretation. The following CS $\mathcal{C}$ for conversion into prenex normal form, that is, pushing quantifiers outside, is a typical example of rewrite rules that require the feature of variable binding (van de Pol, Reference van de Pol1996):

\begin{equation*}\begin{array}[h]{llllll} P \wedge \forall(x.Q[x]) &\!\Rightarrow\!& \forall(x.P \wedge Q[x]) \qquad& \forall(x.Q[x])\wedge P &\!\Rightarrow\!& \forall(x.Q[x] \wedge P) \\ P \vee \forall(x.Q[x]) &\!\Rightarrow\!& \forall(x.P \vee Q[x]) & \forall(x.Q[x])\vee P &\!\Rightarrow\!& \forall(x.Q[x] \vee P) \\ P \wedge \exists(x.Q[x]) &\!\Rightarrow\!& \exists(x.P \wedge Q[x]) & \exists(x.Q[x])\wedge P &\!\Rightarrow\!& \exists(x.Q[x] \wedge P) \\ P \vee \exists(x.Q[x]) &\!\Rightarrow\!& \exists(x.P \vee Q[x]) & \exists(x.Q[x])\vee P &\!\Rightarrow\!& \exists(x.Q[x] \vee P) \\ \neg \forall(x. Q[x]) &\!\Rightarrow\!& \exists(x. \neg(Q[x])) & \neg \exists(x. Q[x]) &\!\Rightarrow\!& \forall(x. \neg(Q[x]))\end{array}\end{equation*}

Existing proof methods in the theory of higher-order rewriting to the CS $\mathcal{C}$ are not straightforwardly applicable (Jouannaud and Rubio, Reference Jouannaud and Rubio2001). Alternatively, they require consideration of an involved function space to interpret binders (van de Pol 1996; Reference van de Pol1994). The present paper provides a simpler method of showing termination of CS such as $\mathcal{C}$ , as shown in Example 9.7.

Organisation. This paper is organised as follows. We first review the technical background of our semantics in Section 2. We formally define second-order CSs in Section 3. Section 4 gives algebraic semantics of CS’ syntax and valuations. Section 5 gives algebraic semantics of CS’ rewriting. Section 6 gives algebraic semantics of CS’ meta-rewriting. Section 7 shows that a known model of higher-order rewrite rules given by hereditary monotone functionals is an instance of our algebraic models. Finally, in Section 9, we investigate the termination of binding CSs and show examples of termination proofs using algebraic models.

2.1 Introduction to second-order abstract syntax

2.1.1 Object and metavariables

Second-order CSs are founded on second-order abstract syntax. We introduce second-order abstract syntax. We first explain the distinction between object variables and metavariables, which is important for our modelling of CSs. For example, consider a $\lambda$ -term

\begin{equation*} \lambda x. (M y) \end{equation*}

in a certain mathematical context. Here ‘x’ and ‘y’ are $\lambda$ -calculus variables (i.e. object-level variables, because now the $\lambda$ -calculus is the object system), while at the level of text, ‘M’ is a meta-level variable. We distinguish ‘object-level variables’ and ‘metavariables’ in this sense and call ‘object-level variables’ simply ‘variables’.

2.1.2 Metavariables with arities

Metavariables have also the notion of arities. For example, writing

(1) \begin{equation} \lambda x. (M[x]\; y)\end{equation}

we mean that M may contain the variable x. In this case, we say that the metavariable M has arity 1. We formalise this notion of metavariables in this paper.

2.1.3 Function symbols with binding arities

Second-order abstract syntax provides a general framework for syntax with variable binding by a signature consisting of ‘function symbols with binding arities’. In second-order abstract syntax, the $\lambda$ -abstraction is not a primitive construct. The above $\lambda$ -term is encoded by using second-order abstract syntax as follows:

\begin{equation*} \textsf{abs}(x. \textsf{app}(M[x], y))\end{equation*}

where $x.-$ is the primitive variable binding construct of second-order abstract syntax. Here we assume that $\textsf{app}$ is a function symbol with binding arity $<0,0>$ , which means that $\textsf{app}$ takes two arguments and each argument binds no variable, and $\textsf{abs}$ is a function symbol with binding arity $<1>$ , which means that it takes one argument and the argument has one variable binding. We call a term like $\textsf{abs}(x. \textsf{app}(M[x], y))$ a meta-term meaning that a term involving metavariables. Likewise, using a function symbol $\lambda$ with binding arity $<1>$ and an infix function symbol $@$ with arity $<0,0>$ , we can construct a meta-term $\lambda(x. M[x] @ y)$ , which is closer to the familiar notation (cf. Example 3.2).

2.2 The presheaf category ${\textbf{Set}^\mathbb{F}}$

In modelling second-order abstract syntax, we use a framework of categorical algebra using presheaves. First we explain presheaves used in this paper. The category $\mathbb{F}$ has finite cardinals $n=\{{1,\ldots,n}\}$ (n is possibly 0) as objects, and all functions between them as arrows $n\to n'$ .

The category ${\textbf{Set}^\mathbb{F}}$ plays a central role in the algebraic models of syntax with variable binding (Fiore et al. Reference Fiore, Plotkin and Turi1999; Tanaka and Power, Reference Tanaka and Power2006). The objects of it are functors $\mathbb{F} \to \textbf{Set}$ and the arrows are natural transformations between them. An object A of ${\textbf{Set}^\mathbb{F}}$ is called a presheaf and is written as $A\in{\textbf{Set}^\mathbb{F}}$ .

A map between presheaves $A,B \in {\textbf{Set}^\mathbb{F}}$ is a natural transformation $f : A \rightarrow B$ , that is, a family of functions of the form $f(n) : A(n) \rightarrow B(n)$ parameterised by all $n\in\mathbb{N}$ that makes the naturality diagram commute

2.3 Algebraic model of abstract syntax and variable binding

In their seminal paper, Fiore et al. (Reference Fiore, Plotkin and Turi1999) investigated algebraic models of abstract syntax involving variable binding. A typical example of such a syntax is the syntax for untyped $\lambda$ -terms:

\begin{equation*} \frac{}{x_1,\ldots, x_n \,\vdash x_i } \qquad \frac{x_1,\ldots, x_n \,\vdash t x_1,\ldots, x_n \,\vdash s}{x_1,\ldots, x_n \,\vdash t @ s} \\[.5em] \frac{x_1,\ldots, x_n, x_{n+1} \,\vdash t}{x_1,\ldots, x_n \,\vdash \lambda (x_{n+1} . t)}\end{equation*}

This is an abstract syntax generated by three constructors, that is, the variable former, the application $@$ and the abstraction $\lambda$ . The point is that $@$ is a binary function symbol, but $\lambda$ is not merely a unary function symbol. It also makes the variable $x_{n+1}$ bound and decreases the context. This can be formulated by the function symbols with binding arities given in Section 2.1.3. In order to model the phenomenon of variable binding generally (not only for $\lambda$ -terms), Fiore, Plotkin and Turi took the presheaf category ${\textbf{Set}^\mathbb{F}}$ to be the universe of discourse. This is regarded as the category of object variables (regarded as contexts) by the method of de Bruijn index/level (i.e. natural numbers) and their renamings. A main result in Fiore et al. (Reference Fiore, Plotkin and Turi1999) is that abstract syntax with variable binding is characterised as an initial algebra of suitable endofunctor generated by a signature (e.g. for $\lambda$ -terms). Now a function symbol with binding arity, denoted by $f:\langle n_1,\ldots,n_l\rangle$ , has l arguments and binds $n_i$ variables in the i-th argument $(1 \le i \le l)$ . A signature $\Sigma$ is a set $\Sigma$ of function symbols with binding arities.

For example, for abstract syntax of $\lambda$ -terms, we take a signature $\Sigma$ consisting of $\lambda:\langle 1 \rangle$ and an infix function symbol $@ : \langle 0,0 \rangle$ , as described in Section 2.1.3. The corresponding signature endofunctor $\Sigma_\lambda$ on ${\textbf{Set}^\mathbb{F}}$ is $\Sigma_\lambda(A) = \mathrm{V} + A\!\times\! A + \delta A$ where each summand corresponds to the arity of function symbol where the context extension is defined by $(\delta A)(n) = A(n+1)$ , and the presheaf $\mathrm{V} \in {\textbf{Set}^\mathbb{F}}$ of variables is $\mathrm{V}(n) = \{{1,\ldots,n}\} $ .

In general, given a signature $\Sigma$ , we also denote by $\Sigma$ the corresponding signature endofunctor ^{Footnote 1} defined like $\Sigma_\lambda$ (more precisely, see Definition 4.1). A $\Sigma$ -algebra is a pair $(A,\alpha)$ consisting of a presheaf A and a map $\alpha : \Sigma A \to A$ , called an algebra structure that provides the interpretations of constructors. An initial $\Sigma_\lambda$ -algebra $(\Lambda,\textsf{in})$ can be constructed inductively as the presheaf $\Lambda$ of all $\lambda$ -terms modulo $\alpha$ -equivalence with free variable renaming. The initial algebra directly models the abstract syntax with binding, namely

\begin{equation*} \mathrm{a\, judgment}\, n \,\vdash t \;\; \mathrm{is\, modelled\, as}\, \;\; t \in \Lambda(n),\\\end{equation*}

and renaming of free variables $\rho : n \to n'$ in a $\lambda$ -term is modelled by the presheaf action $\Lambda(\rho):\Lambda(n)\to\Lambda(n')$ . Under the method of de Bruijn levels, n means the set of variables from 1 to n. This is a generic way of modelling abstract syntax with binding with respect to a signature functor $\Sigma$ . However, the method is limited to modelling of object-level abstract syntax.

2.4 Free $\Sigma$ -monoids: second-order abstract syntax with metavariables

Not only object-level abstract syntax, how can we deal with metavariables and the distinction of substitutions for object and metavariables in the algebraic model of syntax with binding? This problem was explored in Hamana (Reference Hamana2004); Fiore (Reference Fiore2008) and a clear answer has been obtained.

Given a signature functor $\Sigma$ , a $\Sigma$ -monoid (Fiore et al. Reference Fiore, Plotkin and Turi1999) is a $\Sigma$ -algebra $(A,\alpha)$ with a monoid structure

that is compatible with the algebra structure in the monoidal category $({\textbf{Set}^\mathbb{F}},\bullet,\mathrm{V})$ ^{Footnote 2} . The unit $\nu$ models the variable former, and the multiplication $\mu$ models substitution for object variables, where the monoidal product $\bullet$ gives the arity of substitution.

An important structure is a free $\Sigma$ -monoid generated by an arbitrary presheaf Z, where generators Z is regarded as the presheaf of metavariables. A free $\Sigma$ -monoid over $Z\in{\textbf{Set}^\mathbb{F}}$ , denoted by $\mathrm{M}_\Sigma Z$ , is constructed inductively as an initial $(\mathrm{V}+\Sigma+Z\bullet-)$ -algebra, which gives the language involving binding and metavariables. Terms of this language are expressed as the following BNF:

(2) \begin{align} {\mathrm{M}_\Sigma} {Z}(n) \ni \; &t ::= x \| f(\, n\!+\!1.\ldots.n\!+\!i_1. t_1,\; \ldots, n\!+\!1.\ldots.n\!+\!i_m.t_m \,) \| M[t_1,\ldots,t_m] \end{align}

\begin{align} Z(m) \ni \; &M \nonumber\end{align}

where $x\in \{{1,\ldots,n}\}$ and each $f \in \Sigma$ is a function symbol that binds $i_j$ variables at the j-th argument. This characterisation shows that the functor $\mathrm{V}+\Sigma$ models syntax with binding (as in Section 2.1.1) and the functor $Z\bullet-$ models the syntactic construct of metavariables represented as a term

\begin{equation*}M[{t_1,\ldots,t_m}]\end{equation*}

where $M \in Z(m)$ is a metavariable and the index m, called also arity, which denotes possible free variables $1,\ldots, l$ appearing in a term substituted for M. Terms $t_1,\ldots,t_m$ are replacements of the free variables $1,\ldots, m$ after instantiating M. For example, a substitution that replaces a metavariable M with a term $1 @ 1$ (where 1 is a free variable) is formulated as map $\theta$ from the presheaf Z of metavariables to $\mathrm{M}_\Sigma Z$ , which maps the metavariable M as $\theta (M) = 1 @ 1$ . Then applying it to a term $\lambda(x. \;M[x]\; @\, y)$

(3) \begin{equation} \theta^\sharp(\lambda(x. \;M[x]\; @\, y)) = \lambda(x. \;(x@x)\; @\, y) \end{equation}

is a substitution process. The freeness of $\mathrm{M}_\Sigma Z$ states that given $\theta$ , there uniquely exists the extension $\theta^\sharp$ to a $\Sigma$ -monoid morphism that makes the following diagram commute:

The general form of freeness is stated for an arbitrary $\Sigma$ -monoid A. To consider the syntactic case, we take $A = \mathrm{M}_\Sigma Z$ . Then, the notion of substitution of metavariables appears. This is syntactically understood as that $\theta$ is an assignment for substitution and $\theta^\sharp$ is the corresponding substitution of terms for metavariables. For (3), we put the metavariable $M \in Z(1)$ .

Notation 2.2. We denote by $f({n+\overrightarrow{i_1}}.t_1,\ldots,{n+\overrightarrow{i_m}}.t_m)$ to mean

\begin{equation*}f(\; n\!+\!1 \cdots n\!+\!i_1. t_1, \; \ldots, \;n\!+\!1\cdots n\!+\!i_m. t_m \;).\end{equation*}

We abbreviate the words left-hand side as ‘lhs’, right-hand side as ‘rhs’, first-order as ‘FO’ and higher-order as ‘HO’.

A binary relation $>$ is well-founded if there is no infinite decreasing sequences $a_1 > a_2 > \cdots$ .

4.1 Algebra of meta-terms

We define the functor $\delta : {\textbf{Set}^\mathbb{F}} \to {\textbf{Set}^\mathbb{F}}$ for context extension by

\begin{equation*}(\delta A)(n) = A(n+1), \quad (\delta A)(\rho) = A(\rho + \mathrm{id}_1)\end{equation*}

for $A \in {\textbf{Set}^\mathbb{F}}, n \in \mathbb{F}, \rho : m \to n$ in $\mathbb{F}$ , and a presheaf $\mathrm{V} \in {\textbf{Set}^\mathbb{F}}$ called the presheaf of variables by

\begin{equation*}\mathrm{V}(n) = \{{1,\ldots,n}\} ; \quad \mathrm{V}(\rho) = \rho.\end{equation*}

The meaning of this definition is that each component $\mathrm{V}(n) = \{{1,\ldots,n}\}$ gives the set of (de Bruijn) variables from 1 to n, and $\mathrm{V}(\rho)$ gives a renaming between them.

Definition 4.1. To a signature $\Sigma$ , we associate the signature functor $\Sigma : {\textbf{Set}^\mathbb{F}} \to {\textbf{Set}^\mathbb{F}}$ given by

\begin{equation*}\Sigma A {\stackrel{{\it def}}{=}} \coprod_{f :<n_1,\ldots,n_l>\in \Sigma} \prod_{1 \le i \le l}\delta^{n_i} A.\end{equation*}

A $\Sigma$ -algebra is an algebra of the functor $\Sigma$ . Namely, a $\Sigma$ -algebra is a pair $(A,\alpha)$ consisting of a presheaf $A \in {\textbf{Set}^\mathbb{F}}$ , called a carrier, and a map $\alpha=[f^A]_{f\in\Sigma} : \Sigma A \rightarrow A$ called the algebra structure, where $f^A$ is a map of ${\textbf{Set}^\mathbb{F}}$

\begin{equation*}f^A : \delta^{n_1} A \!\times\! \ldots \!\times\! \delta^{n_l} A \rightarrow A\end{equation*}

called an operation, defined for each function symbol $f : \langle n_1,\ldots,n_l\rangle \in\Sigma$ , where $[ \; ]$ denotes the copair of coproducts.

Remark 4.2. For each $n\in\mathbb{F}$ , the component of an operation $f^A$ at n is a function

\begin{equation*}f^A_n : A(n+n_1) \!\times\! \cdots \!\times\! A(n+n_l) \rightarrow A(n)\end{equation*}

Definition 4.3. A ( $\mathrm{V}\!+\!\Sigma$ )-algebra $(A,[\nu,\alpha])$ is an algebra of the functor $(\mathrm{V}\!+\!\Sigma) : {\textbf{Set}^\mathbb{F}} \to {\textbf{Set}^\mathbb{F}}$ . Namely, it consists of a $\Sigma$ -algebra $(A,\alpha)$ and a map of ${\textbf{Set}^\mathbb{F}}$

\begin{equation*}\nu : \mathrm{V} \to A.\end{equation*}

called a unit.

Example 4.4. For the signature $\Sigma_\lambda$ of the $\lambda$ -calculus given in Example 3.2, the presheaf $\Lambda$ of all $\lambda$ -terms is defined by

\begin{equation*}\Lambda(n) =\{{t \| \;\triangleright\; n \,\vdash \,\; t }\}\end{equation*}

and for $\rho : m \to n$ in $\mathbb{F}$ , $\Lambda(\rho) : \Lambda(m) \to \Lambda(n)$ is a renaming of $\lambda$ -term by $\rho$ , where each free variable $i \in \{{1,\ldots, m}\}$ is replaced with $\rho(i)$ . It forms a $(\mathrm{V}\!+\!\Sigma_\lambda)$ -algebra by giving the operations

These operations correspond to the constructors of variables, applications and abstractions.

Definition 4.5. A $\Sigma$ -monoid $(A,\alpha,\nu,\mu)$ is a $\Sigma$ -algebra $(A,\alpha)$ equipped with a unit $\nu : \mathrm{V} \to A$ and a family of functions, called a multiplication,

\begin{equation*}\mu^{(n)}_m : A(n)\!\times\! A(m)^n \rightarrow A(m)\end{equation*}

which is natural in $m\in\mathbb{F}$ and extra-natural in $n\in\mathbb{F}$ , and satisfies the following axioms:

where $f:\langle k_1,\ldots,k_l\rangle \in\Sigma,\; \overrightarrow{b}=b_1,\ldots,b_n$ and ${up}_m^{n} {\stackrel{{\it def}}{=}} A(\mathrm{up}_m^{n})$ , where $m \le n$ and a map $\mathrm{up}_m^{n} : m \to n$ in $\mathbb{F}$ is an injection defined by $j\mapsto j$ . Here, an element in the product $A(n)\!\times\! A(m)^n$ is denoted by $(a;\, b_1,\ldots,b_n)$ , or simply $(a;\, \overrightarrow{b})$ .

A $\Sigma$ -monoid models term and substitution structures.

commutes.

Another way to define $\Sigma$ -monoid using a monoidal structure on ${\textbf{Set}^\mathbb{F}}$ is given as follows, which is the original definition (Fiore et al., Reference Fiore, Plotkin and Turi1999) of $\Sigma$ -monoid.

Definition 4.7 $({\textbf{Set}^\mathbb{F}}, \bullet, \mathrm{V})$ forms a monoidal category (Mac Lane, Reference Mac Lane1971), where the ‘substitution’ monoidal product $\bullet$ is defined as follows. For presheaves A and B,

\begin{equation*}(A \bullet B)(n) {\stackrel{{\it def}}{=}} \left(\coprod_{m\in\mathbb{N}} A(m) \!\times\! B(n)^m\right)/\sim\end{equation*}

where $\sim$ is the equivalence relation generated by $(t;\; u_{\rho 1},\ldots,u_{\rho m}) \sim (A(\rho)(t);\; u_1,\ldots,u_l)$ for $\rho:m\to l \in \mathbb{F}$ .

Let $\Sigma$ be a signature functor. It has a canonical strength $st : \Sigma(A) \bullet A \to \Sigma(A\bullet A)$ (Tanaka and Power, Reference Tanaka and Power2006, Theorem 6.3) (Fiore, Reference Fiore2008, Corollary 7). A $\Sigma$ -monoid $A=(A,\,\alpha,\,\nu,\,\mu)$ consists of a monoid object $(A,\nu:\mathrm{V}\to A, \mu : A\bullet A \to A)$ in the monoidal category $({\textbf{Set}^\mathbb{F}}, \bullet, \mathrm{V})$ with a $\Sigma$ -algebra $\alpha:\Sigma A \to A$ such that the following commutes:

In Definition 4.5, a unit $\nu : \mathrm{V} \to A$ can be understood as an (interpretation) map of object variables, which embeds object variables to A. A multiplication $\mu$ can be understood as a map of (interpreted) substitution operation in A. Then, the axioms have the following intuitive reading.

1. (i) This axiom means replacing a variable i with the i-th element $b_i$ in $\overrightarrow{b}$ .

2. (ii) This axiom says that substituting the (interpretation of) variables $\nu(1),\ldots,\nu(n)$ in A for variables $1,\ldots,n$ does not affect the element.

3. (iii) This axiom is the associativity of substitutions, that is, a version of substitution lemma.

4. (iv) This $\Sigma$ -monoid axiom says that the (interpretation of) substitution $\mu$ is pushed into the (interpretation of) term structure.

The two ways of defining $\Sigma$ -monoids are equivalent. In a termination proof of CS, we often need to give a concrete example of $\Sigma$ -monoids. For it, Definition 4.5 of $\Sigma$ -monoids is more convenient than the original Definition 4.7. In theory, Definition 4.7 is more convenient. For instance, we will use it to construct a free $\Sigma$ -monoid in Theorem 4.13. Hereafter, we use both descriptions of $\Sigma$ -monoids.

Concretely,

\begin{equation*}h_n(f^A_n(a_1,\ldots,a_l)) = f^B_n(h_{n+i_1}(a_1),\ldots,h_{n+i_l}(a_l))\end{equation*}

for all $f:\langle i_1,\ldots,i_l\rangle\in\Sigma,\; n\in\mathbb{N},\; a_1,\ldots,a_l \in A(n)$ . This defines the category $\Sigma$ -alg of $\Sigma$ -algebras.

A morphism of $\Sigma$ -monoids $h:(A,\nu^A,\mu^A) \rightarrow (B,\nu^B,\mu^B)$ is a $\Sigma$ -algebra homomorphism that is also a monoid morphism, that is, it satisfies the condition of homomorphism and the following

\begin{align*}h_n(\nu^A_n(i)) &= \nu^B_n(i)\\h_n(\mu^{A(m)}_n(a;\overrightarrow{b})) &= \mu^{B\,(m)}_{n}(h_m(a);\; h_n(b_1),\ldots,h_n(b_m)).\end{align*}

This defines the category $\Sigma$ -Mon of $\Sigma$ -monoids.

Example 4.10. Using the signature $\Sigma_\lambda$ in Example 4.4, the presheaf $\Lambda$ of $\lambda$ -terms forms a $\Sigma_\lambda$ -monoid $(\Lambda,\nu,\mu)$ as follows. Since $\Lambda$ is a $(\mathrm{V}+\Sigma_\lambda)$ -algebra, it has the unit $\nu$ (given in Example 4.4). The multiplication $\mu$ is defined by

\begin{equation*}\begin{array}{lllllllll}&\mu_n( i;\, \overrightarrow{t}) &=& {t_i \qquad(i \in n)}\\&\mu_n( s_1 @ s_2 ;\, \overrightarrow{t} ) &=& \mu_n(s_1; \overrightarrow{t}) \;@\; \mu_n(s_2 ; \overrightarrow{t})\\&\mu_n( \lambda (n+1.\, s) ;\, \overrightarrow{t} ) &=& \lambda (n+1.\, \mu_{n+1}(s;\, \overrightarrow{t},n+1)).\end{array}\end{equation*}

This $\mu$ is a substitution of a $\lambda$ -term. In the ordinary notation,

\begin{equation*}\mu_n(t,\overrightarrow{s}) = t[1:=s_1,\ldots,n:=s_n],\end{equation*}

where $1,\ldots,n$ are variables in de Bruijn level notation. The axioms of $\Sigma$ -monoid are satisfied, because $\mu$ is the substitution operation. This is an instructive concrete example to understand the meaning of axioms. In this case, the presheaf $\Lambda$ is given syntactically, and all operations on $\Lambda$ and $\mu$ are also given syntactically, that is, the constructors of $\lambda$ -terms and the substitution operation.

The presheaf ${\mathrm{T}_\Sigma \!\mathrm{V}}\in{\textbf{Set}^\mathbb{F}}$ of all terms is defined by

\begin{align*} {\mathrm{T}_\Sigma \!\mathrm{V}}(n) &= \{{ t \| \;\triangleright\; n \,\vdash \,\; t}\}\\ {\mathrm{T}_\Sigma \!\mathrm{V}} (\rho)(i) &= \rho(i) \quad (1 \le i \le m)\\ {\mathrm{T}_\Sigma \!\mathrm{V}}(\rho)(f(m\!+\!\overrightarrow{i_1}.t_1,\ldots,m\!+\!\overrightarrow{i_l}.t_l)) &= f(m\!+\!\overrightarrow{i_1}.{\mathrm{T}_\Sigma \!\mathrm{V}}(\rho+\mathrm{id}_{i_1})(t_1),\ldots, m\!+\!\overrightarrow{i_l}.{\mathrm{T}_\Sigma \!\mathrm{V}}(\rho+\mathrm{id}_{i_l})(t_l))\end{align*}

for $f : \langle i_1,\ldots,i_l\rangle \in \Sigma,\; \rho:m\to n$ in $\mathbb{F}$ , which gives renaming of variables in a term.

Proof. An initial $(\mathrm{V}\!+\!\Sigma)$ -algebra is constructed by the colimit of the $\omega$ -chain $0 \to (\mathrm{V}\!+\!\Sigma)\, 0 \to {(\mathrm{V}\!+\!\Sigma)}^2 0 \to \cdots$ (Adamek, Reference Adamek1974). These construction steps correspond to derivations of terms by term forming rules; hence, their union ${\mathrm{T}_\Sigma \!\mathrm{V}}$ gives the object part of the colimit. The arrow part of the colimit is associated with substitution. The associated algebra structure is given as follows: the map $\nu \;:\; \mathrm{V} \rightarrow {\mathrm{T}_\Sigma \!\mathrm{V}}$ is given by

For every $f\in \Sigma$ with biding arity $\langle i_1,\ldots,i_l \rangle$ , the map $f^{\mathrm{T}_\Sigma \!\mathrm{V}} \;:\; \delta^{i_1} {\mathrm{T}_\Sigma \!\mathrm{V}} \!\times\! \cdots \!\times\! \delta^{i_l} {\mathrm{T}_\Sigma \!\mathrm{V}} \rightarrow {\mathrm{T}_\Sigma \!\mathrm{V}}$ in ${\textbf{Set}^\mathbb{F}}$ is given by

In Fiore et al. (Reference Fiore, Plotkin and Turi1999, Theorem 2.1), the ‘syntactic algebra’ is constructed as an initial $(\mathrm{V}\!+\!\Sigma)$ -algebra, which is nothing but this $(\mathrm{V}\!+\!\Sigma)$ -algebra $({\mathrm{T}_\Sigma \!\mathrm{V}}, [\nu,[f^{\mathrm{T}_\Sigma}]_{f\in\Sigma}])$ .

where the functor $|-|= - \circ J$ using the inclusion $J :\mathbb{N} \to \mathbb{F}$ gives the underlying indexed set of a presheaf. Its left adjoint $\underline{(-)}$ is the left Kan extension along J, calculated (Hamana, Reference Hamana2004) as $\underline{Z}(n) = \coprod_{k\in\mathbb{N}} \mathbb{F}(k,n) \!\times\! Z(k)$ for $Z\in\textbf{Set}^\mathbb{N}$ .

Therefore, we have a way to construct a presheaf $\underline{Z}\in{\textbf{Set}^\mathbb{F}}$ from a given $\mathbb{N}$ -indexed set Z of metavariables. Using the adjointness, a map $\phi: Z \to |A|$ in $\textbf{Set}^\mathbb{N}$ for $A\in {\textbf{Set}^\mathbb{F}}$ induces a map $\hat\phi: \underline{Z} \to A$ in ${\textbf{Set}^\mathbb{F}}$ . We also regarded this as a way to construct a map of presheaves from an assignment $\phi$ for metavariables in Section 4.2.

Let Z be an arbitrary $\mathbb{N}$ -indexed set of metavariables. Given a signature $\Sigma$ , the presheaf ${\mathrm{M}_\Sigma\underline{Z}}$ of meta-terms over Z is defined by

\begin{align*} {\mathrm{M}_\Sigma\underline{Z}}(n) &= \{{ t \| Z \;\triangleright\; n \,\vdash \,\; t}\} \end{align*}

and for $\rho:m\to n$ in $\mathbb{F}$ defined by

\begin{align*} {\mathrm{M}_\Sigma\underline{Z}}(\rho)(i) &= \rho(i)\\ {\mathrm{M}_\Sigma\underline{Z}}(\rho)(f(n\!+\!\overrightarrow{i_1}.t_1,\ldots,n\!+\!\overrightarrow{i_l}.t_l)) &= f(n\!+\!\overrightarrow{i_1}.{\mathrm{M}_\Sigma\underline{Z}}(\rho)(t_1),\ldots,n\!+\!\overrightarrow{i_l}.{\mathrm{M}_\Sigma\underline{Z}}(\rho)(t_l))\\ {\mathrm{M}_\Sigma\underline{Z}}(\rho)(M[t_1,\ldots,t_l]) &= M[{\mathrm{M}_\Sigma\underline{Z}}(\rho)(t_1),\ldots,{\mathrm{M}_\Sigma\underline{Z}}(\rho)(t_l)].\end{align*}

Proof. Due to Hamana (Reference Hamana2004). For ${Z}\in\textbf{Set}^\mathbb{N}$ , a free $\Sigma$ -monoid $({\mathrm{M}_\Sigma\underline{Z}}, [f_{\mathrm{M}_\Sigma}]_{f\in\Sigma}, \nu, \mu)$ over Z is constructed as an initial $(\mathrm{V}+\Sigma+\underline{Z}\bullet-)$ -algebra $({\mathrm{M}_\Sigma\underline{Z}}, \nu, [f_{\mathrm{M}_\Sigma}]_{f\in\Sigma}, \sigma)$ . For every $f\in \Sigma$ with binding arity $\langle i_1,\ldots,i_l\rangle$ , the map $f^{\mathrm{M}_\Sigma\underline{Z}} : \delta^{i_1} {\mathrm{M}_\Sigma\underline{Z}} \!\times\! \cdots \!\times\! \delta^{i_l} {\mathrm{M}_\Sigma\underline{Z}} \rightarrow {\mathrm{M}_\Sigma\underline{Z}}$ in ${\textbf{Set}^\mathbb{F}}$ is given by

The unit $\nu$ is given by $\nu_n : i\mapsto i$ . The map $\sigma : \underline{Z}\bullet{\mathrm{M}_\Sigma\underline{Z}} \rightarrow {\mathrm{M}_\Sigma\underline{Z}}$ is given by

The map ${\eta_{\underline{Z}}} : \underline{Z} \rightarrow {\mathrm{M}_\Sigma\underline{Z}}$ is given by

\begin{equation*}\eta_{\underline{Z},\; m} : (\xi,Z) \mapsto Z[\xi(1),\ldots,\xi(m)].\end{equation*}

The multiplication $\mu$ is given as the substitution for variables, which makes the diagram

commute.

4.2 Algebraic characterisation of substitution for metavariables

We have shown that the meta-terms form a free $\Sigma$ -monoid. Formally, given $Z\in\textbf{Set}^\mathbb{N}$ , ${\mathrm{M}_\Sigma\underline{Z}}$ is a free $\Sigma$ -monoid over $\underline{Z} \in {\textbf{Set}^\mathbb{F}}$ . Namely, for an arbitrary $\Sigma$ -monoid $(A,\alpha,\nu^A,\mu^A)$ and $\phi : Z \to |A|$ , there exists a unique $\Sigma$ -monoid morphism $\phi^\sharp$ that makes the diagram

commute.

We have seen that an $\mathbb{N}$ -indexed function $\phi: Z \to |A|$ induces a map $\hat{\phi} : \underline{{Z}} \to A$ of ${\textbf{Set}^\mathbb{F}}$ . It is also extended to a $\Sigma$ -monoid morphism $\phi^\sharp : {\mathrm{M}_\Sigma\underline{Z}} \to A$ defined by

(4) \begin{equation}\begin{split}{\phi}_{n}^\sharp({i}) &= \nu^A_n(i)\\{\phi}_{n}^\sharp({f(n+\overrightarrow{i_1} . t_1,\ldots, n+\overrightarrow{i_l}.t_l)})&= f^A_{n}({\phi}_{n+{i_1}}^\sharp({t_1}),\ldots, {\phi}_{n+{i_l}}^\sharp({t_l}))\\ {\phi}_{n}^\sharp({M[{\overrightarrow{t}}]}) &= \mu^A_{n}(\phi_m(M);\; {\phi}_{n}^\sharp({t_1}),\ldots,{\phi}_{n}^\sharp({t_m}))\quad \text{for }M\in Z(m).\end{split}\end{equation}

This definition gives the meaning of a meta-term in a $\Sigma$ -monoid A by structural recursion. Note that it is not the standard structural recursion because the indices of $\phi$ vary in the recursive calls. The meaning of a variable is obtained using $\nu^A$ , which is the interpretation of variable former, a function symbol f is interpreted as $f^A$ and a meta-application is interpreted as follows. Firstly, the value of a metavariable M is obtained using the map $\phi$ , and secondly, $\mu^A$ replaces semantically free m variables $1,\ldots,m$ with the meanings of $t_1,\ldots,t_m$ obtained by applying $\phi^\sharp$ .

The extension captures the notion of syntactic substitutions for metavariables, where a map $\phi$ is regarded as an assignment of values for metavariables. We formulate substitutions along this idea.

Definition 4.15. Let Z be an $\mathbb{N}$ -indexed set of metavariables, $A\in {\textbf{Set}^\mathbb{F}}$ . An assignment $\theta$ denoted by

\begin{equation*}\theta : {Z} \rightarrow A,\end{equation*}

is an $\mathbb{N}$ -indexed function $\theta : {Z} \to | A|$ . We may denote an assignment $\theta$ by the notation

\begin{equation*}\theta = [M_1 \mapsto a_1 , \ldots, M_m \mapsto a_m]\end{equation*}

which assigns $a_i$ to $M_i$ for $i=1,\ldots,m$ .

Lemma 4.16. Let $k\in\mathbb{N}$ . If $(A,[\nu^A,[f^A]_{f\in\Sigma}])$ is a $(\mathrm{V}\!+\!\Sigma)$ -algebra, so is $(\delta^{k} A,[\nu^{\delta^{k}},[f^{\delta^{k}}]_{f\in\Sigma}])$ , where $\nu^{\delta^{k} A}_n{\stackrel{{\it def}}{=}} \nu^{A}_{n+k},\;f^{\delta^{k} A}_n {\stackrel{{\it def}}{=}} f^{A}_{n+k}$ . Moreover, if $(A,[f^A]_{f\in\Sigma},\nu^A,\mu^A)$ is a $\Sigma$ -monoid, so is $(A,[f^{\delta^{k} A}]_{f\in\Sigma},\nu^{\delta^{k} A},\mu^{\delta^{k} A})$ , where

\begin{align*}\mu_n^{\delta^{k} A} : \delta^{k} A(m) \!\times\! \delta^{k} A(n)^m &\to \delta^{k} A(n)\\a \quad;\; b_1,\ldots,b_m &\mapsto \mu^A_{n+k}(a\,;\,b_1,\ldots,b_m, \nu_{n+k}^A(n+1),\ldots,\nu_{n+k}^A(n+k)).\end{align*}

We now consider the case of assignment $\theta : Z \rightarrow \delta^k{\mathrm{T}_\Sigma \!\mathrm{V}}$ . It assigns a term to each metavariable of arity n as

where k is the number of additional possible free variables other than $1,\ldots,n$ in the results.

Additional free variables generated by an assignment $\theta$ are never captured by any binder. For example, let M be a 0-ary metavariable, and $\theta : Z \rightarrow \delta{\mathrm{T}_\Sigma \!\mathrm{V}};\; \theta_0:M\mapsto c(1)$ . The free variable 1 in c(1) is never captured by applying the substitution $\theta$ , which is automatically shifted to make it free to follow the method of de Bruijn levels, for example,

\begin{align*} \theta^\sharp_0(\lambda(1. M)) &= \lambda(1. \theta^\sharp_1(M)) = \lambda(1. \mu_1^{\delta{\mathrm{T}_\Sigma \!\mathrm{V}}}(\theta_0(M);)) = \lambda(1.\mu_2^{{\mathrm{T}_\Sigma \!\mathrm{V}}}(\theta_0(M);\;\nu_2^{\mathrm{T}_\Sigma \!\mathrm{V}}(2))) \\ &= \lambda(1.\mu_2^{\mathrm{T}_\Sigma \!\mathrm{V}}(c(1);\;2)) = \lambda(1.c(2)).\end{align*}

In the named notation, it corresponds to the phenomenon of avoiding variable capture of bound variables. Applying the substitution $\theta : M\mapsto c(x)$ to $\lambda(x.M)$ , we need to rename the binder variable x to x’ as $\theta^\sharp(\lambda(x.M))=\lambda(x'.c(x))$ .

5.1 Semantics

1. (i) $>_A$ is a family $\{{>_{A(n)}}\}_{n\in\mathbb{N}}$ of binary relations $>_{A(n)}$ on A(n), and

2. (ii) for all $a,b\in A(m)$ and $\rho : m \to n$ in $\mathbb{F}$ , if $a >_{A(m)} b$ , then $A(\rho)(a) >_{A(n)} A(\rho)(b)$ .

It will be denoted by $(A,>_A)$ .

The condition (ii) means that each binary relation is compatible with a presheaf action.

We use the following notion of monotonicity. For a binary relation $>$ , we write $a \ge b$ if $a > b$ or $a=b$ ,

Definition 5.3. Let $(A_1,>_{A_1}) ,\ldots, (A_m,>_{A_m}), (B,>_{B})$ be presheaves equipped with binary relations. A morphism $f: A_1\!\times\!\cdots\!\times\! {}A_m \rightarrow B$ in ${\textbf{Set}^\mathbb{F}}$ is monotone if

\begin{align*}&\text{for all }n\in\mathbb{F},\;\text{for all } a_1,b_1 \in A_1(n),\ldots, a_m,b_m \in A_m(n),\\& \quad\text{if there exists a single $k\in\{{1,\ldots,m}\}$ such that$(a_{k} >_{A(n)} b_{k}$and for all $j \neq k$, $a_j = b_j)$,}\\& \quad\text{then }f_n(a_1,\ldots,a_m) >_{B(n)} f_n(b_1,\ldots,b_m).\end{align*}

We interpret rewrite rules in a $(\mathrm{V}\!+\!\Sigma)$ -algebra.

Definition 5.4. Let A be a $(\mathrm{V}\!+\!\Sigma)$ -algebra. Given an assignment $\theta : Z \rightarrow \delta^{n}{\mathrm{T}_\Sigma \!\mathrm{V}}$ , a term-generated assignment $\widetilde{\theta}: Z \rightarrow \delta^n A$ is given by the composite map in ${\textbf{Set}^\mathbb{F}}$

\begin{equation*}\underline{Z} \rightarrow{\theta} \delta^n {\mathrm{T}_\Sigma \!\mathrm{V}} \rightarrow{\delta^n{!^A}} \delta^{n} A\end{equation*}

where $!^A$ is the unique $(\mathrm{V}\!+\!\Sigma)$ -algebra homomorphism from the initial $(\mathrm{V}\!+\!\Sigma)$ -algebra ${\mathrm{T}_\Sigma \!\mathrm{V}}$ to A. Throughout the paper, we denote by $!^A$ the unique $(\mathrm{V}\!+\!\Sigma)$ -homomorphism.

This definition means that the interpretation of a metavariable M by a term-generated assignment $\phi$ is performed by firstly $\theta$ assigning some term t to M and then interpreting the term in a $(\mathrm{V}\!+\!\Sigma)$ -algebra A. In other words, a term-generated assignment assigns a ‘term-generated’ element of A. This is because the (object) rewrite relation is defined on terms (not on meta-terms). To interpret a rewrite rule, unrestricted assignments $Z \rightarrow A$ are not suitable to model rewriting.

Definition 5.6 Let $\mathcal{C}$ be a CS. A monotone $(\mathrm{V}\!+\!\Sigma)$ -algebra $(A,>_A)$ satisfies a rewrite rule ${Z} \;\triangleright\; 0 \,\vdash \,\; {\ell\!\Rightarrow\! r}$ if for all term-generated assignments $\widetilde\theta : Z \rightarrow \delta^{n} A$ ,

(5) \begin{equation}\widetilde\theta^\sharp_0(\ell) \;>_{A(n)}\; \widetilde\theta^\sharp_0(r)\end{equation}

holds. Namely, for all assignments $\theta : Z \rightarrow \delta^{n}{\mathrm{T}_\Sigma \!\mathrm{V}}$ ,

(6) \begin{equation}!^A_n \theta^\sharp_0(\ell) \,>_{A(n)}\;\,!^A_n \theta^\sharp_0(r)\end{equation}

holds (see Figure 3).

Figure 3.

Interpretation of a rule.

For $n\in\mathbb{N}$ , we define a relation $\to_{\mathcal{C}(n)} {\stackrel{{\it def}}{=}} \{{(s,t) \| n\,\vdash s \to_{\mathcal{C}} t}\}$ .

Proof. For a map $\rho : n \to n'$ in $\mathbb{F}$ , let $\rho(t)$ denote a term by renaming each free variable using $\rho$ . We show the compatibility: if we have a rewrite step $\;\triangleright\; n \,\vdash \,\; {s \rightarrow_\mathcal{C} t}$ , then we have also $\;\triangleright\; {n'} \,\vdash \,\; {\rho(s) \rightarrow_\mathcal{C} \rho(t)}$ for any $\rho : n \to n'$ in $\mathbb{F}$ . The derivation tree of the rewrite $\;\triangleright\; n \,\vdash \,\; {s \rightarrow_\mathcal{C} t}$ begins with

\begin{equation*}\frac{\;\triangleright\; n \,\vdash \,\; {\ell \!\Rightarrow\! r}}{\;\triangleright\; n \,\vdash \,\; {\theta^\sharp(l)\rightarrow_\mathcal{C} \theta^\sharp(r)}}\end{equation*}

The derivation tree of $\;\triangleright\; {n'} \,\vdash \,\; {\rho(s) \rightarrow_\mathcal{C} \rho(t)}$ begins with the inference

\begin{equation*}\frac{\;\triangleright\; 0 \,\vdash \,\; {\ell \!\Rightarrow\! r}}{\;\triangleright\; {n'} \,\vdash \,\; {\theta'^\sharp(l)\rightarrow_\mathcal{C} \theta'^\sharp(r)}}\end{equation*}

where $\theta' : M \mapsto \rho(\theta(M))$ . Mimicking the derivation tree of the rewrite $\;\triangleright\; n \,\vdash \,\; {s \rightarrow_\mathcal{C} t}$ for this, finally we obtain $\;\triangleright\; {n'} \,\vdash \,\; {\rho(s) \rightarrow_\mathcal{C} \rho(t)}$ .

Proposition 5.9. For any $(\mathrm{V}\!+\!\Sigma,\mathcal{C})$ -algebra A,

\begin{equation*} \;\triangleright\; n \,\vdash \,\; {s \rightarrow_\mathcal{C} t } {}\;\;\;\Rightarrow\;\;\; !^A_n(s) \;>_{A(n)}\; !^A_n(t).\end{equation*}

• Case (Rule). Suppose that

  \begin{equation*}\theta_0^\sharp(\ell) \rightarrow_\mathcal{C} \theta_0^\sharp(r)\end{equation*}
  is derived from a rule $({Z} \;\triangleright\; {0} \,\vdash \,\; {\ell \!\Rightarrow\! r } { c}) \in \mathcal{C}$ with $\theta : Z \to \delta^{n}{\mathrm{T}_\Sigma \!\mathrm{V}}$ . Since A is a $(\mathrm{V}\!+\!\Sigma,\mathcal{C})$ -algebra,
  \begin{equation*}!^A_n \theta_0^\sharp(\ell) \;>_{A(n)}\; !_n^A \theta_0^\sharp(r).\end{equation*}

• Case (Fun). Suppose that

  \begin{equation*}{ \;\triangleright\; {n} \,\vdash \,\; {f(\; \ldots,n\!+\!1 \cdots n\!+\!i_j.t_j,\ldots) \Rightarrow_\mathcal{C}\; f(\; \ldots,n\!+\!1 \cdots n\!+\!i_j.t'_j, \ldots) } { c}}\end{equation*}
  is derived from
  \begin{equation*}f: <i_1,\ldots,i_m>\in \Sigma \;\triangleright\; {n+i_j} \,\vdash \,\; {t_j\Rightarrow_\mathcal{C} t'_j} { {b_i}} \quad (\text{some single }j\text{ s.t. }1\le j \le m)\end{equation*}
  By I.H.,
  \begin{equation*}\theta^\sharp_{n+i_j}\; t_j \;>_{A(n+i_j)}\; \theta^\sharp_{n+i_j}\; t'_j\end{equation*}
  Since $f^A$ is monotone,
  \begin{align*}\theta^\sharp\;f(\ldots,n\!+\!1 \cdots n\!+\!i_j.t_j,\ldots)= f^A(\ldots, \theta^\sharp\; t_j,\ldots)&\;>_{A(n)}\;f^A(\ldots, \theta^\sharp\; t'_j,\ldots) \\&=\theta^\sharp f(\; \ldots,n\!+\!1 \cdots n\!+\!i_j.t'_j, \ldots)\end{align*}

We obtain a complete characterisation of terminating CSs.

Proof. ( $\Leftarrow$ ): Let A be a well-founded $(\mathrm{V}\!+\!\Sigma,\mathcal{C},Z)$ -algebra. Assume that $\mathcal{C}$ is non-terminating, that is, there exists an infinite reduction sequence

\begin{equation*}n \,\vdash t_1 \rightarrow_\mathcal{C} t_2 \rightarrow_\mathcal{C} \cdots.\end{equation*}

By Proposition 5.9, we have

\begin{equation*}!_{A(n)}(t_1) \;>_{A(n)}\;\; !_{A(n)}(t_2)\;>_{A(n)}\;\; \cdots.\end{equation*}

This contradicts well-foundedness of $>_A$ .

( $\Rightarrow$ ): When a CS $\mathcal{C}$ is terminating, the $(\mathrm{V}\!+\!\Sigma,\mathcal{C},Z)$ -algebra $({\mathrm{T}_\Sigma \!\mathrm{V}},\rightarrow_\mathcal{C})$ is a desired well-founded algebra, because the binary relation $\rightarrow_\mathcal{C}$ is well-founded.

5.2 Benefit of completeness

In summary, we have a complete algebraic characterisation of rewriting of CSs as an extension of the first-order case (Huet and Lankford, Reference Huet and Lankford1978; Zantema, Reference Zantema1994).

Note that a known model of higher-order rules, the functional interpretation (van de Pol, Reference van de Pol1996), is incomplete as the following example shows.

Example 5.11. (Incompleteness of functional interpretation ( Reference van de Pol van de Pol, 1996 )) Suppose a signature $\Sigma=\{{c:<0>}\}$ . Consider a CS $(\Sigma,\mathcal{C},\{{F^{(1)}, X^{(1)}, Y^{(0)}}\})$ consisting of the following rule only:

\begin{equation*}{F^{(1)}, X^{(1)}, Y^{(0)}} \;\triangleright\; 0 \,\vdash \,\; {c(F[F[X[Y]]]) \!\Rightarrow\! F[X[Y]]}.\end{equation*}

We try to prove termination of $\mathcal{C}$ . This CS is terminating because with any rewrite step the number of c-symbols decreases. Nevertheless the existing interpretation method of higher-order rewriting based on the model of hereditary monotone functionals cannot show termination of $\mathcal{C}$ due to the incompleteness of the model (van de Pol, Reference van de Pol1994; van de Pol, Reference van de Pol1996).

In contrast to it, we can show the termination of $\mathcal{C}$ by using our algebraic semantics as follows. Now we take the monotone $(\mathrm{V}\!+\!\Sigma)$ -algebra $({\mathrm{T}_\Sigma \!\mathrm{V}},\succ_{\mathrm{T}_\Sigma \!\mathrm{V}})$ where

• $s \succ_{{\mathrm{T}_\Sigma \!\mathrm{V}}(n)} t$ if the number of c-symbols in s and t decreases.

Notice that now any term in ${\mathrm{T}_\Sigma \!\mathrm{V}}(n)$ consists of c and variables $1,\ldots,n$ . Hence, any assignment into $\delta^{n}{\mathrm{T}_\Sigma \!\mathrm{V}}$ is of the form $F \mapsto c^k(x),\;X \mapsto c^m(x),\;Y \mapsto c^l(x)$ (k,m,l-times c’s). This gives a well-founded $(\mathrm{V}\!+\!\Sigma,\mathcal{C},Z)$ -algebra $({\mathrm{T}_\Sigma \!\mathrm{V}},\succ_{\mathrm{T}_\Sigma \!\mathrm{V}})$ , which implies the termination of $\mathcal{C}$ by Theorem 3.

Theorem 5.10 gives a complete method to prove termination of a CS by finding a suitable $(\mathrm{V}\!+\!\Sigma)$ -algebra A and checking the satisfiability of rules in $\mathcal{C}$ . But this method is impractical. The notion of $(\mathrm{V}\!+\!\Sigma,\mathcal{C},Z)$ -algebra uses the satisfiability by examining all term-generated assignments, which imposes that assignments must assign terms (not just elements in a model A) to metavariables. Namely, one need to consider all closed (w.r.t. metavariables) instances of left- and right-hand sides of the rule (see (6)). Since a $(\mathrm{V}\!+\!\Sigma)$ -algebra A does not equip with a multiplication, one does not know a way to interpret meta-applications using only A.

In the next section, we improve this situation. We give a method that entails termination.

6.1 Semantics

Monotonicity of an operation corresponds to the (Fun) rule in Figure 4. Notice that the unit $\nu^A$ and the multiplication $\mu^A$ need not be monotone. The reasons are

• On the unit $\nu^A$ : there is no variable rewrite such as $x \,\!\Rightarrow\!\, y$ .

• On the multiplication $\mu^A$ : (Meta) does not simply correspond to the monotonicity of $\mu^A$ . Rather, it should be modelled by admissible assignments, which we will give in Definition 6.4.

Definition 6.3. Let $(\Sigma,\mathcal{C},Z)$ be a CS. A monotone $\Sigma$ -monoid $(A,>_A)$ satisfies a rewrite rule $Z \;\triangleright\; 0\,\vdash \,\; {\ell\!\Rightarrow\! r} \in \mathcal{C}$ if

\begin{equation*}\phi^\sharp_0(\ell) >_{A(n)} \phi^\sharp_0(r)\end{equation*}

for all assignments $\phi : Z \rightarrow \delta^{n} A$ .

Definition 6.4. Let $(A,\nu,\mu)$ be a monotone $\Sigma$ -monoid, and $\phi : Z \rightarrow A$ an assignment. Define the map $\sigma : \underline{Z} \bullet A \rightarrow A$ by the composite

\begin{equation*} \underline{Z} \bullet A \rightarrow^{\phi \bullet \mathrm{id}_A} A \bullet A \rightarrow^{\mu} A\end{equation*}

The assignment $\phi$ is called admissible if ${\sigma}$ is monotone.

The condition ‘ $\sigma$ is monotone’ means that each ${\sigma}_{n}^{(m)}: \underline{Z}(m) \!\times\! A(n)^m \rightarrow A(n)$ is monotone, that is,

\begin{align*}&\text{for all }m\in\mathbb{F},\;\text{for all }(\xi,M) \in \underline{Z}(m)\text{ with }\xi : m' \to m,\\&\text{for all }n\in\mathbb{F},\;\text{for all } a_1,b_1 \in A_1(n),\ldots, a_m,b_m \in A_m(n),\\&\quad \text{if there exists a single $k\in\{{1,\ldots,m}\}$ such that $(a_{k} >_{A(n)} b_{k}$and for all $j \neq k$, $a_j = b_j)$,}\\&\quad \text{then }\mu^{ A}_{n}( A(\xi)(\phi_{m'}(M));\; a_1,\ldots,a_m) >_{A(n)}\; \mu^{ A}_{n}( A(\xi)(\phi_{m'}(M));\; b_1,\ldots,b_m).\end{align*}

The notion of admissible assignments is a necessary ingredient of interpretation of meta-rewriting. Arbitrary assignments are not suitable to interpret meta-rewriting. An arbitrary assignment may not preserve the rewrite relation as the following example shows.

Example 6.5. Suppose the constants $\Sigma = \{{a,b,c :\langle{}\rangle}\}$ , the metavariable set $Z =\{{M^{(1)}}\}$ and the CS

\begin{equation*}\mathcal{C}=\{{\;\triangleright\; 0 \,\vdash \,\; {a\!\Rightarrow\! b}}\}.\end{equation*}

Then we have a meta-rewriting $M[a] \Rightarrow_\mathcal{C} M[b].$ We interpret this rewrite step in a monotone $\Sigma$ -monoid $({\mathrm{M}_\Sigma\underline{Z}}, [a^{\mathrm{M}_\Sigma},b^{\mathrm{M}_\Sigma},c^{\mathrm{M}_\Sigma}], \nu, \mu),\Rightarrow_\mathcal{C})$ (cf. Theorem 4.13). It satisfies the rule $a \Rightarrow_\mathcal{C} b$ . Take an assignment . Then, the interpretation using $\phi$ does not preserve the relation:

(7) \begin{equation}\phi^\sharp(M[a]) = c \not \Rightarrow_\mathcal{C} c = \phi^\sharp(M[b]).\end{equation}

We need a ‘monotonic’ interpretation of meta-rewriting to establish an algebraic termination proof method. The idea of admissible assignments is motivated by prohibiting this kind of ‘non-monotonic’ interpretation of a rewrite step.

This problem has already been recognised by van de Pol (Reference van de Pol1994, Example 5), (1996, Section 4.3). The notion of admissible assignments is analogous to his notion of strict valuations.

1. (i) A satisfies all rules of a CS $(\Sigma,\mathcal{C},Z)$ , and

2. (ii) there is an admissible assignment $Z \rightarrow A$ .

Proof. Let $(A,>_A)$ be a $(\Sigma,\mathcal{C},Z)$ -monoid having an admissible assignment $\phi:Z\to A$ . Then $(\delta^{n} A, >_{\delta^{n} A})$ is also a monotone $\Sigma$ -monoid, where $a >_{\delta^{n} A (k)} b {\;\stackrel{{\it def}}{\Longleftrightarrow}\;} a >_{A(n+k)} b.$ Let $\ell \!\Rightarrow\! r\in \mathcal{C}$ . Since A satisfies the rule, for all $\psi : Z \rightarrow \delta^{n} A$ ,

\begin{equation*}\psi^\sharp_0(\ell) >_{A(n)} \psi^\sharp_0(r)\end{equation*}

holds. Therefore, $\delta^{n} A$ satisfies the rule. There is an admissible assignment defined by

\begin{equation*}Z \rightarrow^\phi A \rightarrow^\iota \delta^{n} A\end{equation*}

where $\iota_k = A({up}_k^{k+n}) : A(k) \to A(k+n)$ . Hence $(\delta^{n} A,>_{\delta^{n} A})$ is a $(\Sigma,\mathcal{C},Z)$ -monoid.

We will clarify a sufficient condition ensuring the existence of an admissible assignment in Section 8. A $(\Sigma,\mathcal{C},Z)$ -monoid is a model for meta-rewriting as a Definition 5.6 for rewriting. For $n\in\mathbb{N}$ , we define a $\mathbb{N}$ -indexed relation $\Rightarrow_{\mathcal{C}(n)} {\stackrel{{\it def}}{=}} \{{(s,t) \| Z \;\triangleright\; n \,\vdash \,\; {s \Rightarrow_{\mathcal{C}} t}}\}$ . An important example of $(\Sigma,\mathcal{C},Z)$ -monoids is as follows.

1. (i) By (Rule), for every rule $\ell\!\Rightarrow\! r$ in $\mathcal{C}$ and assignment $\theta : Z \rightarrow \delta^{n} {\mathrm{M}_\Sigma\underline{Z}}$ , we have $\theta^\sharp_0(\ell) \Rightarrow_\mathcal{C} \theta^\sharp_0(r).$ Hence ${\mathrm{M}_\Sigma\underline{Z}}$ satisfies all rules in $\mathcal{C}$ .

2. (ii) There is an admissible assignment $\theta: Z \rightarrow {\mathrm{M}_\Sigma\underline{Z}}$ defined by $M\mapsto M[1,\ldots,n]$ for each $M\in Z(n)$ .

Proposition 6.10. Let $(\Sigma,\mathcal{C},Z)$ be a CS and $(A,>_A)$ a $(\Sigma,\mathcal{C},Z)$ -monoid. For any admissible assignment $\phi : Z \rightarrow A$ ,

\begin{equation*}Z \;\triangleright\; n \,\vdash \,\; {s \Rightarrow_\mathcal{C} t} \;\;\Rightarrow\;\; \phi_{n}^\sharp(s) >_{A(n)} \phi_{n}^\sharp(t)\end{equation*}

• Case (Rule). Suppose that

  \begin{equation*}Z \;\triangleright\; n \,\vdash \,\; {\theta_0^\sharp(\ell) \Rightarrow_\mathcal{C} \theta_0^\sharp(r)}\end{equation*}
  is derived from a rule $({Z} \;\triangleright\; {0} \,\vdash \,\; {\ell \!\Rightarrow\! r } { c}) \in \mathcal{C}$ with $\theta : Z \to \delta^{n}{\mathrm{M}_\Sigma\underline{Z}}$ . Let $\phi : Z \rightarrow A$ be an admissible assignment. Take an assignment $\psi$ as
  \begin{equation*}\psi = \underline Z \buildrel \theta \over \longrightarrow {\delta ^n}{\mathrm{M}_\Sigma }\underline Z \buildrel {{\delta ^n}{\phi ^\sharp }} \over \longrightarrow {\delta ^n}A\end{equation*}
  By Lemma 6.9, $\psi^\sharp = {(\delta^{n} \phi)}^\sharp \circ \theta^\sharp$ . By Lemma 6.7, since A is a $(\Sigma,\mathcal{C},Z)$ -monoid, so is $\delta^{n} A$ . Therefore,
  \begin{equation*}\phi_n^\sharp \theta_0^\sharp(\ell) = \psi_0^\sharp(\ell) \;>_{A(n)}\;\psi_0^\sharp(r)= \phi_n^\sharp \theta^\sharp(r)\end{equation*}

• Case (Fun). Similarity to the case (Fun) in the proof of Proposition 5.9.

• Case (Meta) Suppose that ${Z \;\triangleright\; n \,\vdash \,\; {M[t_1,\ldots,t_l] \;\Rightarrow_\mathcal{C}\; M[t'_1,\ldots,t'_l]}}$ is derived from

  \begin{equation*}Z \;\triangleright\; n \,\vdash \,\; {t_j \Rightarrow_\mathcal{C} t'_j} \text{ for some single} j, \text{and} \, t_i = t'_i \text{ for all }i \neq j \quad(1 \le i,j \le l)\end{equation*}
  By I.H., $\phi^\sharp(t_j) >_{A(n)} \phi^\sharp(t'_j)$ . Since $\phi$ is admissible,
  \begin{align*}\phi_n^\sharp(M[\ldots,t_j,\ldots]) = \mu^A_n(\phi_l(M); \ldots,\phi_n^\sharp (t_j),\ldots)>_{A(n)}&\;\;\mu^A_n(\phi_l(M); \ldots,\phi_n^\sharp (t'_j),\ldots)\\&= \phi_n^\sharp(M[\ldots,t'_j,\ldots])\end{align*}

Proof. ( $\Leftarrow$ ): Let A be a well-founded $(\Sigma,\mathcal{C},Z)$ -monoid. Assume that $\mathcal{C}$ is not meta-terminating, that is, there exists an infinite meta-rewriting sequence

\begin{equation*}Z \;\triangleright\; n \,\vdash \,\; {t_1 \;\Rightarrow_\mathcal{C}\; t_2 \;\Rightarrow_\mathcal{C}\; t_3 \;\Rightarrow_\mathcal{C}\; \cdots}.\end{equation*}

By Proposition 6.10, for any admissible assignment $\phi:Z \rightarrow A$ ,

\begin{equation*}\phi^\sharp_n(t_1) >_{A(n)} \phi^\sharp_n(t_2)>_{A(n)} \phi^\sharp_n(t_3) >_{A(n)} \cdots.\end{equation*}

This contradicts well-foundedness of $>_A$ .

( $\Rightarrow$ ): When a CS $\mathcal{C}$ is meta-terminating, the $(\Sigma,\mathcal{C},Z)$ -monoid $({\mathrm{M}_\Sigma\underline{Z}},\Rightarrow_\mathcal{C})$ by Proposition 6.8 is a desired well-founded one because the relation $\Rightarrow_\mathcal{C}$ is well-founded.

Remark 6.12. Notice again that the notion of admissible assignments is only used to interpret a meta-rewrite sequence in a $\Sigma$ -monoid A in the above proof of the soundness. We can allow non-admissible assignments in meta-rewriting steps. For example, in the case of the CS $\mathcal{C}$ of the untyped $\lambda$ -calculus, we have

\begin{equation*}{\theta}=[M\mapsto c, N\mapsto a]\end{equation*}

\begin{equation*}\frac{M^{(1)},N^{(0)}\triangleright 0 \vdash \lambda(x.M)@ N\Rightarrow M[N]\in \mathcal{C}}{\lambda(x.c)@\Rightarrow\mathcal{C}^{c}}(\mathrm{Rule})\end{equation*}

where $\theta$ is not admissible. Nevertheless, it is a correct meta-rewriting step and a valid reduction in the $\lambda$ -calculus.

Theorem 6.11 also serves as a method to prove termination of a CS. In practice, applying Theorem 6.11 to a termination problem is easier than applying Theorem 5.10. Theorem 5.10 requires to check the interpretations of all instances of rules by term-generated assignments. Considering all instances means that we need to use induction or case analysis on terms, which is tedious.

On the other hand, Theorem 6.11 uses merely all admissible assignments into a $\Sigma$ -monoid for interpretation, which is simpler to consider.

7.1 Hereditary monotone functionals

Given a set B of base types, we define the set $\mathbb{T}$ of simple types as the least set satisfying

\begin{equation*}\mathbb{T} = B \cup \{{ \sigma \to \tau \| \sigma,\tau\in \mathbb{T}}\}\cup \{{ \sigma \!\times\! \tau \| \sigma,\tau\in \mathbb{T}}\}\end{equation*}

Below we define a set $\mathrm{D}_\tau$ for each $\tau\in\mathbb{T}$ by the set of all hereditary monotone functionals, with the monotone order ${_\mathrm{mon}\!}{>}$ and the strictly monotone order ${_\mathrm{str}\!}{>}$ , parameterised by types (van de Pol, Reference van de Pol1994).

Definition 7.1. (( Reference van de Pol van de Pol, 1994 ) [Definition 11]) Let $(A,>_A)$ be a non-empty set A with a strict partial order $>_A$ on it. A $\mathbb{T}$ -indexed set of hereditary monotone functionals with families of (strict) partial orders

\begin{equation*}(\mathrm{D}, \{{\!\;{_\mathrm{mon}\!}{>}_\tau}\}_{\tau\in\mathbb{T}}, \{{\!\;{_\mathrm{mon}\!}{\ge}_\tau}\}_{\tau\in\mathbb{T}})\end{equation*}

is defined by

1. (i) $\mathrm{D}_\iota = A$ , with $\;{_\mathrm{mon}\!}{>}_\iota {\stackrel{{\it def}}{=}} >_A$ , and $\;{_\mathrm{mon}\!}{\ge}_\iota {\stackrel{{\it def}}{=}} \;{_\mathrm{mon}\!}{>}_\iota \cup\; \mathrm{id}$ for base types $\iota$ .

2. (ii) $\mathrm{D}_{\sigma\!\times\!\tau} = \mathrm{D}_\sigma\!\times\!\mathrm{D}_\tau$ , and $(x_1,x_2) \;{_\mathrm{mon}\!}{>}_{\sigma\!\times\!\tau} (y_1,y_2) $ ${\;\stackrel{{\it def}}{\Longleftrightarrow}\;} (x_1 = y_1\text{ and } x_2 \;{_\mathrm{mon}\!}{>}_{\tau} y_2)\text{ or }(x_1 \;{_\mathrm{mon}\!}{>}_{\sigma} y_1\text{ and } x_2 \;{_\mathrm{mon}\!}{\ge}_{\tau} y_2),$ $(x_1,x_2) \;{_\mathrm{mon}\!}{\ge}_{\sigma\!\times\!\tau} (y_1,y_2){\;\stackrel{{\it def}}{\Longleftrightarrow}\;}(x_1 \;{_\mathrm{mon}\!}{\ge}_{\sigma} y_1\text{ and } x_2 \;{_\mathrm{mon}\!}{\ge}_{\tau} y_2).$

3. (iii) $\mathrm{D}_{\sigma\to\tau} = \{{ f : \mathrm{D}_\sigma \to \mathrm{D}_\tau \| \text{for all }x,y\in \mathrm{D}_\sigma,\;x \;{_\mathrm{mon}\!}{\ge}_\sigma y \;\;\Rightarrow\;\; f(x) \;{_\mathrm{mon}\!}{\ge}_\tau\; f(y)}\}$ . $f \;{_\mathrm{mon}\!}{>}_{\sigma\to\tau}\; g {\;\stackrel{{\it def}}{\Longleftrightarrow}\;} \text{for all } x\in\mathrm{D}_\sigma,\; f(x)\;{_\mathrm{mon}\!}{>}_\tau\; g(x)$ in $\mathrm{D}_\tau$ . $\;{_\mathrm{mon}\!}{\ge}_{\sigma\to\tau} {\stackrel{{\it def}}{=}} \;{_\mathrm{mon}\!}{>}_{\sigma\to\tau}\cup \;\mathrm{id}$ , where $\sigma,\tau\in\mathbb{T}$ .

We call a function in $\mathrm{D}_{\sigma\to\tau}$ a hereditary monotone functional. In (van de Pol 1994; Reference van de Pol1996), it was called a weakly monotone functional.

7.2 Presheaf with strict partial orders

We define the presheaf of hereditary monotone functionals $\mathrm{H}\in{\textbf{Set}^\mathbb{F}}$ as follows. We assume the only base type $\iota$ .

\begin{align*} \mathrm{H}(0) &= \mathrm{D}_\iota\\ \mathrm{H}(n) &= \mathrm{D}_{\iota^n \to \iota} \quad (\text{for }n > 0)\qquad\mathrm{H}(\rho)(f) = {f}\circ<{\pi}_{\rho 1},\ldots,{\pi}_{\rho m}> \end{align*}

where $\rho: m \to n$ , and the projections $\pi_i(d_1,\ldots,d_n) = d_i$ , and the pairing $<g_1,\ldots,g_n>(a) = (g_1(a),\ldots,g_n(a))$ . It is equipped with the strict partial orders defined by

\begin{align*} >_{\mathrm{H}(0)} &{\stackrel{{\it def}}{=}} {_\mathrm{mon}\!}{>}_{\iota} \qquad,\qquad >_{\mathrm{H}(n)} {\stackrel{{\it def}}{=}} {_\mathrm{mon}\!}{>}_{{\iota^n \to \iota}}\end{align*}

7.3 Monoid

The presheaf H forms a monoid in ${\textbf{Set}^\mathbb{F}}$ . For the unit $\nu^\mathrm{H}_n : \mathrm{V}(n) \to \mathrm{H}(n)$ , we take

\begin{equation*} \nu^\mathrm{H}_n(i) = \pi_i \end{equation*}

The multiplication $\mu_n^{\!\mathrm{H}(m)}: \mathrm{H}(m) \!\times\! \mathrm{H}(n)^m \rightarrow \mathrm{H}(n)$ is defined by the composition:

Then these satisfy the monoid laws (i)–(iii) given in Definition 4.5.

7.4 $\Sigma$ -monoid

Suppose that given a signature $\Sigma$ , we could define a monotone $\Sigma$ -algebra

\begin{equation*}(\mathrm{H},[f^\mathrm{H}]_{f\in\Sigma},>^\mathrm{H}).\end{equation*}

Each operation in the context 0 is a hereditary monotone functional. Next we must verify that H forms a $\Sigma$ -monoid. This is not automatic and depends on the chosen hereditary monotone functionals. If we took suitable ones, then the $\Sigma$ -monoid laws hold. ‘Second-order polynomials’ are such suitable ones, which we will see next.

7.5 Example of termination proof using a $\Sigma$ -monoid of hereditary monotone functionals

Consider the following CS $\mathcal{C}$ for case expressions (van de Pol 1994; Reference van de Pol1996) for sums with $\eta$ -reduction. Let $\Sigma=\{{\textsf{inl},\textsf{inr}:\langle 0\rangle,\textsf{case}:\langle 0,1,1\rangle }\}$ .

\begin{equation*}\renewcommand{1}{1}\begin{array}[h]{llllllrllllllll}\textrm{(C1)}\qquad& X^{(0)},F^{(1)},G^{(1)}&\,\triangleright& 0 &\,\vdash& \textsf{case}(\textsf{inl}(X),F,G) &\!\Rightarrow\!& F[X] \\\textrm{(C2)}& Y^{(0)},F^{(1)},G^{(1)}&\,\triangleright& 0 &\,\vdash& \textsf{case}(\textsf{inr}(Y),F,G) &\!\Rightarrow\!& G[Y] \\\textrm{(C3)}& E^{(0)},H^{(1)} &\,\triangleright& 0 &\,\vdash& \textsf{case}(E,x.H[\textsf{inl}(x)],y.H[\textsf{inr}(y)]) &\!\Rightarrow\!& H[E]\end{array}\end{equation*}

It is known that the known syntactic criteria of termination, such as the General Schema (Blanqui, Reference Blanqui2000, Reference Blanqui2016) criterion, cannot deal with the termination of this example because the lhs of the final rule is not a higher-order pattern (Miller, Reference Miller1991). We show the termination of $\mathcal{C}$ by using the $\Sigma$ -monoid H of hereditary monotone functionals. Now we take a monotone $\Sigma$ -monoid $(\mathrm{H},>_\mathrm{H})$ generated by $(\mathbb{N},>)$ where $>$ is the usual order on the natural numbers $\mathbb{N}$ . So, $\mathrm{H}(0)=\mathbb{N}$ . We take operations as follows.

\begin{align*} &\nu^\mathrm{H} : \mathrm{V}(n) \to \mathrm{H}(n);\qquad\quad \nu^\mathrm{H}_n(i) = \pi_i\\ &\textsf{inl}^\mathrm{H},\textsf{inr}^\mathrm{H} : \mathrm{H}(n) \to \mathrm{H}(n);\quad \textsf{inl}^\mathrm{H}_n(x) = \textsf{inr}^\mathrm{H}_n(x) = x\\ &\textsf{case}^\mathrm{H}_n:\mathrm{H}(n)\!\times\!\mathrm{H}(n+1)\!\times\!\mathrm{H}(n+1) \to \mathrm{H}(n)\\ &\textsf{case}^\mathrm{H}_n(z,f,g) = f \circ \langle{Id},z\rangle + g \circ \langle{Id},z\rangle + z +\mathbf{1}\end{align*}

where the constant function $\mathbf{1}(u) = 1$ and the function pairing is defined by $\langle f,g\rangle(x) = (f(x),g(x))$ . The operations are indeed monotone. Then the $\Sigma$ -monoid law holds. For instance, the $\Sigma$ -monoid law (iv) for $\textsf{case}^\mathrm{H}$ at $n=1$ :

\begin{equation*}\mu_1^{(1)}(\textsf{case}^\mathrm{H}_1(z,f,g);b) \;=\; \textsf{case}_1^\mathrm{H}(\mu_1^{(1)}(z,b), \mu^2_{(2)}(f;\; \textsf{up}_1^2(b),\nu_2(2)), \mu^2_{(2)}(g;\; \textsf{up}_1^2(b),\nu_2(2)) )\end{equation*}

holds because

\begin{align*} lhs &= (f \circ \langle{Id},z\rangle + g \circ \langle{Id},z\rangle + z+\mathbf{1}) \circ b\\ &= f\circ\langle b,z\circ b\rangle + g\circ \langle b,z\circ b\rangle + z\circ b +\mathbf{1}\\ rhs &= f\circ\langle{up}_1^2(b),\pi_2\rangle\circ\langle{Id},z\circ b\rangle + g\circ\langle{up}_1^2(b),\pi_2\rangle\circ\langle{Id},z\circ b\rangle + z\circ b +\mathbf{1}\\ &= f\circ\langle b\circ\pi_1 \circ\langle{Id},z\circ b\rangle,\;\pi_2\circ\langle{Id},z\circ b\rangle\rangle + g\circ\langle b\circ\pi_1 \circ\langle{Id},z\circ b\rangle,\;\pi_2\circ\langle{Id},z\circ b\rangle\rangle + z\circ b +\mathbf{1}\\ &= lhs\end{align*}

The general case of other operations is proved similarly.

The $\Sigma$ -monoid H satisfies the rules. The interpretations of both sides of all the rules are decreasing: for all $x,y,e\in \mathbb{N}=\mathrm{H}(0)$ , and for all $f,g,h \in \mathbb{N}\to\mathbb{N} \subseteq \mathrm{H}(1)$ ,

\begin{align*}\textrm{(C1)}\qquad& lhs = f(x) + g(x) + x + 1 \;>\; f(x) = rhs \\\textrm{(C2)}\qquad& lhs = f(y) + g(y) + y + 1 \;>\; g(y) = rhs \\\textrm{(C3)}\qquad& lhs = h(e) + h(e) + e + 1 \;>\; h(e) = rhs\end{align*}

There is an admissible assignment $\phi:Z \rightarrow \mathrm{H}$ defined by

(8) \begin{equation} X^{(0)},Y^{(0)},E^{(0)} \mapsto 1, \quad F^{(1)},G^{(1)},H^{(1)}\mapsto \lambda x.x\end{equation}

where the $\lambda\lambda$ -notation denotes a meta-level function. Thus, $((\mathrm{H},\alpha,\nu,\mu),>_\mathrm{H})$ forms a well-founded $(\Sigma,\mathcal{C},Z)$ -monoid. By Theorem 6.11, the CS $\mathcal{C}$ is meta-terminating.

8.1 Analysis

For the question (1), the answer is No. Consider a CS $(\{{a,b :\langle{}\rangle}\},\{{\;\triangleright\; 0 \,\vdash \,\; {a\!\Rightarrow\! b}}\},Z)$ where $Z=\{{N^{(2)}}\}$ . The monotone $\Sigma$ -monoid $({\mathrm{T}_\Sigma \!\mathrm{V}},\rightarrow_\mathcal{C})$ satisfies the rule $a \!\Rightarrow\! b$ . Consider an assignment $\phi : Z \rightarrow {\mathrm{T}_\Sigma \!\mathrm{V}}$ . Since now only the 2-ary metavariable $N \in Z(2)$ exists, possible mappings of $\phi_2 : \underline{Z}(2) \rightarrow {\mathrm{T}_\Sigma \!\mathrm{V}}(2)$ are the four cases:

\begin{equation*}\phi_2: N \mapsto a,\quad \phi_2: N \mapsto b,\quad \phi_2: N \mapsto 1\quad \phi_2: N \mapsto 2.\end{equation*}

But none of these is admissible. The first two mappings are not admissible as in (7). For $\phi_2:$ $N\mapsto1$ , which assigns the variable 1 to N, interpreting a meta-rewriting $N[b,a] \Rightarrow_\mathcal{C} N[b,b]$ , we have

\begin{equation*}\phi^\sharp(N[b,a]) = b \not \rightarrow_\mathcal{C} b = \phi^\sharp(N[b,b]).\end{equation*}

For $\phi_2: N \mapsto 2$ , similarly interpreting a meta-rewriting $N[a,a] \Rightarrow_\mathcal{C} N[b,a]$ , we have

\begin{equation*}\phi^\sharp(N[a,a]) = a \not \rightarrow_\mathcal{C} a = \phi^\sharp(N[b,a]).\end{equation*}

These failures are due to the fact that the monotone $\Sigma$ -monoid $({\mathrm{T}_\Sigma \!\mathrm{V}},\rightarrow_\mathcal{C})$ lacks ‘an operation, which is monotonic in each argument’.

We next examine a successful case. We take the monotone $\Sigma$ -monoid of hereditary monotone functionals $(\mathrm{H},>_\mathrm{H})$ generated by $(\mathbb{N},>)$ as in Section 7.5, where we take operations $a_n^\mathrm{H} = {\bf 9},$ $b_n^\mathrm{H} = {\bf 8}$ , that is, constant functions returning 9 and 8. Since $9 > 8$ , this satisfies the rule $a \!\Rightarrow\! b$ . Consider an assignment $\phi_2 : \underline{Z}(2) \rightarrow \mathrm{H}(2)$ defined by

\begin{equation*}\phi_2 : N \mapsto \lambda xy.x+y.\end{equation*}

It is admissible because applying $\phi$ , a rewrite sequence

\begin{equation*}0 \,\vdash N[a,a] \;\Rightarrow_\mathcal{C}\; N[b,a] \;\Rightarrow_\mathcal{C}\; N[b,b]\end{equation*}

is interpreted as

\begin{equation*}9+9 \;>\; 8+9 \;>\; 8+8.\end{equation*}

In contrast to this, $({\mathrm{T}_\Sigma \!\mathrm{V}},\rightarrow_\mathcal{C})$ lacked such a ‘+’-like operation.

In general, rather than a binary ‘+’, what we need is a “sum”-like operation that combines n-elements in a model. So, we call it $$\textsf{sum}$$ in the next proposition.

Proposition 8.1. Let $((A,\nu^A,\mu^A),>_A)$ be a monotone $\Sigma$ -monoid, and Z a metavariable set. Suppose that for each $n\ge 2$ with $Z(n)\not = \varnothing$ , there exists a monotone morphism $\textsf{sum}^n : A^n \to A$ of ${\textbf{Set}^\mathbb{F}}$ such that

\begin{equation*} \mu^A( \textsf{sum}^n(a_1,\ldots,a_n); \overrightarrow{b}) = \textsf{sum}^n( \mu^A(a_1;\overrightarrow{b}), \cdots, \mu(a_n;\overrightarrow{b})).\end{equation*}

Then an admissible assignment $\phi : Z\rightarrow A$ exists and is given by

\begin{equation*}\phi_n (M) = \textsf{sum}^n(\nu^A(1),\ldots,\nu^A(n))\qquad\text{for each }M\in Z(n), n \ge 2.\end{equation*}

For a 0- or 1-ary metavariable M, we do not need such a $\textsf{sum}$ , because mapping $M^{(0)}$ to an element in A is no problem, and we can always take the mapping $M^{(1)}$ to the variable 1, which is admissible.

8.2 Examples

We list examples of monotone morphisms $\textsf{sum}^n : A^n \to A$ for known monotone $\Sigma$ -monoids.

• Case . It has been implicitly used in the proof of Proposition 6.8, that is, the admissible assignment $\phi_n: M\mapsto M[1,\ldots,n]$ was obtained from this $\textsf{sum}^n$ .

• Case H of the $\Sigma$ -monoid of hereditary monotone functionals defined in Section 7. $\textsf{sum}^n :$ . Note that van de Pol has considered a similar functional $\textsf{S}$ of ‘summing up measures’ (van de Pol, Reference van de Pol1996) [Definition 4.3.5, Section 4.4] in his hereditary functional model in order to show the existence of strict functionals.

• Case ${\mathrm{T}_\Sigma \!\mathrm{V}}.$ There is no canonical choice. One possible example is

  1. If there is $f:\langle 0,0\rangle\in\Sigma$ , then $f^{\mathrm{T}_\Sigma \!\mathrm{V}} : {\mathrm{T}_\Sigma \!\mathrm{V}} \!\times\! {\mathrm{T}_\Sigma \!\mathrm{V}} \to {\mathrm{T}_\Sigma \!\mathrm{V}}$ is monotone, and compatible with the multiplication. Thus, we can take