1Algebraic Semantics ofHigher-Order Abstract Syntax andSecond-Order Rewriting

Makoto Hamana
Department of Computer Science,
Gunma University, Japan

International School on Rewriting (ISR 2015),
August 10-14, 2015, Leipzig, Germany

2This Lecture
I. Higher-Order Abstract Syntax
1. What is HOAS
2. Algebraic semantics
3. AIM: Meta-terms form a free Σ-monoid
II. Second-Order Rewrite System
1. Deﬁnition of CRS
2. Algebraic interpretation
3. AIM: CRS rewriting forms a monotone (Σ, R)-algebra
4. Termination by interpretation

3

II. Algebraic Semantics ofSecond-Order Rewrite System4Algebraic Semantics of Second-Order Rewrite System
B Deﬁnition of CRS
B Monotone Σ-algebra in SetF
B Main Theorem
A CRS R is terminating(V+Σ, R)-algebra.
B Examples

iﬀ there is a well-founded5

TRS: Review
Term Rewriting System (TRS) R:
f act(0) → S(0)f act(S(x)) → f act(x) ∗ S(x)Terms are deﬁned byTΣ (X) 3t ::= x | f (t1 , . . . , tm )The rewrite relation→R⊆TΣ (X) × TΣ (X)is deﬁned byl→r∈Rlθ →R rθ

s →R tf (. . . , s, . . .) →R f (. . . , t, . . .)where θ is a substitution θ : X → TΣ (X)6

Combinatory Reduction System (CRS) [Klop’80]
Eg. A transformation to prenex normal formsp∧∀(x.q[x]) → ∀(x.p∧q[x])¬∀(x.q[x]) → ∃(x.¬(q[x]))∀(x.q[x])∧p → ∀(x.q[x]∧p)¬∃(x.q[x]) → ∀(x.¬(q[x]))Def.
Variables

x, y, z, · · ·Meta-variables

z(l) (arity l), · · · ∈ Z

Function symbols
Meta-terms

f (l) (arity l), · · · ∈ Σ−−t ::= x | f (l) (→x .s , . . . , →x s ) | z(l) [t , . . . , t ]Rewrite rules R

t1 → t2

Rewrite relation→R on terms TΣV

1l→r∈Rθ ] (l) →R θ ] (r)

1l l

1

(with some syntactic conditions)s →R t−−f (. . . , →x .s, . . .) →R f (. . . , →x .t, . . .)Valuation θ : Z → TΣV maps a metavariable to a term as z 7→ tl

7Presheaf with transitive relation (A, >A )Def. A presheaf A ∈ SetF is equipped with a transitive relation >A if(1) >A is a family {>A(n) }n∈F ,where >A(n) is a transitive relation on A(n) (family)(2) for all a, b ∈ A(m) and ρ : m → n in F,
if a >A(m) b, then A(ρ)(a) >A(n) A(ρ)(b). (natural)
Def. (A1 , >A1 ), . . . , (Al , >Al ), (B, >B )A arrow f : A1 × · · · × Al

- B in SetF is monotone iff (n)(a1 , . . . , al ) >B(n) f (n)(b1 , . . . , bl )Ak (n) 3 ak >A(n) bk ∈ Ak (n) for some k, andAj (n) 3 aj ≥A(n) bj ∈ Aj (n) for all j 6= k.

8Term-generated assignmenta V + Σ-algebra Aa valuation θ : Z → TΣV · · · an arrow of SetF
Def. A term-generated assignment θ̂ : Z → A is given byZθ- TΣV!A-A

where !A is the unique V + Σ-algebra homomorphismfrom an initial algebra TΣV.
ExamplesB A = TΣV (Terms)
B A = MΣ Z (Meta-terms)
B A = H (for clones)

9Monotone Algebra
Def. A monotone V+Σ-algebra (A, >A ) is a V+Σ-algebra
AA = (A, {ν, f }f ∈Σ )equipped with a transitive relation >A such thatevery operation f A is monotone.
A is well-founded if >A(n) is well-founded for every n.

10Monotone Algebraa CRS R
Def. A monotone V+Σ-algebra (A, >A ) satisﬁes a rewrite ruleZ | n `l→r
if for all term-generated assignments θ̂ : Z → A,(1)]θ̂ n (l)>A(n)]θ̂ n (r),holds.
A (V+Σ, R)-algebra A isa monotone V+Σ-algebra A that satisﬁes all rules in R.

11Interpretation in (V+Σ, R)-algebraZηZ- MΣ ZAAAθAAUA
Σ-monoidθ]?

TΣV!A?
V+Σ-algebra A

Z | n `l→r∈R· · · a rulea unique Σ-monoid morphism]]

θ n (l) →R θ n (r)· · · a rewrite

a unique V+Σ-algebra homomor.

]]!A θ n (l) >A(n+k) !A θ n (l)· · · an interpretation

12

Example of (V+Σ, R)-Algebra: Polynomial Interp.
B ∀(y.∃(x.(¬p(x) ∨ q(y)))).
KN ∈ SetF

B V+Σ-algebra (KN , >KN )– carrier KN (n) = N– operations

NνKn (x) = 0KK∧n N (x, y) = ∨n N (x, y) = 2x + 2yKK

∀n N (x) = ∃n N (x) = x + 1
All operations are monotone.
– x >KN (n) y⇔x >N yB CRSp∧∀(x.q[x]) → ∀(x.p∧q[x])K¬n N (x) = 2x

13

Important Example of (V+Σ, R)-Algebra
Terms with Rewrites
Prop. The presheaf TΣV of terms is equipped with the transitive
relation {→+R(n) }n∈N .
Proof. Transitivity of each →+R(n) is immediate.
It is also natural: we haven ` s →R t
n0 ` ρ(s) →R ρ(t)for any ρ : n → n0 in F, by induction on proof trees.

14

Important Example: Term Algebra
Thm. (TΣV, →+R ) is an (V+Σ, R)-algebra.
Moreover, it is initial:
There exists a unique monotone homomorphism TΣV
for any (V+Σ, R)-algebra A.

- A,Proof.
Since TΣV is an initial V+Σ-algebra, !A : TΣVV+Σ-algebra homomorphism.

- A is a unique

It remains to show !A is monotone, i.e.
+s →R t⇒!A(n) (s) >A(n) !A(n) (t)By induction on the proof of s →+R t.

15CorollaryCor.

n ` s →+
R tholds.

⇔!A(n) (s) >A(n) !A(n) (t)for any monotone homomorphism ! : TΣV(V+Σ, R)-algebra(A, >A ).
Proof. [⇒]: By the previous theorem.
[⇐]: Take (A, >A ) = (TΣV, →+R ).

- A to16Main Theorem
Thm. A CRS R is terminating(V+Σ, R)-algebra.

iﬀ there is a well-founded

Proof. (⇐): Suppose a well-founded (V+Σ, R)-algebra (A, >A ).
Assume R is non-terminating:n ` t 1 →R t 2 →R · · · .
By the previous Corollary,!A(n) (t1 ) >A(n) !A(n) (t2 ) >A(n) · · · .
Contradiction.
(⇒): When a CRS R is terminating, the initial (V+Σ, R)-algebra(TΣV, →+R ) is a desired well-founded algebra.
I Proof methond of termination of CRS:
Find a well-founded (V+Σ, R)-algebra.

17

ExampleBinding signature Σ = {c : h0i}.
1f ,x

1CRS R| 1 ` c(f[f[x[1]]]) → f[x[1]].

B Intuitively, this CRS is terminating:at any rewrite step the number of c-symbols decreases.
B The interpretation method of higher-order rewriting uses
hereditary monotone functionals cannot show termination of R
due to the incompleteness [van de Pol ’93 ’96].
B Take the monotone V+Σ-algebra (TΣV, ÂTΣV )s ÂTΣV(n) t
if the number of c-symbols in s and t
B Any assignment into TΣV is of the form f 7→ ck (x), x 7→ cm (x)B This gives a well-founded (V+Σ, R)-algebra.

18

Examplemap(x.f[x], nil) → nilmap(x.f[x], cons(y, ys)) → cons(f[y], map(x.f[x], ys))
B V+Σ-algebra, carrier: presheaf of clones H ∈ SetF
H(0) = N
H(n) = (Nn→ N)(for n > 0)H(ρ)(f ) = f ◦ hπ ρ1 , . . . , π ρm i
Hniln = K1 : Noperations (at n):Hn→Nconsn (x, y) = (+) ◦ hx, y, K2i : N
Hn→Nmapn (f, a) = f ◦ hid, K3i + (×) ◦ ha, f ◦ hid, aiiHν n (0) = K0

19

Example of Termination Proofmetavariables p0 and q1 . CRS R.
p∧∀(x.q[x]) → ∀(x.p∧q[x])∀(x.q[x])∧p → ∀(x.q[x]∧p)p∨∀(x.q[x]) → ∀(x.p∨q[x])∀(x.q[x])∨p → ∀(x.q[x]∨p)p∧∃(x.q[x]) → ∃(x.p∧q[x])∃(x.q[x])∧p → ∃(x.q[x]∧p)p∨∃(x.q[x]) → ∃(x.p∨q[x])∃(x.q[x])∨p → ∃(x.q[x]∨p)¬∀(x.q[x])¬∃(x.q[x])→ ∃(x.¬(q[x]))→ ∀(x.¬(q[x]))(1) Give the de Bruijn level notation version of R
(2) Show termination of R by a polynomial interpretation.

20

Example of Termination Proof
B Just replace the variable x with 1.
p∧∀(1.q[1]) → ∀(1.p∧q[1])¬∀(1.q[1]) → ∃(1.¬(q[1]))∀(1.q[1])∧p → ∀(1.p∧q[1])¬∃(1.q[1]) → ∀(1.¬(q[1])),etc.
B Deﬁne a monotone V+Σ-algebra (K, >K )– carrier K(n) = N– order >K(n) is the standard order > on N
Take the operations as the polynomials.
∧¬

KN

KN

KN

(x, y) = 2x + 2yKN

KN

(x, y) = ∨(x) = 2x∀(x) = ∃(x) = x + 1.

All operations are monotone.
We show that KN satisﬁes the rules: take an assignment

ϕ : X → KN by p 7→ x ∈ N and q 7→ y ∈ N, then21]

ϕn (p∧∀(1.q[1])) = 2x + 2(y + 1) >KN (n) (2x + 2y) + 1]

= ϕn (∀(1.p∧q[1]))]]ϕn (¬∃(1.q[1])) = 2(y + 1) >KN (n) 2y + 1 = ϕn (∀(1.¬(q[1])))Other rules are similar.
Since >KN (n) = > is well-founded, this shows KN is a well-founded(V+Σ, R)-algebra.
Hence the “binding” CRS R is terminating.
(cf. Section 9 of the lecture note)