Formal Verifications ofCall-by-Need and Call-by-Name
Evaluations with Mutual Recursion
Masayuki Mizuno
Joint work with Eijiro Sumii
Tohoku University
November 19, 2019

Our goals
Long-term: formally verified compiler for
non-strict language (e.g. Haskell)2 / 36

Our goals
Long-term: formally verified compiler for
non-strict language (e.g. Haskell)
Short-term: formal verification ofcorrespondence between• Call-by-name [Plotkin 1975 etc.]:
High-level specification of
non-strict languages• Call-by-need [Wadsworth 1971 etc.]:
Implementation of non-strict languages
2 / 36

Background 1: non-strict language
Allows users to define non-strict functions e.g.
const42 x = if true then 42 else x
const42 (loop ())↠ 42
where loop () = 3 + loop ()3 / 36

Background 2: call-by-nameSubstitute arguments without evaluating themconst42 x = if true then 42 else x
const42 (loop ())

where loop () = 3 + loop ()4 / 36

Background 2: call-by-nameSubstitute arguments without evaluating themconst42 x = if true then 42 else x
const42 (loop ())−−−−→ if true then 42 else loop ()namewhere loop () = 3 + loop ()4 / 36

Background 2: call-by-nameSubstitute arguments without evaluating themconst42 x = if true then 42 else x
const42 (loop ())−−−−→ if true then 42 else loop ()name−−−−→ 42
namewhere loop () = 3 + loop ()4 / 36

Problem of call-by-name:redundant computations
double x = x + x
double (3 + 3)

5 / 36

Problem of call-by-name:redundant computations
double x = x + x
double (3 + 3)
name−−−−→ (3 + 3) + (3 + 3)

5 / 36

Problem of call-by-name:redundant computations
double x = x + x
double (3 + 3)
name−−−−→ (3 + 3) + (3 + 3)
name−−−−→ 6 + (3 + 3)

5 / 36

Problem of call-by-name:redundant computations
double x = x + x
double (3 + 3)
name−−−−→ (3 + 3) + (3 + 3)
name−−−−→ 6 + (3 + 3)
name−−−−→ 6 + 6
5 / 36

Problem of call-by-name:redundant computations
double x = x + x
double (3 + 3)
name−−−−→ (3 + 3) + (3 + 3)
name−−−−→ 6 + (3 + 3)
name−−−−→ 6 + 6
name−−−−→ 125 / 36

Background 3: call-by-needShares values of arguments
double x = x + x
double (3 + 3)

6 / 36

Background 3: call-by-needShares values of arguments
double x = x + x
double (3 + 3)
need−−−→ x + x wherex =3+36 / 36

Background 3: call-by-needShares values of arguments
double x = x + x
double (3 + 3)−−−→ x + x whereneed

x =3+3need

x=6−−−→ x + x where

6 / 36

Background 3: call-by-needShares values of arguments
double x = x + x
double (3 + 3)−−−→ x + x whereneed

x =3+3need

x=6−−−→ x + x whereneed−−−→ 126 / 36

Background 3: call-by-needShares values of arguments
double x = x + x
double (3 + 3)−−−→ x + x whereneed

x =3+3need

x=6−−−→ x + x whereneed−−−→ 12
Should correspond with call-by-name
6 / 36

Challenge: recursion (1/2)
Implicit recursion destroys sharing
Y f = (λ x. f (x x)) (λ x. f (x x))
let x = e x in x ⇒ Y (λ x. e x )• Computation of e x inside λ x isrepeated

7 / 36

Challenge: recursion (2/2)
Explicit recursion requires sophisticatedmechanism• Dependency in small-step semantics[Ariola+ 97]::= · · ·| let D, x = E in E ′[x]| let x n = E, D[x, x n ] in E ′[x]D[x, x n ] ::= x = E[x 1 ], · · · , x n−1 = E[x n ], D

E•

Fixed point in denotational semantics[Launchbury 93]µρ′. ρ ⊔ (x 1 7→ [[e1 ]] ρ′ · · · x n 7→ [[en ]] ρ′ )8 / 36

Our results
Simple formal verification (in Coq) ofcorrespondence among call-by-need and
3 diﬀerent styles of call-by-name evaluationsof language with explicit mutual recursion

9 / 36

Our results
Simple formal verification (in Coq) ofcorrespondence among call-by-need and
3 diﬀerent styles of call-by-name evaluationsof language with explicit mutual recursion• Call-by-need natural semantics

9 / 36

Our results
Simple formal verification (in Coq) ofcorrespondence among call-by-need and
3 diﬀerent styles of call-by-name evaluationsof language with explicit mutual recursion• Call-by-need natural semantics▶

heap-based [Launchbury 93]

9 / 36

Our results
Simple formal verification (in Coq) ofcorrespondence among call-by-need and
3 diﬀerent styles of call-by-name evaluationsof language with explicit mutual recursion• Call-by-need natural semantics▶

•

heap-based [Launchbury 93]

Call-by-name natural semantics

9 / 36

Our results
Simple formal verification (in Coq) ofcorrespondence among call-by-need and
3 diﬀerent styles of call-by-name evaluationsof language with explicit mutual recursion• Call-by-need natural semantics▶

•

heap-based [Launchbury 93]

Call-by-name natural semantics▶

heap-based [Launchbury 93]

9 / 36

Our results
Simple formal verification (in Coq) ofcorrespondence among call-by-need and
3 diﬀerent styles of call-by-name evaluationsof language with explicit mutual recursion• Call-by-need natural semantics▶

•

heap-based [Launchbury 93]

Call-by-name natural semantics
heap-based [Launchbury 93]▶ closure-based (cf. [Launchbury 93])▶

9 / 36

Our results
Simple formal verification (in Coq) ofcorrespondence among call-by-need and
3 diﬀerent styles of call-by-name evaluationsof language with explicit mutual recursion• Call-by-need natural semantics▶

•

heap-based [Launchbury 93]

Call-by-name natural semantics
heap-based [Launchbury 93]▶ closure-based (cf. [Launchbury 93])
▶ substitution-based [Church 36]▶

9 / 36

Our results
Simple formal verification (in Coq) ofcorrespondence among call-by-need and
3 diﬀerent styles of call-by-name evaluationsof language with explicit mutual recursion• Call-by-need natural semantics▶

•

heap-based [Launchbury 93]

Call-by-name natural semantics
heap-based [Launchbury 93]▶ closure-based (cf. [Launchbury 93])
▶ substitution-based [Church 36]▶

♦ Cf. correspondence with call-by-namedenotational semantics [Breitner 18]

9 / 36

Proof outline
Consists of 3 correspondences

10 / 36

Outline

1 Proof of the correspondences
2 Formalization in Coq
3 Conclusion

11 / 36

Outline

1 Proof of the correspondences
2 Formalization in Coq
3 Conclusion

12 / 36

Our target language
λ-calculus with mutually recursive bindings
Using de Bruijn indicesx, l ∈ Nat
H, e ∈ Termsv∈ Value ::= abs ee∈ Term ::= var x | loc l | abs e| app e1 e2 | let e in e•

13 / 36

Correspondence between heap-basedcall-by-need and call-by-name evaluations
Closure-basedcall-by-name6
Heap-based ocall-by-need/ Heap-basedcall-by-namehv(

Substitution-basedcall-by-name
14 / 36

Call-by-need semantics [Launchbury 93]⟨H1 ⟩e ⇓d ⟨H2 ⟩v⟨H1 ⟩e1 ⇓d ⟨H2 ⟩abs e0⟨H2, e2 ⟩e0 [0 7→ loc |H2 |] ⇓d ⟨H3 ⟩v⟨H1 ⟩app e1 e2 ⇓d ⟨H3 ⟩v⟨H1 ⟩H1 .l ⇓d ⟨H2 ⟩v⟨H1 ⟩loc l ⇓d ⟨H2 [l 7→ v]⟩v

15 / 36

Call-by-name semantics [Launchbury 93]⟨H1 ⟩e ⇓m ⟨H2 ⟩v⟨H1 ⟩e1 ⇓m ⟨H2 ⟩abs e0⟨H2, e2 ⟩e0 [0 7→ loc |H2 |] ⇓m ⟨H3 ⟩v⟨H1 ⟩app e1 e2 ⇓m ⟨H3 ⟩v⟨H1 ⟩H1 .l ⇓m ⟨H2 ⟩v⟨H1 ⟩loc l ⇓m ⟨H2 ⟩v

16 / 36

One of our main theorem
Theorem (soundness of ⇓d )If ⟨H1 ⟩e1 ⇓d ⟨H1′ ⟩v1 with H1 ≤ R H2 and e1 ∼ R e2 ,then ⟨H2 ⟩e2 ⇓m ⟨H2′ ⟩v2 with H1′ ≤ R′ H2′ and v1 ∼ R′ v2
for some R′ ⊇ R, H2′ , and v2
If call-by-need evaluation converges,
call-by-name evaluation of corresponding heap and term
also converges and gives a corresponding value

17 / 36

Intuition of correspondencee = (let x = (let y = 1 + 2, z = z in y) in x + x)

18 / 36

Intuition of correspondencee = (let x = (let y = 1 + 2, z = z in y) in x + x)⟨⟩e ⇓d ⟨l 1 7→ 3, l 2 7→ 3, l 3 7→ l 3 ⟩6

18 / 36

Intuition of correspondencee = (let x = (let y = 1 + 2, z = z in y) in x + x)⟨⟩e ⇓d ⟨l 1 7→ 3, l 2 7→ 3, l 3 7→ l 3 ⟩6⟨⟩e ⇓m ⟨l 1 7→ (let y = 1 + 2, z = z in y),l 2 7→ 1 + 2, l 3 7→ l 3, l 2′ 7→ 1 + 2, l 3′ 7→ l 3′ ⟩618 / 36

Intuition of correspondencee = (let x = (let y = 1 + 2, z = z in y) in x + x)⟨⟩e ⇓d ⟨l 1 7→ 3, l 2 7→ 3, l 3 7→ l 3 ⟩6⟨⟩e ⇓m ⟨l 1 7→ (let y = 1 + 2, z = z in y),l 2 7→ 1 + 2, l 3 7→ l 3, l 2′ 7→ 1 + 2, l 3′ 7→ l 3′ ⟩6One-to-many correspondnece between
call-by-need and call-by-name locations

18 / 36

Intuition of correspondencee = (let x = (let y = 1 + 2, z = z in y) in x + x)⟨⟩e ⇓d ⟨l 1 7→ 3, l 2 7→ 3, l 3 7→ l 3 ⟩6⟨⟩e ⇓m ⟨l 1 7→ (let y = 1 + 2, z = z in y),l 2 7→ 1 + 2, l 3 7→ l 3, l 2′ 7→ 1 + 2, l 3′ 7→ l 3′ ⟩6One-to-many correspondnece between
call-by-need and call-by-name locations
Contents of the corresponding locations• are the same
(modulo corresponing locations), or

18 / 36

Intuition of correspondencee = (let x = (let y = 1 + 2, z = z in y) in x + x)⟨⟩e ⇓d ⟨l 1 7→ 3, l 2 7→ 3, l 3 7→ l 3 ⟩6⟨⟩e ⇓m ⟨l 1 7→ (let y = 1 + 2, z = z in y),l 2 7→ 1 + 2, l 3 7→ l 3, l 2′ 7→ 1 + 2, l 3′ 7→ l 3′ ⟩6One-to-many correspondnece between
call-by-need and call-by-name locations
Contents of the corresponding locations• are the same
(modulo corresponing locations), or• give the same value
by call-by-name re-evaluation

18 / 36

Definition (lazy correspondence of heaps)
H1 ≤ R H2 iﬀ
for all (l 1, l 2 ) ∈ R,
either H1 .l 1 ∼ R H2 .l 2
or ∃S, H2′ , v2 . ⟨H2 ⟩H2 .l 2 ⇓m ⟨H2′ ⟩v2 ∧(H1 .l 1 ∼(R◦S)∪R v2 ) ∧ (H2 ∼S H2′ )19 / 36

Definition (lazy correspondence of heaps)
H1 ≤ R H2 iﬀ
for all (l 1, l 2 ) ∈ R,
either H1 .l 1 ∼ R H2 .l 2
or ∃S, H2′ , v2 . ⟨H2 ⟩H2 .l 2 ⇓m ⟨H2′ ⟩v2 ∧(H1 .l 1 ∼(R◦S)∪R v2 ) ∧ (H2 ∼S H2′ )S is increased part of the correspondence

19 / 36

Definition (lazy correspondence of heaps)
H1 ≤ R H2 iﬀ
for all (l 1, l 2 ) ∈ R,
either H1 .l 1 ∼ R H2 .l 2
or ∃S, H2′ , v2 . ⟨H2 ⟩H2 .l 2 ⇓m ⟨H2′ ⟩v2 ∧(H1 .l 1 ∼(R◦S)∪R v2 ) ∧ (H2 ∼S H2′ )S is increased part of the correspondence
Heaps increased by re-evaluation arehomomorphic to original heaps• no coinduction required
19 / 36Proof of our main theorem
Theorem (soundness of ⇓d )If ⟨H1 ⟩e1 ⇓d ⟨H1′ ⟩v1 with H1 ≤ R H2 and e1 ∼ R e2 ,then ⟨H2 ⟩e2 ⇓m ⟨H2′ ⟩v2 with H1′ ≤ R′ H2′ and v1 ∼ R′ v2
for some R′ ⊇ R, H2′ , and v2
Proof outline.
By induction on the derivation of ⟨H1 ⟩e1 ⇓d ⟨H1′ ⟩v1
The essential case is evaluation of locations:⟨H1 ⟩H1 .l⇓d ⟨H1′′⟩v⟨H1 ⟩loc l⇓d ⟨H1′′[l7→v ]⟩v
20 / 36Proof outline.
⟨H1 ⟩H1 .l⇓d ⟨H1′′⟩v⟨H1 ⟩loc l⇓d ⟨H1′′[l7→v ]⟩v

From H1 ≤ R H2 , we have two subcases:

21 / 36Proof outline.
⟨H1 ⟩H1 .l⇓d ⟨H1′′⟩v⟨H1 ⟩loc l⇓d ⟨H1′′[l7→v ]⟩v

From H1 ≤ R H2 , we have two subcases:
Subcase (thunk update): H1 .l 1 ∼ R H2 .l 2
To show H1′′[l 1 7→ v1 ] ≤ R′ H2′ ,we use the induction hypothesis and apply
location renaming

21 / 36Proof outline.
⟨H1 ⟩H1 .l⇓d ⟨H1′′⟩v⟨H1 ⟩loc l⇓d ⟨H1′′[l7→v ]⟩v

From H1 ≤ R H2 , we have two subcases:
Subcase (thunk update): H1 .l 1 ∼ R H2 .l 2
To show H1′′[l 1 7→ v1 ] ≤ R′ H2′ ,we use the induction hypothesis and apply
location renaming
Subcase (re-evaluation): ⟨H2 ⟩H2 .l 2 ⇓m ⟨H2′ ⟩v2 ,H2 ∼S H2′ , H1 .l 1 ∼ R◦S v2
Straightforward (thanks to the definition of H1 ≤ R H2 )□21 / 36

Our main theorems
Call-by-need evaluation converges⇒ call-by-name evaluation converges
Call-by-name evaluation converges⇒ call-by-need evaluation converges
Call-by-need evaluation diverges⇒ call-by-name evaluation diverges
Call-by-name evaluation diverges⇒ call-by-need evaluation diverges• Cf. coinductive definition of divergence[Leroy 06]
22 / 36

Correspondence between
heap-based and substitution-basedcall-by-name evaluations
Closure-basedcall-by-name6
Heap-based ocall-by-need/

Heap-basedcall-by-namehv(

Substitution-basedcall-by-name23 / 36

Heap-based call-by-name semantics[Launchbury 93]⟨H1 ⟩e ⇓m ⟨H2 ⟩v⟨H1 ⟩e1 ⇓m ⟨H2 ⟩abs e0⟨H2, e2 ⟩e0 [0 7→ loc |H2 |] ⇓m ⟨H3 ⟩v⟨H1 ⟩app e1 e2 ⇓m ⟨H3 ⟩v⟨H1, e[∀x 7→ loc (|H1 | + x)]⟩e[∀x 7→ loc (|H1 | + x)]⇓m ⟨H2 ⟩v⟨H1 ⟩let e in e ⇓m ⟨H2 ⟩v
24 / 36

Substitution-based call-by-name semanticse ⇓m ve1 ⇓m abs e0
e0 [0 7→ e2 ] ⇓m v
app e1 e2 ⇓m v
e[∀x 7→ let e in e.x] ⇓m v
let e in e ⇓m v

25 / 36

Correspondence between
heaps-terms and substituted-termse = (let x = λw. x in (λ y. λz. x y) true)

26 / 36

Correspondence between
heaps-terms and substituted-termse = (let x = λw. x in (λ y. λz. x y) true)⟨⟩e ⇓m ⟨l 1 7→ λw. l 1, l 2 7→ true⟩λz. l 1 l 2

26 / 36

Correspondence between
heaps-terms and substituted-termse = (let x = λw. x in (λ y. λz. x y) true)⟨⟩e ⇓m ⟨l 1 7→ λw. l 1, l 2 7→ true⟩λz. l 1 l 2e ⇓m λz. (let x = λw. x in λw. x) true

26 / 36

Correspondence between
heaps-terms and substituted-termse = (let x = λw. x in (λ y. λz. x y) true)⟨⟩e ⇓m ⟨l 1 7→ λw. l 1, l 2 7→ true⟩λz. l 1 l 2e ⇓m λz. (let x = λw. x in λw. x) true

Correspondence R between locations andsubstituted terms• R = {(l 1, let x = λw. x in λw. x), (l 2, true)}

26 / 36

Correspondence between
heaps-terms and substituted-termse = (let x = λw. x in (λ y. λz. x y) true)⟨⟩e ⇓m ⟨l 1 7→ λw. l 1, l 2 7→ true⟩λz. l 1 l 2e ⇓m λz. (let x = λw. x in λw. x) true

Correspondence R between locations andsubstituted terms• R = {(l 1, let x = λw. x in λw. x), (l 2, true)}⟨H⟩e1 ∼ R e2(l, e2 ) ∈ R⟨H⟩loc l ∼ R e2
26 / 36Proof of our main theorem
Theorem (substitution-based ⇒ heap-based
convergence)If e2 ⇓m v2 with let R (H) and ⟨H⟩e1 ∼ R e2 ,then ⟨H⟩e1 ⇓m ⟨H ′⟩v1 with let R′ (H ′ ) and ⟨H ′⟩v1 ∼ R′ v2
for some R′ ⊇ R, H ′, and v2 .
Proof outline.
By induction on derivations of e2 ⇓m v2

27 / 36

Problem: substitution for locations
becomes 0-step
There is no rule in substitution-based
semantics that corresponds to:⟨H⟩H.l ⇓m ⟨H ′⟩v⟨H⟩loc l ⇓m ⟨H ′⟩v

28 / 36

Problem: substitution for locations
becomes 0-step
There is no rule in substitution-based
semantics that corresponds to:⟨H⟩H.l ⇓m ⟨H ′⟩v⟨H⟩loc l ⇓m ⟨H ′⟩v
Induction doesn’t work in some theorems:• substitution-based ⇒ heap-based
convergence• heap-based ⇒ substitution-based
divergence
28 / 36

Our trick:distinguish bindings for let and app
Bindings introduced by let always involve
let-expansions
e[∀x 7→ let e in e.x] ⇓m v
let e in e ⇓m v

29 / 36

Our trick:distinguish bindings for let and app
Bindings introduced by let always involve
let-expansions
e[∀x 7→ let e in e.x] ⇓m v
let e in e ⇓m v

Bindings introduced by function applications
are non-recursive and “finite”⇒ We therefore distinguish:

29 / 36

Our trick:distinguish bindings for let and app
Bindings introduced by let always involve
let-expansions
e[∀x 7→ let e in e.x] ⇓m v
let e in e ⇓m v

Bindings introduced by function applications
are non-recursive and “finite”⇒ We therefore distinguish:
For let:(l, e2 ) ∈ R⟨H⟩loc l ∼ R e2
29 / 36

Our trick:distinguish bindings for let and app
Bindings introduced by let always involve
let-expansions
e[∀x 7→ let e in e.x] ⇓m v
let e in e ⇓m v

Bindings introduced by function applications
are non-recursive and “finite”⇒ We therefore distinguish:
For let:(l, e2 ) ∈ R⟨H⟩loc l ∼ R e2

For app:⟨H⟩H.l ∼ R e2
⟨H⟩loc l ∼ R e2
29 / 36Proof of our main theorem
Theorem (substitution-based ⇒ heap-based
convergence)If e2 ⇓m v2 with let R (H) and ⟨H⟩e1 ∼ R e2 ,then ⟨H⟩e1 ⇓m ⟨H ′⟩v1 with let R′ (H ′ ) and ⟨H ′⟩v1 ∼ R′ v2
for some R′ ⊇ R, H ′, and v2 .
Proof outline.
By induction on derivations of e2 ⇓m v2 and⟨H⟩e1 ∼ R e2□
30 / 36

Outline

1 Proof of the correspondences
2 Formalization in Coq
3 Conclusion

31 / 36

Problem: heap-based ⇒substitution-based divergence
TheoremIf ⟨H⟩e1 ⇑m with let R (H) and ⟨H⟩e1 ∼ R e2 , then e2 ⇑m
Coq’s syntactic guard criterion rejects:
cofix heap_s ub st _d iv er ge H e1
( Hdiv : Heaps . diverge H e ) :=( fix h e a p _ s u b s t _ d i v e r g e _ i n n e r H( Hcorr : corr_term R H e1 e2 )match Hdiv in ... with ...
Subst . diverge _name_appL e21( hea p_ su bs t_ di ver ge H e11... end ) H e1

e1 R e2:=e22
R e21 ...)

32 / 36

Solution: detour using
small-step semantics⟨H⟩e1 ⇑me 2 ⇑mo/†∀H ′, e′1 . ⟨H⟩e1 →∗m ⟨H ′⟩e′1=⇒ ⟨H ′⟩e′1 →m∀e′2 . e2 →∗m e′2 =⇒ e′2 →m† uses law of excluded middle
33 / 36

Outline

1 Proof of the correspondences
2 Formalization in Coq
3 Conclusion

34 / 36

Conclusion
Simpler formal verification in Coq ofcorrespondence among call-by-need and
3 diﬀerent styles of call-by-name evaluationsof language with explicit mutual recursion• Call-by-need natural semantics▶

•

heap-based [Launchbury 93]

Call-by-name natural semantics
heap-based [Launchbury 93]▶ closure-based (cf. [Launchbury 93])
▶ substitution-based [Church 36]▶

♦ Also extended with black hole [Nakata+ 09]
35 / 36

Future work

Cost analysis of call-by-need evaluations
Verification of compilers fornon-strict languages• Part of GHC [The Glasgow Haskell Team 92]?

36 / 36