Mathematical Structures in Computer Science (2022), 1–32
doi:10.1017/S0960129522000287

PA P E R

Complete algebraic semantics for second-order rewriting
systems based on abstract syntax with variable binding
Makoto Hamana
Faculty of Informatics, Gunma University, Maebashi, Japan
Email: hamana@gunma-u.ac.jp(Received 21 March 2021; revised 19 August 2022; accepted 23 August 2022)

Abstract
By using algebraic structures in a presheaf category over finite sets, following Fiore, Plotkin and Turi,
we develop sound and complete models of second-order rewriting systems called second-order computation systems (CSs). Restricting the algebraic structures to those equipped with well-founded relations, we
obtain a complete characterisation of terminating CSs. We also extend the characterisation to rewriting on
meta-terms using the notion of -monoid.
Keywords: Term rewriting; higher-order rewriting; termination; algebraic models; higher-order abstract syntax

1. Introduction
In 1998, Gordon Plotkin presented the theory of binding algebras (Plotkin, 1998), which aimed atapplying 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, 1978). Plotkin’s programme of binding algebras later produced
the notion of -monoid (Fiore et al., 1999). It is noteworthy that the free -monoids constructedin the author’s earlier work (Hamana, 2004) are the same as the syntax of ‘meta-expressions’defined by Aczel.
This similarity suggests that -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 (1978).
He developed a system called the Contraction Scheme. Influenced by this, Klop proposed a general system called the Combinatory Reduction Systems (Klop, 1980). Mayr and Nipkow (1998)
proposed a format of rewriting systems on higher-order terms, the higher-order rewrite system,
which is a rewriting system modulo βη-equivalence and which uses the simply typed λ-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 λ-calculus. Blanqui, Jouannaud, and Okada© The Author(s), 2022. Published by Cambridge University Press

https://doi.org/10.1017/S0960129522000287 Published online by Cambridge University Press

2

M. Hamana

proposed a rewriting system with stronger type system and λ-calculus (Blanqui et al., 1999, 2002)
and added rewriting rules. Using the reducibility technique, they have developed techniques forproving termination.
In the field of automated theorem proving, there is an encoding technique called higher-orderabstract syntax (HOAS) (Despeyroux et al., 1995; Pfenning and Elliott, 1988). This is a techniquefor coding binding data structures, especially object-level formulas, using the proof checker’s λcalculus as the meta-language. This idea is intuitive, but there was a fundamental problem: it isdifficult to apply induction to HOAS.
No report of the relevant literature has seriously discussed HOAS and rewriting on higherorder terms in the same context. However, the basic idea is quite similar because both use the typed
λ-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 thatthe models (van de Pol, 1994, 1996) 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 theoryof binding algebras (Fiore et al., 1999) made a breakthrough in solving this problem on HOAS.
They characterised HOAS, that is, abstract syntax with variable binding, as an initial algebra in apresheaf 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., 1999).
In this sense, a connection exists between the theory of binding algebras and rewriting systems onhigher-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 andhas 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-ordersyntax 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 anecessary next step. It was mentioned as a plan in Turi and Plotkin (1997), 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 withvariable 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 onhigher-order terms.

1.3 Rewriting systems and operational semantics

The operational semantics given by SOS and the theory of rewriting systems where the first-orderterm rewriting system (TRS) is the most common formalism have several similarities: they both

https://doi.org/10.1017/S0960129522000287 Published online by Cambridge University Press

Mathematical Structures in Computer Science

3

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 connectionis 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 beapplied 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 secondorder 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, 2005). In this paper, we establish complete algebraic semantics of second-orderrewriting 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 C for conversion into prenex normal
form, that is, pushing quantifiers outside, is a typical example of rewrite rules that require thefeature of variable binding (van de Pol, 1996):
P ∧ ∀(x.Q[x]) ⇒ ∀(x.P ∧ Q[x])∀(x.Q[x]) ∧ P ⇒ ∀(x.Q[x] ∧ P)

P ∨ ∀(x.Q[x]) ⇒ ∀(x.P ∨ Q[x])∀(x.Q[x]) ∨ P ⇒ ∀(x.Q[x] ∨ P)

P ∧ ∃(x.Q[x]) ⇒ ∃(x.P ∧ Q[x])∃(x.Q[x]) ∧ P ⇒ ∃(x.Q[x] ∧ P)

P ∨ ∃(x.Q[x]) ⇒ ∃(x.P ∨ Q[x])∃(x.Q[x]) ∨ P ⇒ ∃(x.Q[x] ∨ P)¬∀(x.Q[x])¬∃(x.Q[x])⇒ ∃(x.¬(Q[x]))⇒ ∀(x.¬(Q[x]))Existing proof methods in the theory of higher-order rewriting to the CS C are not straightforwardly applicable (Jouannaud and Rubio, 2001). Alternatively, they require consideration of an
involved function space to interpret binders (van de Pol, 1994, 1996). The present paper provides
a simpler method of showing termination of CS such as C , as shown in Example 9.7.
Organisation. This paper is organised as follows. We first review the technical background of oursemantics 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 modelof higher-order rewrite rules given by hereditary monotone functionals is an instance of ouralgebraic 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., 1999) and metavariables (Hamana, 2004), also called
second-order abstract syntax (Fiore, 2008), and explain why this is suitable for modelling secondorder CSs.
Moreover, as we will see in the next subsection and Example 3.2, second-order abstract syntax
can encode λ-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.

https://doi.org/10.1017/S0960129522000287 Published online by Cambridge University Press

4

M. Hamana

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-orderabstract syntax. We first explain the distinction between object variables and metavariables, which
is important for our modelling of CSs. For example, consider a λ-term
λx.(My)in a certain mathematical context. Here ‘x’ and ‘y’ are λ-calculus variables (i.e. object-level variables, because now the λ-calculus is the object system), while at the level of text, ‘M’ is ameta-level variable. We distinguish ‘object-level variables’ and ‘metavariables’ in this sense andcall ‘object-level variables’ simply ‘variables’.
2.1.2 Metavariables with arities

Metavariables have also the notion of arities. For example, writing
λx.(M[x] y)(1)

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 λ-abstraction is not a primitive construct. The above λ-term is encoded by using second-orderabstract syntax as follows:abs(x.app(M[x], y))where x.− is the primitive variable binding construct of second-order abstract syntax. Here weassume that app is a function symbol with binding arity 0, 0, which means that app takes twoarguments and each argument binds no variable, and 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 aterm like abs(x.app(M[x], y)) a meta-term meaning that a term involving metavariables. Likewise,using a function symbol λ with binding arity 1 and an infix function symbol @ with arity 0, 0,
we can construct a meta-term λ(x.M[x]@y), which is closer to the familiar notation (cf. Example
3.2).
2.1.4 Convention on α-equivalence

For a formal treatment of named variables modulo α-equivalence, we assume the method of deBruijn levels (de Bruijn, 1972; Fiore et al., 1999; Lescanne and Rouyer-Degli, 1995) for the naming
convention of variables. However, keeping de Bruijn level notation strictly is clumsy, especially inexamples. Hence, we sometimes use the following convention: any term appearing in this paper
hereafter is automatically normalised to a de Bruijn level α-normal form suitably. For example,λ(x.λ(y.y@x)) means λ(1.λ(2.2@1), and λ(x.M[x]) to mean λ(1.M[1]), For metavariables, we use
ordinary named notation and do not use de Bruijn levels.
2.2 The presheaf category SetF

In modelling second-order abstract syntax, we use a framework of categorical algebra usingpresheaves. First we explain presheaves used in this paper. The category F has finite cardinals
n = {1, . . . , n} (n is possibly 0) as objects, and all functions between them as arrows n → n .
https://doi.org/10.1017/S0960129522000287 Published online by Cambridge University Press

Mathematical Structures in Computer Science

5

The category SetF plays a central role in the algebraic models of syntax with variable binding(Fiore et al., 1999; Tanaka and Power, 2006). The objects of it are functors F → Set and the arrows
are natural transformations between them. An object A of SetF is called a presheaf and is written
as A ∈ SetF .
A map between presheaves A, B ∈ SetF is a natural transformation f : A - B, that is, a familyof functions of the form f (n) : A(n) - B(n) parameterised by all n ∈ N that makes the naturality
diagram commute
m
ρ

f (m)

A(m)

?
n

A(ρ)

?
A(n)

f (n)

- B(m)B(ρ)?
- B(n)

2.3 Algebraic model of abstract syntax and variable binding

In their seminal paper, Fiore et al. (1999) investigated algebraic models of abstract syntax involving
variable binding. A typical example of such a syntax is the syntax for untyped λ-terms:
x 1 , . . . , xn

x 1 , . . . , x n t x1 , . . . , xn
x1 , . . . , xn t@sxisx1 , . . . , xn , xn+1 t
x1 , . . . , xn λ(xn+1 .t)
This is an abstract syntax generated by three constructors, that is, the variable former, the application @ and the abstraction λ. The point is that @ is a binary function symbol, but λ is not merelya unary function symbol. It also makes the variable xn+1 bound and decreases the context. Thiscan be formulated by the function symbols with binding arities given in Section 2.1.3. In order tomodel the phenomenon of variable binding generally (not only for λ-terms), Fiore, Plotkin andTuri took the presheaf category SetF 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. (1999) is that abstract syntax withvariable binding is characterised as an initial algebra of suitable endofunctor generated by a signature (e.g. for λ-terms). Now a function symbol with binding arity, denoted by f : n1 , . . . , nl ,
has l arguments and binds ni variables in the i-th argument (1 ≤ i ≤ l). A signature  is a set  offunction symbols with binding arities.
For example, for abstract syntax of λ-terms, we take a signature  consisting of λ : 1 andan infix function symbol @ : 0, 0, as described in Section 2.1.3. The corresponding signature
endofunctor λ on SetF is λ (A) = V + A×A + δA where each summand corresponds to thearity of function symbol where the context extension is defined by (δA)(n) = A(n + 1), and thepresheaf V ∈ SetF of variables is V(n) = {1, . . . , n}.
In general, given a signature , we also denote by  the corresponding signature endofunctor1
defined like λ (more precisely, see Definition 4.1). A -algebra is a pair (A, α) consisting of apresheaf A and a map α : A → A, called an algebra structure that provides the interpretationsof constructors. An initial λ -algebra ( , in) can be constructed inductively as the presheaf ofall λ-terms modulo α-equivalence with free variable renaming. The initial algebra directly models
the abstract syntax with binding, namely
a judgment nt

is modelled as

https://doi.org/10.1017/S0960129522000287 Published online by Cambridge University Presst ∈ (n),6

M. Hamana

and renaming of free variables ρ : n → n in a λ-term is modelled by the presheaf action (ρ) :(n) → (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
. However, the method is limited to modelling of object-level abstract syntax.
2.4 Free -monoids: second-order abstract syntax with metavariables

Not only object-level abstract syntax, how can we deal with metavariables and the distinction ofsubstitutions for object and metavariables in the algebraic model of syntax with binding? This
problem was explored in Hamana (2004); Fiore (2008) and a clear answer has been obtained.
Given a signature functor , a -monoid (Fiore et al., 1999) is a -algebra (A, α) with amonoid structure
ν-

V

μ

A

A•A

that is compatible with the algebra structure in the monoidal category (SetF , •, V)2 . The unitν models the variable former, and the multiplication μ models substitution for object variables,
where the monoidal product • gives the arity of substitution.
An important structure is a free -monoid generated by an arbitrary presheaf Z, where generators Z is regarded as the presheaf of metavariables. A free -monoid over Z ∈ SetF , denoted byM Z, is constructed inductively as an initial (V +  + Z • −)-algebra, which gives the language
involving binding and metavariables. Terms of this language are expressed as the following BNF:
M Z(n)  t ::= x | f ( n+1. . . . .n+i1 .t1 , . . . , n+1. . . . .n+im .tm ) | M[t1 , . . . , tm ]Z(m)  M(2)

where x ∈ {1, . . . , n} and each f ∈  is a function symbol that binds ij variables at the j-th argument. This characterisation shows that the functor V +  models syntax with binding (as in
Section 2.1.1) and the functor Z • − models the syntactic construct of metavariables represented
as a term
M[t1 , . . . , tm ]where M ∈ Z(m) is a metavariable and the index m, called also arity, which denotes possible freevariables 1, . . . , l appearing in a term substituted for M. Terms t1 , . . . , tm are replacements of thefree variables 1, . . . , 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 θ from the presheaf Zof metavariables to M Z, which maps the metavariable M as θ (M) = 1@1. Then applying it to aterm λ(x. M[x] @ y)
θ (λ(x. M[x] @ y)) = λ(x. (x@x) @ y)(3)

is a substitution process. The freeness of M Z states that given θ, there uniquely exists theextension θ to a -monoid morphism that makes the following diagram commute:
Z

ηZ
M Z
@
R
θ@

θ
?
A
The general form of freeness is stated for an arbitrary -monoid A. To consider the syntactic case,
we take A = M Z. Then, the notion of substitution of metavariables appears. This is syntacticallyunderstood as that θ is an assignment for substitution and θ is the corresponding substitution ofterms for metavariables. For (3), we put the metavariable M ∈ Z(1).

https://doi.org/10.1017/S0960129522000287 Published online by Cambridge University Press

Mathematical Structures in Computer Science

7

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 -monoids (Hamana, 2005), extended it to simply typed
case (Hamana, 2007). Fiore (2002) and Miculan and Scagnetto (2003) gave the simply typed andalgebraic 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 withvariable binding. Fiore and Hamana (2013) formulated polymorphic algebraic theories.
−→−→
Notation 2.2. We denote by f (n + i1 .t1 , . . . , n + im .tm ) to meanf ( n+1 · · · n+i1 .t1 , . . . , n+1 · · · n+im .tm ).
We abbreviate the words left-hand side as ‘lhs’, right-hand side as ‘rhs’, first-order as ‘FO’ andhigher-order as ‘HO’.
A binary relation > is well-founded if there is no infinite decreasing sequences a1 > a2 > · · · .

3. Second-Order CSs
In this section, we introduce the framework of mono-sorted second-order CSs as a computationalcounterpart of second-order algebraic theories (Fiore and Hur, 2010; Fiore and Mahmoud, 2010).
We formally define second-order CSs as follows.
(i) A function symbol with (binding) arity, denoted by f : n1 , . . . , nl , has l arguments andbinds ni variables in the i-th argument (1 ≤ i ≤ l). A signature  is a set  of function
symbols with binding arities.
(ii) Let Z be an N-indexed set of metavariables parameterised by arities, where each Z(n) is aset of n-ary metavariables. We may denote by M (n) an n-ary metavariable M ∈ Z(n). We
may simply use the set-notation to describe an N-indexed set Z. For example, writing Z ={M (1) , N (2) }, we mean Z(1) = {M}, Z(2) = {N}, and Z(i) = ∅ for all i  = 1, 2.
(iii) The raw meta-terms are given by the grammar:
t ::= x | x.t | f (t1 , . . . , tn ) | M[t1 , . . . , tn ].
The last form M[t1 , . . . , tn ] is called a meta-application.
(iv) A judgment is of the form
Z ntwhere Z is an N-indexed set of metavariables. When Z is empty, we may write  nsimply write n
t.

t or

(v) A well-formed meta-term t is a raw meta-term such that a judgment Z  nt is derived
by the rules in Figure 1 for some Z, n. By these rules, a meta-term always follows the methodof 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  n
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 θ is a mapping that assigns to an n-ary metavariable M a meta-term s as
- s where Z  n + k
θ: Ms and for some k ∈ N. The same k is used for the presentθ and all metavariables M in Z, considered as additional free variables n + 1, . . . , n + k
appearing in s.
https://doi.org/10.1017/S0960129522000287 Published online by Cambridge University Press

8

M. Hamana

Figure 1. Typing rules of meta-terms.

Figure 2. Second-order rewriting (one-step).

We may denote an assignment θ by the notation θ = [M1  → a1 , . . . , Ml  → al ]. An assignment is extended to a substitution θ for metavariables. By the notation
θ (t)we mean that a meta-term obtained by replacing every meta-application M[t1 , . . . , tn ] in twith a meta-term s whose free variables 1, . . . , n are replaced with t1 , . . . , tn . In this substitution process, to avoid unintended capture of free variables by a binder, variables may besuitably shifted according to the method of de Bruijn levels.
(viii) For meta-terms Z  0
and Z  0
Z 0
⇒ r satisfying:r using a signature , a rewrite rule is of the form(a) is a term of the form f (t1 , . . . , tn ), including the case n = 0.
(b) all metavariables in r occur in .
These are ordinary syntactic conditions of rewrite systems to make them computationally meaningful (Mayr and Nipkow, 1998). Without them, a rule like M ⇒ a or a ⇒ M isallowed, which collapses any term into a, or a generates any term. Since it admits a looping
rewrite a →C a, we impose these conditions. Note also that and r are meta-terms without
free variables (because they are in the context 0) but may have free metavariables taken fromZ.
(ix) A CS is a tuple (, C , Z) of a signature, a non-empty set C of rewrite rules consisting of
-meta-terms and an N-indexed set Z of all metavariables occurring in C satisfying

Z⊇
Zi .
(Zi  0⇒ r) ∈ C

We assume that the rules use disjoint sets Zi of metavariables. If not, we implicitly use
suitable renamed variants of rules. We may simply write a CS by C if  and Z are inferable.
(x) A one-step rewrite  ns →C t is a judgment generated from a given CS C by using theinference rules in Figure 2. (Rule) instantiates a rewrite rule by replacing metavariables withterms. Hence, a rewrite step is defined on terms, not containing any metavariables. We often
simply write a rewrite s →C t and regard →C as a binary relation on terms.
Remark 3.1. In the previous formulations (Hamana, 2017, 2019; Hamana et al., 2020), thelhss of second-order rewrite rules are restricted to Miller’s higher-order patterns at second order
https://doi.org/10.1017/S0960129522000287 Published online by Cambridge University Press

Mathematical Structures in Computer Science

9(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[x1 , . . . , xn ], where x1 , . . . , xn are distinct boundvariables. 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 havealso appeared in the literature, which we will see in Example 5.11 and Section 7.5.
Example 3.2. (Untyped λ-calculus) The signature λ for untyped λ-calculus is given byλ : 1,@ : 0, 0

The CS C for untyped λ-calculus is given by the β and η rules:
M (1) , N (0)0λ(x.M[x])@N⇒ M[N]

M (0)



0

λ(x.M@x)⇒ M

Using C , we have a one-step rewrite
λ(x.x@y)@(λ(z.z)) →C λ(z.z)@yyusing θ : M  → x@y, N → λ(z.z). Formally, in de Bruijn levels, this is derived by
2

1

2@1

(M (1) , N (0)  0(Rule)

1

λ(2.2) θ = [M (1)  → 2@1, N (0)  → λ(2.2)]λ(1.M[1])@N ⇒ M[N]) ∈ C
λ(2.2@1)@(λ2.2) →C λ(2.2)@1

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 S for a call-byvalue CPS translation (Danvy and Rose, 1998).
Assume the metavariables Z = {V (0) , E(1) , (E0 )(0) , (E1 )(0) } and the signature  consisting of thefunction symbols
λ : 1,λ : 1,( − −) : 0, 0,( − − ) : 0, 0

CPS : 0,([ − ]) : 0.

There are two kinds of λ-terms, ordinary (consisting of λ and ( − −)) and over-lined ones (consisting of λ and ( − − )), and the CPS translates ordinary λ-terms to over-lined λ-terms using
the auxiliary translation ([−]). We write the CS 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 therules.
CPS(E0 )⇒ λk.([E0 ]) (λm.km)

CPS(E0 )⇒ λ1.([E0 ]) (λ2.12)([V])⇒ λk.k V([V])⇒ λ1.1 V([λx.E[x]])⇒ λk.k (λx.λk.([E[x]]) (λm.km))([λ1.E[1]])⇒ λ1.1 (λ2.λ3.([E[2]]) (λ4.34))([E0 E1 ]) ⇒ λk.([E0 ]) (λm.([E1 ]) (λn.mn(λa.k a))) ([E0 E1 ]) ⇒ λ1.([E0 ]) (λ2.([E1 ]) (λ3.23(λ4.1 4)))
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 ofde Bruijn indices. Meta-terms in de Bruijn levels can be regarded as ‘normal forms’ of α-equivalentmeta-terms (e.g. λk.k V =α λ1.1 V).
https://doi.org/10.1017/S0960129522000287 Published online by Cambridge University Press

10

M. Hamana

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 (, C , Z) terminating if the rewrite relation →C on all terms iswell-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 SetF reviewed in Section 2. Terms and metaterms have algebraic properties of initial and free -monoids, respectively, which are suitable touse them as the syntax of CSs.

4.1 Algebra of meta-terms

We define the functor δ : SetF → SetF for context extension by(δA)(n) = A(n + 1),(δA)(ρ) = A(ρ + id1 )for A ∈ SetF , n ∈ F, ρ : m → n in F, and a presheaf V ∈ SetF called the presheaf of variables byV(n) = {1, . . . , n}; V(ρ) = ρ.
The meaning of this definition is that each component V(n) = {1, . . . , n} gives the set of (deBruijn) variables from 1 to n, and V(ρ) gives a renaming between them.
Definition 4.1. To a signature , we associate the signature functor  : SetF → SetF given by


def
A =
δ ni A.
f :n1 ,...,nl ∈ 1≤i≤lA -algebra is an algebra of the functor . Namely, a -algebra is a pair (A, α) consisting of- A called the algebraa presheaf A ∈ SetF , called a carrier, and a map α = [f A ]f ∈ : AF
A
structure, where f is a map of Set
f A : δ n1 A×. . .×δ nl A

- A

called an operation, defined for each function symbol f : n1 , . . . , nl  ∈ , where [ ] denotes the
copair of coproducts.
Remark 4.2. For each n ∈ F, the component of an operation f A at n is a function
fnA : A(n + n1 )×· · ·×A(n + nl )- A(n)

Definition 4.3. A (V+)-algebra (A, [ν, α]) is an algebra of the functor (V+) : SetF → SetF .
Namely, it consists of a -algebra (A, α) and a map of SetF
ν : V → A.
called a unit.

https://doi.org/10.1017/S0960129522000287 Published online by Cambridge University Press

Mathematical Structures in Computer Science

11

Example 4.4. For the signature λ of the λ-calculus given in Example 3.2, the presheaf
λ-terms is defined byof all(n) = {t |  nt}

and for ρ : m → n in F, (ρ) : (m) → (n) is a renaming of λ-term by ρ, where each freevariable i ∈ {1, . . . , m} is replaced with ρ(i). It forms a (V+λ )-algebra by giving the operations
ν :V →
ν n (x)

=

x,

@ : ×

→

@n (s, t)

=

s@t,

λ :δ

→

λn (t)=

λ(n + 1.t).

These operations correspond to the constructors of variables, applications and abstractions.
Definition 4.5. A -monoid (A, α, ν, μ) is a -algebra (A, α) equipped with a unit ν : V → A
and a family of functions, called a multiplication,(n)μm: A(n)×A(m)n- A(m)

which is natural in m ∈ F and extra-natural in n ∈ F, and satisfies the following axioms:−→(n)(i) μm(ν n (i); b )= bi (1 ≤ i ≤ n)(m)(ii) μm(a;ν m (1), . . . , ν m (m))

= a

→ →
(n)
(l)
(l)
(l) (n) −→→(iii) μm(a;μm(b1 , −c ), . . . , μm
(bl , −c )) = μm(μl (a; b );−
c)
−
→
−
→
(n) A
(n+k1 )
1(iv) μm(fn (a1 , . . . , al ); b ) = fmA (μm+k(a1 ; upm+k( b ), (ν m+k1 (m + i))i=1,...,k1 ), . . . ,m
1→(n+k )m+k −μm+k l (al ; upm l ( b ), (ν m+kl (m + i))i=1,...,kl ))
l

−
→
def
where f : k1 , . . . , kl  ∈ , b = b1 , . . . , bn and upnm = A(upnm ), where m ≤ n and a map upnm :m → n in F is an injection defined by j  → j. Here, an element in the product A(n)×A(m)n is−→
denoted by (a; b1 , . . . , bn ), or simply (a; b ).
A -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 μ expresses that μ is parameterised with respect to renaming(n)parameters m and n. The statement ‘μm
is extra-natural in n’ means that for any ρ : n → n in F,
the diagram
A(n)×A(m)n
*
HH


(n)
HHμm
A(id)×A(m)ρ
H

HH

j
A(n)×A(m)n
A(m)
HH
*


HH

HH

id
(n )
A(ρ)×A(m)Hj μm
A(n )×A(m)ncommutes.
Another way to define -monoid using a monoidal structure on SetF is given as follows, whichis the original definition (Fiore et al., 1999) of -monoid.
https://doi.org/10.1017/S0960129522000287 Published online by Cambridge University Press

12

M. Hamana

Definition 4.7. (SetF , •, V) forms a monoidal category (Mac Lane, 1971), where the ‘substitution’monoidal product • is defined as follows. For presheaves A and B,



def
(A • B)(n) =A(m)×B(n)m / ∼m∈N

where ∼ is the equivalence relation generated by (t; uρ1 , . . . , uρm ) ∼ (A(ρ)(t); u1 , . . . , ul ) for ρ :m → l ∈ F.
Let  be a signature functor. It has a canonical strength st : (A) • A → (A • A) (Tanaka
and Power, 2006, Theorem 6.3) (Fiore, 2008, Corollary 7). A -monoid A = (A, α, ν, μ) consistsof a monoid object (A, ν : V → A, μ : A • A → A) in the monoidal category (SetF , •, V) with a-algebra α : A → A such that the following commutes:
(A) • Ast(A • A)

μ -

α•A

?
A•A

A

α
?
- A

μ

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 -monoid law stating that μ 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 ν : V → A can be understood as an (interpretation) map of object variables, which embeds object variables to A. A multiplication μ 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 bi in b .
(ii) This axiom says that substituting the (interpretation of) variables ν(1), . . . , ν(n) in A forvariables 1, . . . , n does not affect the element.
(iii) This axiom is the associativity of substitutions, that is, a version of substitution lemma.
(iv) This -monoid axiom says that the (interpretation of) substitution μ is pushed into the(interpretation of) term structure.
The two ways of defining -monoids are equivalent. In a termination proof of CS, we often
need to give a concrete example of -monoids. For it, Definition 4.5 of -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 -monoid in Theorem 4.13. Hereafter, we use both descriptionsof -monoids.
Definition 4.9. A homomorphism h between -algebras (A, [f A ]f ∈ ) to (B, [f B ]f ∈ ) is a map
h : A - B of SetF such thatA

[f A ]f ∈

h

?
B

[f B ]f ∈https://doi.org/10.1017/S0960129522000287 Published online by Cambridge University Press

- A

h
?
- B

Mathematical Structures in Computer Science

13

Concretely,hn (fnA (a1 , . . . , al )) = fnB (hn+i1 (a1 ), . . . , hn+il (al ))for all f : i1 , . . . , il  ∈ , n ∈ N, a1 , . . . , al ∈ A(n). This defines the category -alg of -algebras.
A morphism of -monoids h : (A, ν A , μA ) - (B, ν B , μB ) is a -algebra homomorphism thatis also a monoid morphism, that is, it satisfies the condition of homomorphism and the followingBhn (ν An (i)) = ν n (i)−→hn (μnA(m) (a; b )) = μnB (m) (hm (a); hn (b1 ), . . . , hn (bm )).

This defines the category -Mon of -monoids.
Example 4.10. Using the signature λ in Example 4.4, the presheaf of λ-terms forms a λ monoid ( , ν, μ) as follows. Since is a (V + λ )-algebra, it has the unit ν (given in Example 4.4).
The multiplication μ is defined by−→
μn (i; t )= ti(i ∈ n)−→−→−→μn (s1 @s2 ; t )= μn (s1 ; t ) @ μn (s2 ; t )−→−→μn (λ(n + 1. s); t ) = λ(n + 1. μn+1 (s; t , n + 1)).
This μ is a substitution of a λ-term. In the ordinary notation,→s ) = t[1 := s , . . . , n := s ],μ (t, −n1nwhere 1, . . . , n are variables in de Bruijn level notation. The axioms of -monoid are satisfied,because μ is the substitution operation. This is an instructive concrete example to understand themeaning of axioms. In this case, the presheaf is given syntactically, and all operations on andμ are also given syntactically, that is, the constructors of λ-terms and the substitution operation.
The presheaf TV ∈ SetF of all terms is defined byt}TV(n) = {t |  n
TV(ρ)(i) = ρ(i) (1 ≤ i ≤ m)
−
→
−
→
−
→
−
→
TV(ρ)(f (m+ i1 .t1 , . . . , m+ il .tl )) = f (m+ i1 .TV(ρ + idi1 )(t1 ), . . . , m+ il .TV(ρ + idil )(tl ))for f : i1 , . . . , il  ∈ , ρ : m → n in F, which gives renaming of variables in a term.
Theorem 4.11. The presheaf TV of terms forms an initial (V+)-algebra, i.e. an initial object
in the category (V+)-alg.
Proof. An initial (V+)-algebra is constructed by the colimit of the ω-chain 0 → (V+) 0 →(V+)2 0 → · · · (Adamek, 1974). These construction steps correspond to derivations of terms
by term forming rules; hence, their union TV gives the object part of the colimit. The arrow partof the colimit is associated with substitution. The associated algebra structure is given as follows:
the map ν : V - TV is given byν n : V(n) - TV(n),i - i.
For every f ∈  with biding arity i1 , . . . , il , the map f TV : δ i1 TV×· · ·×δ il TV
SetF is given by−→−→(t1 , . . . , tl ) - f (n+ i1 .t1 , . . . , n+ il .tl ).

https://doi.org/10.1017/S0960129522000287 Published online by Cambridge University Press- TV in

14

M. Hamana

In Fiore et al. (1999, Theorem 2.1), the ‘syntactic algebra’ is constructed as an initial (V+)algebra, which is nothing but this (V+)-algebra (TV, [ν, [f T ]f ∈ ]).
Proposition 4.12. There is an adjunction
(−)
N

Set 

⊥
|−|

-

SetF

where the functor | − | = − ◦ J using the inclusion J : N → F gives the underlying indexed set ofa presheaf. Its left adjoint ( − ) is the left Kan extension along J, calculated (Hamana, 2004) asZ(n) = k∈N F(k, n)×Z(k) for Z ∈ SetN .
Therefore, we have a way to construct a presheaf Z ∈ SetF from a given N-indexed set Z ofmetavariables. Using the adjointness, a map φ : Z → |A| in SetN for A ∈ SetF induces a map
φ̂ : Z → A in SetF . We also regarded this as a way to construct a map of presheaves from anassignment φ for metavariables in Section 4.2.
Let Z be an arbitrary N-indexed set of metavariables. Given a signature , the presheaf M Z ofmeta-terms over Z is defined byM Z(n) = {t | Z  nt}

and for ρ : m → n in F defined byM Z(ρ)(i) = ρ(i)
−
→
−
→
−
→
−
→
M Z(ρ)(f (n+ i1 .t1 , . . . , n+ il .tl )) = f (n+ i1 .M Z(ρ)(t1 ), . . . , n+ il .M Z(ρ)(tl ))M Z(ρ)(M[t1 , . . . , tl ]) = M[M Z(ρ)(t1 ), . . . , M Z(ρ)(tl )].
Theorem 4.13. The presheaf M Z of meta-terms forms a free -monoid over Z.
Proof. Due to Hamana (2004). For Z ∈ SetN , a free -monoid (M Z, [fM ]f ∈ , ν, μ) over Z isconstructed as an initial (V +  + Z • −)-algebra (M Z, ν, [fM ]f ∈ , σ ). For every f ∈  withbinding arity i1 , . . . , il , the map f M Z : δ i1 M Z×· · ·×δ il M Z - M Z in SetF is given by−→−→(t1 , . . . , tl ) - f (n+ i1 .t1 , . . . , n+ il .tl ).
The unit ν is given by ν n : i → i. The map σ : Z • M Z - M Z is given by((ξ , M); t1 , . . . , tm )The map ηZ : Z- M[tξ (1) , . . . , tξ (m) ]- M Z is given by

ηZ, m : (ξ , Z) → Z[ξ (1), . . . , ξ (m)].
The multiplication μ is given as the substitution for variables, which makes the diagramηZ • id- M  Z • M Z
Z • M Z
Q
Q
Q
μ
σ QQ
?
Q
s
M Z
commute.
https://doi.org/10.1017/S0960129522000287 Published online by Cambridge University Press

Mathematical Structures in Computer Science

15

Corollary 4.14. The presheaf TV forms an initial -monoid, i.e. an initial object in the category
-Mon.
Proof. Taking Z = 0 as the empty presheaf, we have TV = M 0.
4.2 Algebraic characterisation of substitution for metavariables

We have shown that the meta-terms form a free -monoid. Formally, given Z ∈ SetN , M Z is afree -monoid over Z ∈ SetF . Namely, for an arbitrary -monoid (A, α, ν A , μA ) and φ : Z → |A|,
there exists a unique -monoid morphism φ that makes the diagram
ηZ- M Z

Z

@
R
φ̂ @

φ
?
A

commute.
We have seen that an N-indexed function φ : Z → |A| induces a map φ̂ : Z → A of SetF . It isalso extended to a -monoid morphism φ : M Z → A defined by
φ n (i) = ν A
n (i)
−
→
−
→
A
φ n (f (n + i1 .t1 , . . . , n + il .tl )) = fn (φ n+i1 (t1 ), . . . , φ n+il (tl ))−→φ n (M[ t ]) = μAn (φ m (M); φ n (t1 ), . . . , φ n (tm )) for M ∈ Z(m).

(4)

This definition gives the meaning of a meta-term in a -monoid A by structural recursion. Notethat it is not the standard structural recursion because the indices of φ vary in the recursive calls.
The meaning of a variable is obtained using ν A , which is the interpretation of variable former, afunction symbol f is interpreted as f A and a meta-application is interpreted as follows. Firstly, thevalue of a metavariable M is obtained using the map φ, and secondly, μA replaces semantically
free m variables 1, . . . , m with the meanings of t1 , . . . , tm obtained by applying φ .
The extension captures the notion of syntactic substitutions for metavariables, where a map φis regarded as an assignment of values for metavariables. We formulate substitutions along thisidea.
Definition 4.15. Let Z be an N-indexed set of metavariables, A ∈ SetF . An assignment θ
denoted byθ : Z → A,
is an N-indexed function θ : Z → |A|. We may denote an assignment θ by the notation
θ = [M1  → a1 , . . . , Mm  → am ]which assigns ai to Mi for i = 1, . . . , m.
Lemma 4.16. Let k ∈ N. If (A, [ν A , [f A ]f ∈ ]) is a (V+)-algebra, so is (δ k A, [ν δ , [f δ ]f ∈ ]),
k

def

def

k

δ A = f A . Moreover, if (A, [f A ]AA
where ν δn A = ν A
f ∈ , ν , μ ) is a -monoid, so is
n+k , fnn+kkk(A, [f δ A ]f ∈ , ν δ A , μδ A ), wherekkkμδn A : δ k A(m)×δ k A(n)m → δ k A(n)
k

a

A
A
; b1 , . . . , bm  → μA
n+k (a ; b1 , . . . , bm , ν n+k (n + 1), . . . , ν n+k (n + k)).

https://doi.org/10.1017/S0960129522000287 Published online by Cambridge University Press

16

M. Hamana

We now consider the case of assignment θ : Z
metavariable of arity n as
Z(n)  Mθn- δ k TV. It assigns a term to eacht ∈ TV(n + k)

where k is the number of additional possible free variables other than 1, . . . , n in the results.
Additional free variables generated by an assignment θ are never captured by any binder. For
example, let M be a 0-ary metavariable, and θ : Z → δTV; θ 0 : M  → c(1). The free variable 1 inc(1) is never captured by applying the substitution θ, which is automatically shifted to make it free
to follow the method of de Bruijn levels, for example,
Vθ 0 (λ(1.M)) = λ(1.θ 1 (M)) = λ(1.μδT(θ 0 (M);)) = λ(1.μT2 V (θ 0 (M); ν T2 V (2)))
1= λ(1.μ2TV (c(1); 2)) = λ(1.c(2)).
In the named notation, it corresponds to the phenomenon of avoiding variable capture of boundvariables. Applying the substitution θ : M  → c(x) to λ(x.M), we need to rename the binder
variable x to x as θ (λ(x.M)) = λ(x .c(x)).

5. Algebraic Semantics of Rewriting
In this section, we interpret CSs by -algebras equipped with binary relations modelling onestep 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 -algebras. A
fundamental characterisation of terminating TRSs has been established.
Theorem 5.1. (Huet and Lankford, 1978; Zantema, 1994) A TRS is terminating if and only ifthere 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-ordercomputation in the framework of algebras in the presheaf category SetF equipped with binary
relations.
5.1 Semantics

Definition 5.2. We say that a presheaf A ∈ SetF is equipped with a binary relation >A when(i) >A is a family {>A(n) }n∈N of binary relations >A(n) on A(n), and(ii) for all a, b ∈ A(m) and ρ : m → n in F, if a >A(m) b, then A(ρ)(a) >A(n) A(ρ)(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 ≥ b if a > b
or a = b,
Definition 5.3. Let (A1 , >A1 ), . . . , (Am , >Am ), (B, >B ) be presheaves equipped with binary
relations. A morphism f : A1 ×· · ·×Am - B in SetF is monotone if
for all n ∈ F, for all a1 , b1 ∈ A1 (n), . . . , am , bm ∈ Am (n),if there exists a single k ∈ {1, . . . , m} such that (ak >A(n) bk and for all j  = k, aj = bj ),then fn (a1 , . . . , am ) >B(n) fn (b1 , . . . , bm ).
We interpret rewrite rules in a (V+)-algebra.
https://doi.org/10.1017/S0960129522000287 Published online by Cambridge University Press

Mathematical Structures in Computer Science17

Figure 3. Interpretation of a rule.

Definition 5.4. Let A be a (V+)-algebra. Given an assignment θ : Z → δ n TV, a term-generated
assignment θ : Z → δ n A is given by the composite map in SetFZθ-δ n TV

δn!A

δnA

where !A is the unique (V+)-algebra homomorphism from the initial (V+)-algebra TV to A.
Throughout the paper, we denote by !A the unique (V+)-homomorphism.
This definition means that the interpretation of a metavariable M by a term-generated assignment φ is performed by firstly θ assigning some term t to M and then interpreting the term ina (V+)-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 → A are not suitable to model rewriting.
Definition 5.5. A monotone (V+)-algebra (A, >A ) is a (V+)-algebra A = (A, [ν, [f A ]f ∈ ]),equipped with a binary relation >A on A such that every operation f A is monotone. Moreover,when for every n ∈ N, >A(n) is a well-founded relation, A is called well-founded.
Definition 5.6. Let C be a CS. A monotone (V+)-algebra (A, >A ) satisfies a rewrite rule Z 0⇒ r if for all term-generated assignments θ : Z → δ n A,
θ 0 (r)θ 0 ( ) >A(n) (5)holds. Namely, for all assignments θ : Z → δ n TV,
A
!An θ 0 ( ) >A(n) !n θ 0 (r)(6)

holds (see Figure 3).
Definition 5.7. A (V+, C , Z)-algebra A is a monotone (V+)-algebra (A, >A ) that satisfies allrules of a CS (, C , Z) (cf. Figure 3).
def

For n ∈ N, we define a relation →C (n) = {(s, t) | n

s →C t}.

Proposition 5.8. The presheaf TV of terms is equipped with the binary relation {→C (n) }n∈N .
Proof. For a map ρ : n → n in F, let ρ(t) denote a term by renaming each free variable using ρ.
We show the compatibility: if we have a rewrite step  n
s →C t, then we have also  nρ(s) →C ρ(t) for any ρ : n → n in F. The derivation tree of the rewrite  ns →C t begins with0⇒rn
θ (l) →C θ (r)https://doi.org/10.1017/S0960129522000287 Published online by Cambridge University Press

18

M. Hamana

The derivation tree of  nρ(s) →C ρ(t) begins with the inference
n

0
⇒r
θ (l) →C θ (r)where θ : M → ρ(θ(M)). Mimicking the derivation tree of the rewrite  nfinally we obtain  nρ(s) →C ρ(t).

s →C t for this,

Proposition 5.9. For any (V+, C )-algebra A,nA
s →C t ⇒ !An (s) >A(n) !n (t).

Proof. By induction on the proof of s →C t.
• Case (Rule). Suppose that
θ 0 ( ) →C θ 0 (r)is derived from a rule (Z  0
algebra,⇒ r) ∈ C with θ : Z → δ n TV. Since A is a (V+, C )A!An θ 0 ( ) >A(n) !n θ 0 (r).

• Case (Fun). Suppose thatnf ( . . . , n+1 · · · n+ij .tj , . . . ) ⇒C f ( . . . , n+1 · · · n+ij .tj , . . . )is derived fromf : i1 , . . . , im  ∈ 

 n + ij

tj ⇒C tj(some single j s.t. 1 ≤ j ≤ m)

By I.H.,θ n+ij tj >A(n+ij ) θ n+ij tj
Since f A is monotone,θ f ( . . . , n+1 · · · n+ij .tj , . . . ) = f A ( . . . , θ tj , . . . ) >A(n) f A ( . . . , θ tj , . . . )= θ f ( . . . , n+1 · · · n+ij .tj , . . . )We obtain a complete characterisation of terminating CSs.
Theorem 5.10. A CS C is terminating if and only if there is a well-founded (V+, C , Z)-algebra.
Proof. (⇐): Let A be a well-founded (V+, C , Z)-algebra. Assume that C is non-terminating, thatis, there exists an infinite reduction sequencen

t1 →C t2 →C · · · .

By Proposition 5.9, we have!A(n) (t1 ) >A(n) !A(n) (t2 ) >A(n) · · · .
This contradicts well-foundedness of >A .
(⇒): When a CS C is terminating, the (V+, C , Z)-algebra (TV, →C ) is a desired well-founded
algebra, because the binary relation →C is well-founded.

https://doi.org/10.1017/S0960129522000287 Published online by Cambridge University Press

Mathematical Structures in Computer Science19

5.2 Benefit of completenessIn summary, we have a complete algebraic characterisation of rewriting of CSs as an extension of
the first-order case (Huet and Lankford, 1978; Zantema, 1994).
Note that a known model of higher-order rules, the functional interpretation (van de Pol, 1996),
is incomplete as the following example shows.
Example 5.11. (Incompleteness of functional interpretation (van de Pol, 1996)) Suppose asignature  = {c : 0}. Consider a CS (, C , {F (1) , X (1) , Y (0) }) consisting of the following rule
only:
F (1) , X (1) , Y (0)  0c(F[F[X[Y]]]) ⇒ F[X[Y]].

We try to prove termination of C . This CS is terminating because with any rewrite step the numberof c-symbols decreases. Nevertheless the existing interpretation method of higher-order rewriting
based on the model of hereditary monotone functionals cannot show termination of C due to theincompleteness of the model (van de Pol, 1994, 1996).
In contrast to it, we can show the termination of C by using our algebraic semantics as follows.
Now we take the monotone (V+)-algebra (TV, TV ) where• s TV(n) t if the number of c-symbols in s and t decreases.
Notice that now any term in TV(n) consists of c and variables 1, . . . , n. Hence, any assignment
into δ n TV is of the form F → ck (x), X  → cm (x), Y  → cl (x) (k, m, l-times c’s). This gives a wellfounded (V+, C , Z)-algebra (TV, TV ), which implies the termination of C by Theorem 5.10.
Theorem 5.10 gives a complete method to prove termination of a CS by finding a suitable(V+)-algebra A and checking the satisfiability of rules in C . But this method is impractical. The notion of (V+, C , Z)-algebra uses the satisfiability by examining all term-generated
assignments, which imposes that assignments must assign terms (not just elements in a modelA) to metavariables. Namely, one need to consider all closed (w.r.t. metavariables) instances ofleft- and right-hand sides of the rule (see (6)). Since a (V+)-algebra A does not equip with amultiplication, 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 -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 (, C , Z) be a CS. We define
the meta-rewriting relation ⇒C by the inference rules defined in Figure 4. Therefore, we consider
the following notion of meta-termination.
Definition 6.1. We call a CS (, C , Z) meta-terminating if the rewrite relation ⇒C is wellfounded.
In this section, we give algebraic semantics of meta-rewriting. We follow basically the lineof semantics given in Section 5, but we use -monoids instead of -algebras for the semantic
structure.

6.1 Semantics

Definition 6.2. A monotone -monoid (A, >A ) is a -monoid (A, ν A , μA ), where A is equippedwith a binary relation >A , such that every operation for  is monotone. Moreover, if >A(n) is awell-founded relation for each n ∈ N, A is called well-founded.
https://doi.org/10.1017/S0960129522000287 Published online by Cambridge University Press

20

M. Hamana

Figure 4. Meta-rewriting (one-step).

Monotonicity of an operation corresponds to the (Fun) rule in Figure 4. Notice that the unit
ν A and the multiplication μA need not be monotone. The reasons are• On the unit ν A : there is no variable rewrite such as x ⇒ y.
• On the multiplication μA : (Meta) does not simply correspond to the monotonicity of μA .
Rather, it should be modelled by admissible assignments, which we will give in Definition 6.4.
Definition 6.3. Let (, C , Z) be a CS. A monotone -monoid (A, >A ) satisfies a rewrite ruleZ 0
⇒ r ∈ C if
φ 0 ( ) >A(n) φ 0 (r)for all assignments φ : Z → δ n A.
Definition 6.4. Let (A, ν, μ) be a monotone -monoid, and φ : Z → A an assignment. Define themap σ : Z • A - A by the composite
Z•A

φ•id
A
-

A•A

μ-

A

The assignment φ is called admissible if σ is monotone.
The condition ‘σ is monotone’ means that each σ n(m) : Z(m)×A(n)mthat is,- A(n) is monotone,

for all m ∈ F, for all (ξ , M) ∈ Z(m) with ξ : m → m,
for all n ∈ F, for all a1 , b1 ∈ A1 (n), . . . , am , bm ∈ Am (n),if there exists a single k ∈ {1, . . . , m} such that (ak >A(n) bk and for all j  = k, aj = bj ),Athen μAn (A(ξ )(φ m (M)); a1 , . . . , am ) >A(n) μn (A(ξ )(φ m (M)); b1 , . . . , bm ).

The notion of admissible assignments is a necessary ingredient of interpretation of metarewriting. 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  = {a, b, c : }, the metavariable set Z = {M (1) } and the CS
C={0a ⇒ b}.

Then we have a meta-rewriting M[a] ⇒C M[b]. We interpret this rewrite step in a monotone monoid (M Z, [aM , bM , cM ], ν, μ), ⇒C ) (cf. Theorem 4.13). It satisfies the rule a ⇒C b. Takehttps://doi.org/10.1017/S0960129522000287 Published online by Cambridge University Press

Mathematical Structures in Computer Science

an assignment φ : M

21- c. Then, the interpretation using φ does not preserve the relation:φ (M[a]) = c  ⇒C c = φ (M[b]).

(7)

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 (1994, Example 5), (1996, Section 4.3).
The notion of admissible assignments is analogous to his notion of strict valuations.
Definition 6.6. A (, C , Z)-monoid is a monotone -monoid (A, >A ) such that(i) A satisfies all rules of a CS (, C , Z), and(ii) there is an admissible assignment Z - A.
Lemma 6.7. If (A, >A ) is a (, C , Z)-monoid, so is (δ n A, >δ n A ).
Proof. Let (A, >A ) be a (, C , Z)-monoid having an admissible assignment φ : Z → A. Thendef(δ n A, >δ n A ) is also a monotone -monoid, where a >δ n A(k) b ⇐⇒ a >A(n+k) b. Let ⇒ r ∈ C .
Since A satisfies the rule, for all ψ : Z - δ n A,
ψ 0 ( ) >A(n) ψ 0 (r)nholds. Therefore, δ A satisfies the rule. There is an admissible assignment defined by
Z

φ-

A

ι-

δnA

n
n
where ιk = A(upk+nk ) : A(k) → A(k + n). Hence (δ A, >δ A ) is a (, C , Z)-monoid.

We will clarify a sufficient condition ensuring the existence of an admissible assignment in
Section 8. A (, C , Z)-monoid is a model for meta-rewriting as a Definition 5.6 for rewriting. Fordefn ∈ N, we define a N-indexed relation ⇒C (n) = {(s, t) | Z  nof (, C , Z)-monoids is as follows.

s ⇒C t}. An important example

Proposition 6.8. (M Z, ⇒C ) is a (, C , Z)-monoid.
Proof. By Theorem 4.13, M Z is a -monoid, and so is M Z. Because of the (Fun)-rule, every
operation f M Z is monotone. We check the conditions of Definition 6.6.
(i) By (Rule), for every rule ⇒ r in C and assignment θ : Z → δ n M Z, we have θ 0 ( ) ⇒C θ 0 (r).
Hence M Z satisfies all rules in C .
- M Z defined by M  → M[1, . . . , n] for each(ii) There is an admissible assignment θ : Z
M ∈ Z(n).

Lemma 6.9. Let φ : Z → A be a map of SetF and ψ : A → B a -monoid morphism. We have(ψ ◦ φ) = ψ ◦ φ .
Proof. By freeness of M Z, the unique -monoid morphism that extends φ followed by a-monoid morphism is represented by the unique -monoid morphism that extends ψ ◦ φ.

https://doi.org/10.1017/S0960129522000287 Published online by Cambridge University Press

22

M. Hamana

Proposition 6.10. Let (, C , Z) be a CS and (A, >A ) a (, C , Z)-monoid. For any admissible
assignment φ : Z → A,Z ns ⇒C t ⇒ φ n (s) >A(n) φ n (t)Proof. By induction on the proof of s ⇒C t.
• Case (Rule). Suppose thatZ n

θ 0 ( ) ⇒C θ 0 (r)is derived from a rule (Z  0⇒ r) ∈ C with θ : Z → δ n M Z. Let φ : Z → A be anadmissible assignment. Take an assignment ψ as
ψ =Z

θ-

δ n M Z

δn φ
-

δnA

By Lemma 6.9, ψ = (δ n φ) ◦ θ . By Lemma 6.7, since A is a (, C , Z)-monoid, so is δ n A.
Therefore,
φ n θ 0 ( ) = ψ 0 ( ) >A(n) ψ 0 (r) = φ n θ (r)• Case (Fun). Similarity to the case (Fun) in the proof of Proposition 5.9.
M[t1 , . . . , tl ] ⇒C M[t1 , . . . , tl ] is derived from• Case (Meta) Suppose that Z  n
Z ntj ⇒C tj for some single j, and ti = ti for all i  = j(1 ≤ i, j ≤ l)

By I.H., φ (tj ) >A(n) φ (tj ). Since φ is admissible,A
φ n (M[ . . . , tj , . . . ]) = μAn (φ l (M); . . . , φ n (tj ), . . . ) >A(n) μn (φ l (M); . . . , φ n (tj ), . . . )= φ n (M[ . . . , tj , . . . ])Theorem 6.11. A CS (, C , Z) is meta-terminating if and only if there is a well-founded (, C , Z)monoid.
Proof. (⇐): Let A be a well-founded (, C , Z)-monoid. Assume that C is not meta-terminating,that is, there exists an infinite meta-rewriting sequence
t1 ⇒C t2 ⇒C t3 ⇒C · · · .

Z nBy Proposition 6.10, for any admissible assignment φ : Z → A,
φ n (t1 ) >A(n) φ n (t2 ) >A(n) φ n (t3 ) >A(n) · · · .
This contradicts well-foundedness of >A .
(⇒): When a CS C is meta-terminating, the (, C , Z)-monoid (M Z, ⇒C ) by Proposition 6.8 isa desired well-founded one because the relation ⇒C is well-founded.
Remark 6.12. Notice again that the notion of admissible assignments is only used to interpreta meta-rewrite sequence in a -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 C of theuntyped λ-calculus, we have
θ = [M  → c, N  → a]
M (1) , N (0)  0λ(x.M)@N ⇒ M[N] ∈ C

λ(x.c)@a ⇒C c
https://doi.org/10.1017/S0960129522000287 Published online by Cambridge University Press(Rule)

Mathematical Structures in Computer Science

23

where θ is not admissible. Nevertheless, it is a correct meta-rewriting step and a valid reductionin the λ-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 istedious.
On the other hand, Theorem 6.11 uses merely all admissible assignments into a -monoid forinterpretation, which is simpler to consider.

7. Hereditary Monotone Functionals as a -monoid
By Theorem 6.11, we can show the meta-termination of a given CS C by finding a well-foundedmonotone (, C , Z)-monoid. It can be regarded as a second-order extension of Theorem 5.1 forthe termination of first-order TRSs.
How to find such a well-founded (, C , Z)-monoid for termination is an important problem inpractice. The first issue is to find an example of -monoid. Trying to define a -algebra structureis usually not problematic, but finding a suitable compatible multiplication μ on it is generally
hard. Fortunately, there is a guideline. There are two typical classes of -monoids:(i) A -monoid of a syntactic term structure, where the syntactic substitution as the multiplication.
(ii) A -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 -monoid TV of terms, and the monoid M Z of meta-terms. In this class of -monoids, the multiplication is compatible withthe algebra structure (i.e. satisfying the -monoid law), because the syntactic substitution isrecursively defined on the term structure.
An example in the class (ii) is the structure called clone (short for closed sets of operations(Cohn, 1965)) 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 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 interpretationof strong normalisation of typed λ-calculus (Gandy, 1980), (van de Pol, 1994, 1996) has defined
the order structure on function spaces called hereditary monotone functionals for termination ofhigher-order rewrite systems in the format of Mayr and Nipkow (1998). In this section, using
hereditary monotone functionals, we show that we can construct a monotone -monoid.

7.1 Hereditary monotone functionals

Given a set B of base types, we define the set T of simple types as the least set satisfying
T = B ∪ {σ → τ | σ , τ ∈ T} ∪ {σ ×τ | σ , τ ∈ T}
Below we define a set Dτ for each τ ∈ T by the set of all hereditary monotone functionals, with themonotone order mon> and the strictly monotone order str>, parameterised by types (van de Pol,1994).
https://doi.org/10.1017/S0960129522000287 Published online by Cambridge University Press

24

M. Hamana

Definition 7.1. ((van de Pol, 1994) [Definition 11]) Let (A, >A ) be a non-empty set A with astrict partial order >A on it. A T-indexed set of hereditary monotone functionals with families of(strict) partial orders(D, {mon>τ }τ ∈T , {mon≥τ }τ ∈T )is defined by
def

def

(i) Dι = A, with mon>ι = >A , and mon≥ι = mon>ι ∪ id for base types ι.
(ii) Dσ×τ = Dσ ×Dτ , and (x1 , x2 ) mon>σ×τ (y1 , y2 )def⇐⇒ (x1 = y1 and x2 mon>τ y2 ) or (x1 mon>σ y1 and x2 mon≥τ y2 ),def(x1 , x2 ) mon≥σ×τ (y1 , y2 ) ⇐⇒ (x1 mon≥σ y1 and x2 mon≥τ y2 ).
(iii) Dσ →τ = {f : Dσ → Dτ | for all x, y ∈ Dσ , x mon≥σ y ⇒ f (x) mon≥τ f (y)}.
deff mon>σ →τ g ⇐⇒ for all x ∈ Dσ , f (x) mon>τ g(x) in Dτ .
defmon≥σ →τ = mon>σ →τ ∪ id, where σ , τ ∈ T.

We call a function in Dσ →τ a hereditary monotone functional. In van de Pol (1994, 1996), it wascalled a weakly monotone functional.

7.2 Presheaf with strict partial orders

We define the presheaf of hereditary monotone functionals H ∈ SetF as follows. We assume theonly base type ι.
H(0) = DιH(n) = Dιn →ι

(for n > 0)H(ρ)(f ) = f ◦ π ρ1 , . . . , π ρm 

where ρ : m → n, and the projections π i (d1 , . . . , dn ) = di , and the pairing g1 , . . . , gn (a) =(g1 (a), . . . , gn (a)). It is equipped with the strict partial orders defined bydef>H(0) = mon>ι

,def>H(n) = mon>ιn →ι

7.3 Monoid

The presheaf H forms a monoid in SetF . For the unit ν H
n : V(n) → H(n), we takeνHn (i) = π i
The multiplication μH(m): H(m)×H(n)mn- H(n) is defined by the composition:f ∈ H(m) ; g1 , . . . , gm ∈ H(n)- f ◦ g1 , . . . , gm .

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

Suppose that given a signature , we could define a monotone -algebra(H, [f H ]f ∈ , >H ).
Each operation in the context 0 is a hereditary monotone functional. Next we must verify that
H forms a -monoid. This is not automatic and depends on the chosen hereditary monotone
https://doi.org/10.1017/S0960129522000287 Published online by Cambridge University Press

Mathematical Structures in Computer Science25functionals. If we took suitable ones, then the -monoid laws hold. ‘Second-order polynomials’
are such suitable ones, which we will see next.

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

Consider the following CS C for case expressions (van de Pol, 1994, 1996) for sums with
η-reduction. Let  = {inl, inr : 0, case : 0, 1, 1}.
(C1)
(C2)
(C3)

X (0) , F (1) , G(1)  0
Y (0) , F (1) , G(1)  0
 0
E(0) , H (1)case(inl(X), F, G)⇒ F[X]case(inr(Y), F, G)⇒ G[Y]case(E, x.H[inl(x)], y.H[inr(y)]) ⇒ H[E]

It is known that the known syntactic criteria of termination, such as the General Schema (Blanqui,
2000, 2016) criterion, cannot deal with the termination of this example because the lhs of the final
rule is not a higher-order pattern (Miller, 1991). We show the termination of C by using the monoid H of hereditary monotone functionals. Now we take a monotone -monoid (H, >H )generated by (N, > ) where > is the usual order on the natural numbers N. So, H(0) = N. We take
operations as follows.
ν H : V(n) → H(n);νHn (i) = π i

HinlH , inrH : H(n) → H(n); inlHn (x) = inrn (x) = x

caseHn : H(n)×H(n + 1)×H(n + 1) → H(n)caseH
n (z, f , g) = f ◦ Id, z + g ◦ Id, z + z + 1
where the constant function 1(u) = 1 and the function pairing is defined by f , g(x) = (f (x), g(x)).
The operations are indeed monotone. Then the -monoid law holds. For instance, the -monoid
law (iv) for caseH at n = 1:
H
H (1)
2
2
2
2
μ(1)
1 (case1 (z, f , g);b) = case1 (μ1 (z, b), μ(2) (f ; up1 (b), ν 2 (2)), μ(2) (g; up1 (b), ν 2 (2)))

holds because
lhs = (f ◦ Id, z + g ◦ Id, z + z + 1) ◦ b= f ◦ b, z ◦ b + g ◦ b, z ◦ b + z ◦ b + 1
rhs = f ◦ up21 (b), π 2  ◦ Id, z ◦ b + g ◦ up21 (b), π 2  ◦ Id, z ◦ b + z ◦ b + 1= f ◦ b ◦ π 1 ◦ Id, z ◦ b, π 2 ◦ Id, z ◦ b + g ◦ b ◦ π 1 ◦ Id, z ◦ b, π 2 ◦ Id, z ◦ b + z ◦ b + 1= lhs
The general case of other operations is proved similarly.
The -monoid H satisfies the rules. The interpretations of both sides of all the rules are
decreasing: for all x, y, e ∈ N = H(0), and for all f , g, h ∈ N → N ⊆ H(1),
(C1)
(C2)
(C3)

lhs = f (x) + g(x) + x + 1 > f (x) = rhs
lhs = f (y) + g(y) + y + 1 > g(y) = rhs
lhs = h(e) + h(e) + e + 1 > h(e) = rhs

There is an admissible assignment φ : Z- H defined by

X (0) , Y (0) , E(0)  → 1,

F (1) , G(1) , H (1)  → λx.x(8)where the λλ-notation denotes a meta-level function. Thus, ((H, α, ν, μ), >H ) forms a wellfounded (, C , Z)-monoid. By Theorem 6.11, the CS C is meta-terminating.
https://doi.org/10.1017/S0960129522000287 Published online by Cambridge University Press

26

M. Hamana

8. On the Existence of Admissible Assignments
To give a (, 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 (, C , Z) and a candidate monotone
-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 : }, {  0a ⇒ b}, Z) where Z ={N (2) }. The monotone -monoid (TV, →C ) satisfies the rule a ⇒ b. Consider an assignment- TV. Since now only the 2-ary metavariable N ∈ Z(2) exists, possible mappings of
φ:Z
φ 2 : Z(2) - TV(2) are the four cases:
φ 2 : N  → a,

φ 2 : N  → b,

φ 2 : N  → 1 φ 2 : N  → 2.

But none of these is admissible. The first two mappings are not admissible as in (7). For φ 2 :N  → 1, which assigns the variable 1 to N, interpreting a meta-rewriting N[b, a] ⇒C N[b, b], wehaveφ (N[b, a]) = b  →C b = φ (N[b, b]).
For φ 2 : N → 2, similarly interpreting a meta-rewriting N[a, a] ⇒C N[b, a], we haveφ (N[a, a]) = a  →C a = φ (N[b, a]).
These failures are due to the fact that the monotone -monoid (TV, →C ) lacks ‘an operation,
which is monotonic in each argument’.
We next examine a successful case. We take the monotone -monoid of hereditary monotonefunctionals (H, >H ) generated by (N, > ) as in Section 7.5, where we take operations aH
n = 9,bH
n = 8, that is, constant functions returning 9 and 8. Since 9 > 8, this satisfies the rule a ⇒ b.
Consider an assignment φ 2 : Z(2) - H(2) defined by
φ 2 : N → λxy.x + y.
It is admissible because applying φ, a rewrite sequence0N[a, a] ⇒C N[b, a] ⇒C N[b, b]

is interpreted as
9 + 9 > 8 + 9 > 8 + 8.
In contrast to this, (TV, →C ) lacked such a ‘+’-like operation.
In general, rather than a binary ‘+’, what we need is a “sum”-like operation that combinesn-elements in a model. So, we call it sum in the next proposition.
Proposition 8.1. Let ((A, ν A , μA ), >A ) be a monotone -monoid, and Z a metavariable set.
Suppose that for each n ≥ 2 with Z(n)  = ∅, there exists a monotone morphism sumn : An → A
of SetF such that
−
→
−
→
−
→
μA (sumn (a1 , . . . , an ); b ) = sumn (μA (a1 ; b ), · · · , μ(an ; b )).
Then an admissible assignment φ : Z - A exists and is given by
φ n (M) = sumn (ν A (1), . . . , ν A (n))

for each M ∈ Z(n), n ≥ 2.

Proof. Using the compatibility of sumn with the multiplication, we see that the morphism σ in
Definition 6.4 is monotone, hence φ is admissible.
https://doi.org/10.1017/S0960129522000287 Published online by Cambridge University Press

Mathematical Structures in Computer Science27

For a 0- or 1-ary metavariable M, we do not need such a sum, because mapping M (0) to anelement in A is no problem, and we can always take the mapping M (1) to the variable 1, which isadmissible.

8.2 Examples

We list examples of monotone morphisms sumn : An → A for known monotone -monoids.
- M[a1 , . . . , an ]. It has been implicitly used in the proof of• Case M Z. sumn : a1 , . . . , an
Proposition 6.8, that is, the admissible assignment φ n : M  → M[1, . . . , n] was obtained fromthis sumn .
• Case H of the -monoid of hereditary monotone functionals defined in Section 7. sumn :- a1 + · · · + an . Note that van de Pol has considered a similar functional S
a1 , . . . , anof ‘summing up measures’ (van de Pol, 1996)[Definition 4.3.5, Section 4.4] in his hereditary
functional model in order to show the existence of strict functionals.
• Case TV. There is no canonical choice. One possible example is- If there is f : 0, 0 ∈ , then f TV : TV×TV → TV is monotone, and compatible with themultiplication. Thus, we can take- f TV (a1 , . . . , f TV (an−1 , an )).

sumn : a1 , . . . , an−1 , an

9. Termination of Binding CSs
Let (, C , Z) be a CS such that every meta-application occurring in rules of C is of the form
M l [x1 , . . . , xl ], where every xi is a variable. We call such a CS a binding CS because it is essentiallymeta-application free (see also a similar notion of binding TRSs (Hamana, 2003)). To interpret arule and meta-rewriting in a binding CS C , we do not need the monoid structure of -monoids,that is, the multiplication μ is not used. In this section, we investigate the termination of bindingCSs.
For example, interpreting a meta-term M[1, 2] (for a metavariable M (2) ) in a rule by anassignment φ : Z → A into a -monoid (A, ν, μ), we haveφ 2 (M[1, 2]) = μ(2)2 (φ 2 (M); ν 2 (1), ν 2 (2)) = φ 2 (M).
The second equation is due to the right unit law of the -monoid A (Definition 4.5 (ii)). So,
to interpret a meta-term like M[1, 2], we need merely an assignment φ. Similarly, when thearguments of a meta-application are arbitrary variables n1 , . . . , nl ∈ N, we haveφ (M[n1 , . . . , nl ]) = μ(φ(M); ν(n1 ), . . . , ν(nl )) = μ(φ(A(ξ )(M)); ν(1), . . . , ν(l)) = φ(M ξ )where M ∈ Z(l); ξ : l → n, ξ (i) = ni (1 ≤ i ≤ l), and (ξ , M) ∈ Z(n), because A • V is defined as aquotient 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[n1 , . . . , nl ], where ni ∈ N.
Binding meta-terms are meta-terms generated by a signature , variables V and metavariables Z, where metavariables are substitutable syntactic objects. Hence, we characterise it as adeffree (V+)-algebra over Z defined by B Z = TV+ (Z). Syntactically, B Z is constructed by aconstruction rule
(BMeta)M ∈ Z(l) 1 ≤ ni ≤ n (i = 1, . . . , l)n M[n1 , . . . , nl ] ∈ B Z(n)https://doi.org/10.1017/S0960129522000287 Published online by Cambridge University Press

28

M. Hamana

and the construction rules for variables and function terms in Figure 1. The free (V+)-algebra
B Z over Z is constructed by an initial (V+) + Z-algebra.
We repeat the discussion of interpretation of rewriting.
Definition 9.1. The interpretation of a meta-term Z  nt in an (V+)-algebra (A, [ν, α]) by
an assignment φ : Z → A is denoted by φ n (t), which is an element of A(n), defined by
φ n (i) = ν n (i)−→−→φ n (f (n + i1 .t1 , . . . , n + il .tl )) = fnA (φ n+i1 (t1 ), . . . , φ n+il (tl ))φ n (M[n1 , . . . , nm ]) = A(ξ )(φ m (M)),
defwhere M ∈ Z(m), a map ξ : m → n in F is defined by ξ (i) = ni .
Definition 9.2. Let (, C , Z) be a binding CS. A monotone (V+)-algebra (A, >A ) satisfies arewrite rule Z  0⇒ r iffor all assignments φ : Z

φ 0 ( ) >A(n) φ 0 (r)- δ n A.

Definition 9.3. A (, C , Z)-algebra A is a monotone (V+)-algebra A that satisfies all rules of a
CS (, C , Z).
Notice that a binding CS is a CS built only from binding meta-terms. We define the metarewriting on binding meta-terms by the inference system consisting ofsj ∈ B Z(n + ij ) (1 ≤ j ≤ m)
(Rule)(im )(M1(i1 ) , . . . , Mm
0

θ = [M1  → s1 , . . . , Mm  → sm ]⇒ r) ∈ CZ n
θ ( ) C θ (r)and (Fun) of Figure 4, where ⇒C is replaced with C . It satisfies C = ⇒C ∩B Z)(n).

n∈N (B Z×

Proposition 9.4. Let (, C , Z) be a binding CS. For any (, C , Z)-algebra (A, α) and any
assignment φ : Z → A,Z ns C t ⇒ φ n (s) >A(n) φ n (t)Proof. By induction on the proof of s C t.
• Case (Rule). Suppose that
θ 0 ( ) C θ 0 (r)Z n
is derived from a rule (Z  0
ment. Take an assignment ψ as⇒ r) ∈ C with θ : Z → δ n B Z. Let φ : Z → A be an assignψ =Zθ-δ n B Z

δn φ
-

δnA

By Lemma 6.9, ψ = (δ n φ) ◦ θ . Since A is a (, C , Z)-algebra, so is δ n A. Therefore,
φ n θ 0 ( ) = ψ 0 ( ) >A(n) ψ 0 (r) = φ n θ (r)• Case (Fun). Similarity to the case (Fun) in the proof of Proposition 5.9.

https://doi.org/10.1017/S0960129522000287 Published online by Cambridge University Press

Mathematical Structures in Computer Science

29

Theorem 9.5. A binding CS (, C , Z) is meta-terminating on all binding meta-terms if and only
if there is a well-founded (, C , Z)-algebra.
Proof. (⇐): Let A be a well-founded (, C , Z)-algebra. Assume that C is not meta-terminating,that is, there exists an infinite meta-rewriting sequenceZ nt1 C t2 C t3 C · · · .

By Proposition 9.4, for any admissible assignment φ : Z → A,
φ n (t1 ) >A(n) φ n (t2 ) >A(n) φ n (t3 ) >A(n) · · · .
This contradicts well-foundedness of >A .
(⇒): When a CS C is meta-terminating, the (, C , Z)-algebra (B Z, C ) is a desired wellfounded one because the relation C is well-founded.
Corollary 9.6. Let (, C , Z) be a binding CS. If there is a well-founded (, C , Z)-algebra, then C
is terminating.
Proof. It is clear that the meta-termination of C on binding meta-terms implies the terminationof C on terms because all terms are binding meta-terms.
Hence, in the case of binding CSs this becomes an interesting termination proof method byinterpretation because we do not need a monoid structure.
Example 9.7. (Prenex normal forms) We show the termination of the binding CS (, C , Z)
for conversion into prenex normal forms given in the introduction. Formally, it is given by thesignature  = {∀, ∃ : 1, ∧, ∨ : 0, 0, ¬ : 0} and the metavariable set Z = {P(0) , Q(1) }. The set C
of rules in de Bruijn levels is obtained by just replacing the variable x with 1.
Z 0

P ∧ ∀(1.Q[1])⇒ ∀(1.P ∧ Q[1])Z 0¬∀(1.Q[1])⇒ ∃(1.¬(Q[1]))Z 0∀(1.Q[1]) ∧ P⇒ ∀(1.P ∧ Q[1])Z 0¬∃(1.Q[1])⇒ ∀(1.¬(Q[1]))We use Theorem 9.5 to show termination. Take a (V+)-algebra K such that the carrier is K(n) =N with >K(n) by the standard order > on N for all n ∈ N, and the operations are given byν Kn (i) = 0¬Kn (x) = 2x

∧Kn (x, y) = ∨Kn (x, y) = 2x + 2y
∀Kn (x) = ∃Kn (x) = x + 1.

All operations are monotone. We show that K satisfies the rules: take an assignment φ : X → δ n K
by P  → x ∈ N and Q  → y ∈ N, thenφ 0 (P ∧ ∀(1.Q[1])) = 2x + 2(y + 1) >K(0) (2x + 2y) + 1 = φ 0 (∀(1.P ∧ Q[1]))φ 0 (¬∃(1.Q[1])) = 2(y + 1) >K(0) 2y + 1 = φ 0 (∀(1.¬(Q[1]))).
The interpretations of other rules are similarly calculated. Since >K(n) = > is well-founded, thisshows K forms a well-founded (, C , Z)-algebra. Thus, the binding CS C is terminating on all
terms by Corollary 9.6.
This interpretation is much simpler than the -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 secondorder function symbols such as ∀, ∃, λ, λ.

https://doi.org/10.1017/S0960129522000287 Published online by Cambridge University Press

30

M. Hamana

Example 9.8. (CPS translation) The binding CS S for a CPS translation in Example 3.3
CPS(E0 ) ⇒ λk.([E0 ]) (λm.km)([V])⇒ λk.k V([λx.E[x]]) ⇒ λk.k (λx.λk.([E[x]]) (λm.km))([E0 E1 ])⇒ λk.([E0 ]) (λm.([E1 ]) (λn.mn(λa.k a)))is shown to be terminating by the following polynomial interpretation: take a (V+)-algebra K
where the carrier K(n) = N, the unit ν Kn (x) = 0, and the operations:
CPSKn (e) = 5e + 5([e])Kn = 5e + 1(e0 e1 )Kn = e0 + e1K

λn (e) = e

λKn (e) = e + 1(e0 e1 )Kn = e0 + e1 + 1.

The (V+)-algebra K satisfies the rules. We take an assignment φ : Z → δ n K by E  → e ∈ N, V  →v ∈ N, E0  → e0 ∈ N, E0  → e0 ∈ N. Then all rules are decreasing. For instance, the interpretationof the last rule is decreasing as
φ 0 (([E0 E1 ])) = 5(e0 + e1 + 1) + 1 > 5e0 + 1 + (5e1 + 1 + 3)
= φ 0 (λk.([E0 ]) (λm.([E1 ]) (λn.mn(λa.k a)))).
Hence C is terminating by Corollary 9.6.
Example 9.9. (A theory of π-calculus) As the final example, we consider an example takenfrom a theory of π-calculus given by Stark. The π-calculus of Milner is one of the most fundamental concurrent calculi (Milner, 1999). Stark gave a free algebra model of π-calculus (Stark,2008). A theory of π-calculus consists of 12 axioms. In Hamana (2019), we have analysed thatthe 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 π-calculus. We omit
writing contexts. The signature  isnil : in : 0, 1

tau : 0

sum : 0, 0

out : 0, 0, 0

new : 1and the set C of rules is given bynew(a.X)⇒X

sum(nil, X)⇒X

new(a.sum(X[a], Y[a])) ⇒ sum(new(a.X[a]), new(a.Y[a]))new(a.out(a, B, X[a]))⇒ nilnew(a.out(B, C, X[a])) ⇒ out(B, C, new(a.X[a]))new(a.in(B, c.X[a, c]))⇒ in(B, c.new(a.X[a, c]))new(a.tau(X[a]))⇒ tau(new(a.X[a]))new(a.in(a, b.X[a, b]))⇒ nil

This is a binding CS. Now we take the (V+)-algebra K where the carrier K(n) = N and theoperations:ν Kn (x) = 0 new(x) = 2x + 1 out(x, y, z) = 2x + 2y + 2z + 2
tau(x) = 2x + 2 in(x, y) = 2x + 2y + 2 sum(x, y) = 2x + 2y + 4 nil = 1
The (V+)-algebra K satisfies the rules. We take an assignment φ : Z → δ n K that assigns
x, y, b, c ∈ N to metavariables X, Y, B, C, respectively. Then all rules are decreasing. For instance,
https://doi.org/10.1017/S0960129522000287 Published online by Cambridge University Press

Mathematical Structures in Computer Science31

the interpretation of the third rule is decreasing as
φ n (new(a.sum(X[a], Y[a]))) = 2(2x + 2y + 4) + 1 > 2(2x + 1) + 2(2y + 1) + 4= φ n (sum(new(a.X[a]), new(a.Y[a])))Hence 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 secondorder CSs. Restricting the algebraic structures to those equipped with well-founded relations, wehave obtained complete characterisations of terminating CSs. We have also extended the characterisation to rewriting on meta-terms using the notion of -monoids. A known model ofhigher-order rewrite rules given by hereditary monotone functionals has been shown to be an
instance of -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.

Notes
1 It is finitary, hence the initial algebra exists (Adamek, 1974).
2 A signature functor has a canonical strength st : (A) • A → (A • A) (Tanaka and Power, 2006, Theorem 6.3) (Fiore,2008, Corollary 7).

References
Aczel, P. (1978). A General Church-Rosser Theorem. Technical report, University of Manchester.
Adamek, J. (1974). Free algebras and automata realizations in the language of categories. Commentationes Mathematicae
Universitatis Carolinae 15 (589602).
Blanqui, F. (2000). Termination and confluence of higher-order rewrite systems. In: Rewriting Techniques and Application(RTA 2000), LNCS, vol. 1833. Springer, 47–61.
Blanqui, F. (2016). Termination of rewrite relations on λ-terms based on Girard’s notion of reducibility. Theoretical Computer
Science 611 50–86.
Blanqui, F., Jouannaud, J.-P. and Okada, M. (1999). The calculus of algebraic constructions. In: Rewriting Techniques andApplications (RTA 1999), LNCS, vol. 1631. Springer, 301–316.
Blanqui, F., Jouannaud, J.-P. and Okada, M. (2002). Inductive data type systems. Theoretical Computer Science 272 41–68.
Cohn, P. (1965). Universal Algebra. Harper & Row.
Danvy, O. and Rose, K. (1998). Higher-order rewriting and partial evaluation. In: Rewriting Techniques and Applications, 9thInternational Conference, (RTA’98), LNCS, vol. 1379.
de Bruijn, N. (1972). Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, withapplication to the Church-Rosser theorem. Indagationes Mathematicae 34 381–391.
Despeyroux, J., Felty, A. and Hirschowitz, A. (1995). Higher-order abstract syntax in Coq. In: Typed Lambda Calculi andApplications, LNCS, vol. 902, 124–138.
Fiore, M. (2002). Semantic analysis of normalisation by evaluation for typed lambda calculus. In: 4th International Conference
on Principles and Practice of Declarative Programming (PPDP 2002). ACM Press, 26–37.
Fiore, M. (2008). Second-order and dependently-sorted abstract syntax. In: LICS’08, 57–68.
Fiore, M. and Hamana, M. (2013). Multiversal polymorphic algebraic theories: Syntax, semantics, translations, and equational
logic. In: 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS, vol. 2013, 520–529.
Fiore, M. and Hur, C.-K. (2010). Second-order equational logic. In: CSL’10, LNCS, vol. 6247, 320–335.
Fiore, M. and Mahmoud, O. (2010). Second-order algebraic theories. In: MFCS’10, LNCS, vol. 6281, 368–380.
Fiore, M., Plotkin, G. and Turi, D. (1999). Abstract syntax and variable binding. In: Proceedings of 14th Annual Symposiumon Logic in Computer Science, 193–202.

https://doi.org/10.1017/S0960129522000287 Published online by Cambridge University Press

32

M. Hamana

Gandy, R. (1980). Proofs of strong normalization. In: Seldin, J. P. and Hindley, J. R. (eds.) To H.B. Curry: Essays on
Combinatory Logic, Lambda Calculus and Formalism. Academic Press Limited.
Hamana, M. (2003). Term rewriting with variable binding: An initial algebra approach. In: Fifth ACM-SIGPLAN International
Conference on Principles and Practice of Declarative Programming (PPDP’03), 148–159.
Hamana, M. (2004). Free -monoids: A higher-order syntax with metavariables. In: Asian Symposium on Programming
Languages and Systems (APLAS 2004), LNCS, vol. 3302, 348–363.
Hamana, M. (2005). Universal algebra for termination of higher-order rewriting. In: RTA’05, LNCS, vol. 3467, 135–149.
Hamana, M. (2007). Higher-order semantic labelling for inductive datatype systems. In: PPDP’07, 97–108.
Hamana, M. (2011). Polymorphic abstract syntax via Grothendieck construction. In FoSSaCS’11, LNCS, vol. 3467, 381–395.
Hamana, M. (2017). How to prove your calculus is decidable: Practical applications of second-order algebraic theories andcomputation. Proceedings of the ACM on Programming Languages 1 (22) 1–28.
Hamana, M. (2019). How to prove decidability of equational theories with second-order computation analyser SOL. Journalof Functional Programming 29 (e20).
Hamana, M., Abe, T. and Kikuchi, K. (2020). Polymorphic computation systems: Theory and practice of confluence withcall-by-value. Science of Computer Programming 187 (102322).
Huet, G. and Lankford, D. S. (1978). On the uniform halting problem for term rewriting systems. Technical Report Rapport
Laboria 283, INRIA.
Jouannaud, J.-P. and Rubio, A. (2001). Higher-order recursive path orderings à la carte. In: International Workshop on
Rewriting in Proof and Computation (RPC’01), 161–175.
Klop, J. (1980). Combinatory Reduction Systems. PhD thesis, CWI, Amsterdam, vol. 127. Mathematical Centre Tracts.
Lescanne, P. and Rouyer-Degli, J. (1995). Explicit substitutions with de Bruijn’s levels. In: Rewriting Techniques andApplications, 6th International Conference (RTA-95), LNCS, vol. 914. Springer, 294–308.
Libal, T. and Miller, D. (2016). Functions-as-constructors higher-order unification. In: Proceedings of FSCD 2016, vol. 52.
LIPIcs, 26:1–26:17.
Mac Lane, S. (1971). Categories for the Working Mathematician, vol. 5. Graduate Texts in Mathematics. Springer-Verlag, NewYork.
Mayr, R. and Nipkow, T. (1998). Higher-order rewrite systems and their confluence. Theoretical Computer Science 192 (1)
3–29.
Miculan, M. and Scagnetto, I. (2003). A framework for typed HOAS and semantics. In: Proceedings of PPDP’03. ACM Press,
184–194.
Miller, D. (1991). A logic programming language with lambda-abstraction, function variables, and simple unification. Journalof Logic and Computation 1 (4) 497–536.
Milner, R. (1999). Communicating and Mobile Systems - The π -Calculus. CUP.
Pfenning, F. and Elliott, C. (1988). Higher-order abstract syntax. In: Proceedings of the ACM SIGPLAN ’88 Symposium on
Language Design and Implementation, 199–208.
Plotkin, G. (1998). Binding algebras: A step between universal algebra and type theory (invited talk). In: Rewriting Techniquesand Applications, 9th International Conference, RTA’98, Tsukuba, Japan.
Stark, I. (2008). Free-algebra models for the π -calculus. Theoretical Computer Science 390 (2–3) 248–270.
Tanaka, M. and Power, J. (2006). A unified category-theoretic semantics for binding signatures in substructural logics. Journalof Logic and Computation 16 (1) 5–25.
Taylor, W. (1993). Abstract clone theory. Algebras and Orders 389 507–530. NATO ASI Series C.
Turi, D. and Plotkin, G. (1997). Towards a mathematical operational semantics. In: Proceedings of the Twelfth Annual IEEE
Symposium on Logic in Computer Science, LICS ’97, 280–291.
van de Pol, J. (1994). Termination proofs for higher-order rewrite systems. In: The First International Workshop on HigherOrder Algebra, Logic and Term Rewriting (HOA’93), LNCS, vol. 816, 305–325.
van de Pol, J. (1996). Termination of Higher-order Rewrite Systems. PhD thesis, Universiteit Utrecht. https://cs.au.dk/
jaco/papers/thesis.pdf
Yokoyama, T., Hu, Z. and Takeichi, M. (2003). Deterministic higher-order patterns for program transformation. In: Logic
Based Program Synthesis and Transformation, 13th International Symposium LOPSTR 2003, Uppsala, Sweden, August 25–
27, 2003, Revised Selected Papers, 128–142.
Yokoyama, T., Hu, Z. and Takeichi, M. (2004). Deterministic second-order patterns. Information Processing Letters 89 (6)309–314.
Zantema, H. (1994). Termination of term rewriting: Interpretation and type elimination. Journal of Symbolic Computation
17 23–50.

Cite this article: Hamana M (2022). Complete algebraic semantics for second-order rewriting systems based on abstract
syntax with variable binding. Mathematical Structures in Computer Science. https://doi.org/10.1017/S0960129522000287

https://doi.org/10.1017/S0960129522000287 Published online by Cambridge University Press