Higher-Order Semantic Labelling forInductive Datatype Systems
Makoto Hamana ∗Gunma University / The University of Tokyo
hamana@ipl.t.u-tokyo.ac.jp

Abstract

1.

We give a novel transformation for proving termination ofhigher-order rewrite systems in the format of Inductive Data
Type Systems (IDTSs) by Blanqui, Jouannaud and Okada.
The transformation called higher-order semantic labelling
attaches algebraic semantics of the arguments to each function symbol. We systematically deﬁne the labelling and showthat labelled systems give termination models in the framework of Fiore, Plotkin and Turi’s binding algebras. As applications, we give simple proofs of termination of the explicit substitution system λX and currying transformation via
higher-order semantic labelling. Moreover, we prove a new
result of modularity of termination of IDTSs by introducing the notion of solid IDTSs. We prove that termination ispreserved under the disjoint union of an IDTS and a higherorder program scheme.

In this paper we develop a theory of higher-order semanticlabelling, which is a transformation for proving termination(meaning strong normalisation) of Blanqui, Jouannaud andOkada’s Inductive Data Type Systems [3, 1].
We illustrate how this transformation method is applicable to several seemingly different problems: we prove termination of

Categories and Subject Descriptors F.4.2 [Grammars andOther Rewriting Systems]; D.3.1 [Programming Laguages]:
Formal Deﬁnitions and Theory—syntax,semantics; F.3.2[Logics and Meaning of Programs]: Semantics of Programming Languages—Algebraic approaches to semantics, Denotational semantics, Operational Semantics
General Terms Theory, Languages
Keywords Termination, modularity, initial algebra semantics, higher-order abstract syntax, higher-order rewriting,categorical semantics∗ Currently visiting IPL, The University of Tokyo as a Domestic Researcher

from Gunma University, Japan. This work is supported in part by the JSPS
Grant-in-Aid for Scientiﬁc Research (90334135).

Permission to make digital or hard copies of all or part of this work for personal orclassroom use is granted without fee provided that copies are not made or distributedfor proﬁt or commercial advantage and that copies bear this notice and the full citationon the ﬁrst page. To copy otherwise, to republish, to post on servers or to redistributeto lists, requires prior speciﬁc permission and/or a fee.
PPDP’07 July 14–16, 2007, Wroclaw, Poland.
c 2007 ACM 978-1-59593-769-8/07/0007. . . $5.00
Copyright °Introduction• the explicit substitution system of the λX-calculus (Sect.
4), and• the currying transformation (Sect. 5.1) that is an extension of Kennaway, Klop, Sleep and de Vries’ result.
We also prove modularity of termination for the disjoint
union of an Inductive Data Type System (IDTS) and ahigher-order recursive program scheme (HO-RPS) (Sect.
5.2) via higher-order semantic labelling and introduction of
the “solid” property of IDTSs. To the author’s best knowledge, these are new results on modularity of termination ofhigher-order rewrite rules.
Higher-order extensions of term rewriting systems [34]are known as several formats: major representatives are
Combinatory Reduction Systems (CRSs) [21, 22], Higherorder Rewrite Systems [28], and Inductive Data Type Systems [3]. There exist several termination criteria: higherorder recursive path order (HORPO) [16, 18], the General
Schema [3, 1], hereditary monotone functional interpretation[31], binding algebra interpretation [14]. Recently improvements of HORPO/General Schema are actively investigated[6, 32, 17, 2].
This paper is based on the algebraic semantics of CRS by
the author [14] by binding algebras and Σ-monoids. The notion of binding algebras and Σ-monoids was introduced by
Fiore, Plotkin and Turi [11] to give algebraic semantics ofhigher-order abstract syntax. Typed versions of binding algebras for typed higher-order abstract syntax are extensively
investigated [10, 26, 33, 19]. A higher-order syntax for freeΣ-monoids was developed by the author [13].
Organisation. This paper is organised as follows. We ﬁrst
review the deﬁnition of Inductive Data Type Systems and its

semantics in Sect. 2. We give higher-order semantic labellingof IDTSs in Sect. 3. In Sect. 4, we consider an applicationof higher-order semantic labelling to the termination problem of the λX-calculus. In Sect. 5, we investigate semantic labelling with term model and its application to currying
transformation and modularity of termination of IDTSs.
~ for a sequence
Convention. We use the vector notation A~
A1 , · · · , Al , and |A| for its length. We use the notations[x := t] for the usual capture-avoiding substitution that replaces all x in s with t. We may call this meta-level substitutions to distinguish them from explicit substitutions. FV(t)denotes the set of all free variables in t. We often omit superscripts or subscripts (for types, typing contexts) of a mathematical object if they are clear from contexts.

• Z is a family (Zα )α∈I(B) of sets of metavariables (written as small-caps letters Z or, capital letters M, N )such that all the sets are pairwise disjoint. The raw syntax isgiven as follows.
• Terms have the formt ::= x | x.t | f (t1 , . . . , tn ).
These forms are respectively called variables, abstractions, and function terms.
• Meta-terms extend terms tot ::= x | x.t | f (t1 , . . . , tn ) | Z(t1 , . . . , tn ).
The last form is called a meta-application.

2.

Preliminaries

2.1

Inductive Data Type Systems

The Inductive Data Type Systems (IDTS) are introduced by
Blanqui, Jounnaud and Okada [3]. This is a framework of
rewrite rules on terms built on inductively deﬁned datatypes
and simple types. The IDTS is extended further by Blanqui[1] by admitting higher-order pattern matching when applying rewrite rules. We use this version of IDTS [1] with thefollowing restrictions.
• We use simple types up to the second-order.
• IDTS’s binder (−.−) always appears as an argument of afunction symbol. For example, lam(xb .x) for a function
symbol lam : (b → b) → b.
• We do not assume a global set of variables. Instead, we
use local typing contexts.
Since the fragment we use is just a subclass of IDTSs in[1], the termination criterion of IDTSs, called the General
Schema [1, 3], is also applicable to this fragment. Notice that
although this fragment has simple types up to second-order,
it can encode simple types of arbitrary order by the featureof inductive types (see the case of simply-typed λX-calculus
in Sect. 4.1). Hence this fragment has enough expressibility
to represent higher-order rewrite rules involving all simple
types and inductive types.
For a set B of base types, the set I(B) of ﬁrst-order types,
and the set T (B) of types are given as follows:
B3b
I(B) 3 α ::= b | b1 , . . . , bn → b
T (B) 3 τ ::= b | α1 , . . . , αn → b
An IDTS-alphabet A is a triple (B, Σ, Z) (or, often justdenoted by (B, Σ)) where• B is a set of base types (denoted by b, a),• Σ, called a signature, is a family (Στ )τ ∈T (B) of sets of→function symbols (denoted by f : (−a1 → b1 ), . . . , (−a→n →bn ) → b)

A context Γ is a sequence of variable:type-pairs. A metaterm t is well-typed if Γ ` t : τ is derived from thefollowing rules for some context Γ.
x:τ ∈Γ
Γ `x:τ

Z ∈ Zb1 ,...,bn →bΓ ` t1 : b1 · · · Γ ` tn : bnΓ ` Z(t1 , . . . , tn ) : b
−−−→
−−−−→
Γ, i1 : a1 ` t1 : b1 · · · Γ, in : an ` tn : bn−→−→Γ ` f ( ia1 1 .t1 , . . . , iann .tn ) : b→
where f : (−a1 → b1 ), . . . , (−a→n → bn ) → b ∈ Σ.
Notation 2.1 Since the binders are clear from the type of−→−→function symbol, we often abbreviate f ( ia1 1 .t1 , . . . , iann .tn )as just f (t1 , . . . , tl ).
A rewrite rule l → r consists of two meta-terms l andr with the following additional restrictions: (i) ` l : τ and` r : τ for some type τ (hence l and r are closed (w.r.t.
variables) meta-terms), (ii) l must be a function term where
all meta-applications have the form Z(x1 , . . . , xn ) (called ahigher-order pattern) with distinct variables xi , (iii) r can
only contain metavariables occurring in the left-hand side.
We may use the notation Z|Γ ` s → t : τ for a rule ora rewrite step if metavariables and variables in s and t areincluded in Z and Γ respectively. We may also simply writeZ ` s → t : τ or Γ ` s → t : τ if another part is notimportant.
A valuation θ is a mapping that assigns to a metavariable
Z : ~b → τ a term t
θ : Z 7−→ t
where x1 : b1 , · · · , xn : bn ` t : τ . Any valuation θ isextended to a function θ∗ on meta-terms:θ∗ (x) = xθ∗ (x.t) = x.θ∗ (t)θ∗ (f (t1 , . . . , tn )) = f (θ∗ (t1 ), . . . , θ ∗ (tn ))θ∗ (Z(t1 , . . . , tn )) = θ(Z) (θ∗ (t1 ), . . . , θ ∗ (tn ))The right-hand side of the last equation means replacing freevariables x1 , . . . , xn in θ(Z) with θ∗ (t1 ), . . . , θ ∗ (tn ) . We
may also write tθ for θ∗ t.
A set of rewrite rules under a alphabet (B, Σ, Z) is called
an IDTS and denoted by (B, Σ, R), or simply (Σ, R) or R.
The rewrite relation →(Σ,R) or simply →R is generated bycontext and valuation closure of a given IDTS (Σ, R).
By the notation s B t, we mean that a well-typed metaterm t is a (strict) sub-meta-term of a well-typed meta-terms. Also, we regard B as a relation. We use D = B ∪ id.
As usual, turning over a symbol, we mean its inverse (e.g.
∗+B −1 = C), and (−) , (−) for the reﬂexive and transitive
closure, and the transitive closure, respectively.
2.2

Binding algebras – semantic structure of syntax
with variable binding

In a previous work, algebraic semantics of CRSs is given bybinding algebras [14]. Since IDTS can be seen as a typed
version of CRS, algebraic semantics of IDTSs can be givenby typed binding algebras [10, 26, 33, 19]. We review thenotion of typed binding algebras in this subsection.
A key idea of binding algebras is to model variables inabstract syntax as natural numbers. To match this semantic
treatment and syntactic presentation tightly, in this paper weassume the method of de Bruijn levels (N.B. not indices)[8, 24] for a formal treatment of named variables modulo αequivalence in IDTSs. Under the method of de Bruijn levels,
variables are natural numbers.
A variable i ∈ N of type τ ∈ B is denoted by i : τor iτ . In this setting, a typing context Γ is a ﬁnite subset{1 : τ 1 , · · · , l : τ l } of typed variables.
Now, we model these variables and contexts in a categorical setting. 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 m → n. For a set B of allbase types, the slice category F ↓ B is seen as the categoryof contexts and their renamings, i.e. objects Γ : n → B arecontexts, and arrows f : Γ → Γ0 are functions f : n → n0
such that Γ = Γ0 ◦f for Γ : n → B, Γ0 : n0 → B. Binary coproducts Γ+Γ0 are given by copairs [Γ, Γ0 ] : n+n0 → B. By
abuse of notation, for a type τ , we denote just by τ a context
τ : 1 → B, 1 7→ τ . Thus we have a coproduct Γ + τ .
We use the functor category (SetF↓B )B to deﬁne binding
algebras. An object of a functor category may be called apresheaf . Ordinary universal algebra is a structure on sets.
Binding algebra is a structure on presheaves. The reason
we use presheaves is to uniformly deal with (context,type)indexed sets of syntactic entities. A typical example is welltyped terms indexed by contexts and types, i.e. for IDTSs,
the set of all meta-terms. For instance, for an IDTS-alphabet(B, Σ, Z), we can deﬁne the indexed set of all meta-terms by
MΣ Z τ (Γ) = {t | Γ ` t : τ }.
With a suitable arrow part, this MΣ Z forms a presheaf, i.e.,an object of (SetF↓B )B .

We deﬁne the functor δ τ : SetF↓B → SetF↓B for context
extension by a variable of type τ , which is used to model abound variable, by (δ τ A)(Γ) = A(Γ + τ ) for A ∈ SetF↓B .
We write δ~τ for the composition δ τ 1 ◦· · ·◦δ τ l . To a signature
Σ, we associate the signature functor Σ : (SetF↓B )B →(SetF↓B )B given byaY(ΣA)b =
δ a~i Abi .
f :(a~1 →b1 ),··· ,(a~l →bl )→b∈Σ 1≤i≤l

A point of this modeling is that an arrow type, say a → b, isinterpreted as a presheaf δ a Ab . This is the crucial differenceof binding algebras from polynomial functor-algebras on
sets for modeling ﬁrst-order abstract syntax or inductive
types.
A Σ-(binding) algebra is a pair of a presheaf (for a carrier) and a natural transformation (for operations) (A, α :ΣA → A) where the algebra structure α is a copair [f A ]f ∈Σ
of all operations on A corresponding to function symbols. A
homomorphism of Σ-algebras is a map φ : (A, α) → (B, β)such that φ ◦ α = β ◦ Σφ.
A set of variables of a certain type taken from a context is
modeled by the presheaf V ∈ (SetF↓B )B deﬁned by Yoneda
embedding Vτ = F ↓ B(τ , −), hence Vτ (Γ) ∼= {x | x : τ ∈Γ}.
To model substitution, we use the notion of monoid in a
monoidal category. The structure of Σ-monoids is for thispurpose where a substitution is modeled by a multiplicationof a monoid. The deﬁnition is given below.
Remark 2.2 In this work, Σ-monoid structure is used in the
proofs in Sect.3, but in the applications of semantic labellingfrom Sect.4, Σ-monoids are not used. So the readers who areinterested in applications can skip the following deﬁnitions.
The category (SetF↓B )B forms a monoidal category withthe unit V and the “substitution” monoidal product • givenbyYaAτ (Γ) ×Bτ i (∆))/ ∼(A • B)τ (∆) = (
Γ∈F↓B

i∈m

where Γ = {i : τ 1 , . . . , m : τ m } and ∼ is the equivalence
relation generated by(t; uρ1 , . . . , uρm ) ∼ (A(ρ)(t); u1 , . . . , ul )for an arrow ρ : Γ → Γ0 of F ↓ B.
A Σ-monoid (A, α, ν, µ) consists of a monoid object [25]M = (M, η : V → M, µ : M • M → M ) in themonoidal category ((SetF↓B )B , •, V) with a Σ-binding algebra α : ΣM → M that satisﬁes µ ◦ (α • idM ) = α ◦ Σµ ◦ st,where the strength st is the one deﬁned in [11]. A morphism of Σ-monoids (M, α) −→ (M 0 , α0 ) is a morphismin (SetF↓B )B which is both Σ-algebra homomorphism andmonoid morphism.
By [11, 26, 33] and as a straightforward variation of [13],we have

Theorem 2.3 MΣ Z forms a free Σ-monoid. Moreover,when Z = 0, the presheaf MΣ 0 = TΣV of all terms forms
an initial V + Σ-algebra and an initial Σ-monoid.
A morphism φ : Z −→ A of (SetF↓B )B is called
an assignment when its target has a Σ-monoid structure(A, α, η, µ). By freeness of MΣ Z, any assignment φ :Z −→ A is extended to a Σ-monoid morphism φ∗ :MΣ Z −→ A:
MΣ Z b (Γ) −→ Ab (Γ)
x 7−→ η(Γ)(x)(x ∈ Γ)∗f (Θ1 .t1 , . . . , Θn .tn ) 7−→ fA (Γ)(φ (Γ+Θ1 )(t1 ), . . .)using typed binding algebras [10, 26]. The main feature ofsemantic labelling is that termination of the original rewrite
system is preserved by transforming it to a semantically labelled system. Often termination of the labelled systems canbe shown by applying the General Schema criterion evenwhen the original system does not follow it since the labelled
system has much more information in function symbols.
Henceforth, we assume an IDTS-alphabet (B, Σ, Z) anda weakly monotone V+Σ-algebra M . We introduce labellingof functions symbols: choose for every f ∈ Σ a corresponding non-empty well-founded poset (Sf , ≥S ) of labels, calleda semantic label set. The signature Σ for labelled function
symbols is deﬁned by∗

Z (t1 , . . . , tn ) 7−→ µ(Γ)( φ(Γ)( Z ); φ (Γ)(t1 ), . . . ).

A valuation θ deﬁned in Sect. 2.1 can be seen as an assignment θ : Z −→ TΣV and in this case, its Σ-monoid
morphism extension θ∗ coincides with the extension of valuation described in Sect. 2.1 (cf. [14]).
2.3 Algebraic semantics of rewrite rules onhigher-order terms
For a presheaf A, we write ≥A for a family of partial orders(≥Aτ (Γ) ) where ≥Aτ (Γ) is a partial order on a set Aτ (Γ)
for each type τ and context Γ. Let (A1 , ≥A1 ), . . . , (Al , ≥Al), (B, ≥B ) be presheaves equipped with partial orders. A
map f : A1 × · · · × Al −→ B in SetF↓B is weakly monotone if for all Γ, all a1 , b1 ∈ A1 (Γ), . . . , al , bl ∈ Al (Γ) withak ≥Ak (Γ) bk for some k and aj = bj for all j 6= k, thenf (Γ)(a1 , . . . , al ) ≥B(Γ) f (Γ)(b1 , . . . , bl ). A weakly monotone V+Σ-algebra (A, ≥A ) is a V+Σ-algebra equipped withpartial orders such that every operation is weakly monotone.
For a V + Σ-algebra A, a term-generated assignmentφ : Z −→ A is a morphism of (SetF↓B )B that can be
expressed as a compositeφ=!◦θ
where ! is the unique homomorphism from the initial V+Σalgebra TΣV to A, and θ is a valuation Z −→ TΣV.
A weakly monotone V + Σ-algebra (A, ≥A ) satisﬁes arewrite rule Z|Γ ` l → r : τ of an IDTS if!θ∗τ (Γ)(l) ≥Aτ (Γ) !θ∗τ (Γ)(r)for all term-generated assignments φ =! ◦ θ : Z −→ A.
Why the notion of term-generated assignments is needed isthat the IDTS’s rewrite relation is generated on terms (noton meta-terms). A quasi-model A for (Σ, R) is a weakly
monotone V+Σ-algebra A that satisﬁes all rules in R.

3.

Higher-Order Semantic Labelling

We now proceed to deﬁning semantic labelling for IDTSs.
This extends semantic labelling for ﬁrst-order term rewriting systems (TRSs) by Zantema [35] by employing the initial algebra semantics of typed higher-order abstract syntaxΣτ = {fp | f ∈ Στ , p ∈ Sf }.
A function symbol is labelled if Sf contains more than one
element. For unlabelled f , the set Sf containing only one
element can be left implicit; in that case we write f insteadof fp .
Choose for f : (~a1 → b1 ), . . . , (~al → bl ) → b ∈ Σ, asemantic label map that is a weakly monotone morphism of
SetF↓B deﬁned byfhh−ii : δ~a1 Mb1 × · · · × δ~al Mbl −→ (KSf )bwhere KSf ∈ (SetF↓B )B is the constant presheaf deﬁned by(KSf )b (Γ) = Sf . 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 Σ. Labelling of function symbols is
given by the following map.
Deﬁnition 3.1 (Labelling map) Let φ : Z −→ M be aterm-generated assignment such that φ =! ◦ θ. The labelling
map φL : MΣ Z −→ MΣ Z is a map of (SetF↓B )B deﬁned by
φLτ ,Γ : MΣ Z τ ,Γ −→ MΣ Z τ ,ΓφLτ ,Γ (x) = x
φLτ ,Γ (Z(~t)) = Z(φ~σL ,Γ~t)φLτ ,Γ (f (Θ1 .t1 , . . . , Θl .tl ))= fhh!θ∗ (t1 ),...,!θ∗ (tl )iif (φLτ 1 ,Γ+Θ1 t1 , . . . , φLτ l ,Γ+Θl tl )τ ,ΓIt is obvious that the presheaf MΣ Z of Σ-meta-terms forms
a free Σ-monoid. Moreover, MΣ Z forms a non-free Σmonoid. This has the Σ-monoid structure(MΣ Z, [f φ ]f ∈Σ , ν φ , β φ )described below for each term-generated assignment φ :Z −→ M . For clarity, here we only give the V+Σ-algebra
structure part. The monoid structure is given in Appendix A.
Let || − || be the function that erases all labels in a labeled
meta-term.
Unit. ν φ : V → MΣ Z is deﬁned by x 7→ x.

apσ,τ (λσ,τ (x.M (x)), N ) → M (x)hx := N iap(M (x), N (x))hx := Ki → ap(M (x)hx := Ki, N (x)hx := Ki)
λ(y.M (x, y))hx := Ki → λ(x.M (y, x)hy := Ki)v(x)hx := Ki → K
M hx := Ki → M
Figure 1. The IDTS RλX of the λX-calculus→
Operations. For f : (−a1 → b1 ), . . . , (−a→n → bn ) → b ∈Σ, the corresponding operationf φ : δ~a1 MΣ Zb1 × · · · × δ~al MΣ Zbl −→ MΣ Zb
is deﬁned byφf (Γ)(s1 , . . . , sl ) = fhh!θ∗ ||s1 || ...,!θ∗ ||sl ||iif (s1 , . . . , sl ).
τ ,ΓGiven an IDTS (Σ, R) and a V+Σ-algebra M , we deﬁne
the labelled rules with respect to M by
R = {φLτ ,0 l → φLτ ,0 r | Z ` l → r : τ ∈ R,
term-generated assignment φ : Z −→ M }.
Thus R is a set of rewrite rules consisting of labelled metaterms. So, (Σ, R) forms an IDTS that gives rewriting on Σterms.

Theorem 3.2 For each term-generated assignment φ :Z −→ M , (MΣ Z, [f φ ]f ∈Σ , ν φ , β φ ) is a Σ-monoid.

Notation 3.5 A meta-term of the form

Corollary 3.3 For each term-generated assignment φ :Z −→ M , the labelling map φL : MΣ Z −→ MΣ Z is
the unique Σ-monoid morphism from the free Σ-monoid to(MΣ Z, [f φ ]f ∈Σ , ν φ , β φ ) that extends η Z : Z −→ MΣ Z,
Z 7−→ Z .

in an IDTS is often abbreviated as just Z for a metavariable
Z ∈ Zb1 ,...,bn →b .

Proof It is clear that (η Z )∗ = φL by just comparing thedeﬁnitions of φL and the Σ-monoid extension (−)∗ . HenceφL gives a Σ-monoid morphism. ¤Lemma 3.4 Let φ : 0 −→ M and θ : Z −→ MΣ 0 be
assignments. Then(i) φL ◦ β = β φ ◦ (φL • φL ) .
∗(ii) φL ◦ θ∗ = (φL θ) ◦ (φ∗ θ)L .

rhs = (φL θ)∗ (φ∗ θ)L Z(~t)= (φL θ)∗ Z((φ∗ θ)L~t)= β φ (φL θ Z; (φL θ)∗ (φ∗ θ)L~t)= β φ (φL θ Z; φL θ∗~t) = lhs(by I.H.)¤

Moreover, we deﬁne the IDTS Decr (called “decreasing
rules”) over Σ to consist of the rules
fp (Z1 , . . . , Zl ) → fq (Z1 , . . . , Zl )for all f : (~τ 1 → σ 1 ), . . . , (~τ l → σ l ) → τ ∈ Σ and allp >S q ∈ Sf , where >S denotes the strict part of ≥S .
Using Lemma 3.4, we have the following key proposition
to establish semantic labelling.
Proposition 3.6 Let M be a quasi-model for an IDTS R. If
we have Γ ` s →R t : τ thenΓ ` φLτ ,Γ (s) →∗Decr · →R φLτ ,Γ (t)Proof (i) Since φL is a monoid morphism, the multiplication
β is preserved.
(ii) By induction on meta-terms in MΣ Z. The cases x andf (~s) ∈ MΣ Z τ (Γ) are straightforward. For the case Z(~t) ∈MΣ Z τ (Γ), we have the following.
lhs = φL θ∗ (Z(~t))= φL β(θ Z; θ∗~t) = β φ (φL θ Z; φL θ∗~t)

1. . . . n.Z(1, . . . , n)(by Lemma 3.4)

holds for the assignment φ : 0 −→ M .
Proof By induction on proof trees of →R .
(i) Case Γ ` θ∗τ ,Γ l →R θ∗τ ,Γ r : τ .
This is derived from Z|Γ ` l → r ∈ R where θ : Z −→MΣ 0. Let φ : 0 −→ M be the assignment. Now we havea labeled rule(φ∗ θ)Lτ ,Γ l → (φ∗ θ)Lτ ,Γ r ∈ R.
By Lemma 3.4 and closedness of R-rewrite by the valuation φL θ : Z −→ MΣ 0, we have∗φLτ ,Γ (θ∗τ ,Γ l) = (φL θ)τ ,Γ (φ∗ θ)Lτ ,Γ l∗

→R (φL θ)τ ,Γ (φ∗ θ)Lτ ,Γ r
= φLτ ,Γ (θ∗τ ,Γ r)(ii) Case Γ ` f (. . . , s, . . .) →R f (. . . , t, . . .) : τ .
This is derived from Γ, Θ ` s →R t : σ. Since (M, ≥M )is a quasi-model, we have !θ∗σ,Γ+Θ s ≥Mσ (Γ+Θ) !θ∗σ,Γ+Θ t
for an term-generated assignment φ =!θ into M . By
induction hypothesis, we have φLσ,Γ+Θ s →∗Decr · →R
φLσ,Γ+Θ t. Notice also that hh−ii is weakly monotone. So,
φLτ ,Γ (f (. . . , s, . . .))= fhh...,!θ∗ ~ s,...ii
n+i

τ ,Γ

(. . . , φLσ,Γ+Θ s, . . .)→∗Decr fhh...,!θ∗σ,Γ+Θ t,...ii

τ ,Γ(. . . , φLσ,Γ+Θ s, . . .)→∗Decr · →R fhh...,!θ∗σ,Γ+Θ t,...ii

τ ,Γ

propagation rules are interpreted as the same λ-terms, i.e.
not decreasing. In this section, we give a short termination
proof of RλX via higher-order semantic labelling.
4.1

First, we formulate the simply-typed λX-calculus as an
IDTS. This means to give an inductive type for λX-terms.
We ﬁx the set BType of base types for the λX-calculus.
We choose the IDTS-alphabet consisting of the following
IDTS’s base types B and signature ΣλX :
BType
B
vσ
apσ,τ
λσ,τ
xsubσ,τ

(. . . , φLσ,Γ+Θ t, . . .)= φLτ ,Γ (f (. . . , φLσ,Γ+Θ t, . . .))¤Theorem 3.7 (Higher-order semantic labelling) Let M
be a quasi-model for an IDTS R and R the labelled IDTS
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. 3.6. [⇒]: By erasing all labels in rewrite steps. ¤4.

Termination of λX via Higher-Order
Semantic Labelling

As an application of higher-order semantic labelling, we
prove the termination of an explicit substitution system λXcalculus [5, 4]. The λX-calculus uses explicit names and is
known as the simplest explicit substitution system; it has
no composition of substitutions. The following is the λXcalculus taken from [4].
(λx.M )N → M hx := N i(M N )hx := Ki → M hx := Ki N hx := Ki(λy.M )hx := Ki → λy.M hx := Ki

if x 6= y

xhx := Ki → K
M hx := Ki → M

if x 6∈ FV(M )The λX-calculus has good properties: conﬂuence and preservation of strong normalisation (PSN), and the simply typed
λX-calculus is strongly normalising.
Proving termination of the simply-typed λX-calculus is
not an obvious task. Actually, the direct proofs using the
reducibility method are rather involved and long [15, 23].
Moreover, the λX-calculus as an IDTS does not follow theGeneral Schema [1] directly since a precedence between theapplication and the explicit substitution operators cannot be
determined from the rules. It is also difﬁcult to interpretthese rules by some “measure” that is strictly decreasing by
a well-founded order. A candidate of such interpretation is tointerpret λX-terms as simply-typed λ-terms. But we immediately ﬁnd that this does not succeed since the substitution

Formulating λX-calculus as an Inductive Data
Type System3ι3 σ, τ ::= ι | Varτ | Arr(σ, τ ): Varσ → σ: Arr(σ, τ ), σ → τ: (Varσ → τ ) → Arr(σ, τ ): (Varσ → τ ), σ → τ

The type Varσ represents the type of λX’s variables of typeσ, and the type Arr(σ, τ ) represents the λX’s arrow type. We
may also assume constants of type Varσ .
The use of a type Varσ → τ to represent binders of λterms is known in the ﬁeld of mechanized reasoning. It isan essential idea to implement higher-order abstract syntax(HOAS) that admits induction in Coq [9]. Semantic analysis
uncovers algebraic structures of HOAS: Fiore, Plotkin andTuri’s binding algebra [11], which is also used as the semantic basis of our theory. This relates to modeling arrow types
by the context extension: actually, δ σ A ∼= Vσ → A holds[11, 10].
This inductive representation is important for the termination proof. The General Schema requires strict positivity and an existence of a well-founded order on base types
as its assumption [3, 1]. The signature ΣλX actually satisﬁes these conditions by taking v, ap, λ as the constructorsof Arr-types. The reason we do not just reuse the IDTS’s
arrow type σ → τ for the λX’s arrow type is that it does
not satisfy such strict positivity condition. A naive choice
λσ,τ : (σ → τ ) → (σ → τ ) for abstractions has a negative occurrence of a type (consider λσ,σ ). Precise deﬁnitionsof these conditions on the General Schema are postponed toSect. 5.
The λX-calculus is formulated as the IDTS (ΣλX , RλX )given in Fig. 1 which does not follow the General Schema
yet. For readability, we write shx := ti for xsubσ,τ (xVarσ. s, t)
and omit types.
4.2

Termination proof

First we observe that the IDTS RλX has a quasi-model
consisting of all simply-typed λ-terms, which will be used as
the label structure. Let `λ denote the judgment relation ofdthe simply-typed λ-calculus. We deﬁne the translation (−)
from the IDTS’s base types B to simple types as follows:bι = ι

[τ = bVarτ\τ ) = σArr(σ,b→bτ.

ap(λx.s)t (λ(x.M (x)), N ) → M (x)hx := N is[x:=t]
aps t (M (x), N (x))hx := Kis[x:=u]t[x:=u] → aps[x:=u]t[x:=u] (M (x)hx := Kis[x:=u] , N (x)hx := Kit[x:=u] )λ(y.M (x, y))hx := Ki(λy.s)[x:=u] → λ(x.M (y, x)hy := Kis[x:=u] )v(x)hx := Kiu → K
M hx := Kis → M.
The set Decr of decreasing rules is consisting of the rules for all s > t ∈ S
aps (M, N ) → apt (M, N )M (x)hx := Kis → M (x)hx := Kit .
Figure 2. The labelled IDTS RλX ∪ Decr
For an IDTS’s context Γ, we denote by Γ̂ a λ-calculus’s
context obtained by applying this translation to each typein Γ. We deﬁne the presheaf Λ of all λ-terms by Λτ (Γ) ={t | Γ̂ `λ t : τ̂ }. The presheaf Λ has an obvious ΣλX term algebra structure that interprets the symbols v, λ, ap in
λX as variable, abstraction, application operations in the λcalculus:Varτ) = xτvΛτ (Γ)(xσλΛσ,τ (Γ)(t) = λx .tapΛ
σ,τ (Γ)(s, t) = s t
and the operation for the explicit substitutionxsubΛ
σ,τ (Γ) : Λτ (Γ + Varσ ) × Λσ (Γ) → Λτ (Γ);
xsubΛσ,τ (Γ)(s, t) = s[x := t]that interprets explicit substitution as the “meta-level” substitution. This shows that the presheaf Λ forms a V + ΣλX algebra.
We deﬁne the family of partial orders < on Λ by s <τ ,Γt ⇔ s →∗β t for Γ `λ s : τ , Γ `λ t : τ . Then (Λ, <)is a weakly monotone ΣλX -algebra. Since the unique homomorphism X(−) from the initial V + ΣλX -algebra TΣλXV
to the V + ΣλX -algebra Λ evaluates all explicit substitutions (cf. [12] for more detailed treatment of algebraic characterisation of explicit substitutions), for any ground (w.r.t.
metavariables) instance Γ ` l → r : τ of rules of RλX , wehaveX τ ,Γ (l) < Xτ ,Γ (r).
Thus (Λ, <) is a quasi-model of (ΣλX , RλX ).
Using this, we attach labels to the IDTS RλX . We label
the function symbols ap and xsub. S
We choose the semanticlabel set S = Sap = Sxsub = τ ,Γ Λτ (Γ). Deﬁne thewell-founded partial order on S by s ≥ t ⇔ s (→βap∪ B )∗ t. The semantic label maps are deﬁned by hhs, tiiΓ =xsub
s t, hhs, tiiΓ = s[x := t], which are weakly monotone.

The labelled IDTS RλX consists of the rules generated byassigning to M 7→ s, N 7→ t, K 7→ u for all s, t, u ∈ Sgiven in Figure 2.
We take the precedence A ordered by for all s > t ∈ S,
aps A xsubt A apt A λ. Since the base types B is notchanged in the labelled system, the positivity conditions are
satisﬁed. Then, RλX ∪ Decr follows the General Schema.
Hence RλX is terminating.
The idea of the use of labelling to prove termination of
λX is also taken in [4], where a transformation of λX to aﬁrst-order TRS and a variant of ﬁrst-order semantic labellingare used. The crucial difference is that we have used higherorder semantics (λ-terms) rather than ﬁrst-order one givenby the maximal reduction lengths of λ-terms in [4].
Our approach to use a term model has generality not only
for the case of λX. In the next section, we will consider otherapplications.

5.

Labelling with Higher-Order Term ModelIn the termination proof of λX, we have used the term modelΛ for labelling. In the ﬁrst-order case, semantic labellingwith a term model were considered under the name selflabelling [27] by Middeldorp, Ohsaki, and Zantema, andshowed its usefulness by applying it to several different
termination problems of TRSs. In this section, we extend it
to the higher-order case. We ﬁrst review some notions of theassumption of the General Schema [3, 1].
Deﬁnition 5.1 Let (B, Σ, Z) be an IDTS-alphabet. We assume that each base type τ ∈ B has an associated set of
constructors taken from Σ. The set of all declarations of constructors deﬁnes a preorder ≤B on B by τ ≤B σ if τ occursin ~α for a constructor c : ~α → σ. Any constructor must not
be the root symbol of left-hand side of a rewrite rule. Let=B be the equivalence relation generated by ≤B . An inductive type σ is strictly positive if for any type τ s.t. τ =B σ,τ does not occur at a negative position of the type of a constructor c for σ.
A metavariable Z is accessible in a meta-term t if there are
distinct bound variables ~x such that Z(~x) ∈ Acc(t), where
Acc(t) is the least set satisfying the following clauses:(i) t ∈ Acc(t).
(ii) if x.t ∈ Acc(t) then t ∈ Acc(t).
(iii) if c(~s) ∈ Acc(t) then each si ∈ Acc(t).
(iv) if f (~s) ∈ Acc(t) and si is of basic type then si ∈ Acc(t).
(v) if Z(~s) ∈ Acc(t) and Z does not occur in ~s and t, theneach si ∈ Acc(t).
More schematically, a metavariable Z is accessible int if Z appears as like t = f (. . . , c(. . . , ~x.Z(~s), . . .), . . .),where any constructor c can be nested any number of(including 0) times. So, for example, M is accessible inap(λ(x.M (x)), N ). Actually, all metavariables in the lefthand sides of RλX are accessible. Next we introduce somenotions for termination of IDTSs.
Deﬁnition 5.2 (Solid meta-term) A meta-term t is called
solid if for each meta-application Z(s1 , . . . , sn ) in t, all si
do not contain function symbols.
The notion of solid meta-term is crucial in our theory
presented below. This ensures that in many cases unexpectedvanishing of redexes, which is a typical pitfall of termination
proofs, does not happen. See Remark 5.7.
Deﬁnition 5.3 We also call an IDTS (B, Σ, R) solid if (i)all types in B are strictly positive and ≤B is well-founded,
and for each rule l → r ∈ R, (ii) all metavariables in r areaccessible in l, and (iii) r is solid.
Note that the left-hand side l is already solid since so are
Miller’s higher-order patterns. Fortunately, the conditions ofsolid IDTSs are not so restrictive requirements in practice.
An example of solid IDTS is the λX-calculus RλX . The
simply-typed λβ-calculus is also solid. All examples except
for recursor rules in [3, 1] are solid. It also means that there
are terminating IDTSs that are not solid.
Deﬁnition 5.4 We call an IDTS R precedence terminating
if there exists a well-founded order A on function symbols(called a precedence) such that for every rule f (~t) → r ∈ R,
and every g ∈ Fun(r), f A g, where Fun(r) denotes the setof all function symbols in r.
Lemma 5.5 Every precedence terminating solid IDTS is
terminating.
Proof For each l → r ∈ R, by the deﬁnition of theGeneral Schema and an easy induction argument, r is in acomputable closure [1] of l. ¤The solid property is required to use the General Schemain the above proof. Currently, we do not know how it is

weakened. The next theorem states that any terminating
solid IDTS can be transformed into a precedence terminating
IDTS by labelling.
Theorem 5.6 Let (Σ, R) be a terminating solid IDTS and(Σ, R) its labelled IDTS by the quasi-model (TΣV, →∗R ).
Then, (Σ, R ∪ Decr) is precedence terminating.
Proof DeﬁneSthe semantic label set for each f ∈ Σ by
Sf = S = τ ,Γ TΣVτ (Γ) with the well-founded partial
order ≥= (→R ∪ B )∗ , and the semantic labelling map
fhh~sii = f (~s).
By semantic labelling with S, we have (Σ, R). Deﬁne theprecedence on Σ by
fs A gt ⇔ s > t.
We check that R ∪ Decr is precedence terminating.
• Case l → r ∈ R. There exist Z ` l → r ∈ R and avaluation φ : Z −→ TΣV such that l = φL l → φL r =r ∈ R. The label of the root function symbol of l isφ∗ l. Any label p of a function symbol in r is obtainedby p = φ∗ (t) for some subterm t E r. Thenφ∗ l →R φ∗ r D φ∗ t = p.

(1)

• Case fs (~Z) → ft (~Z) ∈ Decr with s > t. Hence fs A ft .
¤Remark 5.7 The condition that r must be solid is essential
to establish the subterm property in (1). In higher-ordercase, the subterm relation is not closed under valuations, i.e.
s B t ⇒ φ∗ s B φ∗ t does not hold in general, whereas inﬁrst-order case it obviously holds. Consider Z(f ) B f where
f is a function symbol. Applying a valuation Z 7→ c, we havecB
6 f . This is due to the fact that Z(f ) is not solid.
The proof of Thm. 5.6 is important. This particular semantic labelling, i.e. taking a term algebra as semantics andthus labelling function symbols with terms is useful to showpreservation of termination of extension of a terminating
system. For instance, the termination proof of λX-calculus
given in Sect. 4 is an example of semantic labelling with aterm algebra along this scheme.
5.1

Currying transformation

Kennaway, Klop, Sleep, and de Vries showed the preservation of termination under currying in [20] for ﬁrst-order
TRSs. Then, Middeldorp et al. gave alternative proof using
self-labelling [27]. In this subsection we extend this result tothe higher-order case via higher-order semantic labelling.

Deﬁnition 5.8 Let (B, Σ, R) be an IDTS. Deﬁne the newbase type set Bap by
Bap 3 τ ::= ι | Arr(α, τ )α ∈ I(B)Deﬁne the signatures byΣp = {fi : α1 , . . . , αi → Arr(αi+1 , . . . , Arr(αn , τ ))| f : α1 , . . . , αn → τ ∈ Σ, f 6= ap}
Σa = {apα,τ : Arr(α, τ ), α → τ | α ∈ I(B), τ ∈ Bap }Σap = Σ ∪ Σa ∪ Σp ,and assume that all fi (i 6= n) are constructors. The IDTS
(Bap , Σap , Rap ) is the union of R and the set of the following
rules, called ap-rules:
ap(fi (Z1 , . . . , Zi ), Z) → fi+1 (Z1 , . . . , Zi , Z)
for all i = 1, . . . , n − 1, f : σ 1 , . . . , σ n → τ ∈ Σ, where
fn is written as f .
Namely, Rap has all curried functions generated from Σ.
A problem is whether termination is preserved under this addition. One would expect that this should hold, but its proof
is not entirely obvious. A naive approach based on simulation of Rap -reduction by R-reduction is not applicable since
1-step Rap -reduction using ap-rule may become 0-step Rreduction. The ﬁrst proof of this theorem for TRSs in [20]needs rather involved analysis (about four page long). Semantic labelling with higher-order terms is again useful.
Theorem 5.9 Assume all fi 6∈ Σ, and ap does not appear
in R. If a solid IDTS (B, Σ, R) is terminating, its curriedversion (Bap , Σap , Rap ) is terminating.
Proof Deﬁne the weak monotone Σap -algebra
T = (TΣapV, →∗(Σap ,R) )with the operation for apα,τ : Arr(α, τ ), α → τ where
α = ~a → b by
apTτ : TΣapVArr(α,τ ) × δ~a (TΣapV)b → TΣapVτ
apTτ (Γ)(x, t)= ap(x, t)
if x ∈ Γ
apTτ (Γ)(fi (s1 , . . . , si ), t) = fi+1 (s1 , . . . , si , t) if i 6= n
apTτ (Γ)(f (s1 , . . . , si ), t) = ap(f (s1 , . . . , si ), t) if f 6= fi
and the usual term algebra interpretations for symbols in Σ.
Monotonicity of apT is shown by induction on the proof
trees of →R . Then, T is a quasi-model of (Σap , Rap ) since(i) for each rule in R, it is clearly decreasing by →R , (ii)for each ap-rule, both sides of the rule are interpreted asfi+1 (s1 , . . . , si , t).
S
Take the semantic label set S = σ,Γ TΣapVσ (Γ) with the∗well-founded partial order s ≥ t ⇔ s (→(Σap ,R) ∪ B ) t.
By applying semantic labelling with S, we have the labelled

IDTS Rap , in which each label is a term obtained by evaluating all ap’s. Take the precedence
aps A apt A fs A ft

∀f (6= ap) ∈ Σap , ∀s > t ∈ S

Then, Rap ∪ Decr is precedence terminating since (a) for
each rule in R, similar to the proof of Thm. 5.6, (b) for eachlabelled ap-rule, aps is greater than fs . Moreover, since eachfi is a constructor, all ap-rules are solid, (c) for each rule in
Decr, similar to the proof of Thm. 5.6. By Lemma 5.5, Rap
is terminating. ¤5.2

Modularity with Higher-Order Recursive Program
Schemes

A recursive program scheme (RPS) (cf. survey [7]) is a simple form of ﬁrst-order functional program, which is given as
a set of ﬁrst-order rewrite rules of the formf (x1 , . . . , xn ) → t
with distinct x’s such that for every function symbol f in asignature there exists at most one such rule.
We consider its higher-order extension. By a higher-orderrecursive program scheme (HO-RPS), we mean an IDTS
(Σ, R, Z) consisting of the following form of rules with
distinct metavariable Z’s and the same condition for f as
RPS:
f (1 . . . i1 .Z1 (1, . . . , i1 ), . . . , 1 . . . in .Zn (1, . . . , in )) → t
for f : (~a1 → b1 ), . . . , (~al → bl ) → b ∈ Σ. Notice that now
t is a (higher-order) meta-term.
Using semantic labelling with a higher-order term modeland precedence termination, we prove the following: thecombination of an arbitrary terminating solid IDTS and aterminating solid HO-RPS that deﬁnes new functions is terminating. To the author’s best knowledge, this is a new result
on modularity of termination of higher-order rewrite rules.
Modularity of higher-order rewriting is known as a difﬁcult and subtle problem. Van Oostrom observes that almost
no property is modular by ﬁnding many tricky counterexamples to modularity of higher-order rewriting systems [30].
He also remarks that extending a signature of a terminating CRS does not necessarily preserves termination [29, 30].
However, our new notion of solid system successfully avoids
such a counterexample. First, we show a lemma that statestermination is preserved under signature extension for solid
HO-RPSs.
Lemma 5.10 Let (B, Θ, S) be a terminating solid HO-RPS,(B0 , Θ0 ) an alphabet such that all types in B ∪ B 0 are strictly
positive, and ≤B∪B0 is well-founded. Then, the solid IDTS
(B ∪ B 0 , Θ ∪ Θ0 , S) is terminating.
Proof It is easy to see that for a terminating solid HO-RPS(B, Θ, S), the precedence A deﬁned in Def. 5.4 is wellfounded order on Θ. Hence (B, Θ, S) is also precedenceterminating. Then, (B ∪ B 0 , Θ ∪ Θ0 , S) is again precedence
terminating using the same precedence A regarded as a strict
partial order on Θ ∪ Θ0 , since the rules are unchanged. ¤Theorem 5.11 Let (B, Σ, R) be a terminating solid IDTS
and (B 0 , Θ, S) a terminating solid HO-RPS such that(i) all types in B∪B 0 are strictly positive, and ≤B∪B0 is wellfounded,(ii) Σ ∩ Θdef = ∅,where Θdef is the subset of Θ consisting of all f such that
there is a corresponding rule in Θ. Then (B ∪ B0 , Σ ∪ Θ, R ∪S) is terminating.
Proof We denote by t↓S the normal form of t by the rewrite→(Σ∪Θ,S) . Let Σ0 = (Σ ∪ Θ) − Θdef . We show that if(Σ0 , R) is terminating then (Σ ∪ Θ, R ∪ S) is terminating byfollowing the scheme of the proof of Thm. 5.6. In this case
we use the Σ ∪ Θ-algebra T = (TΣ0V, →∗(Σ0 ,R) ) deﬁned forf ∈ Θdef by
f T (~t) = f (~t)↓S
and other operations are deﬁned by the usual term algebra operations. The operation f T is well-deﬁned by thefollowing reasons. Since (Σ ∪ Θ, S) is orthogonal, (Σ ∪Θ, S) is conﬂuent [21]. Since (B, Θ, S) is terminating, (B ∪B 0 , Σ ∪ Θ, S) is also terminating by Lemma 5.10. Since(B∪B 0 , Σ∪Θ, S) is terminating and conﬂuent, the S-normal
form f (~t) ↓S is unique and always in TΣ0V (i.e. all Θdef symbols are consumed).
We show that T is a quasi-model of (Σ ∪ Θ, R ∪ S).
(i) Weak monotonicity of T . For f ∈ Σ0 , its operation isitself, so monotone. For f ∈ Θdef , by Lemma B.2 inAppendix.
(ii) We show that T satisﬁes all rules in R ∪ S. Take θ :Z −→ TΣ0V.
(ii-a) Case l → r ∈ R. θ∗ l →R θ∗ r.
(ii-b) Case l → r ∈ S. Since lθ →S rθ,θ∗ l = (lθ)↓S = (rθ)↓S = θ∗ r.
For a well-founded poset of semantic labels, we take[( TΣ0Vσ (Γ), (→(Σ0 ,R) ∪ B )∗ ).
σ,Γ

The precedence is deﬁned by fs A gt if(i) for f, g ∈ Σ0 or f, g ∈ Θdef , s (→(Σ0 ,R) ∪ B )+ t, or

6.

Conclusion

We have presented a theory of higher-order semantic labelling for inductive data type systems (IDTSs). The technical novelty is to handle metavariables and higher-order functions in IDTSs for the labelling process. This is done by exploiting typed binding algebras and the author’s previous results on algebraic semantics of higher-order syntax [13] andhigher-order rewriting [14]. Typed binding algebras are algebras in the presheaf category (SetF↓B )B where B is a set oftypes and F is skeleton of the category of ﬁnite sets modelingbinding in the style of Fiore, Plotkin and Turi [11].
We have given a number of applications of higher-order
semantic labelling: it shows termination of the λX-calculus,
preservation of termination under currying and a new modularity result. This shows usefulness of higher-order semanticlabelling.

References[1] F. Blanqui. Termination and conﬂuence of higher-orderrewrite systems. In Rewriting Techniques and Application(RTA 2000), LNCS 1833, pages 47–61. Springer, 2000.
[2] F. Blanqui. (HO)RPO revisited. Technical Report 5972,
INRIA, 2006. Research report.
[3] F. Blanqui, J.-P. Jouannaud, and M. Okada. Inductive data
type systems. Theoretical Computer Science, 272:41–68,
2002.
[4] R. Bloo and H. Geuvers. Explicit substitution: on the edge ofstrong normalization. Theor. Comput. Sci. 211, 1-2:375–395,
1999.
[5] R. Bloo and K. H. Rose. Preservation of strong normalisationin named lambda calculi with explicit substitution andgarbage collection. In CSN-95: Computer Science in the
Netherlands, pages 62–72, 1995.
[6] C. Borralleras and A. Rubio. A monotonic higher-order
semantic path ordering. In Procs. 8th International Conference on Logic for Programming, Artiﬁcial Intelligence andReasoning (LPAR), LNCS 2250, pages 531–547, 2001.
[7] B. Courcelle. Recursive application schemes. In J. van
Leeuwen, editor, Handbook of Theoretical Computer Science,
pages 459–492. 1990. Chapter 9, vol. B.
[8] N. de Bruijn. Lambda calculus notation with namelessdummies, a tool for automatic formula manipulation, withapplication to the church-rosser theorem. Indagationes
Mathematicae, 34:381–391, 1972.

(ii) for f ∈ Θdef , g ∈ Θ such that f (~Z) → r ∈ S andg ∈ Fun(r).

[9] J. Despeyroux, A. Felty, and A. Hirschowitz. Higher-orderabstract syntax in Coq. In Typed Lambda Calculi andApplications, LNCS 902, pages 124–138, 1995.

Then, it is easy to see that R ∪ S ∪ Decr is precedence
terminating. ¤This theorem is applicable to any terminating solid IDTS
and HO-RPS, i.e. even one that does not follow the General
Schema. Hence this theorem is not obtained by a direct
application of the General Schema criterion.

[10] M. Fiore. Semantic analysis of normalisation by evaluation
for typed lambda calculus. In 4th International Conference on
Principles and Practice of Declarative Programming (PPDP
2002), pages 26–37. ACM Press, 2002.
[11] M. Fiore, G. Plotkin, and D. Turi. Abstract syntax andvariable binding. In Proc. 14th Annual Symposium on Logic

in Computer Science, pages 193–202, 1999.
[12] N. Ghani, T. Uustalu, and M. Hamana. Explicit substitutions
and higher-order syntax. Higher-Order and Symbolic
Computation, 19(2/3):263–282, 2006.
[13] 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.
[14] M. Hamana. Universal algebra for termination of higherorder rewriting. In Proceedings of 16th International
Conference on Rewriting Techniques and Applications(RTA’05), LNCS 3467, pages 135–149. Springer, 2005.
[15] D. J.Dougherty and P. Lescanne. Reductions, intersection
types, and explicit substitutions. Mathematical Structures in
Computer Science, 13(1):55–85, 2003.
[16] J.-P. Jouannaud and A. Rubio. The higher-order recursive
path ordering. In Proc. LICS’99, pages 402–411. IEEE,
1999.
[17] J.-P. Jouannaud and A. Rubio. Higher-order orderings fornormal rewriting. In Proc. of RTA’06, LNCS 4098, pages
387–399, 2006.
[18] J.-P. Jouannaud and A. Rubio. Polymorphic higher-orderrecursive path orderings. Journal of ACM, 54(1), 2007.
[19] S. Katsumata. A generalisation of pre-logical predicates tosimply typed formal systems. In ICALP, pages 831–845,
2004.
[20] J.R. Kennaway, J.W. Klop, M.R. Sleep, and F.J. de Vries. On
comparing curried and uncurried rewrite systems. Journal of
Symbolic Computation, 21(1):15–39, 1996.
[21] J.W. Klop. Combinatory Reduction Systems. PhD thesis,
CWI, Amsterdam, 1980. volume 127 of Mathematical Centre
Tracts.
[22] 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.
[23] S. Lengrand, P. Lescanne, D. J.Dougherty, Mariangiola
Dezani-Ciancaglini, and Steffen van Bakel. Intersection types
for explicit substitutions. Information and Computation,
189(1):17–42, 2004.
[24] P. Lescanne and J. Rouyer-Degli. Explicit substitutions withde Bruijn’s levels. In Rewriting Techniques and Applications,
6th International Conference (RTA-95), LNCS 914, pages
294–308. Springer, 1995.
[25] S. Mac Lane. Categories for the Working Mathematician,volume 5 of Graduate Texts in Mathematics. Springer-Verlag,
New York, 1971.
[26] M. Miculan and I. Scagnetto. A framework for typed
HOAS and semantics. In Fifth ACM-SIGPLAN International
Conference on Principles and Practice of Declarative
Programming (PPDP’03), pages 184–194. ACM Press, 2003.
[27] A. Middeldorp, H. Ohsaki, and H. Zantema. Transforming
termination by self-labelling. In Proceedings of the 13th
International Conference on Automated Deduction, LNCS

1104, pages 373–386, 1996.
[28] T. Nipkow. Higher-order critical pairs. In Proc. 6th IEEE
Symp. Logic in Computer Science, pages 342–349, 1991.
[29] V. van Oostrom. Conﬂuence for Abstract and Higher-Order
Rewriting. PhD thesis, Vrije Universiteit, Amsterdam, 1994.
[30] V. van Oostrom. Counterexamples to higher-order modularity. Draft, 2005.
[31] J. van de Pol. Termination proofs for higher-order rewrite
systems. In the First International Workshop on HigherOrder Algebra, Logic and Term Rewriting (HOA’93), LNCS
816, pages 305–325, 1994.
[32] F. van Raamsdonk. On termination of higher-order rewriting.
In Rewriting Techniques and Applications, 12th International
Conference (RTA 2001), pages 261–275, 2001.
[33] M. Tanaka and J. Power. A uniﬁed category-theoretic
formulation of typed binding signatures. In Proc. of the 3rd
ACM SIGPLAN workshop on Mechanized reasoning about
languages with variable binding (MERLIN’05), pages 13–24,
2005.
[34] Terese. Term Rewriting Systems. Number 55 in Cambridge
Tracts in Theoretical Computer Science. Cambridge University Press, 2003.
[35] H. Zantema. Termination of term rewriting by semanticlabelling. Fundamenta Informaticae, 24(1/2):89–105, 1995.

A.

The Σ-monoid MΣ Z

We describe the Σ-monoid structure of MΣ Z. The unit of
the monoid MΣ Z is ν φ : V → MΣ Z as described in Sect.
3. The multiplication β φ : MΣ Z • MΣ Z −→ MΣ Z isβ φτ,Γ (xτ ; ~t) = tx
β φτ,Γ (Z[s1 , . . . , sl ]; ~t) = Z[β φτ,Γ (s1 ; ~t), . . . , β φτ,Γ (sl ; ~t)]β φτ,Γ (fq (s1 , . . . , sl ); ~t)= fp (β φ (s1 ; upn+i1 (~t), n+1, . . . , n+i1 ), . . .)where
p = hh!θ∗ ||β φ (s1 ; upi1 (~t), n + 1, . . . , n + i1 )||, . . .iib,Γf : (~a1 → b1 ), . . . , (~al → bl ) → b ∈ Σ,|~ak | = ik(for each k),|Γ| = n,|~t| = m.

Note that the length of “upi1 (~t), n + 1, . . . , n + i1 ” ism + i1 , and it renames a variable m + k to n + k for eachk = i1 , . . . , il to make bound variables sense.
To check that MΣ Z satisﬁes the monoid law is straightforward induction on meta-terms. To check the Σ-monoid
law β φ ◦ ([f φ ]f ∈Σ • id) = [f φ ]f ∈Σ ◦ Σβ φ ◦ st, we instantiate this at Γ ∈ F ↓ B and chase an element. This eventually
becomes the equality
β φb,Γ (fr (s1 , . . . , sl ); ~t)= fp (β φ (s1 ; upi1 (~t), n+1, . . . , n+i1 ), . . .)where r = hh!θ∗ |s1 |, . . . , !θ∗ |sl |iib,Γ and p is the one given
above. This obviously holds by the deﬁnition of β φ .

B.

Lemmas for Proposition 5.11

Lemma B.1 Let θ : Z −→ TΣ0V, t ∈ MΣ∪Θ Z(Γ).
(θt)↓S = θ(t↓S )Proof Let t↓S be the normal form of t by rewriting on metaterms by S. Then tθ →∗S = (t ↓S )θ is a S-normal form.
Suppose tθ →!S m. Since S has the unique normal form
property (UN, cf. [34]), m = (t↓S )θ. Hence (θt)↓S = θ(t↓S). ¤Lemma B.2 Let f ∈ Θdef . Thens →R t ⇒ f (. . . , s, . . .)↓S →∗R f (. . . , t, . . .)↓S .
Proof By case analysis of proof trees of →R .
(i) Case lθ →R rθ for Z ` l → r : b ∈ R, θ :Z −→ TΣ0V. We show f (lθ) ↓S →R f (rθ) ↓S for aunary f . The n-ary cases are similar. Take valuations
θ0 : M 7→ lθ, θ 00 : M 7→ rθ where M is a fresh
metavariable. By Lemma B.1,f (lθ)↓S = (θ0 f (M ))↓S
= θ0 (f (M )↓S )→∗R θ00 (f (M )↓S )= (θ00 f (M ))↓S
= f (rθ)↓S .

(ii) Case g(. . . , s, . . .) →R g(. . . , t, . . .). Similar to the case(i). Now we take θ0 : M 7→ g(. . . , s, . . .), θ00 : M 7→g(. . . , t, . . .).
¤