Preorder-Constrained
Simulations for Program
Refinement with Effects
Koko Muroya(RIMS, Kyoto University)
Takahiro Sanada(RIMS, Kyoto University)

Natsuki Urabe(NII)
CMCS (Luxembourg), 6 April 2024

Today’s topic● a coinductive technique forquantitative equational reasoning on effectful programs

2

Muroya (RIMS, Kyoto U.)

Quantitative equational reasoning● “p behaves the same as p′
and p′ terminates with a less number of steps”● p ⇓n ⟹ p′ ⇓m ∧ n ≥ m￼￼￼● (basic) quantitative notion of observational refinement

3

Muroya (RIMS, Kyoto U.)Quantitative equational reasoning● “p behaves the same as p′and p′ terminates with a certain number of steps”● (p ⇓nΔm⟹ p′ ⇓ ∧ n Q m) ⟺ p ⪯Q p′given a “length preorder” Q ⊆ ℕ × ℕ￼￼￼￼● (basic) quantitative notion of observational refinement

4

Muroya (RIMS, Kyoto U.)

A coinductive approach● stepwise reasoning on execution traces, using
nondeterministic
automata Simulations for Program Refinement with Effects
23:6
Preorder-Constrained● e.g. standard simulationxÕÕwxÕaR yx

xÕÕ RwyÕxÕaR ywx● (FYI: simulation is the asymmetric version of bisimulation)● p ⪯= p′x

ΔRy(a) C-Final (p ⇓n ⟹ p′(b) C-Step(1) where⟺⇓m ∧n =x ” m)ÕÕ(c) C-Step (2) where

Figure 4 Conditions of Def. 4. Black parts are universally quantified, and magen
existentially quantified.

⟸ p R p′ such thatx(a) Final

￼￼

176
177
178

y(b) Step

xÕÕ ”œ F1 ). A term err() œ T err is an example of such a state in A err . Lastly, Ca
the key condition of Def. 4. It asserts that any transition x
xÕ followed by someÕ wx

wÕ

x in A1 can be simulated by some transitions yy Õ in A2 .
Muroya (RIMS, Kyoto U.)
5Thanks to C-Step, which
compares not just single steps
but numbers of stepÕÕ

￼175

RR ÕyxÕ
aaR yx

● stepwise reasoning on execution traces, using
nondeterministic automata● parameterised by a length preorder Q ⊆ ℕ × ℕ● (FYI: simulation is the asymmetric version of bisimulation)
ΔQp′ ⟺ (p ⇓n ⟹ p′ ⇓m ∧ n Q m)

● p⪯

23:6
Preorder-ConstrainedSimulations
for Program Refinement with
Preorder-Constrained Simulations
for Program Refinementwith Effects⟸ p R p′ such thatxRyxÕÕw
xÕaR Rx x yy(a) C-Final(b) C-Step(1) where xÕÕ ”(a) C-FinalÕÕxÕÕ Rxww
xÕy ÕxÕ
ÕaaR yR x ywxw

a(b) C-Step(1) wherex Õ” |(c) C-Step(2) where|aw|Q|w
ÕÕ(c) C-Step￼￼Conditionsof quantified,Def. 4. Blackare universally
Figure 4 Conditions of Def. 4. BlackFigure
parts 4areuniversallyandparts
magentaparts are quantified, aexistentially quantified.
existentially quantified.
￼6Counting simulation [M. 2020]

6Muroya (RIMS, Kyoto U.)

Counting simulation [M. 2020]
nondeterministic automata● p⪯QΔp′ ⟺ (p ⇓n ⟹ p′ ⇓m ∧ n Q m)

23:6
Preorder-Constrained
Simulations
for Program Refinement with
Preorder-Constrained Simulations
for Program Refinementwith Effects⟸ p R p′ such thatxRxÕÕwxÕaR Rx x yyÕÕxÕÕ Rxw
w
xÕy Õ
xÕ
Õ
aaR y
R x ywxy(a) C-Final(b) C-Step(1) where xÕÕ ”(a) C-Final(b) C-Step(1) wherexÕÕ Õ” |(c) C-Step(2) where|aw|Q|w(c) C-St

Conditionsof quantified,Def. 4. Blackare universally
Figure 4 Conditions of Def. 4. BlackFigure
parts 4areuniversally
andparts
magentaparts are quantified,existentially quantified.
existentially quantified.
4● soundness
only
for “deterministic”
programs
4XX
4
4·
3
33+1·
·
3 + (0 + 1)3 + 0

33·3+0￼￼

in0
in1
3 + in(0, 0 + 1)

33·
3+0·
in0
in1
3+in(0,0+1)
1+2+07·● or “branching-free” automata￼3:6● stepwise reasoning on execution traces, using·X
3+1·
5
3 + (0 + 1)

33·
3+0·
1+2+0 U.)
5
Muroya(RIMS,Kyoto

Counting simulation [M. 2020]● Today’s topic: a coinductive technique for quantitative equational
reasoning on effectful programs● Goal: extend counting simulation to a wider class of effects

8

Muroya (RIMS, Kyoto U.)

Overview● Goal: extend counting simulation to a wider class of effects● Challenge 1:● Solution 1:● Challenge 2:● Solution 2:● Contribution:

9

Muroya (RIMS, Kyoto U.)

Challenge 1: varying observation● ✅ exception
Qtermination onlyΔp ⪯ p′ ⟺ (p ⇓n ⟹ p′ ⇓m ∧ n Q m)
● ❌ nondeterminism
QresultΔp ⪯ p′ ⟺ (p ⇓n v ⟹ p′ ⇓m v ∧ n Q m)
● ❌ I/OΔ10￼

￼

￼

￼

￼

p ⪯ p′ ⟺ (p ⇓n (v, tr) ⟹ p′ ⇓m (v, tr) ∧ n Q m)

￼Qresult, and trace of I/O values

Muroya (RIMS, Kyoto U.)

● internal vs. external choice● nondeterminism: internal, unobservable choice(1,1) ⇓ 1 ⟹ 1 ⇓ 1 ∧ 1 = 1coincidence of results● input: external, observable choice(1,1) ⇓ (1,i)⟹ 1 ⇓ (1,ε) ∧ 1 = 1𝚗𝚒𝚛coincidence of results, but
no coincidence of I/O traces𝚗𝚘𝚒

Challenge 1: varying observation

11

Muroya (RIMS, Kyoto U.)

● program trace tr ∈ Σ*
where Σ = {τ} ∪ ℕ ∪ Ωpurecomputation

effect traces
execution
result(e.g.

10)● examples:● Tr((1,2)) = {01,12}● Tr((1,2)) = {01,12}● Tr(1) = {1}𝚛𝚗𝚘𝚒𝚛𝚗𝚘𝚒𝚛𝚗𝚘𝚗𝚒𝚒● Tr(1 + 1) = {τ2}𝚛𝚘Solution 1: “observation preorder” on traces

12Muroya (RIMS, Kyoto U.)

● program trace tr ∈ Σ*
where Σ = {τ} ∪ ℕ ∪ Ωpurecomputation

effect traces(e.g.

execution
resultl0p1l1

⋯

lkn𝚗𝚒

● in general: p0

𝚛𝚘Solution 1: “observation preorder” on traces

13n10)✓Muroya (RIMS, Kyoto U.)

Solution 1: “observation preorder” on traces● program trace tr ∈ Σ*
where Σ = {τ} ∪ ℕ ∪ Ωpurecomputation

effect traces
execution
result(e.g.

0)⊆ Σ* × Σ*𝚗𝚒𝚛𝚘𝒬● introducing “observation preorder”

114

Muroya (RIMS, Kyoto U.)

Solution 1: “observation preorder” on traces● program trace tr ∈ Σ*
where Σ = {τ} ∪ ℕ ∪ Ωpurecomputation

effect traces
executionresult(e.g.

● introducing “observation preorder”

10)⊆ Σ* × Σ*● e.g. lifted length preorder:𝚗𝚒𝚛𝚘𝒬

Δ·given Q ⊆ ℕ × ℕ, t Q u ⟺ | t | Q | u |15

Muroya (RIMS, Kyoto U.)

Solution 1: “observation preorder” on traces● program trace tr ∈ Σ*
where Σ = {τ} ∪ ℕ ∪ Ωpurecomputation
executionresult(e.g.

10)⊆ Σ* × Σ*● introducing “observation preorder”● e.g. “filtered equality”
given Σ′ ⊆ Σ,Δt =(remΣ′) u ⟺ t and u are the same except for Σ′𝚗￼𝚒𝒬￼￼● τabτcττ =(rem{τ}) abc

𝚛𝚘effect traces

16Muroya (RIMS, Kyoto U.)

Solution 1: “observation preorder” on traces● program trace tr ∈ Σ*
where Σ = {τ} ∪ ℕ ∪ Ωpurecomputation

effect traces
executionresult(e.g.

0)⊆ Σ* × Σ*𝚗𝚒𝚛𝚘𝒬● introducing “observation preorder”

117

Muroya (RIMS, Kyoto U.)

Solution 1: “observation preorder” on traces● program trace tr ∈ Σ*

Σ = {τ}ℕ ∪Simulations
Ω Refinement
where3:2
strained
Preorder-Constrained
Simulations
for∪Programfor Programwith Effects
Refinement with Effec

pureeffect tracescomputation(e.g.
Q-similarity
Q-trace
Q-similarity
inclusion
Qy(1,(2,Q)-similarity
Q)-similarity(2, Q)-similarity
1 0)
≠æ≠æ
≠æ
···≠æ
≠æ
··Ωæ
·≠æΩæexecution.Q
ıQ.Qı
..1,Q.2,Q
2,Qresulte generativeFigure
spectrum,
1 The
parameterised
generative spectrum,by the observation
parameterised
preorderby theQ observation preorderon preorder Q observation(1, Q)-simulation
preorder Q(1, Q)-simulation
Q-trace inclusion ıQ● introducing “observation preorder”==rem{· }Q̇=rem{· }ﬁndstandard= simulation
weak=remsimulation{· }Q̇instances)Q̇(newﬂ =rem{· }ﬁ nd⊆ Σ* × Σ*

Q-trace inclusion ı

standard
finitesimulation
trace inclusion
finite trace inclusi
weakweaksimulation
trace inclusion
weak trace inclusi
refinement ∞Q
refinement ∞Q
err for exception
err for exc
Q(new instances)refinement∞Qfor
nondeterminism
refinement∞ndnd for nondet

𝚗𝚒𝚛𝚘𝒬

Q
ﬂ =rem{· }Q̇ ﬂ =rem{· }refinement ∞Q
for
I/O
refinement∞io
io for I
ances of theTable
two ends
1 Instancesof the generativeof the twospectrum
ends of the(seegenerativeSec. 5 forspectrum
details) (see Sec. 5 for de18

Muroya (RIMS, Kyoto U.)

Examples≤, ⪯= , ⪯ =𝗈𝗂𝖽𝗇𝗋𝗋𝖾● exhibit quantitative refinement ⪯19

Muroya (RIMS, Kyoto U.)

Overview● Goal: extend counting simulation to a wider class of effects● Starting point: ✅ exception ❌ nondeterminism ❌ I/O● Challenge 1: varying observation● Solution 1: “observation preorder” on traces● Challenge 2:● Solution 2:● Contribution:20

Muroya (RIMS, Kyoto U.)

Challenge 2: branching effects● ✅ exception● ❌ nondeterminism● ❌ I/O● unsoundness of counting simulation for branching effects● due to incomplete inspection of branches
23:6

23:6
Preorder-ConstrainedSimulations
for Program Refinement with EffectsPreorder-Constrained Simulations
for Program Refinementwith Effects

cf. definition of counting simulationxRxÕÕwxÕaR Rx x yyy(a) C-Final(b) C-Step(1) where xÕÕ ”(a) C-Final

ÕÕxÕÕ Rxww
xÕy ÕxÕÕaaR y
R x ywx

xÕÕ RwyxÕaR yx(b) C-Step(1) wherex Õ” |(c) C-Step(2) where|aw|Q|w
ÕÕ(c) C-Step (2) wher

Conditionsof quantified,Def. 4. Blackare universally
Figure 4 Conditions of Def. 4. BlackFigure
parts 4areuniversally
andparts
magentaparts are quantified, and mageexistentially quantified.
existentially quantified.

21

Muroya (RIMS, Kyoto U.)

Solution 2: limited ∃● from unlimited ∃ to limited ∃Refinement with Effects 23:8

Preorder-Constrained Simulations for ProgrxM

xÕÕ Rw
yÕxÕ
Õ
aw
R yx

yÕxÕÕw
w
R yx

w

R

yÕÕw
R yx

xkx

yÕR ywM
where (b) Step M where (c) Final 1 w(c) C-Step (2) where |aw|Q|wÕ |(a) Final|w| < M · wQwÕ a1 · · · ak QwÕÁQwÕ”

rsally quantified, and magenta parts areFigure 6 Conditions of Def. 9. Black parts areexistentially quantified.

● enabling full inspection of branches
3·3+03X2425243

When an (M, Q)-simulation (resp. Q-simulsimilar (resp. Q-similar) to y and write x .
22

Muroya (RIMS, Kyoto U.)

Overview● Goal: extend counting simulation to a wider class of effects● Starting point: ✅ exception ❌ nondeterminism ❌ I/O● Challenge 1: varying observation● Solution 1: “observation preorder” on traces● Challenge 2: branching effects● Solution 2: limited ∃● Contribution:23

Muroya (RIMS, Kyoto U.)

Contribution: (M,)-simulation● parameterised by● “look-ahead bound” M ∈ ℕ+

∈ Σ* × Σ*𝒬𝒬● observation preorder

24

Muroya (RIMS, Kyoto U.)

Contribution: (M,)-simulation● parameterised by● “look-ahead bound” M ∈ ℕ+

∈ Σ* × Σ*𝒬𝒬● observation preorder

25

Muroya (RIMS, Kyoto U.)

Contribution: (M,)-simulation● parameterised by● “look-ahead bound” M ∈ ℕ+

∈ Σ* × Σ*𝒬𝒬● observation preorder

26

Muroya (RIMS, Kyoto U.)

Examples of (M,)-simulations· -simulation for (a)(2,≤)●(1, =· ∪ =rem{τ}∪Ω )-simulation for (b)●(2, =· ∪ =rem{τ} )-simulation for (c)𝒬●27

Muroya (RIMS, Kyoto U.)

Overview● Goal: extend counting simulation to a wider class of effects● Starting point: ✅ exception ❌ nondeterminism ❌ I/O● Challenge 1: varying observation● Solution 1: “observation preorder” on traces● Challenge 2: branching effects● Solution 2: limited ∃● Contribution: (M,)-simulation

𝒬● Result: ✅ exception ✅ nondeterminism ✅ I/O
28

Muroya (RIMS, Kyoto U.)

Overview● Goal: extend counting simulation to a wider class of effects● Starting point: ✅ exception ❌ nondeterminism ❌ I/O● Challenge 1: varying observation● Solution 1: “observation preorder” on traces● Challenge 2: branching effects● Solution 2: limited ∃● Contribution: a generative spectrum of (M,)-simulations

𝒬● Result: ✅ exception ✅ nondeterminism ✅ I/O29

Muroya (RIMS, Kyoto U.))-simulations

𝒬

A generative spectrum of (M,30

Muroya (RIMS, Kyoto U.)

Overview● Goal: extend counting simulation to a wider class of effects● Starting point: ✅ exception ❌ nondeterminism ❌ I/O● Challenge 1: varying observation● Solution 1: “observation preorder” on traces● Challenge 2: branching effects● Solution 2: limited ∃● Contribution: a generative spectrum of (M,)-simulations

𝒬● Result: ✅ exception ✅ nondeterminism ✅ I/O
31

Muroya (RIMS, Kyoto U.)● ❌ probabilistic choice● a naive attempt yields a false refinement:0.5(1,1) ⊑≤+0.5(0,1)● Idea: from nondeterministic automata to weighted𝚛𝚘automata?

𝚛𝚘

Future work 1: bunching branches

32

Muroya (RIMS, Kyoto U.)?
Q● p⪯p′ ⟸ p ≲M, p′ for nondeterministic automata(p),(p′)that represent whole execution of p, p′⟸ reachability in a graph “pairing”(p) with(p′)● polynomial time solving, based on whole execution 😐
● Idea: solving without executing programs

￼
￼

𝒜

￼

￼

𝒬

● using TRS techniques? [M. & Hamana, FLOPS ’24]

￼𝒜𝒜𝒜

Future work 2: efficient solving

33

Muroya (RIMS, Kyoto U.)

Overview● Goal: extend counting simulation to a wider class of effects● Starting point: ✅ exception ❌ nondeterminism ❌ I/O● Challenge 1: varying observation● Solution 1: “observation preorder” on traces● Challenge 2: branching effects● Solution 2: limited ∃● Contribution: a generative spectrum of (M,)-simulations● Result: ✅ exception ✅ nondeterminism ✅ I/O● (with a game-theoretic characterisation)𝒬● (with the up-to technique)34

Muroya (RIMS, Kyoto U.)