Term Evaluation Systems
with Refinements
Koko Muroya(RIMS, Kyoto University)

Makoto Hamana(Kyusyu Institute of Technology)

FLOPS 2024 (Kumamoto), 15 May 2024

Two kinds of rewriting in functional programming
evaluation

refinement

run-time rewriting

compile-time rewriting
beta-lawC[(λx . t) v] ⇒ C[t{v/x}]

beta-reduction

E[(λx . t) v] → E[t{v/x}]

eta-law

C[λx . v x] ⇒ C[v]2Muroya (RIMS, Kyoto U.)

Two kinds of rewriting in functional programming● with different roles:
evaluation

refinement

run-time rewriting

compile-time rewriting
beta-lawC[(λx . t) v] ⇒ C[t{v/x}]

beta-reduction

E[(λx . t) v] → E[t{v/x}]

eta-law

C[λx . v x] ⇒ C[v]specification ofoperational semantics

model of optimisation
to be validated wrt. evaluation

3

Muroya (RIMS, Kyoto U.)

Validation of refinement ⇒ wrt. evaluation →● by proving contextual improvement [Sands ’96]
● “two terms t, u have the same result, and u requires fewer steps than t ”
Δk● t ⪯ u ⟺ ∀C, v, v′ . if C[t] →mv then C[u] → v′ ∧ v =Val v′ ∧ k ≥ mλx . t =Val λx′ . t′n =Val n● namely, by proving: refinement t ⇒ u implies contextual improvement t ⪯ u￼￼￼￼￼

● our goal: develop a proof methodology

4

Muroya (RIMS, Kyoto U.)Our goal● develop a proof methodology● to validate refinement ⇒ wrt. evaluation →● to establish: refinement ⇒ implies contextual improvement ⪯● by a rewriting-theoretic approachcontribution 1● exploiting critical pair analysis● in the hope of (partial) automation● by rewriting-theoretic modelling of both refinement ⇒ and evaluation →contribution 2
5

Muroya (RIMS, Kyoto U.)Our goal● develop a proof methodology● to validate refinement ⇒ wrt. evaluation →● to establish: refinement ⇒ implies contextual improvement ⪯● by a rewriting-theoretic approachcontribution 1● exploiting critical pair analysis● in the hope of (partial) automation● by rewriting-theoretic modelling of both refinement ⇒ and evaluation →contribution 2
6

Muroya (RIMS, Kyoto U.)

Modelling evaluation → and refinement ⇒● being aware of different rewriting-theoretic properties!
evaluation

refinement

run-time rewriting

compile-time rewriting
beta-lawC[(λx . t) v] ⇒ C[t{v/x}]

beta-reduction

E[(λx . t) v] → E[t{v/x}]

eta-law

C[λx . v x] ⇒ C[v]rule-based rewriting

rule-based rewriting

restricted byevaluation contexts [Felleisen ’88]

unrestricted

new kind of rewriting

7

general, standard, rewriting

Muroya (RIMS, Kyoto U.)

Modelling evaluation → and refinement ⇒● being aware of different rewriting-theoretic properties!
evaluation

refinement

run-time rewriting

compile-time rewriting
beta-lawC[(λx . t) v] ⇒ C[t{v/x}]

beta-reduction

E[(λx . t) v] → E[t{v/x}]

new kind of rewriting

eta-law

C[λx . v x] ⇒ C[v]8general, standard, rewriting

Muroya (RIMS, Kyoto U.)

Modelling evaluation → and refinement ⇒: an example● being aware of different rewriting-theoretic properties!
evaluation

refinement

therun-timeleft-to-rightrewriting
call-by-value
λ-calculus

compile-time rewritingt ::= x ∣ λx . t ∣ t@tv ∈ Val ::=λx . tbeta-reduction
E E[(λx∈ Ectx ::=□∣E@t∣
v@E. t) v] → E[t{v/x}]ℰ = {(λx . t)@v → t{v/x}}

beta-law

new kind of rewriting. t)□v]∣ λx⇒. CC[t{v/x}]CC[(λx∈ Ctx ::=∣ E@t ∣ t@E(λx . t)@v ⇒ t{v/x},ℛ={}
eta-law
λx . v@x⇒vC[λx . v x] ⇒ C[v]9general, standard, rewriting

Muroya (RIMS, Kyoto U.)

Modelling evaluation → and refinement ⇒: an example● being aware of different rewriting-theoretic properties!

termsevaluation

refinement

therun-timeleft-to-rightrewritingcall-by-value
λ-calculus

compile-time rewritingt ::= x ∣ λx . t ∣ t@tv ∈ Val ::=λx . tbeta-reduction
E E[(λx∈ Ectx ::=□∣E@t∣
v@E. t) v] → E[t{v/x}]ℰ = {(λx . t)@v → t{v/x}}

beta-law. t)□v]∣ λx⇒. CC[t{v/x}]CC[(λx∈ Ctx ::=∣ E@t ∣ t@E(λx . t)@v ⇒ t{v/x},ℛ={}
eta-law
λx . v@x⇒vC[λx . v x] ⇒ C[v]

Σ = {λ, @}new kind of rewriting

10general, standard, rewriting

Muroya (RIMS, Kyoto U.)

Modelling evaluation → and refinement ⇒: an example● being aware of different rewriting-theoretic properties!

valuesevaluation

refinement

therun-timeleft-to-rightrewriting
call-by-value
λ-calculus

compile-time rewritingt ::= x ∣ λx . t ∣ t@tv ∈ Val ::=λx . tbeta-reduction
E E[(λx∈ Ectx ::=□∣E@t∣
v@E. t) v] → E[t{v/x}]ℰ = {(λx . t)@v → t{v/x}}

beta-law𝖥𝖭Val ⊆. t)□v]∣ λx⇒. CC[t{v/x}]CC[(λx∈ Ctx ::=∣ E@t ∣ t@E(λx . t)@v ⇒ t{v/x},ℛ={}
eta-law
λx . v@x⇒vC[λx . v x] ⇒ C[v]( →ℰ )

new kind of rewriting

11general, standard, rewriting

Muroya (RIMS, Kyoto U.)

Modelling evaluation → and refinement ⇒: an example● being aware of different rewriting-theoretic properties!

valuesevaluation

refinement

therun-timeleft-to-rightrewriting
call-by-value
λ-calculus

compile-time rewritingt ::= x ∣ λx . t ∣ t@tv ∈ Val ::=λx . tbeta-reduction
E E[(λx∈ Ectx ::=□∣E@t∣v@E. t) v] → E[t{v/x}]ℰ = {(λx . t)@v → t{v/x}}

beta-law

λx . x ∈ Val,. t)□v]∣ λx⇒. CC[t{v/x}]CC[(λx∈ Ctx ::=∣ E@t ∣ t@E(λx . t)@v ⇒ t{v/x},ℛ={}
eta-law
λx . v@x⇒vC[λx . v x] ⇒ C[v]x@y ∉ Val

new kind of rewriting

12general, standard, rewriting

Muroya (RIMS, Kyoto U.)

Modelling evaluation → and refinement ⇒: an example● being aware of different rewriting-theoretic properties!

evaluation contexts

evaluation

refinementtherun-timeleft-to-rightrewriting
call-by-value
λ-calculus

compile-time rewritingt ::= x ∣ λx . t ∣ t@tv ∈ Val ::=λx . tbeta-reduction
E E[(λx∈ Ectx ::=□∣E@t∣
v@E. t) v] → E[t{v/x}]ℰ = {(λx . t)@v → t{v/x}}

beta-law□ @x ∈ Ectx,. t)□v]∣ λx⇒. CC[t{v/x}]CC[(λx∈ Ctx ::=∣ E@t ∣ t@E(λx . t)@v ⇒ t{v/x},ℛ={}
eta-law
λx . v@x⇒vC[λx . v x] ⇒ C[v](λx . x)@ □ ∈ Ectx

new kind of rewriting

13

general, standard, rewriting

Muroya (RIMS, Kyoto U.)

Modelling evaluation → and refinement ⇒: an example● being aware of different rewriting-theoretic properties!

evaluation contexts

evaluation

refinement

therun-timeleft-to-rightrewriting
call-by-value
λ-calculus

compile-time rewritingt ::= x ∣ λx . t ∣ t@t
v ∈ Val ::=λx . tbeta-reduction
E E[(λx∈ Ectx ::=□∣E@t∣v@E. t) v] → E[t{v/x}]ℰ = {(λx . t)@v → t{v/x}}

beta-law□ @x ∈ Ectx,. t)□v]∣ λx⇒. CC[t{v/x}]CC[(λx∈ Ctx ::=∣ E@t ∣ t@E(λx . t)@v ⇒ t{v/x},ℛ={}
eta-law
λx . v@x⇒vC[λx . v x] ⇒ C[v]((λx . x)@y)@ □ ∉ Ectx

new kind of rewriting

14

general, standard, rewriting

Muroya (RIMS, Kyoto U.)

Modelling evaluation → and refinement ⇒: an example● being aware of different rewriting-theoretic properties!

evaluation rules

evaluation

refinement

therun-timeleft-to-rightrewriting
call-by-value
λ-calculus

compile-time rewritingt ::= x ∣ λx . t ∣ t@tv ∈ Val ::=λx . t
beta-reduction
E E[(λx∈ Ectx ::=□∣
E@t∣v@E. t) v] → E[t{v/x}]ℰ = {(λx . t)@v → t{v/x}}

beta-law. t)□v]∣ λx⇒. CC[t{v/x}]CC[(λx∈ Ctx ::=∣ E@t ∣ t@E(λx . t)@v ⇒ t{v/x},ℛ={}
eta-law
λx . v@x⇒vC[λx . v x] ⇒ C[v](λx . x)@y →ℰ y

new kind of rewriting

15general, standard, rewriting

Muroya (RIMS, Kyoto U.)

Modelling evaluation → and refinement ⇒: an example● being aware of different rewriting-theoretic properties!

evaluation rules

evaluation

refinement

therun-timeleft-to-rightrewriting
call-by-value
λ-calculus

compile-time rewritingt ::= x ∣ λx . t ∣ t@tv ∈ Val ::=λx . tbeta-reduction
E E[(λx∈ Ectx ::=□∣E@t∣
v@E. t) v] → E[t{v/x}]ℰ = {(λx . t)@v → t{v/x}}

beta-law. t)□v]∣ λx⇒. CC[t{v/x}]CC[(λx∈ Ctx ::=∣ E@t ∣ t@E(λx . t)@v ⇒ t{v/x},ℛ={}
eta-law
λx . v@x⇒vC[λx . v x] ⇒ C[v](λx . x)@(y@z) ↛ℰ

new kind of rewriting

16

general, standard, rewriting

Muroya (RIMS, Kyoto U.)

Modelling evaluation → and refinement ⇒: an example● being aware of different rewriting-theoretic properties!
evaluation

refinement

therun-timeleft-to-rightrewriting
call-by-value
λ-calculus

compile-time rewritingt ::= x ∣ λx . t ∣ t@t
v ∈ Val ::=λx . tbeta-reduction
E E[(λx∈ Ectx ::=□∣E@t∣
v@E. t) v] → E[t{v/x}]ℰ = {(λx . t)@v → t{v/x}}

beta-law. t)□v]∣ λx⇒. CC[t{v/x}]CC[(λx∈ Ctx ::=∣ E@t ∣ t@E(λx . t)@v ⇒ t{v/x},ℛ={}
eta-law
λx . v@x⇒vC[λx . v x] ⇒ C[v]λx . □ ∈ Ctx,

new kind of rewriting(arbitrary) contexts

17((λx . x)@y)@ □ ∈ Ctx

general, standard, rewriting

Muroya (RIMS, Kyoto U.)

Modelling evaluation → and refinement ⇒: an example● being aware of different rewriting-theoretic properties!
evaluationrefinementtherun-timeleft-to-rightrewriting
call-by-value
λ-calculus

compile-time rewritingt ::= x ∣ λx . t ∣ t@tv ∈ Val ::=λx . tbeta-reduction
E E[(λx∈ Ectx ::=□∣E@t∣
v@E. t) v] → E[t{v/x}]ℰ = {(λx . t)@v → t{v/x}}

beta-law

new kind of rewriting. t)□v]∣ λx⇒. CC[t{v/x}]CC[(λx∈ Ctx ::=∣ E@t ∣ t@E(λx . t)@v ⇒ t{v/x},ℛ={}
eta-law
λx . v@x⇒v

refinement rules

C[λx . v x] ⇒ C[v]18general, standard, rewriting

Muroya (RIMS, Kyoto U.)Term Evaluation and Refinement Systems (TERS)
Def. A TERS (Σ, ℰ, ℛ, Ectx, SClass) is given by:● a signature Σ● a set ℰ of evaluation rules l → r● a set ℛ of refinement rules l ⇒ r● a set Ectx ⊆ Ctx of evaluation contexts( →ℰ )𝖥𝖭● a set SClass of syntax classes including Val ⊆19

Muroya (RIMS, Kyoto U.)Term Evaluation and Refinement Systems (TERS)
Ex. A TERS CBVλ for the left-to-right call-by-value λ-calculus● a signature Σ = {λ, @}● a set ℰ = {(λx . t)@v → t{v/x}} of an evaluation rule
● a set ℛ = {(λx . t)@v ⇒ t{v/x},λx . v@x ⇒ v} of refinement rules● evaluation contexts E ∈ Ectx ::= □ ∣ E@t ∣ v@E( →ℰ )𝖥𝖭● a set SClass of syntax classes including Val = {λx . t} ⊆20

Muroya (RIMS, Kyoto U.)Term Evaluation and Refinement Systems (TERS)
Ex. A TERS Hndl for a λ-calculus with e ect handlers [Pretnar ’15]

ff21

Muroya (RIMS, Kyoto U.)Our goal● develop a proof methodology● to validate refinement ⇒ wrt. evaluation →● to establish refinement ⇒ implies contextual improvement ⪯● by a rewriting-theoretic approachcontribution 1● exploiting critical pair analysis● in the hope of (partial) automation● by rewriting-theoretic modelling of both refinement ⇒ and evaluation →as Term Evaluation and Refinement Systems (TERS)
contribution 2

22

Muroya (RIMS, Kyoto U.)Our goal● develop a proof methodology● to validate refinement ⇒ wrt. evaluation →● to establish refinement ⇒ implies contextual improvement ⪯● by a rewriting-theoretic approachcontribution 1● exploiting critical pair analysis● in the hope of (partial) automation● by rewriting-theoretic modelling of both refinement ⇒ and evaluation →as Term Evaluation and Refinement Systems (TERS)
contribution 2

23

Muroya (RIMS, Kyoto U.)

Sufficient conditions for contextual improvement ⪯Thm. (su cient conditions for improvement)
If a TERS is● deterministic● value-invariant
akin to local coherence
for equational rewriting[Huet ’80] [Aoto & Toyama ’12]

● locally coherent,then refinement ℛ is contextual improvement w.r.t. evaluation ℰ(i.e. t ⪯ u for each t ⇒ℛ u)
ffi

24

Muroya (RIMS, Kyoto U.)

Sufficient conditions for contextual improvement ⪯Thm. (su cient conditions for improvement)
If a TERS is● deterministic

feasiblepen-and-paperproof● value-invariant
tedious, error-prone,case analysis● locally coherent,

where critical pair analysis canhelp!

then refinement ℛ is contextual improvement w.r.t. evaluation ℰ(i.e. t ⪯ u for each t ⇒ℛ u)ffi

25

Muroya (RIMS, Kyoto U.)

Sufficient conditions for contextual improvement ⪯Thm. (critical pair theorem)
A well-behaved TERS
● refinement respecting evaluation contexts

feasiblepen-and-paperproof● linearity for (l ⇒ r) ∈ ℛ● left-linearity for (l → r) ∈ ℰ● lhs l being Miller’s HO pattern for (l ⊸ r) ∈ ℛ ∪ ℰ● …
is locally coherent iff every critical pair is joinable.

26

automatedenumeration &joinability check

Muroya (RIMS, Kyoto U.)Term Evaluation and Refinement Systems (TERS)
Ex. A TERS CBVλ for the left-to-right call-by-value λ-calculus● a signature Σ = {λ, @}● a set ℰ = {(λx . t)@v → t{v/x}} of an evaluation rule
● a set ℛ = {(λx . t)@v ⇒ t{v/x},λx . v@x ⇒ v} of refinement rules● evaluation contexts E ∈ Ectx ::= □ ∣ E@t ∣ v@E● a set SClass of syntax classes including Val = {λx . t} ⊆( →ℰ )Prop. For the TERS CBVλ, refinement ℛ is contextual improvement ⪯.
✓ determinism✓ value-invariance✓ local coherence✓ well-behavedness

automaticallyenumerated & checked𝖥𝖭✓ 2 critical pairs joinable
27

Muroya (RIMS, Kyoto U.)Term Evaluation and Refinement Systems (TERS)
Ex. A TERS Hndl for a λ-calculus with e ect handlers [Pretnar ’15]
Prop. For the TERS Hndl,
refinement ℛ iscontextual improvement ⪯.
✓ determinism✓ value-invariance✓ local coherence✓ well-behavedness✓ 10 critical pairs joinableff28

automatically enumerated & checked

Muroya (RIMS, Kyoto U.)

Overview
evaluation

refinement

run-time rewriting

compile-time rewriting

specification ofoperational semantics

model of optimisation
to be validated wrt. evaluation

formalise Term
Evaluation andRefinement Systems(TERS)(Σ, ℰ, ℛ, Ectx, SClass)29

Muroya (RIMS, Kyoto U.)

Overview
evaluation

refinement

run-time rewriting

compile-time rewriting

specification ofoperational semantics

model of optimisation
to be validated wrt. evaluation30• formally, contextual
improvement• develop a proof
methodology
centred around
critical pair analysis

Muroya (RIMS, Kyoto U.)