Universal Algebra for
Termination of Higher-Order Rewriting
Makoto Hamana
Department of Computer Science, Gunma University, Japan
hamana@cs.gunma-u.ac.jp

Abstract. We show that the structures of binding algebras and Σmonoids by Fiore, Plotkin and Turi are sound and complete models of
Klop’s Combinatory Reduction Systems (CRSs). These algebraic structures play the same role of universal algebra for term rewriting systems. Restricting the algebraic structures to the ones equipped with wellfounded relations, we obtain a complete characterisation of terminating
CRSs. We can also naturally extend the characterisation to rewriting on
meta-terms by using the notion of Σ-monoids.

1

Introduction

At RTA’98, Plotkin presented the theory of binding algebras [Plo98], which aimed
to apply ideas in universal algebra to type theory. It is interesting that this wasgiven as an invited talk at RTA. That is to say, in the context of rewriting,it can be read as a possibility of a new direction of foundation of higher-orderrewriting as a type theoretic system. Plotkin’s idea of binding algebras was
inspired by Aczel’s work [Acz78]. In the field of rewriting, also inspired by Aczel’s
same work, Klop invented a system of higher-order rewriting called Combinatory
Reduction System (CRS) [Klo80]. It is natural to think that these two works,
having a common origin, have some relationship. However, such a relationshipis not obvious, especially about how the seemingly complex syntax of CRSs canbe understood in the theory of binding algebras.
Plotkin’s program of binding algebras later produced the notion of Σ-monoids[FPT99]. Interestingly, the free Σ-monoids constructed in [Ham04] is the sameas the syntax of “meta-terms” of CRSs (cf. Theorem 5). This similarity suggeststhat the universal algebra for CRSs may be Σ-monoids. Based on this idea, thepresent paper provides a complete algebraic characterisation of CRSs.
Contribution. Complete characterisation of terminating CRSs obtained in thispaper provides a method of proving the termination of CRSs by algebraic interpretation. The following CRS R for conversion into prenex normal form, i.e.
pushing quantifiers outside, is a typical example of higher-order rewrite rulesthat require the feature of variable binding [Pol96, Raa]:p ∧ ∀(x.q[x]) → ∀(x.p ∧ q[x])∀(x.q[x]) ∧ p → ∀(x.p ∧ q[x])¬∀(x.q[x]) → ∃(x.¬(q[x]))¬∃(x.q[x]) → ∀(x.¬(q[x]))J. Giesl (Ed.): RTA 2005, LNCS 3467, pp. 135–149, 2005.
c Springer-Verlag Berlin Heidelberg 2005°

136

Makoto Hamana

with the similar rewrite rules for ∨ and ∃ at the left column. Intuitively, rewriting using R and its termination are clear; notwithstanding, the application ofexisting proof methods in the theory of higher-order rewriting to the CRS R isnot so straightforward [JR01], or it requires consideration of an involved function
space to interpret binders [Pol96, Pol94]. The present paper provides a simpler
method of showing termination of CRS such as R (cf. Example 24).
Organisation. This paper is organised as follows. We first review the definitionof CRSs in Section 2. We then introduce the notion of “structural CRSs”. define
a class of structurally well-formed CRSs in Section 3. Section 4 gives algebraic
semantics of CRSs syntax and valuations. Section 5 gives algebraic semantics
of CRSs rewriting. Section 6 gives algebraic semantics of CRSs meta-rewriting.
Finally, in Section 7, we show examples of termination proofs using a result of
this paper.
Future work. This work opens a new direction of model theoretic study ofhigher-order rewriting. An immediate application will be semantic labelling method[Zan94] for CRSs using the algebraic structure developed in this paper. Recursive
path ordering on free structures in more general setting is also hopeful.

2

Combinatory Reduction Systems

We review the definition of CRSs. We use the definition of the standard reference[KOR93] of CRSs with a slight modification of syntax used in [DR98]: −.− and−[−] instead of ordinary ones [−]− and −(−) in [KOR93].
CRS. Assume a signature Σ of function symbols F l with arity, metavariables zl
with arity (in both cases the superscript l ∈ N is the arity).
(i) CRS terms have the formt ::= x | x.t | F l (t1 , . . . , tl ).
The three forms are respectively called variables, abstractions, and function
terms.
(ii) CRS meta-terms extend CRS terms tot ::= x | x.t | F l (t1 , . . . , tl ) | zl [t1 , . . . , tl ].
The last form is called a meta-application.
(iii) A valuation θ is a mapping that assigns to n-ary metavariable z an n-ary
substitute (a meta-level lambda notation, cf. [KOR93]):
θ:z- λ(x1 , . . . , xn ).t(1)

Valuations are extended to a function on meta-terms:
θ(x) = xθ(x.t) = x.θ(t)θ(F (t1 , . . . , tl )) = F (θ(t1 ), . . . , θ(tl ))θ(z[t1 , . . . , tl ]) = θ(z) (θ(t1 ), . . . , θ(tl ))(2)

Universal Algebra for Termination of Higher-Order Rewriting

137

Note that the rhs of the equation (2) uses an application at the meta-levelto the substitute. The valuation is safe if there are no two substitutes θ(z)and θ(z’) such that θ(z) contains a free variable x which appears also boundin θ(z’).
(iv) CRS rules, written l → r, consist of two meta-terms l and r with the following additional restrictions:(iv-a) l and r are closed (w.r.t. variables) meta-terms,(iv-b) l must be a “pattern”, i.e. a function term where all meta-applications
have the form z[x1 , . . . , xn ] with distinct xi ,(iv-c) r can only contain meta-applications with meta-variables occurring in
the left-hand side.
The rewrite rule l → r is safe for θ, if for no z in l and r, the substituteθ(z) has a free variable x occurring in an abstraction x.− of l and r. A setof rewrite rules is called a CRS.
(v) The CRS rewrite relation →R is generated by context and safe valuation
closure of a given CRS R:
l→r∈R
safe θ
θ(l) →R θ(l)s →R tx.s →R x.t

s →R tF (. . . , s, . . .) →R F (. . . , t, . . .)where l → r must be safe for the safe valuation θ. The third rule means arewriting at the i-th argument of F .

3Structural CRSs

In this section, we introduce the notion of structural CRS as a class of wellformed CRSs. This idea of structural CRS is to treat only CRS (meta-)terms
built from binding signature (cf. Aczel’s contraction schemes [Acz78]). A binding
signature specifies how many binders are taken in arguments of each function
symbol.
Formally, a binding signature Σ is consisting of a set Σ of function symbols with an arity function a : Σ → N∗ . A function symbol of binding arity
hn1 , . . . , nl i, denoted by f : hn1 , . . . , nl i, has l arguments and binds ni variablesin the i-th argument (1 ≤ i ≤ l).
For a formal treatment of named variables modulo α-equivalence in CRSs,
we assume the method of de Bruijn levels [dB72, LRD95, FPT99] for the naming
convention of variables (N.B. not for metavariables) in CRSs. We also use theconvention that n ∈ N denotes the set {1, . . . , n} (n is possibly 0). Under the
method of de Bruijn levels, this n means the set of variables from 1 to n.
Definition 1. A (meta-)term t is called structural if t is built from a binding
signature Σ and consistent with the binding arities of function symbols in Σ.
Schematically, structural meta-terms have the form:t ::= x | F (x1 · · · xi1.t1 , . . . , x1 · · · xil.tl ) | zl [t1 , . . . , tl ]138

Makoto Hamana

where F has the binding arity hi1 , . . . , il i.
More precisely, structural meta-terms are defined as follows. Fix an N-indexed
set Z of metavariables defined by Z(l) , {z | z has arity l}. A meta-term t is
structural if n ` t is derived from the following rules.
x∈n
n `x

F : hi1 , . . . , il i ∈ Σ n+i1 ` t1 · · · n+il ` tln ` F ( n+1 . . . n+i1 .t1 , . . . , n+1 . . . n+il .tl )z ∈ Z(l) n ` t1 · · · n ` tl
n ` z[t1 , . . . , tl ]By these rules, a meta-term always follows the method of de Bruijn levels. Using
only the first two rules (or equivalently, assuming Z(l) = ∅ for all l), we obtainstructural terms under n.
The notion of structural is obviously extended to rewrite rules, CRS, andvaluations. A rewrite rule is called structural if all meta-terms in the rule are
structural. A CRS is structural if all rules are structural.
Definition 2. A valuation θ is structural if for any mapping by θ : z 7→
λ(x1 , . . . , xn ).t, t is a structural term and all variables in t are included in
x1 , . . . , xn .
Structual CRS is a fairly good assumption because we can easily find that
almost all concrete examples of CRSs considered in the literature are structural;
namely, we can easily find a suitable binding signature of a given “plain” CRS.
Actually, in Raamsdonk’s collection [Raa] of examples of higher-order rewrite
systems all CRSs are structural .
Example 3 (CPS translation). The format of structural CRS is very similar
to an “everyday” meta-language for expressing formal systems in computer science and logic. An example is the structural CRS R for prenex normal form in
the introduction. Another example related to theory of programming languages
is the following CRS S of a call-by-value CPS translation [DR98].
Assume the metavariables Z = {v0 , e1 , (e0 )0 , (e1 )0 } and the binding signature Σ consisting of the function symbols λ, λ : h1i, (− −), (− −) : h0, 0i,
CPS, ([−]) : h0i. We write the structural CRS S of CPS translation in two ways:
the left column is written in the usual named notation, and the right column iswritten in de Bruijn level notation, which is the format we use in this paper.
CPS(e)→ λk.([e]) (λm.km)
CPS(e)→ λ1.([e]) (λ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 variablenames with numbers according to their (de Bruijn’s) levels. Notice that thiscompletely differs from the more well-known method of de Bruijn indexes. Metaterms in de Bruijn levels are just “normal forms” of α-equivalent meta-terms (e.g.
λk.k v =α λ1.1 v).

Universal Algebra for Termination of Higher-Order Rewriting139

Is the structural CRS S terminating1 ? Intuitively, termination is clear because ([−]) recursively decomposes a λ-term. In this paper, we derive a formal
way of showing termination from an algebraic characterisation of rewriting of
CRS. How this S is shown to be terminating will be given in Example 25 at theend of the paper.

4

Algebraic Semantics of Syntax

In this section and in the next section, we consider algebraic semantics of CRSs.
As far as the author knows, this is the first algebraic consideration of CRSs.
The basic idea is similar to the algebraic semantics of TRSs by monotone Σalgebras popularized by Zantema [Zan94]. But the framework of usual first-orderuniversal algebra is insufficient. We consider CRS’s syntax in the framework ofbinding algebras by Fiore, Plotkin and Turi [FPT99].
4.1

Binding Algebras

We review the notion of binding algebras. For detail, see [FPT99]. Let F be thecategory which has finite cardinals n = {1, . . . , n} (n is possibly 0) as objects,
and all functions between them as arrows m → n. This is the category of object
variables by the method of de Bruijn levels (i.e. natural numbers) and theirrenamings. We use the functor category SetF . We define the functor δ : SetF →SetF as follows: for L ∈ SetF , n ∈ F, ρ ∈ arr F, (δL)(n) = L(n + 1), (δL)(ρ) =L(ρ + id1 ). To a binding signature
Σ, we associate
the signature functor Σ :`Q
SetF → SetF given by ΣA , f :hn1 ,...,nl i∈Σ 1≤i≤l δ ni A. A Σ-binding algebra(or simply Σ-algebra) is a pair (A, α) consisting of a presheaf A ∈ SetF and amap ([ ] denotes a copair of coproducts) α = [fA ]f ∈Σ : ΣA - A called algebra- A defined forstructure, where fA is an operation fA : δ n1 A × . . . × δ nl A
each function symbol f : hn1 , . . . , nl i ∈ Σ.
The “the presheaf of variables” V ∈ SetF is defined by V(n) = n, V(ρ) =ρ (ρ : m → n ∈ F). Then, (SetF , •, V) forms a monoidal category [Mac71],
where the “substitution” monoidal
product is defined as follows. For presheaves`
A and B, (A • B)(n) , ( m∈N A(m)×B(n)m )/ ∼ where ∼ is the equivalence
relation generated by (t; uρ1 , . . . , uρm ) ∼ (A(ρ)(t); u1 , . . . , ul ) for ρ : m → l ∈ F.
Throughout the paper, we use the following notation: an element of A(m) ×B(n)m is denoted by (t; u1 , . . . , um ) where t ∈ A(m) and u1 , . . . , um ∈ B(m). A
representative of an equivalence class in A•B(n) is also denoted by this notation.
Let Σ be a signature functor with strength st defined by a binding signature.
A Σ-monoid M = (α, η, µ) consists of a monoid object [Mac71] (M, η : V →M, µ : M • M → M ) in the monoidal category (SetN , •, V) with a Σ-binding
algebra α : ΣM → M satisfying µ ◦ (α • idM ) = α ◦ Σµ ◦ st. A Σ-monoid
morphism (M, α) - (M 0 , α0 ) is a morphism in SetF which is both Σ-algebra
homomorphism and monoid morphism.
1

This does not contain β-reduction rules, i.e. only for translation.

140

4.2

Makoto Hamana

Algebra of Structural CRS Terms

Structural terms and meta-terms have a good algebraic structure. We define thepresheaf TΣV ∈ SetF of all structural terms under n by TΣV(n) = {t | n `t, t is a term} with obvious arrow part [Ham04]. We also define the map ν :- TΣV in SetF by ν(n) : V(n)- TΣV(n), x- x. We abbreviateVn+1, . . . , n+k.t to n+~k.t. For every f ∈ Σ with the arity hi1 , . . . , il i, we define
the map FT : δ i1 TΣV×· · ·×δ il TΣV - TΣV in SetF by (t1 , . . . , tl ) - F (n+i~1 .t1 , . . . , n+ ~il .tl ).
Theorem 4. Structural CRS terms TΣV forms an initial V + Σ-binding algebra.
Proof. Due to [FPT99]. The “syntactic algebra” in ([FPT99] Theorem 2.1) isnothing but the V + Σ-algebra (TΣV, [ν, [FTΣ ]F ∈Σ ]).
utMoreover, let Z be an arbitrary N-indexed set of metavariables (cf. Sect. 3).
The presheaf MΣ Z of meta-terms is defined byMΣ Z(n) = {t | n ` t}.
- MΣ Z in SetF , called multiplication,
There is the map β : MΣ Z • MΣ Z
that performs a substitution for variables [Ham04].
Theorem 5. Structural
CRS meta-terms MΣ Z forms a free Σ-monoid over Ẑ,`
where Ẑ(n) = k∈N F(k, n)×Z(k).
Proof. Due to [Ham04]. For Ẑ ∈ SetN , the free Σ-monoid constructed in [Ham04]
is nothing but (MΣ Z, [FMΣ ]F ∈Σ , ν, β) by just identifying minor notational difference of terms: regard ovar(x), [n]t, dzeht1 , . . . , tl i in [Ham04] as x, n.t, z[t1 , . . . , tl ]respectively in the present paper. Here, operations FMΣ are defined by the sameas FTΣ .
ut
4.3

Algebraic Characterisation of Valuations
Definition 6. An assignment φ : Z - A is a morphism of SetN whose target
A has a Σ-monoid structure (A, ν, β).
Notice that Z in the above definitions is a presheaf in SetF . So just an Nindexed set X of metavariables cannot be the source of this presentation ofvaluation. Fortunately, we `can always construct a presheaf from an N-indexed
set X by defining X̂(n) , k∈N F(k, n)×X(k) (see [Ham04] Sect. 5.2). Hence,
hereafter we abuse the notation to use X to denote its presheaf version X̂ ∈ SetF
in an assignment.
An assignment φ is extended to a Σ-monoid morphism φ∗ : MΣ Z - A:
MΣ Z(n)x
F (n+ i~1 .t1 , . . . , n+ ~il .tl )z[t1 , . . . , tl ]- A(n)- ν(n)(x)(x ∈ n)- FA (n+ i~1 .φ∗ (n+i1 )(t1 ), . . . , n+ ~il .φ∗ (n+il )(tl ))- β(n)( φ(l)(z); φ∗ (n)(t1 ), . . . φ∗ (n)(tl ) )where f : hi1 , . . . , il i ∈ Σ. In the special case A = TΣV, we have

Universal Algebra for Termination of Higher-Order Rewriting141- TΣ V gives a structural valuation,
Proposition 7. An assignment θ : Z∗
TΣV gives its “homomorphic” extension on meta-terms.
and θ : MΣ Z
To see why, first we note that the assignment θ is a family of maps θ(n) :Z(n) - TΣV(n) such that
θ(n) : z- t ∈ TΣV(n).

Namely, it maps an n-ary metavariable z to some structural term t under n.
Comparing the definition of structural valuation with this, and regarding thesubstitute λ(x1 , . . . , xn ).t as t ∈ TΣV(n) (because θ is structural), both definitions coincide. Hence, hereafter we use the word “valuation” in this sense:
Definition 8. A valuation is an assignment θ : Z - TΣV into the Σ-monoidof terms. Also, we use the following: a meta-valuation is an assignment θ :Z - MΣ X into the Σ-monoid of meta-terms.
Now we know in what sense θ∗ is a “homomorphic” extension of a valuation
θ (which is not explained formally in the ordinary definitions [KOR93, OR94,
DR98, Oos94]). Namely θ∗ is a Σ-monoid morphism, which preserves Σ-algebra
structure (i.e. Σ-homomorphism) and monoid structure.
4.4

Structural Valuations are Sufficient

A valuation in the original sense (Sect. 2) was a map θ : z 7→ λ(x1 , . . . , xn ).t
where t is an arbitrary term, which means that λ(x1 , . . . , xn ).t may have variables
other than x1 , . . . , xn . But in the case of a structural valuation, variables in t
are taken only from x1 , . . . , xn . We show that structural valuations are sufficientto generate CRS rewrite relation on terms if we make some weakening of rules.
For m ≤ m0 , let ρ : N → N be the function defined by ρ(m + i) , m0 + i
for each i ∈ Z. Suppose N-indexed metavariable sets Z 0 = Y ∪ {zm }, Z =0Y ∪ {zm }, z 6∈ Y . The weakening of the arity of the metavariable z by ρ fromm to m0 is a function ρz on (unstructural) meta-terms defined as follows.
ρz (z[t1 , . . . , tm ]) = z[1, . . . , m0 − m, ρz (t1 ), . . . , ρz (tm )]ρz (n.t) = ρ(n).ρz (t) ρz (F (~t)) = F (ρz (~t)) ρz (x) = ρ(x)(x ∈ N).
Notation 9. We may use the notation Z|n ` s → t for a rule or a rewrite step
if metavariables and variables in s and t are included in Z and n respectively. We
may also simply write Z ` s → t or n ` s → t if another part is not important.
Let R be a structural CRS that follows the method of de Bruijn levels. Then
weakening closure of R, denoted by R◦ , is defined by the following inference
rules (i.e. the least set satisfying the rules):l→r∈Rl → r ∈ R◦

Y ∪ {zm } ` l → r ∈ R◦
Y ∪ {zm+j } ` ~j.ρz l → ~j.ρz r ∈ R◦

142

Makoto Hamana

where ρz is weakening of the arity of the metavariable z from m to m + j(j ∈ N is arbitrary). This means that although originally a metavariable zm canbe replaced with a term exactly containing m-variables, it will be weakened tozm+j , which can be replaced with a term containing m + j-variables.
Then, we reformulate the generation of rewrite relation as follows:n + i ` s ⇒R t~n ` F (. . . , n+ i.s, . . .) ⇒R F (. . . , n+~i.t, . . .)Z ` ~n.l → ~n.r ∈ R
n ` θ∗ (n)(l) ⇒R θ∗ (n)(r)where θ : Z :- TΣV is a valuation.

Proposition 10. For a structural CRS R that follows the method of de Bruijn
levels, the ordinary definition (cf. Sect. 2) and the above definition with R◦
generate the same rewrite relation on structural terms, i.e. s ⇒R◦ t iff s →R t
for structural terms s, t.

5

Algebraic Semantics of Rewriting

In this section, we interpret rewrite rules of structural CRSs by Σ-binding algebras, and give a complete characterisation of termination in this framework.
Hereafter, in this paper we only consider structural CRSs. So we just say “aCRS” for a structural CRS.
For a presheaf A, we write >A for a family of transitive relations {>A(n) }n∈N ,where >A(n) is a transitive relation on the set A(n) for each n ∈ N. In this paper,
we use the following notion of monotonicity [Zan94].
Definition 11. Let (A1 , >A1 ), . . . , (Al , >Al ), (B, >B ) be presheaves equippedwith transitive relations. A map f : A1 ×· · ·×Al - B in SetF is monotone if
all a1 , b1 ∈ A1 (n), . . . , al , bl ∈ Al (n) with ak >A(n) bk for some k and aj = bj for
all j 6= k, then f (n)(a1 , . . . , al ) >B(n) f (n)(b1 , . . . , bl ).
We interpret rewrite rules in a V+Σ-algebra.
Definition 12. Let A be a V + Σ-algebra. A term-generated assignment φ :Z - A is a morphism of SetN that is expressed as the composite
Z

θ

- TΣV

!A

- A

for some valuation θ, where !A is the unique V + Σ-algebra homomorphism fromthe initial V+Σ-algebra TΣV. Throughout the paper, we denote by !A this uniqueV + Σ-homomorphism.
This means that an interpretation of a metavariable z by a term-generated assignment θ is performed by firstly assigning to z some term t and then interpreting the term in a V+Σ-algebra A. Why this is needed is that CRS rewrite relationis generated on terms (not on meta-terms). So, to interpret CRS rewrite rules,
not all assignments are needed; only term-generated assignments are sufficient.

Universal Algebra for Termination of Higher-Order Rewriting

143

Definition 13. A monotone V + Σ-algebra (A, >A ) is a V + Σ-algebra A =- A), equipped with a transitive relation(A, [ν, [FA ]F ∈Σ ]), (where ν : V>A(n) on A(n) for each n ∈ N such that every operation fA is monotone. Moreover, if >A(n) is a well-founded strict partial order for each n ∈ N, A is called
well-founded .
Definition 14. Let R be a CRS. A monotone V+Σ-algebra (A, >A ) satisfies a
CRS rewrite rule Z ` ~n.l → ~n.r ifφ∗ (n)(l) >A(n) φ∗ (n)(r)- A. A (V +Σ, R)-algebra A is a
for all term-generated assignments φ : Z
monotone V+Σ-algebra A that satisfies all rules in the weakening closure R◦ .
+Define the N-indexed transitive relation →+R(n) , {(s, t) | n ` s ⇒R◦ t},where the latter (−)+ denotes the transitive closure.

Theorem 15. For a CRS R, (TΣV, →+R ) is an initial (V + Σ, R)-algebra, i.e.
for any (V + Σ, R)-algebra A, there exists a unique monotone homomorphism
TΣV - A.
Proof. Let (A, >A ) be a (V+Σ, R)-algebra. Since TΣV is an initial V+Σ-algebra- A is a unique V + Σ-algebra homomorphism. So,(Theorem 4), !A : TΣV
the remaining task is to show !A is monotone. This is proved by induction on
the structure of inference of ⇒R and induction on the length of ⇒+ . Note that!A ◦ θ is term-generated and all operations FA on A are monotone.
ut
The following states that (V + Σ, R)-algebras are sound and complete formany-step rewrite relation (where Notation 9 is used).
Corollary 16. Let R be a CRS. The followings are equivalent:(i) n ` s →+R t holds,(ii) !A (n)(s) >A(n) !A (n)(t) for all (V+Σ, R)-algebras (A, >A ).
Proof. (i)⇒(ii): By Theorem 15.
(ii)⇒(i): Take (A, >A ) = (TΣV, →+
R ).

u
t

Restricting the above corollary to the case of well-founded monotone algebras,
we obtain a complete characterisation of terminating CRSs.
Theorem 17. A CRS R is terminating if and only if there is a well-founded(V+Σ, R)-algebra.
Proof. (⇐): Let A be a well-founded (V + Σ, R)-algebra. Assume R is nonterminating, i.e. there exists an infinite reduction sequence n ` t1 →R t2 →R· · · . By Corollary 16, we have !A (n)(t1 ) >A(n) !A (n)(t2 ) >A(n) · · · . This contradicts well-foundedness of >A .
(⇒): When a CRS R is terminating, the initial (V +Σ, R)-algebra (TΣV, →+R)
is a desired well-founded algebra, because the strict partial order →+iswellR
founded.
ut

144

Makoto Hamana

Example 18 (Incompleteness of functional interpretation [Pol96]). Assume the metavariables Z = {f1 , x1 } and the binding signature Σ = {c : h0i}.
Consider the CRS R consisting of the following only:c(f[f[x[1]]]) → f[x[1]].
We want to show termination of R. Intuitively, this termination seems easy to
be proved because with any rewrite step the number of c-symbols decreases.
Nevertheless the existing interpretation method of higher-order rewriting basedon the model of hereditary monotone functionals cannot show termination of R
due to incompleteness of the model [Pol94, Pol96]. In contrast to it, we can show
termination of R by using Theorem 17 as follows. Take the monotone V + Σalgebra (TΣV, ÂTΣV ) where s ÂTΣV(n) t iff the number of c-symbols in s and t
decreases. Notice that now all terms in TΣV(n) are consisting of c and variables
in n only. Hence, all assignments into TΣV are of the forms f 7→ ck (1), x 7→
cm (1) (k-times and m-times c’s). This gives a well-founded (V +Σ, R)-algebra(TΣV, ÂTΣV ), which implies termination of R by Theorem 17.

6

Algebraic Semantics of Meta-Rewriting

We go beyond the standard definition of rewriting of CRS, and consider rewriting
on meta-terms, which we call meta-rewriting. In the literature, although metarewriting has not been formally defined, Oostrom considered the notions of metaCR and meta-SN of CRS and pointed out each of them is not derived from CR
and SN of CRS respectively ([Oos94] Sect. 3.4).
We consider meta-termination, i.e. termination of meta-rewriting. In thissection, we give algebraic semantics of meta-rewriting. Basically we repeat thesemantics in Sect. 5, but we use Σ-monoids instead of Σ-binding algebras for thesemantics structure.
Rewriting on Meta-terms. First we formally define meta-rewriting. Let Z be
an N-indexed set of metavariables. For a CRS R in which any two rules havedisjoint metavariables taken from Z (if not, rename rules suitably), we denote
the CRS by (R, Z). We define the meta-rewriting relation ÃR as follows:~n.l → ~n.r ∈ R
n ` θ∗ (n)(l) ÃR θ∗ (n)(l)n+i ` s ÃR t~n ` F (. . . , n+ i.s, . . .) ÃR F (. . . , n+~i.t, . . .)z ∈ Z(l) n ` s ÃR tn ` z[. . . , s, . . .] ÃR z[. . . , t, . . .]- MΣ X (Definition 8). We say that R iswhere θ is a meta-valuation Z
meta-terminating if ÃR is well-founded.
Definition 19. A monotone Σ-monoid (A, >A ) is a Σ-monoid A equipped witha transitive relation >A(n) on A(n) for each n ∈ N such that every operation
is monotone. Moreover, if >A(n) is a well-founded strict partial order for eachn ∈ N, A is called well-founded .

Universal Algebra for Termination of Higher-Order Rewriting

145

Let R be a CRS. A monotone Σ-monoid A = (A, >A ) satisfies a rewrite ruleZ ` ~n.l → ~n.r ∈ R ifφ∗ (n)(l) >A(n) φ∗ (n)(r)for all assignments2 φ : Z - A. If A satisfies all rules in the weakening closureR◦ , it is called (Σ, R)-monoid .
An important example of (Σ, R)-monoid is (MΣ Z, Ã+R ).
Definition 20. Let (A, ν, β) be a monotone Σ-monoid, and φ : Z
assignment. Define the map σ : Z • A - A by the composite
Z •A

φ•idA

- A•A

- A anβ- A.

The assignment φ is called admissible if σ is monotone3 .
Notice that the multiplication β need not to be monotone. Actually, it israther difficult to find a Σ-monoid whose multiplication is monotone. The unit
ν : V - A is automatically monotone because V has no transitive relation.
The notion of admissible assignments is an important ingredient of interpretation of meta-rewriting. Arbitrary assignments are not suitable to interpretmeta-rewriting because it may cause non-order preservation. For example, assume the constants Σ = {a, b, c}, the metavariable Z = {z1 } and the CRS
R = {a → b}. Then we have a meta-rewriting z[a] ÃR z[b]. We interpret this- c.
rewrite step in the (Σ, R)-monoid (MΣ Z, Ã+
R ). Take the assignment φ : z
Then, this does not preserve the order:φ∗ (z[a]) = c 6ÃR c = φ∗ (z[b]).
We need “monotonic” interpretation of meta-rewriting to establish algebraic termination method. The idea of admissible assignment is motivated by to prohibit
this kind of “non-monotonic” interpretation of a rewrite step.
This problem is already recognised by van de Pol [Pol94]. The notion ofadmissible assignments is analogue to his notion of strict functionals. Actually,
we can show that hereditary monotone functionals in his model forms a monotone
Σ-monoid and our admissible assignments into this monotone Σ-monoid is thesame as the strict valuations at the second-order types. Hence, we can apply themethod of termination proof using hereditary monotone functionals to CRSs.
For instance, termination of the examples of higher-order rewrite systems given
in [Pol94, Pol96] (and their CRS versions are in [Raa]) can be shown by using
Σ-monoids of hereditary monotone functionals given in [Pol94, Pol96].
Now we show a theorem analogue to Theorem 15 stating (MΣ Z, Ã+R ) is an“initial model”. More precisely,
2
3Compare this definition `with Definition 14 for rewriting.
m- A(n) is monotone, i.e. if
More precisely, σ(n) :m∈N Z(m) × A(n) / ∼z ∈ Z(m) and all a1 , b1 ∈ A(n), . . . , am , bm ∈ A(n) with ak >A(n) bk for some k andaj = bj for all j 6= k, we have σ(n)(z; a1 , . . . , am ) >A(n) σ(n)(z; b1 , . . . , bm ).

146

Makoto Hamana

Theorem 21.
For a CRS (R, Z), (MΣ Z, Ã+R ) is a free(Σ, R)-monoid over Z, i.e. for any admissible assignment φ from Z into a (Σ, R)-monoid(A, >A ), there exists a unique Σ-monoid map
φ∗ that is monotone and makes the right diagram commute in SetF , where η Z : zl - z[1, . . . , l].

Z

ηZ
MΣ Z
@@
@
φR

φ∗
?
A

- A be an admissible assignment into a (Σ, R)-monoid
Proof. Let φ : Z(A, >A ). Since MΣ Z is a free Σ-monoid [Ham04], φ∗ is a unique Σ-monoid morphism that makes the above diagram commute in SetF . So, the remaining task
is to show φ∗ is monotone. This is proved by induction on the structure of inference of ÃR and the length of Ã+
R . The case for instantiation of a rewrite rule,
we use (φ∗ ◦ θ)∗ = φ∗ ◦ θ∗ , which is proved by induction on meta-terms. The
crucial case is to show φ∗ preserves the relation of z[. . . , s, . . .] ÃR z[. . . , t, . . .].
This holds because we have assumed that φ is admissible.
ut
Theorem 22. A CRS (R, Z) is meta-terminating if and only if there is a wellfounded (Σ, R)-monoid.
Proof. (⇐): Let A be a well-founded (Σ, R)-monoid. Assume R is not metaterminating, i.e. there exists an infinite meta-rewriting sequenceZ|n ` t1 ÃR t2 ÃR t3 ÃR · · · .
By Theorem 21, for any admissible assignment φ : Z- A, we haveφ∗ (n)(t1 ) >A(n) φ∗ (n)(t2 ) >A(n) φ∗ (n)(t3 ) >A(n) · · · .
This contradicts well-foundedness of >A .
(⇒): When a CRS R is meta-terminating, the free (Σ, R)-monoid (MΣ Z, Ã+R)over Z is a desired well-founded one, because the strict partial order Ã+iswellR
founded.
ut

7Termination of Binding CRSs

Let (R, X) be a CRS such that every meta-application in rules of R is always ofthe form zl [1, . . . , l]. We call such a CRS a binding CRS because it is essentiallymeta-application-free (cf. binding TRS [Ham03]). To interpret a rule and metarewriting in a binding CRS R, we do not need the monoid structure of Σmonoids, i.e. the multiplication β is not used. Because, for example, interpret- A into a
the meta-term z[1, 2] (for z2 ) in a rule by an assignment φ : X
Σ-monoid (A, ν, β):φ∗ (z[1, 2]) = β(φ(z); ν(1), ν(2)) = φ(z).
This is due to A • V ∼= A, i.e. V is the unit of the monoidal category SetF . So,
to interpret a meta-term like z[1, 2], we just need an assignment φ. Hence, weUniversal Algebra for Termination of Higher-Order Rewriting

147

assume A to be a X+V+Σ-algebra for interpretation of binding CRSs. Then we
can replete the discussion of interpretation of meta-rewriting: A satisfies a rule
- A into~n.l → ~n.r ∈ R if φ∗ (n)(l) >A φ∗ (n)(r) for all assignments φ : X
X +V+Σ-algebras. We denote by BΣ X an initial X +V+Σ-algebra and call anelement of it a binding meta-term. Notice that a binding CRS is a CRS built
only from binding meta-terms.
We define the meta-rewriting on binding metaS
terms by →R ,ÃR ∩ n∈N (BΣ X × BΣ X)(n). Then, (BΣ X, →+R ) is an initial(X +V+Σ, R)-algebra.
Proposition 23. A binding CRS (R, X) is meta-terminating on binding metaterms if and only if there is a well-founded (X +V+Σ, R)-algebra.
For a binding CRS R, it is clear that meta-termination of R on binding
meta-terms implies termination of R on terms because all terms are binding
meta-terms (meta-application-free). Hence, in the case of binding CRSs thisbecomes an interesting termination proof method by interpretation because we
do not need a monoid structure.
Example 24. We show termination of the CRS R for conversion into prenex
normal form in the introduction. Formally, R is built from the binding signatureΣ = {∀, ∃ : h1i, ∧, ∨ : h0, 0i, ¬ : h0i} and the metavariables X = {p0 , q1 }. The
structural CRS R in de Bruijn levels is obtained by just replacing the variable
x with 1.
p ∧ ∀(1.q[1]) → ∀(1.p ∧ q[1])∀(1.q[1]) ∧ p → ∀(1.p ∧ q[1])¬∀(1.q[1]) → ∃(1.¬(q[1]))¬∃(1.q[1]) → ∀(1.¬(q[1])).

We use Proposition 23 to show termination. Take the X +V +Σ-algebra K by
K(n) = N with >K(n) by the usual order > on N for all n ∈ N. The operations
are given by∧K(n) (x, y) = ∨K(n) (x, y) = 2x + 2y
¬K(n) (x) = 2x∀K(n) (x) = ∃K(n) (x) = x + 1.
All operations are monotone. We can show that K satisfies the rules: take anassignment φ : X - K by p 7→ x ∈ N and q 7→ 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]))).
Similar for other rules. Since >K(0) is well-founded, this shows K with φ is a wellfounded (X +V+Σ, R)-algebra. Thus, the binding CRS R is meta-terminating
on binding meta-terms by Proposition 23. Hence R is terminating on all CRS
terms. This interpretation is simpler than the hereditary monotone functionalmodel given in [Pol96].

148

Makoto Hamana

Example 25. The CRS S for a CPS translation in Example 3 is also shown to
be terminating by the following polynomial interpretation: take the X +V+Σalgebra K by K(n) = N with the unit ν : V → K, i 7→ 0 and the operations:CPSK(n) (e) = 5e + 5([e])K(n) = 5e + 1(e0 e1 )K(n) = e0 + e1

λK(n) (e) = e λK(n) (e) = e + 1(e0 e1 )K(n) = e0 + e1 + 1.

Checking this satisfies S is just by calculation. Hence S is terminating.
Namely, if a CRS is a binding CRS, we do not need functionals to interprethigher-order function symbols such as ∀, ∃, λ, λ.
Acknowledgments. I am grateful to Gordon Plotkin, John Power, Neil Ghani,
Aart Middeldorp, and the anonymous referees. This work is supported by the
JSPS Grant-in-Aid for Scientific Research (16700005).

References[Acz78]P. Aczel. A general Church-Rosser theorem. Technical report, University ofManchester, 1978.
[dB72] N. de Bruijn. Lambda calculus notation with nameless dummies, a tool
for automatic formula manipulation, with application to the church-rosser
theorem. Indagationes Mathematicae, 34:381–391, 1972.
[DR98] O. Danvy and K.H. Rose. Higher-order rewriting and partial evaluation.
In Rewriting Techniques and Applications, 9th International Conference,(RTA’98), LNCS 1379, 1998.
[FPT99] M. Fiore, G. Plotkin, and D. Turi. Abstract syntax and variable binding. In
Proc. 14th Annual Symposium on Logic in Computer Science, pages 193–202,
1999.
[Ham03] M. Hamana. Term rewriting with variable binding: An initial algebra approach. In Fifth ACM-SIGPLAN International Conference on Principles
and Practice of Declarative Programming (PPDP’03), pages 148–159, 2003.
[Ham04] M. Hamana. Free Σ-monoids: A higher-order syntax with metavariables. In
Asian Symposium on Programming Languages and Systems (APLAS 2004),
LNCS 3302, pages 348–363, 2004.
[JR01] J.-P. Jouannaud and A. Rubio. Higher-order recursive path orderings à lacarte. In International Workshop on Rewriting in Proof and Computation(RPC’01), pages 161–175, 2001.
[Klo80] J.W. Klop. Combinatory Reduction Systems. PhD thesis, CWI, Amsterdam,
1980. volume 127 of Mathematical Centre Tracts.
[KOR93] J.W. Klop, V. van Oostrom, and F. van Raamsdonk. Combinatory reduction
systems: Introduction and survey. Theor. Comput. Sci., 121(1&2):279–308,
1993.
[LRD95] P. Lescanne and J. Rouyer-Degli. Explicit substitutions with de Bruijn’s levels. In Rewriting Techniques and Applications, 6th International Conference(RTA-95), LNCS 914, pages 294–308. Springer, 1995.
[Mac71] S. Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer-Verlag, New York, 1971.

Universal Algebra for Termination of Higher-Order Rewriting[Oos94][OR94][Plo98][Pol94][Pol96][Raa][Zan94]149

V. van Oostrom. Confluence for Abstract and Higher-Order Rewriting. PhD
thesis, Vrije Universiteit, Amsterdam, 1994.
V. van Oostrom and F. van Raamsdonk. Comparing combinatory reduction
systems and higher-order rewrite systems. In the First International Workshop on Higher-Order Algebra, Logic and Term Rewriting (HOA’93), LNCS
816, 1994.
G. Plotkin. Binding algebras: A step between universal algebra and typetheory (invited talk). In Rewriting Techniques and Applications, 9th International Conference, RTA’98, Tsukuba, Japan, 1998.
J. van de Pol. Termination proofs for higher-order rewrite systems. In
the First International Workshop on Higher-Order Algebra, Logic and Term
Rewriting (HOA’93), LNCS 816, pages 305–325, 1994.
J. van de Pol. Termination of Higher-order Rewrite Systems. PhD thesis,
Universiteit Utrecht, 1996.
F. van Raamsdonk. Examples of higher-order rewriting systems. at
http://www.cs.vu.nl/~femke/ps/.
H. Zantema. Termination of term rewriting: interpretation and type elimination. Journal of Symbolic Computation, 17:23–50, 1994.

Appendix: Elementary Description of The Category SetF
For those who are not familiar with category theory, we devote this section toan elementary description of the central categorical structure used in this paper:
the category SetF and related morphisms. The functor category SetF plays ancentral role in this paper. The objects of it are functors F → Set and the arrows
are natural transformations between them. In more elementary term, an objects
A of SetF (often written as A ∈ SetF ) is given by a N-indexed set {A(n)}n∈N
with “the arrow part” i.e. for each function ρ : m → n ∈ F, we also need to givea function A(ρ) : A(m) - A(n).
An arrow (or called a map, morphism) between objects A, B ∈ SetF is anatural transformation f : A - B; more elementary, it is given by a family- B(n) parameterised by all n ∈ N
of functions of the form f (n) : A(n)that satisfies the condition ∀a ∈ A(m) . B(ρ)(f (m)(a)) = f (n)(A(ρ)(a)) for all
functions ρ : m → n. This condition (“naturality”) diagrammatically means thecommutativity of the diagram
m
ρ
?
n

A(m)
A(ρ) ?
A(n)

f (m)
f (n)

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

Very roughly, we can think of A ∈ SetF as an N-indexed set equipped with“something”, and a map f : A - B of SetF as an N-indexed function f (n) :A(n) - B(n) with “some coherence law”. These “something” precisely mean
the above descriptions. We may ignore them to get a rough understanding (withkeeping in mind that these have officially such conditions). An object A ∈ SetF
is often called a presheaf .