1Complete Algebraic Semantics for
Second-Order Rewriting Systems
based on
Abstract Syntax with Variable Binding

Makoto Hamana
Faculty of Informatics, Gunma University, JapanSYCO 1019th December, 2022, Edinburgh

2This Talk
B Complete algebraic semantics of second-order rewriting
B Based on my paper– Complete Algebraic Semantics for Second-Order Rewriting Systems based on
Abstract Syntax with Variable Binding– MSCS, CUP, 2022,
Special Issue of John Power Festschrift

3First-order Rewriting: Review
First-Order Term Rewriting System (TRS) R:
f act(0) → S(0)f act(S(x)) → f act(x) ∗ S(x)Rewrite steps:fact(S(S(0))) => fact(S(0)) * S(S(0)) => (fact(0) * S(0)) * S(S(0))=> (S(0) * S(0)) * S(S(0)) ==> S(S(0))(normal form)
Fundametal problem
B Termination(Strong Normalisation)

B How can we prove the termination of R?

4TRS: Sound and Complete Algebraic Characterisation
Thm. [Huet and Lankford’78]
A ﬁrst-order term rewriting system R is terminating⇔
there exists a well-founded monotone Σ-algebra (A, >A ) thatis compatible with R.

Termination proof method[⇐] Find a well-founded monotone Σ-algebra that is compatible with R.

5First-order Rewriting: Review
First-Order Term Rewriting System (TRS) R:
f act(0) → S(0)f act(S(x)) → f act(x) ∗ S(x)Semantics: well-founded monotone Σ-algebra (N, >) given byN

f act (x) = 2x + 2Nx∗ y =x+y

NS (x) = 2x + 1

N

0 =1

Then it is compatible with R as
f actN (0N )=2+2

f actN (S N (x)) = 2(2x + 1) + 2Hence R is terminating.

= S N (0N )

>

2+1>

2x + 2x + 1 = f actN (x) ∗ S N (x)6

Aim: Sound and Complete Algebraic Characterisation
Thm. [Huet and Lankford’78]
A ﬁrst-order term rewriting system R is terminating⇔
there exists a well-founded monotone Σ-algebra A thatis compatible with R.
B Aim: Extend this to second-order rewriting
B Give: Complete algebraic semantics of second-order rewriting

7

Example of Second-Order Rewriting : 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]))Signature: ¬, ∧, ∨, ∀, ∃Second-Order Rewriting System is deﬁned on
Second-Order Abstract Syntax [Hamana’04, Fiore LICS’06]
B Abstract syntax with variable binding [Fiore, Plotkin, Turi LICS’99]
B Metavariables with arities (e.g. p,q)
B Substitutions (Metavars, object vars)

8Example: the λ-calculus as a Second-Order Rewriting System

λ(x.M[x]) @ N → M[N]λ(x.M @ x) → M
B Signature: λ, @9Abstract Syntax and Variable Binding [Fiore,Plotkin,Turi LICS’99]
B Aim: To model syntax with variable binding, e.g.
x1 , . . . , x n ` x i

x1 , . . . , x n ` t x 1 , . . . , x n ` s
x1 , . . . , xn ` t@s

x1 , . . . , xn , xn+1 ` t
x1 , . . . , xn ` λ(xn+1 .t)
B Syntax generated by 3 constructors
B λ is a special unary function symbol:
it decreases the context

10Abstract Syntax and Variable Binding [Fiore,Plotkin,Turi LICS’99]
B Aim: model syntax with variable binding, e.g.
n `in `t n `sn ` t@sn+1 `tn ` λ(n + 1.t)
B Category F for variable contexts
objects: n = {1, . . . , n}(variable contexts)
arrows: all functions n → n0 (renamings)
B Presheaf category SetF

11Models of Syntax with Binding: Σ-Algebras in SetF
Def. A binding signature Σ is a set of function symbols with binding arities:
f : hn1 , . . . , nl iwhich has l arguments and binds ni variables in the i-th argument .
Def. A Σ-algebra A = (A, [f A ]f ∈Σ ) in SetF consists ofB carrier: a presheaf A ∈ SetF
B operations: arrows of SetFfAnn: δ 1A × . . . × δ lA

corresponding to function symbols f : hn1 , . . . , nl i ∈ Σ.
B Context extension:δA ∈ SetF ; (δA)(n) = A(n + 1)

-A

12

Example: λ-terms
B Binding signature Σλ for λ-terms
λ : h1i,@ : h0, 0i

B Carrier: the presheaf Λ of all λ-terms
Λ(n) = {t | n ` t}Λ(ρ) : Λ(m) → Λ(n)renaming on λ-terms for ρ : m → n in F.

B Forms a V+Σλ -algebravarΛ : V → Λi 7→ i@Λ : Λ × Λ → Λs , t 7→ s@t

λΛ: δΛλΛ (n) : Λ(n + 1) → Λ(n)t

B Presheaf of variables: V ∈ SetF ; V(n) = {1, . . . , n}
B Thm. Λ (= TΣV) is an initial V + Σλ -algebra.

→Λ7→ λn+1.t13Second-Order Abstract Syntax
B Abstract syntax with variable binding
B Metavariables with arities
B Substitutions (Metavars, object vars)

14

Models of Secound-Order Abstract Syntax: Σ-monoids
B A Σ-monoid [Fiore, Plotkin, Turi’99] is– a Σ-algebra A with– a monoid structureVν- A ¾µA•A

in the monoidal category (SetF , •, V),– both are compatible.
B Idea– Unit ν models the embedding of variables– Multiplication µ models substitution for object variables

15

Algebraic Characterisation of Syntax with Binding
Given a binding signature ΣB The presheaf of all Σ-terms
TΣV(n) = {t | n ` t}
B Multiplication µ : TΣV • TΣV → TΣV(m)µn(t; s1 , . . . , sm ) , t[1 := s1 , . . . , n := sm ](the substitution of Σ-terms for de Bruijn variables)

15

Algebraic Characterisation of Syntax with Binding
Given a binding signature Σ
B The presheaf of all Σ-terms
TΣV(n) = {t | n ` t}
B Multiplication µ : TΣV • TΣV → TΣV(m)µn(t; s1 , . . . , sm ) , t[1 := s1 , . . . , n := sm ](the substitution of Σ-terms for de Bruijn variables)
B Thm. [Fiore, Plotkin, Turi’99]– (TΣV, ν, µ) is an initial Σ-monoid.
– (TΣV, ν)

is an initial V + Σ-algebra.

I How to model metavariables and substitutions for metavariables?

15Algebraic Characterisation of Syntax with Binding
Given a binding signature ΣB The presheaf of all Σ-terms
TΣV(n) = {t | n ` t}
B Multiplication µ : TΣV • TΣV → TΣV(m)µn(t; s1 , . . . , sm ) , t[1 := s1 , . . . , n := sm ](the substitution of Σ-terms for de Bruijn variables)
B Thm. [Fiore, Plotkin, Turi’99]– (TΣV, ν, µ) is an initial Σ-monoid.
– (TΣV, ν)

is an initial V + Σ-algebra.

I How to model metavariables and substitutions for metavariables?
I Free Σ-monoids [Hamana, APLAS’04]

16

Meta-terms: Terms with Metavariables [Aczel ’78]
B A binding signature ΣB Z is an N-indexed set of metavariables parameterised by arities:lZ(l) , {M | M , where l ∈ N}.
B Raw meta-terms generated by Z:t ::= x | f (x1 · · · xi1.t1 , . . . , x1 · · · xil.tl ) | M[t1 , . . . , tl ]B A meta-term t is a raw meta-term derived from:x∈nn `xf : hi1 , . . . , il i ∈ Σ n+i1 ` t1 · · · n+il ` tln ` f ( n+1 . . . n+i1 .t1 , . . . , n+1 . . . n+il .tl )M ∈ Z(l) n ` t1 · · · n ` tln ` M[t1 , . . . , tl ]

17

Meta-terms: Terms with Metavariables
B Presheaf MΣ Z ∈ SetF
MΣ Z(n) = {t | n ` t}
B V+Σ-algebra (MΣ Z, [ν, fT ]f ∈Σ )ν(n) : V(n)xfT- MΣ Z(n),-xii: δ 1 MΣ Z× · · · × δ l MΣ Z
(t1 , . . . , tl )- MΣ Z- f (n+i1 .t1 , . . . , n+il .tl ).

B Multiplication µ : MΣ Z • MΣ Z → MΣ Zt,s- t[1 := s1 , . . . , n := sn ]· · · substitution of meta-terms for object variables

18Free Σ-monoids: Syntax with Metavariables [Hamana, APLAS’04]
Thm. (MΣ Z, ν, µ) forms a free Σ-monoid over Z.
B Freeness of MΣ Z: in SetF , given assignment θZ

ηZ- MΣ Z@@@
θ @@R∃! θ ]Σ-monoid morphism?

AΣ-monoidB The unique Σ-monoid morphism θ ] that extends θ.

19Instance: Substitution for Metavariables
Case A = TΣV· · · a Σ-monoid of terms,
ηZ- MΣ ZZ@@
θ @R@∃! θ ]

Σ-monoid morphism?

TΣV
B θ ] is a substitution of terms for metavariables Z
B E.g. Σ: signature for λ-terms, for θ(M(1) ) = a@a]

θ ( λ(x.M[x]@y) ) = λ( x.(x@x)@y )B Other examples of Σ-monoid A:– MΣ Z: meta-substitution: substitution of meta-terms for metavars– Any Σ-monoid as a model – θ ] is compositional interpretation

20

Second-Order Rewriting System
Eg. A transformation to prenex normal formsp∧∀(x.q[x]) → ∀(x.p∧q[x])Def.
Rewrite rules Rl→r¬∀(x.q[x]) → ∃(x.¬(q[x]))on meta-terms MΣ Z(with some syntactic conditions)

Rewrite relation→Ron terms TΣVl→r∈R
θ ] (l) →R θ ] (r)s →R tf (. . . , x.s, . . .) →R f (. . . , x.t, . . .)B Substitution θ : Z → TΣV maps metavariables to terms
B NB. rewriting is deﬁned on terms (without metavars)

21

Presheaf with relation (A, >A )Def. A presheaf A ∈ SetF is equipped with a binary relation >A , if
1. >A is a family {>A(n) }n∈F ,2. which is compatible with presheaf action.
(for all a, b ∈ A(m) and ρ : m → n in F,
if a >A(m) b, then A(ρ)(a) >A(n) A(ρ)(b).)

22

Monotone Algebra
Def. A monotone V+Σ-algebra (A, >A ) is a V+Σ-algebra (A, [ν, f A ]f ∈Σ )B equipped with a relation >A such that
B every operation f A is monotone.
Thm. (TΣV, →R ) is a monotone V+Σ-algebra.

23

Models of Rewrite System R: (V+Σ, R)-algebras
A (V+Σ, R)-algebra (A, >A ) is a monotone V+Σ-algebra satisfying all rules in R as:ZηZ- MΣ Z

@
@@
θ]
θ@
@
@
R?
initial V+Σ-algebra TΣV!A?
V+Σ-algebra

Al→r∈R· · · a rulea unique Σ-monoid mor. extends θ]]θ n (l) →R θ n (r)· · · a rewrite

a unique V+Σ-algebra homomor.

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

24Soundness and Completeness of Models
Prop.

s →R t⇔!A (s) >A !A (t)for all (V+Σ, R)-algebras A, assignments θ.

Proof. [⇒]: By induction of the proof of rewrite.
[⇐]: Take (A, >A ) = (TΣV, →R ).

25

Complete Characterisation of Terminating Second-Order RewritingThm. A second-order rewriting system R is terminating
iﬀ there is a well-founded (V+Σ, R)-algebra (A, >A ).

Proof. (⇐): Suppose a well-founded (V+Σ, R)-algebra (A, >A ).
Assume R is non-terminating:
t1 →R t2 →R · · · .
By soundness,!A (t1 ) >A(n) !A (t2 ) >A · · · .
Contradiction.
(⇒): When R is terminating, the (V+Σ, R)-algebra (TΣV, →R ) is a well-founded algebra.
I Because of the algebraic chatersiations of abstract sytanx with binding [FPT’99] andmeta-terms [H.04]

26

Application: Termination by Interpretationp∧∀(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]))Take a well-founded monotone V+Σ-algebra (K, >K )where K(n) = N with >K(n) = > on N.
OperationsKKKν n (i) = 0∧n (x, y) = ∨n (x, y) = 2x + 2yK∀n (x) = ∃n (x) = x + 1.

¬n (x) = 2xK

K(V+Σ,R)-algebra]]!θ 0 (p ∧ ∀(1.q[1])) = 2x + 2(y + 1) >K(0) (2x + 2y) + 1 =!θ 0 (∀(1.p ∧ q[1]))]]!θ 0 (¬∃(1.q[1])) = 2(y + 1) >K(0) 2y + 1 =!θ 0 (∀(1.¬(q[1]))).

27

Summary
B Complete algebraic semantics of second-order rewriting systems
B Based on my paper– Complete Algebraic Semantics for Second-Order Rewriting Systems based on
Abstract Syntax with Variable Binding– MSCS, CUP, 2022,
Special Issue of John Power Festschrift

29

Summary
B Complete algebraic characterisation of second-order rewriting systems
B using algebraic models of second-order abstrax syntax
Further Topics and Applications
B Meta-rewriting: rewriting on meta-terms using monotone Σ-monoids
B Modularity of Termination for Second-Order rewriting [H. LMCS’21]
A: terminating & B terminating ⇒A ] B : terminatingwith several conditions
B Tool SOL for termination and conﬂuence checking
1st places in the Higher-order Category of– International Conﬂuence Competition 2020
– Termination Competition 2022
http://solweb.mydns.jp/webcui/sol/28

Summary
B Complete algebraic semantics of second-order rewriting systems
B Based on my paper– Complete Algebraic Semantics for Second-Order Rewriting Systems based on
Abstract Syntax with Variable Binding– MSCS, CUP, 2022,
Special Issue of John Power Festschrift
B Short history: I visted LFCS, Edinburgh
in 1999-2000 as a JSPS postdoc.
B Thanks to John Power, Gordon Plotkin