日本ソフトウェア科学会第 35 回大会 (2018 年度) 講演論文集

関数プログラム・計算系の分割停止性検証:
外山-Klop-Barendregt の定理の高階化
浜名 誠
高階関数プログラムや計算体系を分割して停止性検証を行うことのできる新しい定理を提示する。本論文では、二階計算のためのフレームワークと証明の概略、そして定理に基づく検証法を実装した SOL システムについて紹介する。本方法は実際に有効で SOL システムは 2018 年度の国際停止性コンペティションの高階停止性部門にて、自動証明数の最高スコアを獲得した。

1 Introduction
Suppose that there are two terminating functional programs A and B. One asks you a question: Is the combination of two programs A + B
terminating? In other words, is evaluation of any
expression involving functions deﬁned in A and B
terminating?
The answer seems to be YES, i.e., A + B shouldbe terminating. However, it is NO, in general.
Toyama’s counterexample.
An example byToyama [17] illustrates this situation. Consider
the following two functional programs prog1 andprog2:
prog1 = [|rule|f(0,1,X) => f(X,X,X) |]prog2 = [|rule|or(X,Y) => X
or(X,Y) => Y|](This is written in the language of termination
checker SOL system [10] [11].) The prog1 consistsof one rule for the function f, which is deﬁned only
when the ﬁrst argument is 0 and the second argument is 1. In other cases, computation is stuck.
For example, the evaluation of f(0,0,0) does notproceed further by prog1.
The prog2 consists of the binary function
or, which returns one of the arguments nondeterministically. Both prog1 and prog2 are terDivide-and-Conquer Second-Order Termiantion
This is an unrefereed paper. Copyrights belong to theauthor.
Makoto Hamana, 群馬大学 理工学府, Dept. of Computer Science, Gunma University.

minating separately.
However, the combination prog1+prog2 is not
terminating, because evaluating the expressionf(or(0,1),or(0,1),or(0,1)), the following computation happens:f(or(0,1),or(0,1),or(0,1))=> f(0,or(0,1),or(0,1))=> f(0,1,or(0,1))=> f(or(0,1),or(0,1),or(0,1))

The ﬁnal expression is the same as the initial expression, hence it is non-terminating. This example
shows that termination cannot be checked modularly in general.
One may wonder this unexpected result is dueto the presence of non-deterministic function or
in prog2, and purely functional language, suchas Haskell or Agda, does not admit such a nondeterministic function.
Drosten’s counterexample.
However, nondeterminism is not essential to the non-modularityof termination. There is a counterexample consisting of only deterministic functions, which is given
by Drosten [3].
prog3 = [|rule|f(0,1,X) => f(X,X,X) ; 0 => 2
f(X,Y,Z) => 2
; 1 => 2|]

prog4 = [|rule|g(X,Y,Y) => X|]

; g(Y,Y,X) => X

Both prog3 and prog4 are deterministic and terminating. But prog3+prog4 is not terminating:f(g(0,1,1),g(0,1,1),g(0,1,1))=> f(0,g(0,1,1),g(0,1,1))=>> f(0,g(2,2,1),g(0,1,1))=> f(0,1,g(0,1,1))=> f(g(0,1,1),g(0,1,1),g(0,1,1))

Although these two examples are rather simple,

they show termination checking cannot be done
modularly. This implies that we cannot expect
modular termination checking of larger or more realistic functional programs in general.
But practically, we seriously need modular termination checking. We need to ﬁnd a suﬃciently
large class that admits it. In the theory of rewriting, an important modular termination result has
been known.

to higher-order functional programs. We will show
eﬀectiveness of this theorem in §3 and §2. In thispaper, we show the following new theorem.

Theorem 6.11 (Modular termination). Let(ΣC ] Θ, C) and (ΣC ] ΣQ ] Θ, Q) be second-ordercomputation systems such that(i) ΣC is the deﬁned function symbols of C,(ii) ΣQ is the deﬁned function symbols of Q,(iii) Θ is the signature for constructors,
Theorem 1.1 (Toyama-Klop-Barendregt 1995 (iv) ΣC ∩ ΣQ = ∅ and C is solid,[18]) Termination is modular for disjoint sum of(v) (ΣC ]Θ, C) extended with tuples and projection
left-linear conﬂuent and terminating ﬁrst-orderrules is terminating,term rewriting systems.
(vi) (ΣC ] ΣQ ] Θ, Q) is terminating by the General
Schema,Note that the examples of prog1,prog2 (where (vii) >T is well-founded, every constructor is posiprog2 is not conﬂuent) and prog3,prog4 (where
tive, and >ΣC ]ΣQ ]Θ is well-founded,
prog4 is not left-linear) are not in the scope of thisThen (ΣC ] ΣQ ] Θ, C ] Q) is terminating.
theorem.
From the viewpoint of modern functional programming languages (such as Haskell) and automated proof checkers (such as Agda and Coq),
Thm. 1.1 is unfortunately rather weak.

The terminology, details and the proof strategy ofthis theorem are explained in this paper. Roughly
speaking, this theorem states that if two higherorder functional programs C and Q are terminating,which can share functions and data structures, andsatisﬁes, the combination of C and Q is again terminating. Our theorem improves the following important aspects of Toyama-Klop-Barendregt’s theorem.

•

First-order term rewriting systems admit onlyﬁrst-order functions, which excludes the λcalculus. This is not realistic in view of modern
functional programming.

•

Disjoint sum means that two rewrite systems
cannot share the same function symbols. Thisis again not realistic in programming setting.
E.g., a user program uses functions deﬁned in alibrary program. Both a library and a user program use the same data structure, such as lists(which means nil and cons function symbols
are shared in two programs, i.e., not disjoint).
Such a usual situation is excluded in the disjoint
setting.

•

Second-order rules are allowed, rather thanﬁrst-order. This includes various typed λcalculus, such as computational λ-calculus, callby-need λ-calculus, linear λ-calculus, and computational meta-language (of any higher-order)[10] [11].

•Sharing functions and constructors, rather
than disjoint union. Two computation rules C
and Q can share constructors Θ, and the rules
Q can use all functions deﬁned in the other C.

•

Left-linear means that the left-hand side of every rule does not admit repeated same variables.

•

No left-linear or conﬂuence conditions.

•

Conﬂuent means that any divergent computation paths are joinable (i.e. deterministic in thesense of functional programming).

Our new theorem. All the previous researches
on modular termination in the theory of rewriting dealt with only ﬁrst-order rules. In this paper,
we show a novel modular termination theorem forsecond-order computation systems, which can involve λ-calculus of any order. It relaxes the above
restrictions in various directions. This is applicable

Moreover, this theorem ensures that the used termination checking methods for C and Q are notnecessary the same. Our theorem allows•

Heterogeneous termination checking, whichmeans that C is checked by some (very strong)termination checker, and C is checked by theGeneral Schema criterion (which is forced by
the theorem). This is practically eﬀective asshown in §3.
The problem on higher-order modular termina-

tion has untouched over 20 years. One reason ofthis is due to the proof of modularity is quite involved even in the ﬁrst-order case (Thm. 1.1),
hence a direct higher-order extension has been considered as hopeless.
Our approach. Our approach to prove Thm.
6.11 is novel and completely diﬀerent from the proof
method of the ﬁrst-order case. A key is the higherorder semantic labelling method developped by theauthor [9], which uses both the syntax and semantic structure of higher-order terms for termination
proof.
Organisation. The paper is organised as follows.
We ﬁrst examine a simple example of the use of
our theorem in §2. We implemented the modularity of termination in our tool SOL. We show in §3
the benchmark resuls of SOL in the internationaltermination competition held this year. SOL took
the highest score in the higher-order category. In§4 and §5, we introduce the framework and models
of second-order algebraic computation rules. In §6,
we show our modularity theorem.
In this paper, we mean termination for strong
normalisation (in short, SN, meaning that any
computation path is ﬁnite).

2 Example
As a simple illustration of the use of our theorem, we consider the following example of map andfilter functions.
listsig = [signature|nil : acons : a, List(a) -> List(a)|]mapsig = [signature|
map : (a -> List(b)), a -> List(b) |]mapsys = [rule|(map1) map(x.F[x],nil) => nil(map2) map(x.Z[x],cons(U,V))=> cons(Z[U],map(Z,V))|]filsig = [signature|filter : (a -> Bool), List(a) -> List(a) |]filsys = [rule|(fil1) filter(x.I[x],nil) => nil(fil2) filter(x.J[x],cons(X1,Y1))=> filter2(J[X1],x.J[x],X1,Y1)(fil3) filter2(true,x.G1[x],V1,W1)=> cons(V1,filter(G1,W1))(fil4) filter2(false,x.J1[x],X2,Y2)=> filter(x.J1[x],Y2)|]
mapfil = mapsys ++ filsys

We consider termination of mapfil, meaning thattermination of map, filter, filter2 and any com-bination of these.
Termination of map is immediate, because it isa structural recursive function. Actually, existing termination checker, such as Agda’s termination checker, can automatically prove terminationof map. But proving termination of filsys is diﬃcult. Agda cannot judge the termination of it.
There is a model theoretic method to prove termination by van de Pol [14]. It is by interpretingthe function symbols as monotone functionals overnatural numbers N. In the case of filsys, by using
the interpretation[[cons]](x, y) = 2 + y + 2x[[true]] = [[false]] = 3[[filter]](f, x) = x + f (0) + 2xf (x) + 2f (x) + 1[[filter2]](x, f, z, y)= 2x + 2y + 3z + f (0) + 2yf (y) + 3f (y) + 1
the rules are interpreted as strictly decreasing, thus
we conclude SN of filsys. This interpretation canbe found manually or by using a suitable SMT
solver.
What about the combined system mapfil? Notethat filsys and mapsys share the constructors
cons and nil, hence mapfil is “not the disjointsum” of two systems.
We prove termination of the computation system
mapfil by Thm. 6.11. Take C to be filsys withtuple rules and ΣC = filsig, Θ = listsig. Then
C is solid and is shown to be terminating by interpretation where the interpretation is the one used
before extended with [[h−, . . . , −i]](x1 , . . . , xn ) =x1 + . . . + xn + 1. Take ΣQ to be mapsig, and Q to
be mapsys. Then (ΣC ] ΣQ ] Θ, Q) is terminatingby the General Schema [1]. Thus, all the conditions in Thm. 6.11 are satisﬁed, hence the theorem
is applicable. We conclude that the mapfil using
the signature filsig++mapsig++listsig is terminating.

3 Benchmark
We have implemented the modular termination
checking method based on Thm. 6.11 in the system
SOL, second-order laboratory. SOL is a tool to checkconﬂuence and termination of second-order computation systems [10] [11]. The termination criterion
is based on the General Schema [1]. The system
SOL consists of about 7000 line Haskell codes, andworks on the interpreter of Glasgow Haskell Compiler (tested on GHCi, version 7.6.2). SOL uses thefeature of quasi-quotation (i.e. [signature|..]and [rule|..] are quasi-quotations) of TemplateResult
YES
NO
MAYBE
error
timeout

SOL
199
20
37
5
0

Wanda
151
14
28
66
2

SizeChange
93
0
163
3
2

Score

219

165

93

The table shows the number of judged results by each tool. The result YES/NO is a judged result of SN.
MAYBE is a result when the tool cannot judge. The score of a tool is the number of judged answers.
For full details, see http://group-mmm.org/termination/competitions/Y2018/and http://group-mmm.org/termination/competitions/Y2018/caches/termination 30047.html .
Figure1

Results and scores in Termination Competition 2018

Haskell [15] with a custom parser generated by Alex
(for lexer) and Happy (for paper), which realises
readable notation for signature, terms and rules.
It makes the language of our formal computation
rules available within a Haskell script.
SOL participated the Higher-Order Rewriting(union beta) category of the International Termination Competition 2018, aﬃliated with the Federated Logic Conference (FLOC 2018) in Oxford,
UK. The participated tools in the Higher-Order
Rewriting category are our SOL, Wanda [13] and
SizeChange [2]. SOL took the highest scoreamong three tools. The results are summarisedin the Fig. 1. Each tool tested 224 problems prepared for the competition, and tried to judge thetermination of each problem.
The modular checking method implemented in
SOL is one of the keys of this success. SOL callsa suitable external ﬁrst-order termination checkers
AProVE, NaTT, or TTT2 for a ﬁrst-order part ofa problem and uses the modularity. The external ﬁrst-order tools are powerful than other higherorder tools in many cases (for ﬁrst-order problems).
Hence it enhances the checking power of SOL.

quence A1 , · · · , An , and |A| for its length. The
notation s[u]p means replacing the position p of s
at with u, and s|p means selecting a subterm of
the position p. We use the abbreviations “lhs” and“rhs” to mean left-hand side and right-hand side,
respectively.
4. 1 Syntax
Types. We assume that A is a set of atomic types(e.g. Bool, Nat, etc.) We assume that the set ofmolecular types (or mol types for short) B isgenerated by atomic types, and type constructors
is the least set satisfying
B = A ∪ {T (a1 , . . . , an ) |a1 , . . . , an ∈ B, T is an n-ary type constructor}
By a type constructor T of arity n, we mean that it
takes n-mol types a1 , . . . , an and gives a mol type
T (a1 , . . . , an ). Note that we do not regard “→” asa type constructor (in our sense). We usually write
mol types as a, b, c, . . ..
Terms. A signature Σ is a set of function symbols of the formf : (a1 → b1 ), . . . , (am → bm ) → c

4 Second-Order Computation with Molecwhere all ai , bi , c are mol types (thus any function
ular Types
In this section, we introduce the framework of
second-order computation based on second-orderalgebraic theories [4], [5] with minor modiﬁcation
on types. We formulate computation rules of calculi for programming languages as second-order algebraic theories. It gives a formal framework toprovide syntax and computation.
Notation 4.1 We use the notation A for a se-

symbol is of up to second-order type).
Example 4.2 The simply typed λ-terms on basetypes Ty are modelled in our setting as follows.
Suppose that Arr is a type constructor. The set
B of all mol types is the least set satisfying B =Ty ∪ {Arr(a, b) | a, b ∈ B}, i.e. the set of all simple
types in our encoding. The λ-terms are given by a

y:b∈Γ
Θ . Γ ` y :b

(M : a1 , . . . , am → b) ∈ Θ
Θ . Γ ` ti : ai (1 ≤ i ≤ m)
Θ . Γ ` M [t1 , . . . , tm ] : b
Figure2(Rule)

f : (a1 → b1 ), · · · , (am → bm ) → c ∈ Σ
Θ . Γ, xi : ai ` ti : bi (1 ≤ i ≤ m)
Θ . Γ ` f ( xa1 1 .t1 , . . . xamm .tm ) : c

Typing rules of meta-terms(Θ . Γ ` ` ⇒ r : c) ∈ C
Θ . Γ ` ` ⇒C r : c

f : (a1 → b1 ), · · · , (ak → bk ) → c ∈ Σ
Θ . Γ, xi : ai ` ti ⇒C t0i : bi (some i s.t. 1 ≤ i ≤ k)(Fun)

Θ . Γ ` f (xa1 1 .t1 , . . . , xai i .ti . . . , xa1 1 .tk ) ⇒C f (xa1 1 .t1 , . . . , xai i .t0i . . . , xa1 1 .tk ) : c. Γ0 , xi : ai ` si : bi (1 ≤ i ≤ k)
M1 : (a1 → b1 ), . . . , Mk : (ak → bk ) . Γ ` t1 ⇒C t2 : c(Sub). Γ, Γ0 ` t1 [ M 7→ x.s ] ⇒C t2 [ M 7→ x.s ] : c
Figure3

Second-order computation (one-step)that when we instantiate M : a → b with a term
) s, free variables of s (which are of types a) are relama,b : (a → b) → Arr(a, b)
Σlam =| a, b ∈ Bplaced with (meta-)terms t1 , . . . , tn (cf. Def. 4.3).
appa,b : Arr(a, b), a → b
We may write x1 , . . . , xn . t for x1 . · · · .xn . t, and we
As this example, a signature is very often preassume ordinary α-equivalence for bound variables.
sented by function symbols parameterised by sevA second-order equational theory is a set of proved
eral molecular types. We often present a signatureequations deduced from a set of axioms.
simply schematically by
A metavariable context Θ is a sequence of()(metavariable:type)-pairs,
and a context Γ is a selam : (a → b) → Arr(a, b)
quence of (variable:mol type)-pairs. A judgment is
app : Arr(a, b), a → bof the form Θ . Γ ` t : b. A meta-term t is
to mean the signature Σlam . Moreover, simply writwell-typed by the typing rules Fig. 2. Note that a
ing function symbols lam and app, we mean lama,b
raw meta-term of the form x.t does not have a type.
and appa,b in Σlam having appropriate mol type
But we will use raw terms x.t in various places, such
subscripts a, b.
as in substitution below.
signature(

Note that Arr(a, b) is a mol type, but a function
type a → b is not a mol type. Hereafter, we use thethe above convention for a presentation of arbitrary
signature parameterised by mol types, also in SOL.
A sequence of types may be empty in the abovedeﬁnition. The empty sequence is denoted by (),which may be omitted, e.g., b1 , . . . , bm → c , or() → c. The latter case is simply denoted by c.
A metavariable is a variable of (at most) ﬁrstorder function type, declared as M : a → b (written as capital letters M, N, K, . . .). A variable ofa molecular type is merely called variable (written
usually x, y, . . ., or sometimes written xb when it isof type b). The raw syntax is given as follows.
- Terms have the formt ::= x | x.t | f (t1 , . . . , tn ).
- Meta-terms extend terms tot ::= x | x.t | f (t1 , . . . , tn ) | M [t1 , . . . , tn ].
The last form is called a meta-application, meaning

4. 2 Second-order computation
Given a meta-term t with free variables
x1 , . . . , xn , the notation t {x1 7→ s1 , . . . , xn 7→ sn }denotes ordinary capture avoiding substitution that
replaces the variables with terms s1 , . . . , sn .
Deﬁnition 4.3 (Substitution of terms formetavariables) Let Γ = y1 : b1 · · · , yk : b1 . Letini = |ai | and ai = a1i , . . . , an
i . Suppose (1 ≤ i ≤ k)nii
. Γ0 , x1i : a1i , . . . , xn
` si : bii : aiΘ, M1 : a1 → b1 , . . . , Mk : ak → bk . Γ ` e : c

Then substitution of terms for metavariables Θ .
Γ, Γ0 ` e [ M 7→ x.s ] : c is deﬁned as:x [ M 7→ x.s ] , x
Mi [t1 , . . . , tni ] [ M 7→ x.s ]i, si {x1i 7→ t1 [ M 7→ x.s ], . . . , xn
i 7→ tni [ M 7→ x.s ]}f (y1 .t1 , . . . , ym .tm ) [ M 7→ x.s ], f (y1 .t1 [ M 7→ x.s ], . . . , ym .tm [ M 7→ x.s ])where [ M 7→ x.s ] denotes a substitution formetavariables [M1 7→ x1 .s1 , . . . , Mk 7→ xk .sk ].
Computation rules. For meta-terms Θ . Γ `` : b and Θ . Γ ` r : b, a computation rule isof the form
Θ . Γ ``⇒r :bsatisfying: (i) ` is a deterministic second-order pattern . (ii) all metavariables in r appear in `. We
usually omit the context and type and simply write` ⇒ r.
We call a set C of rules a computation system.
We write s ⇒C t to be one-step computation using
C obtained by the inference system given in Fig.
3. We also regard ⇒C to be a binary relation on
meta-terms.

5 Mathematical Models of secondorder computation
5. 1 Models of meta-terms
We ﬁrst deﬁne the category Ctx of contexts.
The category Ctx has variable contexts {x1 :τ 1 , · · · , xn : τ n }, given by functions Γ : n → B
as objects, and arrows ρ : Γ → Γ0 , which are functions ρ : n → n0 such that Γ = Γ0 ◦ ρ, i.e. renaming
between Γ and Γ0 . The coproduct is Γ, Γ0 deﬁned
by [Γ, Γ0 ] : n+n0 → B. Since judgments are indexed
by contexts and types, the category is doubly indexed sets by Ctx for variable contexts, and B for
types.

A point of this modeling is that a function type,say a → b, is interpreted as a presheaf δ a Ab .
A Σ-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 homomorphismof Σ-algebras is a map ϕ : (A, α) → (B, β) suchthat ϕ ◦ α = β ◦ Σϕ.
A substitution is modeled by a multiplication ofa monoid in a “substitution” monoidal category.
Namely, the category (SetCtx )B forms a monoidal
category with the unit V and the “substitution”
monoidal product • given byaY(A • B)τ (∆) = (Aτ (Γ) ×Bτ i (∆))/ ∼
Γ∈Ctx

i∈m

where Γ = {xi : τ 1 , . . . , xm : τ m } and∼ is the equivalence relation generated by(t; uρ1 , . . . , uρm ) ∼ (A(ρ)(t); u1 , . . . , un ) for a renaming ρ : Γ → Γ0 in Ctx.
A Σ-monoid (A, α, ν, µ) consists of a monoid
A = (A, η : V → A, µ : A • A → A) in the monoidal
category ((SetCtx )B , •, V) with a Σ-algebra α :ΣA → A satisfying the compatibility condition [6].
- (A0 , α0 ) is
A morphism of Σ-monoids (A, α)Ctx Ba morphism in (Set ) which is both Σ-algebra
homomorphism and monoid morphism.
An important example is the Σ-monoid of all
meta-terms. Given a signature Σ and a metavariable context Θ, we deﬁne the indexed set of all
meta-terms by
MΣ Z τ (Γ) = {t | Θ . Γ ` t : b}.

Remark 5.1 The category Ctx corresponds toFiore and Hur’s F[T ] [4], and Staton’s Ctx0 [16].
The context extension δ τ : SetCtx → SetCtx by avariable of type τ is deﬁned by (δ τ A)(Γ) = A(Γ, τ ).
The presheaf V ∈ (SetCtx )B of variables is deﬁned by the Yoneda embedding Vτ = Ctx(hτ i, −),where hτ i : 1 → B maps 1 7→ τ ∈ B. HenceVτ (Γ) ∼= {x | x : τ ∈ Γ}, i.e. the set of variables ofa certain type τ taken from a context Γ.
We deﬁne the functor δ τ : SetCtx → SetCtx
for context extension by a variable of type τ by(δ τ A)(Γ) = A(Γ + τ ) for A ∈ SetCtx , which models
variable binding. We write δ τ for the compositionδ τ 1 ◦ · · · ◦ δ τ n . To a signature Σ, we associate thesignature functor Σ : (SetCtx )B → (SetCtx )B givenbyaY(ΣA)b =
δ ai Abi .
f :(a1 →b1 ),··· ,(an →bn )→b∈Σ 1≤i≤lwhich becomes MΣ Z ∈ (SetCtx )B . The presheaf
MΣ Z has a monoid structureν : V → MΣ Z;
ν(x) = xµ : MΣ Z • MΣ Z → MΣ Zµ(t; s1 , . . . , sn ) = t[x1 7→ s1 , . . . , xn 7→ sn ]for Θ . x1 : a1 , . . . , xn : an ` t : bwhich is nothing but an embedding ν of variables
into meta-terms, and a substitution µ for variables.
Theorem 5.2 [7] [4] The meta-terms with themonoid (MΣ Z, ν, µ) forms a free Σ-monoid. Moreover, when Z = 0, the presheaf MΣ Z 0 = TΣV of allterms forms an initial Σ-monoid.
A substitution θ = [M1 7→ x1 .s1 , . . . , Mk 7→
xk .sk ] for metavariables Θ = {M1 : a1 , . . . , Mn :- MΣ Zan } can be extended to a map θ : Θ
where Θ ∈ (SetCtx )B ( [4] §3) and its Σ-monoid- A gives amorphism extension θ] : MΣ Z

term substitution [ M 7→ x.s ]. We may simply
write the map for metavariable substitution as θ :Θ - MΣ Z.
This process of extension is generalised to anarbitrary Σ-monoid A as follows. A morphism- A of (SetCtx )B is called an assignϕ : Θment when its target has a Σ-monoid structure(A, α, η, µ). By freeness of MΣ Z, any assignmentϕ : Θ - A is uniquely extended to a Σ-monoid
morphism ϕ] : MΣ Z - A:
MΣ Z b (Γ)
xf (Θ1 .t1 , . . . , Θn .tn )Z[t1 , . . . , tn ]is clear that a weak model A satisﬁes any one-step
computation using C.
In short, in a weak model, every rule is interpreted as “weakly” smaller, meaning that someof rule may be interpreted as equal elements in amodel. Note that any (equational) algebraic model
is a weak model by taking the equality = to be thepreorder. Hence any computation system has atleast one weak model.

5. 3 Labelling rules by an weak model- Ab (Γ)
This section reviews and simpliﬁes the higher- η(Γ)(x)(x ∈ Γ)orderlabelling method [9] for termination to adapt- fA (Γ)(ϕ] (Γ+Θ1 )(t1 ), . . .)thepresent
setting of computation systems.
- µ(Γ)( ϕ(Γ)(Z); ϕ] (Γ)(t1 ), . . . ).

This gives a way to interpret meta-terms in a Σmonoid A. Hence we will write[[t]]ϕ]for ϕ (t). Note that substitution t θ is a specialcase, when A = MΣ Z.
5. 2 Algebraic models of second-ordercomputation rules
We give algebraic models of second-order computation rules. This section reviews [8] [9].
To model computation steps, we need an order
structure on a presheaf. Computation may be looping, hence we need preorders (i.e. reﬂexive andtransitive relations).
By a presheaf A ∈ (SetCtx )B is equipped with apreorder ≥, we mean that when ≥ is a family of
preorders {≥Ab (Γ) }Γ∈Ctx,b∈B , where ≥Ab (Γ) is on
Ab (Γ) and is compatible with presheaf action.
- B between
A map f : A1 × · · · × An
presheaves equipped with preorders in SetCtx
is weakly monotone if for all Γ, all a1 , b1 ∈A1 (Γ), . . . , an , bn ∈ Al (Γ) with ak ≥Ak (Γ) bk
for some k and aj = bj for all j 6= k,then f (Γ)(a1 , . . . , an ) ≥B(Γ) f (Γ)(b1 , . . . , bn ). A
weakly monotone Σ-monoid (A, ≥) is a Σ-monoid
equipped with preorders such that every operation f A is weakly monotone. The notions of strict
monotone and strict monotone Σ-monoid is deﬁned
similarly, replacing ≥ with its strict part of thetransitive relation >. Hereafter, we will omit subscripts.
Weak model.
A weak model (A, ≥) of C isa weakly monotone Σ-monoid in which for everyΘ . ` ⇒ r,[[`]]ϕ ≥ [[r]]ϕholds for every assignment ϕ : Θ → A. Then it

The main feature of semantic labelling is thattermination of the original computation system ispreserved by transforming it to a semantically labelled system. By labelling functions with semantic
elements of a weak model, it enrich the informationof computation rules without changing its essential
computation behavior.
Suppose that a given computation system C has aweak model (A, ≥), where ≥ is not necessary wellfounded. We choose for every f ∈ Σ a label set
L(f ), which is a set of labels attached to f . A label set must be non-empty and well-founded poset,
constructed from a (not necessary well-founded)weak model A. The labelled signature Σlab isΣlab = {fq | f ∈ Σ, q ∈ L(f )}.
which consists of function symbols with labels q in
the label set. A function symbol is labelled if L(f )contains more than one element. For unlabelled f ,the set L(f ) containing only one element can beleft implicit; in that case we write f instead of fp .
A label construction for a function symbolf : (a1 → b1 ), . . . , (an → bn ) → b is a weakly monotone morphism
hh−, . . . , −iif : δ a1 Ab1 × · · · × δ an Abn- L(f ),

where L(f ) is regarded as a constant presheaf returning the set L(f ). This constructs a label for ffrom semantic elements in Ab1 , . . . , Abn .
Then we deﬁne MΣlab Z to be the presheaf of
all meta-terms generated by the labelled signature- MΣlab Z withΣlab . The labelling labϕ : MΣ Z
A is a function deﬁned
an assignment ϕ : Θbylabϕ (x) = x
labϕ (M[t1 , . . . , tn ]) = M[labϕ (t1 ), . . . , labϕ (tn )]labϕ (f (x1 .t1 , . . . , xn .tn ))= fhh[[t1 ]]ϕ,...,[[tn ]]ϕiif (x1 .labϕ (t1 ), . . . , xn .labϕ (tn ))where every semantic element [[si ]]ϕ is calculated
by forgetting the labels in si , and the label for f isconstructed by the label construction hh−, . . . , −iifusing a weak model A.

deﬁne f .d g ∈ Fun(r).

Proposition 5.3 (MΣlab Z, [fϕ ]f ∈Σ , ν ϕ , β ϕ ) is a Σmonoid.

Used(x) = ∅[Used(f (x.t)) = {g | Fun(ti ) 3 h .d g}

Proof. The unit is ν ϕ : V → MΣlab Z deﬁned by
x 7→ x, and for f : (a1 → b1 ), . . . , (an → bn ) → b ∈Σ, the operation
fϕ : δ a1 MΣlab Z b1 × · · · × δ an MΣlab Z bn - MΣlab Z b
fϕ (s1 , . . . , sn ) = fhh[[s1 ]]ϕ ...,[[sn ]]ϕiif (s1 , . . . , sn ).
and the multiplication is.
¤
The labelling labϕ is a Σ-monoid morphismfrom the initial Σ-monoid MΣ Z to the Σ-monoid(MΣlab Z, [fϕ ]f ∈Σ , ν ϕ , β ϕ ). We deﬁne the labelledrules by
C lab , {labϕ (l) → labϕ (r) | Θ . l → r ∈ C,
term-generated assignment ϕ : Θ - A}.
Theorem 5.4 ( [9]) Suppose a computation system C has a weak model A. Construct a labeled system C lab by A by choosing a label construction. If
C lab follows the General Schema, then C is strongly
normalising.
Proof. The structure of the proof is much the sameas in [9]. The notion of so-called decreasing rules is
not necessary in the present form because the General Schema’s condition on function symbols automatically satisﬁes the decreasing rules. Computation for C lab uses the multiplication β ϕ , and theproofs of [1] is redone with β ϕ instead of normal
substitution for variables.
¤

6 Proving Modularity Theorem
Throughout this section, we use the following notational convention. For a presheaf A ∈ (SetCtx )B ,we denote by u ∈ A if there exists suitable τ and Γsuch that u ∈ Aτ (Γ).
Let SN to be the set of all strongly terminating terms. We deﬁne the presheaf of minimal nonterminating terms as follows:
TΣ∞Vτ (Γ) , {u | SN 63 u B ∀t ∈ SN}.
A minimal non-terminating term is a nonterminating term whose subterms are SN [12].
Deﬁnition 6.1 The function dependency relation.d is deﬁned as follows: for a rule f (t) → r, we

Deﬁnition 6.2 Given a meta-term or computation system Q, we deﬁne the set Used(Q) of usedfunction symbols w.r.t. labelling L byi[if f is labelled w.r.t L
Used(ti ) if f is unlabelled w.r.t L
Used(f (x.t)) =i[
Used(M [t]) =Used(ti )i[Used(C) =Used(l) ∪ Used(r)l⇒r∈CDeﬁnition 6.3 The library rules of a given computation system C with respect to labelling L is theset of all rules which are used in some other rules,deﬁned by
Lib(C) , {f (x.t) ⇒ r ∈ C | f ∈ Used(C)}.
Given A ∈ (SetCtx )B , A> is A extended withthe undeﬁned element >, deﬁned by A> (Γ)τ =A(Γ)τ ∪ {>}.
Deﬁnition 6.4 A weakly monotone Σ-monoid(A> , ≥) is called Σt-monoid if
X ∈ (SetCtx )B ∧ (∀τ , Γ. ﬁnite
G set X(Γ)τ ⊆ A(Γ)τ
⇒
X(Γ)τ ∈ A(Γ)τ )A Σt-monoid morphism is a Σ-monoid morphismF
between Σt-monoids that preserves .
Deﬁnition 6.5 A weak t-model (A> , ≥) of C
w.r.t. labelling L is a Σt-monoid w.r.t. L in which
for every Θ . ` ⇒ r : τ ∈ Lib(C),ϕ] (`) ≥ ϕ] (r)holds for every assignment ϕ : Θ → A> .
F
We denote by X the least upper bound of a set
X. For an inﬁnite set X or there is no least upperFbound, we suppose X , >.
Deﬁnition 6.6 Let C be a computation system,(A> , η, µ) a weak t-model of C, ϕ : Z → A an

thatassignment. We deﬁne a morphism

- A>
b (Γ)
- η(Γ)(x)(x ∈ Γ)- fA (Γ)(ϕ∗ (Γ,x1 )(t1 ), . . .)∗ϕ : MΣ Z b (Γ)
xf (x.t)if f ∈GUsed(C){ϕ∗ (u) | f (x.t) ⇒+C u}
if f 6∈ Used(C)- µΓ ( ϕ(Γ)(Z); ϕ∗ (Γ)(t1 ), . . . ).

f (x.t)Z[t]Note that ϕ∗ is not homomorphic, hence not a
Σ-monoid morphism. The labelling lab∗ϕ is deﬁned
using ϕ∗ .

rθ D (rθ)|p ∈ TΣ∞V.

¤

Proposition 6.9 If
SN ∪ TΣ∞V 3 s ⇒C t ∈ SN ∪ TΣ∞Vthenlab∗ϕ (s) ⇒+lab∗ϕ (t).
C lab ∪Decl

Let Decl>L be the decreasing rules associated to>L [9].

Theorem 6.10 Let C be a computation system,
Deﬁnition 6.7 The labelling lab∗ϕ : MΣ Z - MΣlab Z (A> , >) be a well-founded t-weak model of C with
with an assignment ϕ : Θ - A is a function delabelling (L, ≥L ). If C lab ∪ Decl>L is SN, then C is
ﬁned bySN.
lab∗ϕ (x) = x
lab∗ϕ (M[t1 , . . . , tn ]) = M[lab∗ϕ (t1 ), . . . , lab∗ϕ (tn )]lab∗ϕ (f (x1 .t1 , . . . , xn .tn ))= fhhϕ∗ (t1 ),...,ϕ∗ (tn )iif (x1 .lab∗ϕ (t1 ), . . . , xn .lab∗ϕ (tn ))∗We deﬁne MΣlab Z to be the presheaf of all metaterms labelled by lab∗ϕ .

Lemma 6.8 Let C be a computation system. For
every u ∈ TΣ∞Vτ (Γ), there exist•••

a rule Z . l ⇒ r : τ ∈ C
an assignment θ : Z → TΣVa position p of rθ

such that the following rewrite sequence is possible:>εTΣ∞V 3 u ⇒∗ C lθ ⇒C rθ D (rθ)|p ∈ TΣ∞VεProof. Let u ∈ TΣ∞Vτ and Q an inﬁnite rewrite
sequenceu = u0 ⇒C u1 ⇒C · · ·Since all proper subterms of u are SN, Q must contain a root rewrite step. Suppose the ﬁrst root step
appear as (1) in(2)u ⇒∗ C lθ ⇒C rθ
(1)

where f (x1 .l1 , . . . , xn .ln ) = l. Since (2) is below
the root step rewrite, it must be
u = f (x1 .t1 , . . . , xn .tn ) ⇒∗C f (x1 .l1 , . . . , xn .ln )θ
and for each i, (and each ti of type τ i )SN 3 ti ∧xi ` ti ⇒∗C li θ : τ i∧ li θ ∈ SN

by the assumption that all proper subterms of u are
SN. Since li is a deterministic second-order pattern,
we see θ(M ) ∈ SN for every metavariable M in l.
Since rθ is not SN and θ is SN, there exists p such

Proof.
The contrapositive is proved by using
Lemma 6.8 and Prop. 6.9.
¤
We say that a computation system has tuples andprojection rules if for each type τ ∈ T and n ∈ N,nthere are function symbols h−, . . . , −in
→ τ
τ : τ
n
and rules hX1 , . . . , Xn iτ ⇒ Xi for i = 1, . . . , n.
A term is solid [9] if for each meta-application
M [t1 , . . . , tn ], every ti does not contain function
symbols. A computation system C is solid if (i)all types are strictly positive and the type order iswell-founded, and for each rule l ⇒ r ∈ C, (ii) all
metavariables in r are accessible in l, and (iii) r issolid.
Theorem 6.11 Let (ΣC ] Θ, C) and (ΣC ] ΣQ ]Θ, Q) be computation systems such that(i) ΣC is the deﬁned function symbols of C,(ii) ΣQ is the deﬁned function symbols of Q,(iii) Θ is the signature for constructors,(iv) ΣC ∩ ΣQ = ∅ and C is solid,(v) (ΣC ] Θ, C) extended with tuples and projection
rules is terminating,(vi) (ΣC ] ΣQ ] Θ, Q) is terminating by the General
Schema,(vii) >T is well-founded, every constructor is positive, and >ΣC ]ΣQ ]Θ is well-founded,
Then (ΣC ] ΣQ ] Θ, C ] Q) is terminating.
Proof sketch. Let Σ be ΣC ] Θ. Take a weakly
monotone Σ-monoid (TΣV, ⇒∗C ). Then (TΣV, ⇒∗C )is a well-founded weak Σt-model because••

projection rules gives the least upper boundsby ⇒∗C
Lib(C) ⊆ C ⊆ ⇒∗C with projection rules is

SN.
We label all function symbols f ∈ ΣC , i.e., deﬁne alabelling L by[
hhtiif , f (t); Lf ,TΣV(Γ)τ ; ≥L , ( ⇒C ∪D)∗
τ ,ΓThen hh−iif : (TΣV, ⇒∗C ) → (Lf , ≥L ) is weakly
monotone. We have C lab and we can show SN of
C lab ∪ Q ∪ Decl≥L by the General Schema. By Thm.
6.10, we obtain the result.
¤
Acknowledgments. I am grateful to TatsuyaAbe, Kazuhiko Sakaguchi, Yuito Murase, andKentaro Kikuchi for various discussions and related
development of SOL system for the internationaltermination and conﬂuence competitions in 2017and 2018.
参 考 文 献[ 1 ] F. Blanqui. Termination and conﬂuence of
higher-order rewrite systems. In Rewriting Techniques and Application (RTA 2000), LNCS 1833,
pages 47–61. Springer, 2000.
[ 2 ] F. Blanqui and G. Genestier. Termination of
λπ modulo rewriting using the size-change principle. In Proc. 16th International Workshop on Termination, WST 2018, pages 10–14, 2018.
[ 3 ] K. Drosten. Termersetzungssysteme. InformatikFachberichte 210. Springer, 1989. in German.
[ 4 ] M. Fiore and C.-K. Hur. Second-order equational logic. In Proc. of CSL’10, LNCS 6247, pages
320–335, 2010.
[ 5 ] M. Fiore and O. Mahmoud. Second-order algebraic theories. In Proc. of MFCS’10, LNCS 6281,
pages 368–380, 2010.
[ 6 ] M. Fiore, G. Plotkin, and D. Turi. Abstract syntax and variable binding. In Proc. of LICS’99, pages
193–202, 1999.
[ 7 ] M. Hamana. Free Σ-monoids: A higher-ordersyntax with metavariables. In Proc. of APLAS’04,
LNCS 3302, pages 348–363, 2004.
[ 8 ] M. Hamana. Universal algebra for termination ofhigher-order rewriting. In Proc. of RTA’05, LNCS
3467, pages 135–149, 2005.
[ 9 ] M. Hamana. Higher-order semantic labelling for
inductive datatype systems. In Proc. of PPDP’07,
pages 97–108. ACM Press, 2007.
[10] M. Hamana. How to prove your calculus is decidable: Practical applications of second-order algebraic theories and computation. Proceedings of
the ACM on Programming Languages, 1(22):1–28,
September 2017.
[11] M. Hamana. Polymorphic rewrite rules: Conﬂuence, type inference, and instance validation. In
Proc. of 14th International Symposium on Functional and Logic Programming (FLOPS’18), LNCS
10818, pages 99–115, 2018.
[12] N. Hirokawa and A. Middeldorp. Predictive labeling. In Proc. RTA’06, LNCS 4098, pages 313–
327, 2006.
[13] C. Kop. Higher Order Termination. PhD thesis,
Vrije Universiteit, Amsterdam, 2012.
[14] J. van de Pol. Termination proofs for higherorder rewrite systems. In the First International
Workshop on Higher-Order Algebra, Logic andTerm Rewriting (HOA’93), LNCS 816, pages 305–
325, 1994.
[15] T. Sheard and S. Peyton Jones. Template
metaprogramming for Haskell. In Proc. Haskell
Workshop 2002, 2002.
[16] S. Staton. Instances of computational eﬀects:
An algebraic perspective. In Proc. of LICS’13, page519, 2013.
[17] Y. Toyama. Counterexamples to termination forthe direct sum of term rewriting systems. Inf. Process. Lett., 25(3):141–143, 1987.
[18] Y. Toyama, J. W. Klop, and H. P. Barendregt. Termination for direct sums of left-linear
complete term rewriting systems. Journal of theACM, 42(6):1275–1304, 1995.