Local Coherence and Program
Refinement(work in progress)

Makoto Hamana(Gunma University)

Koko Muroya(RIMS, Kyoto University)

58th TRS Meeting (Niigata), 20 February 2023

Term Evaluation andTerm Rewriting(work in progress)

Makoto Hamana(Gunma University)

Koko Muroya(RIMS, Kyoto University)

58th TRS Meeting (Niigata), 20 February 2023

Is program semantics a TRS?
● Yes?
● Arithmetics is a TRS.

(1 + 2) + (3 + 4) → 3 + (3 + 4) → 3 + 7 → 10
(1 + 2) + (3 + 4) → (1 + 2) + 7 → 3 + 7 → 103Muroya (RIMS, Kyoto U.)Is program semantics a TRS?
● No!
● Left-to-right arithmetics is not a TRS.

(1 + 2) + (3 + 4) → 3 + (3 + 4) → 3 + 7 → 10
(1 + 2) + (3 + 4) ↛ (1 + 2) + 7 → 3 + 7 → 10
● The evaluation order is specified by evaluation contexts[Felleisen, LFP ’88 & POPL ‘88], e.g.

●E ::= □ ∣ E + t ∣ n + E□ + (3 + 4) is an evaluation context.

1. evaluate the first argument to a number
2. evaluate
the secondargumentan evaluationcontext.
● (1 + 2) + □ is not

4

Muroya (RIMS, Kyoto U.)Is program semantics a TRS?
● No!
● Left-to-right arithmetics is not a TRS.

(1 + 2) + (3 + 4) → 3 + (3 + 4) → 3 + 7 → 10
(1 + 2) + (3 + 4) ↛ (1 + 2) + 7 → 3 + 7 → 10
● The evaluation order is specified by evaluation contexts[Felleisen, LFP ’88 & POPL ‘88], e.g.

●E ::= □ ∣ E + t ∣ n + E□ + (3 + 4) is an evaluation context.

● (1 + 2) + □ is not an evaluation context.

5

Muroya (RIMS, Kyoto U.)Is program semantics a TRS?
● No!
● The evaluation order is specified by evaluation contexts[Felleisen, LFP ’88 & POPL ’88], e.g.

E ::= □ ∣ E + t ∣ n + E● Context-sensitive rewriting [Lucas, ’00] is not enough.
● Question How can then we transfer TRS techniques toprogram semantics?
● e.g. critical pair analysis● Answer Use Term Evaluation Systems, a variant of TRS!

6

Muroya (RIMS, Kyoto U.)Term Evaluation Systems (TES)● evaluation(l → r) ∈ R θ : subst. E ∈ ℰ
E[lθ] →R E[rθ]closed under evaluation contexts ℰ only
● cf. ordinary rewriting(l → r) ∈ R θ : subst. C : context
C[lθ] →R C[rθ]closed under any contexts

7

Muroya (RIMS, Kyoto U.)Term Evaluation Systems (TES)● evaluation(l → r) ∈ R θ : subst. E ∈ ℰ
E[lθ] →R E[rθ]closed under evaluation contexts ℰ only
● cf. ordinary rewriting(l → r) ∈ R θ : subst. C : context
C[lθ] →R C[rθ]enewt
be ngnoit
itir
acr
w
eet
indryndau
sttionauleva

closed under any contexts

8

Muroya (RIMS, Kyoto U.)

Interaction between evaluation and rewriting● From program semantics perspective:terms

t ::= n ∣ t + t ∣ t × t● Question Is refinement correct wrt. evaluation?
● Goal to prove that t ⇒ u implies● s[t]p : →-normalising ⟹ s[u]p : →-normalising
9

Muroya (RIMS, Kyoto U.)

Interaction between evaluation and rewriting (refinement)● From program semantics perspective:
evaluation contexts

E ::= □ ∣ E + t ∣ n + E ∣ E × t ∣ n × E

evaluation rulesm + n → m + n,evaluation relationl→r
EE[l] → E[r]m×n→m×n● Question Is refinement correct wrt. evaluation?
● Goal to prove that t ⇒ u implies● s[t]p : →-normalising ⟹ s[u]p : →-normalising
10

Muroya (RIMS, Kyoto U.)

Interaction between evaluation and rewriting (refinement)● From program semantics perspective:
evaluation contexts

E ::= □ ∣ E + t ∣ n + E ∣ E × t ∣ n × E

evaluation rulesm + n → m + n,evaluation relationl→r
EE[l] → E[r]refinement rulesl × (m + n) ⇒ l × m + l × n,m×n→m×n

m+n⇒m×n● Question Is refinement correct wrt. evaluation?
● Goal to prove that t ⇒ u implies● s[t]p : →-normalising ⟹ s[u]p : →-normalising
11

Muroya (RIMS, Kyoto U.)

Interaction between evaluation and rewriting (refinement)● From program semantics perspective:
evaluation contexts

E ::= □ ∣ E + t ∣ n + E ∣ E × t ∣ n × E

evaluation rulesm + n → m + n,evaluation relationl→rEE[l] → E[r]refinement rulesl × (m + n) ⇒ l × m + l × n,m×n→m×n

m+n⇒m×n● Question Is refinement correct wrt. evaluation?
● Goal to prove that t ⇒ u implies, for any context C,● C[t] : →-normalising ⟹ C[u] : →-normalising
12

Muroya (RIMS, Kyoto U.)

Interaction between evaluation and rewriting (refinement)● From program semantics perspective:
evaluation contexts

E ::= □ ∣ E + t ∣ n + E ∣ E × t ∣ n × E

evaluation rulesm + n → m + n,

evaluation relationl→r
EE[l] → E[r]refinement rulesl × (m + n) ⇒ l × m + l × n,

m×n→m×n
correct

incorrectm+n⇒m×n● Question Is refinement correct wrt. evaluation?
● Goal to prove that t ⇒ u implies, for any context C,● C[t] : →-normalising ⟹ C[u] : →-normalising
13

Muroya (RIMS, Kyoto U.)

Interaction between evaluation and rewriting (refinement)● From TES/TRS perspective:evaluation relation(l → r) ∈ R θ : subst. E ∈ ℰ
E[lθ] →R E[rθ]refinement relation(l ⇒ r) ∈ A θ : subst. C : context
C[lθ] ⇒A C[rθ]● Question Is refinement correct wrt. evaluation?
● Goal to prove that t ⇒A u implies, for any context C,● C[t] : →R-normalising ⟹ C[u] : →R-normalising
14

Muroya (RIMS, Kyoto U.)

Interaction between evaluation and rewriting (refinement)
evaluation relation(l → r) ∈ R θ : subst. E ∈ ℰ
E[lθ ] →R E[r θ ]refinement relation(l ⇒ r) ∈ A θ : subst. C : context
C[lθ ] ⇒A C[r θ ]● Question Is refinement correct wrt. evaluation?
● Goal to prove that t ⇒A u implies, for any context C,● C[t] : →R-normalising ⟹ C[u] : →R-normalising● Sufficient to prove that t ⇒A u implies● t : →R-normalising ⟹ u : →R-normalising
15

Muroya (RIMS, Kyoto U.)

k•Interaction
isAn
given
R-peakby aistriple
given(tbya tevaluation
triple(t1that, s, t2s)and!
suchandss!
!RRt(refinement).
s !R t2 .
1 , s,2 ) such
R trewriting
1that1t2andbetween⇤⇤⇤→ r) ∈ R θ : subst. E ∈ ℰak• (tAnR-peakt2 ) is R-joinable(t1 , s, evaluationt2 ) isifR-joinable
there (lexists
if therea termexists
u sucha termthat ut1 such!R uthatandt1t2!!
relation
1 , s,
R
E[lθ ] →R E[r θ ])-peak• An (A,is givenR)-peakby aistriple
given(tbya ttriple(t that, s, t2s) )sucht1thatandss)!ARt1t2and.
s !R
1 , s,2 )⇒such(lr) ∈ A1 θ : subst.
CA: context
refinement relation

C[lθ ] ⇒A C[r θ ])-peak• An (A,(t1 ,R)-peaks, t2 ) is (t(A,s, t2 ) is (A, R)-joinable
if there existif terms
there exist
u1 , u2terms
such uthat1 , R)-joinable
1 , u2t1su⇤==ndt2u●2!)
uuand.
u)
A2 12 to prove
A u1 . that t ⇒A u implies
Sufficient● t : →R-normalising ⟹ u : →R-normalising⇤⇤/ t2s✏⇤t1s / t2s✏⇤ ✏/ u/ t2✏⇤↵◆[M.,⇤PhD thesis ’20]⇤

t1s/ u2 / t2/ u2↵◆◆↵ = ⇤◆↵ =t1 / ut1s/ t2/ u1/ u1⇤s/ u2 / t 2⇤↵◆◆↵ = ⇤● For deterministic →R, sufficient to prove that t ⇒A u impliess

↵◆

t16
⇤

/
/ u6s

↵◆

t16

/

⇤/
/ u2

↵◆

/

t1 616⇤2t1/ u1/ u2◆↵ =/ u1

local coherence[Aoto & Toyama,LMCS’12]
Muroya (RIMS,KyotoU.)• A position p of a term t is said to be active if t[⇤]p 2 E.

Critical pairlocalcoherence• A term analysis
t is said to be ready iffor
every variable
positionof t is active.
We say a set R of evaluation rules is linear if all its rules are linear on both sides. Similarly,
we say a template A is linear if all its axioms are linear on both sides. We also say a template Ais right-ready if all its axioms have a ready right hand side.
Definition 2.8 (R-peaks, R-joinability, (A, R)-peaks, (A, R)-joinability). Let E(⌃, R) be a TES
with a template A.
• An R-peak is given by a triple (t1 , s, t2 ) such that s !R t1 and s !R t2 .
⇤⇤• An R-peak (t1 , s, t2 ) is R-joinable if there exists a term u such that t1 !R u and t2 !R u.
• An (A, R)-peak is given by a triple (t1 , s, t2 ) such that s )A t1 and s !R t2 .
⇤• An (A, R)-peak (t1 , s, t2 ) is (A, R)-joinable if there exist terms u1 , u2 such that t1 ! u1 ,⇤=t2 ! u2 and u2 )A u1 .

s✏t1⇤/ t2s✏⇤/ u↵◆

t1/ t2⇤⇤/ u2↵◆ =/ u1

Definition 2.9 (local confluence). A TES E(⌃, R) is locally confluent if any R-peak is R-joinable.

Definition 2.10
2.11 (determinism).
(local coherence).
A TES
with
a deterministic
template A isiflocallycoherentrelation
if anyA TESE(⌃,E(⌃,R) isR)
said
to be
its evaluation
000(A,RR)-peak(A,following:R)-joinable.
!
satisfies isthefor any t, u, u 2 T (⌃, X), if t !R u and t !R u then u = u .
In a TES, a term is said to be closed if it has no occurrence of variables.
2Definition 2.12 (program/contextnal refinement). Let E(⌃, R) be a TES with a template A.
• A program refinement between closed terms is given by a relationthat is defined as follows: t prog u i↵ t + implies u +.

prog ✓ T (⌃, R) ⇥ T (⌃, R)• A contextual refinement between terms17
is given by a relation ctxt ✓ T (⌃, R) ⇥MuroyaT (⌃, R)(RIMS,
that Kyoto U.)
is defined as follows: tu i↵ C[t]C[u] for any one-hole context C that makes

II. Term Evaluation Systems (TES) with refinement

The axiom and the rule, however, have the following non-joinable peak, where the variable x
is matched to f (g(y), z) while the variable y is matched to the left hand side g(y) of the rule.

Critical pair analysis for local coherencef f (g(y),z),g(y)/ f f (y,z),g(y)

⇥/

⇥/

⇥↵◆

↵◆

f g(y),f (g(y),z)/ f y,f (g(y),z)

Definition 5.2 (overlaps). Let (l1 ) r1 ) 2 A and (l2 ! r2 ) 2 R.
• A shrinking overlap between (l1 ) r1 ) and (l2 ! r2 ) is given by data (l1 ) r1 , l2 ! r2 , p, ✓),such that p is a non-variable position of l1 and ✓ is a most general unifier between l1 |p andl2 .
• An expanding overlap between (l1 ) r1 ) and (l2 ! r2 ) is given by data (l1 ) r1 , l2 ! r2 , p, ✓),such that p is a non-variable position of l2 and ✓ is a most general unifier between l2 |p andl1 .
Definition 5.3 (critical pairs).
• The (shrinking) critical pair generated by a shrinking overlap (l1 ) r1 , l2 ! r2 , p, ✓) is givenby a triple (r1 ✓, l1 ✓, l1 ✓[r2 ✓]p ).
• The (expanding) critical pair generated by an expanding overlap (l1 ) r1 , l2 ! r2 , p, ✓) is
6given by a triple (l2 ✓[r1 ✓]p , l2 ✓, r2 ✓).
Lemma 5.4 (Critical Pair Lemma). Let ES,V (⌃, R) be a well-behaved TES with a template A.
Let s ) t1 where an axiom (l1 ) r1 ) 2 A is applied to a position q1 of s. Let s ! t2 where anevaluation rule (l2 ! r2 ) 2 R is applied to a position q2 of s. If Var (l1 ) \ Var (l2 ) = ;, R is linear,and A is linear, right-ready and compatible with V , then either of the following holds:
1. the peak (t1 , s, t2 ) is joinable; or,
2. there exist a position p of s and terms u1 , u2 , such that ti = s[ui ]p (i 2 {1, 2}), and (u1 , s|p , u2 )is an instance of a critical pair.
II. Term Evaluation Systems (TES) with refinement

18

Muroya (RIMS, Kyoto U.)

Proof. Let ✓ , ✓ be two substitutions that match (l ) r ) and (l ! r ) respectively to s, i.e.

and moreover, s = s[l2 ✓[x✓[l1 ✓]p2 ]p1 ]q2 , t1 = s[l2 ✓[x✓[r1 ✓]p2 ]p1 ]q2 , and t2 = s[r2 ✓]q2 . Let bea substitution such that (x) = x✓[r1 ✓]p2 and (y) = ✓(y) for any y 6= x. Because the rulel2 ! r2 is linear, the variable x appears only A
once in l2 , and no more than once in r2 . RWe=therefore have t1 = s[l2 [x✓[r1 ✓]p2 ]p1 ]q2 = s[l2 ]q2 ! s[r2 ]q2 , and t2 ) s[r2 ]q2 .

3. Correctness of refinement t ⇒u wrt. evaluation t → uTheorem 5.5 (Critical Pair Theorem). Let ES,V (⌃, R) be a well-behaved TES with a template A.
If R is linear, and A is linear, right-ready and compatible with V , the TES ES,V (⌃, R) with thetemplate A is locally coherent if and only if every critical pair is joinable.
Proof. The “if” part is a consequence of Lem. 5.4 and Lem. 3.2. Using Lem. 3.2, we can show thefollowing: any terms t, u such that t ! u and any evaluation context E 2 E satisfy E[t] ! E[u];• well-behaved
withany
a notionof values
and,any terms t, evaluationu such thatcontexts,t ! u andsubstitution✓ satisfy t✓ ! u✓.
The “only if” part is straightforward, because every critical pair (u1 , t, u2 ) satisfies t ) u1 andt ! u2 .• ℰ is defined by a certain BNF, e.g.: E ::= □ ∣ ⋯ ∣ f (v, E ) ∣ f (E, t)• linear rules6Far simulation for contextual refinement

6.1

Far simulation• l, r are linear terms in (l → r) ∈ R, (l ⇒ r) ∈ A• right-ready rules
Our methodology is to use a simulation notion to prove program refinement, which is an asymmetricversion•• ofprogram
equivalence.
definetheAE(⌃,
setaAvariableofwe
axiomswhere(l ) simulationr)r[2A2 Tnotion,(⌃, X). dubbed far simulation, forr of (lof⇒r)R)∈is given
A, ifbypaisHere□i↵ ]l,pr ∈ℰ
intemplate
position,
general• term
It is anof X)
a simulation
notion [3, Def. 4.4.1] that was
Given arewriting
template A, systems.
the rewrite relation)A adaptation✓ T (⌃, X) ⇥ T (⌃,is defined as follows:t )A u i↵there exist arefinement
position p of t, withan axiom(l ) r) 2 A andoperationala substitution ✓,semantics.
such thatused to prove
programa particulart|p = l✓ andu|p =wrt.
r✓. values Vrules• compatible
Definition
6.1 (farsimulation).
Given
setA,T (⌃,and! and• A template
A is said
to be compatible
with aaset
V 2X) twoif, forrelations
any v 2 V andany R on A, the relation R is1(l ) r) 2 A,
exist a theposition
p and a substitution✓ such that v[l✓]a far simulation
if ifittheresatisfies
following:(Termination)
R p 2 V# and✓ +, and (Step) R 1 ! ✓⇤v[r✓]⇤ 62 V , then v[r✓]p !R v[l✓]p .
⇤! R 1 p.
Lemma 2.4. The rewrite relation )A is closed under substitutions, and closed under contexts inC (1) (⌃,X).
Farsimulationin fact satisfies a stronger condition than the condition (Termination), when

While therelation !R represents dynamics of a TES E(⌃, R), the rewrite relation
the relation!evaluation
is deterministic.

II. Term Evaluation
withequationalrefinement
19 respected by the dynamics. To em)ASystems
represents(TES)a staticalproperty that should be

Muroya (RIMS, Kyoto U.)

Overview● Term Evaluation Systems with refinement (ordinary rewriting)evaluation relation(l → r) ∈ R θ : subst. E ∈ ℰ
E[lθ] →R E[rθ]refinement relation(l ⇒ r) ∈ A θ : subst. C : context
C[lθ] ⇒A C[rθ]● Question Is refinement correct wrt. evaluation?
● Goal to prove that t ⇒A u implies, for any context C,● C[t] : →R-normalising ⟹ C[u] : →R-normalising
20

Muroya (RIMS, Kyoto U.)