1Polymorphic Rewrite Rules
Conﬂuence, Type Inference, and Instance Validation

Makoto Hamana
Department of Computer Science,
Gunma University, JapanFLOPS 2018
Nagoya University, May, 2018

2Motivation
B A calculus for programming languages is often given as
simply-typed computation rules
B Require a schematic type notation
B Simply-typed λ-calculus:(β)Γ ` (λxσ . M ) N⇒

M [x := N ]:τ– Point: σ and τ are not ﬁxed types, but schemata of types– Represents various instances of rules, such as(β bool,int )Γ ` (λxbool . M ) N⇒

M [x := N ]: int(β int→int,bool )Γ ` (λxint→int . M ) N⇒

M [x := N ]: bool···3Problems and This Work
B Not explored in the theory of rewriting
B How to ensure conﬂuence of polymorphic rules generally
B A novel framework for polymorphic computation rules
B A computational reﬁnement of second-order algebraic theories[Fiore, Hur CSL’10]– logic programming [Staton FoSSaCS’13]– algebraic eﬀects [Staton LICS’13]– quantum computation [Staton POPL’15]

4

Example: Conﬂuence of λc [Moggi’88]
I The computational λ-calculus
Call-by-value λ-calculus with let for sequential computation(β-v)
lam(x.M[x]) @ V => M[V]; (η-v)lam(x.V @ x) => V
; (η-let) let(L, x.x) => L(β-let-v) let(V, x.M[x]) => M[V](let1-p) P @ M=> let(P,x.x@M)(let2-v) V @ P=> let(P,y.V@y)(assoc)let(let(L,x.M[x]), y.N[y]) => let(L,x.let(M[x],y.N[y]))B Values and non-values:
Values
V::= x | λx.M

Non-values P ::= M @N | let x = M in N
B Encoding: λx.M as lam(x.M), let x = M in N as let(M,x.N)
B SN [Lindley, Stark TLCA’05]
B Conﬂuent?

5

Two Rewriting Properties
Conﬂuence

Local Conﬂuence

MB|∗ ||||||} |BB
BB∗
BB
B!

BBBB
∗ BBB!

|||
||∗
|}||

M1B

N

M2

MB||||||}||

BB
BB
BB
B!

BBBB
∗ BBB!

|||||∗|}||

M1B

N

M2

Newman’s lemma
If a rewrite system is locally conﬂuent & terminating,then it is conﬂuent.

61: lam(x.(V’@x))@V

2: lam(x.(lam(x’.H[x’])@x))

V’@V = V’@V

lam(x’.H[x’])= lam(x.H[x])11°11°(β-v) °°
11(η-v)°§°»©
©
(η-v) ©©
¤©©

77
77
77(β-v)
7¾

4: let(let(L,x’.M’[x’]),x.x)

DDz
DD (assoc)z(η-let) zz
DDzDDz}zz!
let(L,x’.M’[x’]) o let(L,x’.let(M’[x’],x.x))

3: let(V,x.x)

11°11°(β-let-v) °°11(η-let)°§°»V=V

5: let(let(L,x.x),y.N[y])zzz(assoc) zzzz}zlet(L,x.let(x,y.N[y]))6: let(let(let(L’,x’.M’[x’]),x.M[x]),y.N[y])DDDD (η-let)
DDDD!
/ let(L,x.N[x])MMM
qq
MMM(assoc)(assoc)qqqq
MMMqq
MM&
xqqq
let(let(L’,x’.M’[x’]),x.let(M[x],y.N[y]))let(let(L’,x’.let(M’[x’],y’.M[y’])),y.N[y])OOOooOOOoo
OOOoo∗o∗oOOO ooo' · wo

The joinablity of Critical Pairs shows local conﬂuence.
Applying Newman’s lemma, we have conﬂuence
I Knuth-Bendix critical pair checking

7

Critical Pair Checking by PolySOL (1)PolySOL: Haskell-based tool for conﬂuence and termination
Step 1. Write a Haskell script describing rewrite rules and.
signature using PolySOL’s DSL (by Template Haskell)siglamC = [signature|
app : Arr(a,b),a -> blam : (a -> b) -> Arr(a,b)
let : a,(a -> b) -> b|]
B a,b are type variables
B Arr is a type constructor
lamC = [rule|lam(x.M[x]) @ V => M[V]; (η-v)
lam(x.V @ x) => V(β-v)(β-let-v) let(V, x.M[x]) => M[V]; (η-let) let(L, x.x) => L(let1-p) P @ M=> let(P,x.x@M)(let2-v) V @ P=> let(P,y.V@y)(assoc)let(let(L,x.M[x]), y.N[y]) => let(L,x.let(M[x],y.N[y]))|]8

Critical Pair Checking by PolySOL (2)Step 2. Invoke the command cri for critical pair checking*PolSOL> cri lamC siglamC
1: Overlap (β-v)-(η-v)--- M|-> z1.(V’@z1)-------------------------------------L: lam(x.M[x])@V => M[V]R: lam(x’.(V’@x’)) => V’(lam(x.(V’@x))@V)(V’@V) <-(β-v)-∧-(η-v)-> (V’@V)---> (V’@V) =OK= (V’@V) <--..
4: Overlap (η-let)-(assoc)--- M|-> let(L’,x’.M’[x’]), N’|-> z1.z1----------------------L: let(M,x.x) => M
R: let(let(L’,x’.M’[x’]),y’.N’[y’]) => let(L’,x’.let(M’[x’],y’.N’[y’]))let(let(L’,x’.M’[x’]),x.x)let(L’,x’.M’[x’]) <-(eta-let)-∧-(assoc)-> let(L’,xd13.let(M’[xd13],yd13.yd13))---> let(L’,x’.M’[x’]) =E= let(L’,xd13.M’[xd13]) <--..
#Joinable! (Total 6 CPs)

9

Critical Pair(β-v)(η-v)

lam(x.M[x]) @ V => M[V]lam(x.V @ x)=> V

B Second-order uniﬁcation?

lam(x.M[x]) = lam(x.V @ x)
a uniﬁer θ = {M 7→ z.(V @ z)}

1: lam(x.(V’@x))@V®
®
(β-v) ®®
¦®®

33
33 (η-v)
33¼V’@V = V’@V
B This is ordinary10Problems and Questions
1. The notion of uniﬁer for an overlap is non-standard in thecall-by-value case(let1-p)(let2-v)

P @ M
V @ P

=> let(P,x.x@M)=> let(P,y.V@y)

B Not overlapped
B Values and non-values:
Values

V::= x | lam(x.M)

Non-values P ::= M @N | let(M,x.N)
Q1 I What is a general deﬁnition of overlaps when there is arestriction on the term structures?

2. Diﬀerent occurrences of the same function symbol may have11
diﬀerent types(assoc)

let(let(L,x.M[x]), y.N[y]) => let(L,x.let(M[x],y.N[y]))M : c → a, N : a → b, L : c .
a,(a→b)→bΓ ` let⇒ let(letc,(c→a)→ac,(c→b)→b(L, x .letcca(L, x .M [x]), y .N [y])a,(a→b)→ba(M [x], y .N [y]))Q2 I What should be uniﬁcation between polymorphic terms?
3. Specifying all the type annotations in the rule speciﬁcation
manually is tedious and prone to error
Q3 I What is type inference algorithm
for polymorphic computation rules?

: b12This Work
A1I Introduce predicates called instance validation onsubstitutions
It is used for formulating computation steps having some
restriction of term structures.
They aﬀect to the notion of critical pairs.
A2I Formulate uniﬁcation between polymorphic terms
A3I Give a type inference algorithm for polymorphic rules

Q1. What is a general deﬁnition of overlaps?
Q2. What should be uniﬁcation between polymorphic terms?
Q3. What is type inference algorithm for polymorphic rules?

13

A1: Instance Validation
Def. An instance validation is an predicate validthat takes a substitution [ M 7→ x.s ] for metavariables.
Any predicate is OK. e.g.
B Any: valid θdef⇔

B Injectivity: valid θalways true, i.e. any instantiation is valid.
def⇔θ is an injective substitution

B Values/non-values: valid [M1 7→ x1 .s1 , . . .]def

⇔ ((Mi ≡ V ⇒ si is a value) & (Mi ≡ P ⇒ si is a non-value))
for all i.
(values V and non-values P )Instance validation valid is used in formulating
B one-step computation
B overlaps for critical pairs

14

A2: Uniﬁcation between Polymorphic Terms
What should be a uniﬁer between the following polymorphic terms?
lam(bool→t)→Arr(bool,t)(xbool?

.M [x]) = lam(v→int)→Arr(v,int)v(x .gv→int(x))

Here t, v are type variables.
Answer: a type substitution ξ : v 7→ bool, t 7→ int
with a substitution of terms for variables θ : M 7→ xbool .gbool→int (x)Def.
A uniﬁer between polymorphic terms s, t is a pair (θ, ξ) such thatsξθ = tξθ15Computation Step: ⇒C
Given a set C of polymorphic computation rules

S is the set of all type variables in τ i , σ i , τΘ . Γ0 , xi : τ i ` si : σ i ξ(1 ≤ i ≤ k)

type subst. ξ : S → T
valid [ M 7→ x.s ](M1 : (τ 1 → σ 1 ), . . . , Mk : (τ k → σ k ) . Γ ` ` ⇒ r : τ ) ∈ C
Θ . Γ, Γ0 ` `ξ [ M 7→ x.s ] ⇒C rξ [ M 7→ x.s ] : τ ξS . f : (σ 1 → τ 1 ), . . . , (σ m → τ m ) → τ ∈ Σ
Θ . Γ, xi : σ i ` ti ⇒C t0i : σ i ξ

ξ:S →T(some i s.t. 1 ≤ i ≤ m)σi
1σ (xσ 1 .t , . . . , xσ i .t0 , . . .) : τ ξΘ . Γ ` f σ (xσ.t,.
.
.
,x.t,.
.
.)⇒f1i
C
111iii

16

A3: Type Inference
B Type inference function:
infer(Σ, t)
where t is a “plain” term, and Σ is a signature
B A modiﬁcation Damas-Milner type inference algorithm WB Types in our framework is basically ML polymorphism
Thm. (Soundness) If infer(Σ, t) = (Θ . t0 : τ ), then there exists Γsuch that Θ . Γ ` t0 : τ .
Thm. (Completeness) If a given term is typable, then the algorithm
infers a more general type.

17

Example: Conﬂuence of λneed
Maraist, Odersky, and Wadler’s call-by-need λ-calculus λneed[JFP’98]

sigNeed = [signature|lam : (a->b) -> Arr(a,b); app : Arr(a,b),a -> b; let : a,(a->b) -> b |]lmdNeed = [rule|(rG)
let(M, x.N)
=> N
(rI)
lam(x.M[x]) @ N=> let(N,x.M[x])(rV-v) let(V, x.C[x])=> C[V](rC-v) let(V, x.M[x])@N=> let(V, x.M[x]@N)(rA)
let(let(L,x.M[x]), y.N[y]) => let(L,x.let(M[x],y.N[y])) |]I Demo: http://www.cs.gunma-u.ac.jp/hamana/polysol/

18

Summary of This Work
A1I Introduce instance validation predicates on substitutions forformulating computation steps and critical pairs
when there are some restriction of the term structures
A2I Formulate uniﬁcation between polymorphic terms
A3I Give a type inference algorithm for polymorphic rules
I PolySOL system
http://www.cs.gunma-u.ac.jp/hamana/polysol/
Q1. What is a general deﬁnition of overlaps?
Q2. What should be uniﬁcation between polymorphic terms?
Q3. What is type inference algorithm for polymorphic rules?