BigStep: Bigstep semantics of untyped lambda calculus
module plfa.part2.BigStep where
Introduction
The callbyname evaluation strategy is a deterministic method for computing the value of a program in the lambda calculus. That is, callbyname produces a value if and only if beta reduction can reduce the program to a lambda abstraction. In this chapter we define callbyname evaluation and prove the forward direction of this ifandonlyif. The backward direction is traditionally proved via CurryFeys 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 callbyname strategy as a relation between an input
term and an output value. Such a relation is often called a bigstep
semantics, written M ⇓ V
, as it relates the input term M
directly
to the final result V
, in contrast to the smallstep reduction
relation, M —→ M′
, that maps M
to another term M′
in which a
single subcomputation has been completed.
Imports
open import Relation.Binary.PropositionalEquality using (_≡_; refl; trans; sym; congapp) open import Data.Product using (_×_; Σ; Σsyntax; ∃; ∃syntax; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩) open import Function using (_∘_) open import plfa.part2.Untyped using (Context; _⊢_; _∋_; ★; ∅; _,_; Z; S_; `_; #_; ƛ_; _·_; subst; substzero; exts; rename; β; ξ₁; ξ₂; ζ; _—→_; _—↠_; _—→⟨_⟩_; _∎; —↠trans; appLcong) open import plfa.part2.Substitution using (Subst; ids)
Environments
To handle variables and function application, there is the choice
between using substitution, as in —→
, or to use an environment.
An environment in callbyname 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
callbyname 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
Bigstep evaluation
The bigstep 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 termL
in operator position. If that produces a closure containing a lambda abstractionƛ N
, then we evaluate the bodyN
in an environment extended with the argumentM
. Note thatM
is not evaluated in rule⇓app
because this is callbyname and not callbyvalue.
Exercise bigstepeg
(practice)
Show that (ƛ ƛ # 1) · ((ƛ # 0 · # 0) · (ƛ # 0 · # 0))
terminates under bigstep callbyname evaluation.
 Your code goes here
The bigstep semantics is deterministic
If the bigstep relation evaluates a term M
to both V
and
V′
, then V
and V′
must be identical. In other words, the
callbyname relation is a partial function. The proof is a
straightforward induction on the two bigstep 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''
Bigstep evaluation implies beta reduction to a lambda
If bigstep 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 bigstep 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
nonempty. 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 mutuallyrecursive 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.
subid : ∀{Γ} {A} {M : Γ ⊢ A} → subst ids M ≡ M subid = plfa.part2.Substitution.subid
We define an auxilliary function for extending a substitution.
extsubst : ∀{Γ Δ} → Subst Γ Δ → Δ ⊢ ★ → Subst (Γ , ★) Δ extsubst{Γ}{Δ} σ N {A} = subst (substzero 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 c ≈ N
produces an equivalent
environment and substitution: (γ ,' V) ≈ₑ (extsubst σ N)
,
or equivalently, (γ ,' V) x ≈ₑ (extsubst σ 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 substzero
to S x
is the same as just σ x
,
which is a corollary of a theorem in
Chapter Substitution.
substzeroexts : ∀{Γ Δ}{σ : Subst Γ Δ}{B}{M : Δ ⊢ B}{x : Γ ∋ ★} → (subst (substzero M) ∘ exts σ) (S x) ≡ σ x substzeroexts {Γ}{Δ}{σ}{B}{M}{x} = congapp (plfa.part2.Substitution.substzeroextscons{σ = σ}) (S x)
So the proof of ≈ₑext
is as follows.
≈ₑext : ∀ {Γ} {γ : ClosEnv Γ} {σ : Subst Γ ∅} {V} {N : ∅ ⊢ ★} → γ ≈ₑ σ → V ≈ N  → (γ ,' V) ≈ₑ (extsubst σ N) ≈ₑext {Γ} {γ} {σ} {V} {N} γ≈ₑσ V≈N {Z} = V≈N ≈ₑext {Γ} {γ} {σ} {V} {N} γ≈ₑσ V≈N {S x} rewrite substzeroexts {σ = σ}{M = N}{x} = γ≈ₑσ
We proceed by induction on the input variable.

If it is
Z
, then we immediately conclude using the premiseV ≈ N
. 
If it is
S x
, then we rewrite using thesubstzeroexts
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.
subsub : ∀{Γ Δ Σ}{A}{M : Γ ⊢ A} {σ₁ : Subst Γ Δ}{σ₂ : Subst Δ Σ} → subst σ₂ (subst σ₁ M) ≡ subst (subst σ₂ ∘ σ₁) M subsub {M = M} = plfa.part2.Substitution.subsub {M = M}
We arive 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 ⇓→—↠×≈ {σ = extsubst τ (subst σ M)} N⇓V (λ {x} → ≈ₑext{σ = τ} δ≈ₑτ ⟨ σ , ⟨ γ≈ₑσ , refl ⟩ ⟩ {x})  β{∅}{subst (exts τ) N}{subst σ M} ...  ⟨ N' , ⟨ —↠N' , V≈N' ⟩ ⟩  ƛτN·σM—→ rewrite subsub{M = N}{σ₁ = exts τ}{σ₂ = substzero (subst σ M)} = let rs = (ƛ subst (exts τ) N) · subst σ M —→⟨ ƛτN·σM—→ ⟩ —↠N' in let g = —↠trans (appLcong σ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 thatsubst σ x —↠ N
andV ≈ N
for someN
. The premiseγ ≈ₑ σ
tells us thatγ x ≈ σ x
, soclos L δ ≈ σ x
. By the definition of≈
, there exists aτ
such thatδ ≈ₑ τ
andσ x ≡ subst τ L
. Usingδ ⊢ L ⇓ V
andδ ≈ₑ τ
, the induction hypothesis gives ussubst τ L —↠ N
andV ≈ N
for someN
. So we have shown thatsubst σ x —↠ N
andV ≈ N
for someN
. 
Case
⇓lam
. We immediately havesubst σ (ƛ N) —↠ subst σ (ƛ N)
andclos (subst σ (ƛ N)) γ ≈ subst σ (ƛ N)
. 
Case
⇓app
. Usingγ ⊢ L ⇓ clos N δ
andγ ≈ₑ σ
, the induction hypothesis gives ussubst σ L —↠ ƛ subst (exts τ) N (1)
and
δ ≈ₑ τ
for someτ
. Fromγ≈ₑσ
we haveclos M γ ≈ subst σ M
. Then with(δ ,' clos M γ) ⊢ N ⇓ V
, the induction hypothesis gives usV ≈ N'
andsubst (subst (substzero (subst σ M)) ∘ (exts τ)) N —↠ N' (2)
Meanwhile, by
β
, we have(ƛ subst (exts τ) N) · subst σ M —→ subst (substzero (subst σ M)) (subst (exts τ) N)
which is the same as the following, by
subsub
.(ƛ subst (exts τ) N) · subst σ M —→ subst (subst (substzero (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 bigstep 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 subid{M = M}  eq2 = ⟨ subst (exts σ) N′ , rs ⟩
Exercise bigaltimpliesmulti
(practice)
Formulate an alternative bigstep semantics, of the form M ↓ N
, for
callbyname 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 bigstep evaluation
The proof of the backward direction, that beta reduction to a lambda
implies that the callbyname semantics produces a result, is more
difficult to prove. The difficulty stems from reduction proceeding
underneath lambda abstractions via the ζ
rule. The callbyname
semantics does not reduce under lambda, so a straightforward proof by
induction on the reduction sequence is impossible. In the article
Callbyname, callbyvalue, and the λcalculus, Plotkin proves the
theorem in two steps, using two auxilliary reduction relations. The
first step uses a classic technique called CurryFeys standardisation.
It relies on the notion of standard reduction sequence, which acts
as a halfway point between full beta reduction and callbyname by
expanding callbyname 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 smallstep version of callbyname 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 callbyname evaluation.
Theorem 2
`M` left reduces to `ƛ N` if and only if `⊢ M ⇓ ƛ N`.
(Plotkin’s callbyname 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 callbyname 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 callbyvalue 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)