Polymorphic Rewrite Rules:
Conﬂuence, Type Inference, and Instance Validation
Makoto Hamana
Department of Computer Science, Gunma University, Japan
hamana@cs.gunma-u.ac.jp
Abstract. We present a new framework of polymorphic rewrite rules having
predicates to restrict their instances. It is suitable for formulating and analysing
fundamental calculi of programming languages. A type inference algorithm and acriterion to check local conﬂuence property of polymorphic rules are also given,
with demonstration of the eﬀectiveness of our methodology by examininationof sample program calculi. It includes the call-by-need λ-calculus and Moggi’s
computational lambda-calculus.

1 Introduction
Fundamental calculi of programming languages are often formulated as simply-typed
computation rules. Describing such a simply-typed system requires a schematic typenotation that is best formulated in a polymorphic typed framework. To illustrate thissituation, consider the simply-typed λ-calculus as a sample calculus:(β)Γ ` (λx σ . M) N⇒

M[x := N] :τAn important point is that σ and τ are not ﬁxed types, but schemata of types. Therefore,(β) actually describes a family of actual computation rules. Namely, it represents various
instances of rules by varying σ and τ, such as the following.
(βbool,int )(βint→int,bool )Γ ` (λxbool . M) NΓ ` (λxint→int . M) N⇒⇒

M[x := N]
M[x := N]: int: boolFrom the viewpoint of meta-theory, as in a mechanised formalisation of mathematics,
the (β)-rule should be formulated in a polymorphic typed framework, where types τand σ vary over simple types. This viewpoint has not been well explored in the general theory of rewriting. For instance, no method has been established for checking
the conﬂuence property of a general kind of polymorphically typed computation rules
automatically
We have already recognized this problem. In a previous paper [12], we investigated the decidability of various program calculi by conﬂuence and termination checking. The type system used there was called molecular types, which was intended to
mimic polymorphic types in a simple type setting. However, this mimic setting provided no satisfactory framework to address polymorphic typed rules. For example,
molecular types did not have a way to vary types. Therefore, instantiation of (β) to(βbool,int )(βint→int,bool ) described above could not be obtained. For that reason, no conﬂuence of instances of polymorphic computation rules is obtained automatically. Further
manual meta-theoretic analysis is necessary.

2

Makoto Hamana
1: lam(x.(V’@x))@V

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

1°° 111 (η-v)(β-v) °°
11
§°°
»

ªª
(η-v) ªª¥ªª

V’@V = V’@V

1°° 111 (η-let)
11
§°°
»

(β-let-v) °°lam(x’.H[x’]) = lam(x.H[x])4: let(let(L,x’.M’[x’]),x.x)||(η-let) ||||~||let(L,x’.M’[x’]) o

3: let(V,x.x)

66
66 (β-v)
66
½

V

=

V

5: let(let(L,x.x),y.N[y])BB
BB
BB(assoc)
BB
Ã

|
||
||
|
|~ |

(assoc)let(L,x’.let(M’[x’],x.x))let(L,x.let(x,y.N[y]))BB
BB (η-let)BBBBÃ/ let(L,x.N[x])6: let(let(let(L’,x’.M’[x’]),x.M[x]),y.N[y])rrr(assoc)rrr

LLL
LLL(assoc)
LLL
L%

r
yrrr
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])
NNN
pp
NNN
p∗pp
p
∗ NNN
p
NN& xpppp·
Fig. 1. Critical pairs of the λC -calculus

In the present paper, we give an extended framework for polymorphic computation
rules that solve these issues. The framework is polymorphic and a computational reﬁnement of second-order algebraic theories by Fiore et al. [5, 6]. Second-order algebraic
theories have been shown to be a useful framework that models various important notions of programming languages, such as logic programming [28] and algebraic eﬀects[29], quantum computation [30]. The present polymorphic framework has also applications in these ﬁelds.
1.1

Example: conﬂuence of the computational λ-calculus

We begin with examining a sample conﬂuence problem to illustrate our frameworkand methodology. We consider Moggi’s computational λ-calculus, the λC -calculus [21],which is a fundamental λ-calculus for eﬀectful computation. It is an extension of thecall-by-value λ-calculus enriched with let-construct to represent sequential computation. The λC has two classes of terms: values and non-values.
Values V ::= x | λx.M

Non-values P ::= M@N | let x = M in N

(1)

We now express the expression λx.M as lam(x.M) and let x = M in N as let(M,x.N).
Then the computation rules of λC are described as follows.
lamC = [rule|(β-v)
lam(x.M[x]) @ V => M[V]; (η-v)lam(x.V @ x) => 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])) |]Polymorphic Rewrite Rules: Conﬂuence, Type Inference, and Instance Validation

3

The descriptions “lamC = [rule|” and “|]” indicate the beginning and end of the rule
speciﬁcation in our conﬂuence checker PolySOL. Here the metavariables V and P represent values and non-values, respectively. To the author’s best knowledge, conﬂuenceof the λC -calculus has not been formally proved in the literature including the original[21] and subsequent works [26, 17, 24]. We now prove conﬂuence of the simply typed
λC -calculus.
M@
Conﬂuence (CR) is a property of the reduction relation, stat@@∗∗ ~~@@ing that any two divergent computation paths ﬁnally commute~ÂÄ~~(see the right ﬁgure). Hence, the proof requires to analyse all M1
M2
CR
@
@@
possible situations that admit two ways of reductions, and also to
~~
@
~
∗ @Â
Ä~~ ∗
check convergence of them. In the case of λC , careful inspection
Nof the rules reveals that it has, in all, 6 patterns of such situations
as depicted in Fig. 1. Now we see that all of these patterns are convergent. Importantly,
this ﬁnite number of checks is suﬃcient to conclude that all other inﬁnite numbersof instances of the divergent situations are convergent. This property is called local
conﬂuence, meaning that every possible one-step divergence is joinable. By applying
Newman’s lemma [13, 1], stating “termination and local conﬂuence imply conﬂuence”,
we can conclude that λC is conﬂuent since termination of λC has been proved [17]. This
proof method is known as Knuth and Bendix’s critical pair checking [16]. The divergent
terms in Fig. 1 are called critical pairs because these show critical situations that may
break conﬂuence. The critical pair is obtained by an overlap between two rules, whichis computed by second-order uniﬁcation [20]. For example, there is an overlap between
the rules (β-let-v),(η-let) because the left-hand sides of them?

let(V, x.M[x]) = let(L, x.x)
are uniﬁable by second-order uniﬁcation with a uniﬁer θ = {L 7→ V, M 7→ x.x}. The
instantiated term let(V, x.x) by θ is the source of the divergence (3:) in Fig. 1, which
admits reductions by the two rules (β-let-v),(η-let).
But there are problems. In computing the critical pairs of λC in Fig. 1, the classicalcritical pair method was not applicable. Actually we need a suitable extension of themethod. In the following, we list the problems, related questions and the answers wewill give in this paper.

Problem 1. The notion of uniﬁer for an overlap is non-standard in the call-by-value
case. For example, the left-hand sides of (let1-p) and (let2-v) look overlapped,
but actually are not. A candidate uniﬁer P 7→ V is not correct because P is a non-value
while V is a value.

Q1. What is a general deﬁnition of overlaps when there is a restriction on the term
structures?
Problem 2. Diﬀerent occurrences of the same function symbol may have diﬀerent
types.

4

Makoto Hamana

For example, in (assoc), each let has actually a diﬀerent type (highlighted one) as:
M : c → a, N : a → b, L : c .
a, (a → b) → bΓ ` letc, (c → a) → a(letc, (c → b) → b⇒ let(L, xc .M[x]), ya .N[y])a, (a → b) → b(L, xc .let(M[x], ya .N[y])): b

To compute an overlap between let-terms, we need also to adjust the types of let toequate them.
Q2. What should be the notion of uniﬁcation between polymorphic second-order terms?
Moreover, specifying all the type annotations as above manually is tedious in practice. Ideally, we write a “plain” rule as (assoc), and hope that some system automatically infers the type annotations.
Q3. What is the type inference algorithm for polymorphic second-order computation
rules?
In this paper, we solve these questions.
A1I We introduce predicates called instance validation on substitutions (Def. 3). It is
used for formulating computation steps having some restriction of term structures.
Hence they aﬀect to the notion of critical pairs.
A2I We formulate the notion of uniﬁer for polymorphic terms (Def. 7).
A3I We give a type inference algorithm for polymorphic computation rules in Fig. 4.
1.2 Critical pair checking using the tool PolySOL
Based on the above answers, we have implemented these features in our tool PolySOL.
PolySOL is a tool to check conﬂuence and termination of polymorphic second-ordercomputation systems. The system PolySOL consists of about 3000 line Haskell codes,
and works on the interpreter of Glasgow Haskell Compiler (tested on GHCi, version 7.6.2). PolySOL uses the feature of quasi-quotation (i.e. [signature|..] and[rule|..] are quasi-quotations) of Template Haskell [27] with a custom parser generated by Alex (for lexer) and Happy (for paper), which realises readable notation for
signature, terms and rules. It makes the language of our formal computation rules available within a Haskell script.
PolySOL ﬁrst infers and checks the types of variables and terms in the computation
rules using a given signature. To check conﬂuence of the simply-typed λC -calculus, wedeclare the following signature in PolySOL:
siglamC = [signature|
app : Arr(a,b),a -> b ; lam : (a -> b) -> Arr(a,b)
let : a,(a -> b) -> b|]where a,b are type variables, and Arr(a,b) encodes the arrow type of the target λcalculus in PolySOL. The rule set lamC given in the beginning of this subsection is
actually a part of rule speciﬁcation written using PolySOL’s language. Using these, we
can command PolySOL to perform critical pair checking.

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

5*SOL> 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) <--2: Overlap (eta-v)-(β -v-x)--- V|-> lam(x’.H3[x’]), M’|-> z1.z2.H3[z2], V’|-> z1.z1---L: lam(x. V@x ) => V
R: (lam(x’.M’[x,x’])@V’[x]) => M’[x,V’[x]]lam(x.(lam(x’.H3[x’])@x))lam(x’.H3[x’]) <-(eta-v)-∧-(beta-v-x)-> lam(x.H3[x])---> lam(x’.H3[x’]) =E= lam(x.H3[x]) <--3: Overlap (beta-let-v)-(eta-let)--- M’|-> V, M|-> z1.z1---------------------------------L: let(V,x.M[x]) => M[V]R: let(M’,x’.x’) => M’let(V,x.x)
V <-(beta-let-v)-∧-(eta-let)-> V---> V =OK= V <--4: Overlap (eta-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]) <--5: Overlap (assoc)-(eta-let)--- M’|-> L, M|-> z1.z1--------------------------------------L: let( let(L,x.M[x]) ,y.N[y]) => let(L,x.let(M[x],y.N[y]))R: let(M’,x’.x’) => M’let(let(L,x.x),y.N[y])let(L,x19.let(x19,y19.N[y19])) <-(assoc)-∧-(eta-let)-> let(L,y.N[y])---> let(L,x19.N[x19]) =E= let(L,y.N[y]) <--6: Overlap (assoc)-(assoc)--- L|-> let(L’,x’.M’[x’]), N’|-> z1.M[z1]---------------------L: let( let(L,x.M[x]) ,y.N[y]) => let(L,x.let(M[x],y.N[y]))R: let(let(L’,x’.M’[x’]),y’.N’[y’]) => let(L’,x’.let(M’[x’],y’.N’[y’]))let(let(let(L’,x’.M’[x’]),x.M[x]),y.N[y])let(let(L’,x’.M’[x’]),x.let(M[x],y.N[y])) <-(assoc)-∧-(assoc)-> let(let(L’,x.let(M’[x],y’.M[y’])),y.N[y])-> let(L’,x.let(M’[x],y’.let(M[y’],y.N[y])))=E= let(L’,x.let(M’[x],x’.let(M[x’],y.N[y]))) <#Joinable! (Total 6 CPs)

The above PolySOL’s output corresponds to the diagrams shown in Fig. 1. The labels
L: and R: indicate the rules used in the left and right paths of a divergence, and the highlight in L-rule shows that the subterm is uniﬁable with the root of left-hand side of Rrule. For example, in the overlap 1, the subterm lam(x.M[x]) in the L-rule is uniﬁable
with the term lam(x’.(V’@x’)) in the R-rule using the uniﬁer M|-> z1.(V’@z1)
described at the immediate above. Then using this information, PolySOL generates theunderline term lam(x.(V’@x))@V which exactly corresponds to the source in the ﬁrst
divergent diagram (1:) in Fig. 1. The lines involving ∧ (indicating “divergence”) mimics
the divergence diagram and the joinablity test in text. The sign =OK= denotes syntactic
equal, and =E= denotes the α-equivalence.
Organisation. The paper is organised as follows. We ﬁrst introduce the framework of
second-order algebraic theories and computation rules in §2. We next give a type inference algorithm for polymorphic computation rules in §3. We then establish a conﬂuence criteria based on critical pair checking in §4. In §5, we prove conﬂuece of Maraist,
Odersky, and Wadler’s call-by-need λ-calculus λneed [18] using our framework. In §6,
we summarise the paper and discuss related work.

6

Makoto Hamanay:τ∈ΓΘ . Γ ` y :τ(M : σ1 , · · · , σm → τ) ∈ Θ
Θ . Γ ` ti : σi (1 ≤ i ≤ m)
Θ . Γ ` M[t1 , . . . , tm ] : τS . f : (σ1 → τ1 ), . . . , (σm → τm ) → τ ∈ Σ
ξ:S →TΘ . Γ, xi : σi ` ti : σi ξ (some i s.t. 1 ≤ i ≤ m)σm
Θ . Γ ` f σ (x1σ1 .t1 , . . . , xiσi .ti , . . . , xm.tm ) : τξHere, σ , ((σ1 → τ1 ), . . . , (σm → τm ) → τ)ξ.
Fig. 2. Typing rules of meta-terms

2

Polymorphic Computation Rules

In this section, we introduce the framework of polymorphic second-order computation
rules. It gives a formal uniﬁed framework to provide syntax, types, and computation forvarious simply-typed computational structure. It is a simpiﬁed framework of generalpolymorphic framework [11, 4] of second-order abstract syntax with metavariables [7]and its rewriting system [8, 9, 10] with molecular types [12]. The present framework introduces type variables into types and the feature of instance validation for instantiationof axioms. The polymorphism in this framework is essentially ML polymorphism, i.e.,
predicative and only universally quantiﬁed at the outermost and has type constructors
on types.
Notation 1. We use the notation A for a sequence A1 , · · · , An , and |A| for its length. The
notation s[u] p means replacing the position p of s at with u, and s| p means selecting a
subterm of the position p. We use the abbreviations “lhs” and “rhs” to mean left-handside and right-hand side, respectively.
Types. We assume that A is a set of atomic types (e.g. Bool, Nat, etc.), and a set V oftype variables (written as s, t, · · · ). We also assume a set of type constructors together
with arities n ∈ N, n ≥ 1. The sets of “0-order types” T0 and (at most ﬁrst-order) types
T are generated by the following rules:b∈Ab ∈ T0s∈Vs ∈ T0τ1 , . . . , τn ∈ T0 T n-ary type constructor
T (τ1 , . . . , τn ) ∈ T0

σ1 , . . . , σ n , τ ∈ T0
σ1 , . . . , σ n → τ ∈ T

We call σ → τ with |σ| > 0 a function type. We usually write types as σ, τ, . . .. Asequence of types may be empty in the above deﬁnition. The empty sequence is denotedby (), which may be omitted, e.g., () → τ, or simply τ. For example, Bool is an atomic
type, List(1) is a type constructor, and Bool → List(Bool) is a type.
Terms. A signature Σ is a set of function symbols of the form
t1 , . . . , tn . f : (σ1 → τ1 ), . . . , (σm → τm ) → τ
where (σ1 → τ1 ), . . . , (σm → τm ), τ ∈ T and type variables t1 , . . . , tn may occur inthese types. Any function symbol is of up to second-order type. A metavariable is aPolymorphic Rewrite Rules: Conﬂuence, Type Inference, and Instance Validation

7

variable of (at most) ﬁrst-order function type, declared as M : σ → τ (written as
capital letters M, N, K, . . .). A variable (of a 0-order type) is written usually x, y, . . .,and sometimes written xτ when it is of type τ. The raw syntax is given as follows.
- 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 ], called meta-application, means that when we instantiate
M : a → b with a meta-term s, free variables of s (which are of types a) are replacedwith meta-terms t1 , . . . , tn (cf. Def. 2). We may write x1 , . . . , xn . t for x1 . · · · .xn . t, andwe assume ordinary α-equivalence for bound variables. An equational theory is a set ofproved equations deduced from a set of axioms. A metavariable context Θ is a sequenceof (metavariable:type)-pairs, and a context Γ is a sequence of (variable:type in T1 )-pairs.
A judgment is of the form Θ . Γ ` t : b. A type substitution ρ : S → T is a mappingthat assigns a type σ ∈ T to each type variable s in S . We write τ ρ (resp. t ρ) to be
the one obtained from a type τ (resp. a meta-term t) by replacing each type variable in τ
(resp. t) with a type using the type substitution ρ : S → T . A meta-term t is well-typed
by the typing rules Fig. 2. Note that in a well-typed function term, a function symbol isannotated by its type asσmf σ (x1σ1 .t1 , . . . , xiσi .ti , . . . , xm
.tm )where f has the polymorphic type σ , ((σ1 → τ1 ), . . . , (σm → τm ) → τ)ξ. The
type annotation is important in conﬂuence checking of polymorphic rules. The notationt {x1 7→ s1 , . . . , xn 7→ sn } denotes ordinary capture avoiding substitution that replaces
the variables with terms s1 , . . . , sn .
Deﬁnition 2. (Substitution of meta-terms for metavariables [7, 5, 6])
Let ni = |τi | and τi = τ1i , . . . , τni i . SupposeΘ . Γ0 , xi1 : τ1i , . . . , xini : τni i ` si : σi

(1 ≤ i ≤ k),Θ, M1 : τ1 → σ1 , . . . , Mk : τk → σk . Γ ` e : τThen the substituted meta-term Θ . Γ, Γ0 ` e [ M 7→ x.s ] : τ is deﬁned byx [ M 7→ x.s ] , x
Mi [t1 , . . . , tni ] [ M 7→ x.s ] , si {xi1 7→ t1 [ M 7→ x.s ], . . . , xini 7→ tni [ M 7→ x.s ]}f ξ (y1 .t1 , . . . , ym .tm ) [ M 7→ x.s ] , f ξ (y1 .t1 [ M 7→ x.s ], . . . , ym .tm [ M 7→ x.s ])where [ M 7→ x.s ] denotes a substitution for metavariables [M1 7→ x1 .s1 , . . .], Mk 7→
xk .sk ].
For meta-terms Θ . Γ ` ` : τ and Θ . Γ ` r : τ, a polymorphic second-ordercomputation rule (or simply rule) is of the form Θ . Γ ` ` ⇒ r : τ satisfying(i) ` is a higher-order pattern [20], i.e., a meta-term in which every occurrence of metaapplication in ` is of the form M[x1 , . . . , xn ], where x1 , . . . , xn are distinct boundvariables.
(ii) All metavariables in r appear in `.

8

Makoto Hamana

S is the set of all type variables in τi , σi , τ
ξ:S →TΘ . Γ0 , xi : τi ` si : σi ξ (1 ≤ i ≤ k)valid [ M 7→ x.s ](M1 : (τ1 → σ1 ), . . . , Mk : (τk → σk ) . Γ ` ` ⇒ r : τ) ∈ C(RuleSub)(Fun)

Θ . Γ, Γ0 ` `ξ [ M 7→ x.s ] ⇒C rξ [ M 7→ x.s ] : τξS . f : (σ1 → τ1 ), . . . , (σm → τm ) → τ ∈ Σ
ξ:S →TΘ . Γ, xi : σi ` ti ⇒C ti0 : σi ξ (some i s.t. 1 ≤ i ≤ m)σmσm
Θ . Γ ` f σ (x1σ1 .t1 , . . . , xiσi .ti , . . . , xm.tm ) ⇒C f σ (x1σ1 .t1 , . . . , xiσi .ti0 , . . . , xm.tm ) : τξHere, σ , ((σ1 → τ1 ), . . . , (σm → τm ) → τ)ξ.
Fig. 3. Polymorphic second-order computation (one-step)

Deﬁnition 3. An instance validation is an arbitrary predicate valid that takes a substitution [ M 7→ x.s ] for metavariables and returns true or false. In this paper, we use thefollowing various instance validations (but not limited to these).
def• Any: valid θ ⇔ always true, i.e. any substitution is valid.
def• Injectivity: valid θ ⇔ θ is an injective substitution (i.e. diﬀerent metavariables
must map to diﬀerent meta-terms).
• Values/non-values: valid [M1 7→ x1 .s1 , . . . , Mn 7→ xn .sn ]def⇔ ((Mi ≡ V ⇒ si is a value) & (Mi ≡ P ⇒ si is a non-value)) for all i = 1, . . . , n.
Here, the notation “Mi ≡ V” means that the metavariable Mi ’s letter is “V”. The
deﬁnitions of values and non-values should be given separately. For the case of
λC -calculus, we take the deﬁnition (1) for values and non-values in §1.1.
A (polymorphic second-order) computation system is a triple (Σ, C, valid) consisting of a signature Σ, a set C of rules, and an instance validation valid. We write s ⇒C t
to be one-step computation using (Σ, C, valid) obtained by the inference system given
in Fig. 3. The (RuleSub) instantiates a polymorphic computation rule ` ⇒ r in C by
substitution [ M 7→ x.s ] of meta-terms for metavariables and substitution ξ on types,
where the predicate valid checks whether [ M 7→ x.s ] is applicable. The (Fun) meansthat the computation step is closed under polymorphic function symbol contexts.
Example 4. (Decidable equality) The injectivity validation in Def. 3 is useful in formulating a system involving the notion of “names”, such as π-calculus. We deﬁne thesignature Σ by
. eq : Name, Name → Booland the rules by
(eq1)
(eq0)

. a,b,c : Name

. false, true : BoolX : Name. ` eq(X, X) ⇒ true : Bool
X, Y : Name . ` eq(X, Y) ⇒ false : Bool

We set the predicate valid to be Injectivity. Then we have expected computation, suchas eq(a,b) ⇒C false, eq(b,b) ⇒C true. Without the instance validation, the rules

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

W(Σ, x)W(Σ, x.t)W(Σ, f (t))

W(Σ, M[t])9= if x : τ appears in Σ then ([], . xτ : τ) else error= let a = freshVar(θ0 , Θ . t0 : τ0 ) = W({x : a} ∪ Σ, t)in (θ0 , Θ . xa .t0 : a → τ0 )= if f : d → c appears in Σ thenlet n = newNum in(d0 → c0 ) = attach the index n to all type vars in (d → c)(θ, Θ, u, a) = foldr (Witer Σ) ([], [], [], []) tb = freshVarθ0 = unify((a → b)θ, d0 → c0 )in (θ0 ◦ θ, { fn : (d0 → c0 )} ∪ Θ . fn (u) : b)else error= let (θ, Θ, u, a) = foldr (Witer Σ) ([], [], [], []) tb = freshVarin (θ, {M : a → b} ∪ Θ . M[u] : b)

Witer Σ (t, (θ0 , Θ0 , u, τ)) = let (θ, Θ . u : τ) = W(Σ, t)in (θ ◦ θ0 , Θ ∪ Θ0 , (u, u), (τ, τ))
mkMatch(Θ)= {(σ, τ) | (M : σ) ∈ Θ, (M : τ) ∈ Θ, σ , τ}infer(Σ, t)= let (θ, Θ . u : τ) = W(Σ, t)
θ0 = unify(mkMatch(Θθ)) ◦ θin Θ θ0 . u θ0 : τ θ0
= infer({rule : s, s → t} ∪ Σ, rule(s, t))infer(Σ, s ⇒ t)

• freshVar returns a new type variable• newNum returns a new number (or by counting up the stored number)• foldr is the usual “foldr” function for the sequence of terms (regarded as a list) torepeatedly apply the functionm W by the function Witer• unify returns the most general unifer of the pairs of types.
• “[]” denotes the empty sequence or substitution.
Fig. 4. Type inference algorithm

become meaningless because they admits an non-injective substitution {X 7→ a, Y 7→ a},which entails eq(a,a) ⇒C false.

3Type Inference for Polymorphic Computation Rules

We have formulated that polymorphic computation rules were explicitly typed as Example 4. But when we give an implementation of conﬂuence/termination checker, toinsist that the user writes fully-annotated type and context information for computation
rules is not a good system design. Hence we give a type inference algorithm. In the caseof λC -calculus, the user only provides the signature siglamC and “plain” rules lamC

10

Makoto Hamanain §1.1. The type inference algorithm infers the missing context and type annotations(highlights) as:
M : s → t, N : s . ` app

Arr(s, t), s → t(s → t) → Arr(s, t)( lam(x s . M[x]), N ) ⇒ M[N] : t

These annotations are important for checking conﬂuence of polymorphic rules in computing overlapping between rules.
Algorithm. Our algorithm is given in Fig. 4, which is a modiﬁcation of Damas-Milner
type inference algorithm W [3]. It has several modiﬁcations to cope with the languageof meta-terms and to return enough type information for conﬂuence checking. The algorithm takes a signature Σ and an un-annotated meta-term t. A sub-function W returns(θ, Θ . u : τ), which is a pair of type substitution θ and an inferred judgment. The
types in it are still need to be uniﬁed. The context Θ may contain uniﬁable declarations,such as M : σ and M : τ with σ , τ, and these σ and τ should be uniﬁed. The mainfunction infer(Σ, t) does it, and returns the form
Θ . t0 : τ.
The meta-term t0 is a renamed t, where every function symbol f in the original t now
has a unique index as fn , and Θ is the set of inferred type declarations for fn ’s and all
the metavariables occurring in t0 . Similarly, for a given plain rule s ⇒ t, the function
infer(Σ, s ⇒ t) returns Θ . s0 ⇒ t0 : τ, where Θ is an inferred context and corresponding
renamed terms s0 , t0 as the sole term case. This is realised as inferring types for a metaterm to implement a rule using the new binary function symbol rule (see the deﬁnitionof infer(Σ, s ⇒ t)).
We denote by | t | a meta-term obtained from t by erasing all type annotations in
the variables and the function symbols of t. We use the usual notion of “more general”
relation on substitutions, denoted by τ0 ≥ τ, if there exists a substitution σ such thatσ ◦ τ0 = τ.
Theorem 5. (Soundness) If infer(Σ, t) = (Θ . t0 : τ), then there exists Γ such thatΘ . Γ ` t0 : τ .
Theorem 6. (Completeness) If Θ . Γ ` t : τ holds and infer(Σ, | t |) = (Θ0 . t0 : τ0 ),then τ0 ≥ τ and• If M : σ ∈ Θ then, there exists M : σ0 ∈ Θ0 such that σ0 ≥ σ• If f σ→τ occurs in t, then there exists fn : σ0 → τ0 ∈ Θ0 such that fn occurs in t0 at
the same position as t, and σ0 → τ0 ≥ σ → τ.
The reason why our algorithm attaches an index n to each occurence of a function
symbol f as “ fn ” is to distinguish diﬀerent occurrences of the same f in a term, and tocorrectly infer the type of each of them (see Prob. 2 in §1.1). If we have infer(Σ, t) =(Θ . t0 : τ), then we can fully annotate types for the plain term t. We can pick the typeof each function symbol in t by ﬁnding fn : σ0 → τ0 ∈ Θ, which means that this f has
the inferred type σ0 → τ0 .

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

4

11

Conﬂuence of Polymorphic Computation Systems

In this section, we establish a conﬂuence criterion of polymorphic computation systems
based on critical pair checking. For a computation system C, we regard “ ⇒C ” deﬁned
by Fig. 3 as a binary relation on well-typed terms. Moreover, we write ⇒∗C for thereﬂexive transitive closure, ⇒+C for the transitive closure, and ⇐C for the converse of⇒C , respectively. We say:
1. a, b ∈ A are joinable, written a ↓ b, if ∃c ∈ A. a ⇒∗C c & b ⇒∗C c.
2. ⇒C is conﬂuent if ∀a, b ∈ A. a ⇒∗C b & a ⇒∗C c implies b ↓ c.
3. ⇒C is locally conﬂuent if ∀a, b ∈ A. a ⇒C b & a ⇒C c implies b ↓ c .
4. ⇒C is strongly normalising (SN) if ∀a ∈ A, there is no inﬁnite sequence a ⇒C
a1 ⇒C a2 ⇒C · · · .
We call a meta-term linear if no metavariable occurs more than once, and C is left-linear
if for every ` ⇒ r in C, ` is linear.
Notion of uniﬁer between two polymorphic meta-terms. To compute critical pairs,
we need to compute overlapping between rules using second-order uniﬁcation. Ordinary uniﬁer between terms s and t is a substitution θ of terms for variables that makessθ = tθ. In case of polymorphic second-order algebraic theory, we should also take into
account of types. For example, what should be a uniﬁer between the following terms?
λ(bool→t)→Arr(bool,t) (xbool .M[x]) = λ(v→int)→Arr(v,int) (xv .gv→int (x))?

Here t, v are type variables. These terms are uniﬁable by a substitution of meta-terms
θ : M 7→ xbool .gbool→int (x) together with a type substitution ξ : v 7→ bool, t 7→ int.
Therefore, we deﬁne:
Deﬁnition 7. A uniﬁer between meta-terms s, t is a pair (θ, ξ) such that s ξ θ = t ξ θ,
where ξ is a substition of types for type variables, and θ is a substition of metaterms formetavariables.
Critical pairs of polymorphic computation systems. We now formulate the notionof critical pairs for our polymorphic case. We ﬁrst recall basic notions. A position p isa ﬁnite sequence of natural numbers. The empty sequence ε is the root position. Givena meta-term t, t| p denotes a subterm of t at a position p.Suppose a computation system
C is given. We say two rules l1 ⇒ r1 , l2 ⇒ r2 in C are variant if l1 ⇒ r1 is obtained byinjectively renaming variables and metavariables of l2 ⇒ r2 . We say that a position p
in a term t is a metavariable position if t| p is a metavariable or meta-application.
Deﬁnition 8. An overlap between two rules l1 ⇒ r1 and l2 ⇒ r2 of a computation system (Σ, C, valid) is a tuple hl1 ⇒ r1 , p, l2 ⇒ r2 , θ, ξi satisfying the following properties:••••l1 ⇒ r1 , l2 ⇒ r2 are variants of rules in C without common (meta)variables.
p is a non-metavariable position of l1 .
If p is the root position, l1 ⇒ r1 and l2 ⇒ r2 are not variants.
(θ, ξ) is a uniﬁer between l1| p and l2 such that valid(θ) holds.

12

Makoto Hamana

The component θ in an overlap is intended to be the output of the pattern uniﬁcation
algorithm [20]. An overlap represents an overlapping situation of computation, meaningthat the term t is rewritten to the two diﬀerent ways. We deﬁne overlap(l1 ⇒ r1 , l2 ⇒r2 ) , {all possible overlaps between l1 ⇒ r1 and l2 ⇒ r2 }. We collect all the overlaps∪
in C by O , {overlap(l1 ⇒ r1 , l2 ⇒ r2 ) | l1 ⇒ r1 , l2 ⇒ r2 ∈ C}.
Deﬁnition 9. The critical pair (CP) generated from an overlap h`1 ⇒ r1 , p, `2 ⇒r2 , θ, ξi is a triple hr10 , t, r20 i where t = `1 ξθ and t ⇒C r10 which rewrites the root
position of t using `1 ⇒ r1 , and t ⇒C r20 which rewrites the position p of t using`2 ⇒ r2 .
Then, we obtain the critical pairs of C by collecting all the critical pairs generated
from overlaps in O.
Proposition 10. Let (Σ, C, valid) be a polymorphic second-order computation system.
Suppose C is left-linear. If for every critical pair ht, u, t0 i of (Σ, C, valid), we have t ↓ t0 ,then ⇒C is locally conﬂuent.
Theorem 11. Let (Σ, C, valid) be a polymorphic second-order algebraic theory. Assume that C is left-linear and strongly normalising. If for every critical pair ht, u, t0 iof (Σ, C, valid), we have t ↓ t0 , then ⇒C is conﬂuent.
Proof. By Prop. 10 and Newman’s lemma.

5

Example: Conﬂuence of the Call-by-Need λ-Calculus

We examine conﬂuece of Maraist, Odersky, and Wadler’s call-by-need λ-calculus λneed[18]. We consider the simply-typed version of it. The signature is:
sigNeed = [signature|lam : (a->b) -> Arr(a,b); app : Arr(a,b),a -> b; let : a,(a->b) -> b |]which consists of the function symbol lam for λ-abstraction, app (also written as an inﬁx operator @ below) for application, and let-construct. We represent the arrow typesof the “object-level” λneed -calculus by the binary type constructor Arr, and use the function types a->b of the “meta-level” polymorphic second-order computation system torepresent binders, where a,b are type variables. The λneed has ﬁve rules, which arestraightforwardly deﬁned in PolySOL as:
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])) |]We also impose the distinction of values and non-values as in the λC -calculus. Here V
is a metavariable for values, and M,N,C,L are metavariables for all terms. We choose theinstance validation valid to be Values/non-values in Def. 3. We can tell it to PolySOL
by writing the suﬃx “-v” in the labels (rV-v),(rC-v). We command PolySOL toperform critical pair checking.

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

13*PolySOL> cri lmdNeed sigNeed
1: Overlap (rG)-(rA)--- M|-> let(L’,x’.M’[x’]), N’|-> z1.N------------------------------L: let(M,x.N) => N
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.N)
N <-(rG)-∧-(rA)-> let(L’,xd2.let(M’[xd2],yd2.N))---> N =OK= N <--2: Overlap (rC-v)-(rG)--- M’|-> V, M|-> z1.N’-------------------------------------------L: let(V,x.M[x]) @N => let(V,x.(M[x]@N))
R: let(M’,x’.N’) => N’(let(V,x.N’)@N)
let(V,x5.(N’@N)) <-(rC-v)-∧-(rG)-> (N’@N)---> (N’@N) =OK= (N’@N) <--3: Overlap (rC-v)-(rV-v)--- V’|-> V, C’|-> z1.M[z1]-------------------------------------L: let(V,x.M[x]) @N => let(V,x.(M[x]@N))
R: let(V’,x’.C’[x’]) => C’[V’](let(V,x.M[x])@N)
let(V,x7.(M[x7]@N)) <-(rC-v)-∧-(rV-v)-> (M[V]@N)---> (M[V]@N) =OK= (M[V]@N) <--4: Overlap (rA)-(rG)--- M’|-> L, M|-> z1.N’---------------------------------------------L: let( let(L,x.M[x]) ,y.N[y]) => let(L,x.let(M[x],y.N[y]))R: let(M’,x’.N’) => N’let(let(L,x.N’),y.N[y])let(L,x10.let(N’,y10.N[y10])) <-(rA)-∧-(rG)-> let(N’,y.N[y])---> let(N’,y10.N[y10]) =E= let(N’,y.N[y]) <--5: Overlap (rA)-(rA)--- L|-> let(L’,x’.M’[x’]), N’|-> z1.M[z1]--------------------------L: let( let(L,x.M[x]) ,y.N[y]) => let(L,x.let(M[x],y.N[y]))R: let(let(L’,x’.M’[x’]),y’.N’[y’]) => let(L’,x’.let(M’[x’],y’.N’[y’]))let(let(let(L’,x’.M’[x’]),x.M[x]),y.N[y])let(let(L’,x’.M’[x’]),x.let(M[x],y.N[y])) <-(rA)-∧-(rA)-> let(let(L’,x’.let(M’[x’],y’.M[y’])),y.N[y])---> let(L’,x.let(M’[x],y.let(M[y],y.N[y])))=E= let(L’,x’.let(M’[x’],x.let(M[x],y.N[y]))) <--#Joinable! (Total 5 CPs)

PolySOL reports that there are 5 critical pairs, and all are successfully joinable. Thisshows local conﬂuence. Strong normalisation of λneed can be shown by a translation as
the treatment of λC in [24]. Hence we conclude that λneed is conﬂuent. In [18], conﬂuence of untyped λneed has been established by a diﬀerent proof method, i.e., analysis
of developments steps in the λ-calculus [2]. This method is somewhat speciﬁc to thecase of λ-calculus. In contrast to it, our approach is general rewriting theoretic, and not
speciﬁc to variants of λ-calculus, i.e., based on critical pair checking of computation
rules.

6

Summary and Related Work

6.1

Summary

We have presented a new framework of polymorphic computation rules having predicates to restrict their instances. It was shown to be suitable for formulating and analysing
fundamental calculi of programming languages. We have given a type inference algorithm and a criteria to check conﬂuence property of polymorphic rules. These havegiven a handy method to prove conﬂuence of second-order computation rules. We havedemonstrated eﬀectiveness of our methodology by examining sample program calculi
using our framework.

14

Makoto Hamana

6.2 Related Work
Nipkow has studied critical pairs for conﬂuence of higher-order rewrite systems[23],[19]. The rewrite rule format there was rules on simply-typed λ-terms modulo
βη-equivalence, and there are no polymorphic types nor instance validation. Therefore,
none of our examples (λC ,λneed , and decidable equality) and the conﬂuence shown in
the present paper can be directly formulated and checked in Nipkow’s framework.
There are systems of automatic checking of conﬂuence of Nipkow’s higher-orderrule format, such as ACPH [25] and CSIˆho [22]. Because these are based on Nipkow’s
format, these tool do not have the features of polymorphic types nor instance validation.
Hence, all of our examples are beyond the scope of the existing conﬂuence checking
systems. In this respect, to the best of the author’s knowledge, our system is the ﬁrst
automatic tool that can check conﬂuence of the call-by-value variants of the λ-calculus
directly, as shown in the paper.
A framework of polymorphic higher-order rewrite rules was given [14, 15], andour framework is similar but there are several diﬀerences in the foundations, e.g., ourframework is based on (polymorphic) second-order algebraic theories [6, 4], while theiris based on a polymorphic λ-calculus. The main purpose of [14, 15] was to establish termination criterion of higher-order rewrite rules. The issue of conﬂuence of polymorphic
rules has remain untouched. To the best of the author’s knowledge, the present paper
is probably the ﬁrst study of conﬂuence of general kind of polymorphic second-orderrewrite rules (N.B. this is not about the polymorphic λ-calculus).
We gave a type inference algorithm of polymorphic computation rules, which has
not been given in the context of rewriting theory (while it may be standard in the context
of the theory of programming languages). Lack of a suitable type inference algorithm inthe theory of rewriting has aﬀected to the existing higher-order conﬂuence tools such as
CSIˆho and ACPH. These tools force the user to write more detailed type informationin rewrite rule speciﬁcations than PolySOL. The user need to declear all free and boundvariables with their types used in the rules. PolySOL’s rule speciﬁcation is simpler due
to the type inference. Our algorithm may also be beneﬁcial to other tools to improve
this situation.
In [12], the present author developed a simply-typed framework of second-orderequational logic and computation rules, and gave a tool SOL for checking methods oftermination conﬂuence. It lacked proper polymorphism and instance validation, hence
the examples considered in the present paper could not be handled. Note that Plotkin’s
call-by-value λ-calculus could be formulated in [12] by explicitly modifying the rulesby meta-programming like method to reﬂect value variables. But this approach works
only for small calculi, such as the call-by-value λ-calculus, and for larger calculi, suchas λC and λneed , the number of overlaps explodes and we cannot hope to manage it.
In [4], we gave a general framework of multiversal polymorphic algebraic theories
and their algebraic models. It admits multiple type universes and higher-kinded polymorphic types, hence it is richer than the present setting. The model theory encompasses
the present simpler framework. But in [4], we did not develop neither polymorphic computation rules, conﬂuence, nor instance validation.

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

15

Acknowledgments. I am grateful to Masahito Hasegawa for his question on how tocheck conﬂuence of Moggi’s computational λ-calculus by my previous tool SOL. It
opened my eyes to the necessity of proper treatment of call-by-value calculi and led me
to the notion of instance validation developped in this paper.

References[1] F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
[2] H.P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North Holland, 1984.
[3] L. Damas and R. Milner. Principal type-schemes for functional programs. In Proc.
POPL’82, pages 207–212, 1982.
[4] M. Fiore and M. Hamana. Multiversal polymorphic algebraic theories: Syntax, semantics, translations, and equational logic. In 28th Annual ACM/IEEE Symposium on Logic in
Computer Science, LICS 2013, pages 520–529, 2013.
[5] M. Fiore and C.-K. Hur. Second-order equational logic. In Proc. of CSL’10, LNCS 6247,
pages 320–335, 2010.
[6] M. Fiore and O. Mahmoud. Second-order algebraic theories. In Proc. of MFCS’10, LNCS
6281, pages 368–380, 2010.
[7] M. Hamana. Free Σ-monoids: A higher-order syntax with metavariables. In Proc. of
APLAS’04, LNCS 3302, pages 348–363, 2004.
[8] M. Hamana. Universal algebra for termination of higher-order rewriting. In Proc. of
RTA’05, LNCS 3467, pages 135–149, 2005.
[9] M. Hamana. Higher-order semantic labelling for inductive datatype systems. In Proc. of
PPDP’07, pages 97–108. ACM Press, 2007.
[10] M. Hamana. Semantic labelling for proving termination of combinatory reduction systems.
In Proc. WFLP’09, LNCS 5979, pages 62–78, 2010.
[11] M. Hamana. Polymorphic abstract syntax via Grothendieck construction. In FoSSaCS’11,
LNCS3467, pages 381–395, 2011.
[12] M. Hamana. How to prove your calculus is decidable: Practical applications of secondorder algebraic theories and computation. Proceedings of the ACM on Programming Languages, 1(22):1–28, September 2017.
[13] G. Huet. Conﬂuent reductions: Abstract properties and applications to term rewriting systems. Journal of ACM, 27(4):797–821, 1980.
[14] J.-P. Jouannaud and A. Rubio. Polymorphic higher-order recursive path orderings. Journalof ACM, 54(1):2:1–2:48, 2007.
[15] J.-P. Jouannaud and A. Rubio. Normal higher-order termination. ACM Trans. Comput.
Log., 16(2):13:1–13:38, 2015.
[16] D. Knuth and P. Bendix. Simple word problems in universal algebras. In Computational
Problem in abstract algebra, pages 263–297. Pergamon Press, Oxford, 1970.
[17] S. Lindley and I. Stark. Reducibility and >>-lifting for computation types. In Proc. of
TLCA’05, pages 262–277, 2005.
[18] J. Maraist, M. Odersky, and P. Wadler. The call-by-need lambda calculus. J. Funct. Program., 8(3):275–317, 1998.
[19] R. Mayr and T. Nipkow. Higher-order rewrite systems and their conﬂuence. Theor. Comput.
Sci., 192(1):3–29, 1998.
[20] D. Miller. A logic programming language with lambda-abstraction, function variables, andsimple uniﬁcation. Journal of Logic and Computation, 1(4):497–536, 1991.
[21] E. Moggi. Computational lambda-calculus and monads. LFCS ECS-LFCS-88-66, University of Edinburgh, 1988.

16

Makoto Hamana[22] J. Nagele, B. Felgenhauer, and A. Middeldorp. CSI: New evidence – a progress report. In
Proc. of CADE’17, LNCS (LNAI) 10395, pages 385–397, 2017.
[23] T. Nipkow. Higher-order critical pairs. In Proc. 6th IEEE Symp. Logic in Computer Science,
pages 342–349, 1991.
[24] Y. Ohta and M. Hasegawa. A terminating and conﬂuent linear lambda calculus. In Proc. of
RTA’06, pages 166–180, 2006.
[25] K. Onozawa, K. Kikuchi, T. Aoto, and Y. Toyama. ACPH: System description. In 6th
Conﬂuence Competition (CoCo 2017), 2017.
[26] A. Sabry and P. Wadler. A reﬂection on call-by-value. ACM Trans. Program. Lang. Syst.,
19(6):916–941, 1997.
[27] T. Sheard and S. Peyton Jones. Template metaprogramming for Haskell. In Proc. Haskell
Workshop 2002, 2002.
[28] S. Staton. An algebraic presentation of predicate logic. In Proc. of FOSSACS 201, pages
401–417, 2013.
[29] S. Staton. Instances of computational eﬀects: An algebraic perspective. In Proc. of
LICS’13, page 519, 2013.
[30] S. Staton. Algebraic eﬀects, linearity, and quantum programming languages. In Proc. of
POPL’15, pages 395–406, 2015.