62

Makoto Hamana

Semantic Labelling for Proving
Termination of Combinatory Reduction Systems
Makoto Hamana
Department of Computer Science, Gunma University, Japan
hamana@cs.gunma-u.ac.jp

Abstract. We give a novel transformation method for proving termination ofhigher-order rewrite rules in Klop’s format called Combinatory Reduction System (CRS). The format CRS essentially covers the usual pure higher-order functional programs such as Haskell. Our method called higher-order semantic labelling is an extension of a method known in the theory of term rewriting. This attaches semantics of the arguments to each function symbol. We systematically deﬁne the labelling by using the complete algebraic semantics of CRS, Σ-monoids.
We also examine the power of higher-order semantic labelling by several examples. This includes an interesting example from the viewpoint of functional
programming.

1

Introduction

Rewrite rules appear everywhere in computer science. In programming language theory,
we use often transformation of states, expressions, terms, or programs given by someform of rewrite rules. Functional programs such as Haskell can also be regarded as
rewrite rules. When reasoning with such rewrite rules, termination is one of the mostimportant property, because it is necessary for decidable equality checking. This topic
has been extensively investigated in the ﬁeld of term rewriting [BN98, Ter03].
In this paper, we deal with higher-order rewrite rules in Klop’s format called combinatory reduction systems (CRSs) [Klo80, KOR93]. The format CRS is known as oneof the most early detailed formulation of higher-order rewriting systems (i.e. rewriting
systems having the feature of variable binding and meta-level substitutions) in the theory of term rewriting. A CRS is a set of rewrite rules on second-order terms. We give amethod to prove termination, meaning strong normalisation, of a CRS by a translation
called higher-order semantic labelling. This is an extension of a method for ﬁrst-orderterm rewriting systems (TRSs) [Zan95].
Weakness of existing syntactic methods. Higher-order extensions of term rewriting systems [Ter03] are known as several formats: major representatives are CRSs,
Higher-order Rewrite Systems [Nip91], and Inductive Data Type Systems [BJO02].
There exist several termination criteria: higher-order recursive path order (HORPO)[JR07], the General Schema [BJO02, Bla00], hereditary monotone functional interpretation [Pol94], binding algebra interpretation [Ham05]. Recently improvements of
HORPO/General Schema are actively investigated [BR01, Raa01, JR06]. A recent survey on this ﬁeld can be found in [BJR08].
S.Escobar (Ed.): WFLP 2009, LNCS 5979, pp. 62–78, 2010.
c Springer-Verlag Berlin Heidelberg 2010

Semantic Labelling for Proving Termination of Combinatory Reduction Systems

63

For CRSs, the General Schema is a decidable syntactic criteria of termination [Bla00].
The idea of the General Schema is to control the arguments of the right-hand side recursive calls in a rewrite rule by checking that they are smaller than the left-hand sides
ones in the strict subterm order extended in a multiset or lexicographic manner.
The General Schema criteria is eﬀective for rewrite rules deﬁned structural recursively on term structures. However, there are many realistic rewrite rules which do not ﬁt
into this scheme. We use often rewrite rules deﬁned non-structural recursively on term
structures. The General Schema is not applicable to prove termination of such rewrite
rules. What does this mean? This implies that rather than syntactic structures, semantic
structures should be more explicit in many situations, and they can be a “hint” of complete termination proofs. Our approach to give termination proofs in this paper does not
aim to be fully automatic. Finding appropriate semantics of rewrite rules automaticallyis hard in general. But in most cases, one has the intended semantics for rewrite rules
in one’s mind that matches the intended application (if not, why one could write suchrewrite rules?) Hence, making such semantics explicit is merely a matter of formulation. Notice that our method is not fully semantical either. We combine both syntactic
and semantical information. Below, we give two examples to illustrate this situation.
Example 1 (The preﬁx sum of a list). Consider the following CRS P for computing
the preﬁx sum of a list, i.e., the list with the sum of all preﬁxes of a given list using thehigher-order function map (taken from [BR01]).
map(a.f[a], nil) → nilmap(a.f[a], x : xs) → f[x] : map(a.f[a], xs)
ps(nil) → nil
ps(x : xs) → x : ps(map(a.x + a, xs))

We want to prove termination of the CRS P. Unfortunately, the CRS P does notfollow the General Schema, hence the exiting syntactic method is not powerful enough.
This is because the argument of ps in the right-hand side of the last rule is not a subtermof the argument of ps in the left-hand side. However, we know that the map function
does not change the length of a list, thus a shorter list than x : xs is always used in
the recursive call of ps. To prove termination of ps, this “semantic” information (rather
than only syntactical structures) should be eﬀectively used.
Higher-order semantic labelling developed in this paper solves this problem. It is amethod to reﬂect such information in rewrite rules. In this case, we use the “length” ofa list for ps as the semantics. Higher-order semantic labelling transforms the original
CRS P to the following labelled CRS:
ps0 (nil) → nil
psi+1 (x : xs) → x : psi (map(a.x + a, xs))

where i ∈ N. This i denotes the “semantics” of argument ps, i.e., the length of a list.
This transformation to attach semantics to function symbols is systematically deﬁned in
the structure of Σ-monoids, which is abstract algebraic structures of higher-order terms.
Then, this labelled CRS successfully follows the General Schema with the precedence

64

Makoto Hamana

psi > ps j > map > : for i > j ∈ N. This ordering is used to compare two term
structures in a recursive manner. If two root function symbols can be compared by
the ordering, thier arguments need not to be comparied. Hence, the order psi+1 > psi
eﬀectively solve the above mentioned problem on the mismatch between the term sizeand semantical size. Our main theorem (Thm. 10) of higher-order semantic labelling isthat if the labelled CRS is terminating, then the original CRS is terminating. Hence, we
can conclude termination of the CRS P.

Example 2 (Haskell’s rewrite rules). Glasgow Haskell Compiler (GHC) has a pragma
called “rewrite rules” [JTH01] for an optimization purpose. GHC applies rewrite rules
to the source program wherever it can. The following is an example that composes twomaps in a program.
{-# RULES"map/map" forall f g xs.
#-}

map f (map g xs) = map (f.g) xs

Rewriting by this Haskell’s rewrite rule are expected to be terminating at the compile time. But GHC makes no attempt to ensure that the rule is terminating becauseof complications of the combination of the rewrite rule and compiler’s optimization
rules [JTH01]. But ideally we should ensure termination of rewrite rules. To consider
this problem in a formal setting, we model this Haskell’s rewrite rule as the following
CRS’s rewrite rule:
map(f, map(g, xs)) → map(a.f[g[a]], xs)

A diﬃculty is that this rule is not deﬁned structural recursively on a data structure.
Moreover, the ﬁrst argument of map in the right-hand side is bigger than ones in theleft-hand side. Hence, this does not follow the General Schema.
Higher-order semantic labelling again solves this problem. We use “the number ofmaps” in the second argument of map as the semantics. Higher-order semantic labelling transforms the original rule to the following labelled rules:
mapi+1 (f, mapi (g, xs)) → mapi (a.f[g[a]], xs)
mapi (f, xs)→ map j (f, xs)

for all i ∈ N
for all i > j ∈ N

Each label denotes the number of maps in the second argument. The General Schema
succeeds in showing termination of the rules with the precedence mapi > map j for alli > j ∈ N. Hence by our main theorem, we conclude termination of the original map’srule..
These two examples use seemingly simple semantics, i.e., “the length of lists” and“the number of maps”. But to compute them actually needs a sophisticated semanticalaccount because the rewrite rules involve higher-order functions. Moreover, semantics
need not to be numbers or “sizes”. Arbitrary (higher-order) algebraic structures (e.g.
λ-terms, domains, categories, etc.) can be semantics of a CRS. In other words, the semantic information for labels cannot be obtained by just syntactic counting of symbols.
In this paper, using the complete algebraic semantics Σ-monoid, we systematically givehigher-order semantic labelling for CRSs.

Semantic Labelling for Proving Termination of Combinatory Reduction Systems

65

Contribution. The contribution of this paper is summarised as follows.
(i) Theoretical contribution.
• We generalised semantics labelling for TRSs [Zan95] to higher-order semanticlabelling for CRSs in the framework of Σ-monoids. This also showed that Σmonoids was certainly the right structure as the semantics of CRSs.
• We showed that semantic labelled meta-terms form a Σ-monoid.
• We identiﬁed the commutativity of the labelling operation with the substitutions appearing in formulation of CRSs is an essential property to establish
semantic labelling.
(ii) Practical contribution. We demonstrate higher-order semantic labelling by several
examples for which the General Schema alone fails.
Background. Semantic labelling on higher-order terms has been deﬁned for Inductive
Datatype Systems [Ham07]. The present paper much simpliﬁes the labelling method
to deal with CRSs. We also aim to apply it to examples taken from functional programming. The semantics used in this paper is based on the algebraic semantics of
CRS Σ-monoids. The notion of Σ-monoids was introduced by Fiore, Plotkin and Turi
[FPT99], then a higher-order abstract syntax for free Σ-monoids was developed by theauthor [Ham04]. The algebraic semantics for CRSs [Ham05] was an application of thisΣ-monoid structure. The outline of semantic labelling for CRSs (without proofs) waspresented at 13th International Conference on Logic for Programming Artiﬁcial Intelligence Reasoning (LPAR’06) as a short paper.
How to read the paper. Theories on term rewriting usually avoid the use of semantics as much as possible. In contrast to it, we rely on the semantics of higher-orderterms and rewriting. The semantics structure Σ-monoid is a natural extension of theﬁrst-order universal algebra to the second-order setting by shifting the base category
from Set to a presheaf category [FPT99]. It is systematically deﬁned in the frameworkof categorical universal algebra. Why categorical notions are needed is to make deﬁnitions and discussions on higher-order rewriting mathematically simple, manageable andsystematic. The seemingly “elementary” extension of ﬁrst-order semantic structures tohigher-order setting by hand (within ordinary set-theoretic setting) makes deﬁnitions
and theories quite complex because of the combinations of ordinary ﬁrst-order structures and higher-order structures. Category theory prevents this explosion by giving aright abstraction for algebraic and higher-order terms. Hence, this paper assumes basic
knowledge of category theory for reading the development of the semantic labelling
method, such as functor categories, monoidal categories, monoids and algebras (e.g.
[Mac71] Chap. II, VII).
Future work. As a future work, we plan to make our method to be more accessible
for users of proof assitants and dependently-typed programming languages. One of themost expected area that seriously needs termination proofs is proof assitants. Finding
appropriate semantics fully automatic is impossible, but one’s intended semantics might
be directly mechanised within a proof assitant such as Coq or Agda. Combining itwith syntactic methods will greatly reduce eﬀorts to give full termination proofs inproof assitants. Hence, giving a convenient library and recipes for higher-order semanticlabelling in a proof assitant might be interesting.

66

Makoto Hamana

Organisation. This paper is organised as follows. We ﬁrst review the deﬁnition of
CRSs in Section 2 and the semantics of CRSs in Section 3. We give higher-order semantic labelling of CRSs in Section 4. In Section 5, we give the quasi-model version ofhigher-order semantic labelling and show several examples of termination proof using
our method. All omitted proofs are given in Appendix.

2

Combinatory Reduction Systems

CRS. We review the deﬁnition of CRSs. We use the deﬁnition of the standard reference[KOR93] of CRSs with a slight modiﬁcation of syntax used in [DR98]: −.− and −[−]
instead of ordinary ones [−]− and −(−) in [KOR93].
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 form t ::= x | x.t | f l (t1 , . . . , tl ). These forms are respectively
called variables, abstractions, and function terms.
(ii) CRS meta-terms extend CRS terms to t ::= 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 where t is aterm. Any valuation is 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 ))(1)

Note that the right-hand side of the equation (1) uses an application at the metalevel to 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 bound in θ(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 theform z[x1 , . . . , xn ] with distinct variables xi ,(iv-c) r can only contain meta-applications with meta-variables occurring in the lefthand side.
The rewrite rule l → r is safe for θ , if for all z in l and r, the substitute θ(z) does
not have a free variable x occurring in an abstraction x.− of l and r. A set of rewrite
rules under the signature Σ is called a CRS and denoted by (Σ, R) or simply R.
(v) The CRS rewrite relation →R is generated by context and safe valuation closure ofa given CRS R:
l→r∈R
safe θ
θ(l) →R θ(r)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 rewriting at
the i-th argument of f . We say that R is terminating if →R is well-founded.

Semantic Labelling for Proving Termination of Combinatory Reduction Systems

67

Structural CRSs. In this paper, we treat CRSs using (meta-)terms built from binding
signatures, which we call structural CRSs (cf. Aczel’s contraction schemes [Acz78]).
A binding signature Σ consists of a set Σ of function symbols with an arity function a :Σ → N∗ , where N∗ denotes the set of all ﬁnite sequences of natural numbers. A function
symbol of binding arity hn1 , . . . , nl i, denoted by f : hn1 , . . . , nl i, has l arguments andbinds ni variables in 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] for the naming convention of variables (N.B. not for metavariables) in CRSs. We
also use the convention 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. Structural metaterms are of the form t ::= x | f (x1 · · · xi1.t1 , . . . , x1 · · · xil.tl ) | zl [t1 , . . . , tl ] satisfying
the restriction generated by the inference system given blow. Fix an N-indexed set Z ofmetavariables deﬁned by Z(l) , {z | z has arity l}. A meta-term t is structural if n ` t
is derived from the following rules for some n ∈ N.
x∈n
n `x

f : hi1 , . . . , il i ∈ Σ n+i1 ` t1 · · · n+il ` tl
n ` f ( n+1 . . . n+i1 .t1 , . . . , n+1 . . . n+il .tl )z ∈ Z(l) n ` t1 · · · n ` tl
n ` z[t1 , . . . , tl ]By using these rules, we obtain meta-terms in the method of de Bruijn levels. A rewrite
rule 1. · · · n.l → 1. · · · n.r is called structural if l and r are structural, i.e. n ` l andn ` l. A CRS is structural if all rules are structural. A valuation θ is structural if forany mapping by θ : z 7→ λ(x1 , . . . , xn ).t, t is a structural term and all variables in t areincluded in x1 , . . . , xn . 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 the other part is not important.

3

Semantics of CRSs

3.1

Binding Algebras

The semantics of CRS is given by the notion of binding algebras and Σ-monoids. Whatare Σ-monoids? A Σ-monoid is an algebra equipped with substitution operation on (semantics of) terms. This substitution operation is called multiplication, typically denotedby β in this paper. Why this is a multiplication is that the substitution operation satisﬁes
the monoid law (imagine compositions of substitutions with the identity substitution)in an abstract setting.
We review the notion of binding algebras and Σ-monoids. For detail, see [FPT99].
Let F be the category which has ﬁnite cardinals n = {1, . . . , n} (n is possibly 0) as objects, and all functions between them as arrows. This is the category of object variables
by the method of de Bruijn levels (i.e. natural numbers) and their renamings. We use
the functor category SetF . An object A of SetF is often called a presheaf . Subscripts
may be used to denote parameters. The functor δ : SetF → SetF for “index extension”
is deﬁned by (δL)(n) = L(n + 1) for L ∈ SetF . To a binding signature Σ, we associate the`Qsignature functor Σ : SetF → SetF given by ΣA = f :hn1 ,...,nl i∈Σ 1≤i≤l δni A. A Σ-algebra

68

Makoto Hamana

is a pair (A, α) consisting of a presheaf A ∈ SetF called a carrier and a map ([ ] denotes- A called an algebra structure, wherea copair of coproducts) α = [ fA ] f ∈Σ : ΣAn1nl
A deﬁned for each function symbol f :fA is an operation fA : δ A × . . . × δ A
hn1 , . . . , nl i ∈ Σ. The “presheaf of variables” V ∈ SetF is deﬁned by V(n) = n, V(ρ) =`ρ (ρ : m → n in F). 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 in F. Then, (SetF , •, V) forms a monoidal category [Mac71], where the“substitution” monoidal product is deﬁned as follows. 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 anequivalence class in A•B(n) is also denoted by this notation. Let Σ be a signature functor
with strength st deﬁned by a binding signature. A Σ-monoid M = (M, α, η, µ) consistsof a monoid (M, η : V → M, µ : M • M → M) in the monoidal category (SetF , •, V)
with a Σ algebra structure α : ΣM → M satisfying µ◦(α•id M ) = α◦Σµ◦st. A Σ-monoid
morphism M - M 0 is a morphism in SetF which is both Σ-algebra homomorphismand monoid morphism.
3.2

Algebra of Meta-terms

Let Z be an arbitrary N-indexed set of metavariables (cf. Sec. 2). The presheaf MΣ Z ofmeta-terms is deﬁned by MΣ Z(n) = {t | n ` t}. We abbreviate n+1, . . . , n+k.t to n+~k.t. For
every f : hi1 , . . . , il i ∈ Σ, we deﬁne the map fT : δi1 MΣ Z×· · ·×δil MΣ Z - MΣ Z in SetF
by (t1 , . . . , tl ) - f (n+i~1 .t1 , . . . , n+~il .tl ). The multiplication β : MΣ Z • MΣ Z - MΣ Z
is a map in SetF that performs a substitution of variables deﬁned inductively as follows.
β(n)(i; ~t) = tiβ(n)(z[s1 , . . . , sl ]; ~t) = z[β(n)(s1 ; ~t), . . . , β(n)(sl ; ~t)]β(n)( f (m+ i~1 .s1 , . . . , m+~il .sl ); ~t) = f (m+ i~1 . β(m+i1 )(s1 ; upi1 (~t), m+1, . . . , m+i1 ), . . .
m+~il . β(m+il )(sl ; upil (~t), m+1, . . . , m+il )where f : hi1 , . . . , il i ∈ Σ and ~t denotes t1 , . . . , tm , and the weakening map from MΣ Z(m)to MΣ Z(m + i) is deﬁned by upi , MΣ Z(idm + wi ) where wi : 0 → i. Then, thestructural meta-terms (MΣ Z, [ fT ] f ∈Σ , ν, β) is a free Σ-monoid over a presheaf Ẑ, where- MΣ Z in SetF is deﬁned by x
- x and Ẑ(n) = `k∈N F(k, n) × Z(k)ν : V
[Ham04]. Hereafter, given N-indexed set Z, we abuse the notation to use Z to denote its
presheaf version Ẑ ∈ SetF in an assignment.
- A of SetF whose target
Deﬁnition 3. We call an assignment a morphism φ : Z- A is
A has a Σ-monoid structure (A, α, η, µ). By freeness, an assignment φ : Z
extended to the Σ-monoid morphism φ∗ : MΣ Z - A deﬁned byφ∗n (x) = ηn (x)(x ∈ n)φ∗n ( f (n+ i~1 .t1 , . . . , n+~il .tl )) = fA (φ∗n+i1 (t1 ), . . . , φ∗n+il (tl ))φ∗n (z[t1 , . . . , tl ]) = µn ( φl (z); φ∗n (t1 ), . . . φ∗n (tl ) )where f : hi1 , . . . , il i ∈ Σ.

Semantic Labelling for Proving Termination of Combinatory Reduction Systems

69

When the N-indexed set of metavariables Z = 0 (empty set), MΣ 0 is the presheafof all structural terms (written as T ΣV in [Ham05]). Moreover, MΣ 0 forms the initial Σmonoid [FPT99, Ham04]. An assignment θ : Z - MΣ 0 gives a structural valuation,- MΣ 0 gives its “homomorphic” extension on meta-terms. We alsoand θ∗ : MΣ Z
call a valuation an assignment θ : Z - MΣ 0.
3.3

Algebraic Semantics of Rewriting

Henceforth, in this paper we consider structural CRSs only. So we say “a CRS” for astructural CRS.
The notions of models and quasi-models for CRSs are deﬁned as follows. For apresheaf A, we write ≥A for a family of preorders {≥A(n) }n∈N , where ≥A(n) is a preorder
on a set A(n) for each n ∈ N. Let (A1 , ≥A1 ), . . . , (Al , ≥Al ), (B, ≥B ) be presheaves equippedwith preorders. A map f : A1 × · · · × Al - B in SetF is weakly monotone if all n ∈ N,
all a1 , b1 ∈ A1 (n), . . . , al , bl ∈ Al (n) with ak ≥A(n) bk for some k and a j = b j for all j , k,then f (n)(a1 , . . . , al ) ≥B(n) f (n)(b1 , . . . , bl ). A weakly monotone V + Σ-algebra (A, ≥A )is a V+Σ-algebra A = (A, [ν, [ fA ] f ∈Σ ]), where ν : V - A, equipped with preorders{≥A(n) }n∈N , such that every operation fA is weakly monotone. Let A be a V + Σ-algebra.
A term-generated assignment φ : Z - A is a morphism of SetF that is expressed asθ!A
the composite Z - MΣ 0 - A for some valuation θ, where !A is the unique V + Σalgebra homomorphism from the initial V + Σ-algebra MΣ 0. A V+Σ-algebra A satisﬁes
a rewrite rule Z ` ~n.l → ~n.r if φ∗ (n)(l) = φ∗ (n)(r) for all term-generated assignments- A. A model A for a CRS (Σ, R) is a V+Σ-algebra A that satisﬁes all rules
φ:Zin the weakening closure R◦ (cf. [Ham05]). A weakly monotone V+Σ-algebra (A, ≥A )satisﬁes a rewrite rule Z ` ~n.l → ~n.r if φ∗ (n)(l) ≥A(n) φ∗ (n)(r) for all term-generated- A. A quasi-model A for (Σ, R) is a weakly monotone V + Σassignments φ : Z
algebra A that satisﬁes all rules in the weakening closure R◦ . An important fact is thatany Σ-monoid (M, α, ν, µ) gives a V+Σ-algebra (M, [ν, α]). Thus in this paper, we willbasically work with Σ-monoids rather than V+Σ-algebras, which gives uniform semantic
treatment of algebras with substitutions.

4Higher-Order Semantic Labelling

We are now ready to give our semantic labelling for CRSs. We give an abstract formulation along the idea of initial algebra semantics in the framework of Σ-monoids.
4.1

Semantic Labelling for Meta-terms

Henceforth, we assume that Z is an N-indexed set of metavariables, Σ is a binding
signature and M is a Σ-monoid. We introduce labelling of functions symbols: choose
for every f ∈ Σ a corresponding non-empty set S f of labels, called semantic label set.
The binding signature Σ for labelled function symbols is deﬁned by
Σ = { f p | f ∈ Σ, p ∈ S f }70

Makoto Hamana

where the binding arity of f p is deﬁned to be the binding arity of f . A function symbol
is labelled if S f contains more than one element. For unlabelled f , the set S f containing
only one element can be left implicit; in that case we will often write f instead of f p .
Choose for f : hi1 , . . . , il i ∈ Σ, a semantic label map that is a morphism of SetF
deﬁned by
hh−ii f : δi1 M × · · · × δil M - KS f .
where KS f ∈ SetF is the constant presheaf deﬁned by KS f (n) = S f . If it is clear from thecontext, the superscript of hh−ii f will be omitted. The semantic label map was originallycalled a projection, denoted by π f in [Zan95]. Then, as in the case of ordinary signature,
we deﬁne MΣ Z by the presheaf of all meta-terms generated by the labelled signature Σ.
Deﬁnition 4 (Labelling map). Let φ : Z - M be an assignment. The labelling map
φL : MΣ Z - MΣ Z is a morphism of SetF deﬁned by
φL : M Σ Z n - M ZΣ nnφn (z[~t]) = z[φLn~t]φn (x) = xLLφn ( f (n+ i~1 .t1 , . . . , n+~il .tl )) = fhhφ∗ (t1 ),...,φ∗ (tl )ii f (n+ i~1 .φLn+i1 t1 , . . . , n+~il .φLn+il tl )
L

n+i1

n+il

n

We state the following characterisation that clariﬁes what is the mathematical structure of semantic labelled meta-terms.
Theorem 5. For each assignment φ : Z - M, (M Z, [ fφ ] f ∈Σ , νφ , βφ ) is a Σ-monoid.
ΣCorollary 6. For each assignment φ : Z → M, the labelling map φL : MΣ Z → MΣ Z is
the unique Σ-monoid morphism (MΣ Z, [ fT ] f ∈Σ , ν, β) → (MΣ Z, [ fφ ] f ∈Σ , νφ , βφ ).
Proof. Let iφ : Z → MΣ Z be the assignment into the Σ-monoid (MΣ Z, [ fφ ] f ∈Σ , νφ , βφ )deﬁned by z 7→ z. It is clear that i∗φ = φL by just comparing the deﬁnitions of φL and theΣ-monoid extension (−)∗ . Hence φL gives a Σ-monoid morphism.
tuBelow we describes the Σ-monoid structure on MΣ Z mentioned above for each as- M. Let | − | be the function that erases all labels in a labeled
signment φ : Z
meta-term for the ordinary signature Σ.
Unit. νφ : V → MΣ Z is deﬁned by x 7→ x.
Operations. For f : hi1 , . . . , il i ∈ Σ, the corresponding operation fφ : δi1 MΣ Z × · · · ×
δil M Z - M Z is deﬁned byΣΣ

fφ (n)(s1 , . . . , sl ) = fhhφ∗n+i (|s1 |),...,φ∗n+i (|sl |)ii (n + i1 .s1 , . . . , n + il .sl ).
1

Multiplication. βφ : MΣ Z • MΣ Zln

- M Z is deﬁned byΣβφ (n)(x; ~t) = t x
βφ (n)(z[s1 , . . . , sl ]; ~t) = z[βφ (n)(s1 ; ~t), . . . , βφ (n)(sl ; ~t)]βφ (n)( fq (m+ i~1 .s1 , . . . , m+~il .sl ); ~t) f p (m+ i~1 . βφ (m+i1 )(s1 ; upm+i1 (~t), m+1, . . . , m+i1 ), . . .) if m + 1 > n= f (n+ i~ . β (n+i )(s ; up (~t), n+1, . . . , n+i ), . . .)if m + 1 ≤ n
p
1 φ
1
1
1
n+i1

Semantic Labelling for Proving Termination of Combinatory Reduction Systems

71

where p = hhφ∗ (n)|βφ (n+i1 )(s1 ; upi1 (~t), n+1, . . . , n+i1 )|, . . . , φ∗ (n)|βφ (n+il )(sl ; upil (~t), n+1, . . . , n + il )|iin . For the third clause, we assume that m is the length of ~t, and I is the
maximum of i1 , . . . , il , Note that the length of “upi1 (~t), n+1, . . . , n+i1 ” is m + i1 , and it
renames m + k by n + k to make bound variables sense.
Laws. To check that MΣ Z satisﬁes the monoid law is straightforward induction on metaterms. To check the Σ-monoid law βφ ◦ ([ fφ ] f ∈Σ • id) = [ fφ ] f ∈Σ ◦ Σβφ ◦ st, we instantiate
this at n ∈ F and chase an element, this eventually becomes the equality
βφ (n)( fr (m+ i~1 .s1 , . . . , m+~il .sl ); ~t) = f p (m+ i~1 . βφ (m+i1 )(s1 ; upi1 (~t), m+1, . . . , m+i1 ), . . .
m+~il . βφ (m+il )(sl ; upil (~t), m+1, . . . , m+il )where r = hhφ∗n+i1 (|s1 |), . . . , φ∗n+il (|sl |)iin and p is the one given above. This obviously
holds by the deﬁnition of βφ .
4.2Commutativity

In CRSs, there are two kinds of variables, i.e. “variables” and “metavariables”. Accordingly, there are two kinds of substitutions:• substitution of variables (written as β in Lemma 7), to perform (essentially) the
β-reduction of an instantiated meta-application, such as an instance of f[x].
• substitution of metavariables (written as θ in Lemma 8), used to instantiate rewrite
rules, and formally called valuation (Def. 3).
The labelling map φL has to commute with these two substitutions. This is needed isthat to establish higher-order semantic labelling. We translate a usual rewrite s →R t to
the labelled rewrite φLn s →R φLn t (Prop. 9). This process requires to push substitutions
from inside to outside of an application of the labelling map in term structures in twolevels (i.e. for variables and for metavariables). Mathematically, this is commutativityof labelling with substitutions.
- M be an assignment. Then, the following diagram comLemma 7. Let φ : 0Fmutes in Set :β- MΣ 0MΣ 0 • MΣ 0
φL • φL?
MΣ 0 • MΣ 0

φL
?
- M 0
Σ

βφ

Proof. Since φL is a Σ-monoid morphism, it preserves the multiplication.
Lemma 8. Let φ : 0 - M and θ : Z - MΣ 0 be assignments. Then, the following
diagram commutes in SetF :
MΣ Z

θ∗

- MΣ 0(φ∗ θ)L?
MΣ Z(φL θ)

∗

φL
?
- M 0
Σ

72

Makoto Hamana

Here (−)∗ denotes the Σ-monoid morphism extension (−)∗ (cf. Def. 3) for the case of
the labelled signature Σ.
4.3 Labelled System
For a given CRS (Σ, R) and Σ-monoid M, we deﬁne the labelled rules by
R = {Z ` ~n.φLn l → ~n.φLn r | Z ` ~n.l → ~n.r ∈ R, assignment φ : Z- M}.

Thus R is a set of rewrite rules on labelled terms in MΣ Z(0). So, (Σ, R) forms a CRS
that gives rewriting on Σ-terms. We have seen that the labelling map φL is a Σ-monoid
morphism, i.e., preserves Σ-meta-term structures. The following proposition states thatφL moreover preserves R-rewrite structures.
Proposition 9. Let M be a model of R. If we have CRS rewriting n ` s →R t on MΣ 0n ,then for the assignment φ : 0 - M, we have rewriting n ` φLn s →R φLn t on MΣ 0n .
Theorem 10 (Higher-order semantic labelling). Let M be a model of R. A CRS R is
terminating if and only if R is terminating.
Proof. For both directions, we prove contrapositions. [⇐]: By Prop. 9. [⇒]: By erasing
all labels in rewrite steps.
tu
4.4

ExampleWe illustrate how to apply the higher-order semantic labelling method. Higher-order semantic labelling itself merely transforms a CRS into a labelled one. We need separately
a way to prove termination of the labelled system. For this purpose, we use Blanqui’s
version of the General Schema for CRSs [Bla00] to prove termination of labelled CRSs
because in our experience, this is the most powerful decidable method to prove termination of CRSs. The General Schema uses a precedence which is a partial order onfunction symbols occurring in a CRS. Using a precedence, if all rewrite rules of a given
CRSs follows the General Schema, we conclude termination of it.
Example 11 (CRS for preﬁx sum). Consider the example of CRS P for computing
preﬁx sum of lists given in Example 1. The CRS P is formulated under the binding
signature Σ = {map : h1, 0i, S, ps : h0i, 0, nil : hi, +, “ : ” : h0, 0i}.
To use higher-order semantic labelling, we need a model of P. Here we take thepresheaf Mn , (Nn → N) of all functions on N. This M forms a monoid in themonoidal category SetF by taking the multiplication β : M • M → M as the composition “◦”, and the unit ν : V → M as the projections of Cartesian products i 7→ πi .
To construct a Σ-monoid M, we deﬁne a Σ-algebra structure on M. First, we deﬁne theoperations at the stage 0 (here we call the component parameter of a natural transformation stage):
mapM0 ( f, y) = y

ps(x) = x

:M0 (x, y) = y + 1

nilM0 = 0

x +M0 y = 0.

Semantic Labelling for Proving Termination of Combinatory Reduction Systems

73

The idea of this model is to count the number of cons’s. The deﬁnition of :M0 reﬂects
this idea and the deﬁnition of mapM0 comes from the observation that map does notchange the number of cons’s. For each f : hi1 , . . . , il i ∈ Σ, the operation at stage n ≥ 1 isgiven by using pairing of functions fMn (a1 , . . . , al ) , fM0 ◦ha1 , . . . , al i, more concretely,fMn (a1 , . . . , al )(Γ) = fM0 (a1 (Γ), . . . , al (Γ)) for Γ ∈ Nn . This indeed gives a morphismof SetF . We can straightforwardly check that this gives a model of P. We label thefunction symbol ps and assume that other function symbols are unlabelled. We use thenatural numbers N as the semantic label set S ps . The semantic label map is deﬁned by
hhxiips
0 = x. Then, we have the following labelled rules
ps0 (nil) → nil
psi+1 (x : xs) → x : psi (map(a.x + a, xs))

for all i ∈ N. the General Schema succeeds in showing termination of this labelled CRS
with the precedence psi > ps j > map > nil, : for i > j ∈ N.

5

Labelling with Quasi-Models

Until now the model M was a presheaf and semantic label set S f was a set. Here we
require them to be equipped with well-founded partial orders. The operations fM andsemantic label map hh−ii f have to be weakly monotone morphisms in SetF . Moreover,here M is only required to be a quasi-model for a CRS, meaning that the interpretationof the left-hand side of a rule is greater than or equal to (≥) the corresponding right-handside.
We deﬁne this labelling with quasi-models formally. For f : hi1 , . . . , il i ∈ Σ, we
associate a well-founded poset (S f , ≥S ) of semantic labels and a semantic label map
that is a weakly monotone morphism hh−ii f : δi1 M × · · · × δil M - KS f . The labelled
signature Σ is deﬁned by using the semantic label set S f as in Sec. 4. Let (M, ≥ M ) bea quasi-model for a CRS R. Using the semantic label map and the Σ-monoid M, thelabelled CRS R is also deﬁned by the same as in Sec. 4.3. Moreover, we deﬁne the CRS
Decr (called “decreasing rules”) over Σ to consist of the rules
f p (i~1 .z1 [i~1 ], . . . , i~1 .zl [~il ]) → fq (i~1 .z1 [i~1 ], . . . , i~1 .zl [~il ])for all f : hi1 , . . . , il i ∈ Σ and all p >S q ∈ S f . Here each metavariable zk has arity ik(for 1 ≤ k ≤ l) and >S denotes the strict part of ≥S .
Proposition 12. Let (M, ≥ M ) be a quasi-model for R. If we have rewriting n ` s →R t
- M, n ` φL s →∗ ; → φL t holds. Hereon MΣ 0n , then for the assignment φ : 0
n
R n
Decr
“;” denotes the sequential composition of relations.
Theorem 13. Let M be a quasi-model for a CRS R and R the labelled CRS with respect
to M. Then R is terminating if and only if R ∪ Decr is terminating.
Proof. For both directions, we prove contrapositions. [⇐]: By Prop. 12. [⇒]: By erasing all labels in rewrite steps.
t
u

74

Makoto Hamana

Example 14 (CRS for quick sort). Quick sort algorithm on natural numbers can be
implemented as the CRS R with the standard rewrite rules: if,++, ﬁlter, “>”, “≤”.
0>y→ false0≤y→ truex>0→ trues(x) ≤ 0→ falses(x) > s(y) → x > ys(x) ≤ s(y) → x ≤ yif(true, x, y) → x
nil ++ys→ ys
if(false, x, y) → y(x : xs) ++ys → x : (xs ++ys)
ﬁlter(p, nil) → nilﬁlter(p, x : xs) → if(p[x], x : ﬁlter(p, xs), ﬁlter(p, xs))
qsort(nil) → nil
qsort(x : xs) → qsort(ﬁlter(a. a ≤ x, xs)) ++((x : nil) ++qsort(ﬁlter(a. a > x, xs)))

Since the argument of qsort in the right-hand side of the last rule (ﬁlter(· · · )) is structurally bigger than the argument of qsort in the left-hand side (x : xs), the General
Schema is not applicable. The higher-order recursive path ordering for the corresponding rewrite system written in the format called Inductive Data Type Systems [BJO02]
also fails [BR01].
Here, we use higher-order semantic labelling with a quasi-model. Let D = N × N∗
defwith the order hn, li ≥ hn0 , l0 i ⇐⇒ n ≥ n0 . We use the carrier Mk , (Dk → D). The
operations at stage 0 are:trueM0 = h1, ifalseM0 = h0, i(

0M0 = h0, i(sM0 (hn, li) = hn + 1, li

h1, i if m > n
h1, i if m ≤ n≤ (m, n) =h0, i otherwise M0
h0, i otherwiseyif b = h1, izif b = h0, iqsortM0 (hn, li) = hn, i
ifM0 (b, y, z) =  h0, i otherwise>M0 (m, n) =ﬁlterM0 (p, hn, li) = hthe number of p(hi, i) = h1, i for every i in l, i++M0 (hn, li, hn0 , l0 i) = hn + n0 , l · l0 i
nilM0 = h0, i:M0 (ha, si, hn, li) = hn + 1, a · li
The operations at stage n > 0 are deﬁned similarly to Example 11. This is indeed aquasi-model and cannot be a model. We label the function symbol qsort only. The semantic label set S qsort is N with the usual order. The semantic label map is hhhn, liiiqsort=
0n, which is weakly monotone. Then, we have the labelled rules:
qsort0 (nil) → nil
qsorti+1 (x : xs) → qsort j (ﬁlter(a.a ≤ x, xs)) ++((x : nil) ++qsortk (ﬁlter(a.a > x, xs))) where i + 1 > j, kqsorti (xs) → qsort j (xs)for all i > j ∈ N

the General Schema shows termination of the labelled CRS with the precedence qsorti >qsort j > ﬁlter > if, ++, “>”, “≤” > nil, :, 0, S, true, false for i > j ∈ N.

Semantic Labelling for Proving Termination of Combinatory Reduction Systems

75

Example 15 (Haskell’s rewrite rule for map/map). Consider the CRS’s rewrite rulein Example 2. We take the same carrier Mn = (Nn → N) as in Example 14. Now the- N, mapM ( f, x) = x + 1. The M is
operation on M is mapM0 : (N → N) × N
0indeed a quasi-model. We use the semantic label set and semantic label map for map
are S map = N with the usual order, and hh f, xiimap= x, which is weakly monotone. This0gives the labelled rules given in Introduction, hence the original rule terminates.

6

Conclusion

We have given a method of proving termination of higher-order rewrite rules in Klop’s
format called combinatory reduction system (CRS). The method to prove termination,
called higher-order semantic labelling, is an extension of a method known in the theoryof term rewriting. This attaches semantics of the arguments to each function symbol.
We systematically deﬁne the labelling by using the complete algebraic semantics of
CRS, Σ-monoids. A key to establish the main theorem of semantic labelling was commutativity of labelling with two kinds of substitutions appearing in formulation of CRS.
We have examined the power of higher-order semantic labelling by several examples
taken from functional programming. This shows usefulness of higher-order semanticlabelling in programming languages.
Acknowledgments. I am grateful to the anonymous referees for useful comments on
improving the presentation of the paper. This work is supported by the JSPS Grant-inAid for Scientiﬁc Research (19700006).

References[Acz78]P. Aczel. A general Church-Rosser theorem. Technical report, University of Manchester, 1978.
[BJO02] F. Blanqui, J.-P. Jouannaud, and M. Okada. Inductive data type systems. TheoreticalComputer Science, 272:41–68, 2002.
[BJR08] F. Blanqui, J.-P. Jouannaud, and A. Rubio. The computability path ordering: The endof a quest. In Proc. of CSL’08, pages 1–14, 2008.
[Bla00] Frederic Blanqui. Termination and conﬂuence of higher-order rewrite systems.
In Rewriting Techniques and Application (RTA 2000), LNCS 1833, pages 47–61.
Springer, 2000.
[BN98] F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press,
1998.
[BR01] Cristina Borralleras and Albert Rubio. A monotonic higher-order semantic path ordering. In Procs. 8th International Conference on Logic for Programming, Artiﬁcial
Intelligence and Reasoning (LPAR), LNCS 2250, pages 531–547, 2001.
[dB72]
N. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automaticformula 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.

76

Makoto Hamana[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.
[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.
[Ham05] M. Hamana. Universal algebra for termination of higher-order rewriting. In Proceedings of 16th International Conference on Rewriting Techniques and Applications(RTA’05), LNCS 3467, pages 135–149. Springer, 2005.
[Ham07] M. Hamana. Higher-order semantic labelling for inductive datatype systems. In Ninth
ACM-SIGPLAN International Conference on Principles and Practice of Declarative
Programming (PPDP’07), pages 97–108, 2007.
[JR06]
J.-P. Jouannaud and A. Rubio. Higher-order orderings for normal rewriting. In Proc.
of RTA’06, LNCS 4098, pages 387–399, 2006.
[JR07]
J.-P. Jouannaud and A. Rubio. Polymorphic higher-order recursive path orderings.
Journal of ACM, 54(1), 2007.
[JTH01] S. P. Jones, A. Tolmach, and T. Hoare. Playing by the rules: rewriting as a practicaloptimisation technique in GHC. In Haskell Workshop 2001, 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.
[Mac71] S. Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts
in Mathematics. Springer-Verlag, New York, 1971.
[Nip91] T. Nipkow. Higher-order critical pairs. In Proc. 6th IEEE Symp. Logic in Computer
Science, pages 342–349, 1991.
[Pol94] 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.
[Raa01] F. van Raamsdonk. On termination of higher-order rewriting. In Rewriting Techniquesand Applications, 12th International Conference (RTA 2001), pages 261–275, 2001.
[Ter03] Terese. Term Rewriting Systems. Number 55 in Cambridge Tracts in TheoreticalComputer Science. Cambridge University Press, 2003.
[Zan95] H. Zantema. Termination of term rewriting by semantic labelling. Fundamenta Informaticae, 24(1/2):89–105, 1995.

A Appendix
A.1

Proof of Lemma 8

By induction on meta-terms in MΣ Z. The cases x and f (~s) ∈ MΣ Z n are straightforward.
For the case z[~t] ∈ MΣ Z n , we have the following.
lhs = φL θ∗ (z[~t])= φL β(θz; θ∗~t) = βφ (φL θz; φL θ∗~t)(by Lemma 7)

rhs = (φL θ)∗ (φ∗ θ)L z[~t]= (φL θ)∗ z[(φ∗ θ)L~t]= βφ (φL θz; (φL θ)∗ (φ∗ θ)L~t)= βφ (φL θz; φL θ∗~t) = lhs(by I.H.)

Semantic Labelling for Proving Termination of Combinatory Reduction Systems

A.2

77

Proof of Proposition 9

By induction on proof trees of →R . Since R is structural, it suﬃces to consider thefollowing two cases [Ham05].
(i) Case n ` θ∗n l →R θ∗n r.
This is derived from Z ` ~n.l → ~n.r ∈ R where θ : Z
be the assignment. Now we have a labeled rule

- MΣ 0. Let φ : 0- M(φ∗ θ)Ln l → (φ∗ θ)Ln r ∈ R.
By Lemma 8 and closedness of R-rewrite by the valuation φL θ : Z
have∗- M 0, weΣ∗

φLn (θ∗n l) = (φL θ)n (φ∗ θ)Ln l →R (φL θ)n (φ∗ θ)Ln r = φLn (θ∗n r)(ii) Case n ` f (. . . , n + ~i.s, . . .) →R f (. . . , n + ~i.t, . . .).
This is derived from n + i ` s →R t. Since M is a model, notice φ∗n+i s = φ∗n+i t. By
induction hypothesis, we have φLn+i s →R φLn+i t. So,
φLn ( f (. . . , n + ~i.s, . . .))= fhh...,φ∗n+i s,...iin (. . . , n + ~i.φLn+i s, . . .)= fhh...,φ∗n+i t,...iin (. . . , n + ~i.φLn+i s, . . .)→R fhh...,φ∗n+i t,...iin (. . . , n + ~i.φLn+i t, . . .)= φLn ( f (. . . , n + ~i.t, . . .))A.3 Proof of Proposition 12
By induction on proof trees of →R .
(i) Case n ` θ∗n l →R θ∗n r. This case is proved by the same as in the proof of Prop. 9.
(ii) Case n ` f (. . . , n + i.s, . . .) →R f (. . . , n + i.t, . . .)This is derived from n + i ` s →R t. Since (M, ≥ M ) is a quasi-model, we haveφ∗n+i s ≥ M(n+i) φ∗n+i t. By induction hypothesis, we have φLn+i s →∗Decr ; →R φLn+i t. Notice also that hh−ii is weakly monotone. So,
φLn ( f (. . . , n + i.s, . . .)) = fhh...,φ∗ ~ s,...ii (. . . , n + ~i.φLn+i s, . . .)n+in→∗Decr fhh...,φ∗n+i t,...iin (. . . , n + ~i.φLn+i s, . . .)→∗Decr ; →R fhh...,φ∗n+i t,...iin (. . . , n + ~i.φLn+i t, . . .)= φLn ( f (. . . , n + ~i.t, . . .))

78

A.4

Makoto Hamana

Structural CRSs as Typed CRSs

In [Bla00], Blanqui deﬁned a version of higher-order rewriting format Inductive Data
Type Systems (IDTS), which he called “new deﬁnition of IDTS” ([Bla00] Def. 1). We
call his “new deﬁnition of IDTS” typed CRS since as mentioned in his paper, it is a
simply-typed version of CRS. Blow we show that our structural CRSs is a subclass of
Blanqui’s typed CRSs. Hence we can apply General Schema for typed CRSs given in[Bla00] to structural CRSs to show termination of structural CRSs.
To give a typed CRSs, the following alphabet A ([Bla00] Def. 1) is required. In
typed CRSs, types are simple types generated by the base types. (i) a set of base types,(ii) type-indexed collection of variables, (iii) type-indexed collection of function symbols, (iv) type-indexed collection of metavariables. Then the set of all meta-terms of a
typed CRS is constructed from A, and a typed CRS is a set of pairs of meta-terms.
Suppose that a structural CRS (Σ, R) using a N-indexed set Z of metavariables isgiven. We show that this gives rise to the following alphabet A and typed CRS. We
assume the only base type ι and all variables (now, natural numbers) have the base type.
For each function symbol f : hi1 , . . . , il i ∈ Σ, we assign to the type f : ιi1 , . . . , ιil → ι
where ιi = (ι → · · · → ι) → ι (the part (ι → · · · → ι) denotes i-times ι). For eachmetavariable z of arity n in Z, we associate a metavariable z in A of the type ιn → ι.
S
Then, the set of all structural meta-terms k∈N MΣ Z(k) is equal to the set of all metaterms of typed CRS given in [Bla00] under this alphabet A. Thus, the structural CRS R
is a typed CRS. Valuations and generation of a rewrite relation for structural CRSs also
ﬁt into those of typed CRS version.