module plfa.part2.BigStep where

Introduction

The call-by-name evaluation strategy is a deterministic method for computing the value of a program in the lambda calculus. That is, call-by-name produces a value if and only if beta reduction can reduce the program to a lambda abstraction. In this chapter we define call-by-name evaluation and prove the forward direction of this if-and-only-if. The backward direction is traditionally proved via Curry-Feys standardisation, which is quite complex. We give a sketch of that proof, due to Plotkin, but postpone the proof in Agda until after we have developed a denotational semantics for the lambda calculus, at which point the proof is an easy corollary of properties of the denotational semantics.

We present the call-by-name strategy as a relation between an input term and an output value. Such a relation is often called a big-step semantics, written M ⇓ V, as it relates the input term M directly to the final result V, in contrast to the small-step reduction relation, M β€”β†’ Mβ€², that maps M to another term Mβ€² in which a single sub-computation has been completed.

Imports

open import Relation.Binary.PropositionalEquality
  using (_≑_; refl; trans; sym; cong-app)
open import Data.Product.Base using (_Γ—_; Ξ£; Ξ£-syntax; βˆƒ; βˆƒ-syntax; proj₁; projβ‚‚)
  renaming (_,_ to ⟨_,_⟩)
open import Function.Base using (_∘_)
open import plfa.part2.Untyped
  using (Context; _⊒_; _βˆ‹_; β˜…; βˆ…; _,_; Z; S_; `_; #_; Ζ›_; _Β·_;
  subst; subst-zero; exts; rename; Ξ²; ξ₁; ΞΎβ‚‚; ΞΆ; _β€”β†’_; _β€”β† _; _β€”β†’βŸ¨_⟩_; _∎;
  β€”β† -trans; appL-cong)
open import plfa.part2.Substitution using (Subst; ids)

Environments

To handle variables and function applications, there is the choice between using substitution, as in β€”β†’, or to use an environment. An environment in call-by-name is a map from variables to closures, that is, to terms paired with their environments. We choose to use environments instead of substitution because the point of the call-by-name strategy is to be closer to an implementation of the language. Also, the denotational semantics introduced in later chapters uses environments and the proof of adequacy is made easier by aligning these choices.

We define environments and closures as follows.

ClosEnv : Context β†’ Set

data Clos : Set where
  clos : βˆ€{Ξ“} β†’ (M : Ξ“ ⊒ β˜…) β†’ ClosEnv Ξ“ β†’ Clos

ClosEnv Ξ“ = βˆ€ (x : Ξ“ βˆ‹ β˜…) β†’ Clos

As usual, we have the empty environment, and we can extend an environment.

βˆ…' : ClosEnv βˆ…
βˆ…' ()

_,'_ : βˆ€ {Ξ“} β†’ ClosEnv Ξ“ β†’ Clos β†’ ClosEnv (Ξ“ , β˜…)
(Ξ³ ,' c) Z = c
(Ξ³ ,' c) (S x) = Ξ³ x

Big-step evaluation

The big-step semantics is represented as a ternary relation, written Ξ³ ⊒ M ⇓ V, where Ξ³ is the environment, M is the input term, and V is the result value. A value is a closure whose term is a lambda abstraction.

data _⊒_⇓_ : βˆ€{Ξ“} β†’ ClosEnv Ξ“ β†’ (Ξ“ ⊒ β˜…) β†’ Clos β†’ Set where

  ⇓-var : βˆ€{Ξ“}{Ξ³ : ClosEnv Ξ“}{x : Ξ“ βˆ‹ β˜…}{Ξ”}{Ξ΄ : ClosEnv Ξ”}{M : Ξ” ⊒ β˜…}{V}
    β†’ Ξ³ x ≑ clos M Ξ΄
    β†’ Ξ΄ ⊒ M ⇓ V
      -----------
    β†’ Ξ³ ⊒ ` x ⇓ V

  ⇓-lam : βˆ€{Ξ“}{Ξ³ : ClosEnv Ξ“}{M : Ξ“ , β˜… ⊒ β˜…}
    β†’ Ξ³ ⊒ Ζ› M ⇓ clos (Ζ› M) Ξ³

  ⇓-app : βˆ€{Ξ“}{Ξ³ : ClosEnv Ξ“}{L M : Ξ“ ⊒ β˜…}{Ξ”}{Ξ΄ : ClosEnv Ξ”}{N : Ξ” , β˜… ⊒ β˜…}{V}
    β†’ Ξ³ ⊒ L ⇓ clos (Ζ› N) Ξ΄   β†’   (Ξ΄ ,' clos M Ξ³) ⊒ N ⇓ V
      ---------------------------------------------------
    β†’ Ξ³ ⊒ L Β· M ⇓ V

  • The ⇓-var rule evaluates a variable by finding the associated closure in the environment and then evaluating the closure.

  • The ⇓-lam rule turns a lambda abstraction into a closure by packaging it up with its environment.

  • The ⇓-app rule performs function application by first evaluating the term L in operator position. If that produces a closure containing a lambda abstraction Ζ› N, then we evaluate the body N in an environment extended with the argument M. Note that M is not evaluated in rule ⇓-app because this is call-by-name and not call-by-value.

Exercise big-step-eg (practice)

Show that (Ζ› Ζ› # 1) Β· ((Ζ› # 0 Β· # 0) Β· (Ζ› # 0 Β· # 0)) terminates under big-step call-by-name evaluation.

-- Your code goes here

The big-step semantics is deterministic

If the big-step relation evaluates a term M to both V and Vβ€², then V and Vβ€² must be identical. In other words, the call-by-name relation is a partial function. The proof is a straightforward induction on the two big-step derivations.

⇓-determ : βˆ€{Ξ“}{Ξ³ : ClosEnv Ξ“}{M : Ξ“ ⊒ β˜…}{V V' : Clos}
  β†’ Ξ³ ⊒ M ⇓ V β†’ Ξ³ ⊒ M ⇓ V'
  β†’ V ≑ V'
⇓-determ (⇓-var eq1 mc) (⇓-var eq2 mc')
    with trans (sym eq1) eq2
... | refl = ⇓-determ mc mc'
⇓-determ ⇓-lam ⇓-lam = refl
⇓-determ (⇓-app mc mc₁) (⇓-app mc' mc'')
    with ⇓-determ mc mc'
... | refl = ⇓-determ mc₁ mc''

Big-step evaluation implies beta reduction to a lambda

If big-step evaluation produces a value, then the input term can reduce to a lambda abstraction by beta reduction:

  βˆ…' ⊒ M ⇓ clos (Ζ› Nβ€²) Ξ΄
  -----------------------------
β†’ Ξ£[ N ∈ βˆ… , β˜… ⊒ β˜… ] (M β€”β†  Ζ› N)

The proof is by induction on the big-step derivation. As is often necessary, one must generalize the statement to get the induction to go through. In the case for ⇓-app (function application), the argument is added to the environment, so the environment becomes non-empty. The corresponding Ξ² reduction substitutes the argument into the body of the lambda abstraction. So we generalize the lemma to allow an arbitrary environment Ξ³ and we add a premise that relates the environment Ξ³ to an equivalent substitution Οƒ.

The case for ⇓-app also requires that we strengthen the conclusion. In the case for ⇓-app we have Ξ³ ⊒ L ⇓ clos (Ξ» N) Ξ΄ and the induction hypothesis gives us L β€”β†  Ζ› Nβ€², but we need to know that N and Nβ€² are equivalent. In particular, that Nβ€² ≑ subst Ο„ N where Ο„ is the substitution that is equivalent to Ξ΄. Therefore we expand the conclusion of the statement, stating that the results are equivalent.

We make the two notions of equivalence precise by defining the following two mutually-recursive predicates V β‰ˆ M and Ξ³ β‰ˆβ‚‘ Οƒ.

_β‰ˆ_ : Clos β†’ (βˆ… ⊒ β˜…) β†’ Set
_β‰ˆβ‚‘_ : βˆ€{Ξ“} β†’ ClosEnv Ξ“ β†’ Subst Ξ“ βˆ… β†’ Set

(clos {Ξ“} M Ξ³) β‰ˆ N = Ξ£[ Οƒ ∈ Subst Ξ“ βˆ… ] Ξ³ β‰ˆβ‚‘ Οƒ Γ— (N ≑ subst Οƒ M)

Ξ³ β‰ˆβ‚‘ Οƒ = βˆ€ x β†’ (Ξ³ x) β‰ˆ (Οƒ x)

We can now state the main lemma:

If Ξ³ ⊒ M ⇓ V  and  Ξ³ β‰ˆβ‚‘ Οƒ,
then  subst Οƒ M β€”β†  N  and  V β‰ˆ N  for some N.

Before starting the proof, we establish a couple lemmas about equivalent environments and substitutions.

The empty environment is equivalent to the identity substitution ids, which we import from Chapter Substitution.

β‰ˆβ‚‘-id : βˆ…' β‰ˆβ‚‘ ids
β‰ˆβ‚‘-id ()

Of course, applying the identity substitution to a term returns the same term.

sub-id : βˆ€{Ξ“} {A} {M : Ξ“ ⊒ A} β†’ subst ids M ≑ M
sub-id = plfa.part2.Substitution.sub-id

We define an auxiliary function for extending a substitution.

ext-subst : βˆ€{Ξ“ Ξ”} β†’ Subst Ξ“ Ξ” β†’ Ξ” ⊒ β˜… β†’ Subst (Ξ“ , β˜…) Ξ”
ext-subst{Ξ“}{Ξ”} Οƒ N {A} = subst (subst-zero N) ∘ exts Οƒ

The next lemma we need to prove states that if you start with an equivalent environment and substitution Ξ³ β‰ˆβ‚‘ Οƒ, extending them with an equivalent closure and term V β‰ˆ N produces an equivalent environment and substitution: (Ξ³ ,' V) β‰ˆβ‚‘ (ext-subst Οƒ N), or equivalently, (Ξ³ ,' V) x β‰ˆ (ext-subst Οƒ N) x for any variable x. The proof will be by induction on x and for the induction step we need the following lemma, which states that applying the composition of exts Οƒ and subst-zero to S x is the same as just Οƒ x, which is a corollary of a theorem in Chapter Substitution.

subst-zero-exts : βˆ€{Ξ“ Ξ”}{Οƒ : Subst Ξ“ Ξ”}{B}{M : Ξ” ⊒ B}{x : Ξ“ βˆ‹ β˜…}
  β†’ (subst (subst-zero M) ∘ exts Οƒ) (S x) ≑ Οƒ x
subst-zero-exts {Ξ“}{Ξ”}{Οƒ}{B}{M}{x} =
   cong-app (plfa.part2.Substitution.subst-zero-exts-cons{Οƒ = Οƒ}) (S x)

So the proof of β‰ˆβ‚‘-ext is as follows.

β‰ˆβ‚‘-ext : βˆ€ {Ξ“} {Ξ³ : ClosEnv Ξ“} {Οƒ : Subst Ξ“ βˆ…} {V} {N : βˆ… ⊒ β˜…}
  β†’ Ξ³ β‰ˆβ‚‘ Οƒ  β†’  V β‰ˆ N
    --------------------------
  β†’ (Ξ³ ,' V) β‰ˆβ‚‘ (ext-subst Οƒ N)
β‰ˆβ‚‘-ext {Ξ“} {Ξ³} {Οƒ} {V} {N} Ξ³β‰ˆβ‚‘Οƒ Vβ‰ˆN Z = Vβ‰ˆN
β‰ˆβ‚‘-ext {Ξ“} {Ξ³} {Οƒ} {V} {N} Ξ³β‰ˆβ‚‘Οƒ Vβ‰ˆN (S x)
  rewrite subst-zero-exts {Οƒ = Οƒ}{M = N}{x} = Ξ³β‰ˆβ‚‘Οƒ x

We proceed by induction on the input variable.

  • If it is Z, then we immediately conclude using the premise V β‰ˆ N.

  • If it is S x, then we rewrite using the subst-zero-exts lemma and use the premise Ξ³ β‰ˆβ‚‘ Οƒ to conclude.

To prove the main lemma, we need another technical lemma about substitution. Applying one substitution after another is the same as composing the two substitutions and then applying them.

sub-sub : βˆ€{Ξ“ Ξ” Ξ£}{A}{M : Ξ“ ⊒ A} {σ₁ : Subst Ξ“ Ξ”}{Οƒβ‚‚ : Subst Ξ” Ξ£}
  β†’ subst Οƒβ‚‚ (subst σ₁ M) ≑ subst (subst Οƒβ‚‚ ∘ σ₁) M
sub-sub {M = M} = plfa.part2.Substitution.sub-sub {M = M}

We arrive at the main lemma: if M big steps to a closure V in environment Ξ³, and if Ξ³ β‰ˆβ‚‘ Οƒ, then subst Οƒ M reduces to some term N that is equivalent to V. We describe the proof below.

β‡“β†’β€”β† Γ—β‰ˆ : βˆ€{Ξ“}{Ξ³ : ClosEnv Ξ“}{Οƒ : Subst Ξ“ βˆ…}{M : Ξ“ ⊒ β˜…}{V : Clos}
       β†’ Ξ³ ⊒ M ⇓ V  β†’  Ξ³ β‰ˆβ‚‘ Οƒ
         ---------------------------------------
       β†’ Ξ£[ N ∈ βˆ… ⊒ β˜… ] (subst Οƒ M β€”β†  N) Γ— V β‰ˆ N
β‡“β†’β€”β† Γ—β‰ˆ {Ξ³ = Ξ³} (⇓-var{x = x} Ξ³x≑LΞ΄ δ⊒L⇓V) Ξ³β‰ˆβ‚‘Οƒ
    with Ξ³ x | Ξ³β‰ˆβ‚‘Οƒ x | Ξ³x≑LΞ΄
... | clos L Ξ΄ | ⟨ Ο„ , ⟨ Ξ΄β‰ˆβ‚‘Ο„ , Οƒx≑τL ⟩ ⟩ | refl
      with β‡“β†’β€”β† Γ—β‰ˆ{Οƒ = Ο„} δ⊒L⇓V Ξ΄β‰ˆβ‚‘Ο„
...   | ⟨ N , ⟨ Ο„Lβ€”β† N , Vβ‰ˆN ⟩ ⟩ rewrite Οƒx≑τL =
        ⟨ N , ⟨ Ο„Lβ€”β† N , Vβ‰ˆN ⟩ ⟩
β‡“β†’β€”β† Γ—β‰ˆ {Οƒ = Οƒ} {V = clos (Ζ› N) Ξ³} (⇓-lam) Ξ³β‰ˆβ‚‘Οƒ =
    ⟨ subst Οƒ (Ζ› N) , ⟨ subst Οƒ (Ζ› N) ∎ , ⟨ Οƒ , ⟨ Ξ³β‰ˆβ‚‘Οƒ , refl ⟩ ⟩ ⟩ ⟩
β‡“β†’β€”β† Γ—β‰ˆ{Ξ“}{Ξ³} {Οƒ = Οƒ} {L Β· M} {V} (⇓-app {N = N} L⇓ƛNΞ΄ N⇓V) Ξ³β‰ˆβ‚‘Οƒ
    with β‡“β†’β€”β† Γ—β‰ˆ{Οƒ = Οƒ} L⇓ƛNΞ΄ Ξ³β‰ˆβ‚‘Οƒ
... | ⟨ _ , ⟨ ΟƒLβ€”β† Ζ›Ο„N , ⟨ Ο„ , ⟨ Ξ΄β‰ˆβ‚‘Ο„ , ≑ƛτN ⟩ ⟩ ⟩ ⟩ rewrite ≑ƛτN
      with β‡“β†’β€”β† Γ—β‰ˆ {Οƒ = ext-subst Ο„ (subst Οƒ M)} N⇓V
             (Ξ» x β†’ β‰ˆβ‚‘-ext{Οƒ = Ο„} Ξ΄β‰ˆβ‚‘Ο„ ⟨ Οƒ , ⟨ Ξ³β‰ˆβ‚‘Οƒ , refl ⟩ ⟩ x)
           | Ξ²{βˆ…}{subst (exts Ο„) N}{subst Οƒ M}
...   | ⟨ N' , ⟨ β€”β† N' , Vβ‰ˆN' ⟩ ⟩ | Ζ›Ο„NΒ·ΟƒMβ€”β†’
        rewrite sub-sub{M = N}{σ₁ = exts Ο„}{Οƒβ‚‚ = subst-zero (subst Οƒ M)} =
        let rs = (Ζ› subst (exts Ο„) N) Β· subst Οƒ M β€”β†’βŸ¨ Ζ›Ο„NΒ·ΟƒMβ€”β†’ ⟩ β€”β† N' in
        let g = β€”β† -trans (appL-cong ΟƒLβ€”β† Ζ›Ο„N) rs in
        ⟨ N' , ⟨ g , Vβ‰ˆN' ⟩ ⟩

The proof is by induction on Ξ³ ⊒ M ⇓ V. We have three cases to consider.

  • Case ⇓-var. So we have Ξ³ x ≑ clos L Ξ΄ and Ξ΄ ⊒ L ⇓ V. We need to show that subst Οƒ (` x) β€”β†  N and V β‰ˆ N for some N. The premise Ξ³ β‰ˆβ‚‘ Οƒ tells us that Ξ³ x β‰ˆ Οƒ x, so clos L Ξ΄ β‰ˆ Οƒ x. By the definition of β‰ˆ, there exists a Ο„ such that Ξ΄ β‰ˆβ‚‘ Ο„ and Οƒ x ≑ subst Ο„ L. Using Ξ΄ ⊒ L ⇓ V and Ξ΄ β‰ˆβ‚‘ Ο„, the induction hypothesis gives us subst Ο„ L β€”β†  N and V β‰ˆ N for some N. So we have shown that subst Οƒ x β€”β†  N and V β‰ˆ N for some N.

  • Case ⇓-lam. We immediately have subst Οƒ (Ζ› N) β€”β†  subst Οƒ (Ζ› N) and clos (subst Οƒ (Ζ› N)) Ξ³ β‰ˆ subst Οƒ (Ζ› N).

  • Case ⇓-app. Using Ξ³ ⊒ L ⇓ clos (Ζ› N) Ξ΄ and Ξ³ β‰ˆβ‚‘ Οƒ, the induction hypothesis gives us

      subst Οƒ L β€”β†  Ζ› subst (exts Ο„) N                                     (1)

    and Ξ΄ β‰ˆβ‚‘ Ο„ for some Ο„. From Ξ³β‰ˆβ‚‘Οƒ we have clos M Ξ³ β‰ˆ subst Οƒ M. Then with (Ξ΄ ,' clos M Ξ³) ⊒ N ⇓ V, the induction hypothesis gives us V β‰ˆ N' and

      subst (subst (subst-zero (subst Οƒ M)) ∘ (exts Ο„)) N β€”β†  N'         (2)

    Meanwhile, by Ξ², we have

      (Ζ› subst (exts Ο„) N) Β· subst Οƒ M
  β€”β†’ subst (subst-zero (subst Οƒ M)) (subst (exts Ο„) N)

    which is the same as the following, by sub-sub.

      (Ζ› subst (exts Ο„) N) Β· subst Οƒ M
  β€”β†’ subst (subst (subst-zero (subst Οƒ M)) ∘ exts Ο„) N              (3)

    Using (3) and (2) we have

      (Ζ› subst (exts Ο„) N) Β· subst Οƒ M β€”β†  N'                             (4)

    From (1) we have

      subst Οƒ L Β· subst Οƒ M β€”β†  (Ζ› subst (exts Ο„) N) Β· subst Οƒ M

    which we combine with (4) to conclude that

      subst Οƒ L Β· subst Οƒ M β€”β†  N'

With the main lemma complete, we establish the forward direction of the equivalence between the big-step semantics and beta reduction.

cbnβ†’reduce :  βˆ€{M : βˆ… ⊒ β˜…}{Ξ”}{Ξ΄ : ClosEnv Ξ”}{Nβ€² : Ξ” , β˜… ⊒ β˜…}
  β†’ βˆ…' ⊒ M ⇓ clos (Ζ› Nβ€²) Ξ΄
    -----------------------------
  β†’ Ξ£[ N ∈ βˆ… , β˜… ⊒ β˜… ] (M β€”β†  Ζ› N)
cbnβ†’reduce {M}{Ξ”}{Ξ΄}{Nβ€²} M⇓c
    with β‡“β†’β€”β† Γ—β‰ˆ{Οƒ = ids} M⇓c β‰ˆβ‚‘-id
... | ⟨ N , ⟨ rs , ⟨ Οƒ , ⟨ h , eq2 ⟩ ⟩ ⟩ ⟩ rewrite sub-id{M = M} | eq2 =
      ⟨ subst (exts Οƒ) Nβ€² , rs ⟩

Exercise big-alt-implies-multi (practice)

Formulate an alternative big-step semantics, of the form M ↓ N, for call-by-name that uses substitution instead of environments. That is, the analogue of the application rule ⇓-app should perform substitution, as in N [ M ], instead of extending the environment with M. Prove that M ↓ N implies M β€”β†  N.

-- Your code goes here

Beta reduction to a lambda implies big-step evaluation

The proof of the backward direction, that beta reduction to a lambda implies that the call-by-name semantics produces a result, is more difficult to prove. The difficulty stems from reduction proceeding underneath lambda abstractions via the ΞΆ rule. The call-by-name semantics does not reduce under lambda, so a straightforward proof by induction on the reduction sequence is impossible. In the article Call-by-name, call-by-value, and the Ξ»-calculus, Plotkin proves the theorem in two steps, using two auxiliary reduction relations. The first step uses a classic technique called Curry-Feys standardisation. It relies on the notion of standard reduction sequence, which acts as a half-way point between full beta reduction and call-by-name by expanding call-by-name to also include reduction underneath lambda. Plotkin proves that M reduces to L if and only if M is related to L by a standard reduction sequence.

Theorem 1 (Standardisation)
`M β€”β†  L` if and only if `M` goes to `L` via a standard reduction sequence.

Plotkin then introduces left reduction, a small-step version of call-by-name and uses the above theorem to prove that beta reduction and left reduction are equivalent in the following sense.

Corollary 1
`M β€”β†  Ζ› N` if and only if `M` goes to `Ζ› Nβ€²`, for some `Nβ€²`, by left reduction.

The second step of the proof connects left reduction to call-by-name evaluation.

Theorem 2
`M` left reduces to `Ζ› N` if and only if `⊒ M ⇓ Ζ› N`.

(Plotkin’s call-by-name evaluator uses substitution instead of environments, which explains why the environment is omitted in ⊒ M ⇓ Ζ› N in the above theorem statement.)

Putting Corollary 1 and Theorem 2 together, Plotkin proves that call-by-name evaluation is equivalent to beta reduction.

Corollary 2
`M β€”β†  Ζ› N` if and only if `⊒ M ⇓ Ζ› Nβ€²` for some `Nβ€²`.

Plotkin also proves an analogous result for the Ξ»α΅₯ calculus, relating it to call-by-value evaluation. For a nice exposition of that proof, we recommend Chapter 5 of Semantics Engineering with PLT Redex by Felleisen, Findler, and Flatt.

Instead of proving the backwards direction via standardisation, as sketched above, we defer the proof until after we define a denotational semantics for the lambda calculus, at which point the proof of the backwards direction will fall out as a corollary to the soundness and adequacy of the denotational semantics.

Unicode

This chapter uses the following unicode:

β‰ˆ  U+2248  ALMOST EQUAL TO (\~~ or \approx)
β‚‘  U+2091  LATIN SUBSCRIPT SMALL LETTER E (\_e)
⊒  U+22A2  RIGHT TACK (\|- or \vdash)
⇓  U+21DB  DOWNWARDS DOUBLE ARROW (\d= or \Downarrow)