# Adequacy: Adequacy of denotational semantics with respect to operational semantics

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₂) renaming (_,_ to ⟨_,_⟩) open import Data.Sum open import Relation.Nullary using (¬_) open import Relation.Nullary.Negation using (contradiction) 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 greater-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 ⊥ above-fun⊥ ⟨ v , ⟨ w , lt ⟩ ⟩ with sub-inv-fun lt ... | ⟨ Γ , ⟨ f , ⟨ Γ⊆⊥ , ⟨ lt1 , lt2 ⟩ ⟩ ⟩ ⟩ with all-funs∈ f ... | ⟨ A , ⟨ B , m ⟩ ⟩ 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' above-fun-⊔{u}{u'} ⟨ v , ⟨ w , v↦w⊑u⊔u' ⟩ ⟩ with sub-inv-fun v↦w⊑u⊔u' ... | ⟨ Γ , ⟨ f , ⟨ Γ⊆u⊔u' , ⟨ lt1 , lt2 ⟩ ⟩ ⟩ ⟩ with all-funs∈ f ... | ⟨ A , ⟨ B , m ⟩ ⟩ 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 ⟩ ⟩ = contradiction ⟨ v , ⟨ w , ⊑-conj-R1 lt ⟩ ⟩ af12 g : ∀{u u' : Value} → ¬ above-fun (u ⊔ u') → ¬ above-fun u' g{u}{u'} af12 ⟨ v , ⟨ w , lt ⟩ ⟩ = contradiction ⟨ v , ⟨ w , ⊑-conj-R2 lt ⟩ ⟩ af12

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 = 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 ... | ƛ_ = ⟨ clos L δ , ⟨ L⇓c₂ , ⟨ 𝕍w , 𝕍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 with above-fun-⊔ ⟨ v' , ⟨ w'' , lt ⟩ ⟩ ... | inj₁ af2 = contradiction af2 naf2 ... | inj₂ af3 = 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 arbitrary 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 ⟩ ⟩ = ⟨ c , ⟨ M⇓c , sub-𝕍 𝕍v v'⊑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 ⟩ ⟩ = ⟨ c , ⟨ (⇓-var eq 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 ⟩ ⟩ = ⟨ c' , ⟨ ⇓-app L⇓L' 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 ... | ⟨ c₁ , ⟨ M⇓c₁ , 𝕍v₁ ⟩ ⟩ | ⟨ c₂ , ⟨ M⇓c₂ , 𝕍v₂ ⟩ ⟩ rewrite ⇓-determ M⇓c₂ M⇓c₁ = ⟨ c₁ , ⟨ M⇓c₁ , 𝕍⊔-intro 𝕍v₁ 𝕍v₂ ⟩ ⟩ ↓→𝔼 𝔾γγ' (⊔-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 = contradiction fv1 nfv1 ... | inj₂ fv2 = contradiction fv2 nfv2 ↓→𝔼 {Γ} {γ} {γ'} {M} {v'} 𝔾γγ' (sub{v = v} d v'⊑v) fv' with ↓→𝔼 {Γ} {γ} {γ'} {M} 𝔾γγ' d (above-fun-⊑ fv' v'⊑v) ... | ⟨ c , ⟨ M⇓c , 𝕍v ⟩ ⟩ = ⟨ c , ⟨ M⇓c , sub-𝕍 𝕍v v'⊑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-𝕍`

.

## Proof of denotational adequacy

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)) ⟨ ⊥ , ⟨ ⊥ , ⊑-refl ⟩ ⟩ ... | ⟨ clos {Γ} M′ γ , ⟨ M⇓c , Vc ⟩ ⟩ with 𝕍→WHNF Vc ... | ƛ_ {N = N′} = ⟨ Γ , ⟨ N′ , ⟨ γ , M⇓c ⟩ ⟩ ⟩

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′) adequacy{M}{N} eq with ↓→⇓ eq ... | ⟨ Γ , ⟨ N′ , ⟨ γ , M⇓ ⟩ ⟩ ⟩ = 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)
```