Science of Computer Programming 187 (2020) 102322

Contents lists available at ScienceDirect

Science of Computer Programming
www.elsevier.com/locate/scico

Polymorphic computation systems: Theory and practice of
conﬂuence with call-by-value
Makoto Hamana a,∗ , Tatsuya Abe b , Kentaro Kikuchi cabc

Department of Computer Science, Gunma University, JapanSTAIR Lab, Chiba Institute of Technology, Japan
Research Institute of Electrical Communication, Tohoku University, Japana r t i c l e

i n f oa b s t r a c t

Article history:
Received 21 November 2018
Received in revised form 7 September 2019
Accepted 19 September 2019
Available online 17 October 2019
Keywords:
Polymorphism
λ-calculus
Type inference
Second-order algebraic theory
Conﬂuence

We present a new framework of polymorphic computation rules that can accommodate a
distinction between values and non-values. It is suitable for analysing fundamental calculi
of programming languages. We develop a type inference algorithm and new criteria tocheck the conﬂuence property. These techniques are then implemented in our automatedconﬂuence checking tool PolySOL. Its effectiveness is demonstrated through examination ofvarious calculi, including the call-by-need lambda-calculus, Moggi’s computational lambdacalculus, and skew-monoidal categories.
© 2019 Elsevier B.V. All rights reserved.

1. Introduction
1.1. How to formalise a concrete calculus
Fundamental calculi of programming languages are often formulated as simply-typed computation rules. Describing sucha simply-typed system requires a schematic type notation that is best formulated in a polymorphically typed framework. To
illustrate this situation, consider the simply-typed λ-calculus as a sample calculus:(β)

  (λxσ . M ) N ⇒ M [x := N ] : τAn important point is that neither σ nor τ is a ﬁxed type, but each is a schema of types. Therefore, (β) actually describes
a family of actual computation rules. It represents various instances of rules by varying σ and τ , such as the following.

(βbool,int )(βint→int,bool )  (λxbool . M ) N⇒ M [x := N ] : int  (λxint→int . M ) N ⇒ M [x := N ] : bool

From the viewpoint of meta-theory, as in a mechanised formalisation of mathematics, the (β)-rule should be formulated
in a polymorphically 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.

* Corresponding author.

E-mail addresses: hamana@cs.gunma-u.ac.jp (M. Hamana), abet@stair.center (T. Abe), kentaro.kikuchi@riec.tohoku.ac.jp (K. Kikuchi).

https://doi.org/10.1016/j.scico.2019.102322
0167-6423/© 2019 Elsevier B.V. All rights reserved.

2

M. Hamana et al. / Science of Computer Programming 187 (2020) 102322

We were aware of this diﬃculty. Our earlier study [1] 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 means of instantiating types by replacing type variables
with other types. Therefore, instantiation of (β) to (βbool,int )(βint→int,bool ) described above was unobtainable. For that reason, no conﬂuence of instances of polymorphic computation rules is obtained automatically. Further manual meta-theoretic
analysis is necessary.
1.2. A new framework of polymorphic computation rules with values and non-values distinction
To resolve these issues, we present an extended framework for polymorphic computation rules herein. To make theframework applicable to describing and analysing fundamental calculi of programming languages, we also introduce a distinction between values and non-values in the framework.
This framework is polymorphic and a computational reﬁnement of second-order algebraic theories by Fiore et al. [2,3]. Second-order algebraic theories have been shown to be a useful framework that models various important notions ofprogramming languages such as logic programming [4], algebraic effects [5], and quantum computation [6]. The present
polymorphic framework also has applications in these ﬁelds.
1.3. Differences from ordinary untyped rewriting systems
This new framework is not merely an instance of ordinary untyped rewriting systems [7–9]. One cannot simply apply
existing theory to the new typed framework. The framework introduces new features: polymorphic types and values/nonvalues distinctions in the rule format. We provide suitable adaptation and extension of the theory and techniques ofrewriting.
1.3.1. Polymorphic typed rules and their conﬂuence
The following examples underscore that the conﬂuence property in the present setting differs from that in the untyped
setting. Let ck : a → bool be a polymorphic function symbol, where a is a type variable. Moreover, atomic types int, char, booland constants true, false are assumed. The following rules use different instances of the polymorphic function symbol ck.

(1)
(2)

x : int  ckint→bool (x)x : char  ckchar→bool (x)⇒ true : bool
⇒ false : bool

These formulate the function ck as a checking function of whether the type of the argument is of int or not. These are
written in our formal framework we introduce into §2. The system is conﬂuent because there is no overlapping and it isterminating.
However, the corresponding untyped rules are non-conﬂuent. Forgetting types, we have the following rules as

(1)
(2)

ck(x)
ck(x)

⇒ true⇒ falsewhere ck is a unary untyped function symbol. As one might expect, the untyped system is not conﬂuent because ck(x) is
rewritten to two normal forms: true and false. This result shows that the types are important and that they affect the notionof overlap between rules, which is a core notion of critical pair checking.
1.3.2. Values and non-values
The notion of values is important in programming languages. Not only call-by-value programming languages such as ML,
but functional programming languages having distinction of pure functions and effectful computations, such as Haskell, havethe notion of (pure) values.
Plotkin’s call-by-value λ-calculus [10] is the most fundamental λ-calculus having the notion of values. This λ-calculus isdeﬁned by a version of β-reduction law as(β)

  (λxσ . M ) V⇒ M [x := V ] : τ

where V denotes a value that is either a variable or an abstraction

ValuesV ::= y | λ w . M

Therefore, the metavariable V is only instantiated by a term in the particular subclass of terms, called values. The ordinary theory of term rewriting does not allow such syntactic restrictions on the form of terms. Because the restriction ofterms reﬂects the notion of substitutions of terms for variables, we cannot apply the ordinary theory directly to investigate
conﬂuence of call-by-value calculi. We will introduce the following new notions for it:M. Hamana et al. / Science of Computer Programming 187 (2020) 102322

3

1. Overlaps for rules having metavariables for values and non-values (Deﬁnition 4.3)
2. Call-by-value joinability (Deﬁnition 4.5)
3. Meta-conﬂuence and object conﬂuence (§4.5)
The ﬁrst two notions are necessary to establish conﬂuence in the call-by-value setting. The third notion is important forestablishing conﬂuence of object λ-calculi. Meta-conﬂuence is a conﬂuence property at the meta-level, i.e., conﬂuence on“terms with metavariables”, which are wider than the terms with no metavariables. In §6, it is explained that the polymorphic computation system of Moggi’s computational λ-calculus, the λC -calculus, is not meta-conﬂuent. Nevertheless, its
object conﬂuence can be proved using the notion of call-by-value joinability.
1.4. Example 1: conﬂuence of the call-by-need λ-calculus
Examination of a sample conﬂuence problem is useful to illustrate our framework and methodology. Here we consider
Maraist, Odersky, and Wadler’s call-by-need λ-calculus λneed [11]. Its simply-typed version is explained below. The λneed
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
λneed are described as shown below:
lmdNeed = [rule|(G)
let(M, x.N)=> N
(I)lam(x.M[x]) @ N=> let(N,x.M[x])(V-v) let(V, x.C[x])=> C[V](C-v) let(V, x.M[x])@N=> let(V, x.M[x]@N)(A)
let(let(L,x.M[x]), y.N[y]) => let(L,x.let(M[x],y.N[y])) |]Descriptions “lmdNeed = [rule|” and “|]” present the beginning and end of the rule speciﬁcation in our conﬂuence
checker PolySOL. Here V is a metavariable for values. Also, M,N,C,L are metavariables for all terms.
Remark 1.1. The value metavariable V cannot be replaced with non-values. That is, V can only be replaced with variables or abstractions. This fundamental assumption is important for a formal description of a calculus having the notion ofvalues/non-values, such as the call-by-need λ-calculus and the computational λ-calculus (see §6). 2
Next, conﬂuence of the simply-typed λneed -calculus is proved. Conﬂuence (CR) is a property of the reduction relation,
stating that any two divergent computation paths are ﬁnally joinable, as shown in the panel:
M
∗

∗

CR

M1
∗

M2
∗

N

The proof requires analysis of all possible situations that admit two ways of reductions, and also to check their convergence.
In the case of λneed , careful inspection of the rules reveals that it has, in all, seven patterns of such situations, as depicted
in Fig. 1. Next it is apparent that all of these patterns are convergent. Importantly, this ﬁnite number of checks is suﬃcient
to infer that all other inﬁnite numbers of 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 [12,7], which statesthat “termination and local conﬂuence imply conﬂuence”, we infer that λneed is conﬂuent because termination (i.e. strong
normalisation) of λneed can be shown by a translation into a terminating λ-calculus, as Ohta et al. have described [13].
Therefore, we conclude that λneed is conﬂuent.
This proof method is known as Knuth and Bendix’s critical pair checking [14]. The divergent terms in Fig. 1 are designatedas critical pairs because these show critical situations that may break conﬂuence. A critical pair is obtained by an overlap
between two rules, which is computed using second-order uniﬁcation [15]. For instance, an overlap exists between the rules(V-v),(C-v) because their left-hand sides?

let(V, x.C[x]) = let(V’, x.M[x])are uniﬁable by second-order uniﬁcation with a uniﬁer θ = {V → V’, C → x.M[x]}. The instantiated term let(V’,x.M[x])@N by θ is the source of the divergence (4:) in Fig. 1, which admits reductions by the two rules (C-v),(V-v).

4

M. Hamana et al. / Science of Computer Programming 187 (2020) 102322

2: lam(x.let(let(L’,x’.M’[x’]),x.N)

1: let(V’,x.N)
(G)

N

(V-v)

=

(G)

N

(A)

N

let(L’,x.let(M’[x],y.N)

3: let(V,x.N’)@N

4: let(V’,x.M[x])@N

(C-v)

(C-v)

let(V,x.(N’@N))

(G)

N’@N

let(V’,x.(M[x]@N))let(L,x.let(N’,y.N[y]))M[V’]@N

6: let(let(V’,x.M[x]),y.N[y])5: let(let(L,x.N’),y.N[y])
(A)

(V-v)

(G)

(A)

let(N’,y.N[y])let(V’,x.let(M[x],y.N[y]))(V-v)

let(M[V’],y.N[y])7: let(let(let(L’,x’.M’[x’]),x.M[x]),y.N[y])
(A)

(A)

let(let(L’,x’.let(M’[x’],y’.M[y’])),y.N[y])let(let(L’,x’.M’[x’]),x.let(M[x],y.N[y]))∗∗·Fig. 1. Critical pairs of λneed -calculus.

Nevertheless, some diﬃculties arise. In computing the critical pairs of λneed in Fig. 1, the classical critical pair method
is not applicable. Actually, suitable extensions of the method are required. In the following herein, we list the problems,
related questions, and the answers we obtained.
Problem 1. The notion of a uniﬁer for an overlap is non-standard in the call-by-value case. For example, the left-hand sidesof (V-v) and (A) appear to be overlapped, but actually they are not. A candidate uniﬁer V → let(L,x.M[x]), C →
y.N[y] is not correct because V is a value, whereas let(L,x.M[x]) is a non-value.
Q1. What is a general deﬁnition of overlaps in the call-by-value setting?
Problem 2. Different occurrences of the same function symbol might have different types.
For example, in (A), each let has actually a different type (highlighted one) as

M : c → a, N : a → b , L : c   let a, (a → b) → b(let c, (c → a) → a( L , xc . M [x]), ya . N [ y ]) ⇒ let c, (c → b) → b( L , xc .let a, (a → b) → b( M [x], ya . N [ y ])) : b
Computing an overlap between let-terms demands adjustment of the types of let to equate them.
Q2. What should be the notion of uniﬁcation between polymorphic second-order terms?
Moreover, specifying all the type annotations as described above manually is tedious in practice. Ideally, we write a“plain” rule as (A), and expect that some system infers the type annotations automatically.
Q3. What is the type inference algorithm for polymorphic second-order computation rules?
As described in this paper, we solve these questions.
A1. We introduce a validation predicate on substitutions (Deﬁnition 2.5) to check value/non-value restrictions of the term
structures. It is used for formulating computation steps in call-by-value and overlaps between rules.
Moreover, we reformulate the notion of overlaps to compute critical pairs in call-by-value (Deﬁnition 4.3), and introduce
the notion of call-by-value joinability (Deﬁnition 4.5) of critical pairs.
A2. We formulate the notion of a uniﬁer for call-by-value polymorphic terms (Deﬁnition 4.1).
A3. We give a type inference algorithm for polymorphic computation rules in Fig. 4.

M. Hamana et al. / Science of Computer Programming 187 (2020) 102322

5

1.5. 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 checkconﬂuence and termination of polymorphic second-order computation systems. The system works on top of the interpreterof Glasgow Haskell Compiler. PolySOL uses the feature of quasi-quotation (i.e. [signature|..] and [rule|..] arequasi-quotations) of Template Haskell [16], with a custom parser which provides a 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 λneed -calculus, we declare the following signature in PolySOL:
sigNeed = [signature|lam : (a -> b) -> Arr(a,b)
let : a,(a -> b) -> b;

app : Arr(a,b),a -> b|]where a,b are type variables, and Arr(a,b) encodes the arrow type of the target λ-calculus in PolySOL. The rule set
lmdNeed given in the beginning of this section is actually a part of rule speciﬁcation written using PolySOL’s language.
Using these, we can command PolySOL to perform critical pair checking.
*SOL> criCBV lmdNeed sigNeed
1: Overlap (G)-(V-v)--- M|-> V’, C’|-> z1.N --------------------------------(G) let(M,x.N) => N(V-v) let(V’,x’.C’[x’]) => C’[V’]let(V’,x.N)
N <-(G)-∧-(V-v)-> N---> N =OK= N <--2: Overlap (G)-(A)--- M|-> let(L’,x’.M’[x’]), N’|-> z1.N -------------------(G) let(M,x.N) => N
(A) 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 <-(G)-∧-(A)-> let(L’,xd3.let(M’[xd3],yd3.N))---> N =OK= N <--3: Overlap (C-v)-(G)--- M’|-> V, M|-> z1.N’ --------------------------------(C-v) let(V,x.M[x])@N => let(V,x.(M[x]@N))(G) let(M’,x’.N’) => N’let(V,x.N’)@N
let(V,x8.(N’@N)) <-(C-v)-∧-(G)-> N’@N---> N’@N =OK= N’@N <--4: Overlap (C-v)-(V-v)--- V|-> V’, C’|-> z1.M[z1] --------------------------(C-v) let(V,x.M[x])@N => let(V,x.(M[x]@N))(V-v) let(V’,x’.C’[x’]) => C’[V’]let(V’,x.M[x])@N
let(V’,x11.(M[x11]@N)) <-(C-v)-∧-(V-v)-> M[V’]@N---> M[V’]@N =OK= M[V’]@N <--5: Overlap (A)-(G)--- M’|-> L, M|-> z1.N’ ----------------------------------(A) let(let(L,x.M[x]),y.N[y]) => let(L,x.let(M[x],y.N[y]))(G) let(M’,x’.N’) => N’let(let(L,x.N’),y.N[y])let(L,x15.let(N’,y15.N[y15])) <-(A)-∧-(G)-> let(N’,y.N[y])---> let(N’,y15.N[y15]) =E= let(N’,y.N[y]) <--6: Overlap (A)-(V-v)--- L|-> V’, C’|-> z1.M[z1] ----------------------------(A) let(let(L,x.M[x]),y.N[y]) => let(L,x.let(M[x],y.N[y]))(V-v) let(V’,x’.C’[x’]) => C’[V’]let(let(V’,x.M[x]),y.N[y])let(V’,x27.let(M[x27],y27.N[y27])) <-(A)-∧-(V-v)-> let(M[V’],y.N[y])---> let(M[V’],y27.N[y27]) =E= let(M[V’],y.N[y]) <--7: Overlap (A)-(A)--- L|-> let(L’,x’.M’[x’]), N’|-> z1.M[z1] ---------------(A) let(let(L,x.M[x]),y.N[y]) => let(L,x.let(M[x],y.N[y]))(A) 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])) <-(A)-∧-(A)-> let(let(L’,xd.let(M’[xd],yd.M[yd])),y.N[y])---> let(L’,x.let(M’[x],y4.let(M[y4],y.N[y]))) =E= let(L’,x.let(M’[x],x5.let(M[x5],y.N[y]))) <--#Joinable! (Total 7 CPs)

The above PolySOL’s output corresponds to the diagrams shown in Fig. 1. Each item shows which two rules are overlapped, a substitution for metavariables for the overlap, and the two rules. The highlight in the ﬁrst rule shows that thesubterm is uniﬁable with the root of left-hand side of the second rule.
For example, in the overlap 3:, the subterm let(V,x.M[x]) in the rule (C-v) is uniﬁable with the termlet(M’,x’.N’) in the rule (G) using the uniﬁer M’|-> V, M|-> z1.N’ described immediately above (C-v). Then
using this information, PolySOL generates the underlined term let(V,x.N’)@N which exactly corresponds to the source

6

M. Hamana et al. / Science of Computer Programming 187 (2020) 102322

in the ﬁrst divergent diagram (3:) in Fig. 1. The lines involving ∧ (indicating “divergence”) mimics the divergence diagram
and the joinability test in text. The sign =OK= denotes syntactic equality, and =E= denotes α-equivalence.
Maraist et al. has shown that conﬂuence of untyped λneed has been established by a different proof method [11], i.e.,analysis of developments steps in the λ-calculus [17]. This method is somewhat speciﬁc to the case 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 checkingof computation rules.
1.6. Contributions
This paper is the fully reworked and extended version of the conference paper [18]. Besides proofs of all results, thepresent paper establishes a theory of conﬂuence of polymorphic computation systems with value/non-value metavariables.
In addition, we provide a new example solving the coherence problem of skew-monoidal categories (§7). More precisely,
the contributions of this paper are summarised as follows.
1. We develop a new framework of polymorphic second-order computation that has predicates of “instance validations”
to reﬂect value/non-value distinctions (§2).
2. We present a type reconstruction algorithm for polymorphic second-order rules (§3).
3. We develop a theory of conﬂuence in the call-by-value setting (§4) by introducing the notion of “call-by-value joinability” of critical pairs (§4.5). To do so, we formulate meta-conﬂuence and object conﬂuence (§4.2).
4. We develop conﬂuence criteria without termination:• conﬂuence by strong closedness (§5.1)• conﬂuence by orthogonality (§5.2)• modular conﬂuence checking (§5.3)
The criterion for the ﬁrst is new, and the criteria and proofs for the second and the third are adapted from the case of(simply-typed) higher-order rewrite systems [9] to our polymorphic setting.
5. Using PolySOL, we give conﬂuence proofs of various calculi, including the call-by-need λ-calculus, Moggi’s computational λ-calculus (§6), and skew-monoidal categories (§7).
1.7. 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 criterion based on critical pair checking in the call-by-value setting in §4. We further establish conﬂuence criteria
without requiring termination in §5. In §6, we prove conﬂuence of Moggi’s computational λ-calculus using PolySOL. In §7,
we consider a further example, the coherence problem of skew-monoidal categories using PolySOL. In §8, we describe theimplementation of PolySOL. In §9, we report the results in International Conﬂuence Competition 2018, which showed theeffectiveness of PolySOL’s checking method and the new conﬂuence criteria. In §10, we summarise the paper and discuss
related work.
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 for various simply-typed computational structure. It is a polymorphic
extension of second-order rewriting systems [19–21] based on second-order abstract syntax with metavariables [2,22] withmolecular types [1]. The present framework introduces type variables into types and the feature of instance validation for instantiation of axioms for value/non-value distinction. The polymorphism in this framework is essentially ML polymorphism,i.e., predicative and universally quantiﬁed at the outermost only and has type constructors on types.
Notation 2.1. We use the notation A for a sequence A 1 , · · · , A n , and | A | for its length. We use the abbreviations “lhs” and“rhs” to mean left-hand side and right-hand side, respectively.
2.1. Types
We assume that A is a set of atomic types (e.g. Bool, Nat, etc.), and a set V of type variables (written as s, t, a, b, · · · ).
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∈A

s∈V

b ∈ T0s ∈ T0τ1 , . . . , τn ∈ T0
T n-ary type constructor
T (τ1 , . . . , τn ) ∈ T0

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

M. Hamana et al. / Science of Computer Programming 187 (2020) 102322

y:τ ∈   y :τ7

( M : σ1 , · · · , σm → τ ) ∈   t i : σi (1 ≤ i ≤ m)
   M [t 1 , . . . , tm ] : τS  f : (σ1 → τ1 ), . . . , (σm → τm ) → τ ∈ , xi : σi  t i : τi ξ (1 ≤ i ≤ m)

ξ : S →Tσσm
   f σ (xσ1 1 .t 1 , . . . , xi i .t i , . . . , xm.tm ) : τ ξHere, σ  ((σ1 → τ1 ), . . . , (σm → τm ) → τ )ξ .
Fig. 2. Typing rules of meta-terms.

We call σ → τ with |σ | > 0 a function type. We usually write types as σ , τ , . . .. A sequence of types may be empty in theabove deﬁnition. The empty sequence is denoted by (), which may be omitted, e.g., () → τ , or simply τ . For example, Boolis an atomic type, List is a unary type constructor, and Bool → List(Bool) is a type.
2.2. Terms and meta-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 , τ ∈ T0 , and type variables t1 , . . . , tn may occur in these types. As a result function
symbols have at most second-order function types. A metavariable is a 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 , . . ., andsometimes written xτ when it is of type τ . The raw syntax is given as follows.

- Terms have the formt ::= x | xσ .t | f (t 1 , . . . , tn ).
- Meta-terms extend terms to t ::= x | xσ .t | f (t 1 , . . . , tn ) | M [t 1 , . . . , tn ].
The last form M [t 1 , . . . , tn ], called meta-application, means that when we instantiate M : a → b with a meta-term s, freevariables of s (which are of types a) are replaced with meta-terms t 1 , . . . , tn (cf. Deﬁnition 2.2). We may write x1 , . . . , xn . t
for x1 . · · · .xn . t, and we assume ordinary α-equivalence for bound variables. An equational theory is a set of proved equations
deduced from a set of axioms. A metavariable context
is a sequence of (metavariable:type)-pairs, and a context  is a   t : τ . A type substitution ξ : S → T is asequence of (variable:type in T0 )-pairs. A judgment is of the form
mapping that assigns a type σ ∈ T to each type variable s in S. We write τ ξ (resp. t ξ ) to be the type (resp. meta-term)
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 in Fig. 2. Note that in a well-typed function term, afunction symbol is annotated by its type asσσσ

f σ (x1 1 .t 1 , . . . , xi i .t i , . . . , xmm .tm )where f has the polymorphic type σ  ((σ1 → τ1 ), . . . , (σm → τm ) → τ )ξ . The type annotation is important in conﬂuence
checking of polymorphic rules. The notation t {x1 → s1 , . . . , xn → sn } denotes ordinary capture avoiding substitution that
replaces variables x1 , . . . , xn with terms s1 , . . . , sn .
n

Deﬁnition 2.2 (Substitution of meta-terms for metavariables [22,2,3]). Let ni = |τi | and τi = τi1 , . . . , τi i . Supposenn  , x1i τi1 , . . . , xi i τi i  si : σi

(1 ≤ i ≤ k),, M 1 : τ1 → σ1 , . . . , M k : τk → σk    e : τThen the substituted meta-term ,   e [ M → x.s ] : τ is deﬁned byx [ M → x.s ]  xnM i [t 1 , . . . , tni ] [ M → x.s ]  si {x1i → t 1 [ M → x.s ], . . . , xi i → tni [ M → x.s ]}ξξ
f ( y 1 .t 1 , . . . , ym .tm ) [ M → x.s ]  f ( y 1 .t 1 [ M → x.s ], . . . , ym .tm [ M → x.s ])where [ M → x.s ] denotes a substitution for metavariables [ M 1 → x1 .s1 , . . . , M k → xk .sk ].
We typically denote by θ a substitution, write e θ for e [ M → x.s ], and call t θ an instance of t.

8

M. Hamana et al. / Science of Computer Programming 187 (2020) 102322

2.3. Notions of values and non-values
Next we introduce the syntactic notions for value/non-values in our framework. In the case of λneed -calculus, we haveused the following two classes of values and non-values

Values V ::= x | λx. M

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

This deﬁnes two special names V , P of metavariables for values and non-values. To give a general deﬁnition of this kind of
distinction, we need a syntactic equality on variable names. We write “ X ≡ V ” for it, which means that the metavariable X ’s
letter is “V ”.
Deﬁnition 2.3. A metavariable X is called a value metavariable if X ≡ V or X ≡ V i . A metavariable is called a non-value
metavariable if X ≡ P or X ≡ P i . Indices i are natural numbers or some syntactic objects (e.g. metavariables, such as P M ).
A metavariable which is neither value nor non-value metavariable is often called a general metavariable.
Deﬁnition 2.4. A pattern meta-term is a meta-term which is not a metavariable, nor a meta-application. Value patterns Val area ﬁnite set of pattern meta-terms used for specifying values. Likewise, non-value patterns NonVal are a ﬁnite set of patternmeta-terms used for specifying non-values. These two sets must specify disjoint term sets, i.e., {t θ | t ∈ Val, subst. θ} ∩{t θ | t ∈ NonVal, subst. θ} = ∅.
In the case of λneed -calculus, we takeVal  {x, λx. M }NonVal  { M@N , let x = M in N }Deﬁnition 2.5 (Valid predicate for substitution). A substitution θ of meta-terms for metavariables is valid if for every X → x.sin θ , the following holds:(i) If X is a value metavariable, then s is an instance of a meta-term in V al.
(ii) If X is a non-value metavariable, then s is an instance of a meta-term in NonVal.
(iii) If X is a general metavariable, then there is no restriction on s.
We write valid θ if a substitution θ is valid. This is an instance of a valid predicate given in our previous work [18].
Remark 2.6. An arbitrary predicate to classify terms, rather than the value/non-value predicate, was allowed in our previous work [23]. To keep the theory simple and to investigate more detailed properties in this paper, we focus only on
value/non-value distinction of terms, and develop a general theory of conﬂuence for call-by-value calculi. 2
2.4. Polymorphic second-order computation system
For meta-terms
the form

 



: τ and   r : τ , a polymorphic second-order computation rule (or simply rule) is of⇒r :τ

satisfying
is not a metavariable nor meta-application, i.e., of the form f (x.t ).
is a higher-order pattern [15], i.e., a meta-term in which every occurrence of meta-application inM [x1 , . . . , xn ], where x1 , . . . , xn are distinct bound variables.
(iii) All metavariables in r appear in .
(i)
(ii)

is of the form

A polymorphic second-order computation system with values/non-values is formally given by a tuple ( , C , Val, NonVal)
consisting of a signature , a set C of rules, and value and non-value patterns. We may call it simply a computation
system.
Given a computation system ( , C , Val, NonVal), one-step computation   s ⇒C t : τ
is obtained by the inference system given in Fig. 3. The (RuleSub) instantiates a polymorphic computation rule ⇒ r in C by
substitution [ M → x.s ] of meta-terms for metavariables and substitution ξ on types. The (Fun) means that the computation
step is closed under polymorphic function symbol contexts.

M. Hamana et al. / Science of Computer Programming 187 (2020) 102322(RuleSub)

(Fun)

9

S is the set of all type variables in τi , σi , τξ : S →T  , xi : τi  si : σi ξ (1 ≤ i ≤ k)valid [ M → x.s ]( M 1 : (τ1 → σ1 ), . . . , M k : (τk → σk )    ⇒ r : τ ) ∈ C ,  ξ [ M → x.s ] ⇒C r ξ [ M → x.s ] : τ ξS  f : (σ1 → τ1 ), . . . , (σm → τm ) → τ ∈ξ : S →T
 , xi : σi  t i ⇒C t i : τi ξ (some i s.t. 1 ≤ i ≤ m)
σ

σ

σm
σm
   f σ (xσ1 1 .t 1 , . . . , xi i .t i , . . . , xm.tm ) ⇒C f σ (xσ1 1 .t 1 , . . . , xi i .t i , . . . , xm.tm ) : τ ξHere, σ  ((σ1 → τ1 ), . . . , (σm → τm ) → τ )ξ .
Fig. 3. Polymorphic second-order computation ⇒C on meta-terms.

If one-step computation happens under the empty metavariable context obtained as ·    s ⇒C t : τ (i.e. computationon terms, not on meta-terms), we write it as  s →C t : τ .
We also usually omit contexts and types, and simply write s ⇒C t or s →C t. We regard ⇒C and →C to be binary relations
on meta-terms and terms, respectively.
Example 2.7. The simply-typed λneed -calculus is formulated as a polymorphic second-order computation system withvalues/non-values(sigNeed, lmdNeed, Val, NonVal)
where the signature and rules are given as
sigNeed = [signature|lam : (a -> b) -> Arr(a,b)
let : a,(a -> b) -> b;

app : Arr(a,b),a -> b|]lmdNeed = [rule|(G)
let(M, x.N)=> N
(I)lam(x.M[x]) @ N=> let(N,x.M[x])(V-v) let(V, x.C[x])=> C[V](C-v) let(V, x.M[x])@N=> let(V, x.M[x]@N)(A)
let(let(L,x.M[x]), y.N[y]) => let(L,x.let(M[x],y.N[y])) |]and value and non-value patterns are deﬁned by

Val  {x, λx. M }NonVal  { M@N , let x = M in N }.

Note that in the signature, the type Arr(a,b) encodes a function type a → b of any order in the λneed -calculus. The
limitation to second-order in our framework is irrelevant to the type structure of the object language. As this example
shows, the second-order computation system can express a λ-calculus of any order (not only second-order) using type
constructors. 2
3. Type inference for polymorphic computation rules
We have formulated that polymorphic computation rules were explicitly typed. But when we give an implementation of
conﬂuence/termination checker, to insist 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 case of λneed -calculus, the user only
provides the signature sigNeed and “plain” rules lmdNeed in §1.4. The type inference algorithm infers the missing context
and type annotations (highlights) as:

M : s → t, N : s   appArr(s, t), s → t( lam(s → t) → Arr(s, t)(xs. M [x]), N ) ⇒ M [ N ] : t
These annotations are important for computing overlaps between rules when checking conﬂuence of polymorphic rules.
3.1. Algorithm
Our algorithm is given in Fig. 4, which is a variant of Damas–Milner type inference algorithm W [24]. It has several
modiﬁcations to cope with the language of meta-terms and to return enough type information for conﬂuence checking.

10

M. Hamana et al. / Science of Computer Programming 187 (2020) 102322= if x : τ appears in then ([],  xτ : τ ) else error= let a = freshVar(θ , t : τ ) = W ({x : a} ∪ , t )in (θ ,
 xa .t : a → τ )= if f : d → c appears in thenlet n = newNum in(d → c ) = attach the index n to all type vars in (d → c )(θ, , u , a) = foldr (Witer ) ([], [], [], []) tb = freshVarθ = unify((a → b)θ, d → c )in (θ ◦ θ, { f n : (d → c )θ } ∪ θ  f n (u ) : bθ )W ( , x)W ( , x.t )W ( , f (t ))else error

W ( , M [t ])= let (θ, , u , a) = foldr (Witer ) ([], [], [], []) tb = freshVarin (θ, { M : a → b} ∪
 M [u ] : b )Witer (t , (θ0 ,0, u,τ )) = let (θ,in (θ ◦ θ0 ,

 u : τ ) = W ( , t)
∪ 0 , (u , u ), (τ , τ ))mkMatch( )= {(σ , τ ) | ( M : σ ) ∈infer( , t )= let (θ, u : τ ) = W ( , t)
θ = unify(mkMatch( θ)) ◦ θin θ  u θ : τ θ= infer({rule : s, s → t} ∪ , rule(s, t ))infer( , s ⇒ t ), (M : τ ) ∈, σ = τ }• 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) to repeatedly apply the function W by the function Witer .
• unify returns the most general uniﬁer of the pairs of types.
• “[]” denotes the empty sequence or substitution.
Fig. 4. Type inference algorithm.

The algorithm takes a signature
and an un-annotated meta-term t. A sub-function W returns (θ, u : τ ), which isa pair of type substitution θ and an inferred judgment. The types in it are still needed to be uniﬁed. The context
maycontain uniﬁable declarations, such as M : σ and M : τ with σ = τ , and these σ and τ should be uniﬁed. The main function
infer( , t ) does it, and returns the form

 t : τ.
The meta-term t is a renamed t, where every function symbol f in the original t now has a unique index as f n , andisthe set of inferred type declarations for f n ’s and all the metavariables occurring in t . Similarly, for a given plain rule s ⇒ t,
 s ⇒ t : τ , whereis an inferred context and corresponding renamed terms s , t
the function infer( , s ⇒ t ) returns
as the sole term case. This is realised as inferring types for a meta-term to implement a rule using the new binary function
symbol rule (see the deﬁnition of 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 τ ≥ τ , if there exists a substitution σsuch that σ ◦ τ = τ . It is a preorder.
Theorem 3.1 (Soundness). If infer( , t ) = ( t : τ ), then there exists  such that  t :τ .

Proof. By induction on the structure of t.
Theorem 3.2 (Completeness). If   t : τ holds under a signature
substitution θ such that τ θ = τ andand infer( , | t |) = ( t : τ ), then there exists a• If M : σ ∈ then, there exists M : σ ∈such that σ θ = σ .
• If f σ →τ occurs in t, then there exists f n : σ → τ ∈such that f n occurs in t at the same position as t, and (σ → τ )θ =σ → τ.
Proof. By induction on the typing derivation of   t : τ.

M. Hamana et al. / Science of Computer Programming 187 (2020) 102322

11

The reason why our algorithm attaches an index n to each occurrence of a function symbol f as “ f n ” is to distinguishdifferent occurrences of the same f in a meta-term, and to correctly infer the type of each of them (see Prob. 2 in §1.4).
If we have infer( , t ) = (  t : τ ), then we can fully annotate types for the plain term t. We can pick the type of eachfunction symbol in t by ﬁnding f n : σ → τ ∈ , which means that this f has the inferred type σ → τ .
4. Conﬂuence of polymorphic computation systems in call-by-value
In this section, we establish a conﬂuence criterion of polymorphic computation systems based on critical pair checking.
4.1. Abstract rewriting
We review classical results on abstract rewriting [12,7]. Abstract rewriting is a general framework for analysing propertiesof rewriting without touching the structure of “terms”, only focusing the rewrite relation between elements (in this sense“abstract”).
An abstract rewriting system (ARS) is a pair ( A , →) of a set A and a binary relation → on A. We write →∗ for the reﬂexive
transitive closure, →+ for the transitive closure, and ← for the converse of →. We deﬁne ↔  → ∪ ←. We say:
1. a, b ∈ A are joinable, written a ↓ b, if ∃c . a →∗ c & b →∗ c.
2. → is conﬂuent if ∀a, b, c ∈ A . a →∗ b & a →∗ c implies b ↓ c.
3. → is Church-Rosser (CR) if ∀a, b ∈ A . a ↔∗ b implies a ↓ b.
4. → is locally conﬂuent (WCR) if ∀a, b, c ∈ A . a → b & a → c implies b ↓ c.
5. → is strongly normalising (SN) if ∀a ∈ A, there is no inﬁnite sequence a → a1 → a2 → · · · .
6. a is a normal form if there is no b ∈ A such that a → b.
We identify an ARS A with its relation → (e.g. we say A is CR to mean → is CR). It is well-known that conﬂuence andChurch-Rosser properties are equivalent, hence we have used the word CR to also mean conﬂuence.
4.2. Two conﬂuence properties
Suppose a polymorphic computation system C = ( , C , Val, NonVal) is given. First we note an important fact that thepair (the set of all meta-terms, ⇒C ) forms an ARS. Hence any notion and result on ARS are applicable to second-ordercomputation. Henceforth, we may regard a computation system C as the ARS. We say:(i) C is meta-conﬂuent if the ARS (the set of all meta-terms, ⇒C ) is conﬂuent.
(ii) C is object conﬂuent if the ARS (the set of all terms, →C ) is conﬂuent.
The difference between terms and meta-terms was in §2.2.
Since ⇒C ⊇ →C (see §2.4) and rewrite steps do not introduce new metavariables, if C is meta-conﬂuent, then it is also
object conﬂuent, but not vice versa. What we want to establish for concrete calculi (such as the λneed -calculus) is object
conﬂuence.
Meta-conﬂuence means the conﬂuence property at the meta-level, i.e., conﬂuence on the meta-terms with metavariables,
which are wider than the terms (with no metavariables). Practically, meta-conﬂuence is usually easier to establish, therefore
one often ﬁrstly establishes meta-conﬂuence and next concludes object conﬂuence as a derived property. The proof of
λneed -calculus in §1.4 actually chose this strategy: ﬁrstly established the meta-conﬂuence of the polymorphic computation
system, and then concluded the object conﬂuence. But this strategy does not always work. In §6, we will see that thepolymorphic computation system of λC -calculus is not meta-conﬂuent; nevertheless, we can prove its object conﬂuence ofit using the notion of call-by-value joinability (Deﬁnition 4.5).
4.3. Notion of uniﬁer between two polymorphic meta-terms in call-by-value
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 makes sθ = t θ . In the case of polymorphic second-orderalgebraic theory, we should also take types into account. 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 → xbool .gbool→int (x) together witha type substitution ξ : v → bool, t → int.
Moreover, a uniﬁer for value/non-value metavariables should be valid. For example, consider a uniﬁcation problem:M @ λ(a→b)→Arr(a,b) (x. N [x]) = P @ V?

12

M. Hamana et al. / Science of Computer Programming 187 (2020) 102322

This is uniﬁable by a valid substitution θ = { M → P , V → λ(a→b)→Arr(a,b) (x. N [x])}, because λ(a→b)→Arr(a,b) (x. N [x]) is a value,
and a general metavariable M can be replaced with a non-value P (but P → M is invalid). A non-solvable problem is

V @ λ(a→b)→Arr(a,b) (x. N [x]) = P 1 @ P 2?

Neither V → P 1 nor P 1 → V is valid. Moreover, P 2 → λ(a→b)→Arr(a,b) (x. N [x]) is invalid, because P 2 is a non-value metavariable while λ-abstraction is a value.
This leads us to the following deﬁnition.
Deﬁnition 4.1. A uniﬁer between meta-terms s and t is a tuple (ξ, ϑ) such that s ξ ϑ = t ξ ϑ , where(i) ξ is a substitution of types for type variables, and(ii) ϑ is a valid substitution of meta-terms for metavariables.
The most general uniﬁer is a maximal uniﬁer with respect to the preorder on substitutions of type variables and of metaterms.
4.4. Critical pairs of polymorphic computation systems with values/non-values
We now formulate the notion of critical pairs for our polymorphic case with values/non-values distinction. We ﬁrst recall
basic notions.
A position p is a ﬁnite sequence of natural numbers. The empty sequence ε is the root position, and the concatenationof positions is denoted by pq or p .q. The order on positions is deﬁned by p < q if there exists a non-empty p such thatp . p = q. The set Pos(t ) of the positions of a meta-term t is deﬁned byPos(x) = {ε }Pos(x.t ) = {ε } ∪ {1. p | p ∈ Pos(t )}Pos( f (t 1 , . . . , tn )) = {ε } ∪ {i . p | 1 ≤ i ≤ n, p ∈ Pos(t i )}Pos( M [t 1 , . . . , tn ]) = {ε } ∪ {i . p | 1 ≤ i ≤ n, p ∈ Pos(t i )}The notation s[u ] p means replacing the subterm at the position p of s with u, and s| p means selecting the subterm of s at
the 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 .
Deﬁnition 4.2. We say that a position p in a meta-term t is a metavariable position if t | p is a metavariable or metaapplication, i.e., t | p = M [c 1 , . . . , cn ]. This description includes the case t | p = M by the case n = 0, for which we identify M [ ]with just a metavariable M.
An overlap represents an overlapping of the two rules, which admits the situation that a term can be rewritten by thetwo different rules.
Deﬁnition 4.3. An overlap between two rules l1 ⇒ r1 and l2 ⇒ r2 of a polymorphic computation system ( , C , Val, NonVal)
is a tuple l1 ⇒ r1 , p , l2 ⇒ r2 , ξ, ϑ satisfying the following properties:(i) l1 ⇒ r1 , l2 ⇒ r2 are variants of rules in C without common (meta)variables.
(ii) (ξ, ϑ) is a most general uniﬁer between l1 | p and l2 .
(iii) p is a non-metavariable position of l1 , or if p is a metavariable position of l1 , i.e., l1 | p = M [c 1 , . . . , cn ], then M is a value
or non-value metavariable.
(iv) If p is the root position, l2 ⇒ r2 is not a variant of l1 ⇒ r1 .
The ordinary deﬁnition of overlap requires that the position p of l1 be a non-metavariable position because l1 | p matches
anything if it is a metavariable, which means that it should not be considered as overlapping. But in the call-by-value
case, the situation differs, because a value metavariable V (resp. a non-value metavariable P ) represents value patterns(resp. non-value patterns) in V al. If l1 | p is a value metavariable, then we need to check overlapping between value patterns
and a meta-term. We note that the notion of values is not stable under reduction (unlike the notion of types). For example,
a β-reduction stepλ(x.x)@ y ⇒C y

M. Hamana et al. / Science of Computer Programming 187 (2020) 102322

13transforms a non-value (an application) to a value (a variable). Therefore, a non-value metavariable position in a meta-term
might become a value position during computation. This means that we need to analyse the cases when a meta-term
involves a value/non-value metavariable. The bold face sentence in the item (iii) describes it.
Deﬁnition 4.4. The critical pair (CP) generated by an overlap l1 ⇒ r1 , p , l2 ⇒ r2 , ξ, ϑ is a triple r1 θ, l1 θ, r2  where• θ  ϑ ◦ ξ,
• l1 θ ⇒C r1 θ which rewrites the root position ε of l1 θ using l1 ⇒ r1 ,• l1 θ ⇒C r2 which rewrites the position p of l1 θ using l2 ⇒ r2 .
This is depicted as

l1 θ
p

ε

r1 θ

r2

This is a critical situation that admits two ways of reduction, hence called a critical pair. Ordinary Knuth-Bendix critical pairs lack the middle l1 θ , hence “pairs”. But including “the source of divergence” designates a situation more clearly(especially in the implementation), hence our notion of critical pair consists of three terms. We deﬁneoverlap(l1 ⇒ r1 , l2 ⇒ r2 )  {all possible overlaps between l1 ⇒ r1 and l2 ⇒ r2 }.
Algorithmically, this function scans all subterms of l1 and tries to unify each of them with l2 to produce an overlap using
second-order uniﬁcation. We then collect all overlaps in C byO{overlap(l1 ⇒ r1 , l2 ⇒ r2 ) | l1 ⇒ r1 , l2 ⇒ r2 ∈ C }.

Finally, we obtain all critical pairs of C by generating the critical pair of each overlap in O .
4.5. Joinability of critical pairs
We assume that for each metavariable M, there exist a value metavariable V M and a non-value metavariable P M . We
say that a critical pair r1 , t , r2  is joinable if r1 ⇓C r2 , depicted as

t
r1

r2
∗

∗

·

Deﬁnition 4.5. We say that a critical pair r1 , t , r2  is call-by-value joinable if for every substitution ρ of metavariables formetavariables in t satisfyingρ : M → V M or M → P M for each metavariable M occuring in t ,then the joinability r1 ρ ⇓C r2 ρ holds. This is depicted as

tρ

(2)

r1 ρ

r2 ρ
∗

·

∗

This amounts to checking joinability in the call-by-value setting. In the call-by-value setting, M denotes either a value or
non-value. Hence we check for each M in t, two cases of the joinability: when M is a value metavariable and when M is a
non-value metavariable. This is done by applying all possible renamings ρ that change M in t to either a value metavariable
V M or a non-value metavariable P M .

14

M. Hamana et al. / Science of Computer Programming 187 (2020) 102322

Lemma 4.6.
1. If a critical pair is joinable, then it is also call-by-value joinable, but not vice versa.
2. If a critical pair r1 , t , r2  is call-by-value joinable, then r1 θ ↓C r2 θ for any substitution θ of terms (without metavariables) for
metavariables.
Proof.
(i) By deﬁnition.
(ii) Instantiating the joinability (2) of call-by-value critical pairs to terms, we have the result.
We ﬁrst prove an easier case, which does not have value/non-value distinction.
Proposition 4.7. Let ( , C ) be a polymorphic second-order computation system without value/non-value metavariables. If every critical pair of ( , C ) is joinable, then ⇒C is locally conﬂuent.
Proof. We show “if u ⇐C w ⇒C s then u ⇓C s” by induction on the proof of u ⇐C w, using the inference rules in Fig. 3.

• (RuleSub) Let l ⇒ r ∈ C and consider the situationεpr θ ⇐== lθ ==⇒ sfor a valid substitution θ for metavariables and type variables.
(i) If the rewrite position p is not “a metavariable position of l or below it”, then it is an instance of a critical pair,hence r θ ⇓C s.
(ii) Case p = p · q is a metavariable position in l or below it, i.e., there exists a metavariable M : σ1 , . . . , σn → τ suchthatl| p = M [c ]where c 1 , . . . , cn are distinct bound variables, since l is a higher-order pattern. Suppose θ has the following assignment:θ : M → x1 , . . . , xn . t
Let t p be a one-step reduct of t by contracting the position q ast {x → c } ⇒C t p
We deﬁne
Mplp l [ M p ]p ;

θ p  [ M p → t p ]Mpi.e., l p as a modiﬁed l, where M [c ] at the position p of l is replaced with a new metavariable M p : τ .
(Note that the arity changed from M to M p , and since M is never a value/non-value metavariable, θ p is always
valid. If value/non-value metavariables are involved, the validity of θ p is not ensured.)Deﬁne θ to be M → c .t p , N → θ( N ) for N = M, which is valid. Since l is a higher-order pattern, we have
ε

p

Mp

rθ ⇐==== lθ ====⇒ l p θ p θ = s



∗




∗

r θ ⇐=============== l θp• (Fun): Consider the situation f ξ (x.s) ⇐== f ξ (x.u ) ==⇒ t, where p is not the root position because (Fun) is applied.
Hereafter, we omit the superscript of f .
(i) Case that the right rewrite happens at the root, i.e., there exists l ⇒ r ∈ C and a valid θ such thatpεs ⇐==== f (x.u ) = lθ ===⇒ r θFlipping the left and right rewrites, r θ ⇓C s is proved as the case for (RuleSub).

M. Hamana et al. / Science of Computer Programming 187 (2020) 102322(RuleSub)

(Fun)

15

S is the set of all type variables in τi , σi , τξ : S →T  , xi : τi  si : σi ξ (1 ≤ i ≤ k)valid [ M → x.s ]( M 1 : (τ1 → σ1 ), . . . , M k : (τk → σk )    ⇒ r : τ ) ∈ C ,  ξ [ M → x.s ] →C r ξ [ M → x.s ] : τ ξS  f : (σ1 → τ1 ), . . . , (σm → τm ) → τ ∈ξ : S →T
 , xi : σi  t i →C t i : τi ξ (some i s.t. 1 ≤ i ≤ m)
σ

σ

σm
σm
   f σ (xσ1 1 .t 1 , . . . , xi i .t i , . . . , xm.tm ) →C f σ (xσ1 1 .t 1 , . . . , xi i .t i , . . . , xm.tm ) : τ ξHere, σ  ((σ1 → τ1 ), . . . , (σm → τm ) → τ )ξ .
Fig. 5. Polymorphic second-order computation →C on terms.

(ii) Case the i , j-th arguments of f are rewritten. Without loss of generality, we assume i < j ∈ N .
ipjqf (· · · , xi .u i , · · · , x j .u j , · · · ) ⇐== f (x.u ) ==⇒ f (· · · , xi .u i , · · · , x j .u j , · · · )



jq



ip

f (· · · , xi .u i , · · · , x j .u j , · · · ) ============== f (· · · , xi .u i , · · · , x j .u j , · · · )(iii) Case the i-th argument of f is rewritten by two ways as:
ipiqf (· · · , xi .u i , · · · ) ⇐=== f (x.u ) ===⇒ f (· · · , xi .u i , · · · )



∗



∗

f (· · · , xi .s, · · · ) =================== f (· · · , xi .s, · · · )The above diagram commutes by the induction hypothesis:u i ⇒∗C s ⇐∗C u i and closedness of reduction by contexts.
The next is a key proposition, which takes value/non-values into account.
Proposition 4.8. Let ( , C , Val, NonVal) be a polymorphic second-order computation system. If every critical pair is call-by-value
joinable, then →C is locally conﬂuent.
Proof. We show “if w ←C u →C s then w ↓C s” by induction on the proof of w ←C u, using the inference rules in Fig. 5.

• (RuleSub) Let l ⇒ r ∈ C and consider the situation
rθ 
ε

lθ

- s

p

for a valid substitution θ for metavariables and type variables.
(i) If the rewrite position p is not “a metavariable position of l or below it”, then r θ, lθ, s is an instance of a criticalpair, hence by Lemma 4.6, it is joinable.
(ii) Case p = p · q is a metavariable position in l or below it, i.e., there exists a metavariable M : σ1 , . . . , σn → τ suchthat l| p = M [c ]. Suppose θ has the assignmentθ : M → x1 , . . . , xn . t .
(a) If M is a value or non-value metavariable, then r θ, lθ, s is an instance of a critical pair, hence by Lemma 4.6,
it is joinable.
(b) If M is a general metavariable, then it is proved by the same way as the proof of Proposition 4.7, (RuleSub) (ii).
• (Fun): This case is proved by the same way as the proof of Proposition 4.7 (Fun).
Theorem 4.9. Let ( , C , Val, NonVal) be a polymorphic second-order computation system. Assume that C is strongly normalising. If
every critical pair is call-by-value joinable, then C is object conﬂuent, i.e., →C is conﬂuent.
Proof. By Proposition 4.8 and Newman’s lemma.

16

M. Hamana et al. / Science of Computer Programming 187 (2020) 102322

1: new(a.new(b.H[b]))2: new(a.new(b.X’[a]))(idem-new)(new/new)(new/new)(idem-new)

new(b.H[b])new(a.new(b.H[a]))new(a.new(b.X’[b]))new(a.X’[a])3: new(a.new(b.new(b’.X’[a,b,b’])))(new/new)(new/new)

new(a.new(b.new(b’.X’[a,b’,b])))new(a.new(b.new(b’.X’[b,a,b’])))·

Fig. 6. Critical pairs of a calculus of the new name generation.

5. Conﬂuence criteria without termination
A given calculus is often not terminating or proving its termination is diﬃcult. Nevertheless we want to prove conﬂuence. This section presents three additional conﬂuence criteria: two techniques not requiring termination, called strongclosedness (§5.1) and orthogonality (§5.2), and one technique by modularity (§5.3). These criteria have been implemented
in the PolySOL system.
5.1. Conﬂuence by strong closedness
As an example, we consider the laws of the new name generation operator (or, restriction operator) [5, Sec. V]. They
include a function symbol new for new name generation and two rules. The idea is that new(a.X[a]) ﬁrst generates aname a and then continues as X using a, as in the new operator of the π-calculus [25].
sigrest = [signature|
new : (N -> A) -> A |]rest = [rule|(idem-new) new(a.X)=> X(new/new) new(a.new(b.X[a,b])) => new(a.new(b.X[b,a])) |]The law (idem-new) states that generating a new name a and continuing X without using a is equivalent to just doing X.
The law (new/new) states that generating new names a and b and continuing X using a,b is equivalent to generating
new names a and b, and continuing X using b,a (N.B. the application order is changed).
By invoking the command “cri” for critical pair checking, PolySOL checks their critical pairs. It reports three CPs, all ofwhich are joinable (see Fig. 6). Importantly, the system is not strongly normalising because the rhs of the rule (new/new)matches its lhs. Therefore, we cannot infer conﬂuence based on Newman’s lemma. Other criteria must be sought.
Examining the CPs carefully as shown in Fig. 6, one can ﬁnd a particular phenomenon: all the CPs are joinable by at-mostone-step (from left, right, or both sides). This property, which is known as strong closedness of CPs, is useful to provide a
suﬃcient condition deriving strong conﬂuence [12] of a computation system, which implies conﬂuence without termination.
We will formulate this method formally. For an ARS ( A , →), we deﬁne →=  → ∪ id A (i.e., the reﬂexive closure of →).
We say that → is strongly conﬂuent if∀a, b, c ∈ A . a → b & a → c implies ∃d. b →∗ d & c →= d.
Proposition 5.1 (Strong conﬂuence [12]). Every strongly conﬂuent ARS is conﬂuent.
Deﬁnition 5.2. A computation system ( , C ) is strongly closed if for every critical pair r1 , t , r2  of ( , C ), there exist u 1=∗
and u 2 such that r1 ⇒∗C u 1 ⇐=C r 2 and r 1 ⇒C u 2 ⇐C r 2 .
A meta-term is called linear if no metavariable occurs more than once. A computation system is called linear if bothsides of rules are linear, and left-linear if every left-hand side of rules is linear. We now prove a theorem deriving strong
conﬂuence by checking the strong closedness of CPs.
Theorem 5.3. Let ( , C ) be a linear polymorphic second-order computation system. If ( , C ) is strongly closed and both sides of eachrule are higher-order patterns, then ⇒C is strongly conﬂuent, hence conﬂuent.

M. Hamana et al. / Science of Computer Programming 187 (2020) 102322

17

Proof. We show “if u ⇐C w ⇒C s then u ⇒∗C ◦⇐=C s” by induction on the proof of u ⇐C w, using the inference rules inFig. 3.

• (RuleSub) Let l ⇒ r ∈ C and consider the situationεpr θ ⇐== lθ ==⇒ sfor a valid substitution θ for metavariables and type variables.
(i) If the rewrite position p is a non-metavariable position of l, then it is an instance of a critical pair, hence r θ ⇒∗C◦⇐=
C s by strong closedness.
(ii) Case p is a metavariable position in l or below it, i.e., there exists a metavariable M : σ1 , . . . , σn → τ such thatl| p = M [c ]. Since l is a higher-order pattern, c 1 , . . . , cn are distinct bound variables. Suppose θ : M → x1 , . . . , xn . t
Mp

and t {x → c } ⇒C t p . We deﬁne l p  l [ M p ] p , θ p  [ M p → t p ], and θ : M → c .t p , N → θ( N ) for N = M, which isvalid. Since l and r are linear and higher-order patterns, we have
ε

p

Mp

rθ ⇐==== lθ ====⇒ l p θ p θ = s








=

r θ ⇐=============== l θ• (Fun): This case is proved in the same way as the proof of Proposition 4.7 (Fun).
Example 5.4. The computation system rest given in the beginning of this subsection is strongly conﬂuent because every
CP is strongly closed, hence conﬂuent. 2
The method for proving conﬂuence of linear rewriting systems through strong closedness of CPs has been used in Suzuki
et al.’s paper [26] for nominal rewriting systems. We gave a suﬃcient condition for strong conﬂuence for polymorphic
computation systems. Our method is also straightforwardly applicable to the case of Mayr and Nipkow’s higher-order rewrite
systems [9].
5.2. Conﬂuence by orthogonality
Another conﬂuence criterion not requiring termination is “orthogonality”.
Deﬁnition 5.5. A computation system ( , C ) is called orthogonal if it is left-linear and for any rules l1 ⇒ r1 , l2 ⇒ r2 in C ,there exists no overlap between l1 ⇒ r1 and l2 ⇒ r2 .
par

We show that every orthogonal computation system is conﬂuent. We ﬁrst deﬁne a notion of parallel reduction ⇒Cusing the inference system in Fig. 7.
Lemma 5.6.
par(i) s ⇒C s.

par(ii) If s ⇒C t then s ⇒C t.

(iii) If s ⇒C t then s ⇒∗C t.
par

Proof.
(i) By induction on s.
(ii) By induction on the proof of s ⇒C t, using (i).
par(iii) By induction on the proof of s ⇒C t.
parThus, to obtain conﬂuence of ⇒C , it suﬃces to show that ⇒C
par

par

u ⇒C ◦ ⇐C t.

par

par

has the diamond property: if u ⇐C s ⇒C t then

par

par

Notation 5.7. We write θ ⇒C δ to mean that for any metavariable M (with arity n) with θ : M → x.s, θ : M → x.t, s ⇒C t
par

par

holds. We also write t ⇒C t as an abbreviation for t i ⇒C t i for all i = 1, . . . , |t |.
The following lemma is used in the proof of Theorem 5.11.

18

M. Hamana et al. / Science of Computer Programming 187 (2020) 102322(Varpar )y:τ ∈par   y ⇒C y : τ( M : σ1 , · · · , σm → τ ) ∈par   t i ⇒C t i : σi (1 ≤ i ≤ m)

(Metavarpar )(RuleSubpar )(Funpar )par   M [t 1 , . . . , tm ] ⇒C M [t 1 , . . . , tm ] : τS is the set of all type variables in τi , σi , τξ : S →Tpar
  , xi : τi  si ⇒C si : σi ξ (1 ≤ i ≤ k)valid [ M → x.s ]valid [ M → x.s ]( M 1 : (τ1 → σ1 ), . . . , M k : (τk → σk )    ⇒ r : τ ) ∈ C
par ,  ξ [ M → x.s ] ⇒C r ξ [ M → x.s ] : τ ξS  f : (σ1 → τ1 ), . . . , (σm → τm ) → τ ∈par , xi : σi  t i ⇒C t i : τi ξ (1 ≤ i ≤ m)σm   f σ (xσ1 1 .t 1 , . . . , xm.tm ) ⇒Cparσ

ξ : S →Tσ

f σ (x1 1 .t 1 , . . . , xmm .tm ) : τ ξHere, σ  ((σ1 → τ1 ), . . . , (σm → τm ) → τ )ξ .
parFig. 7. Parallel reduction ⇒Cparon meta-terms.

parLemma 5.8. If θ ⇒C δ then sθ ⇒C sδ .
parThe next lemma expresses the following idea: in a parallel-reduction step lθ ⇒C s, where l is a linear higher-order pattern and does not overlap with any rule, the l-part cannot change, i.e., all reductions must take place inside the meta-terms
introduced via θ .
Lemma 5.9. Let ( , C ) be a polymorphic second-order computation system, and let l be a linear higher-order pattern that does notparparoverlap with any left-hand side of C . Then, if lθ ⇒C s then there exists a valid substitution δ such that lδ = s and θ ⇒C δ .
Corollary 5.10. Let ( , C ) be an orthogonal polymorphic second-order computation system, and let l ⇒ r ∈ C . Then, if lθ = f (x.t ) andparpart ⇒C t then there exists a valid substitution δ such that lδ = f (x.t ) and θ ⇒C δ .
parWe now prove a theorem deriving the diamond property of ⇒C .
par

Proposition 5.11. Let ( , C ) be a polymorphic second-order computation system. If ( , C ) is orthogonal, then ⇒C has the diamondproperty.
par

Proof. We show “if u ⇐C
par

par

par

w ⇒C

par

par

s then u ⇒C ◦ ⇐Cs” by induction on the sum of the lengths of the proofs ofu ⇐C w and w ⇒C s, with a case analysis according to the inference rules in Fig. 7.
Here we consider the most diﬃcult case where the last inference rule used in one of the two proofs is (RuleSubpar ) andthe other is (Funpar ). The other cases are shown by using the induction hypothesis.
par• Let l ⇒ r ∈ C , t ⇒C t and consider the situation(RuleSubpar )(Funpar )r θ ⇐======= lθ = f (x.t ) =====⇒ f (x.t )parfor valid substitutions θ, θ for metavariables and type variables such that θ ⇒C θ . Then by Corollary 5.10, thereparexists a valid substitution δ such that lδ = f (x.t ) and θ ⇒C δ . Hence by the induction hypothesis, there exists a valid
par

par

par

substitution δ such that θ ⇒C δ and δ ⇒C δ . By applying (RuleSubpar ), we have f (x.t ) = lδ ⇒C r δ . On the otherparhand, by Lemma 5.8, we have r θ ⇒C r δ , thus closing the diamond.

Combining this with Lemma 5.6, we have:
Theorem 5.12. Every orthogonal computation system is meta-conﬂuent.

M. Hamana et al. / Science of Computer Programming 187 (2020) 102322

19

Mayr and Nipkow have shown that every orthogonal higher-order pattern rewrite system without polymorphism is conﬂuent [9] using a different notion of parallel reduction called superdevelopments originally used in Aczel’s paper [27]. We
parhave shown that every orthogonal polymorphism computation system is conﬂuent using the parallel reduction “ ⇒C ” inthe style of developments as in Tait and Martin-Löf’s proof for λ-calculus [17]. In the next subsection, we also apply thistechnique to show commutation of mutually orthogonal computation systems.
5.3. Modular conﬂuence checking
It is sometimes useful to split the system into two subsystems for making its conﬂuence proof easier; in particular, into
the higher-order part and the ﬁrst-order part to which we can apply a powerful conﬂuence prover for ﬁrst-order term
rewriting systems. In this subsection, we present a criterion for modular conﬂuence checking.
As an example, consider a λ-calculus with a union operator, called the λG-calculus [28].
siglamU = [signature|app: Arr(G,G),G -> G ; lam : (G -> G) -> Arr(G,G)
union : G,G -> G
; 0
: G
|]
lamU = [rule|(beta)
lam(x.M[x]) @ N=> M[N](eta)
lam(x.M@x)=> M(u-unitr) union(X,0)=> X(u-unitl) union(0,Y)=> Y(u-assoc) union(union(X,Y),Z) => union(X,union(Y,Z))(u-com)union(X,Y)=> union(Y,X)|]

The ﬁrst two rules are for the λ-calculus, the (u-*) rules formalise the union operator (which may be considered as nondeterministic choice). This system is not terminating because of (u-com). Moreover, the union rules have many overlaps,
hence is not orthogonal, nor strong conﬂuent. Hence, we cannot apply the previous methods to prove conﬂuence of lamU.
Now we see that this system can be clearly split into the higher-order part (β and η ) and the ﬁrst-order part (the rules
for union). There exists no overlap between these two parts. The situation is formally stated as follows.
Deﬁnition 5.13. Two computation systems ( 1 , C1 ) and ( 2 , C2 ) are mutually orthogonal if they are left-linear and for any
rules l1 ⇒ r1 ∈ C1 and l2 ⇒ r2 ∈ C2 , there exists no overlap between l1 ⇒ r1 and l2 ⇒ r2 .
We need abstract properties. Let ( A , →1 ) and ( A , →2 ) be two ARSs. We say that →1 and →2 commute if∀a, b, c ∈ A . a →∗1 b & a →∗2 c implies ∃d. b →∗2 d & c →∗1 d
and that →1 and →2 have the commuting diamond property if∀a, b, c ∈ A . a →1 b & a →2 c implies ∃d. b →2 d & c →1 d
The following lemmas on commutation hold [7, pp. 31–32].
Lemma 5.14. If →1 and →2 are conﬂuent and commute then →1 ∪ →2 is also conﬂuent.
Lemma 5.15. If →1 and →2 have the commuting diamond property then they commute.
Since ⇒∗C = ( ⇒C )∗ by Lemma 5.6, commutation of ⇒C1 and ⇒C2 equals commutation of ⇒C and ⇒C . Hence,1
2
to obtain conﬂuence of a computation system ( 1 ∪ 2 , C1 ∪ C2 ) from two conﬂuent computation systems ( 1 , C1 ) andparpar( 2 , C2 ), it suﬃces to show that ⇒C and ⇒C have the commuting diamond property.
par

par

1

2

Proposition 5.16. Let ( 1 , C1 ) and ( 2 , C2 ) be two polymorphic second-order computation systems. If (parparmutually orthogonal, then ⇒C and ⇒C have the commuting diamond property.
1par

Proof. We show “if u ⇐C
par

par

1

par

1 , C1 ) and (2 , C2 ) are

2

par

w ⇒C

2

par

par

2

1

s then u ⇒C ◦ ⇐Cs” by induction on the sum of the lengths of the proofs ofu ⇐C w and w ⇒C s, with a case analysis according to the inference rules in Fig. 7.
1
2
Here we consider the most diﬃcult case where the last inference rule used in one of the two proofs is (RuleSubpar ) andthe other is (Funpar ). The other cases are shown by using the induction hypothesis.

20

M. Hamana et al. / Science of Computer Programming 187 (2020) 102322

6: let(V,x.x)

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

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

(η-v)

V’@V

= V’@V

(η-v)

(β-v)

(η-let)(β-let-v)

lam(x’.H[x’]) = lam(x.H[x])

=

V

V

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

9: let(let(L,x.x),y.N[y])(η-let)(assoc)(assoc)let(L,x’.M’[x’])let(L,x’.let(M’[x’],x.x))(η-let)let(L,x.let(x,y.N[y]))let(L,x.N[x])10: let(let(let(L’,x’.M’[x’]),x.M[x]),y.N[y])(assoc)(assoc)let(let(L’,x’.let(M’[x’],y’.M[y’])),y.N[y])let(let(L’,x’.M’[x’]),x.let(M[x],y.N[y]))∗∗·Fig. 8. Critical pairs of the λC -calculus (excerpt).

par• Let l ⇒ r ∈ C1 , t ⇒C2 t and consider the situation(RuleSubpar )(Funpar )r θ ⇐======= lθ = f (x.t ) =====⇒ f (x.t )parfor valid substitutions θ, θ for metavariables and type variables such that θ ⇒C θ . Then by Lemma 5.9, there exists
par1

a valid substitution δ such that lδ = f (x.t ) and θ ⇒C δ . Hence by the induction hypothesis, there exists a valid
par

2

par

par

substitution δ such that θ ⇒C δ and δ ⇒C δ . By applying (RuleSubpar ), we have f (x.t ) = lδ ⇒C r δ . On the other
1
1
2
par
hand, by Lemma 5.8, we have r θ ⇒C r δ , thus closing the diamond.
2

Clearly, if the left-linear computation systems (are mutually orthogonal. Thus, we have:

1 , C1 ) and (2 , C2 ) have two disjoint signatures (i.e.,1∩2 = ∅), they

Theorem 5.17. Let ( 1 , C1 ) and ( 2 , C2 ) be polymorphic second-order computation systems over two disjoint signatures. If (and ( 2 , C2 ) are left-linear and conﬂuent then the computation system ( 1 ∪ 2 , C1 ∪ C2 ) is meta-conﬂuent.

1 , C1 )In particular, we can split the whole system into the higher-order and the ﬁrst-order parts, provided that they havedisjoint signatures.

Corollary 5.18. Let ( 1 , C1 ) be a polymorphic second-order computation system and let ( 2 , C2 ) be a ﬁrst-order computation system,
where 1 and 2 are disjoint signatures. If ( 1 , C1 ) and ( 2 , C2 ) are left-linear and meta-conﬂuent then the computation system( 1 ∪ 2 , C1 ∪ C2 ) is meta-conﬂuent.

Example 5.19. The computation system lamU given in the beginning of this subsection is left-linear. Splitting it into thehigher-order rules (β and η rules) and the ﬁrst-order rules for union, both of which are meta-conﬂuent, we see that thecomputation system lamU is meta-conﬂuent, and also object conﬂuent. 2

6. Example 2: conﬂuence of the computational λ-calculus

In this section, we present a proof of conﬂuence of Moggi’s computational λ-calculus, the λC -calculus [29] using PolySOL.
The λC -calculus is a fundamental calculus for effectful computation, which is an extension of the call-by-value λ-calculus
enriched with let-construct to represent sequential computation.

M. Hamana et al. / Science of Computer Programming 187 (2020) 102322

21

The λC -calculus has seven rules, which are straightforwardly deﬁned in PolySOL as follows:siglamC = [signature|
app : Arr(a,b),a -> b ; lam : (a -> b) -> Arr(a,b)
let : a,(a -> b) -> b|]lamC = [rule|lam(x.V @ x) => V(β-v)
lam(x.M[x]) @ V => M[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])) |]It consists of the function symbol lam for λ-abstraction, app (also written as the inﬁx operator @) for application, andlet-construct. We represent the arrow types of the “object-level” λC -calculus by the binary type constructor Arr, and use
the function types a -> b of the “meta-level” polymorphic second-order computation system to represent binders, wherea,b are type variables.
To the best of our knowledge, conﬂuence of the λC -calculus has not been formally proved in the literature including
the original [29] and subsequent works [30,31,13]. Next, we use PolySOL to check the conﬂuence of the simply-typed
λC -calculus.
We impose the distinction of values and non-values as in the λneed -calculus. Here V is a metavariable for values, P
is a metavariable for non-values, and M,N,L are general metavariables for all terms. We tell PolySOL the value/non-value
metavariable distinction by writing the suﬃxes “-v” and “-p” in the labels. Although the rule set is not so large, the whole
proof is fairly large because it has a number of non-trivial overlaps as a result of the value/non-value distinction.
By invoking the command “criCBV” for critical pair checking in call-by-value, PolySOL checks their critical pairs using
value/non-value metavariables. It reports 23 CPs. All are successfully call-by-value joinable. Because the output is long, we
present only some of them, and explain some details. The reader can obtain the full output easily using the web interface(see 8.3).
*SOL> criCBV lamC siglamC
1: Overlap (beta-v)-(eta-v)--- M|-> z1.(z1@z1), V’|-> x ----------------------(beta-v) lam(x.M[x])@V => M[V](eta-v) lam(x’.(V’@x’)) => V’lam(x2.(x2@x2))@V
V@V <-(beta-v)-∧-(eta-v)-> lam(x2.(x2@x2))@V---> V@V =OK= V@V <--2: Overlap (beta-v)-(eta-v)--- V|-> lam(x’.(V’@x’)) --------------------------(beta-v) lam(x.M[x])@V => M[V](eta-v) lam(x’.(V’@x’)) => V’lam(x.M[x])@lam(x’.(V’@x’))
M[lam(x’.(V’@x’))] <-(beta-v)-∧-(eta-v)-> lam(x.M[x])@V’---> M[V’] =OK= M[V’] <--..

The CP (2:) results from the overlap between (beta-v) and (eta-v), where the metavariable V matches with theroot of the lhs of (eta-v). Because ordinary critical pair checking does not check a metavariable position as an overlap,
this overlap is particular to the call-by-value setting. The reason it should be regarded as an overlap is that V is either avariable or an abstraction because it represents a value. In the case of λC , the rule (eta-v) is the only rule having a value
as lhs, which makes it matchable. The CPs (4:) and (5:) in the following have the same reason.
..
4: Overlap (eta-v)-(eta-v_x)--- V|-> lam(x’.(V’25@x’)), V’|-> z1.V’25 --------(eta-v) lam(x.(V@x)) => V(eta-v_x) lam(x’.(V’[x]@x’)) => V’[x]lam(x.(lam(x’.(V’25@x’))@x))lam(x’.(V’25@x’)) <-(eta-v)-∧-(eta-v_x)-> lam(x.(V’25@x))---> V’25 =OK= V’25 <--5: Overlap (beta-let-v)-(eta-v)--- V|-> lam(x’.(V’@x’)) ----------------------(beta-let-v) let(V,x.M[x]) => M[V](eta-v) lam(x’.(V’@x’)) => V’let(lam(x’.(V’@x’)),x.M[x])M[lam(x’.(V’@x’))] <-(beta-let-v)-∧-(eta-v)-> let(V’,x.M[x])---> M[V’] =OK= M[V’] <--..

We depict a graphical representation of some of them in Fig. 8. The following check illuminates the call-by-value CP
checking.

22

M. Hamana et al. / Science of Computer Programming 187 (2020) 102322..
11: Overlap (let1-p)-(beta-v)--- P|-> lam(x’.M’[x’])@V’ -----------------------when M’|-> x95.VM’[x95], M|-> VM(let1-p) P@M => let(P,x.(x@M))(beta-v) lam(x’.M’[x’])@V’ => M’[V’](lam(x’.VM’[x’])@V’)@VM
let(lam(x’.VM’[x’])@V’,x92.(x92@VM)) <-(let1-p)-∧-(beta-v)-> VM’[V’]@VM---> VM’[V’]@VM =OK= VM’[V’]@VM <--11: Overlap (let1-p)-(beta-v)--- P|-> lam(x’.M’[x’])@V’ -----------------------when M’|-> x95.VM’[x95], M|-> PM(let1-p) P@M => let(P,x.(x@M))(beta-v) lam(x’.M’[x’])@V’ => M’[V’](lam(x’.VM’[x’])@V’)@PM
let(lam(x’.VM’[x’])@V’,x92.(x92@PM)) <-(let1-p)-∧-(beta-v)-> VM’[V’]@PM---> let(PM,y1.(VM’[V’]@y1)) =E= let(PM,y4.(VM’[V’]@y4)) <--11: Overlap (let1-p)-(beta-v)--- P|-> lam(x’.M’[x’])@V’ -----------------------when M’|-> x6.PM’[x6], M|-> VM..
11: Overlap (let1-p)-(beta-v)--- P|-> lam(x’.M’[x’])@V’ -----------------------when M’|-> x6.PM’[x6], M|-> PM..
#Joinable! (Total 23 CPs)

The four CPs above are caused by a single CP (11:) generated by an overlap between (let1-p) and (beta-v) as

11: (lam(x’.M’[x’])@V’)@M(β-v)(let1-p)let(lam(x’.M’[x’])@V’,x.(x@M))

M’[V’]@M

This CP results from the fact that the non-value metavariable P in (let1-p) can match with the lhs
lam(x’.M’[x’])@V’ of (beta-v), which is the underlined part of the above CP. An important fact is that this is
not joinable at the level of rewriting on meta-terms. The right M’[V’]@M is a normal form, whereas the left is reduced to adifferent normal form by (beta-v) as

let(lam(x’.M’[x’])@V’, x.(x@M)) ⇒C let(M’[V’], x.(x@M))
However, this is call-by-value joinable (Deﬁnition 4.5), meaning that it is joinable by case analysis varying M,M’ overvalue/non-value metavariables. In the output presented above, the part like “when M’|-> x95.VM’[x95], M|-> PM”
denotes checking the case in which M’ is a value metavariable and M is a non-value metavariable. We have adopted anaming convention by which a metavariable starting with V is a value metavariable and a metavariable starting with P isa non-value metavariable (Deﬁnition 2.3). All possible instantiations of M,M’ as value/non-value metavariables are the fourcases described above. In each case, the left meta-term in a CP is reduced to the right meta-term.
Termination of λC has been proved [31]. Hence, by Theorem 4.9, we have object conﬂuence of lamC. This concludes thatthe λC -calculus is conﬂuent.
7. Example 3: coherence of skew-monoidal categories
We show a further example, which is different from the λ-calculus. A skew-monoidal category [32,33] is a category C
together with a distinguished object I, a functor ⊗ : C × C → C (monoidal product) and natural transformations

λA : I ⊗ A → A

ρA : A → A ⊗ I

α A , B ,C : ( A ⊗ B ) ⊗ C → A ⊗ ( B ⊗ C )subject to the axioms:

I⊗I

(a)
ρI

(b) ( A ⊗ I) ⊗ BλII(c) (I ⊗ A ) ⊗ B
λ A ⊗id B

A⊗B

id A ⊗λ B

A⊗B
I ⊗ ( A ⊗ B)A⊗B(d) ( A ⊗ B ) ⊗ I
ρ A⊗B

λ A⊗B

α A , B ,IA⊗B

α A , B ⊗C , D(e) ( A ⊗ ( B ⊗ C )) ⊗ D

A ⊗ ( B ⊗ I)
id A ⊗ρ B

A ⊗ (( B ⊗ C ) ⊗ D )

α A , B ,C ⊗id D(( A ⊗ B ) ⊗ C ) ⊗ D

A ⊗ (I ⊗ B )ρ A ⊗id B

I
αI, A , B

α A ,I, B

id A ⊗α B ,C , D

α A ⊗ B ,C , D( A ⊗ B ) ⊗ (C ⊗ D )

α A , B ,C ⊗ D

A ⊗ ( B ⊗ (C ⊗ D ))

M. Hamana et al. / Science of Computer Programming 187 (2020) 102322

23

The idea of this categorical structure is as follows. A monoidal category [34] is a category equipped with a “monoidal”
product ⊗ and three natural isomorphisms λ, ρ , α , considered as the unit and associative “laws” for the monoidal product.
A skew-monoidal category is a variation of it, in which λ, ρ , α are just one-directional natural transformations, rather than
isomorphisms. Since skew-monoidal categories are related to relative monads [35], these are related to computer science.
Uustalu [33] proved a remarkable property called coherence, which states that every formal arrow having a certain formof codomain has a unique normal form under the axioms of skew-monoidal category. His proof employed normalisation byevaluation technique. Here we show the unique normal form property by a different technique, namely, our critical pairchecking method for polymorphic computation rules using PolySOL.
7.1. Laws
Following Uustalu’s paper [33], the axioms of a skew-monoidal category C are equationally expressed as the following
laws on arrows of C , which we call SkewMon.

Laws of the composition(idL) id ◦ f = f(assoc) ( f ◦ g ) ◦ h = f ◦ ( g ◦ h)(idR) f = f ◦ id

Bi-functoriality of ⊗id A ⊗ id B = id A ⊗ B(⊗-id)(⊗-comp) (h ⊗ k) ◦ ( f ⊗ g ) = (h ◦ f ) ⊗ (k ◦ g )Laws of natural transformations λ, ρ , α(λ-nat) λ ◦ (id ⊗ f ) = f ◦ λ(ρ -nat) ( f ⊗ id) ◦ ρ = ρ ◦ f(α -nat) α ◦ ( f ⊗ g ) ⊗ h = f ⊗ ( g ⊗ h) ◦ α
Laws of skew monoidal category(a) λ ◦ ρ = id(c) λ ◦ α = λ ⊗ id(e) (id ⊗ α ) ◦ α ◦ (α ⊗ id) = α ◦ α(b) (id ⊗ λ) ◦ α ◦ (ρ ⊗ id) = id(d) α ◦ ρ = id ⊗ ρThese laws can be regarded as textual representation of basic commutative diagrams. Namely, these specify which twoarrows having the same source and target are equal (i.e. commute). For example, the law (e) is formally of the followingform: (idA ⊗ αB , C , D) ◦ αA , B ⊗ C , D ◦ (αA ⊗ B , C , D ⊗ idD) = αA , B , C ⊗ D ◦ αA ⊗ B , C , D : Hom(( A ⊗ B ) ⊗ C ) ⊗ D , A ⊗ ( B ⊗ (C ⊗ D )))This speciﬁes the equality of two arrows from ( A ⊗ B ) ⊗ C ) ⊗ D to A ⊗ ( B ⊗ (C ⊗ D )), equivalently saying that the diagram(e) commutes.
In the description of SkewMon, we omitted the subscripts of id, λ, ρ , α and types, but the laws oﬃcially have suitablesubscripts, contexts and types, as the above highlights. Note that different occurrences of “α” has different subscripts. Thisis actually the point we have mentioned in Problem 2 in §1.4. Describing correct subscripts manually for all the rules istedious, but necessary to check overlaps between rules.
Since conﬂuence implies the unique normal form property [12,7], we show conﬂuence of the computation rules obtained
from SkewMon by orienting the laws as left-to-right computation rules.
7.2. Proof with PolySOL
We formulate a skew-monoidal category by using a signature
sigskew = [signature|
times : Hom(a,c),Hom(b,d) -> Hom(Pr(a,b),Pr(c,d))app: Hom(b,c),Hom(a,b) -> Hom(a,c); id : Hom(a,a)
lmd: Hom(Pr(I,a),a); rho : Hom(a,Pr(a,I))
alpha : Hom(Pr(Pr(a,b),c),Pr(a,Pr(b,c)))|]where we assume the binary type constructors Hom and Pr for the hom-sets and the monoidal product ⊗, and the function
symbol times (which is written as the inﬁx “*” below) is for arrow’s ⊗, app (which is written as the inﬁx “@” below) forthe composition ◦ and the rest are for id, λ, ρ , α . We formulate the laws as computation rules in PolySOL, where capitalletters such as F,G are metavariables for arrows.
skew = [rule|(idL)
id @ F => F
(ox-id)id * id;(idR) F @ id => F
=> id

24

M. Hamana et al. / Science of Computer Programming 187 (2020) 102322(ox-comp) (H * K) @ (F * G)=> (H @ F) * (K @ G);(alpha-nat) alpha @ ((F * G) * H) => (F * (G * H)) @ alpha(lmd-nat)
lmd @ (id * F)=> F @ lmd(rho-nat)(F * id) @ rho=> rho @ F;(a) lmd @ rho
=> id
(b)
(id * lmd) @ (alpha @ (rho * id)) => id(b’) ((id * lmd) @ alpha) @ (rho * id) => id(c) lmd @ alpha => lmd * id(d) alpha @ rho => id * rho(e)(id * alpha) @ (alpha @ (alpha * id)) => alpha @ alpha(e’) ((id * alpha) @ alpha) @ (alpha * id) => alpha @ alpha|]The rules are straightforward implementation of the original laws, except for the following point:• We did not include the associative law of the composition:(assoc) (F @ G) @ H => F @ (G @ H)

• Instead, we added the laws (b’) and (e’), which are variants of (b) and (e), where we applied (assoc) to theirlhss.
The reason of this modiﬁcation is adding (assoc) as a rule greatly increases critical pairs. Since the lhss of almost all
rules of skew have the composition @, they overlap with the subterm (F @ G) of lhs of (assoc). Many CPs generated
by this way are not joinable. Therefore, we decided (assoc) should not be considered as a computation rule. Instead, we
regard @ as a ﬂatten composition operator like a string concatenation in string rewriting system.
By invoking the command “crity” for critical pair checking with types, PolySOL checks their critical pairs using theinferred well-typed rules. It reports one non-joinable critical pair out of 6.
*SOL> crity skew sigskew
1: Overlap (idL)-(idR)--- F’|-> id, F|-> id ----------------------------------(idL) (id@F) => F
(idR) F’@id => F’
id@id
id <-(idL)-∧-(idR)-> id---> id =OK= id <--2: Overlap (ox-comp)-(ox-id)--- H|-> id, K|-> id -----------------------------(ox-comp) (H * K)@(F * G) => (H@F) * (K@G)(ox-id) id * id => id(id * id)@(F * G)
(id@F) * (id@G) <-(ox-comp)-∧-(ox-id)-> id@(F * G)---> F * G =OK= F * G <--3: Overlap (ox-comp)-(ox-id)--- F|-> id, G|-> id -----------------------------(ox-comp) (H * K)@(F * G) => (H@F) * (K@G)(ox-id) id * id => id(H * K)@(id * id)(H@id) * (K@id) <-(ox-comp)-∧-(ox-id)-> (H * K)@id---> H * K =OK= H * K <--4: Overlap (lmd-nat)-(ox-id)--- F|-> id -----------------------------------------(lmd-nat) lmd@(id * F) => F@lmd(ox-id) id * id => id
lmd@(id * id)
id@lmd <-(lmd-nat)-∧-(ox-id)-> lmd@id---> lmd =OK= lmd <--5: Overlap (rho-nat)-(ox-id)--- F|-> id -----------------------------------------(rho-nat) (F * id)@rho => rho@F(ox-id) id * id => id(id * id)@rho
rho@id <-(rho-nat)-∧-(ox-id)-> id@rho---> rho =OK= rho <--6: Overlap (alpha-nat)-(ox-id)--- F|-> id, G|-> id ------------------------------(alpha-nat) alpha@((F * G) * H) => (F * (G * H))@alpha(ox-id) id * id => idalpha@((id * id) * H)
(id * (id * H))@alpha <-(alpha-nat)-∧-(ox-id)-> alpha@(id * H)---> (id * (id * H))@alpha =#= alpha@(id * H) <--#NON 1 joinable... (Total 6 CPs)

To make the non-joinable CP (6:) joinable, we add a new computation rule

M. Hamana et al. / Science of Computer Programming 187 (2020) 102322

25

skewext = [rule|(ext1)
alpha@(id * H) => (id * (id * H))@alpha |]This is a sound rule, because it is nothing but the naturality of α.

( A ⊗ B) ⊗ C
id A ⊗ B ⊗h

( A ⊗ B) ⊗ C

α A , B ,CA ⊗ (B ⊗ C )(ext1)

α A , B ,C

id A ⊗(id B ⊗h)A ⊗ (B ⊗ C )Note that each alpha and id in the rule (ext1) have oﬃcially different subscripts as the above diagram shows. They
are automatically supplied in PolySOL by the type inference algorithm.
The diagram shows also a “2-cell” (ext1) transforming the down-lower-right arrow to the upper-right-down arrow,
which is considered as a “proof” why the diagram commutes. Likewise, every rule in skew is considered as such a “proof”,
therefore if two arrows (represented as meta-terms) with the same source and target has the unique normal form using
skew, then it has a proof of commutativity.
We check again skew with the extended rule skewext.
*SOL> crity (skewext++skew) sigskew..
4: Overlap (alpha-nat)-(ox-id)--- F|-> id, G|-> id ---------------------------(alpha-nat) alpha@((F * G) * H) => (F * (G * H))@alpha(ox-id) id * id => idalpha@((id * id) * H)
(id * (id * H))@alpha <-(alpha-nat)-∧-(ox-id)-> alpha@(id * H)---> (id * (id * H))@alpha =OK= (id * (id * H))@alpha <--..
7: Overlap (ext1)-(ox-id)--- H|-> id -----------------------------------------(ext1) alpha@(id * H) => (id * (id * H))@alpha(ox-id) id * id => idalpha@(id * id)(id * (id * id))@alpha <-(ext1)-∧-(ox-id)-> alpha@id---> alpha =OK= alpha <--#Joinable! (Total 7 CPs)

PolySOL reports 7 critical pairs, which are all successfully joinable. This shows local conﬂuence of the computation system (skewext++skew). We next consider critical pairs generated by the ﬂatten composition. This is by computing
overlaps between two rules l1 ⇒ r1 and l2 ⇒ r2 , where the preﬁx (w.r.t. the composition) of l1 is uniﬁable with the suﬃx
(w.r.t. the composition) of l2 , as critical pairs of string rewriting. There are 7 overlaps: (b)-(e), (λ-nat)-(e), (λ-nat)-(ρ -nat),(ρ -nat)-(b), (ρ -nat)-(e), (α -nat)-(c), (c)-(d) and all of these are joinable.
Finally, we check strong normalisation of skew using PolySOL’s command solsn.
*SOL> solsn skew sigskew..
This is a first-order system.
******** FO SN check ********
Check SN using NaTT (Nagoya Termination Tool)
Input TRS:
1: app(id(),F) -> F
2: app(F,id()) -> F
3: times(id(),id()) -> id()..
Direct POLO(bPol) ... removes: 4 8 1 3 5 10 7 14 12 11 9 13 6 2
times
w: 2 * x1 + 2 * x2 + 2
lmd
w: 1
id
w: 1
rho
w: 1
alpha
w: 4
app
w: x1 + 2 * x2 + 1
Number of strict rules: 0>>YES

Since the types of all the function symbols in sigskew are up to ﬁrst-order (N.B. Hom is just an algebraic data type
constructor, not the arrow type constructor), PolySOL tried to call an external ﬁrst-order termination checker NaTT (Nagoya
Termination Tool) [36], and NaTT succeeded in proving termination. The technique used there was to assign a polynomial
to each function symbol as[[⊗]](x1 , x2 ) = 2x1 + 2x2 + 2,[[◦]](x1 , x2 ) = x1 + 2x2 + 1,[[λ]] = [[id]] = [[ρ ]] = 1,[[α ]] = 4

26

M. Hamana et al. / Science of Computer Programming 187 (2020) 102322

Then all rules are strictly decreasing using the interpretation. Hence we conclude that it is conﬂuent, which implies that
SkewMon has the unique normal form property.
Moreover, we have an additional result: the theory of Skew is decidable, meaning that any equality on the arrows isdecidable and checked by rewriting to normal forms.
8. Implementation of PolySOL
In this section, we describe some details of the PolySOL system. The PolySOL system consists of about 8000 line Haskell
codes, and works on GHCi, the interpreter of Glasgow Haskell Compiler (tested on version 7.6.2 and 8.0.2). PolySOL uses
Template Haskell [16] with a custom parser generated by Alex (for lexer) and Happy (for parser) to provide a readable
notation for signatures and rules. There is a command line interface using GHCi (§8.2). There is also a web interface (§8.3).
8.1. Syntax
PolySOL’s language is realised as an embedded domain speciﬁc language in Haskell by using the quasi-quotation featureof Template Haskell. The syntax [signature|..] and [rule|..] are quasi-quotations, and the keywords signatureand rule are implemented as “quasi-quoters” of Template Haskell, which parse the contents of strings and return thealgebraic data of parse trees. PolySOL’s syntax has a simple layout rule. Newline is regarded as a separator of declarations
in signature and rules. For example,
sig = [signature|lam : (a -> b) -> Arr(a,b)
app : Arr(a,b),a -> b|]

If one wants to write the declarations sequentially, one can also use the semicolon “;” for the separator, e.g.
sig = [signature| lam : (a -> b) -> Arr(a,b) ;app : Arr(a,b),a -> b |]The label for a rule is a string starting with a lower case letter, enclosed by round brackets, such as “(beta)”, which isplaced before a rule.
PolySOL has the following naming rule for identiﬁers. The start symbol of an identiﬁer should be• function symbol: lower case letter, e.g., lam, app• metavariable: capital letter, e.g., M, N1• (bound) variable: lower case letter, e.g., x, y0• type constructor: capital letter, e.g., Arr, Hom• type variable: lower case letter, e.g. a, b
8.2. The command line interface
The command line interface is the most fundamental use of PolySOL. The user invokes GHCi and loads a ﬁle containing
the deﬁnition of signature and rules. For example, by invoking% ghci 01need.hs

PolySOL starts with loading the ﬁle “01need.hs”, which contains the line
import SOL

to import PolySOL system and deﬁnitions siglamC and lamC given in §6. The ﬁle “01need.hs” is also available in the
web inference.
To check conﬂuence or strong normalisation of the computation system, the user invokes a SOL’s command implemented
as a Haskell function such as*SOL> criCBV lamC siglamCfor critical pair checking of computation using value/non-value distinction in §6. Another example is*SOL> crity skew sigskew

for critical pair checking with types as done in §7.
PolySOL has the following commands implemented as Haskell functions:M. Hamana et al. / Science of Computer Programming 187 (2020) 102322

Result
YES
NO
MAYBE
TOTAL

CSI^ho
49
15
30
94

27

PolySOL
66
16
12
94

The table shows the number of decided results by each tool. The result YES/NO is a decided result of CR. MAYBE is a result when thetool cannot decide. The total of a tool is the number of problems. The results and detailed outputs of each tool in the competition wererecorded in the oﬃcial site: http://cops.uibk.ac.at/results/?y=2018&c=HRS.
Fig. 9. Results of HRS category in Conﬂuence Competition 2018.

• criCBV <rules> <signature>
Enumerating critical pairs of a polymorphic computation system using value/non-value distinction.

• crity <rules> <signature>
Enumerating critical pairs of a polymorphic computation system.

• sn <rules> <signature>
Checking SN of a computation system using the General Schema criterion.

• solsn <rules> <signature>
Checking SN of a computation system using multiple methods.

• cr <rules> <signature>
Checking conﬂuence of a computation system using multiple methods.
8.3. Web interface
There is also a web interface for PolySOL, which is available at the ﬁrst author Makoto Hamana’s homepage. The examples in this paper have been stored in the web interface and one can chose an example from the pull-down menu.
PolySOL supports two ﬁle formats:• SOL format (.hs) implemented as a Haskell embedded domain speciﬁc language used throughout the paper, and• TRS format (.trs) used in the Conﬂuence Competition.
The TRS format is also used in the evaluation discussed in the next section.
9. Evaluation
9.1. Results in Conﬂuence Competition 2018
PolySOL participated in the Higher-Order Rewriting (HRS) category of the International Conﬂuence Competition 2018
(CoCo’18)1 held at the Federated Logic Conference (FLoC 2018) in Oxford, U.K. [37].
This event had automatic tools competing for the number of decided results of conﬂuence problems. We inferred thatparticipation in the competition would demonstrate how PolySOL was more effective than existing tools.
In the HRS category, 94 problems of higher-order rewrite systems (which are only simply-typed, not polymorphic) [8,9] were given. Because our polymorphic computation systems subsume the second-order fragment of higher-order rewrite
systems, PolySOL is able to address the simply-typed conﬂuence problems that are provided for the competition. We haveadapted PolySOL to support the TRS format, which is the format of rewrite systems in the competition.
Two tools participated in the HRS category: CSI^ho [38] and PolySOL (named SOL there). Results show that PolySOL
solved more problems than CSI^ho (see Fig. 9). This outcome derives from the fact that PolySOL implemented new criteriaof conﬂuence, strong closedness, and modular checking developed in §5.

9.2. Benchmark
To assess the behaviour of these tools more precisely, we again tested the tools against the problems of the Conﬂuence
Computation 2018 in our own environment. We conducted the benchmark test on a machine with Intel(R) Xeon E7-4809,
2.00 GHz 4 CPU (8 cores each), 256 GB memory, Red Hat Enterprise Linux 7.3, and timeout set to 120 s. The results aredescribed on a relevant web page2 . We excerpt the results of problems 514–789 in Fig. 10 with short comments in theﬁnal column of the table. Comments show the methods used by PolySOL to solve problems. The new conﬂuence criteria

1
2

Conﬂuence Competition oﬃcial site: http://project-coco.uibk.ac.at/2018/.
http://www.cs.gunma-u.ac.jp/hamana/polysol/scpro.html

28

M. Hamana et al. / Science of Computer Programming 187 (2020) 102322
Prob. No.

CSI^ho(sec.)PolySOL(sec.)

514
515
516
517
518
723
724
725
726
727
728
729
730
746
747
748
749
750
751
752
758
759
764
766
767
768
769
772
773
775
776
777
780
781
782
783
784
785
789

YES
YES
YES

1.448
0.772
1.459
0.482
0.617
58.633
0.734
0.747
0.676
0.656
58.63758.703
0.698
0.517
0.586
0.508
0.559
0.669
0.689
0.671
0.631
58.642
0.635
0.566
0.594
2.052
0.504
58.5660.59
58.70558.7210.699
0.611
58.71958.57158.573
0.656
0.645
0.5

YES
YES
YES
NO
NO

0.412
0.032
0.041
0.03
0.043
0.489
0.023
0.041
0.03
0.023
0.33
0.341
0.614
0.023
0.029
0.316
0.05
0.046
0.045
0.319
0.079
0.039
0.03
0.023
0.302
0.279
0.038
0.027
0.035
0.026
15.117
0.038
0.239
0.186
0.028
0.027
0.054
0.059
0.027

MAYBE
MAYBE
MAYBE

YES
NO
YES
NO
MAYBE
MAYBE

YES
MAYBE
MAYBE
MAYBE
MAYBE
MAYBE
MAYBE
MAYBE
MAYBE
MAYBE

NO
NO
NO
MAYBE
MAYBE
MAYBE
MAYBE
MAYBE
MAYBE

NO
MAYBE
MAYBE
MAYBE
MAYBE
MAYBE
MAYBE
MAYBE

MAYBE

YES
NO
YES
NO
YES
MAYBE

YES
MAYBE
MAYBE
MAYBE

NO
YES
YES
MAYBE

NO
MAYBE

NO
MAYBE
MAYBE

YES
YES
YES
NO
YES
YES
NO
YES
YES
YES
YES
MAYBE
MAYBE
MAYBE

Used method

non-joinable CP checknon-joinable CP checkjoinable CP checknon-joinable CP checkjoinable CP checkjoinable CP checknon-joinable CP checkjoinable CP checkjoinable CP checkstrong closedness
non-joinable CP checkstrong closedness
modularity
joinable CP checkstrong closedness
strong closedness
strong closedness

The unit of checking time shown in the next column of each result is second.
Fig. 10. Detailed results for problems used in Conﬂuence Competition 2018 (excerpt).

are effective. CSI^ho reports counter-examples to conﬂuence for some cases (problems 766 and 767) that PolySOL cannot
ﬁnd. After the competition, we improved PolySOL for more exact matching with the speciﬁcations of rewrite systems usedin the competition. For this reason, some results of PolySOL in the above benchmark URL show changes or improvementsfrom those in the competition.
9.3. On checking speed
Another interesting point in this benchmark is checking speed. Results show that PolySOL is more than 10 times fasterthan CSI^ho for almost all of the problems. One reason might be that PolySOL has its own termination checker, which
is simple and fast [1]. However, CSI^ho sometimes calls an external higher-order termination checker, which is generally
expensive. For PolySOL, we directly implemented the theory of conﬂuence checking developed in this paper using no clever
implementation trick. The benchmark result demonstrates that, for the case of conﬂuence, such a simple and theoreticallysound strategy is an effective method to implement an automated checking tool.
10. Summary and related work
10.1. Summary
We have presented a new framework of polymorphic computation rules that can accommodate a distinction between
values and non-values. The framework was demonstrated to be suitable for formulating and analysing fundamental calculi
of programming languages. We have given a type inference algorithm and criteria to check the conﬂuence property ofpolymorphic rules. These have provided a handy method to prove conﬂuence of polymorphic second-order computation
rules with call-by-value. We have demonstrated the effectiveness of our methodology by examining sample calculi using
our automated conﬂuence checking tool, PolySOL.

M. Hamana et al. / Science of Computer Programming 187 (2020) 102322

29

10.2. Related work
Mayr and Nipkow studied critical pairs for the conﬂuence of higher-order rewrite systems [8,9]. Their rewrite rule format
was rules on simply-typed λ-terms modulo β η -equivalence. There are no polymorphic types nor value/non-value distinctions. Therefore, no example (λC , λneed and skew monoidal category) which has conﬂuence described in this paper can beformulated directly or can be checked in their framework.
The systems ACPH [39] and CSI^ho [38] can automatically check conﬂuence of higher-order rules. They are based on theMayr–Nipkow higher-order rule format. Therefore, these tools have neither features of polymorphic types nor value/nonvalue distinction. Therefore, all of our examples are beyond the scope of the existing conﬂuence checking systems. In thisrespect, this report is the ﬁrst description of our system, to the best of our knowledge, the ﬁrst automatic tool that cancheck conﬂuence of the call-by-value variants of the λ-calculus directly, as described in the paper.
A framework of polymorphic higher-order rewrite rules was presented by Jouannaud et al. [40,41]. Our framework
is similar, but with several fundamentally important differences. For instance, our framework is based on (polymorphic)
second-order algebraic theories [3,42], whereas theirs is based on a polymorphic λ-calculus. The main purpose of [40,41]
was establishment of a termination criterion for higher-order rewrite rules. The issue of conﬂuence of polymorphic rules
has remained unaddressed. To the best of our knowledge, the present paper is the ﬁrst to describe a study of conﬂuence ofa general kind of polymorphic second-order rewrite rules.
We presented a type inference algorithm of polymorphic computation rules, which has not been given in the context ofrewriting theory, although it might be standard in the context of the theory of programming languages. Lack of a suitable
type inference algorithm in the theory of rewriting has affected existing higher-order conﬂuence tools such as ACPH and
CSI^ho. These tools force the user to write more detailed type information in rewrite rule speciﬁcations than PolySOL. The
user needs to declare all free and bound variables used in the rules, with their types. Actually, PolySOL’s rule speciﬁcation
is simpler because of the type inference. Our algorithm might also be beneﬁcial to other tools to improve this situation.
For our earlier work [1], we developed a simply-typed framework of second-order equational logic and computation
rules. We also developed a tool SOL for checking methods of termination conﬂuence. It lacked proper polymorphism andthe treatment of call-by-value. For that reason, the examples examined in this paper could not be handled directly.
Our earlier paper [42] presented a general framework of multiversal polymorphic algebraic theories based on polymorphic abstract syntax [43], and developed polymorphic equational logic and their algebraic models. It admits multiple typeuniverses and higher-kinded polymorphic types, hence it is richer than the present setting. However, we developed neither
polymorphic computation rules, call-by-value, nor their conﬂuence.
Acknowledgements
The ﬁrst author is grateful to Masahito Hasegawa for his question about methods to check conﬂuence of Moggi’s computational λ-calculus using the earlier tool, SOL. The author was thereby enlightened to the necessity of proper treatment ofcall-by-value calculi, which led to the framework described in this paper. This work was partly supported by JSPS KAKENHI
Grant Numbers JP17K00092, JP17K00005 and JP19K11891.
References[1] M. Hamana, How to prove your calculus is decidable: practical applications of second-order algebraic theories and computation, Proc. ACM Program.
Lang. 1 (22) (2017) 1–28.
[2] M. Fiore, C.-K. Hur, Second-order equational logic, in: Proc. of CSL’10, in: LNCS, vol. 6247, 2010, pp. 320–335.
[3] M. Fiore, O. Mahmoud, Second-order algebraic theories, in: Proc. of MFCS’10, in: LNCS, vol. 6281, 2010, pp. 368–380.
[4] S. Staton, An algebraic presentation of predicate logic, in: Proc. of FoSSaCS’13, 2013, pp. 401–417.
[5] S. Staton, Instances of computational effects: an algebraic perspective, in: Proc. of LICS’13, 2013, pp. 519–528.
[6] S. Staton, Algebraic effects, linearity, and quantum programming languages, in: Proc. of POPL’15, 2015, pp. 395–406.
[7] F. Baader, T. Nipkow, Term Rewriting and All That, Cambridge University Press, 1998.
[8] T. Nipkow, Higher-order critical pairs, in: Proc. 6th IEEE, in: Symp. Logic in Computer Science, 1991, pp. 342–349.
[9] R. Mayr, T. Nipkow, Higher-order rewrite systems and their conﬂuence, Theor. Comput. Sci. 192 (1) (1998) 3–29.
[10] G.D. Plotkin, Call-by-name, call-by-value and the lambda-calculus, Theor. Comput. Sci. 1 (2) (1975) 125–159.
[11] J. Maraist, M. Odersky, P. Wadler, The call-by-need lambda calculus, J. Funct. Program. 8 (3) (1998) 275–317.
[12] G. Huet, Conﬂuent reductions: abstract properties and applications to term rewriting systems, J. ACM 27 (4) (1980) 797–821.
[13] Y. Ohta, M. Hasegawa, A terminating and conﬂuent linear lambda calculus, in: Proc. of RTA’06, 2006, pp. 166–180.
[14] D. Knuth, P. Bendix, Simple word problems in universal algebras, in: Computational Problem in Abstract Algebra, Pergamon Press, Oxford, 1970,
pp. 263–297.
[15] D. Miller, A logic programming language with lambda-abstraction, function variables, and simple uniﬁcation, J. Log. Comput. 1 (4) (1991) 497–536.
[16] T. Sheard, S.P. Jones, Template metaprogramming for Haskell, in: Proc. Haskell Workshop, 2002, 2002.
[17] H. Barendregt, The Lambda Calculus: Its Syntax and Semantics, North Holland, 1984.
[18] M. Hamana, Polymorphic rewrite rules: conﬂuence, type inference, and instance validation, in: Proc. of 14th International Symposium on Functionaland Logic Programming (FLOPS’18), in: LNCS, vol. 10818, 2018, pp. 99–115.
[19] M. Hamana, Universal algebra for termination of higher-order rewriting, in: Proc. of RTA’05, in: LNCS, vol. 3467, 2005, pp. 135–149.
[20] M. Hamana, Higher-order semantic labelling for inductive datatype systems, in: Proc. of PPDP’07, ACM Press, 2007, pp. 97–108.
[21] M. Hamana, Semantic labelling for proving termination of combinatory reduction systems, in: Proc. WFLP’09, in: LNCS, vol. 5979, 2010, pp. 62–78.
[22] M. Hamana, Free -monoids: a higher-order syntax with metavariables, in: Proc. of APLAS’04, in: LNCS, vol. 3302, 2004, pp. 348–363.

30

M. Hamana et al. / Science of Computer Programming 187 (2020) 102322[23] M. Hamana, Correct looping arrows from cyclic terms: traced categorical interpretation in Haskell, in: Proc. of FLOPS’12, in: LNCS, vol. 7294, 2012,
pp. 136–150.
[24] L. Damas, R. Milner, Principal type-schemes for functional programs, in: Proc. POPL’82, 1982, pp. 207–212.
[25] R. Milner, Communicating and Mobile Systems – The π -Calculus, CUP, 1999.
[26] T. Suzuki, K. Kikuchi, T. Aoto, Y. Toyama, Critical pair analysis in nominal rewriting, in: Proc. of SCSS’16, 2016, pp. 156–168.
[27] P. Aczel, A General Church-Rosser Theorem, Tech. rep., University of Manchester, 1978.
[28] M. Hamana, K. Matsuda, K. Asada, The algebra of recursive graph transformation language UnCAL: complete axiomatisation and iteration categoricalsemantics, Math. Struct. Comput. Sci. 28 (2) (2018) 287–337, https://doi.org/10.1017/S096012951600027X.
[29] E. Moggi, Computational Lambda-Calculus and Monads, LFCS ECS-LFCS-88-66, University of Edinburgh, 1988.
[30] A. Sabry, P. Wadler, A reﬂection on call-by-value, ACM Trans. Program. Lang. Syst. 19 (6) (1997) 916–941.
[31] S. Lindley, I. Stark, Reducibility and -lifting for computation types, in: Proc. of TLCA’05, 2005, pp. 262–277.
[32] K. Szlachányi, Skew-monoidal categories and bialgebroids, Adv. Math. 231 (3–4) (2012) 1694–1730.
[33] T. Uustalu, Coherence for skew-monoidal categories, in: Proc. 5th Workshop on Mathematically Structured Functional Programming, MSFP’14, 2014,
pp. 68–77.
[34] S. Mac Lane, Categories for the Working Mathematician, Graduate Texts in Mathematics, vol. 5, Springer-Verlag, 1971.
[35] T. Altenkirch, J. Chapman, T. Uustalu, Monads need not be endofunctors, Log. Methods Comput. Sci. 11 (1) (2015).
[36] A. Yamada, K. Kusakari, T. Sakabe, Nagoya termination tool, in: Proc. Joint 25th RTA and 12th TLCA, in: LNCS, vol. 8560, 2014, pp. 466–475.
[37] T. Aoto, M. Hamana, N. Hirokawa, A.M.J. Nagele, N. Nishida, K. Shintani, H. Zankl, Conﬂuence Competition 2018, in: Proc. of 3rd International Conference
on Formal Structures for Computation and Deduction, FSCD 2018, in: LIPIcs, vol. 108, 2018, chap. 32, 5 pp.
[38] J. Nagele, B. Felgenhauer, A. Middeldorp, CSI: new evidence – a progress report, in: Proc. of CADE’17, in: LNCS (LNAI), vol. 10395, 2017, pp. 385–397.
[39] K. Onozawa, K. Kikuchi, T. Aoto, Y. Toyama, ACPH: system description, in: 6th Conﬂuence Competition (CoCo 2017), 2017, p. 76.
[40] J.-P. Jouannaud, A. Rubio, Polymorphic higher-order recursive path orderings, J. ACM 54 (1) (2007) 2, 48 pp.
[41] J.-P. Jouannaud, A. Rubio, Normal higher-order termination, ACM Trans. Comput. Log. 16 (2) (2015) 13, 38 pp.
[42] M. Fiore, 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, 2013, pp. 520–529.
[43] M. Hamana, Polymorphic abstract syntax via Grothendieck construction, in: FoSSaCS’11, in: LNCS, vol. 3467, 2011, pp. 381–395.