1Theory and Practice of Second-Order Rewriting:Foundation, Evolution, and SOL

Makoto Hamana
Department of Computer Science,
Gunma University, JapanFLOPS 2020
Virtual Symposium, 14th September, 2020

2This Talk
An overview of the theory and practice of second-order rewriting

3Introduction
B Rewrite rules are ubiquitous in Programming Language research⇒(beta)(λx. M ) N(assoc)

let y=(let x=L in M) in N(unit)

0 + X

⇒

M [x := N ]X⇒(unitR)let x=L in (let y=M in N)
return(x) À-- λy.K yMain problems
B Terminating?
B Unique normal forms?

⇐ conﬂuence

B Decidability of equational theory
I General framework: Second-Order Computation Systems
I System: SOL, Second-Order Laboratory⇒K x

4This Talk
1. Foundation
B Formal deﬁnition
B Properties: Conﬂuence and termination
2. Evolution
B Second-order abstract syntax
B Second-order algebraic theories
B Second-order computation systems
B Examples: λ-calculus, global state
3. SOLB Interface: GHCi, Web interface
B Live Demo5

A Dream of Pragmatics

6

How Second-Order Rewriting EvolvedPlotkin

RTA 1998 Binding Algebras(Tsukuba)

7

How Second-Order Rewriting Evolved
Plotkin

RTA 1998 Binding Algebras(Tsukuba)

I Algebras Ã Types
I Algebraization of program concepts

8How Second-Order Rewriting Evolved
Plotkin

RTA(Tsukuba)

Fiore, Plotkin, Turi LICS

1998 Binding Algebras:
A Step from Universal Algebra to Type Theory
1999 Abstract Syntax and Variable Binding

9How Second-Order Rewriting Evolved
Plotkin

RTA(Tsukuba)

1998 Binding Algebras:
A Step from Universal Algebra to Type Theory

Fiore, Plotkin, Turi

LICS

1999 Abstract Syntax and Variable Binding

Fiore

PPDP

2002 Typed Abstract Syntax with Variable Binding

HamanaAPLAS

2004 Free Σ-monoids: HOAS with Metavariables

HamanaRTA

2005 Complete algebraic semantics of second-order rewriting

Ghani,Uustalu,Hamana HOSC

2006 HOAS with Explicit substitutions

HamanaPPDP2007 Higher-order Semantic labelling for Typed rewriting

Fiore,Hur,Mahmoud

MFCS,CSL

2010 Second-Order Algebraic Theories

Fiore, Hamana

LICS

2013 Polymorphic Algebraic Theories

HamanaICFP2017 Second-Order Computation Systems and SOL

HamanaFLOPS 2018 PolySOL

Hamana,Abe,Kikuchi SCP

2020 Polymorphic Conﬂuence with Call-by-Value

10This Talk
1. Foundation
B Formal deﬁnition
B Properties: Conﬂuence and termination
2. Evolution
I Second-order abstract syntax
B Second-order algebraic theories
B Second-order computation systems
B Examples: λ-calculus, global state
3. SOLB Interface: Web interface
B Live Demo11

What is Second-Order Abstract Syntax
B Ordinary notation
aλx .f x∀x.bird(x) → ﬂy(x)B Second-order abstract syntaxalam(x .app(f, x)),forall(x.imp(bird(x), ﬂy(x)))

B using a signature
lam : (a → b) → Arr(a, b),app : Arr(a, b), a → b,

forall : (i → i) → i,

B with metavariableslam(x.M[x])forall(x.imp(P[x], Q[x]))B Substitution for metavariableslam(x.M[x]){M 7→ y.app(f, y)} = lam(x.app(f, x))
forall(x.L[x]){L 7→ y.forall(y.imp(bird(y), ﬂy(y)))} = · · ·12

Second-Order Abstract Syntax: Related Work
B Meta-terms– Peter Aczel. A general Church-Rosser theorem,
unpublished, University of Manchester, 1978.
– Peter Aczel. Frege structures and the notions of proposition, truth and set, The Kleene
Symposium: Proceedings of the Symposium Held June 18-24, 1978 at Madison,
Wisconsin, U.S.A.
– J. W. Klop. Combinatory Reduction Systems,CWI, volume 127 of Mathematical Centre Tracts, 1980.

13

Second-Order Abstract Syntax: Types and Signature
Typed syntax with variable binding and metavariables
B A is a set of atomic types (e.g. Bool, Nat, etc.)
B the set of molecular types (mol types) B is
B = A ∪ {T (a1 , . . . , an ) | a1 , . . . , an ∈ B, T is an n-ary type constructor}
B A signature Σ is a set of function symbols of the formf : (a1 → b1 ), . . . , (am → bm ) → c
where all ai , bi , c are mol types
B Any function symbol is of up to second-order type

14

Second-Order Abstract Syntax: Terms
B A metavariable is a variable of (at most) ﬁrst-order function type, declared as M : a → b
B A variable is always of a molecular type b (not of a function type)
B The raw syntax- Terms have the formt ::= x | x.t | f (t1 , . . . , tn )- Meta-terms extend terms to t ::= x | x.t | f (t1 , . . . , tn ) | M [t1 , . . . , tn ]The last form M [t1 , . . . , tn ] is called meta-application

15

Second-Order Abstract Syntax: Well-typed Terms
B Judgment
Θ . Γ ` t :b
B Typing rules(M : a1 , . . . , am → b) ∈ Θy :b∈Γ(Var)
Θ . Γ ` y :b

(MetaApp)Θ . Γ ` t i : ai

(1 ≤ i ≤ m)

Θ . Γ ` M [t1 , . . . , tm ] : bf : (a1 → b1 ), · · · , (am → bm ) → c ∈ Σ(Fun)Θ . Γ, xi : ai ` ti : bi

(1 ≤ i ≤ m)

am
1.t,.
.
.
Θ . Γ ` f ( xaxm .tm ) : c11

16

Second-Order Abstract Syntax, Example: the simply-typed λ-calculus
B The signature Σlam for the λ-terms
lama,b : (a → b) → Arr(a, b)
appa,b : Arr(a, b), a → b– parameterised by mol types a, b ∈ B– Arr is a binary type constructor– app is denoted by @.
B Encoding of λ-termsa. ` lama,b (x .x) : Arr(a, b)

a. f : Arr(a, b) ` lama,b (x .app(f, x)) : b

B Encoding of meta-level λ-terms
M : a → b, N : a . ` lama,b (x.M [x]) @a,b N : b
M : a → b, N : a . `M [N ] : b

17Second-Order Abstract Syntax: Semantics
Algebraic models of abstract syntax with variable binding and substitutions= Σ-monoids [Fiore,Plotkin,Turi LICS’99]= Σ-algebras + monoids in a presheaf category SetF
A free Σ-monoid MΣ Z generated by Z is a second-order abstract syntax [HamanaAPLAS’04] .
with metavariables
ZηZ- MΣ Z..
..
@..
@.. ϕ∗@..
ϕ @..
..?
@R
Σ-monoid Aunique Σ-monoid morphism = interpretation

B A is arbitrary algebraic model
B MΣ Zb (Γ) 3 t ::= x | x.t | f (t1 , . . . , tn ) | M [t1 , . . . , tn ]B Models are useful to evaluate terms (e.g. sizes)

18This Talk
1. Foundation
B Formal deﬁnition
B Properties: Conﬂuence and termination
2. Evolution
B Second-order abstract syntax
I Second-order algebraic theories
B Second-order computation systems
B Examples: λ-calculus, global state
3. SOLB Interface: Web interfaceB Live Demo

19

Second-Order Equational Logic
B An equation is of the form
Θ . Γ `s = t :bfor meta-terms Θ . Γ ` s : b and Θ . Γ ` t : b
B Second-order equational logic is an equational logic on second-order terms
B A given set E of equations (axioms) generates a second-order equational theory.
B The inference rules:Θ . Γ0 , xi : ai ` si : bi
(Ax)

(1 ≤ i ≤ k)

(M1 : (a1 → b1 ), . . . , Mk : (ak → bk ) . Γ ` t1 = t2 : c) ∈ E
Θ . Γ, Γ0 ` t1 [ M 7→ x.s ] = t2 [ M 7→ x.s ] : cand reﬂexivity, symmetry, transitivity, and congruence
B Models: second-order algebras satisfying E

20

Second-Order Equational Logic, Example: Simply-typed λ-calculus
B The signature Σlam for the λ-terms
lama,b : (a → b) → Arr(a, b)
appa,b : Arr(a, b), a → b– parameterised by mol types a, b ∈ B– Arr is a binary type constructor– app is denoted by @.
B The β and η lawsaM : a → b, N : a . ` lama,b (x .M [x]) @a,b N= M [N ] : ba

M : b . ` lama,b (x .M @a,b x) = M : b
B Ordinary λ-theory is obtained as a second-order equational theory
B The CCC model of λ-calculus can be an second-order algebraic model [Fiore, PPDP’02]

21

This Talk
1. Foundation
B Formal deﬁnition
B Properties: Conﬂuence and termination
2. Evolution
B Second-order abstract syntax
B Second-order algebraic theories
I Second-order computation systems
B Examples: λ-calculus, global state
3. SOLB Interface: Web interface
B Live Demo22Second-Order Rewriting
B A computation rule is of the form
Θ . Γ `` ⇒ r :b

1. ` is a deterministic second-order pattern

2. all metavariables in r appear in `.

B Second-order pattern [Miller’01]:
a meta-term ` in which every occurrence of meta-application is of the form
M [x1 , . . . , xn ],where x1 , . . . , xn are distinct bound variables.
B Deterministic second-order pattern [Yokoyama, Hu, Takeichi, IPL’04]:
every occurrence of meta-application M [t1 , . . . , tn ] satisﬁes
1. every ti is a term without binders, metavariables or free variables, but it can containfunction symbols with arity n > 0 and bound variables
2. every ti contains at least one bound variable,
3. ti E
6 tj for every 1 ≤ i, j ≤ n.

23

Second-Order Rewriting
B A computation rule is of the form
Θ . Γ `` ⇒ r :b

1. ` is a deterministic second-order pattern

2. all metavariables in r appear in `.

B Second-order pattern [Miller’01]:a meta-term ` in which every occurrence of meta-application is of the form
M [x1 , . . . , xn ],where x1 , . . . , xn are distinct bound variables.
B Deterministic second-order pattern [Yokoyama, Hu, Takeichi, IPL’04]:
Good: A solvable matching problem p = t has a unique matcher
for a deterministic second-order pattern p and a term.
B E.g. M[cons(x,y)], lam(x.M[var(x)]), f(Y,c(x.y.K[y,d(x)]))24

Second-Order Rewriting
B A signature Σ and a set C of computation rules form a computation system (Σ, C).
B Given C, one-step rewriting ⇒Cis deﬁned byΘ . Γ0 , xi : ai ` si : bi(Rule)(1 ≤ i ≤ k)

(M1 : (a1 → b1 ), . . . , Mk : (ak → bk ) . ` ` ⇒ r : c) ∈ C
Θ . Γ0 ` ` [ M 7→ x.s ] ⇒C r [ M 7→ x.s ] : cf : (a1 → b1 ), · · · , (ak → bk ) → c ∈ Σ(Fun)Θ . Γ, xi : ai ` ti ⇒C t0i : bi(some i s.t. 1 ≤ i ≤ k)

ai
ai 0
a1
a1
a1
1.t,.
.
.
,.t)
⇒f
(x.t,.
.
.
,
Θ . Γ ` f (xax.t,.
.
.
,xx.t,.
.
.
,x
11Cki1111 .tk ) : ciii

25Conﬂuence
B To check a computation system (Σ, C) conﬂuent
B Based on Newman’s lemma: local conﬂuence & SN implies conﬂuence
B Local conﬂuence is checked by Knuth-Bendix critical pair checking
B Critical pairs are computed by second-order uniﬁcation,
modiﬁed Function-as-Constructor Uniﬁcation (FCU) [Libal,Miller FSCD’16]
B Uniﬁcation between deterministic second-order patterns
B For more details, [H. PACMPL’17,JFP’19][Hamana,Abe,Kikuchi SCP’20]

26

Termination Checking of Second-Order Computation Systems
B To check a computation system (Σ, C) Strongly Normalising (SN)
1. Interpretation by an algebraic model with well-founded orders ⇒C t

a rewrite step[[−]]?

[[s]] >A [[t]]in a model (A, >A )Thm. [H. RTA’04] A computation system (Σ, C) is SN iﬀ
there exists a well-founded model (A, >A ) of (Σ, C).
2. Syntactic check: The General Schema [Blanqui’00, RTA’00,TCS’16]
3. Modular termination
A : SN and B : SN⇒

A ] B SN

27

Modular Termination Checking
B A : SN and B : SN⇒

A ] B SN?

B Toyama’s counterexample [IPL 1987]

A:f(0,1,X) => f(X,X,X)

B:

or(X,Y)or(X,Y)=> X=> Y

B Each of A and B is terminating.
B Butf(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))28Modular Termination Checking
Theorem [Hamana arXiv:1912.03434]
Given computation systems, where Θ is the set of constructors
B (ΣA ]Θ, A)B (ΣA ] ΣB ] Θ, B),

if(i) A is accessible(ii) each A-function calls only A-functions with second-order patterns(iii) A with projection rules (hM1 , M2 i ⇒ Mi ) is SN (not necessary by GS)(iv) B is SN by the General Schema.
then (ΣA ] ΣB ] Θ, A ] B) is SN.
Proof By higher-order semantic labelling [H. PPDP’07]
based on the algebraic models of second-order rewriting [H. RTA’04] and GS.

29

Modular Termination CheckingTheorem [Hamana arXiv:1912.03434]
Given computation systems, where Θ is the set of constructors
B (ΣA ]Θ, A)

B (ΣA ] ΣB ] Θ, B),

if(i) A is accessible(ii) each A-function calls only A-functions with second-order patterns(iii) A with projection rules (hM1 , M2 i ⇒ Mi ) is SN (not necessary by GS)(iv) B is SN by the General Schema.
then (ΣA ] ΣB ] Θ, A ] B) is SN.
Applications
1. Dividing C into ﬁrst-order part A + higher-order part B, andinvoking external FO SN checkers (implemented in SOL)

30

Modular Termination CheckingTheorem [Hamana arXiv:1912.03434]
Given computation systems, where Θ is the set of constructors
B (ΣA ]Θ, A)

B (ΣA ] ΣB ] Θ, B),

if(i) A is accessible(ii) each A-function calls only A-functions with second-order patterns(iii) A with projection rules (hM1 , M2 i ⇒ Mi ) is SN (not necessary by GS)(iv) B is SN by the General Schema.
then (ΣA ] ΣB ] Θ, A ] B) is SN.
Applications
2. SN of CBPV + algebraic eﬀect handler + eﬀect theory.
[Levy’06][Pretnar,Plotkin’13] [Plotkin,Power’02]

31

Example: Theory of Global StateB The theory of global state for the single location [Plotkin,Power’02] as computation rules
sigst = [signature|lk : (Val -> A) -> A;

ud : Val,A -> A|]

gstate = [rule|(lu) lk(v.ud(v,X))=> X(ll) lk(w.lk(v.X[v,w])) => lk(v.X[v,v])(uu) ud(V,ud(W,X))=> ud(W,X)(ul) ud(V,lk(w.X[w]))=> ud(V,X[V]) |]B (lu) says that looking-up the state, binding the value to v, then updating the state to v, isequivalent to doing nothing.
B Correspond to state monad
I An algebraization of program concept
B Decidable?
B SN: the number of lk,ud are decreasing.

32

Example: Local Conﬂuence of Theory of Global StateWe check local conﬂuence in SOL
Step 1: Enumerate critical pairs*SOL> cri gstate sigst
1: Overlap (lu)-(uu v)--- V’|-> z1.z1, X|-> ud(H1,H2), W’|-> z1.H1, X’|-> z1.H2 -(lu) lk(v.ud(v,X)) => X(uu v) ud(V’[v],ud(W’[v],X’[v])) => ud(W’[v],X’[v])lk(v.ud(v,ud(H1,H2)))
ud(H1,H2) <-(lu)-∧-(uu v)-> lk(v.ud(H1,H2))---> ud(H1,H2) =#= lk(v.ud(H1,H2)) <--...
8: Overlap (ul)-(ll)--- X|-> z1.lk(v’.X’[v’,z1]) -----------------------------(ul) ud(V,lk(w.X[w])) => ud(V,X[V])(ll) lk(w’.lk(v’.X’[v’,w’])) => lk(v’.X’[v’,v’])ud(V,lk(w.lk(v’.X’[v’,w])))ud(V,lk(v’.X’[v’,V])) <-(ul)-∧-(ll)-> ud(V,lk(vd32.X’[vd32,vd32]))---> ud(V,X’[V,V]) =OK= ud(V,X’[V,V]) <--#NON 3 joinable... (Total 8 CPs)

33

Example: Theory of Global State
Step 2: Manual Knuth-Bendix competition
Add rules from non-joinable critical pairs
gstateEx1 = [rule| (lu1)(lu2)

lk(v1.ud(W’,X’))=> ud(W’,X’)
lk(v2.ud(v2,X’[v2])) => lk(w’.X’[w’]) |]Step 3: Recheck*SOL> cri (gstate ++ gstateEx1) sigst..
#NON 1 joinable... (Total 17 CPs)

Step 4: Repeat this process until all CPs are joinable
gstateEx2 = [rule| (l) lk(w.X) => X |]B The theory of global state is decidable.
B Computation system (gstate ++ gstateEx1 ++ gstateEx2) provides a decision procedure.

34

Further Topics and Future Work
1. Foundation
B Properties: Conﬂuence and termination
I Churh-Rosser modulo equivalence
2. Evolution
B Second-order abstract syntax, algebraic theories, computation systems
B Polymorphic computatin systems with call-by-value
B Examples: λ-calculus, global state
I Examples: π-calculus [Stark TCS’08][H. JFP’19],
coherence of monoidal category [H. JFP’19], Skew monoidal category [H. SCP’20]
3. SOLB Interface: GHCi, Web interface
I More powerful and generic rewriting tool
I More checking properties, strategic/manual rewriting engine and UII Open source at GitHub, Hackage – in preparation

35

Summary
An overview of the theory and practice of second-order rewriting
B Importance of algebraization of program concepts
B Second-order algebraic theories can axiomatise program concepts
B Second-order rewriting gives a computational method forsecond-order algebraic theories
B Looking for– Collaborators– Postdocs/internships welcome!
B Contact <hamana@gunma-u.ac.jp>
B Try SOL on web
http://www.cs.gunma-u.ac.jp/hamana/sol/

36

How Second-Order Rewriting Evolved
Plotkin

RTA(Tsukuba)

1998 Binding Algebras:
A Step from Universal Algebra to Type Theory

Fiore, Plotkin, Turi

LICS

1999 Abstract Syntax and Variable Binding

Fiore

PPDP

2002 Typed Abstract Syntax with Variable Binding

HamanaAPLAS

2004 Free Σ-monoids: HOAS with Metavariables

HamanaRTA

2005 Complete algebraic semantics of second-order rewriting

Ghani,Uustalu,Hamana HOSC

2006 HOAS with Explicit substitutions

HamanaPPDP2007 Higher-order Semantic labelling for Typed rewriting

Fiore,Hur,Mahmoud

MFCS,CSL

2010 Second-Order Algebraic Theories

Fiore, Hamana

LICS

2013 Polymorphic Algebraic Theories

HamanaICFP2017 Second-Order Computation Systems and SOLHamana

FLOPS 2018 PolySOL

Hamana,Abe,Kikuchi SCP

2020 Polymorphic Conﬂuence with Call-by-Value