Term Evaluation Systems with Refinements:
First-Order, Second-Order, andContextual Improvement
Koko Muroya1[0000−0003−0454−6900] and Makoto Hamana2[0000−0002−3064−8225]
1

RIMS, Kyoto University, Japan
kmuroya@kurims.kyoto-u.ac.jp
2
Kyushu Institute of Technology, Japan
hamana@cs.gunma-u.ac.jp

Abstract. For a programming language, there are two kinds of term rewriting: run-time rewriting (“evaluation”) and compile-time rewriting (“refinement”).
Whereas refinement resembles general term rewriting, evaluation is commonly
constrained by Felleisen’s evaluation contexts. While evaluation specifies a programming language, refinement models optimisation and should be validatedwith respect to evaluation. Such validation can be given by Sands’ notion ofcontextual improvement. We formulate evaluation in a term-rewriting-theoreticmanner for the first time, and introduce Term Evaluation and Refinement Systems(TERS). We then identify sufficient conditions for contextual improvement, andprovide critical pair analysis for local coherence that is the key sufficient condition. As case studies, we prove contextual improvement for a computational
lambda-calculus and its extension with effect handlers.
Keywords: term rewriting · evaluation contexts · critical pair analysis

1

Introduction

Term rewriting is a general model of computation. The ecosystem of a functional programming language utilizes two types of term rewriting: run-time rewriting, which weshall refer to as evaluation, and compile-time rewriting, referred to as refinement. Runtime evaluation specifies operational semantics of the language. It can only happen in aparticular order, usually deterministically. On the other hand, compile-time refinement
models optimisation. It can happen anywhere, nondeterministically. The difference between evaluation and refinement, as kinds of term rewriting, can be summarised in termsof contexts, cf. Fig. 1. Evaluation →E uses a rewrite rule l → r inside a Felleisen’s evaluation context [9, 8] E ∈ Ectx only; this is a new kind of restriction from the rewriting
theoretic point of view. In contrast, refinement ⇒R uses a rewrite rule l ⇒ r inside anarbitrary context C ∈ Ctx; this resembles general term rewriting.
From the viewpoint of rewriting theory, the roles of evaluation and refinement are
rather unusual. It is evaluation that specifies (the behaviour of) a programming language as operational semantics. Evaluation is not simply a deterministic restriction ofrefinement. Refinement which models optimisation should be validated with respect to2

K. Muroya and M. Hamana(l → r) ∈ E E ∈ Ectx
E[lθ] →E E[rθ](l ⇒ r) ∈ R C ∈ Ctx
C[lθ] ⇒R C[rθ]

Fig. 1. Evaluation and refinement relations, where θ is a substitution

evaluation. Indeed, compiler optimisation is meant to preserve evaluation results andimprove time efficiency of evaluation. This preservation and improvement deserve formal validation.
Such validation can be provided as observational equivalence [22], and its quantitative variant, contextual improvement [27]. Observational equivalence t  u assertsthat two terms t and u cannot be distinguished by any context C; formally, if C[t] terminates, C[u] terminates with the same evaluation result, and vice versa. Contextual
improvement additionally asserts that C[u] terminates with no more evaluation steps
than C[t]. This is a suitable notion to validate refinement which models optimisation.
Whereas the theory of refinement, which resembles general term rewriting, has been
deeply developed, evaluation seems to be a new kind of restricted rewriting and it lacks
a general theory from the perspective of term rewriting. This prevents useful ideas andtechniques of term rewriting from transferring from refinement to evaluation. In recent
work [23] on a proof methodology of observational equivalence, it is informally observed that a rewriting technique can be useful for proving observational equivalence
and contextual improvement. This methodology informally employs critical pair analysis, a fundamental technique in rewriting theory. The idea is that t  u holds if replacing
t with u (which means applying a refinement rule t ⇒ u) in any program does not conflict with any evaluation rule l → r.
This paper aims at formalising this connection between observational equivalence
proofs and critical pair analysis. In doing so, we introduce a new rewriting-theoretic
formalisation of evaluation. Our contributions are:• introducing a new formalisation of term evaluation systems (TES), and its combination with refinement, dubbed term evaluation and refinement systems (TERS), in
both first-order and second-order settings,• identifying sufficient conditions for contextual improvement that include a notionof local coherence,• establishing critical pair analysis for local coherence, and• demonstrating TERS with examples including a computational lambda-calculus
and its extension with effect handlers.
The key concepts of our development are evaluation contexts, values and local coherence. Evaluation contexts are treated axiomatically. Values specify successful resultsof evaluation; not all normal forms of evaluation are deemed successful. Such distinction of values has been studied in second-order rewriting [14]. Finally, local coherenceis a notion from the rewriting literature; it is namely a sufficient condition for confluenceTerm Evaluation Systems

3in equational rewriting [15, 3]. We exploit the notion for TERS instead of equational
rewriting3 .
1.1

Examples of TES and TERS

The standard left-to-right call-by-value lambda-calculus is a TES. Terms t, t0 including
values v are defined as below, and the call-by-value evaluation strategy is specified using
evaluation contexts E and one evaluation rule →:v ::= λx.t,t, t0 ::= x | v | t t0 ,E ::=  | E t | v E,

(λx.t) v → t[v/x].

Values v appearing in this specification play a significant role. The definition of evaluation contexts notably includes the clause v E where the left subterm v is restricted tovalues. This ensures the left-to-right evaluation of application t t0 ; the right subterm t0
can be evaluated only after the left subterm t has been evaluated to a value. Additionally,
the redex (λx.t) v restricts the right subterm v to values. This ensures the call-by-value
evaluation of application.
A simplified computational lambda-calculus λml∗ [26] is a TERS. Its terms are either
values v, v0 or computations p, p0 , and its evaluation (which has been studied [7]) is
specified using evaluation contexts E and two evaluation rules →:v, v0 ::= x | λx.p,p, p0 ::= return(v) | let x = p in p0 | v v0 ,E ::=  | let x = E in p, (λx.p) v → p[v/x], let x = return(v) in p → p[v/x].
We can observe that evaluation contexts constrain where evaluation rules can be applied,
namely in the subterm p of let x = p in p0 . Again, values in evaluation rules assure
the call-by-value evaluation of application and let-binding.
Originally, the calculus λml∗ is specified by equations rather than evaluation. Directed equations can be seen as the following five refinement rules ⇒:(λx.p) v ⇒ p[v/x],
λx.v x ⇒ v,

let x = return(v) in p ⇒ p[v/x],
let x = p in return(x) ⇒ p,

let x1 = (let x2 = p2 in p1 ) in p3 ⇒ let x2 = p2 in let x1 = p1 in p3 .
While the first two rules represent β-conversion, the third one represents η-conversion.
The fourth one removes the trivial let-binding, and the last one flattens let-bindings. We
can observe that the last three rules simplify terms.
We now have a TERS of λml∗ which has both evaluation and refinement. We are
now interested in whether refinement is valid with respect to evaluation. Our goal hereis namely to prove contextual improvement: that is, for any refinement t ⇒R u and any
context C ∈ Ctx, if evaluation of C[t] terminates, then evaluation of C[u] terminateswith no more evaluation steps.
To prove contextual improvement, we would need to analyse how each evaluation
step interferes with the refinement t ⇒R u. This amounts to analyse how each evaluation
3

TERS is not equational rewriting. Refinement is compile-time rewriting, and we do not evaluate modulo refinement.

4

K. Muroya and M. Hamana

E[lθ]
s

%

|
∗

" 0y
s

E[lθ]
E[rθ]

∗

s

x

%

E[lθ]
E[rθ]

" 0 u}

s
l

s

%
x



s0 ks

E[rθ]

k

∗

u

(1 + k ≥ l)

Fig. 2. Joinability for confluence, commutation and local coherence

rule l → r can conflict with each refinement rule l0 ⇒ r0 . This is what exactly criticalpair analysis is targeted at.
Critical pair analysis is usually for proving confluence, which is a fundamental property of term rewriting. It firstly enumerates the situation where two rewrite rules conflictwith each other. It then checks if the two conflicting rewritings can be joined. This is
illustrated in Fig. 2 (left), where the joining part is depicted in dashed arrows, and ‘∗’means an arbitrary number of rewriting.
In our development, we exploit critical pair analysis for proving contextual improvement, and more specifically for proving local coherence. The analysis is targetedat conflicts between evaluation → and refinement ⇒. We analyse if these conflicts canbe joined using evaluation and refinement; see Fig. 2 (right). To ensure improvement,
our notion of local coherence asserts that the joining part satisfies the inequality 1+k ≥ labout the number of evaluation steps.
To prove the joinability for local coherence, we need to be careful with evaluationkcontexts. We need to show that the 1 + k evaluation steps E[lθ] →E E[rθ] →E u canlbe simulated by the l evaluation steps s →E s0 . Naively, this can be done by showingthat the evaluation rule l → r can also be applied to the term s. This, however, involves
making sure that the rule l → r can be applied inside an evaluation context. This is nota trivial issue; the evaluation context E might be modified by the refinement E[t] ⇒R s.
This modification should be “mild”, and more precisely, refinement should not turn anevaluation context into a non-evaluation context (see Def. 12 (2)).
Note that local coherence can be seen as a generalisation of commutation [30]; see
Fig. 2 (middle). Commutation is the case where k = 0, l = 1, and allowing only one∗
step of refinement ⇒R instead of ⇒R .

2

Preliminaries

Let N be the set of natural numbers. For any n ∈ N, let [n] denote the set {1, . . . , n}(mind the starting point); for example, [0] = ∅, [1] = {1}, [2] = {1, 2}. We write A for asequence A1 , . . . , An , and |A| for its length (i.e. n).
∗Given a binary relation → on a set S , let → denote the reflexive and transitivekclosure of →. For any k ∈ N, → denotes the k-fold composition of →. An elementx ∈ S is a normal form (with respect to →), if there exists no element x0 ∈ S such thatx → x0 . Let NF(→) denote the set of normal forms with respect to →.

Term Evaluation Systems

35First-order Term Evaluation and Refinement Systems

Evaluation and refinement. Let Σ be a signature. Each element f ∈ Σ comes withan arity n ∈ N; we write f : n. (First-order) terms are defined by the grammar t ::= x |f (t1 , . . . , tn ) where x is a variable and f : n. Let TΣ be the set of terms. A term is closed
if it has no occurrence of variables.
A position of a term is given by a (possibly empty) sequence of positive numbers, inthe usual manner. Concatenation of sequences p, q is denoted by pq or p.q. Let Pos(t)be the set of all positions in a term t. We write s[t] p for the term that is obtained byreplacing the sub-term of s at the position p with t. We write s| p for the sub-term of s at
the position p.
A substitution θ is given by a sequence {x1 7→ t1 , . . . , xk 7→ tk } where x1 , . . . , xk
are distinct variables. We write subst θ when θ is a substitution. Let tθ denote the term
where all occurrences of x1 , . . . , xk in t are replaced by t1 , . . . , tk , respectively. We calltθ an instance of t.
A context is a term that involves exactly one hole . Let Ctx be the set of contexts. Let C[t] denote the term where the hole  of C ∈ Ctx is replaced by t. A set
C of contexts is closed under substitutions if C ∈ C implies Cθ ∈ C for any subst θ,and closed under composition if C, C 0 ∈ C implies C[C 0 ] ∈ C. The set C is inductive
if any C ∈ C is  or of the form f (t1 , . . . , ti−1 , C 0 , ti+1 , . . . , tn ) such that C 0 ∈ C andf (t1 θ, . . . , ti−1 θ, , ti+1 θ, . . . , tn θ) ∈ C for any subst θ.
Term evaluation systems (TES) can now be defined, as the standard term rewriting
with the new restriction imposed by means of evaluation contexts.
Definition 1 (TES). A term evaluation system is a tuple (Σ, E, Ectx, Val) consisting of– a signature Σ,– a set E of evaluation rules, where (l → r) ∈ E with l, r ∈ TΣ , such that (i) every freevariable occuring in r also occurs in l and (ii) l is not a variable,– a set Ectx ⊆ Ctx of evaluation contexts that is closed under substitutions, closed
under composition and inductive, and– a set Val ⊆ NF(→E ) of values that satisfies (i) v ∈ Val implies vθ ∈ Val for any
subst θ, and (ii) it comes with an equivalence relation =Val ⊆ Val × Val, where:– the evaluation relation →E ⊆ TΣ × TΣ is defined in Fig. 1.
Values specify which normal forms of →E are regarded as successful results. For
example, in a TES for arithmetics, a term x + y is a normal form but it is not deemed asuccessful result. The equivalence relation =Val specifies observations of these results interms of equivalence classes. For example, when the syntactic equality ≡ is used, eachvalue v ∈ Val becomes a distinct observation. On the other hand, when the total relation> is used, values are all identified; this means that successful termination is the only
possible observation.
The evaluation relation →E is closed under evaluation contexts in Ectx. It is also
closed under substitutions, thants to Ectx being inductive.
Each TES can be equipped with refinement, which resembles general, unrestricted,
term rewriting.
Definition 2 (TERS). A term evaluation and refinement system is a tuple (Σ, E, R, Ectx, Val)
consisting of6

K. Muroya and M. Hamana– A TES (Σ, E, Ectx, Val), and– a set R of refinement rules where (l ⇒ r) ∈ R with l, r ∈ TΣ , such that (i) every freevariable occuring in r also occurs in l and (ii) l is not a variable.
– The refinement relation ⇒R ⊆ TΣ × TΣ is defined by the inference rule in Fig. 1.
We often simply write a TES (E, Val) and a TERS (E, R, Val). The refinement relation ⇒R is closed under substitutions, and closed under arbitrary contexts in Ctx.
The following example is from the literature on context-sensitive rewriting.
Example 3 (Nats [20, Ex. 8.19]). Let Nats be the TERS defined as follows.
Signature ΣValues Val
Evaluation contexts Ectx
Evaluation rules E
nats → 0 : inc(nats)inc(x : y) → s(x) : inc(y)hd(x : y) → x
tl(x : y) → ynats : 0, inc : 1, hd : 1, tl : 1, ‘:0 : 2, s : 1, 0 : 0
V ::= 0 | s(V)E ::=  | hd(E) | tl(E) | inc(E)Refinement rule R
tl(inc(nats)) ⇒ inc(tl(nats))

We define =Val by the syntactic equality ≡, to allow each value to be observed separately.
The refinement rule is reversed, compared to the original one [20, Ex. 8.19], so that it
induces improvement; see Sec. 4 for details.
Joinability and improvement. Evaluation is constrained by means of evaluation contexts, usually to have the evaluation relation →E deterministic. Bridging the gap between evaluation and refinement, we are interested in joinability up to R defined asfollows. The joinability is quantitative with an extra constraint on the number of evaluation steps.
Definition 4 (Peaks, joinability).
– An E-peak is given by a triple (s1 , t, s2 ) such that t →E s1 and t →E s2 .
– An (R, E)-peak is given by a triple (s1 , t, s2 ) such that t ⇒R s1 and t →E s2 .
– An E-peak (s1 , t, s2 ) is trivial if s1 ≡ s2 holds.
– An (R, E)-peak (s1 , t, s2 ) is joinable up to R if there exist k, l ∈ N and u1 , u2 suchkl∗that s1 →E u1 , s2 →E u2 , 1 + l ≥ k and u2 ⇒R u1 .
Definition 5 (Rewriting properties).
– A TES (E, Val) is deterministic if every E-peak (s1 , t, s2 ) is trivial.
– A TERS (E, R, Val) is locally coherent if every (R, E)-peak is joinable up to R.
We say a TERS (E, R, Val) is deterministic if (E, Val) is deterministic. We also simply
say an (R, E)-peak is joinable, omitting “up to R.”
We formalise the key concept that relates evaluation with refinement in TERS. It is
the so-called (contextual) improvement [27]: that is, any refinement t ⇒R s cannot be
distinguished by evaluation →E inside any contexts, and the refinement cannot increase
the number of evaluation steps that are needed for termination. Observation is madeaccording to the set Val of values and its associated equivalence relation =Val .

Term Evaluation Systems

7

Definition 6 (Value-invariance, improvement).
– A TERS (E, R, Val) is value-invariant if, for any v ∈ Val and s ∈ TΣ , v ⇒R s impliess ∈ Val and v =Val s.
– For a TERS (E, R, Val), R is improvement w.r.t. E if, for any k ∈ N, v ∈ Val,kt ⇒R s and any C ∈ Ctx such that C[t], C[s] are closed terms, C[t] →E v impliesmC[s] →E v0 for some m ∈ N and v0 ∈ Val such that v =Val v0 and k ≥ m.
Improvement is notoriously difficult to directly prove, because of the universal
quantification over all contexts. The following is our first main theorem providing arewriting-theoretic sufficient condition for improvement, for deterministic TERS.
Theorem 7 (Sufficient condition for improvement: first-order version). If a TERS
(E, R, Val) is deterministic, value-invariant and locally coherent, then the set R of refinement rules is improvement w.r.t. the set E of evaluation rules.
This theorem requires to prove determinism, value-invariance and local coherence.
When a TERS is orthogonal, determinism boils down to showing that each term canbe uniquely decomposed into an evaluation context and a redex. In typical TERS, theequivalence relation =Val on values can be decided by simply comparing head symbols.
This makes it easy to verify value-invariance. We will show that local coherence can beshown by critical pair analysis in Sec. 4.

4

Critical pair analysis for local coherence

Critical pairs. The definition of critical pairs is standard; it resembles the definition ofcritical pairs for commutation [30]. Note that critical pairs are generated by two kindsof overlaps, due to asymmetry of (R, E)-peaks.
Definition 8 (Unifiers).
– A unifier between t and u is a substitution θ such that tθ = uθ.
– A most general unifier between t and u is given by a unifier θ between t and usuch that, for any unifier σ between t and u, there exists a substitution σ0 such thatσ = θσ0 .
Definition 9 (Overlaps). Let X1 , X2 ∈ {R, E}. Given rules (l1 _1 r1 ) ∈ X1 , (l2 _2r2 ) ∈ X2 and a substitution θ, a quadruple (l1 _1 r1 , l2 _2 r2 , p, θ) is an (X1 , X2 )overlap if it satisfies the following.
– The rules l1 _1 r1 and l2 _2 r2 do not have common variables.
– If p = ε, the rules l1 _1 r1 and l2 _2 r2 are not variants of each other.
– The sub-term l1 | p is not a variable, where p is a position of l1 .
– The substitution θ is a most general unifier between l1 | p and l2 .
Definition 10 (Critical pairs).
– The critical pair generated by an (R, E)-overlap (l1 ⇒ r1 , l2 → r2 , p, θ) is an (R, E)peak (r1 θ, l1 θ, (l1 θ)[r2 θ] p ).
– The critical pair generated by an (E, R)-overlap (l1 → r1 , l2 ⇒ r2 , p, θ) is an (R, E)peak ((l1 θ)[r2 θ] p , l1 θ, r1 θ).
Lemma 11. If a critical pair (t1 , s, t2 ) is joinable, then for any substitution θ, (t1 θ, sθ, t2 θ)
is a joinable (R, E)-peak.

8

K. Muroya and M. Hamanatl(inc(nats))ow+

tl(inc(0 : inc(nats)))inc(tl(nats))inc(tl(0 : inc(nats)))tl(s(0) : inc(inc(nats)))+sinc(inc(nats))
Fig. 3. Joinability of the critical pair

Critical pair theorem. To obtain the so-called critical pair theorem, we need to impose
extra conditions on TERS that are summarised below.
Definition 12 (Well-behaved TERS). A TERS (Σ, E, R, Ectx, Val) is well-behaved if itsatisfies the following.
1. For any C1 , C2 ∈ Ctx, if C1 [C2 ] ∈ Ectx then C1 , C2 ∈ Ectx.
2. For any E ∈ Ectx and C 0 ∈ Ctx, if E ⇒R C 0 then C 0 ∈ Ectx.
3. For any (l ⇒R r) ∈ R and any variable x, the following holds.
(a) The variable x appears at most once in l, and at most once in r.
(b) Let p be the position of x in l. For the position q of x in r, if l[] p ∈ Ectx thenr[]q ∈ Ectx.
4. For any (l →E r) ∈ E, any variable x appears at most once in l.
The condition (1) is usually satisfied by inductively-defined evaluation contexts.
The condition (2) was already discussed in Sec. 1.1. The other conditions are rather
technical (see Sec. A.3 for some details), but these are easy to verify.
Theorem 13 (Critical pair theorem). A well-behaved TERS is locally coherent if andonly if every critical pair is joinable.
The example. The TERS Nats in Example 3 is deterministic, value-invariant and locally coherent (Prop. 29 in Appendix). By Thm. 7, its refinement R is improvement
w.r.t. its evaluation E. In the proof of local coherence, we observe that the TERS Nats
has one critical pair; it is joinable as in Fig. 3. The direction of refinement, which wereversed compared to the original [20], is crucial. Refinement must not increase thenumber of evaluation steps.

5

Second-Order Term Evaluation and Refinement Systems

Next we extend our framework to the second-order setting. By second-order we mean touse second-order abstract syntax [12, 10], i.e. syntax with variable binding and metavariables. It allows us to formally deal with higher-order term languages as in second-orderalgebraic theories [11] and second-order computation systems [13, 14].

Term Evaluation Systems

9

Meta-terms. In addition to the countably infinite set X of variables, let Z be a countably
infinite set of metavariables. Each element M ∈ Z comes with an arity m ∈ N; we write
M : m. Let ≡ denote the syntactic equality on metavariables. Let Σ be a signature, eachof whose element f ∈ Σ comes with a sequence hn1 , . . . , nl i of natural numbers called abinding arity; we write f : hn1 . . . , nl i.
Let MΣ denote the set of meta-terms defined using the signature Σ, the set X ofvariables and the set Z of metavariables. A judgement Θ B Γ ` t consists of a set Θof metavariables, a set Γ of variables, and a meta-term t. A well-formed meta-term is ameta-term t such that a judgement Θ B Γ ` t is derivable by formation rules below forsome Θ, Γ. We assume that meta-terms are well-formed.
x∈Γ
ΘBΓ`x

(M : m) ∈ Θ {Θ B Γ ` ti }i∈[m]Θ B Γ ` M[t1 , . . . , tm ]( f : hn1 , . . . , nl i) ∈ Σ {Θ B Γ, xi ` ti }i∈[l]Θ B Γ ` f (x1 .t1 , . . . , xl .tl ){|xi | = ni }i∈[l]

In a meta-term f (x1 .t1 , . . . , xl .tl ), each xi .ti introduces bound variables xi . We assume the α-equivalence for bound variables. A meta-term M[t1 , . . . , tm ] is called a metaapplication. The arguments t1 , . . . , tm can be seen as explicit substitution for variables;
when a meta-term s substitutes the metavariable M, free variables of s gets substitutedby t1 , . . . , tm . A term is a meta-term that contains no meta-application. A term is closed
if it has no occurrence of variables.
A position of a meta-term is given by a (possibly empty) sequence of positive numbers. Let Pos(t) be the set of all positions in a meta-term t. We write s[t] p for the metaterm that is obtained by replacing the sub-term of s at the position p with t. We writes| p for the sub-term of s at the position p.
We say that a position p in a meta-term t is a metavariable position if t| p is a metaapplication, i.e., t| p = M[t1 , . . . , tn ]. This description includes the case t| p = M wheren = 0, for which we identify M[ ] with just a metavariable M.
A substitution θ is given by a sequence [M1 7→ x1 .s1 , . . . , Mk 7→ xk .sk ] such that:(i) M1 , . . . , Mk are distinct metavariables, and (ii) for some Θ, Γ and for each i ∈ [k],(Mi : |xi |) ∈ Z and Θ B Γ, xi ` si hold. We call Θ B Γ a support of θ, and write
substΘBΓ θ when θ is a substitution with a support Θ B Γ. We sometimes simply write
subst θ, omitting the support. Given a meta-term Θ, M1 : |x1 |, . . . , Mk : |xk | B Γ ` t, a
meta-term tθ is defined byxθ = x( f (x1 .t1 , . . . , xl .tl ))θ = f (x1 .t1 θ, . . . , xl .tl θ) si {(xi )1 7→ t1 θ, . . . , (xi )m 7→ tm θ} (∃i ∈ [k]. M ≡ Mi )(M[t1 , . . . , tm ])θ =  M[t θ, . . . , t θ](otherwise)
1m

The meta-term si {(xi )1 7→ t1 θ, . . . , (xi )m 7→ tm θ} is the result of standard (captureavoiding) substitution for variables. We call tθ an instance of t.
A meta-term is a higher-order pattern if each occurrence of meta-application has
the form M[x1 , . . . , xm ] such that x1 , . . . , xm are distinct bound variables.

10

K. Muroya and M. Hamana

A context C is a meta-term that involves exactly one hole . A context is flat if
any prefix of the position of the hole is not a metavariable position; e.g. f (x.) is aflat context, but M[] and M[ f (x.)] are not flat contexts. Let Ctx be the set of contexts. Let C[t] denote the term where the hole  of C ∈ Ctx is replaced by t. A set
C of contexts is closed under substitutions if C ∈ C implies Cθ ∈ C for any subst θ,and closed under composition if C, C 0 ∈ C implies C[C 0 ] ∈ C. The set C is inductive
if any C ∈ C is  or of the form f (t1 , . . . , ti−1 , C 0 , ti+1 , . . . , tn ) such that C 0 ∈ C andf (t1 θ, . . . , ti−1 θ, , ti+1 θ, . . . , tn θ) ∈ C for any subst θ.
Syntax classes. We introduce a notion of syntactic classification for terms, typicallyused for distingushing values and non-values, following [14]. In loc. cit., the callby-value lambda-calculus (dubbed λvalue -calculus) involves the following two syntax
classes of values and non-values.
ValuesV ::= x | λx.M

Non-values

P ::= M N

This also specifies two special names V, P of metavariables that are used for values
and non-values. In general, we define a set Sclass of names for syntax classes. Each
syntax class is associated with a BNF grammar to define a set of meta-terms. Every
metavariable is either associated with a syntax class and called “<syntax class name>metavariable”, or not associated and called general metavariable. Moreover, we assume
a default syntax class value to denote values.
For example, in the case of λvalue -calculus, we define Sclass = {values V ::= x |λx.M, non-values P ::= M N}. The metavariable V is called a value metavariable, andM is a general metavariable.
Substitutions must also be consistent with syntax classes. A substitution θ is valid
if for each assignment (M 7→ x.s) ∈ θ, M and s’s syntax class are the same, or if M
is a general metavariable then s can be arbitrary. We write valid θ when θ is a valid
substitution.
Composition of valid substitutions is again valid, under the assumption that eachsyntax class is closed under substitution: that is, for each syntax class, if a meta-term t
is included then tθ is also included, where θ is a substitution.
Evaluation and refinement. Second-order TES and TERS can now be defined, in an
analogous way to the first-order setting.
Definition 14 (Second-order TES). A second-order term evaluation system is a tuple(Σ, E, Ectx, Sclass) consisting of– a signature Σ,– a set E of evaluation rules, where (l → r) ∈ E with l, r ∈ MΣ , such that (i) every
free metavariable occuring in r also occurs in l and (ii) l is not a variable nor ametavariable,– a set Ectx ⊆ Ctx of flat contexts, called evaluation contexts, that is closed undersubstitutions, closed under composition and inductive, and– a set Sclass of syntax classes that includes a value class (V, Val) that satisfies (i)Val ⊆ NF(→E ), (ii) v ∈ Val implies vθ ∈ Val for any valid θ, and (iii) it comes withan equivalence relation =Val ⊆ Val × Val where:Term Evaluation Systems

11– the evaluation relation →E ⊆ MΣ × MΣ is defined in Fig. 1 where θ is valid.
The evaluation relation →E is closed under evaluation contexts in Ectx. It is closed
under substitutions, thanks to Ectx being an inductive set of flat contexts.
Definition 15 (Second-order TERS). A second-order term evaluation and refinement
system is a tuple (Σ, E, R, Ectx, Sclass) consisting of– A second-order TES (Σ, E, Ectx, Sclass), and– a set R of refinement rules where (l ⇒ r) ∈ R with l, r ∈ MΣ , such that (i) every
free metavariable occuring in r also occurs in l and (ii) l is not a variable nor ametavariable.
– The refinement relation ⇒R ⊆ MΣ × MΣ is defined in Fig.1 where θ is valid.
The refinement relation ⇒R is closed under arbitrary contexts in Ctx. It is not closed∗
under substitutions per se, but it satisfies the following: t ⇒R u implies tθ ⇒R uθ forany valid θ.
We also assume that the lhs of every rule is a Miller’s higher-order pattern [21] tomake unification decidable.
Joinability and improvement. The definitions of peaks, joinability (see Def. 4), rewriting properties (Def. 5), and improvement (Def. 6) are inherited from the first-order case.
Finally, the first main theorem (Thm. 7) also holds in the second-order setting:
Theorem 16 (Sufficient condition for improvement: second-order version). If a secondorder TERS (Σ, E, R, Ectx, Sclass) is deterministic, value-invariant and locally coherent,
then R is improvement w.r.t. E.
Examples. In the remainder of this section, we present three examples of TERS.
Example 17 (Left-to-right call-by-value lambda-calculus). A TERS CBVλ of theleft-to-right call-by-value lambda-calculus is defined as follows, where t is a term, v isa value, M is a general metavariable, and V is a value metavariable. We use syntactic
sugar λx.t ≡ λ(x.t), t u ≡ @(t, u).
Signature Σ
Syntax class Sclass
Evaluation contexts Ectx
Evaluation rules E(λx.M[x]) V → M[V]λ : h1i, @ : h0, 0i
valuesV ::= λx.t
E ::=  | E t | v E
Refinement rules R(λx.M[x]) V ⇒ M[V]λx.V x ⇒ V

We define =Val by the total relation >, namely λx.t =Val λy.u for arbitrary t, u ∈ MΣ . Thismeans that we observe only termination (since Val ⊆ NF(→E )), identifying all values.
Example 18 (A simplified computational lambda-calculus λml∗ [26, 7]). A notion ofevaluation for Sabry and Wadler’s computational lambda-calculus λml∗ [26] has beenstudied [7]. A TERS Compλml∗ of the computational lambda-calculus is defined inFig. 4. We use syntactic sugar λx.t ≡ λ(x.t), t u ≡ @(t, u). We define =Val by the total
relation >. This means we observe only termination (since Val ⊆ NF(→E )), identifying
all values.

12

K. Muroya and M. Hamana

Signature Σ

λ : h1i, @ : h0, 0i, let : h0, 1i, return : h0i

Syntax class Sclass
ValuesV, V 0 ::= x | λx.P
P, P0 ::= return(V) | let(P, x.P0 ) | V V 0

Computations

Evaluation contexts Ectx

E ::=  | let(E, x.P)

Evaluation rules E(λx.P[x]) V → P[V](1)

let(return(V), x.P[x]) → P[V](2)

Refinement rules R(λx.P[x]) V ⇒ P[V](r1)

let(return(V), x.P[x]) ⇒ P[V](r2)

λx.V x ⇒ V(r3)

let(P, x.return(x)) ⇒ P(r4)let(let(P1 , x1 .P2 [x1 ]), x2 .P3 [x2 ]) ⇒ let(P1 , x1 .let(P2 [x1 ], x2 .P3 [x2 ]))(r5)

Fig. 4. The TERS Compλml∗

Example 19 (Effect handlers [25]). A TERS Hndl is defined in Fig. 5, where V, V1 , V2
are value metavariables, H is a handler metavariable, and P, P1 , P2 , . . . are computation
metavariables.
We only consider two operations op1 , op2 and two handlers: handler1 for catching the first operation op1 and handler0 for catching no operation, for simplicity. Wechange the evaluation rule (7) to be the so-called shallow handling; the original, deep
handling, rule [25] can be accommodated to a TERS, but this TERS would not be wellbehaved4 .
We also select the refinement rules that do not correspond to an evaluation rule andthose whose lhs is a Miller’s higher-order pattern5 . The refinement rules are numberedaccording to the original presentation [25, Fig. 7].
We define =Val for the TERS Hndl as follows, where v is any value.
x =Val v

true =Val true

false =Val false

fun(x.p) =Val fun(x0 .p0 )handler1 (x.p, x.k.p1 ) =Val handler1 (x0 .p0 , x0 .k0 .p01 )handler0 (x.p) =Val handler0 (x0 .p0 )This means that we distinguish each ground type value (i.e. boolean value), and observe
merely termination for other values (i.e. functions and handlers), although the TERS
Hndl is untyped.
4More specifically, the metavariable P1 would appear twice in the rhs of the original rule of theevaluation rule (7).
5
The refinement rule (7) in [25, Fig. 7] is the only refinement rule whose lhs is not a Miller’shigher-order pattern.

Term Evaluation Systems
Signature Σtrue : h0i, false : h0i, fun : h1i, @ : h0, 0i, return : h0i, op1 : h0, 1i, op2 : h0, 1i,
handler1 : h1, 2i, handler0 : h1i, do : h0, 1i, if : h0, 0, 0i, with_handle : h0, 0i
Syntax class Sclass
functions
F ::= x | fun(x.P)
valuesV ::= true | false | F | H
handlers H ::= handler1 (x.P, x.k.P1 ) | handler0 (x.P)
computations
P, P1 , P2 ::= return(V) | op(V, y.P) | do(P1 , x.P2 )| if(V, P1 , P2 ) | F V | with_handle(H, P)
Evaluation contexts Ectx
E ::=  | do(E, x.P) | with_handle(H, E)
Evaluation rules E where i ∈ [2]do(return(V), x.P[x]) → P[V]do(opi (V, y.P1 [y]), x.P2 [x]) → opi (V, y.do(P1 [y], x.P2 [x]))if(true, P1 , P2 ) → P1
if(false, P1 , P2 ) → P2
fun(x.P[x]) V → P[V]In the following three rules, h1 ≡ handler1 (x.P[x], x.k.P1 [x, k]).
with_handle(h1 , return(V)) → P[V]with_handle(h1 , op1 (V, y.P0 [y])) → P1 [V, fun(y.P0 [y])]with_handle(h1 , op2 (V, y.P0 [y])) → op2 (V, y.with_handle(h1 , P0 [y]))In the following two rules, h0 ≡ handler0 (x.P[x]).
with_handle(h0 , return(V)) → P[V]with_handle(h0 , opi (V, y.P0 [y])) → opi (V, y.with_handle(h0 , P0 [y]))Refinement rules Rdo(P, x.return(x)) ⇒ P
do(do(P1 , x1 .P2 [x1 ]), x2 .P3 [x2 ]) ⇒ do(P1 , x1 .do(P2 [x1 ], x2 .P3 [x2 ]))fun(x.F x) ⇒ F
with_handle(handler0 (x.P[x]), P0 ) ⇒ do(P0 , x.P[x])

13

(1)
(2)
(3)
(4)
(5)
(6)
(7)
(8)
(9)
(10)
(r3)
(r4)
(r9)
(r13)

Fig. 5. The TERS Hndl

6

Second-order critical pair analysis for local coherence

Critical pairs. The following definitions are analogous to those of first-order TERS.
The definition of critical pairs is again standard, akin to commutation.
Definition 20 (Unifiers).
– A unifier between t and u is a valid substitution θ such that tθ = uθ.
– A most general unifier between t and u is given by a unifier θ between t and u suchthat, for any unifier σ between t and u, there exists a valid substitution σ0 such thatσ = θσ0 .
Definition 21 (Overlaps). Let X1 , X2 ∈ {R, E}. Given rules (l1 _1 r1 ) ∈ X1 , (l2 _2r2 ) ∈ X2 and a substitution θ, a quadruple (l1 _1 r1 , l2 _2 r2 , p, θ) is an (X1 , X2 )overlap if it satisfies the following.
– The rules l1 _1 r1 and l2 _2 r2 do not have common variables or metavariables.
– If p = ε, the rules l1 _1 r1 and l2 _2 r2 are not variants of each other.
– The sub-term l1 | p is not a meta-application, where p is a position of l1 .
– The substitution θ is a most general unifier between l1 | p and l2 .

14

K. Muroya and M. Hamana

Definition 22 (Critical pairs).
– The critical pair generated by an (R, E)-overlap (l1 ⇒ r1 , l2 → r2 , p, θ) is an (R, E)peak (r1 θ, l1 θ, (l1 θ)[r2 θ] p ).
– The critical pair generated by an (E, R)-overlap (l1 → r1 , l2 ⇒ r2 , p, θ) is an (R, E)peak ((l1 θ)[r2 θ] p , l1 θ, r1 θ).
Lemma 23. If a critical pair (t1 , s, t2 ) is joinable, then for any valid substitution θ,(t1 θ, sθ, t2 θ) is a joinable (R, E)-peak.
To obtain the so-called critical pair theorem, TERS need to be well-behaved again.
The following conditions are similar to the first-order case (see Def. 12), except for
the last two conditions which ensure that evaluation and refinement are consistent withsyntax classes.
Definition 24 (Well-behaved TERS). A TERS (Σ, E, R, Ectx, Sclass) is well-behaved
if it satisfies the following.
1. For any C1 , C2 ∈ Ctx, if C1 [C2 ] ∈ Ectx then C1 , C2 ∈ Ectx.
2. For any E ∈ Ectx and C 0 ∈ Ctx, if E ⇒R C 0 then C 0 ∈ Ectx.
3. For any (l ⇒R r) ∈ R and any metavariable N that is not a value metavariable, thefollowing holds.
(a) The metavariable N appears at most once in l, and at most once in r.
(b) Let p be the position of N in l. For the position q of N in r, if l[] p ∈ Ectx thenr[]q ∈ Ectx.
4. For any (l →E r) ∈ E, any metavariable N appears at most once in l.
5. For any (l ⇒R r) ∈ R and any valid θ, if lθ belongs to a class then rθ belongs to thesame class.
6. For any (l →E r) ∈ R and any valid θ, if lθ belongs to a class then rθ belongs to thesame class.
Theorem 25 (Critical pair theorem). A well-behaved TERS is locally coherent if andonly if every critical pair is joinable.
The three examples. The TERSs CBVλ, Compλml∗ and Hndl are deterministic, valueinvariant and locally coherent (Prop. 34, Prop. 35 & Prop. 36 in Appendix). By Thm. 7,
every refinement R in the examples is improvement w.r.t. the corresponding evaluation
E.

7

Related work

Unlike general term rewriting (i.e., refinement), evaluation that uses Felleisen’s evaluation contexts has received little attention in the rewriting literature. As an exception,
Faggian et al. [7, 6] studied evaluation for specific simplified computational lambdacalculi including λml∗ . They proved that refinement implies observational equivalence,crucially using the fact that refinement is confluent in these calculi. In contrast, we study
evaluation for general TERS. We identify sufficient conditions (e.g. local coherence) for
contextual improvement, not relying on confluence of refinement.

Term Evaluation Systems

15

In the first-order setting, Lucas’ context-sensitive rewriting [20] is capable of restricting where rewriting may happen, by means of a replacement map µ : Σ → N∗ .
It is possible to encode any replacement map into evaluation contexts. For example,
a replacement map µ(if) = {1} specifies that only the first argument (i.e. the guard
t of if(t, s1 , s2 )) can be rewritten. This can be encoded into evaluation contexts as
E ::=  | if(E, s1 , s2 ). Another example is µ(+) = {1, 2} that specifies both of thetwo arguments of + can be rewritten. This can be encoded as E ::=  | E + t | t + E. Every context-sensitive rewriting system can be simulated by a first-order TES in this way.
Advantages of TERS are that (1) TES can also control the evaluation order easily (e.g.
the left-to-right evaluation of function application), and (2) we have also formulated
second-order TES with refinements as TERS.
Another term-rewriting alternative to evaluation contexts is rewriting strategies [16]that provide a way of determinising rewriting. Evaluation typically comes with a convenient inductive structure, which is lacking in strategies.
There is rich literature on methodologies for proving observational equivalence [1,18, 24, 28]. Some methodologies have been applied to effect handlers [5, 4]. We provide a novel term-rewriting-theoretic methodology centred around local coherence andcritical pair analysis.
Our methodology is partly automatable, thanks to the fact that critical pair analysis
for second-order computation systems can be automated [13, 14]. Our prototype analyzer based on this technology could automatically check the joinablity of all the criticalpairs in the examples (see Appendix C for Hndl). There are few works on automating
observational equivalence proofs for functional programs. Known examples, including
the tool SyTeCi [17], are based on or inspired by algorithmic game semantics [2].
This work is targeted at contextual improvement, a quantitative variant of observational equivalence. There is relatively limited literature on proof methodologies forcontextual improvement. A coinductive approach based on applicative bisimulation has
been used for space improvement [29] and time improvement [19]. This line of work,
however, does not come with any form of automation.

8

Conclusion and future work

We formalised evaluation from the term-rewriting perspective, and introduced TERS in
both first-order and second-order settings. To validate refinement (which models optimisation) with respect to evaluation, we employed the concept of contextual improvement, and identified sufficient conditions for it. The key condition is local coherence,
for which we developed critical pair analysis. We demonstrated TERS with examples
including λml∗ and its extension with effect handlers.
This work contributes to bridging the gap between general term rewriting and evaluation, by introducing TERS. We are interested in bringing more term-rewriting techniques and insights to evaluation; for example to check if a TERS is deterministic, andif refinement implies observational equivalence instead of contextual improvement.
Acknowledgement. The authors are supported by JSPS, KAKENHI Project No. 20H04164,
Japan. K.M. is also supported by JSPS, KAKENHI Project No. 22K17850, Japan.

16

K. Muroya and M. Hamana

References
1. Abramsky, S.: The lazy lambda-calculus, pp. 65–117. Addison Wesley (1990)
2. Abramsky, S.: Algorithmic game semantics: a tutorial introduction. In: NATO Advanced
Study Institute 2001. pp. 21–47 (2001)
3. Aoto, T., Toyama, Y.: A reduction-preserving completion for proving confluence of
non-terminating term rewriting systems. Log. Methods Comput. Sci. 8(1) (2012).
https://doi.org/10.2168/LMCS-8(1:31)2012
4. Biernacki, D., Lenglet, S., Polesiuk, P.: A complete normal-form bisimilarity for algebraic
effects and handlers. In: Ariola, Z.M. (ed.) 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference). LIPIcs, vol. 167, pp. 7:1–7:22. Schloss Dagstuhl - Leibniz-Zentrum fürInformatik (2020). https://doi.org/10.4230/LIPICS.FSCD.2020.7, https://doi.org/10.
4230/LIPIcs.FSCD.2020.7
5. Biernacki, D., Piróg, M., Polesiuk, P., Sieczkowski, F.: Handle with care: relational interpretation of algebraic effects and handlers. Proc. ACM Program. Lang. 2(POPL), 8:1–8:30(2018). https://doi.org/10.1145/3158096, https://doi.org/10.1145/3158096
6. Faggian, C., Guerrieri, G., de’Liguoro, U., Treglia, R.: On reduction and normalization in the computational core. Math. Struct. Comput. Sci. 32(7), 934–
981 (2022). https://doi.org/10.1017/S0960129522000433, https://doi.org/10.1017/
S0960129522000433
7. Faggian, C., Guerrieri, G., Treglia, R.: Evaluation in the computational calculus is nonconfluent. In: 10th International Workshop of Confluence, IWC 2021. pp. 31–36 (2021),
http://www.lix.polytechnique.fr/iwc2021/papers/IWC_2021_paper_6.pdf
8. Felleisen, M.: lambda-v-cs: An extended lambda-calculus for scheme. In: Chailloux,J. (ed.) Proceedings of the 1988 ACM Conference on LISP and Functional Programming, LFP 1988, Snowbird, Utah, USA, July 25-27, 1988. pp. 72–85. ACM (1988).
https://doi.org/10.1145/62678.62686, https://doi.org/10.1145/62678.62686
9. Felleisen, M.: The theory and practice of first-class prompts. In: Ferrante, J., Mager, P. (eds.)
Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming
Languages, San Diego, California, USA, January 10-13, 1988. pp. 180–190. ACM Press(1988). https://doi.org/10.1145/73560.73576, https://doi.org/10.1145/73560.73576
10. Fiore, M.: Second-order and dependently-sorted abstract syntax. In: Proc. of LICS’08. pp.
57–68 (2008)
11. Fiore, M., Mahmoud, O.: Second-order algebraic theories. In: Proc. of MFCS’10. pp. 368–
380. LNCS 6281 (2010)
12. Hamana, M.: Free Σ-monoids: A higher-order syntax with metavariables. In: Chin, W. (ed.)
Programming Languages and Systems: Second Asian Symposium, APLAS 2004, Taipei,
Taiwan, November 4-6, 2004. Proceedings. Lecture Notes in Computer Science, vol. 3302,
pp. 348–363. Springer (2004). https://doi.org/10.1007/978-3-540-30477-7_23
13. Hamana, M.: How to prove decidability of equational theories with secondorder computation analyser SOL. J. Funct. Program. 29,
e20 (2019).
https://doi.org/10.1017/S0956796819000157,
https://doi.org/10.1017/
S0956796819000157
14. Hamana, M., Abe, T., Kikuchi, K.: Polymorphic computation systems: Theory
and practice of confluence with call-by-value. Sci. Comput. Program. 187, 102322(2020). https://doi.org/10.1016/J.SCICO.2019.102322, https://doi.org/10.1016/j.
scico.2019.102322
15. Huet, G.P.: Confluent reductions: Abstract properties and applications to term rewriting systems: Abstract properties and applications to term rewriting systems. J. ACM 27(4), 797–821(1980). https://doi.org/10.1145/322217.322230

Term Evaluation Systems

17

16. Huet, G.P., Lévy, J.: Computations in orthogonal rewriting systems. In: Lassez, J., Plotkin,
G.D. (eds.) Computational Logic - Essays in Honor of Alan Robinson. pp. 395–443. The
MIT Press (1991)
17. Jaber, G.: Syteci: automating contextual equivalence for higher-order programswith references. Proc. ACM Program. Lang. 4(POPL), 59:1–59:28 (2020).
https://doi.org/10.1145/3371127, https://doi.org/10.1145/3371127
18. Koutavas, V., Levy, P., Sumii, E.: From applicative to environmental
bisimulation. Elect. Notes in Theor. Comp. Sci. 276, 215–235 (2011).
https://doi.org/10.1016/j.entcs.2011.09.023
19. Lago, U.D., Gavazzo, F.: Effectful normal form bisimulation. In: Caires, L. (ed.) Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019,
Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS
2019, Prague, Czech Republic, April 6-11, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11423, pp. 263–292. Springer (2019). https://doi.org/10.1007/978-3-03017184-1_10, https://doi.org/10.1007/978-3-030-17184-1_10
20. Lucas, S.: Context-sensitive rewriting. ACM Comput. Surv. 53(4), 78:1–78:36 (2021).
https://doi.org/10.1145/3397677, https://doi.org/10.1145/3397677
21. Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. J. Log. Comput. 1(4), 497–536 (1991).
https://doi.org/10.1093/logcom/1.4.497, https://doi.org/10.1093/logcom/1.4.497
22. Morris Jr, J.H.: Lambda-calculus models of programming languages. Ph.D. thesis, Massachusetts Institute of Technology (1969)
23. Muroya, K.: Hypernet semantics of programming languages. Ph.D. thesis, University ofBirmingham (2020), https://etheses.bham.ac.uk/id/eprint/10433/
24. Plotkin, G.D.: Lambda-definability and logical relations (1973), memorandum SAI-RM-4
25. Pretnar, M.: An introduction to algebraic effects and handlers. invited tutorial paper. In: Ghica, D.R. (ed.) The 31st Conference on the Mathematical Foundationsof Programming Semantics, MFPS 2015, Nijmegen, The Netherlands, June 22-25,
2015. Electronic Notes in Theoretical Computer Science, vol. 319, pp. 19–35. Elsevier (2015). https://doi.org/10.1016/J.ENTCS.2015.12.003, https://doi.org/10.1016/
j.entcs.2015.12.003
26. Sabry, A., Wadler, P.: A reflection on call-by-value. In: Harper, R., Wexelblat, R.L. (eds.) Proceedings of the 1996 ACM SIGPLAN International Conference on Functional Programming,
ICFP 1996, Philadelphia, Pennsylvania, USA, May 24-26, 1996. pp. 13–24. ACM (1996).
https://doi.org/10.1145/232627.232631, https://doi.org/10.1145/232627.232631
27. Sands, D.: Total correctness by local improvement in the transformation of functional programs. ACM Trans. Program. Lang. Syst. 18(2), 175–234 (1996).
https://doi.org/10.1145/227699.227716
28. Statman, R.: Logical relations and the typed lambda-calculus. Information and Control
65(2/3), 85–97 (1985). https://doi.org/10.1016/S0019-9958(85)80001-2
29. Sumii, E.: A bisimulation-like proof method for contextual properties in untyped lambdacalculus with references and deallocation. Theor. Comput. Sci. 411(51-52), 4358–4378(2010). https://doi.org/10.1016/J.TCS.2010.09.009, https://doi.org/10.1016/j.tcs.
2010.09.009
30. Toyama, Y.: Commutativity of term rewriting systems, pp. 393–407. North-Holland (1988)

18

K. Muroya and M. HamanaA

Omitted proofs

A.1

Proofs for Sec. 3 and Sec. 4

Theorem 26 (Thm. 7: sufficient condition for improvement). If a TERS is deterministic, value-invariant and locally coherent, then it supports improvement.
k

Proof. Take arbitrary k ∈ N and t, u ∈ TΣ such that t ⇒R u and t →E v ∈ Val. We firstkmprove that t ⇒R u and t →E v imply u →E v0 , v =Val v0 and k ≥ m, for any k ∈ N, by
induction on k.
Base case. When k = 0, we have t = v. Because the TERS (E, R) is value-invariant, wehave u ∈ Val and v =Val u. We can take m = 0.
k−1

Inductive case. When k > 0, there exists t0 ∈ TΣ such that t →E t0 → E v. Because
the TERS (E, R) is locally coherent, the (R, E)-peak (u, t, t0 ) is joinable up to R; namelylnmthere exist t00 , u0 ∈ TΣ and l, m, n ∈ N such that t0 →E t00 , u →E u0 , t00 ⇒R u0 and
1 + l ≥ n. Because the TERS (E, R) is deterministic, t00 must appear in the sequence
k−1

l

k−l−1

t0 → E v, and hence t →E t0 →E t00 → E v. We prove that we have the following
situation:
t
 0
|
u
t
n 
l
u0 ks m t00
n0  k−l−1
v0
v
Val

n0

namely that there exist n0 ∈ N and v0 ∈ Val such that u0 →E v0 and v =Val v0 , byinduction on m ∈ N.
– Base case. When m = 0, t00 = u0 . We can take n0 = k − l − 1 and v0 = v. Because
1 + l ≥ n, we have k ≥ n + n0 .
m−1

– Inductive case. When m > 0, we have t00 ⇒ R u00 ⇒R u0 for some u00 ∈ TΣ . By I.H.
n00

on m − 1, we have u00 →E v00 such that v00 =Val v and k − l − 1 ≥ n00 . Furthermore,n0

by I.H. of the outer induction on n00 , we have u0 →E v0 such that v00 =Val v0 and
n00 ≥ n0 . We finally have k ≥ n + n0 .
n+n0

As a result, we have u → E v0 such that v =Val v0 and k ≥ n + n0 . We can take m = n + n0 .
Secondly, because ⇒R is closed under any contexts, t ⇒R u implies C[t] ⇒R C[u]kmfor any C ∈ Ctx. Therefore, t ⇒R u and C[t] →E v imply C[u] →E v0 such that k ≥ mand v =Val v0 , for any v ∈ Val.
tu
Lemma 27 (Lem. 11). If a critical pair (t1 , s, t2 ) is joinable, then for any substitution θ,(t1 θ, sθ, t2 θ) is a joinable (R, E)-peak.

Term Evaluation Systems

19

Proof. We have a joinable (R, E)-peak (t1 , s, t2 ). Since refinement and evaluation areclosed under substitution, (t1 θ, sθ, t2 θ) is also a joinable (R, E)-peak.
tuTheorem 28 (Thm. 13: Critical pair theorem). A well-behaved TERS is locally coherent if and only if every critical pair is joinable.
Proof. The “only if” part is straightforward. In the following, we prove the “if” part.
Take an arbitrary (R, E)-peak (t1 , s, t2 ). Our goal is to prove that this (R, E)-peak is
joinable. Since s ⇒R t1 , there exist p ∈ Pos(s), (l ⇒ r) ∈ R and subst θ such thats| p = lθ, t1 = s[rθ] p and s[] p ∈ Ctx. We prove that the (R, E)-peak (t1 , s, t2 ) is joinable,
by induction on the length of the position p.
Base case. When |p| = 0, i.e. p = ε, we have s = lθ and t1 = rθ. Because lθ →E t2 , there
exist p0 ∈ Pos(lθ), (l0 → r0 ) ∈ E and subst θ0 such that (lθ)| p0 = l0 θ0 , t2 = (lθ)[r0 θ0 ] p0 and(lθ)[] p0 ∈ Ectx. We have an (R, E)-peak P = (rθ, lθ, (lθ)[r0 θ0 ] p0 ).
– If p0 = ε, and l ⇒ r and l → r are variants of each other, we have rθ = r0 θ0 and the(R, E)-peak P is joinable.
– Otherwise, there are two possibilities.
• If p0 is a non-variable position of l, the (R, E)-peak P is an instance of thecritical pair generated by an (R, E)-overlap.
• Otherwise, there exist sequences q1 , q2 and a variable y such that: q1 ∈ Pos(l),l|q1 = y, q2 ∈ Pos(yθ), and p0 = q1 q2 . Because of the condition (1) of Def. 12,(lθ)[] p0 ∈ Ectx implies l[]q1 , yθ[]q2 ∈ Ectx. The variable y must appear at
most once in both l and r, due to the condition (3a) of Def. 12. If y does notappear in r, the (R, E)-peak P is joinable by applying the rule l ⇒ r to t2 .
Otherwise, i.e. if y appears once in r, the rule l0 → r0 can be applied to t1
thanks to the condition (3b) of Def. 12, and the rule l ⇒ r can be applied to t2 .
These two applications yield the same result. Therefore, we can conclude thatthe (R, E)-peak P is joinable.
Inductive case. When |p| > 0, we have p = ipt for some positive number i and somesequence pt . We have s = f (x1 .u1 , . . . , xi .ui , . . . , xk .uk ), lθ = ui | pt . We have an (R, E)peak
P0 = ( f (x1 .u1 , . . . , xi .ui [rθ] pt , . . . , xk .uk ), f (x1 .u1 , . . . , xi .ui , . . . , xl .ul ), t2 ).
By s →E t2 , there exist p0 ∈ Pos(s), (l0 → r0 ) ∈ E and subst θ0 such that s| p0 = l0 θ0 ,t2 = s[r0 θ0 ] p0 and s[] p0 ∈ Ectx. We proceed by case analysis on p0 ∈ Pos(s).
– When p0 = ε , we have s = l0 θ0 and t2 = r0 θ0 .
• If p is a non-variable position of l0 , the (R, E)-peak P0 is an instance of thecritical pair generated by an (E, R)-overlap.
• Otherwise, there exist sequences q1 , q2 and a variable y such that: q1 ∈ Pos(l0 ),l0 |q1 = y, q2 ∈ Pos(yθ0 ), and p = q1 q2 . The variable y appears at most once inl0 , due to the condition (4) of Def. 12. We can apply the rule l0 → r0 to t1 . We
can also apply the rule l ⇒ r to t2 , as many times as y appears in r0 . These
applications of l0 → r0 and l ⇒ r yield the same result. The (R, E)-peak P0 is
therefore joinable.

20

K. Muroya and M. Hamana– When p0 , ε, i.e. p0 = i0 p0t for some positive number i0 and some sequence p0t ,there are two possibilities.
• When i0 = i, by I.H., we have a joinable (R, E)-peak
Q = (ui [rθ] pt , ui , ui [r0 θ0 ] p0t ).
Because f (. . . , xi .ui [] pt , . . .) ∈ Ectx, we have f (. . . , xi ., . . .) ∈ Ectx too,
thanks to the condition (1) of Def. 12. Therefore, joinability of the (R, E)-peak
Q implies joinability of the (R, E)-peak P0 .
• When i0 , i, we can assume that i0 < i without loss of generality. The (R, E)peak
P0 = ( f (. . . , xi0 .ui0 , . . . , xi .ui [rθ] pt , . . .),f (. . . , xi0 .ui0 , . . . , xi .ui , . . .),f (. . . , xi0 .ui0 [r0 θ0 ] p0t , . . . , xi .ui , . . .))is joinable (to f (. . . , xi0 .ui0 [r0 θ0 ] p0t , . . . , xi .ui [rθ] pt , . . .)), thanks to the condition(2) of Def. 12.
tu
A.2

The TERS Nats

Proposition 29. The TERS Nats is deterministic, value-invariant and locally coherent.
Proof. The TERS Nats is deterministic, because evaluation rules concern distinct symbols.
To prove value-invariance, we assume v ⇒R u for some v ∈ Val and u ∈ TΣ . It must
hold that v = sn (0), and in this case, the refinement v ⇒R u is impossible. The TERSNats is trivially value-invariant.
To prove local coherence, we use Thm. 13. We first show that the TERS Nats iswell-behaved. The condition (1) of Def. 24 is trivially satisfied. As for the condition(2), each evaluation context E ∈ Ectx never includes the constant nats, and hence therefinement rule cannot be applied to E[t] to obtain C 0 [t]. Therefore the condition (2) istrivially satisfied. The other conditions of well-behavedness are easy to check. We thenshow that any critical pair is joinable. There is only one critical pair, and it is indeed
joinable as follows.
tl(inc(nats))woinc(tl(nats))inc(tl(0 : inc(nats)))+tl(inc(0 : inc(nats)))tl(s(0) : inc(inc(nats)))+sinc(inc(nats))tuTerm Evaluation Systems

A.3

21

On linearity conditions

For a TERS to be well-behaved, its evaluation rules must be left-linear, and its refinement rules must be linear (see Def. 12). Here we observe that relaxing these linearity
conditions, with a reasonable set of evaluation contexts and values, leads to non-joinable(R, E)-peaks that are not instances of a critical pair.
Let a TERS ES be defined as follows.
?

Signature ΣValues Val
Evaluation contexts Ectx
Evaluation rules E
0+x→ xs(x) + y → s(x + y)0−x→0s(x) − s(y) → x − y+ : 2, − : 2, ≡ : 2, s : 1, 0 : 0
V ::= 0 | s(V)E ::=  | s(E) | E + t | E − t | v − E
Refinement rule Rx−x⇒00⇒ x−x?

x≡x→0?

We define =Val by the syntactic equality ≡. The operation ≡ checks syntactic equality.
The non-left-linear refinement rule x − x ⇒ 0 induces the following non-joinable(R, E)-peak.
(s(x) + y) − (s(x) + y),
0 pxs(x + y) − (s(x) + y)
In the term s(x + y) − (s(x) + y), the sub-term s(x) + y cannot be evaluated, becauses(x + y) is not a value.
The non-right-linear refinement rule 0 ⇒ x − x induces the following non-joinable(R, E)-peak.
0
x
/0
0−0
This (R, E)-peak is not joinable with respect to our definition of joinability (see Def. 4).
The bottom term 0 − 0 must not take more evaluation steps than the top term 0.
?

Finally, the non-left-linear evaluation rule x ≡ x → 0 induces the following nonjoinable (R, E)-peak.
?

?

s(x + y) ≡ (s(x) + y)?

ow(s(x) + y) ≡ (s(x) + y)(0

In the term s(x + y) ≡ (s(x) + y), the sub-term s(x) + y cannot be evaluated, becauses(x + y) is not a value.

22

K. Muroya and M. Hamana

A.4

Proofs for Sec. 5 and Sec. 6

Lemma 30 (Lem. 23). If a critical pair (t1 , s, t2 ) is joinable, then for any valid substitution θ, (t1 θ, sθ, t2 θ) is a joinable (R, E)-peak.
Proof. We have a joinable (R, E)-peak (t1 , s, t2 ). Because evaluation is closed under∗valid substitutions, and refinement satisfies t ⇒R u =⇒ tθ ⇒R uθ, (t1 θ, sθ, t2 θ) is alsoa joinable (R, E)-peak.
tuTheorem 31 (Thm. 25: Critical pair theorem). A well-behaved TERS is locally coherent if and only if every critical pair is joinable.
Proof. The “only if” part is straightforward. In the following, we prove the “if” part.
Take an arbitrary (R, E)-peak (t1 , s, t2 ). Our goal is to prove that this (R, E)-peakis joinable. Since s ⇒R t1 , there exist p ∈ Pos(s), (l ⇒ r) ∈ R and valid θ such thats| p = lθ, t1 = s[rθ] p and s[] p ∈ Ctx. We prove that the (R, E)-peak (t1 , s, t2 ) is joinable,
by induction on the length of the position p.
Base case. When |p| = 0, i.e. p = ε, we have s = lθ and t1 = rθ. Because lθ →E t2 ,there exist p0 ∈ Pos(lθ), (l0 → r0 ) ∈ E and valid θ0 such that (lθ)| p0 = l0 θ0 , t2 = (lθ)[r0 θ0 ] p0
and (lθ)[] p0 ∈ Ectx. We have an (R, E)-peak P = (rθ, lθ, (lθ)[r0 θ0 ] p0 ).
– If p0 = ε, and l ⇒ r and l → r are variants of each other, we have rθ = r0 θ0 and the(R, E)-peak P is joinable.
– Otherwise, because (lθ)[] p0 ∈ Ectx is a flat context, every prefix of p0 but p0 itself
is not a metavariable position in lθ.
• If p0 is a non-metavariable position of l, the (R, E)-peak P is an instance of thecritical pair generated by an (R, E)-overlap.
• Otherwise, There exist sequences q1 , q2 , a metavariable N and a sequence ysuch that: q1 ∈ Pos(l), l|q1 = N[y], q2 ∈ Pos((N[y])θ), and p0 = q1 q2 . Becauseof the condition (1) of Def. 24, (lθ)[] p0 ∈ Ectx implies l[]q1 , (N[y])θ[]q2 ∈Ectx. In particular, the latter means that (N[y])θ < NF(→E ), and hence N is
not a value metavariable. The metavariable N must appear at most once in bothl and r, due to the condition (3a) of Def. 24. If N does not appear in r, the(R, E)-peak P is joinable by applying the rule l ⇒ r to t2 . Otherwise, i.e. if N
appears once in r, the rule l0 → r0 can be applied to t1 thanks to the condition(3b) of Def. 24, and the rule l ⇒ r can be applied to t2 , thanks to the condition(6) of Def. 24. These two applications yield the same result. Therefore, we canconclude that the (R, E)-peak P is joinable.
Inductive case. When |p| > 0, we have p = ipt for some positive number i and some sequence pt . We have either s = f (x1 .u1 , . . . , xi .ui , . . . , xk .uk ) or s = M[u1 , . . . , ui , . . . , uk ],such that lθ = ui | pt .
Firstly, assume that we have an (R, E)-peak
P0 = ( f (x1 .u1 , . . . , xi .ui [rθ] pt , . . . , xk .uk ), f (x1 .u1 , . . . , xi .ui , . . . , xl .ul ), t2 ).
By s →E t2 , there exist p0 ∈ Pos(s), (l0 → r0 ) ∈ E and valid θ0 such that s| p0 = l0 θ0 ,t2 = s[r0 θ0 ] p0 and s[] p0 ∈ Ectx. We proceed by case analysis on p0 ∈ Pos(s).

Term Evaluation Systems

23– When p0 = ε , we have s = l0 θ0 and t2 = r0 θ0 .
• If p is a non-metavariable position of l0 , the (R, E)-peak P0 is an instance of thecritical pair generated by an (E, R)-overlap.
• Otherwise, there exist sequences q1 , q2 and a metavariable M such that: q1 ∈Pos(l0 ), l0 |q1 = M[y], q2 ∈ Pos(M[y]θ0 ), and p = q1 q2 . The metavariable M
appears at most once in l0 , due to the condition (4) of Def. 24. We can apply
the rule l0 → r0 to t1 . The substitution θ0 is valid, thanks to the condition (5) of
Def. 24. We can also apply the rule l ⇒ r to t2 as many times as M appears in r0 .
These applications of l0 → r0 and l ⇒ r yield the same result. The (R, E)-peak
P0 is therefore joinable.
– When p0 , ε, i.e. p0 = i0 p0t for some positive number i0 and some sequence p0t ,there are two possibilities.
• When i0 = i, by I.H., we have a joinable (R, E)-peak Q = (ui [rθ] pt , ui , ui [r0 θ0 ] p0t ).
Because f (. . . , xi .ui [] pt , . . .) ∈ Ectx, we have f (. . . , xi ., . . .) ∈ Ectx too,
thanks to the condition (1) of Def. 24. Therefore, joinability of the (R, E)-peak
Q implies joinability of the (R, E)-peak P0 .
• When i0 , i, we can assume that i0 < i without loss of generality. The (R, E)peakP0 =( f (. . . , xi0 .ui0 , . . . , xi .ui [rθ] pt , . . .), f (. . . , xi0 .ui0 , . . . , xi .ui , . . .),f (. . . , xi0 .ui0 [r0 θ0 ] p0t , . . . , xi .ui , . . .))is joinable (to f (. . . , xi0 .ui0 [r0 θ0 ] p0t , . . . , xi .ui [rθ] pt , . . .)), thanks to the condition(2) of Def. 24.
Secondly, assume that we have an (R, E)-peak
P0 = (M[u1 , . . . , ui [rθ] pt , . . . , uk ], M[u1 , . . . , ui , . . . , ul ], t2 ).
By s →E t2 , there exist p0 ∈ Pos(s), (l0 → r0 ) ∈ E and valid θ0 such that s| p0 = l0 θ0 ,t2 = s[r0 θ0 ] p0 and s[] p0 ∈ Ectx. We proceed by case analysis on p0 ∈ Pos(s).
– When p0 = ε, M[u1 , . . . , uk ] = l0 θ0 . Because l0 is a higher-order pattern, this is
impossible.
– When p0 , ε, the proof is the same as the case for the (R, E)-peak
P0 = ( f (x1 .u1 , . . . , xi .ui [rθ] pt , . . . , xk .uk ), f (x1 .u1 , . . . , xi .ui , . . . , xl .ul ), t2 ).
tu
A.5

The TERS CBVλ and Hndl

B

Determinism

We will use a sufficient condition for a TES to be deterministic, namely decisiveness.
Definition 32 (decisiveness). A TES (Σ, E, Ectx, Val) is decisive if each t ∈ TΣ satisfies
either of the following:
1. t ∈ Val,
2. there uniquely exist (l → r) ∈ E, subst θ and E ∈ Ectx such that t = E[lθ],24

K. Muroya and M. Hamana

3. there uniquely exist a variable x and E ∈ Ectx such that t = E[x].
Proposition 33 (sufficient condition for determinism). If a TES is decisive, then it isdeterministic.
Proof. Let t →E s1 and t →E s2 . Because the TES is decisive, t satisfies either the three
conditions in Def. 32. Since the left-hand side of each evaluation rule is not a variable,
to make the evaluation t →E s1 and t →E s2 happen, only the case (2) is possible. In
this case, both s1 and s2 must be E[rθ].
tuProposition 34. The TERS CBVλ is deterministic, value-invariant and locally coherent.
Proof. The TERS CBVλ is deterministic, because it is decisive.
To prove value-invariance, we assume λx.t ⇒R u. There are two possible cases.
– When u = λx.t0 for some t0 such that t ⇒R t0 , we have λx.t =Val λx.t0 .
– When t = λx.(λy.t0 ) x, it must be that u = λy.t0 , and we have λx.(λy.t0 ) x =Val λy.t0 .
Therefore the TERS CBVλ is value-invariant.
To prove local coherence, we use Thm. 13.
Firstly, the TERS CBVλ is well-behaved. The condition (1) of Def. 24 is triviallysatisfied. We can show that the condition (2) is satisfied by straightforward induction
on E ∈ Ectx. The condition (6) is satisfied, because any instance of the lhs of theevaluation rule never belongs to a syntax class (i.e. the value class). The condition (5)is also satisfied; the second refinement rule always turns a value into a value. The otherconditions of well-behavedness are easy to check.
We then show that any critical pair is joinable. There are two critical pairs, which
are for the second refinement rule (the η-rule) and the evaluation rule. These criticalpairs are joinable as follows.

V V0(λx0 .M 0 [x0 ]) Vowrz

(λx.V x) V 0(

V V0(λx0 .M 0 [x0 ]) (λx.V x)+

M 0 [V]+M 0 [λx.V x]owtu

Proposition 35. The TERS Compλml∗ is deterministic, value-invariant and locally coherent.
Proof. Firstly, the TERS Compλml∗ is deterministic, because the two evaluation rules
consume different head symbols. Secondly, the TERS is value-invariant, thanks to theequivalence =Val being the total order.
To prove local coherence, we use Thm. 13.

Term Evaluation Systems

25

The TERS Compλml∗ is well-behaved. The condition (1) of Def. 24 is trivially satisfied. We can show that the condition (2) is satisfied by induction on E ∈ Ectx asfollows.
– When E = , no refinement rule applies to x, so this case is impossible.
– When E = let(E 0 , x.P), we have let(E 0 [t], x.P) ⇒R C 0 [t]. There are four possibilities.
• If E 0 [z] ⇒R C 00 [z] such that C 0 = let(C 00 , x.P), we have C 00 ∈ Ectx by I.H.,
and hence C 0 ∈ Ectx.
• If P ⇒R P0 such that C 0 = let(E 0 , x.P0 ), we have C 0 ∈ Ectx.
• If the refinement rule (r4) is applied at the root position of E[z], we havelet(E 0 [z], x.return(x)) ⇒R E 0 [z]. We have C 0 = E 0 ∈ Ectx.
• If the refinement rule (r5) is applied at the root position of E[z], we havelet(let(E 00 [z], x.P[x]), y.P0 [y]) ⇒R let(E 00 [z], x.let(P[x], y.P0 [y])). We have
C 0 = let(E 00 , x.let(P[x], y.P0 [y])) ∈ Ectx.
The conditions (6) and (5) are also satisfied; note that instances of P[V] are all computations. The other conditions of well-behavedness are easy to check.
We finally show that any critical pair is joinable. There are the following three critical pairs, which are all joinable. In the following, arrows →, ⇒ are labelled by a numberthat indicates which evaluation/refinement rule is applied.

VV

0

s{

r3

(λx.V x) V 0
1

'

V V0

let(return(V), x.return(x))
return(V)

ow

r4

2

+

return(V)let(let(return(V), x.P[x]), x0 .P0 [x0 ])
2
r5
ow
*
let(return(V), x.let(P[x], x0 .P0 [x0 ]))let(P[V], x0 .P0 [x0 ])+2
let(P[V], x0 .P0 [x0 ])tu
Proposition 36. The TERS Hndl is deterministic, value-invariant and locally coherent.
Proof. Firstly, to establish that the TERS Hndl is deterministic, we show that, for anyt ∈ MΣ , if t = E[lθ] = E 0 [l0 θ0 ] for some E, E 0 ∈ Ectx, (l → r), (l0 → r0 ) ∈ E andvalid θ, θ0 , then the decomposition is unique, namely E = E 0 and the rules l → r,
l0 → r0 are variants of each other. This can be proved by induction on E ∈ Ectx.
– When E = , we have t = lθ. By definition of evaluation rules, E 0 =  must hold,and l → r and l0 → r0 must be variants.

26

K. Muroya and M. Hamana– When E = do(E 0 , x.P), we have t = do(E 0 [lθ], P). By I.H., E 0 [lθ] is the only
possible decomposition. The meta-term t itself cannot be an instance of any lhs ofevaluation rules. Therefore, the decomposition E[lθ] is unique.
– When E = with_handle(H, E 0 ), we have t = with_handle(H, E 0 [lθ]). The proofis the same as the previous case.
Consequently, the TERS Hndl is deterministic.
Secondly, by definition of =Val , the TERS Hndl is value-invariant. In particular, therefinement rule (r9) turns a function into a variable or a function; the original function
is identified with the resulting variable or function by =Val .
To prove local coherence, we use Thm. 13.
The TERS Hndl is well-behaved. The condition (1) of Def. 24 is trivially satisfied.
We can show that the condition (2) is satisfied by induction on E ∈ Ectx as follows.
– When E = , no refinement rule applies to x, so this case is impossible.
– When E = do(E 0 , x.P), we have do(E 0 [z], x.P) ⇒R C 0 [z]. There are four possibilities.
• If E 0 [z] ⇒R C 00 [z] such that C 0 = do(C 00 , x.P), we have C 00 ∈ Ectx by I.H., andhence C 0 ∈ Ectx.
• If P ⇒R P0 such that C 0 = do(E 0 , x.P0 ), we have C 0 ∈ Ectx.
• If the refinement rule (r3) is applied at the root position of E[z], we havedo(E 0 [z], x.return(x)) ⇒R E 0 [z]. We have C 0 = E 0 ∈ Ectx.
• If the refinement rule (r4) is applied at the root position of E[z], we havedo(do(E 00 [z], x.P[x]), y.P0 [y]) ⇒R do(E 00 [z], x.do(P[x], y.P0 [y])). We have C 0 =do(E 00 , x.do(P[x], y.P0 [y])) ∈ Ectx.
– When E = with_handle(H, E 0 ), we have with_handle(H, E 0 [z]) ⇒R C 0 [z].
There are three possibilities.
• If E 0 [z] ⇒R C 00 [z] such that C 0 = with_handle(H, C 00 ), we have C 00 ∈ Ectx
by I.H., and hence C 0 ∈ Ectx.
• If H ⇒R H 0 such that C 0 = with_handle(H 0 , E 0 ), we have C 0 ∈ Ectx.
• If the refinement rule (r13) is applied at the root position of E[z], we havewith_handle(handler0 (x.P[x]), E 0 [z]) ⇒R do(E 0 [z], x.P[x]). We have C 0 =do(E 0 , x.P[x]) ∈ Ectx.
The conditions (6) and (5) are also satisfied; note that instances of P[V] are all computations. The other conditions of well-behavedness are easy to check.
We finally show that any critical pair is joinable. There are the following sevencritical pairs, which are all joinable. In the following, arrows →, ⇒ are labelled bya number that indicates which evaluation/refinement rule is applied, and we set h0 ≡

Term Evaluation Systems

27

handler0 (x.P[x]), and i ∈ [2].
do(return(V), x.return(x))
r3
1
qy
)
return(V)return(V)do(opi (V, y.P[y]), x.return(x))
yq
opi (V, y.P[y]) ks

r3

2

+
opi (V, y.do(P[y], x.return(x)))

r3do(do(return(V), x.P[x]), x0 .P0 [x0 ])
1
r4
ow
*
do(return(V), x.do(P[x], x0 .P0 [x0 ]))do(P[V], x0 .P0 [x0 ])+1
do(P[V], x0 .P0 [x0 ])do(do(opi (V, x.P[x]), y.P2 [y]), z.P3 [z])
r4

2

xp
*
do(opi (V, x.P[x]), y.do(P2 [y], z.P3 [z])) do(opi (V, x.do(P[x], y.P2 [y])), z.P3 [z])

2
r4ks
opi (V, x.do(P[x], y.do(P2 [y], z.P3 [z]))) opi (V, x.do(do(P[x], y.P2 [y]), z.P3 [z]))2

fun(x.V x) V 0
VV

0

u}

5

r9

%

V V0

with_handle(h0 , return(V))
r13

9

xp
do(return(V), x.P[x])

1

*

(

P[V]

P[V]

with_handle(h0 , opi (V, y.P0 [y]))r13xp
do(opi (V, y.P0 [y]), x.P[x])10+
opi (V, y.with_handle(h0 , P0 [y]))

*
ow
2
r13
opi (V, y.do(P0 [y], x.P[x]))
t
u

28

K. Muroya and M. Hamana

C

Critical pair analysis of Hndl by our prototype analyzer

C.1

Definition of TERS Hndlsigh = [signature|
true : T
false : T
fun : (T -> T) -> T
app : T,T -> Treturn : T -> T
op1 : T, (T -> T) -> T
op2 : T, (T -> T) -> Thandler1 : (T -> T), (T,T -> T) -> Thandler0 : (T -> T) -> T
do : T, (T -> T) -> T
if : T,T,T -> Twith : T,T -> T|]evals = [rule|(1-v) do(return(V),x.P[x]) => P[V](2-1-v) do(op1(V, y.P1[y]), x.P2[x]) => op1(V, y.do(P1[y],x.P2[x]))(2-2-v) do(op2(V, y.P1[y]), x.P2[x]) => op2(V, y.do(P1[y],x.P2[x]))(3-v) if(true, P1, P2) => P1(4-v) if(false, P1, P2) => P2(5-v) fun(x.P[x])@V => P[V](6-v) with(handler1(x.P[x],x.k.P1[x,k]), return(V)) => P[V](7-v) with(handler1(x.P[x],x.k.P1[x,k]),op1(V,y.P’[y])) => P1[V,fun(y.P’[y])](8-v) with(handler1(x.P[x],x.k.P1[x,k]),op2(V,y.P’[y])) => op2(V,y.with(handler1(x.P[x],x.k.P1[x,k]),P’[y]))(9-v)
with(handler0(x.P[x]),return(V)) => P[V](10-1-v) with(handler0(x.P[x]),op1(V,y.P’[y])) => op1(V,y.with(handler0(x.P[x]),P’[y]))(10-2-v) with(handler0(x.P[x]),op2(V,y.P’[y])) => op2(V,y.with(handler0(x.P[x]),P’[y]))|]refis = [rule|(r3-v) do(P,x.return(x)) => P
(r4-v) do(do(P1,x.P2[x]),x.P3[x]) => do(P1, x1.do(P2[x1],x2.P3[x2]))(r9-v) fun(x.V@x) => V(r13-v) with(handler0(x.P[x]),P’) => do(P’,x.P[x])|]C.2

Local coherence check*Ex> lcoh evals refis
1: Overlap (1-v)-(r3-v)--- P’|-> return(V), P|-> z1.return(z1) ---------------(1-v) |do(return(V),x.P[x])| => P[V](r3-v) do(P’,x’.return(x’)) => P’do(return(V),x.return(x))
return(V) <-(1-v)-∧-(r3-v)-> return(V)---> return(V) =OK= return(V) <--2: Overlap (r4-v)-(1-v)--- P1|-> return(V’), P’|-> z1.P2[z1] -----------------(r4-v) do(|do(P1,x.P2[x])|,x.P3[x]) => do(P1,x1.do(P2[x1],x2.P3[x2]))(1-v) do(return(V’),x’.P’[x’]) => P’[V’]do(do(return(V’),x.P2[x]),x.P3[x])do(return(V’),x17.do(P2[x17],x27.P3[x27])) <-(r4-v)-∧-(1-v)-> do(P2[V’],x.P3[x])---> do(P2[V’],x27.P3[x27]) =OK= do(P2[V’],x.P3[x]) <--3: Overlap (2-1-v)-(r3-v)--- P’|-> op1(V,y.P1[y]), P2|-> z1.return(z1) -------(2-1-v) |do(op1(V,y.P1[y]),x.P2[x])| => op1(V,y.do(P1[y],x.P2[x]))(r3-v) do(P’,x’.return(x’)) => P’do(op1(V,y.P1[y]),x.return(x))
op1(V,y14.do(P1[y14],x14.return(x14))) <-(2-1-v)-∧-(r3-v)-> op1(V,y.P1[y])---> op1(V,y14.do(P1[y14],x14.return(x14))) =OK= op1(V,y.P1[y]) <---

Term Evaluation Systems

29

4: Overlap (r4-v)-(2-1-v)--- P1|-> op1(V’,y’.P1’[y’]), P2’|-> z1.P2[z1] ------(r4-v) do(|do(P1,x.P2[x])|,x.P3[x]) => do(P1,x1.do(P2[x1],x2.P3[x2]))(2-1-v) do(op1(V’,y’.P1’[y’]),x’.P2’[x’]) => op1(V’,y’.do(P1’[y’],x’.P2’[x’]))do(do(op1(V’,y’.P1’[y’]),x.P2[x]),x.P3[x])do(op1(V’,y’.P1’[y’]),x121.do(P2[x121],x1.P3[x1])) <-(r4-v)-∧-(2-1-v)-> do(op1(V’,yd.do(P1’[yd],xd.P2[xd])),x.P3[x])---> op1(V’,y23.do(P1’[y23],x23.do(P2[x23],x1.P3[x1]))) =OK= op1(V’,y26.do(do(P1’[y26],xd.P2[xd]),x26.P3[x26])) <--5: Overlap (2-2-v)-(r3-v)--- P’|-> op2(V,y.P1[y]), P2|-> z1.return(z1) -------(2-2-v) |do(op2(V,y.P1[y]),x.P2[x])| => op2(V,y.do(P1[y],x.P2[x]))(r3-v) do(P’,x’.return(x’)) => P’do(op2(V,y.P1[y]),x.return(x))
op2(V,y33.do(P1[y33],x33.return(x33))) <-(2-2-v)-∧-(r3-v)-> op2(V,y.P1[y])---> op2(V,y33.do(P1[y33],x33.return(x33))) =OK= op2(V,y.P1[y]) <--6: Overlap (r4-v)-(2-2-v)--- P1|-> op2(V’,y’.P1’[y’]), P2’|-> z1.P2[z1] ------(r4-v) do(|do(P1,x.P2[x])|,x.P3[x]) => do(P1,x1.do(P2[x1],x2.P3[x2]))(2-2-v) do(op2(V’,y’.P1’[y’]),x’.P2’[x’]) => op2(V’,y’.do(P1’[y’],x’.P2’[x’]))do(do(op2(V’,y’.P1’[y’]),x.P2[x]),x.P3[x])do(op2(V’,y’.P1’[y’]),x140.do(P2[x140],x240.P3[x240])) <-(r4-v)-∧-(2-2-v)-> do(op2(V’,yd.do(P1’[yd],xd.P2[xd])),x.P3[x])---> op2(V’,y42.do(P1’[y42],x42.do(P2[x42],x240.P3[x240]))) =OK= op2(V’,y45.do(do(P1’[y45],xd.P2[xd]),x45.P3[x45])) <--7: Overlap (5-v)-(r9-v)--- P|-> z1.app(V’,z1) --------------------------------(5-v) |fun(x.P[x])|@V => P[V](r9-v) fun(x’.app(V’,x’)) => V’app(fun(x.app(V’,x)),V)app(V’,V) <-(5-v)-∧-(r9-v)-> app(V’,V)---> app(V’,V) =OK= app(V’,V) <--8: Overlap (9-v)-(r13-v)--- P’|-> z1.P[z1], Pd’|-> return(V) -----------------(9-v) |with(handler0(x.P[x]),return(V))| => P[V](r13-v) with(handler0(x’.P’[x’]),Pd’) => do(Pd’,x’.P’[x’])with(handler0(x.P[x]),return(V))
P[V] <-(9-v)-∧-(r13-v)-> do(return(V),xd66.P[xd66])---> P[V] =OK= P[V] <--9: Overlap (10-1-v)-(r13-v)--- P’|-> z1.P[z1], Pd’|-> op1(V,y.Pd[y]) ---------(10-1-v) |with(handler0(x.P[x]),op1(V,y.Pd[y]))| => op1(V,y.with(handler0(x.P[x]),Pd[y]))(r13-v) with(handler0(x’.P’[x’]),Pd’) => do(Pd’,x’.P’[x’])with(handler0(x.P[x]),op1(V,y.Pd[y]))op1(V,y72.with(handler0(x72.P[x72]),Pd[y72])) <-(10-1-v)-∧-(r13-v)-> do(op1(V,y.Pd[y]),xd73.P[xd73])---> op1(V,y72.with(handler0(x72.P[x72]),Pd[y72])) =OK= op1(V,y76.do(Pd[y76],x76.P[x76])) <--10: Overlap (10-2-v)-(r13-v)--- P’|-> z1.P[z1], Pd’|-> op2(V,y.Pd[y]) ---------(10-2-v) |with(handler0(x.P[x]),op2(V,y.Pd[y]))| => op2(V,y.with(handler0(x.P[x]),Pd[y]))(r13-v) with(handler0(x’.P’[x’]),Pd’) => do(Pd’,x’.P’[x’])with(handler0(x.P[x]),op2(V,y.Pd[y]))op2(V,y86.with(handler0(x86.P[x86]),Pd[y86])) <-(10-2-v)-∧-(r13-v)-> do(op2(V,y.Pd[y]),xd87.P[xd87])---> op2(V,y86.with(handler0(x86.P[x86]),Pd[y86])) =OK= op2(V,y90.do(Pd[y90],x90.P[x90])) <--#Joinable! (Total 10 CPs)
YES

In the proof of Prop. 36, op1 and op2 were summed in opi , so the number of criticalpairs in the proof matches this output.