1. Introduction
In 1998, Gordon Plotkin presented the theory of binding algebras (Plotkin Reference Plotkin1998), which aimed at applying ideas in universal algebra to type theory. It can be read as a possibility of a new algebraic foundation of rewriting systems on higher-order terms. Aczel has developed a general framework of rewrite rules for calculi with variable binding called the Contraction Scheme (Aczel Reference Aczel1978). Plotkin’s programme of binding algebras later produced the notion of
$\Sigma$
-monoid (Fiore et al. Reference Fiore, Plotkin and Turi1999). It is noteworthy that the free
$\Sigma$
-monoids constructed in the author’s earlier work (Hamana Reference Hamana2004) are the same as the syntax of ‘meta-expressions’ defined by Aczel.
This similarity suggests that
$\Sigma$
-monoids might be qualified as a semantics of rewriting systems on abstract syntax with variable binding. Based on this idea, in this paper, we present a complete algebraic semantics of second-order rewriting systems called second-order computation systems (CSs) and apply it to the model-based termination proof technique of second-order CSs.
1.1 Higher-order abstract syntax and rewriting on higher-order terms
An earlier general work on rewriting systems on higher-order terms was done by Aczel (Reference Aczel1978). He developed a system called the Contraction Scheme. Influenced by this, Klop proposed a general system called the Combinatory Reduction Systems (Klop Reference Klop1980). Mayr and Nipkow (Reference Mayr and Nipkow1998) proposed a format of rewriting systems on higher-order terms, the higher-order rewrite system, which is a rewriting system modulo
$\beta\eta$
-equivalence and which uses the simply typed
$\lambda$
-calculus as a meta-language. This system is designed to be applicable to proof checkers and theorem proving systems because it is equipped with the typed
$\lambda$
-calculus. Blanqui, Jouannaud, and Okada proposed a rewriting system with stronger type system and
$\lambda$
-calculus (Blanqui et al. Reference Blanqui, Jouannaud and Okada1999, Reference Blanqui, Jouannaud and Okada2002) and added rewriting rules. Using the reducibility technique, they have developed techniques for proving termination.
In the field of automated theorem proving, there is an encoding technique called higher-order abstract syntax (HOAS) (Despeyroux et al. Reference Despeyroux, Felty and Hirschowitz1995; Pfenning and Elliott, Reference Pfenning and Elliott1988). This is a technique for coding binding data structures, especially object-level formulas, using the proof checker’s
$\lambda$
-calculus as the meta-language. This idea is intuitive, but there was a fundamental problem: it is difficult to apply induction to HOAS.
No report of the relevant literature has seriously discussed HOAS and rewriting on higher-order terms in the same context. However, the basic idea is quite similar because both use the typed
$\lambda$
-calculus as the meta-language. Therefore, rewriting on higher-order terms can be regarded as rewriting on HOAS. The difficulty of applying induction to HOAS also appears in a different way in the field of rewriting systems on higher-order terms. It is fundamentally related to the fact that the models (van de Pol, Reference van de Pol1994, Reference van de Pol1996) given to date for proving termination of rewriting systems on higher-order terms are not complete. This is because they both use a certain function space to model the object language, which makes it difficult to apply induction and which makes it impossible to construct the term model for completeness. Therefore, finding a complete model for rewriting on higher-order terms requires a good model for HOAS. Plotkin et al. in their theory of binding algebras (Fiore et al. Reference Fiore, Plotkin and Turi1999) made a breakthrough in solving this problem on HOAS. They characterised HOAS, that is, abstract syntax with variable binding, as an initial algebra in a presheaf category and established an induction principle on abstract syntax with variable binding.
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):

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. Background on Algebraic Semantics of Second-order Abstract Syntax
In this section, we review the technical basis of our semantics, that is., the algebraic models of abstract syntax with binding (Fiore et al. Reference Fiore, Plotkin and Turi1999) and metavariables (Hamana, Reference Hamana2004), also called second-order abstract syntax (Fiore, Reference Fiore2008), and explain why this is suitable for modelling second-order CSs.
Moreover, as we will see in the next subsection and Example 3.2, second-order abstract syntax can encode
$\lambda$
-terms of arbitrary order (not only second-order). So, second-order abstract syntax and second-order CSs are suitable for modelling calculi using higher-order terms.
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

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

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:

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.1.4 Convention on
$\alpha$
-equivalence
For a formal treatment of named variables modulo
$\alpha$
-equivalence, we assume the method of de Bruijn levels de Bruijn, Reference de Bruijn1972; Fiore et al. Reference Fiore, Plotkin and Turi1999); (Lescanne and Rouyer-Degli, Reference Lescanne and Rouyer-Degli1995) for the naming convention of variables. However, keeping de Bruijn level notation strictly is clumsy, especially in examples. Hence, we sometimes use the following convention: any term appearing in this paper hereafter is automatically normalised to a de Bruijn level
$\alpha$
-normal form suitably. For example,
$\lambda (x .\lambda (y. y @ x))$
means
$\lambda (1. \lambda (2 . 2 @ 1)$
, and
$\lambda(x.M[x])$
to mean
$\lambda(1.M[1])$
, For metavariables, we use ordinary named notation and do not use de Bruijn levels.
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:

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

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:


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

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)$

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)$
.
Remark 2.1. Aczel first introduced the syntactic structure of meta-terms and substitution for abstract syntax with variable binding (Aczel, 1978). This formal language allowed him to consider a general framework of rewrite rules for calculi with variable binding. Hamana clarified the algebraic semantics of it using
$\Sigma$
-monoids Hamana(2005), extended it to simply typed case (Hamana, 2007). Fiore (2002) and Miculan and Scagnetto (2003) gave the simply typed and algebraic characterisation of abstract syntax with binding and substitution. Fiore and Hur (2010); Fiore and Mahmoud (2010) considered algebraic theories for second-order equational presentations. Hamana (2011) gave a polymorphic and algebraic characterisation of abstract syntax with variable binding. Fiore and Hamana (2013) formulated polymorphic algebraic theories.
Notation 2.2. We denote by
$f({n+\overrightarrow{i_1}}.t_1,\ldots,{n+\overrightarrow{i_m}}.t_m)$
to mean

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$
.
3. Second-Order CSs
In this section, we introduce the framework of mono-sorted second-order CSs as a computational counterpart of second-order algebraic theories (Fiore and Hur, Reference Fiore and Hur2010; Fiore and Mahmoud, Reference Fiore and Mahmoud2010).
We formally define second-order CSs as follows.
-
(i) 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.
-
(ii) Let Z be an
$\mathbb{N}$ -indexed set of metavariables parameterised by arities, where each Z(n) is a set of n-ary metavariables. We may denote by
$M^{(n)}$ an n-ary metavariable
$M\in Z(n)$ . We may simply use the set-notation to describe an
$\mathbb{N}$ -indexed set Z. For example, writing
$Z=\{{M^{(1)},N^{(2)}}\}$ , we mean
$Z(1)=\{{M}\},Z(2)=\{{N}\}$ , and
$Z(i)=\varnothing$ for all
$i\not=1,2$ .
-
(iii) The raw meta-terms are given by the grammar:
\begin{equation*}t ::= x \| {x}.{t} \| f(t_1,\ldots,t_n) \| M[{t_1,\ldots,t_n}].\end{equation*}
$M[{t_1,\ldots,t_n}]$ is called a meta-application.
-
(iv) A judgment is of the form
\begin{equation*}{Z} \;\triangleright\; n \,\vdash \,\; t\end{equation*}
$\mathbb{N}$ -indexed set of metavariables. When Z is empty, we may write
$\;\triangleright\; n \,\vdash \,\; {t}$ or simply write
$n \; \,\vdash \,\; t$ .
-
(v) A well-formed meta-term t is a raw meta-term such that a judgment
${Z} \;\triangleright\; n \,\vdash \,\; t$ is derived by the rules in Figure 1 for some Z,n. By these rules, a meta-term always follows the method of de Bruijn levels. Hereafter, we only deal with well-formed meta-terms.
-
(vi) A term t is a raw meta-term such that a judgment
$\;\triangleright\; n \,\vdash \,\; t$ is derived by the rules in Figure 1 for some n. Namely, a term t is a meta-term without metavariables.
-
(vii) An assignment
$\theta$ is a mapping that assigns to an n-ary metavariable M a meta-term s as
where
${Z} \;\triangleright\; {n+k} \,\vdash \,\; s$ and for some
$k \in \mathbb{N}$ . The same k is used for the present
$\theta$ and all metavariables M in Z, considered as additional free variables
$n+1,\ldots,n+k$ appearing in s.We may denote an assignment
$\theta$ by the notation
$\theta = [M_1 \mapsto a_1 , \ldots, M_l \mapsto a_l].$ An assignment is extended to a substitution
$\theta^\sharp$ for metavariables. By the notation
\begin{equation*}\theta^\sharp(t)\end{equation*}
$M[t_1,\ldots,t_n]$ in t with a meta-term s whose free variables
$1,\ldots,n$ are replaced with
$t_1,\ldots,t_n$ . In this substitution process, to avoid unintended capture of free variables by a binder, variables may be suitably shifted according to the method of de Bruijn levels.
-
(viii) For meta-terms
${Z} \;\triangleright\; {0} \,\vdash \,\; { \ell }{b}$ and
${Z} \;\triangleright\; {0}\,\vdash \,\; { r }{ b}$ using a signature
$\Sigma$ , a rewrite rule is of the form
${Z} \;\triangleright\; {0} \,\vdash \,\; {\ell \;\!\Rightarrow\!\; r }{b}$ satisfying:
-
(a)
$\ell$ is a term of the form
$f(t_1,\ldots,t_n)$ , including the case
$n=0$ .
-
(b) all metavariables in r occur in
$\ell$ . These are ordinary syntactic conditions of rewrite systems to make them computationally meaningful Mayr and Nipkow (Reference Mayr and Nipkow1998). Without them, a rule like
$M \!\Rightarrow\! a$ or
$a \!\Rightarrow\! M$ is allowed, which collapses any term into a, or a generates any term. Since it admits a looping rewrite
$a \rightarrow_\mathcal{C} a$ , we impose these conditions. Note also that
$\ell$ and r are meta-terms without free variables (because they are in the context 0) but may have free metavariables taken from Z.
-
-
(ix) A CS is a tuple
$(\Sigma,\mathcal{C},Z)$ of a signature, a non-empty set
$\mathcal{C}$ of rewrite rules consisting of
$\Sigma$ -meta-terms and an
$\mathbb{N}$ -indexed set Z of all metavariables occurring in
$\mathcal{C}$ satisfying
\begin{equation*}Z \supseteq \bigcup_{({Z_i} \;\triangleright\; {0} \,\vdash \,\; {\ell\;\!\Rightarrow\!\; r})\;\in\; \mathcal{C}} Z_i.\end{equation*}
$Z_i$ of metavariables. If not, we implicitly use suitable renamed variants of rules. We may simply write a CS by
$\mathcal{C}$ if
$\Sigma$ and Z are inferable.
-
(x) A one-step rewrite
$\;\triangleright\; n \,\vdash \,\; {s \rightarrow_\mathcal{C} t}$ is a judgment generated from a given CS
$\mathcal{C}$ by using the inference rules in Figure 2. (Rule) instantiates a rewrite rule by replacing metavariables with terms. Hence, a rewrite step is defined on terms, not containing any metavariables. We often simply write a rewrite
$s \rightarrow_\mathcal{C} t$ and regard
$\rightarrow_\mathcal{C}$ as a binary relation on terms.

Figure 1. Typing rules of meta-terms.

Figure 2. Second-order rewriting (one-step).
Remark 3.1. In the previous formulations (Hamana 2017; 2019; Hamana et al. 2020), the lhss of second-order rewrite rules are restricted to Miller’s higher-order patterns at second order (Miller, 1991), or their slight extension of deterministic second-order patterns (Libal and Miller 2016; Yokoyama et al. 2003, 2004). Second-order patterns are meta-terms in which every occurrence of a meta-application is of the form
$M[x_1,\ldots,x_n],$
where
$x_1,\ldots,x_n$
are distinct bound variables. Second-order patterns are useful in view of algorithmic account of CSs because there exists the most general unifier for a solvable unification problem, and an efficient unification algorithm is known (Miller, 1991).
But in view of algebraic semantics, the restriction is unnecessary, hence in this paper we consider a more general syntactic form of rewrite rules that allows non-pattern lhss. Such rules have also appeared in the literature, which we will see in Example 5.11 and Section 7.5.
Example 3.2.
(Untyped
$\lambda$
-calculus) The signature
$\Sigma_\lambda$
for untyped
$\lambda$
-calculus is given by

The CS
$\mathcal{C}$
for untyped
$\lambda$
-calculus is given by the
$\beta$
and
$\eta$
rules:

Using
$\mathcal{C}$
, we have a one-step rewrite

using
$\theta : M \mapsto x @ y,\; N \mapsto \lambda(z.z)$
. Formally, in de Bruijn levels, this is derived by

Example 3.3.
(CPS translation) The format of CS is similar to a meta-language for expressing formal systems in computer science and logic. Here we consider the following CS
$\mathcal{S}$
for a call-by-value CPS translation (Danvy and Rose, Reference Danvy and Rose1998).
Assume the metavariables
$Z = \{{V^{(0)}, E^{(1)},(E_0)^{(0)},(E_1)^{(0)}}\}$
and the signature
$\Sigma$
consisting of the function symbols

There are two kinds of
$\lambda$
-terms, ordinary (consisting of
$\lambda$
and
$(-\; -)$
) and over-lined ones (consisting of
$\overline{\lambda}$
and
$(-\overline{\phantom{\lambda}} -)$
), and the
$\textsf{CPS}$
translates ordinary
$\lambda$
-terms to over-lined
$\lambda$
-terms using the auxiliary translation
${(\![ {\!-\!} ]\!)}$
. We write the CS
$\mathcal{S}$
of CPS translation in two ways: the left column is written in the usual named notation, and the right column is written in de Bruijn level notation, which is the format we use in this paper. Here we omit metavariable and variable contexts in the rules.

A point is that de Bruijn level version is obtained by just renaming variable names with numbers according to their de Bruijn levels. Notice that this differs from the more well-known method of de Bruijn indices. Meta-terms in de Bruijn levels can be regarded as ‘normal forms’ of
$\alpha$
-equivalent meta-terms (e.g.
$\overline{\lambda} k.k\overline{\phantom{\lambda}} V =_\alpha \overline{\lambda} 1.1\overline{\phantom{\lambda}} V$
).
One of the important properties of rewriting systems is termination, which is also called strong normalisation, meaning that any computation path is finite.
Definition 3.4 We call a CS
$(\Sigma,\mathcal{C},Z)$
terminating if the rewrite relation
$\rightarrow_\mathcal{C}$
on all terms is well-founded.
We will give a complete algebraic characterisation of terminating CSs in Section 5.
4. Algebraic Semantics of Meta-terms
In this section, we give a semantics of the syntax of CSs. We consider second-order abstract syntax in the framework of algebras in the presheaf category
${\textbf{Set}^\mathbb{F}}$
reviewed in Section 2. Terms and meta-terms have algebraic properties of initial and free
$\Sigma$
-monoids, respectively, which are suitable to use them as the syntax of CSs.
4.1 Algebra of meta-terms
We define the functor
$\delta : {\textbf{Set}^\mathbb{F}} \to {\textbf{Set}^\mathbb{F}}$
for context extension by

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

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

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}}$

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

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}}$

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

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,

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.
Remark 4.6. The above definition is almost the same as the definition of abstract clone (Taylor, 1993). The naturality condition of
$\mu$
expresses that
$\mu$
is parameterised with respect to renaming parameters m and n. The statement ‘
$\mu_m^{(n)}$
is extra-natural in n’ means that for any
$\rho : n\to n'$
in
$\mathbb{F}$
, the diagram

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,

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:

Remark 4.8. The axioms (i)–(iii) in Definition 4.5 correspond to the monoid laws (two side unit laws and the associativity law), and the axiom (iv) is called the
$\Sigma$
-monoid law stating that
$\mu$
commutes with each function symbol, which corresponds to the diagram in Definition 4.7. The axiom (iv) is a necessary property of substitution on a term-like structure with variable binding.
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.
-
(i) This axiom means replacing a variable i with the i-th element
$b_i$ in
$\overrightarrow{b}$ .
-
(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.
-
(iii) This axiom is the associativity of substitutions, that is, a version of substitution lemma.
-
(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.
Definition 4.9 A homomorphism h between
$\Sigma$
-algebras
$(A,[f^A]_{f\in\Sigma})$
to
$(B,[f^B]_{f\in\Sigma})$
is a map
$h : A \rightarrow B$
of
${\textbf{Set}^\mathbb{F}}$
such that

Concretely,

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

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

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

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

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.
Theorem 4.11. The presheaf
${\mathrm{T}_\Sigma \!\mathrm{V}}$
of terms forms an initial
$(\mathrm{V}\!+\!\Sigma)$
-algebra, i.e. an initial object in the category
$(\mathrm{V}\!+\!\Sigma)$
-alg.
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}])$
.
Proposition 4.12. There is an adjunction

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

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

Theorem 4.13. The presheaf
${\mathrm{M}_\Sigma\underline{Z}}$
of meta-terms forms a free
$\Sigma$
-monoid over
$\underline{Z}$
.
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

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

commute.
Corollary 4.14. The presheaf
${\mathrm{T}_\Sigma \!\mathrm{V}}$
forms an initial
$\Sigma$
-monoid, i.e. an initial object in the category
$\Sigma$
-Mon.
Proof. Taking
$Z=0$
as the empty presheaf, we have
${\mathrm{T}_\Sigma \!\mathrm{V}} ={\mathrm{M}_\Sigma} 0$
.
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

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

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

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

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,

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. Algebraic Semantics of Rewriting
In this section, we interpret CSs by
$\Sigma$
-algebras equipped with binary relations modelling one-step rewriting. We give a complete characterisation of CSs with respect to the algebraic semantics. The basic idea is to follow the algebraic semantics of first-order TRSs by monotone
$\Sigma$
-algebras. A fundamental characterisation of terminating TRSs has been established.
Theorem 5.1. (Reference Huet and Lankford Huet and Lankford 1978 ; Reference Zantema Zantema, 1994 ) A TRS is terminating if and only if there exists a non-empty well-founded monotone algebra that satisfies all rules of the TRS.
This proposition uses the ordinary first-order universal algebra, but the framework of the ordinary first-order universal algebra is insufficient for modelling CSs. We consider second-order computation in the framework of algebras in the presheaf category
${\textbf{Set}^\mathbb{F}}$
equipped with binary relations.
5.1 Semantics
Definition 5.2. We say that a presheaf
$A\in\textbf{Set}^\mathbb{F}$
is equipped with a binary relation
$>_A$
when
-
(i)
$>_A$ is a family
$\{{>_{A(n)}}\}_{n\in\mathbb{N}}$ of binary relations
$>_{A(n)}$ on A(n), and
-
(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

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}}$

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.5. A monotone
$(\mathrm{V}\!+\!\Sigma)$
-algebra
$(A,>_A)$
is a
$(\mathrm{V}\!+\!\Sigma)$
-algebra
$A=(A, [\nu, [f^A]_{f\in\Sigma}])$
, equipped with a binary relation
$>_{A}$
on A such that every operation
$f^A$
is monotone. Moreover, when for every
$n\in\mathbb{N}$
,
$>_{A(n)}$
is a well-founded relation, A is called well-founded.
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$
,

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

holds (see Figure 3).

Figure 3. Interpretation of a rule.
Definition 5.7 A
$(\mathrm{V}\!+\!\Sigma,\mathcal{C},Z)$
-algebra A is a monotone
$(\mathrm{V}\!+\!\Sigma)$
-algebra
$(A,>_A)$
that satisfies all rules of a CS
$(\Sigma,\mathcal{C},Z)$
(cf. Figure 3).
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}\}$
.
Proposition 5.8. The presheaf
${\mathrm{T}_\Sigma \!\mathrm{V}}$
of terms is equipped with the binary relation
$\{{\to_{\mathcal{C}(n)}}\}_{n\in\mathbb{N}}$
.
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

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

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,

Proof. By induction on the proof of
${s \rightarrow_\mathcal{C} t }$
.
-
Case (Rule). Suppose that
\begin{equation*}\theta_0^\sharp(\ell) \rightarrow_\mathcal{C} \theta_0^\sharp(r)\end{equation*}
$({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*}
\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*}
\begin{equation*}\theta^\sharp_{n+i_j}\; t_j \;>_{A(n+i_j)}\; \theta^\sharp_{n+i_j}\; t'_j\end{equation*}
$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.
Theorem 5.10. A CS
$\mathcal{C}$
is terminating if and only if there is a well-founded
$(\mathrm{V}\!+\!\Sigma,\mathcal{C},Z)$
-algebra.
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

By Proposition 5.9, we have

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:

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. Algebraic Semantics of Meta-Rewriting: Monotone
${\Sigma}$
-monoids
We have formulated the rewrite steps of a CS as a binary relation on terms. In this section, we define rewriting on meta-terms, which we call meta-rewriting. Let
$(\Sigma,\mathcal{C},Z)$
be a CS. We define the meta-rewriting relation
$\Rightarrow_\mathcal{C}$
by the inference rules defined in Figure 4. Therefore, we consider the following notion of meta-termination.

Figure 4. Meta-rewriting (one-step).
Definition 6.1. We call a CS
$(\Sigma,\mathcal{C},Z)$
meta-terminating if the rewrite relation
$\Rightarrow_\mathcal{C}$
is well-founded.
In this section, we give algebraic semantics of meta-rewriting. We follow basically the line of semantics given in Section 5, but we use
$\Sigma$
-monoids instead of
$\Sigma$
-algebras for the semantic structure.
6.1 Semantics
Definition 6.2. A monotone
$\Sigma$
-monoid
$(A,>_A)$
is a
$\Sigma$
-monoid
$(A,\nu^A,\mu^A)$
, where A is equipped with a binary relation
$>_{A}$
, such that every operation for
$\Sigma$
is monotone. Moreover, if
$>_{A(n)}$
is a well-founded relation for each
$n\in\mathbb{N}$
, A is called well-founded.
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

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

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,

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

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:

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.
Definition 6.6 A
$(\Sigma,\mathcal{C},Z)$
-monoid is a monotone
$\Sigma$
-monoid
$(A,>_A)$
such that
-
(i) A satisfies all rules of a CS
$(\Sigma,\mathcal{C},Z)$ , and
-
(ii) there is an admissible assignment
$Z \rightarrow A$ .
Lemma 6.7. If
$(A,>_A)$
is a
$(\Sigma,\mathcal{C},Z)$
-monoid, so is
$(\delta^{n} A,>_{\delta^{n} 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$
,

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

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.
Proposition 6.8.
$({\mathrm{M}_\Sigma\underline{Z}}, \Rightarrow_\mathcal{C})$
is a
$(\Sigma,\mathcal{C},Z)$
-monoid.
Proof. By Theorem 4.13,
${\mathrm{M}_\Sigma\underline{Z}}$
is a
$\Sigma$
-monoid, and so is
${\mathrm{M}_\Sigma\underline{Z}}$
. Because of the (Fun)-rule, every operation
$f^{\mathrm{M}_\Sigma\underline{Z}}$
is monotone. We check the conditions of Definition 6.6.
-
(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}$ .
-
(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)$ .
Lemma 6.9. Let
$\phi : \underline{Z} \to A$
be a map of
${\textbf{Set}^\mathbb{F}}$
and
$\psi : A \to B$
a
$\Sigma$
-monoid morphism. We have
$(\psi \circ \phi)^\sharp = \psi \circ \phi^\sharp.$
Proof. By freeness of
${\mathrm{M}_\Sigma\underline{Z}}$
, the unique
$\Sigma$
-monoid morphism that extends
$\phi$
followed by a
$\Sigma$
-monoid morphism is represented by the unique
$\Sigma$
-monoid morphism that extends
$\psi \circ \phi$
.
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$
,

Proof. By induction on the proof of
${s \Rightarrow_\mathcal{C} t }$
.
-
Case (Rule). Suppose that
\begin{equation*}Z \;\triangleright\; n \,\vdash \,\; {\theta_0^\sharp(\ell) \Rightarrow_\mathcal{C} \theta_0^\sharp(r)}\end{equation*}
$({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*}
$\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*}
$\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*}
Theorem 6.11. A CS
$(\Sigma,\mathcal{C},Z)$
is meta-terminating if and only if there is a well-founded
$(\Sigma,\mathcal{C},Z)$
-monoid.
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

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

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


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. Hereditary Monotone Functionals as a
$\Sigma$
-monoid
By Theorem 6.11, we can show the meta-termination of a given CS
$\mathcal{C}$
by finding a well-founded monotone
$(\Sigma,\mathcal{C},Z)$
-monoid. It can be regarded as a second-order extension of Theorem 5.1 for the termination of first-order TRSs.
How to find such a well-founded
$(\Sigma,\mathcal{C},Z)$
-monoid for termination is an important problem in practice. The first issue is to find an example of
$\Sigma$
-monoid. Trying to define a
$\Sigma$
-algebra structure is usually not problematic, but finding a suitable compatible multiplication
$\mu$
on it is generally hard. Fortunately, there is a guideline. There are two typical classes of
$\Sigma$
-monoids:
-
(i) A
$\Sigma$ -monoid of a syntactic term structure, where the syntactic substitution as the multiplication.
-
(ii) A
$\Sigma$ -monoid of (suitably restricted) function spaces, where the composition of functions as the multiplication.
As an example in the class (i), we have considered the
$\Sigma$
-monoid
${\mathrm{T}_\Sigma \!\mathrm{V}}$
of terms, and the
$\Sigma$
-monoid
${\mathrm{M}_\Sigma\underline{Z}}$
of meta-terms. In this class of
$\Sigma$
-monoids, the multiplication is compatible with the algebra structure (i.e. satisfying the
$\Sigma$
-monoid law), because the syntactic substitution is recursively defined on the term structure.
An example in the class (ii) is the structure called clone (short for closed sets of operations (Cohn, Reference Cohn1965)) known in universal algebra. A clone is a family of functions with all projections closed under composition. Therefore, the composition can be used as the multiplication of a
$\Sigma$
-monoid of clone.
For the above-mentioned class (ii) of clones, to define a suitable order structure on a clone, we need to analyse function spaces. Following Gandy’s early work on functional interpretation of strong normalisation of typed
$\lambda$
-calculus (Gandy, Reference Gandy1980), (van de Pol, Reference van de Pol1994); (van de Pol, Reference van de Pol1996) has defined the order structure on function spaces called hereditary monotone functionals for termination of higher-order rewrite systems in the format of Mayr and Nipkow (Reference Mayr and Nipkow1998). In this section, using hereditary monotone functionals, we show that we can construct a monotone
$\Sigma$
-monoid.
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

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

is defined by
-
(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$ .
-
(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).$
-
(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$
.

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

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

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

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 }\}$
.

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.

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$
:

holds because

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)$
,

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

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. On the Existence of Admissible Assignments
To give a
$(\Sigma,\mathcal{C},Z)$
-monoid, we have required the existence of an admissible assignment in Definition 6.6 (ii). In this section, we discuss the following natural questions:
-
(1) Does an admissible assignment always exist for a given CS
$(\Sigma,\mathcal{C},Z)$ and a candidate monotone
$\Sigma$ -monoid?
-
(2) If not, when does an admissible assignment exist?
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:

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

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

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

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

is interpreted as

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

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

Proof. Using the compatibility of
$\textsf{sum}^n$
with the multiplication, we see that the morphism
$\sigma$
in Definition 6.4 is monotone, hence
$\phi$
is admissible.
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
-
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
-
9. Termination of Binding CSs
Let
$(\Sigma,\mathcal{C},Z)$
be a CS such that every meta-application occurring in rules of
$\mathcal{C}$
is of the form
$M^l[x_1,\ldots,x_l]$
, where every
$x_i$
is a variable. We call such a CS a binding CS because it is essentially meta-application free (see also a similar notion of binding TRSs Hamana (Reference Hamana2003)). To interpret a rule and meta-rewriting in a binding CS
$\mathcal{C}$
, we do not need the monoid structure of
$\Sigma$
-monoids, that is, the multiplication
$\mu$
is not used. In this section, we investigate the termination of binding CSs.
For example, interpreting a meta-term M[1,2] (for a metavariable
$M^{(2)}$
) in a rule by an assignment
$\phi: Z \rightarrow A$
into a
$\Sigma$
-monoid
$(A,{\nu},\mu)$
, we have

The second equation is due to the right unit law of the
$\Sigma$
-monoid A (Definition 4.5 (ii)). So, to interpret a meta-term like M[1,2], we need merely an assignment
$\phi$
. Similarly, when the arguments of a meta-application are arbitrary variables
$n_1,\ldots,n_l \in \mathbb{N}$
, we have

where
$M\in Z(l);\; \xi : l \to n,\: \xi(i)=n_i \; (1\le i \le l)$
, and
$(\xi,M) \in \underline{Z}(n)$
, because
$A\bullet V$
is defined as a quotient making the above middle equation equal.
We call a meta-term a binding meta-term when any meta-application in it is of the form
$M[n_1,\ldots,n_l]$
, where
$n_i \in \mathbb{N}$
.
Binding meta-terms are meta-terms generated by a signature
$\Sigma$
, variables V and metavariables Z, where metavariables are substitutable syntactic objects. Hence, we characterise it as a free
$(\mathrm{V}\!+\!\Sigma)$
-algebra over
$\underline{Z}$
defined by
${\mathrm{B}_\Sigma \underline{Z}} {\stackrel{{\it def}}{=}} {\mathrm{T}_{\mathrm{V}+\Sigma}}(\underline{Z})$
. Syntactically,
${\mathrm{B}_\Sigma \underline{Z}}$
is constructed by a construction rule

and the construction rules for variables and function terms in Figure 1. The free
$(\mathrm{V}\!+\!\Sigma)$
-algebra
${\mathrm{B}_\Sigma \underline{Z}}$
over
$\underline{Z}$
is constructed by an initial
$(\mathrm{V}\!+\!\Sigma)+\underline{Z}$
-algebra.
We repeat the discussion of interpretation of rewriting.
Definition 9.1. The interpretation of a meta-term
$Z \;\triangleright\; n \,\vdash \,\; t$
in an
$(\mathrm{V}\!+\!\Sigma)$
-algebra
$(A,[\nu,\alpha])$
by an assignment
$\phi : Z \rightarrow A$
is denoted by
${\phi}_{n}^\sharp({t}),$
which is an element of A(n), defined by

where
$M\in Z(m)$
, a map
$\xi : m \to n$
in
$\mathbb{F}$
is defined by
$\xi(i){\stackrel{{\it def}}{=}} n_i$
.
Definition 9.2. Let
$(\Sigma,\mathcal{C},Z)$
be a binding CS. A monotone
$(\mathrm{V}\!+\!\Sigma)$
-algebra
$(A,>_A)$
satisfies a rewrite rule
$Z \;\triangleright\; 0 \,\vdash \,\; {\ell\!\Rightarrow\! r}$
if

for all assignments
$\phi : Z \rightarrow \delta^{n} A$
.
Definition 9.3. A
$(\Sigma,\mathcal{C},Z)$
-algebra A is a monotone
$(\mathrm{V}\!+\!\Sigma)$
-algebra A that satisfies all rules of a CS
$(\Sigma,\mathcal{C},Z)$
.
Notice that a binding CS is a CS built only from binding meta-terms. We define the meta-rewriting on binding meta-terms by the inference system consisting of

and (Fun) of Figure 4, where
$\Rightarrow_\mathcal{C}$
is replaced with
$\rightsquigarrow_\mathcal{C}$
. It satisfies
$\rightsquigarrow_\mathcal{C} \; =\Rightarrow_\mathcal{C}\!\cap \; \bigcup_{n\in\mathbb{N}}({\mathrm{B}_\Sigma \underline{Z}} \!\times\! {\mathrm{B}_\Sigma \underline{Z}})(n)$
.
Proposition 9.4. Let
$(\Sigma,\mathcal{C},Z)$
be a binding CS. For any
$(\Sigma,\mathcal{C},Z)$
-algebra
$(A,\alpha)$
and any assignment
$\phi : Z \rightarrow A$
,

Proof. By induction on the proof of
${s \rightsquigarrow_\mathcal{C} t }$
.
-
Case (Rule). Suppose that
\begin{equation*}Z \;\triangleright\; n \,\vdash \,\; {\theta_0^\sharp(\ell) \rightsquigarrow_\mathcal{C} \theta_0^\sharp(r)}\end{equation*}
$({Z} \;\triangleright\; {0} \,\vdash \,\; {\ell \!\Rightarrow\! r } { c}) \in \mathcal{C}$ with
$\theta : Z \to \delta^{n}{\mathrm{B}_\Sigma \underline{Z}}$ . Let
$\phi : Z \rightarrow A$ be an assignment. Take an assignment
$\psi$ as
\begin{equation*}\psi = \underline Z \buildrel \theta \over \longrightarrow {\delta ^n}{\mathrm{B}_\Sigma }\underline Z \buildrel {{\delta ^n}{\phi ^\sharp }} \over \longrightarrow {\delta ^n}A\end{equation*}
$\psi^\sharp = {(\delta^{n} \phi)}^\sharp \circ \theta^\sharp$ . Since A is a
$(\Sigma,\mathcal{C},Z)$ -algebra, 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.
Theorem 9.5. A binding CS
$(\Sigma,\mathcal{C},Z)$
is meta-terminating on all binding meta-terms if and only if there is a well-founded
$(\Sigma,\mathcal{C},Z)$
-algebra.
Proof. (
$\Leftarrow$
): Let A be a well-founded
$(\Sigma,\mathcal{C},Z)$
-algebra. Assume that
$\mathcal{C}$
is not meta-terminating, that is, there exists an infinite meta-rewriting sequence

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

This contradicts well-foundedness of
$>_A$
.
(
$\Rightarrow$
): When a CS
$\mathcal{C}$
is meta-terminating, the
$(\Sigma,\mathcal{C},Z)$
-algebra
$({\mathrm{B}_\Sigma \underline{Z}},\rightsquigarrow_\mathcal{C})$
is a desired well-founded one because the relation
$\rightsquigarrow_\mathcal{C}$
is well-founded.
Corollary 9.6. Let
$(\Sigma,\mathcal{C},Z)$
be a binding CS. If there is a well-founded
$(\Sigma,\mathcal{C},Z)$
-algebra, then
$\mathcal{C}$
is terminating.
Proof. It is clear that the meta-termination of
$\mathcal{C}$
on binding meta-terms implies the termination of
$\mathcal{C}$
on terms because all terms are binding meta-terms.
Hence, in the case of binding CSs this becomes an interesting termination proof method by interpretation because we do not need a monoid structure.
Example 9.7. (Prenex normal forms) We show the termination of the binding CS
$(\Sigma,\mathcal{C},Z)$
for conversion into prenex normal forms given in the introduction. Formally, it is given by the signature
$\Sigma=\{{\forall,\exists : \langle 1\rangle,\, \wedge,\vee:\langle 0,0\rangle,\, \neg:\langle 0\rangle}\}$
and the metavariable set
$Z = \{{P^{(0)}, Q^{(1)}}\}$
. The set
$\mathcal{C}$
of rules in de Bruijn levels is obtained by just replacing the variable x with 1.

We use Theorem 9.5 to show termination. Take a
$(\mathrm{V}\!+\!\Sigma)$
-algebra K such that the carrier is
$K(n) = \mathbb{N}$
with
$>_{K(n)}$
by the standard order
$>$
on
$\mathbb{N}$
for all
$n\in\mathbb{N}$
, and the operations are given by

All operations are monotone. We show that K satisfies the rules: take an assignment
$\phi: X \rightarrow \delta^{n} K$
by
$P\mapsto x \in\mathbb{N}$
and
$Q\mapsto y\in \mathbb{N}$
, then

The interpretations of other rules are similarly calculated. Since
$>_{K(n)} \;=\; >$
is well-founded, this shows K forms a well-founded
$(\Sigma,\mathcal{C},Z)$
-algebra. Thus, the binding CS
$\mathcal{C}$
is terminating on all terms by Corollary 9.6.
This interpretation is much simpler than the
$\Sigma$
-monoid of hereditary monotone functionals in Section 7. We merely use ordinary polynomials and did not need to use second-order polynomials as in Section 7.5. Namely, if a CS is a binding CS, we do not need functionals to interpret second-order function symbols such as
$\forall,\exists,\overline{\lambda},\lambda$
.
Example 9.8.
(CPS translation) The binding CS
$\mathcal{S}$
for a CPS translation in Example 3.3

is shown to be terminating by the following polynomial interpretation: take a
$(\mathrm{V}\!+\!\Sigma)$
-algebra K where the carrier
$K(n)=\mathbb{N}$
, the unit
$\nu^K_n(x) =0$
, and the operations:

The
$(\mathrm{V}\!+\!\Sigma)$
-algebra K satisfies the rules. We take an assignment
$\phi: Z \rightarrow \delta^{n} K$
by
$E\mapsto e \in\mathbb{N},\; V\mapsto v\in \mathbb{N},\;E_0 \mapsto e_0\in \mathbb{N},\;E_0 \mapsto e_0\in \mathbb{N}$
. Then all rules are decreasing. For instance, the interpretation of the last rule is decreasing as

Hence
$\mathcal{C}$
is terminating by Corollary 9.6.
Example 9.9.
(A theory of
$\pi$
-calculus) As the final example, we consider an example taken from a theory of
$\pi$
-calculus given by Stark. The
$\pi$
-calculus of Milner is one of the most fundamental concurrent calculi (Milner, Reference Milner1999). Stark gave a free algebra model of
$\pi$
-calculus (Stark, Reference Stark2008). A theory of
$\pi$
-calculus consists of 12 axioms. In Hamana (Reference Hamana2019), we have analysed that the theory should be partitioned into rewrite rules and equations. A reason of doing this is that commutativity axioms for the sum and the new name generation operators cannot be oriented. In this example, we consider the termination of the rule part of the theory of
$\pi$
-calculus. We omit writing contexts. The signature
$\Sigma$
is

and the set
$\mathcal{C}$
of rules is given by

This is a binding CS. Now we take the
$(\mathrm{V}\!+\!\Sigma)$
-algebra K where the carrier
$K(n)=\mathbb{N}$
and the operations:

The
$(\mathrm{V}\!+\!\Sigma)$
-algebra K satisfies the rules. We take an assignment
$\phi: Z \rightarrow \delta^{n} K$
that assigns
$x,y,b,c \in\mathbb{N}$
to metavariables X,Y,B,C, respectively. Then all rules are decreasing. For instance, the interpretation of the third rule is decreasing as

Hence
$\mathcal{C}$
is terminating by Corollary 9.6.
10. Summary
Using the algebraic structures in a presheaf category over finite sets by Fiore, Plotkin and Turi, we have developed sound and complete models of second-order rewriting systems called second-order CSs. Restricting the algebraic structures to those equipped with well-founded relations, we have obtained complete characterisations of terminating CSs. We have also extended the characterisation to rewriting on meta-terms using the notion of
$\Sigma$
-monoids. A known model of higher-order rewrite rules given by hereditary monotone functionals has been shown to be an instance of
$\Sigma$
-monoids. Moreover, we have also shown that binding CSs have been modelled using simpler algebraic structures, which also simplified the model-based termination proof.
Acknowledgements
I am grateful to Gordon Plotkin, John Power, Neil Ghani and Marcelo Fiore for encouragement, suggestions and discussions around related topics. I also thank the reviewers for their positive and constructive comments. This work was supported in part by JSPS KAKENHI Grant Number 20H04164.