Universal Algebra for
Termination of Higher-Order Rewriting

Makoto Hamana
Department of Computer Science,
Gunma University, Japan

RTA’052005, April1

Intro: First-Order Term Rewriting System (TRS)B Terms TΣ X 3 t ::= x | f (t1 , . . . , tm )B Rewrite rules R = {t1 → t2 , . . .}B Rewrite relation →R
B An important problem: termination of R2

Intro: Complete Algebraic Characterisation of TRSs
Theorem [Lankford’79, Zantema’94]
A TRS R is terminating if and only ifthere exists a well-founded monotone (Σ, R)-algebra.
(“ordered” Σ-algebra (A; >A ) that validates all rules in

I. Useful: Finding a well-founded (Σ, R)-algebra implies termination of R
II. Fundamental: Sound and complete semantics of TRS
III. Applications: Semantic labeling, monadic modularity, etc.

Q. Does a similar theorem hold forhigher-order∗ rewriting?
∗Rewriting on terms with variable binding and (meta-level) substitutions

3R)

Contents
Algebraic semantics for
I. CRS rewriting
II. CRS meta-rewriting
III. Binding CRSs

4

Combinatory Reduction System (CRS) [Klop’80]
Example: conversion into prenex normal formP ∧ ∀(x.Q[x])→ ∀(x.P ∧ Q[x])¬∀(x.Q[x]) → ∃(x.¬(Q[x]))∀(x.Q[x]) ∧ P → ∀(x.P ∧ Q[x])¬∃(x.Q[x]) → ∀(x.¬(Q[x]))Definition
Variables

x, y, z, · · ·Metavariables

Zl (arity l), · · ·Function symbols

F l (arity l), · · · ∈ ΣTerms

s ::= x | x.s | F l (s1 , . . . , sl )Meta-terms

t ::= x | x.t | F l (t1 , . . . , tl ) | Zl [t1 , . . . , tl ]CRS rules Rt1 → t2

(with some syntactic conditions)

CRS rewriting →Rl→r∈Rs →R t

s →R tθ(l) →R θ(r)x.s →R x.t

F (. . . , s, . . .) →R F (. . . , t, . . .)A valuation θ is a mapping from metavariables to terms.
5Technical Framework
Algebras in the functor category SetF
(first-order case: algebras are in Set)

F · · · the category of natural numbers and all functions
A presheaf X ∈ SetF is an N-indexed set with arrow part.
Definition [Fiore,Plotkin,Turi]

Σ · · · the functor Σ : SetF → SetF given by a binding signatureA Σ-monoid consists ofB a monoid object A in the monoidal category (SetF , •, V) withB a Σ-algebra α : ΣA → A
such that “the monoid multiplication and α commutes”.

6Technical Framework
Algebras in the functor category SetF
(first-order case: algebras are in Set)

F · · · the category of natural numbers and all functions
A presheaf X ∈ SetF is an N-indexed set with arrow part.
Definition [Fiore,Plotkin,Turi]

Σ · · · the functor Σ : SetF → SetF given by a binding signatureA Σ-monoid consists ofB a monoid object = modelling substitutions
B a Σ-algebra = modelling Σ-terms
such that “substitution on Σ-term” is defined.

6Structural Terms
Observation
Syntax given by the free Σ-monoid MΣ Ẑ over Ẑ [Hamana APLAS’04]

MΣ Ẑ(n) 3 t ::= x | F l (n+1, . . . , n+i.t1 , . . . , n+1, . . . , n+l.tl ) | Zl [t1 , . . . , tl ]I Similarity to CRS Meta-terms
t ::= x | x.t | F l (t1 , . . . , tl ) | Zl [t1 , . . . , tl ]Binding signature Σ

F : hn1 , . . . , nl i ∈ Σ(1 ≤ i ≤ l)
F has l arguments and binds ni variables in the i-th argument.
I Define Structural meta-terms bymeta-terms built from a binding signature.
I Then, structural meta-terms forms a free Σ-monoid.
I Structural meta-terms have a good structural induction principle(due to the initial algebra property).
7

Algebraic Semantics of CRS Syntax
By [Fiore,Plotkin,Turi’99] [Hamana’04],Thm. Structural CRS terms TΣV forms an initial V+Σ-algebra.
Thm. Structural CRS meta-terms MΣ Z forms a free Σ-monoid over Ẑ .
Assumption: Use the method of de Bruijn levels for (meta-)terms
I CRS’s variables are 1, 2, 3, · · · ∈ N.
Presheaves: Use structural (mata-)term sets parameterisedby the set of free variables n = {1, . . . , n}.
DefineV(n) , {1, . . . , n} = n“vars from 1 to n”

TΣV(n) , {t | term t has n-free vars}
MΣ Z(n) , {t | meta-term t has n-free vars}
Z(l) , {Z | metavariable Z has arity l}Then, V, Ẑ, TΣV, MΣ Z ∈ SetF .
8

Structural CRSs
Definition
A Structural CRS is a CRS built from structural meta-terms.
Similarly for other syntactic objects: valuation, rewrite relation.
Assumption:
Hereafter, we only consider structural CRSs.
We just say “a CRS” for a structural CRS.

9Algebraic Semantics of CRS rewriting
Example: Z = {M1 , N0 }CRS for untyped λ-calculus

app(lam(1.M), N) → M[N]RuleB Valuation θ : Zl→r∈Rθ(l) →R θ(r)- TΣV into terms.

M

1- t ∈ TΣV(1)“t has at most 1-free var”

0- s ∈ TΣV(0)“s has no free vars”

NI A valuation is characterised as a morphism of SetF .
B How to interpret rewrite rules?
case for TRS:

ηX- TΣ (X)X..
..
@.. φ∗@..
φ R..?
@
Σ-algebra A

10l→r∈R?

φ∗ (l) >A φ∗ (r)Algebraic Semantics of CRS rewriting
Example: Z = {M1 , N0 }CRS for untyped λ-calculusapp(lam(1.M), N) → M[N]RuleB Valuation θ : Zl→r∈Rθ(l) →R θ(r)- TΣV into terms.

M

1- t ∈ TΣV(1)“t has at most 1-free var”

0- s ∈ TΣV(0)“s has no free vars”

NI A valuation is characterised as a morphism of SetF .
B How to interpret rewrite rules?
case for CRS:ZηZ- MΣ Z..
..
@.. φ∗@..
φ R..?
@
Σ-monoid A

10l→r∈R?
φ∗ (l) >A φ∗ (l)Algebraic semantics of CRS rewritingηZZ- MΣ Z

Z|n ` l → r ∈ Rθ∗?
TΣVunique Σ-monoid mor.

@@θ R@Σ-monoidµ=initial¶θ ∗n (l) →R θ ∗n (r)!A unique V+Σ-algebra hom.
V +Σ-algebra?
V+Σ-algebra A!A θ ∗n (l) >A(n) !A θ ∗n (l)s →+R t?
!A(n) (s) >A(n) !A(n) (t)I (V+Σ, R)-algebra
Theorem For any (V+Σ, R)-algebra A, there exists a unique monotone- (A, >A ).
homomorphism (TΣV, →+R)

11

Algebraic semantics of CRS rewriting
Main Theorem 1 (Complete characterisation of termination)
A CRS R is terminating if and only if there exists a well-founded(V+Σ, R)-algebra.

12Meta-rewriting
More direct interpretation is possible.

I Rewriting on Meta-terms=Meta-rewriting

CRS (R, Z)~n.l → ~n.r ∈ Rn ` θ ∗ (n)(l) ÃR θ ∗ (n)(l)n+i ` s ÃR tn ` F (. . . , n+~i.s, . . .) ÃR F (. . . , n+~i.t, . . .)Z ∈ Z(l)n ` s ÃR tn ` Z[. . . , s, . . .] ÃR Z[. . . , t, . . .]
θ is a mapping Z- MΣ X to meta-terms

13Algebraic Semantics of Meta-rewriting
Theorem ∀ A: (Σ, R)-monoidηZ- MΣ ZZn ` s Ã+R t..
..
@.. φ∗ ∃! monotone Σ-monoid mor.
admissible
@..
φ R
@ ..?
Aφ(n)∗ (s) >A(n) φ(n)∗ (t)Main Theorem 2 (Complete characterisation of meta-termination)
A CRS (R, Z) is meta-terminating if and only ifthere exists a well-founded (Σ, R)-monoid.

14

Binding CRSs
(Essentially) meta-application free fragment

B Simpler interpretation not using monoid structure
B Example:P ∧ ∀(x.Q[x])→ ∀(x.P ∧ Q[x])¬∀(x.Q[x])→ ∃(x.¬(Q[x]))∀(x.Q[x]) ∧ P→ ∀(x.P ∧ Q[x])¬∃(x.Q[x])→ ∀(x.¬(Q[x]))B Crucial fact: for the presheaves Z :metavariables, V :vars,
V is the unit of the monoidal category (SetF , •, V).

15

Binding CRSs
(Essentially) meta-application free fragment

B Simpler interpretation not using monoid structure
B Example:P ∧ ∀(x.Q[x])→ ∀(x.P ∧ Q[x])¬∀(x.Q[x])→ ∃(x.¬(Q[x]))∀(x.Q[x]) ∧ P→ ∀(x.P ∧ Q[x])¬∃(x.Q[x])→ ∀(x.¬(Q[x]))B Crucial fact: for the presheaves Z :metavariables, V :vars,Z•V ∼e.g. Z • V(1) 3 Q[x] = Q ∈ Z(1)=Zdef

B Binding CRSs ⇐⇒ CRSs consisting of binding meta-terms(Z, V and Σ-terms)
t ::= x | F (x1 · · · xi1.t1 , . . . , x1 · · · xil.tl ) | Zl(= Zl [1, . . . , l])

B Consider Z +V+Σ-algebras
Binding meta-terms = the initial Z +V+Σ-algebra

15

Algebraic Semantics of Binding CRSs
B Redo everything for binding CRSs. We again obtain:
B Proposition
A binding CRS (R, Z) is meta-terminating on all binding meta-terms
if and only if there exists a well-founded (Z +V+Σ, R)-algebra.

B This gives a simpler interpretation method of showing
termination of binding CRSs:
because {binding meta-terms} ⊇ {terms}.

16

Binding CRSs – Termination ProofExampleP ∧ ∀(x.Q[x])→ ∀(x.P ∧ Q[x])¬∀(x.Q[x]) → ∃(x.¬(Q[x]))∀(x.Q[x]) ∧ P → ∀(x.P ∧ Q[x])¬∃(x.Q[x]) → ∀(x.¬(Q[x]))Z +V+Σ-algebra K :Carrier: K(n) = N with the usual orderOperations:∧K(n) (x, y) = ∨K(n) (x, y) = 2x + 2y
¬K(n) (x) = 2x
Z +V+Σ-algebra K satisfies R.

∀K(n) (x) = ∃K(n) (x) = x + 1i.e. (Z +V+Σ, R)-algebra.

Hence R is terminating on all CRS terms.

I Simpler than existing proof methods of termination of higher-order rewriting[van de Pol’96].

17

SummaryI. Universal Algebra for CRSs = Σ-monoids
II. Complete characterisations oftermination and meta-termination of CRSs
III. Universal Algebra for binding CRSs = Z +V+Σ-algebras
I Simpler interpretation for termination proof

Thank you.

18