Semantic Labellingfor
Proving TerminationofCombinatory Reduction Systems
Makoto Hamana
Department of Computer Science,
Gunma University, Japan

WFLP’09
June, 2009.
1

Intro: Termination Proof by RPO
Term Rewriting System (TRS) R:
f act(0) → s(0)f act(s(x)) → f act(x) ∗ s(x)Recursive path ordering (RPO) [Dershowitz TCS’82]
proves termination (= SN)2

Intro: Termination Proof by RPO
Term Rewriting System (TRS) R:
f act(0) → s(0)f act(s(x)) → f act(x) ∗ s(x)Proof method:
1. Give a precedence:f act > ∗ > s > 0
Thm. RPO >RPO well-founded & closed under subst., contexts
2. Check for each l → r ∈ R, l >RPO r(i.e.
→ ⊆ >RPO )Then: →R ⊆ >RPO
Hence R is SN.
3

Intro: Semantic Labelling for TRSs [Zantema’95]
Original TRS R:
f act(s(x)) → f act(p(s(x))) ∗ s(x)p(s(0)) → 0p(s(s(x))) → s(p(s(x)))
I RPO doesn’t work
Semantics: Σ-algebra (N, {f actN , sN , pN : N → N, · · ·})Labelled TRS R:
f acti+1 (s(x)) → f acti (p(s(x))) ∗ s(x)p(s(0)) → 0p(s(s(x))) → s(p(s(x)))
f acti+1 > f acti
I RPO works!
Th. [Zantema’95] TRS R is terminating
4⇒

R is terminating.

This Work
B Extends semantic labelling to CRSs
B Klop’s format of higher-order rewriting:
Combinatory Reduction System (CRS) [Klop’80]- Second-order rewriting systems- TRS + variable binding, metavariables, meta-terms

5

Example of CRS: Quick Sort
if(true, x, y)→xif(false, x, y) → yfilter(p, nil) → nil

nil ++xs→ xs(x : xs) ++ys → x : (xs ++ys)

filter(p, x : xs) → if(p[x], x : filter(p, xs), filter(p, xs))
qsort(nil) → nil
qsort(x : xs) → qsort(filter(a. a ≤ x, xs)) ++((x : nil) ++qsort(filter(a. a > x, xs))6

This Work
B Difficulty: what is a suitable semantic structure for labelling CRSs?
B Contribution:
1. Answer
2. Second-order version of semantics labelling
3. Applications to functional programs – so useful
B How to tackle?
- TRSs∗ syntactic proof method: RPO∗ semantics: universal algebra- CRSs
∗ syntactic proof method: the General Schema∗ semantics: ?
7

Termination Proof by the General Schema
The General Schema[Blanqui,Jouannaud,Okada TCS’02, Blanqui RTA’00]
can be used as a higher-order version of RPO method
R higher-order rewrite rules (map, filter, etc.)
Proof method:
1. Give a precedence > on fun. symbols.
2. Check for each l → r ∈ R,
r is in the computable closure (wrt. >) of l(the “General Schema”).
Then R is SN.

8Semantics Labelling for CRS: Theory
CRS’s rewrite:s →R t

Semantic labels must be consistent with:
B functional contexts
g[[s]] ( s ) →R g[[t]] ( t )B binders
λ[[s]]x (x. s ) →R λ[[t]]x (x. t )B function applications
map(x.F (x), cons(M, N )) →R cons(F (M ), · · ·)⇓· · · →R cons[[F ]][[M ]] (F (M ), · · ·)B Σ-monoids [Fiore,Plotkin,Turi LICS’99]
with order structure [Hamana RTA’05]
9

Semantics Labelling for CRS: Theory
B Signatures Σ,Σ(labelled)

B Interpretation by a Σ-monoid (M , ≥)meta-terms MΣ Zhomomorphism φquasi-modell→r∈R?

?

M

φ(l) ≥ φ(r)CRS

B Labellingmeta-terms

MΣ Zlabelling mapφLlabelled meta-terms

?

MΣ Z

l→r∈RCRS?
LL

φ (l) → φ (r) ∈ R

10labelled CRS

Semantics Labelling for CRS: Theory
B Propositionterms

MΣ 0labelling map φLlabelled terms?

MΣ 0s →R t?
L∗L

φ (s) →Decr· →R φ (t)[Proof]- MΣ 0 forms a Σ-monoid- commutativity of labelling map φL with meta and object
substitution operations
B Thm. [Semantic labelling for CRS]
CRS R ∪ Decr is terminating ⇒ R is terminating.
B “Decreasing rules” Decr, for all f ∈ Σ, labels p > q,fp (z1 , . . . , zl ) → fq (z1 , . . . , zl )11

Termination Proof by Semantic Labelling for CRS
CRS R given
Proof method
1. Give a quasi-model for R: Σ-monoid (M, ≥)2. Generate labelled CRS R by attaching semantic labels (wrt M) tochosen fun. symbols
3. Give a precedence on semantically-labelled fun. symbols in R
4. Check that R ∪ Decr satisfies the General Schema
Then R is SN.

12

Example: Quick Sort
if(true, x, y)→xif(false, x, y) → y
filter(p, nil) → nil

nil ++xs→ xs(x : xs) ++ys → x : (xs ++ys)

filter(p, x : xs) → if(p[x], x : filter(p, xs), filter(p, xs))
qsort(nil) → nil
qsort(x : xs) → qsort(filter(a. a ≤ x, xs)) ++((x : nil) ++qsort(filter(a. a > x, xs))

The General Schema doesn’t satisfy R.
Problem:x : xs ≺ arguments of recursive calls in the red parts(i.e. structurally bigger).
13

Example: Quick Sort
Semantics D = N × N∗ with the orderdef0 00hn, li ≥ hn , l i ⇐⇒ n ≥ nCarrier Mk , (D k → D)
trueM0 = h1, i
0M0 = h0, iqsortM0 (hn, li) = hn, ifalseM0 = h0, isM0 (hn, li) = hn + 1, li
yif b = h1, iifM0 (b, y, z) =zif b = h0, i h0, i otherwise

filterM0 (p, hn, li) = hthe number of p(hi, i) = h1, i for i in l, i0000++M0 (hn, li, hn , l i) = hn + n , l · l i
nilM0 = h0, i:M0 (ha, si, hn, li) = hn + 1, a · li

This gives a quasi-model for R.
14

Example: Quick Sort
Take semantic labels as the lengths n from hn, li.
We have the labelled rules R:
qsort0 (nil) → nil
qsorti+1 (x : xs) → qsortj (filter(a.a ≤ x, xs)) ++((x : nil) ++qsortk (filter(a.a > x, xs)))

qsorti (xs) → qsortj (xs)where i + 1 > j, k

for all i > j ∈ N

With the precedence (for i > j)qsorti > qsortj > filter > if, ++, “>”, “≤” > nil, :, 0, S, true, false
R satisfies the General Schema, hence R is SN.

15

Summary
B Semantic labelling for CRS enhances the power of existing proof
methods (the General Schema) for termination of CRS
B Semantic labelling for CRS is established uniformly in theframework of Σ-monoids
B Useful to prove termination of higher-order functional programs
Related WorkHamana, Higher-Order Semantic Labelling for Inductive DatatypeSystems, PPDP’07.
Roux and Blanqui, On the relation between size-based terminationand semantic labelling, CSL’09.

16

Summary
B Semantic labelling for CRS enhances the power of existing proof
methods (the General Schema) of termination of CRS
B Semantic labelling for CRS is established uniformly in theframework of Σ-monoids
B Useful to prove termination of higher-order functional programs
Future Work
Practical termination checkerfor proof assistances + functional programming (e.g. Agda, Coq)
by formalizing semantics and then using semantic labelling17