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 (no divergence).

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 reduction a lambda abstraction.

It is well known that a term can reduce to a lambda abstraction using full Ξ² reduction if and only if it can reduce to a lambda abstraction using the call-by-name reduction strategy. So we shall prove that Ξ³ ⊒ M ↓ (v ↦ w) implies that M halts under call-by-name evaluation, which we define with a big-step semantics written Ξ³' ⊒ M ⇓ c, where c is a closure (a term paired with an environment) and Ξ³' is an environment that maps variables to closures

So we will show that Ξ³ ⊒ M ↓ (v ↦ w) implies Ξ³' ⊒ M ⇓ c, provided Ξ³ 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.

  • We 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 call-by-name big-step semantics of the lambda calculus and prove that it is deterministic.

  • We define the logical relation 𝕍 that relates values and closures, and extend it to a relation on terms 𝔼 and environments 𝔾.

  • 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 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 βŠ₯
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 = βŠ₯-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
... | Ζ›_ =
      ⟨ 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 = βŠ₯-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 ⟩ ⟩ =
      ⟨ 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 = βŠ₯-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 ⟩ ⟩ =
      ⟨ 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

The adequacy property is a corollary of the main lemma. We have βˆ… ⊒ Ζ› N ↓ βŠ₯ ↦ βŠ₯, so β„° M ≃ β„° (Ζ› N) gives us βˆ… ⊒ M ↓ βŠ₯ ↦ βŠ₯. Then the main lemma gives us βˆ… ⊒ M ⇓ clos (Ζ› Nβ€²) Ξ³ for some Nβ€² and Ξ³.

adequacy : βˆ€{M : βˆ… ⊒ β˜…}{N : βˆ… , β˜… ⊒ β˜…}  β†’  β„° M ≃ β„° (Ζ› N)
         β†’  Ξ£[ Ξ“ ∈ Context ] Ξ£[ Nβ€² ∈ (Ξ“ , β˜… ⊒ β˜…) ] Ξ£[ Ξ³ ∈ ClosEnv Ξ“ ]
            βˆ…' ⊒ M ⇓ clos (Ζ› Nβ€²) Ξ³
adequacy{M}{N} eq
    with ↓→𝔼 𝔾-βˆ… ((projβ‚‚ (eq `βˆ… (βŠ₯ ↦ βŠ₯))) (↦-intro βŠ₯-intro))
                 ⟨ βŠ₯ , ⟨ βŠ₯ , βŠ‘-refl ⟩ ⟩
... | ⟨ clos {Ξ“} Mβ€² Ξ³ , ⟨ M⇓c , Vc ⟩ ⟩
    with 𝕍→WHNF Vc
... | Ζ›_ {N = Nβ€²} =
    ⟨ Ξ“ , ⟨ Nβ€² , ⟨ Ξ³ , M⇓c ⟩  ⟩ ⟩

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 the chapter CallByName we established the forward direction: that if call-by-name produces a result, then the program beta reduces to a lambda abstraction. 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 = adequacy (soundness M—↠ƛN)

Suppose M β€”β†  Ζ› N. Soundness of the denotational semantics gives us β„° M ≃ β„° (Ζ› N). Then by adequacy 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)