module plfa.part3.Adequacy where


## Introduction

Having proved a preservation property in the last chapter, a natural next step would be to prove progress. That is, to prove a property of the form

If Ξ³ β’ M β v, then either M is a lambda abstraction or M ββ N for some N.


Such a property would tell us that having a denotation implies either reduction to normal form or divergence. This is indeed true, but we can prove a much stronger property! In fact, having a denotation that is a function value (not β₯) implies reduction to a lambda abstraction.

This stronger property, reformulated a bit, is known as adequacy. That is, if a term M is denotationally equal to a lambda abstraction, then M reduces to a lambda abstraction.

β° M β β° (Ζ N)  implies M ββ  Ζ N' for some N'


Recall that β° M β β° (Ζ N) is equivalent to saying that Ξ³ β’ M β (v β¦ w) for some v and w. We will show that Ξ³ β’ M β (v β¦ w) implies multi-step reduction a lambda abstraction. The recursive structure of the derivations for Ξ³ β’ M β (v β¦ w) are completely different from the structure of multi-step reductions, so a direct proof would be challenging. However, The structure of Ξ³ β’ M β (v β¦ w) closer to that of BigStep call-by-name evaluation. Further, we already proved that big-step evaluation implies multi-step reduction to a lambda (cbnβreduce). So we shall prove that Ξ³ β’ M β (v β¦ w) implies that Ξ³' β’ M β c, where c is a closure (a term paired with an environment), Ξ³' is an environment that maps variables to closures, and Ξ³ and Ξ³' are appropriate related. The proof will be an induction on the derivation of Ξ³ β’ M β v, and to strengthen the induction hypothesis, we will relate semantic values to closures using a logical relation π.

The rest of this chapter is organized as follows.

• To make the π relation down-closed with respect to β, we must loosen the requirement that M result in a function value and instead require that M result in a value that is greater than or equal to a function value. We establish several properties about being greater than a functionββ.

• We define the logical relation π that relates values and closures, and extend it to a relation on terms πΌ and environments πΎ. We prove several lemmas that culminate in the property that if π v c and vβ² β v, then π vβ² c.

• We prove the main lemma, that if πΎ Ξ³ Ξ³' and Ξ³ β’ M β v, then πΌ v (clos M Ξ³').

• We prove adequacy as a corollary to the main lemma.

## Imports

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_β‘_; _β’_; refl; trans; sym; cong; congβ; cong-app)
open import Data.Product using (_Γ_; Ξ£; Ξ£-syntax; β; β-syntax; projβ; projβ)
open import Data.Sum
open import Relation.Nullary using (Β¬_)
open import Data.Empty using (β₯-elim) renaming (β₯ to Bot)
open import Data.Unit
open import Relation.Nullary using (Dec; yes; no)
open import Function using (_β_)
open import plfa.part2.Untyped
using (Context; _β’_; β; _β_; β; _,_; Z; S_; _; Ζ_; _Β·_;
rename; subst; ext; exts; _[_]; subst-zero;
_ββ _; _βββ¨_β©_; _β; _ββ_; ΞΎβ; ΞΎβ; Ξ²; ΞΆ)
open import plfa.part2.Substitution using (ids; sub-id)
open import plfa.part2.BigStep
using (Clos; clos; ClosEnv; β'; _,'_; _β’_β_; β-var; β-lam; β-app; β-determ;
cbnβreduce)
open import plfa.part3.Denotational
using (Value; Env; β; _,_; _β¦_; _β_; _β’_β_; β₯; all-funsβ; _β_; βββ;
var; β¦-elim; β¦-intro; β-intro; β₯-intro; sub; β°; _β_; _iff_;
β-trans; β-conj-R1; β-conj-R2; β-conj-L; β-refl; β-fun; β-bot; β-dist;
sub-inv-fun)
open import plfa.part3.Soundness using (soundness)



## The property of being greater or equal to a function

We define the following short-hand for saying that a value is greather-than or equal to a function value.

above-fun : Value β Set
above-fun u = Ξ£[ v β Value ] Ξ£[ w β Value ] v β¦ w β u


If a value u is greater than a function, then an even greater value u' is too.

above-fun-β : β{u u' : Value}
β above-fun u β u β u'
-------------------
β above-fun u'
above-fun-β β¨ v , β¨ w , lt' β© β© lt = β¨ v , β¨ w , β-trans lt' lt β© β©


The bottom value β₯ is not greater than a function.

above-funβ₯ : Β¬ above-fun β₯
with sub-inv-fun lt
with all-funsβ f
with Ξββ₯ m
... | ()


If the join of two values u and u' is greater than a function, then at least one of them is too.

above-fun-β : β{u u'}
β above-fun (u β u')
β above-fun u β above-fun u'
with sub-inv-fun vβ¦wβuβu'
with all-funsβ f
with Ξβuβu' m
... | injβ x = injβ β¨ A , β¨ B , (βββ x) β© β©
... | injβ x = injβ β¨ A , β¨ B , (βββ x) β© β©


On the other hand, if neither of u and u' is greater than a function, then their join is also not greater than a function.

not-above-fun-β : β{u u' : Value}
β Β¬ above-fun u β Β¬ above-fun u'
β Β¬ above-fun (u β u')
not-above-fun-β naf1 naf2 af12
with above-fun-β af12
... | injβ af1 = contradiction af1 naf1
... | injβ af2 = contradiction af2 naf2


The converse is also true. If the join of two values is not above a function, then neither of them is individually.

not-above-fun-β-inv : β{u u' : Value} β Β¬ above-fun (u β u')
β Β¬ above-fun u Γ Β¬ above-fun u'
not-above-fun-β-inv af = β¨ f af , g af β©
where
f : β{u u' : Value} β Β¬ above-fun (u β u') β Β¬ above-fun u
f{u}{u'} af12 β¨ v , β¨ w , lt β© β© =
g : β{u u' : Value} β Β¬ above-fun (u β u') β Β¬ above-fun u'
g{u}{u'} af12 β¨ v , β¨ w , lt β© β© =


The property of being greater than a function value is decidable, as exhibited by the following function.

above-fun? : (v : Value) β Dec (above-fun v)
above-fun? β₯ = no above-funβ₯
above-fun? (v β¦ w) = yes β¨ v , β¨ w , β-refl β© β©
above-fun? (u β u')
with above-fun? u | above-fun? u'
... | yes β¨ v , β¨ w , lt β© β© | _ = yes β¨ v , β¨ w , (β-conj-R1 lt) β© β©
... | no _ | yes β¨ v , β¨ w , lt β© β© = yes β¨ v , β¨ w , (β-conj-R2 lt) β© β©
... | no x | no y = no (not-above-fun-β x y)


## Relating values to closures

Next we relate semantic values to closures. The relation π is for closures whose term is a lambda abstraction, i.e., in weak-head normal form (WHNF). The relation πΌ is for any closure. Roughly speaking, πΌ v c will hold if, when v is greater than a function value, c evaluates to a closure c' in WHNF and π v c'. Regarding π v c, it will hold when c is in WHNF, and if v is a function, the body of c evaluates according to v.

π : Value β Clos β Set
πΌ : Value β Clos β Set


We define π as a function from values and closures to Set and not as a data type because it is mutually recursive with πΌ in a negative position (to the left of an implication). We first perform case analysis on the term in the closure. If the term is a variable or application, then π is false (Bot). If the term is a lambda abstraction, we define π by recursion on the value, which we describe below.

π v (clos ( xβ) Ξ³) = Bot
π v (clos (M Β· Mβ) Ξ³) = Bot
π β₯ (clos (Ζ M) Ξ³) = β€
π (v β¦ w) (clos (Ζ N) Ξ³) =
(β{c : Clos} β πΌ v c β above-fun w β Ξ£[ c' β Clos ]
(Ξ³ ,' c) β’ N β c'  Γ  π w c')
π (u β v) (clos (Ζ N) Ξ³) = π u (clos (Ζ N) Ξ³) Γ π v (clos (Ζ N) Ξ³)

• If the value is β₯, then the result is true (β€).

• If the value is a join (u β v), then the result is the pair (conjunction) of π is true for both u and v.

• The important case is for a function value v β¦ w and closure clos (Ζ N) Ξ³. Given any closure c such that πΌ v c, if w is greater than a function, then N evaluates (with Ξ³ extended with c) to some closure c' and we have π w c'.

The definition of πΌ is straightforward. If v is a greater than a function, then M evaluates to a closure related to v.

πΌ v (clos M Ξ³') = above-fun v β Ξ£[ c β Clos ] Ξ³' β’ M β c Γ π v c


The proof of the main lemma is by induction on Ξ³ β’ M β v, so it goes underneath lambda abstractions and must therefore reason about open terms (terms with variables). So we must relate environments of semantic values to environments of closures. In the following, πΎ relates Ξ³ to Ξ³' if the corresponding values and closures are related by πΌ.

πΎ : β{Ξ} β Env Ξ β ClosEnv Ξ β Set
πΎ {Ξ} Ξ³ Ξ³' = β{x : Ξ β β} β πΌ (Ξ³ x) (Ξ³' x)

πΎ-β : πΎ β β'
πΎ-β {()}

πΎ-ext : β{Ξ}{Ξ³ : Env Ξ}{Ξ³' : ClosEnv Ξ}{v c}
β πΎ Ξ³ Ξ³' β πΌ v c β πΎ (Ξ³ , v) (Ξ³' ,' c)
πΎ-ext {Ξ} {Ξ³} {Ξ³'} g e {Z} = e
πΎ-ext {Ξ} {Ξ³} {Ξ³'} g e {S x} = g


We need a few properties of the π and πΌ relations. The first is that a closure in the π relation must be in weak-head normal form. We define WHNF has follows.

data WHNF : β {Ξ A} β Ξ β’ A β Set where
Ζ_ : β {Ξ} {N : Ξ , β β’ β}
β WHNF (Ζ N)


The proof goes by cases on the term in the closure.

πβWHNF : β{Ξ}{Ξ³ : ClosEnv Ξ}{M : Ξ β’ β}{v}
β π v (clos M Ξ³) β WHNF M
πβWHNF {M =  x} {v} ()
πβWHNF {M = Ζ N} {v} vc = Ζ_
πβWHNF {M = L Β· M} {v} ()


Next we have an introduction rule for π that mimics the β-intro rule. If both u and v are related to a closure c, then their join is too.

πβ-intro : β{c u v}
β π u c β π v c
---------------
β π (u β v) c
πβ-intro {clos ( x) Ξ³} () vc
πβ-intro {clos (Ζ N) Ξ³} uc vc = β¨ uc , vc β©
πβ-intro {clos (L Β· M) Ξ³} () vc


In a moment we prove that π is preserved when going from a greater value to a lesser value: if π v c and v' β v, then π v' c. This property, named π-sub, is needed by the main lemma in the case for the sub rule.

To prove π-sub, we in turn need the following property concerning values that are not greater than a function, that is, values that are equivalent to β₯. In such cases, π v (clos (Ζ N) Ξ³') is trivially true.

not-above-fun-π : β{v : Value}{Ξ}{Ξ³' : ClosEnv Ξ}{N : Ξ , β β’ β }
β Β¬ above-fun v
-------------------
β π v (clos (Ζ N) Ξ³')
not-above-fun-π {β₯} af = tt
not-above-fun-π {v β¦ v'} af = β₯-elim (contradiction β¨ v , β¨ v' , β-refl β© β© af)
not-above-fun-π {vβ β vβ} af
with not-above-fun-β-inv af
... | β¨ af1 , af2 β© = β¨ not-above-fun-π af1 , not-above-fun-π af2 β©


The proofs of π-sub and πΌ-sub are intertwined.

sub-π : β{c : Clos}{v v'} β π v c β v' β v β π v' c
sub-πΌ : β{c : Clos}{v v'} β πΌ v c β v' β v β πΌ v' c


We prove π-sub by case analysis on the closureβs term, to dispatch the cases for variables and application. We then proceed by induction on v' β v. We describe each case below.

sub-π {clos ( x) Ξ³} {v} () lt
sub-π {clos (L Β· M) Ξ³} () lt
sub-π {clos (Ζ N) Ξ³} vc β-bot = tt
sub-π {clos (Ζ N) Ξ³} vc (β-conj-L lt1 lt2) = β¨ (sub-π vc lt1) , sub-π vc lt2 β©
sub-π {clos (Ζ N) Ξ³} β¨ vv1 , vv2 β© (β-conj-R1 lt) = sub-π vv1 lt
sub-π {clos (Ζ N) Ξ³} β¨ vv1 , vv2 β© (β-conj-R2 lt) = sub-π vv2 lt
sub-π {clos (Ζ N) Ξ³} vc (β-trans{v = vβ} lt1 lt2) = sub-π (sub-π vc lt2) lt1
sub-π {clos (Ζ N) Ξ³} vc (β-fun lt1 lt2) ev1 sf
with vc (sub-πΌ ev1 lt1) (above-fun-β sf lt2)
... | β¨ c , β¨ Nc , v4 β© β© = β¨ c , β¨ Nc , sub-π v4 lt2 β© β©
sub-π {clos (Ζ N) Ξ³} {v β¦ w β v β¦ w'} β¨ vcw , vcw' β© β-dist ev1c sf
with above-fun? w | above-fun? w'
... | yes af2 | yes af3
with vcw ev1c af2 | vcw' ev1c af3
... | β¨ clos L Ξ΄ , β¨ Lβcβ , πw β© β©
| β¨ cβ , β¨ Lβcβ , πw' β© β© rewrite β-determ Lβcβ Lβcβ with πβWHNF πw
... | Ζ_ =
sub-π {c} {v β¦ w β v β¦ w'} β¨ vcw , vcw' β©  β-dist ev1c sf
| yes af2 | no naf3
with vcw ev1c af2
... | β¨ clos {Ξ'} L Ξ³β , β¨ Lβc2 , πw β© β©
with πβWHNF πw
... | Ζ_ {N = N'} =
let πw' = not-above-fun-π{w'}{Ξ'}{Ξ³β}{N'} naf3 in
β¨ clos (Ζ N') Ξ³β , β¨ Lβc2 , πβ-intro πw πw' β© β©
sub-π {c} {v β¦ w β v β¦ w'} β¨ vcw , vcw' β© β-dist ev1c sf
| no naf2 | yes af3
with vcw' ev1c af3
... | β¨ clos {Ξ'} L Ξ³β , β¨ Lβc3 , πw'c β© β©
with πβWHNF πw'c
... | Ζ_ {N = N'} =
let πwc = not-above-fun-π{w}{Ξ'}{Ξ³β}{N'} naf2 in
β¨ clos (Ζ N') Ξ³β , β¨ Lβc3 , πβ-intro πwc πw'c β© β©
sub-π {c} {v β¦ w β v β¦ w'} β¨ vcw , vcw' β© β-dist ev1c β¨ v' , β¨ w'' , lt β© β©
| no naf2 | no naf3
... | injβ af2 = β₯-elim (contradiction af2 naf2)
... | injβ af3 = β₯-elim (contradiction af3 naf3)

• Case β-bot. We immediately have π β₯ (clos (Ζ N) Ξ³).

• Case β-conj-L.

  vβ' β v     vβ' β v
-------------------
(vβ' β vβ') β v


The induction hypotheses gives us π vβ' (clos (Ζ N) Ξ³) and π vβ' (clos (Ζ N) Ξ³), which is all we need for this case.

• Case β-conj-R1.

  v' β vβ
-------------
v' β (vβ β vβ)


The induction hypothesis gives us π v' (clos (Ζ N) Ξ³).

• Case β-conj-R2.

  v' β vβ
-------------
v' β (vβ β vβ)


Again, the induction hypothesis gives us π v' (clos (Ζ N) Ξ³).

• Case β-trans.

  v' β vβ   vβ β v
-----------------
v' β v


The induction hypothesis for vβ β v gives us π vβ (clos (Ζ N) Ξ³). We apply the induction hypothesis for v' β vβ to conclude that π v' (clos (Ζ N) Ξ³).

• Case β-dist. This case is the most difficult. We have

  π (v β¦ w) (clos (Ζ N) Ξ³)
π (v β¦ w') (clos (Ζ N) Ξ³)


and need to show that

  π (v β¦ (w β w')) (clos (Ζ N) Ξ³)


Let c be an arbtrary closure such that πΌ v c. Assume w β w' is greater than a function. Unfortunately, this does not mean that both w and w' are above functions. But thanks to the lemma above-fun-β, we know that at least one of them is greater than a function.

• Suppose both of them are greater than a function. Then we have Ξ³ β’ N β clos L Ξ΄ and π w (clos L Ξ΄). We also have Ξ³ β’ N β cβ and π w' cβ. Because the big-step semantics is deterministic, we have cβ β‘ clos L Ξ΄. Also, from π w (clos L Ξ΄) we know that L β‘ Ζ N' for some N'. We conclude that π (w β w') (clos (Ζ N') Ξ΄).

• Suppose one of them is greater than a function and the other is not: say above-fun w and Β¬ above-fun w'. Then from π (v β¦ w) (clos (Ζ N) Ξ³) we have Ξ³ β’ N β clos L Ξ³β and π w (clos L Ξ³β). From this we have L β‘ Ζ N' for some N'. Meanwhile, from Β¬ above-fun w' we have π w' (clos L Ξ³β). We conclude that π (w β w') (clos (Ζ N') Ξ³β).

The proof of sub-πΌ is direct and explained below.

sub-πΌ {clos M Ξ³} {v} {v'} πΌv v'βv fv'
with πΌv (above-fun-β fv' v'βv)
... | β¨ c , β¨ Mβc , πv β© β© =


From above-fun v' and v' β v we have above-fun v. Then with πΌ v c we obtain a closure c such that Ξ³ β’ M β c and π v c. We conclude with an application of sub-π with v' β v to show π v' c.

## Programs with function denotation terminate via call-by-name

The main lemma proves that if a term has a denotation that is above a function, then it terminates via call-by-name. More formally, if Ξ³ β’ M β v and πΎ Ξ³ Ξ³', then πΌ v (clos M Ξ³'). The proof is by induction on the derivation of Ξ³ β’ M β v we discuss each case below.

The following lemma, kth-x, is used in the case for the var rule.

kth-x : β{Ξ}{Ξ³' : ClosEnv Ξ}{x : Ξ β β}
β Ξ£[ Ξ β Context ] Ξ£[ Ξ΄ β ClosEnv Ξ ] Ξ£[ M β Ξ β’ β ]
Ξ³' x β‘ clos M Ξ΄
kth-x{Ξ³' = Ξ³'}{x = x} with Ξ³' x
... | clos{Ξ = Ξ} M Ξ΄ = β¨ Ξ , β¨ Ξ΄ , β¨ M , refl β© β© β©

ββπΌ : β{Ξ}{Ξ³ : Env Ξ}{Ξ³' : ClosEnv Ξ}{M : Ξ β’ β }{v}
β πΎ Ξ³ Ξ³' β Ξ³ β’ M β v β πΌ v (clos M Ξ³')
ββπΌ {Ξ} {Ξ³} {Ξ³'} πΎΞ³Ξ³' (var{x = x}) fΞ³x
with kth-x{Ξ}{Ξ³'}{x} | πΎΞ³Ξ³'{x = x}
... | β¨ Ξ , β¨ Ξ΄ , β¨ M' , eq β© β© β© | πΎΞ³Ξ³'x rewrite eq
with πΎΞ³Ξ³'x fΞ³x
... | β¨ c , β¨ M'βc , πΞ³x β© β© =
ββπΌ {Ξ} {Ξ³} {Ξ³'} πΎΞ³Ξ³' (β¦-elim{L = L}{M = M}{v = vβ}{w = v} dβ dβ) fv
with ββπΌ πΎΞ³Ξ³' dβ β¨ vβ , β¨ v , β-refl β© β©
... | β¨ clos L' Ξ΄ , β¨ LβL' , πvββ¦v β© β©
with πβWHNF πvββ¦v
... | Ζ_ {N = N}
with πvββ¦v {clos M Ξ³'} (ββπΌ πΎΞ³Ξ³' dβ) fv
... | β¨ c' , β¨ Nβc' , πv β© β© =
ββπΌ {Ξ} {Ξ³} {Ξ³'} πΎΞ³Ξ³' (β¦-intro{N = N}{v = v}{w = w} d) fvβ¦w =
β¨ clos (Ζ N) Ξ³' , β¨ β-lam , E β© β©
where E : {c : Clos} β πΌ v c β above-fun w
β Ξ£[ c' β Clos ] (Ξ³' ,' c) β’ N β c'  Γ  π w c'
E {c} πΌvc fw = ββπΌ (Ξ» {x} β πΎ-ext{Ξ}{Ξ³}{Ξ³'} πΎΞ³Ξ³' πΌvc {x}) d fw
ββπΌ πΎΞ³Ξ³' β₯-intro fβ₯ = β₯-elim (above-funβ₯ fβ₯)
ββπΌ πΎΞ³Ξ³' (β-intro{v = vβ}{w = vβ} dβ dβ) fv12
with above-fun? vβ | above-fun? vβ
... | yes fv1 | yes fv2
with ββπΌ πΎΞ³Ξ³' dβ fv1 | ββπΌ πΎΞ³Ξ³' dβ fv2
rewrite β-determ Mβcβ Mβcβ =
ββπΌ πΎΞ³Ξ³' (β-intro{v = vβ}{w = vβ} dβ dβ) fv12 | yes fv1 | no nfv2
with ββπΌ πΎΞ³Ξ³' dβ fv1
... | β¨ clos {Ξ'} M' Ξ³β , β¨ Mβcβ , πvβ β© β©
with πβWHNF πvβ
... | Ζ_ {N = N} =
let πvβ = not-above-fun-π{vβ}{Ξ'}{Ξ³β}{N} nfv2 in
β¨ clos (Ζ N) Ξ³β , β¨ Mβcβ , πβ-intro πvβ πvβ β© β©
ββπΌ πΎΞ³Ξ³' (β-intro{v = vβ}{w = vβ} dβ dβ) fv12 | no nfv1  | yes fv2
with ββπΌ πΎΞ³Ξ³' dβ fv2
... | β¨ clos {Ξ'} M' Ξ³β , β¨ M'βcβ , π2c β© β©
with πβWHNF π2c
... | Ζ_ {N = N} =
let π1c = not-above-fun-π{vβ}{Ξ'}{Ξ³β}{N} nfv1 in
β¨ clos (Ζ N) Ξ³β , β¨ M'βcβ , πβ-intro π1c π2c β© β©
ββπΌ πΎΞ³Ξ³' (β-intro dβ dβ) fv12 | no nfv1  | no nfv2
with above-fun-β fv12
... | injβ fv1 = β₯-elim (contradiction fv1 nfv1)
... | injβ fv2 = β₯-elim (contradiction fv2 nfv2)
ββπΌ {Ξ} {Ξ³} {Ξ³'} {M} {v'} πΎΞ³Ξ³' (sub{v = v} d v'βv) fv'
with ββπΌ {Ξ} {Ξ³} {Ξ³'} {M} πΎΞ³Ξ³' d (above-fun-β fv' v'βv)
... | β¨ c , β¨ Mβc , πv β© β© =

• Case var. Looking up x in Ξ³' yields some closure, clos M' Ξ΄, and from πΎ Ξ³ Ξ³' we have πΌ (Ξ³ x) (clos M' Ξ΄). With the premise above-fun (Ξ³ x), we obtain a closure c such that Ξ΄ β’ M' β c and π (Ξ³ x) c. To conclude Ξ³' β’ x β c via β-var, we need Ξ³' x β‘ clos M' Ξ΄, which is obvious, but it requires some Agda shananigans via the kth-x lemma to get our hands on it.

• Case β¦-elim. We have Ξ³ β’ L Β· M β v. The induction hypothesis for Ξ³ β’ L β vβ β¦ v gives us Ξ³' β’ L β clos L' Ξ΄ and π v (clos L' Ξ΄). Of course, L' β‘ Ζ N for some N. By the induction hypothesis for Ξ³ β’ M β vβ, we have πΌ vβ (clos M Ξ³'). Together with the premise above-fun v and π v (clos L' Ξ΄), we obtain a closure c' such that Ξ΄ β’ N β c' and π v c'. We conclude that Ξ³' β’ L Β· M β c' by rule β-app.

• Case β¦-intro. We have Ξ³ β’ Ζ N β v β¦ w. We immediately have Ξ³' β’ Ζ M β clos (Ζ M) Ξ³' by rule β-lam. But we also need to prove π (v β¦ w) (clos (Ζ N) Ξ³'). Let c by an arbitrary closure such that πΌ v c. Suppose v' is greater than a function value. We need to show that Ξ³' , c β’ N β c' and π v' c' for some c'. We prove this by the induction hypothesis for Ξ³ , v β’ N β v' but we must first show that πΎ (Ξ³ , v) (Ξ³' , c). We prove that by the lemma πΎ-ext, using facts πΎ Ξ³ Ξ³' and πΌ v c.

• Case β₯-intro. We have the premise above-fun β₯, but thatβs impossible.

• Case β-intro. We have Ξ³ β’ M β (vβ β vβ) and above-fun (vβ β vβ) and need to show Ξ³' β’ M β c and π (vβ β vβ) c for some c. Again, by above-fun-β, at least one of vβ or vβ is greater than a function.

• Suppose both vβ and vβ are greater than a function value. By the induction hypotheses for Ξ³ β’ M β vβ and Ξ³ β’ M β vβ we have Ξ³' β’ M β cβ, π vβ cβ, Ξ³' β’ M β cβ, and π vβ cβ for some cβ and cβ. Because β is deterministic, we have cβ β‘ cβ. Then by πβ-intro we conclude that π (vβ β vβ) cβ.

• Without loss of generality, suppose vβ is greater than a function value but vβ is not. By the induction hypotheses for Ξ³ β’ M β vβ, and using πβWHNF, we have Ξ³' β’ M β clos (Ζ N) Ξ³β and π vβ (clos (Ζ N) Ξ³β). Then because vβ is not greater than a function, we also have π vβ (clos (Ζ N) Ξ³β). We conclude that π (vβ β vβ) (clos (Ζ N) Ξ³β).

• Case sub. We have Ξ³ β’ M β v, v' β v, and above-fun v'. We need to show that Ξ³' β’ M β c and π v' c for some c. We have above-fun v by above-fun-β, so the induction hypothesis for Ξ³ β’ M β v gives us a closure c such that Ξ³' β’ M β c and π v c. We conclude that π v' c by sub-π.

From the main lemma we can directly show that β° M β β° (Ζ N) implies that M big-steps to a lambda, i.e., β β’ M β clos (Ζ Nβ²) Ξ³.

βββ : β{M : β β’ β}{N : β , β β’ β}  β  β° M β β° (Ζ N)
β  Ξ£[ Ξ β Context ] Ξ£[ Nβ² β (Ξ , β β’ β) ] Ξ£[ Ξ³ β ClosEnv Ξ ]
β' β’ M β clos (Ζ Nβ²) Ξ³
βββ{M}{N} eq
with ββπΌ πΎ-β ((projβ (eq β (β₯ β¦ β₯))) (β¦-intro β₯-intro))
... | β¨ clos {Ξ} Mβ² Ξ³ , β¨ Mβc , Vc β© β©
with πβWHNF Vc
... | Ζ_ {N = Nβ²} =


The proof goes as follows. We derive β β’ Ζ N β β₯ β¦ β₯ and then β° M β β° (Ζ N) gives us β β’ M β β₯ β¦ β₯. We conclude by applying the main lemma to obtain β β’ M β clos (Ζ Nβ²) Ξ³ for some Nβ² and Ξ³.

Now to prove the adequacy property. We apply the above lemma to obtain β β’ M β clos (Ζ Nβ²) Ξ³ and then apply cbnβreduce to conclude.

adequacy : β{M : β β’ β}{N : β , β β’ β}
β  β° M β β° (Ζ N)
β Ξ£[ Nβ² β (β , β β’ β) ]
(M ββ  Ζ Nβ²)
with βββ eq
cbnβreduce Mβ


## Call-by-name is equivalent to beta reduction

As promised, we return to the question of whether call-by-name evaluation is equivalent to beta reduction. In chapter BigStep we established the forward direction: that if call-by-name produces a result, then the program beta reduces to a lambda abstraction (cbnβreduce). We now prove the backward direction of the if-and-only-if, leveraging our results about the denotational semantics.

reduceβcbn : β {M : β β’ β} {N : β , β β’ β}
β M ββ  Ζ N
β Ξ£[ Ξ β Context ] Ξ£[ Nβ² β Ξ , β β’ β ] Ξ£[ Ξ΄ β ClosEnv Ξ ]
β' β’ M β clos (Ζ Nβ²) Ξ΄
reduceβcbn Mββ ΖN = βββ (soundness Mββ ΖN)


Suppose M ββ  Ζ N. Soundness of the denotational semantics gives us β° M β β° (Ζ N). Then by βββ we conclude that β' β’ M β clos (Ζ Nβ²) Ξ΄ for some Nβ² and Ξ΄.

Putting the two directions of the if-and-only-if together, we establish that call-by-name evaluation is equivalent to beta reduction in the following sense.

cbnβreduce : β {M : β β’ β}
β (Ξ£[ N β β , β β’ β ] (M ββ  Ζ N))
iff
(Ξ£[ Ξ β Context ] Ξ£[ Nβ² β Ξ , β β’ β ] Ξ£[ Ξ΄ β ClosEnv Ξ ]
β' β’ M β clos (Ζ Nβ²) Ξ΄)
cbnβreduce {M} = β¨ (Ξ» x β reduceβcbn (projβ x)) ,
(Ξ» x β cbnβreduce (projβ (projβ (projβ x)))) β©


## Unicode

This chapter uses the following unicode:

πΌ  U+1D53C  MATHEMATICAL DOUBLE-STRUCK CAPITAL E (\bE)
πΎ  U+1D53E  MATHEMATICAL DOUBLE-STRUCK CAPITAL G (\bG)
π  U+1D53E  MATHEMATICAL DOUBLE-STRUCK CAPITAL V (\bV)