Soundness: Soundness of reduction with respect to denotational semantics 🚧
module plfa.part3.Soundness where
Introduction
In this chapter we prove that the reduction semantics is sound with respect to the denotational semantics, i.e., for any term L
L —↠ ƛ N implies ℰ L ≃ ℰ (ƛ N)
The proof is by induction on the reduction sequence, so the main lemma
concerns a single reduction step. We prove that if any term M
steps
to a term N
, then M
and N
are denotationally equal. We shall
prove each direction of this ifandonlyif separately. One direction
will look just like a type preservation proof. The other direction is
like proving type preservation for reduction going in reverse. Recall
that type preservation is sometimes called subject
reduction. Preservation in reverse is a wellknown property and is
called subject expansion. It is also wellknown that subject
expansion is false for most typed lambda calculi!
Imports
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; sym; cong; cong₂; congapp) open import Data.Product using (_×_; Σ; Σsyntax; ∃; ∃syntax; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩) open import Agda.Primitive using (lzero) open import Relation.Nullary using (¬_) open import Relation.Nullary.Negation using (contradiction) open import Data.Empty using (⊥elim) open import Relation.Nullary using (Dec; yes; no) open import Function using (_∘_) open import plfa.part2.Untyped using (Context; _,_; _∋_; _⊢_; ★; Z; S_; `_; ƛ_; _·_; subst; _[_]; substzero; ext; rename; exts; _—→_; ξ₁; ξ₂; β; ζ; _—↠_; _—→⟨_⟩_; _∎) open import plfa.part2.Substitution using (Rename; Subst; ids) open import plfa.part3.Denotational using (Value; ⊥; Env; _⊢_↓_; _`,_; _⊑_; _`⊑_; `⊥; _`⊔_; init; last; initlast; ⊑refl; ⊑trans; `⊑refl; ⊑env; ⊑envconjR1; ⊑envconjR2; upenv; var; ↦elim; ↦intro; ⊥intro; ⊔intro; sub; renamepres; ℰ; _≃_; ≃trans) open import plfa.part3.Compositional using (lambdainversion; varinv)
Forward reduction preserves denotations
The proof of preservation in this section mixes techniques from previous chapters. Like the proof of preservation for the STLC, we are preserving a relation defined separately from the syntax, in contrast to the intrinsicallytyped terms. On the other hand, we are using de Bruijn indices for variables.
The outline of the proof remains the same in that we must prove lemmas concerning all of the auxiliary functions used in the reduction relation: substitution, renaming, and extension.
Simultaneous substitution preserves denotations
Our next goal is to prove that simultaneous substitution preserves
meaning. That is, if M
results in v
in environment γ
, then applying a
substitution σ
to M
gives us a program that also results in v
, but in
an environment δ
in which, for every variable x
, σ x
results in the
same value as the one for x
in the original environment γ
.
We write δ ⊢ σ ↓ γ
for this condition.
infix 3 _`⊢_↓_ _`⊢_↓_ : ∀{Δ Γ} → Env Δ → Subst Γ Δ → Env Γ → Set _`⊢_↓_ {Δ}{Γ} δ σ γ = (∀ (x : Γ ∋ ★) → δ ⊢ σ x ↓ γ x)
As usual, to prepare for lambda abstraction, we prove an extension
lemma. It says that applying the exts
function to a substitution
produces a new substitution that maps variables to terms that when
evaluated in δ , v
produce the values in γ , v
.
substext : ∀ {Γ Δ v} {γ : Env Γ} {δ : Env Δ} → (σ : Subst Γ Δ) → δ `⊢ σ ↓ γ  → δ `, v `⊢ exts σ ↓ γ `, v substext σ d Z = var substext σ d (S x′) = renamepres S_ (λ _ → ⊑refl) (d x′)
The proof is by cases on the de Bruijn index x
.

If it is
Z
, then we need to show thatδ , v ⊢ # 0 ↓ v
, which we have by rulevar
. 
If it is
S x′
,then we need to show thatδ , v ⊢ rename S_ (σ x′) ↓ γ x′
, which we obtain by therenamepres
lemma.
With the extension lemma in hand, the proof that simultaneous substitution preserves meaning is straightforward. Let’s dive in!
substpres : ∀ {Γ Δ v} {γ : Env Γ} {δ : Env Δ} {M : Γ ⊢ ★} → (σ : Subst Γ Δ) → δ `⊢ σ ↓ γ → γ ⊢ M ↓ v  → δ ⊢ subst σ M ↓ v substpres σ s (var {x = x}) = (s x) substpres σ s (↦elim d₁ d₂) = ↦elim (substpres σ s d₁) (substpres σ s d₂) substpres σ s (↦intro d) = ↦intro (substpres (λ {A} → exts σ) (substext σ s) d) substpres σ s ⊥intro = ⊥intro substpres σ s (⊔intro d₁ d₂) = ⊔intro (substpres σ s d₁) (substpres σ s d₂) substpres σ s (sub d lt) = sub (substpres σ s d) lt
The proof is by induction on the semantics of M
. The two interesting
cases are for variables and lambda abstractions.

For a variable
x
, we have thatv ⊑ γ x
and we need to show thatδ ⊢ σ x ↓ v
. From the premise applied tox
, we have thatδ ⊢ σ x ↓ γ x
, so we conclude by thesub
rule. 
For a lambda abstraction, we must extend the substitution for the induction hypothesis. We apply the
substext
lemma to show that the extended substitution maps variables to terms that result in the appropriate values.
Single substitution preserves denotations
For β reduction, (ƛ N) · M —→ N [ M ]
, we need to show that the
semantics is preserved when substituting M
for de Bruijn index 0 in
term N
. By inversion on the rules ↦elim
and ↦intro
,
we have that γ , v ⊢ M ↓ w
and γ ⊢ N ↓ v
.
So we need to show that γ ⊢ M [ N ] ↓ w
, or equivalently,
that γ ⊢ subst (substzero N) M ↓ w
.
substitution : ∀ {Γ} {γ : Env Γ} {N M v w} → γ `, v ⊢ N ↓ w → γ ⊢ M ↓ v  → γ ⊢ N [ M ] ↓ w substitution{Γ}{γ}{N}{M}{v}{w} dn dm = substpres (substzero M) subzok dn where subzok : γ `⊢ substzero M ↓ (γ `, v) subzok Z = dm subzok (S x) = var
This result is a corollary of the lemma for simultaneous substitution.
To use the lemma, we just need to show that substzero M
maps
variables to terms that produces the same values as those in γ , v
.
Let y
be an arbitrary variable (de Bruijn index).

If it is
Z
, then(substzero M) y = M
and(γ , v) y = v
. By the premise we conclude thatγ ⊢ M ↓ v
. 
If it is
S x
, then(substzero M) (S x) = x
and(γ , v) (S x) = γ x
. So we conclude thatγ ⊢ x ↓ γ x
by rulevar
.
Reduction preserves denotations
With the substitution lemma in hand, it is straightforward to prove that reduction preserves denotations.
preserve : ∀ {Γ} {γ : Env Γ} {M N v} → γ ⊢ M ↓ v → M —→ N  → γ ⊢ N ↓ v preserve (var) () preserve (↦elim d₁ d₂) (ξ₁ r) = ↦elim (preserve d₁ r) d₂ preserve (↦elim d₁ d₂) (ξ₂ r) = ↦elim d₁ (preserve d₂ r) preserve (↦elim d₁ d₂) β = substitution (lambdainversion d₁) d₂ preserve (↦intro d) (ζ r) = ↦intro (preserve d r) preserve ⊥intro r = ⊥intro preserve (⊔intro d d₁) r = ⊔intro (preserve d r) (preserve d₁ r) preserve (sub d lt) r = sub (preserve d r) lt
We proceed by induction on the semantics of M
with case analysis on
the reduction.

If
M
is a variable, then there is no such reduction. 
If
M
is an application, then the reduction is either a congruence (ξ₁ or ξ₂) or β. For each congruence, we use the induction hypothesis. For β reduction we use the substitution lemma and thesub
rule. 
The rest of the cases are straightforward.
Reduction reflects denotations
This section proves that reduction reflects the denotation of a
term. That is, if N
results in v
, and if M
reduces to N
, then
M
also results in v
. While there are some broad similarities
between this proof and the above proof of semantic preservation, we
shall require a few more technical lemmas to obtain this result.
The main challenge is dealing with the substitution in β reduction:
(ƛ N) · M —→ N [ M ]
We have that γ ⊢ N [ M ] ↓ v
and need to show that
γ ⊢ (ƛ N) · M ↓ v
. Now consider the derivation of γ ⊢ N [ M ] ↓ v
.
The term M
may occur 0, 1, or many times inside N [ M ]
. At each of
those occurences, M
may result in a different value. But to build a
derivation for (ƛ N) · M
, we need a single value for M
. If M
occured more than 1 time, then we can join all of the different values
using ⊔
. If M
occured 0 times, then we do not need any information
about M
and can therefore use ⊥
for the value of M
.
Renaming reflects meaning
Previously we showed that renaming variables preserves meaning. Now
we prove the opposite, that it reflects meaning. That is,
if δ ⊢ rename ρ M ↓ v
, then γ ⊢ M ↓ v
, where (δ ∘ ρ)
⊑ γ`.
First, we need a variant of a lemma given earlier.
ext⊑′ : ∀ {Γ Δ v} {γ : Env Γ} {δ : Env Δ} → (ρ : Rename Γ Δ) → (δ ∘ ρ) `⊑ γ  → ((δ `, v) ∘ ext ρ) `⊑ (γ `, v) ext⊑′ ρ lt Z = ⊑refl ext⊑′ ρ lt (S x) = lt x
The proof is then as follows.
renamereflect : ∀ {Γ Δ v} {γ : Env Γ} {δ : Env Δ} { M : Γ ⊢ ★} → {ρ : Rename Γ Δ} → (δ ∘ ρ) `⊑ γ → δ ⊢ rename ρ M ↓ v  → γ ⊢ M ↓ v renamereflect {M = ` x} alln d with varinv d ...  lt = sub var (⊑trans lt (alln x)) renamereflect {M = ƛ N}{ρ = ρ} alln (↦intro d) = ↦intro (renamereflect (ext⊑′ ρ alln) d) renamereflect {M = ƛ N} alln ⊥intro = ⊥intro renamereflect {M = ƛ N} alln (⊔intro d₁ d₂) = ⊔intro (renamereflect alln d₁) (renamereflect alln d₂) renamereflect {M = ƛ N} alln (sub d₁ lt) = sub (renamereflect alln d₁) lt renamereflect {M = L · M} alln (↦elim d₁ d₂) = ↦elim (renamereflect alln d₁) (renamereflect alln d₂) renamereflect {M = L · M} alln ⊥intro = ⊥intro renamereflect {M = L · M} alln (⊔intro d₁ d₂) = ⊔intro (renamereflect alln d₁) (renamereflect alln d₂) renamereflect {M = L · M} alln (sub d₁ lt) = sub (renamereflect alln d₁) lt
We cannot prove this lemma by induction on the derivation of
δ ⊢ rename ρ M ↓ v
, so instead we proceed by induction on M
.

If it is a variable, we apply the inversion lemma to obtain that
v ⊑ δ (ρ x)
. Instantiating the premise tox
we haveδ (ρ x) = γ x
, so we conclude by thevar
rule. 
If it is a lambda abstraction
ƛ N
, we have renameρ (ƛ N) = ƛ (rename (ext ρ) N)
. We proceed by cases onδ ⊢ ƛ (rename (ext ρ) N) ↓ v
.
Rule
↦intro
: To satisfy the premise of the induction hypothesis, we prove that the renaming can be extended to be a mapping fromγ , v₁ to δ , v₁
. 
Rule
⊥intro
: We simply apply⊥intro
. 
Rule
⊔intro
: We apply the induction hypotheses and⊔intro
. 
Rule
sub
: We apply the induction hypothesis andsub
.


If it is an application
L · M
, we haverename ρ (L · M) = (rename ρ L) · (rename ρ M)
. We proceed by cases onδ ⊢ (rename ρ L) · (rename ρ M) ↓ v
and all the cases are straightforward.
In the upcoming uses of renamereflect
, the renaming will always be
the increment function. So we prove a corollary for that special case.
renameincreflect : ∀ {Γ v′ v} {γ : Env Γ} { M : Γ ⊢ ★} → (γ `, v′) ⊢ rename S_ M ↓ v  → γ ⊢ M ↓ v renameincreflect d = renamereflect `⊑refl d
Substitution reflects denotations, the variable case
We are almost ready to begin proving that simultaneous substitution
reflects denotations. That is, if γ ⊢ (subst σ M) ↓ v
, then
γ ⊢ σ k ↓ δ k
and δ ⊢ M ↓ v
for any k
and some δ
.
We shall start with the case in which M
is a variable x
.
So instead the premise is γ ⊢ σ x ↓ v
and we need to show that
δ ⊢ x ↓ v
for some δ
. The δ
that we choose shall be the
environment that maps x
to v
and every other variable to ⊥
.
Next we define the environment that maps x
to v
and every other
variable to ⊥
, that is constenv x v
. To tell variables apart, we
define the following function for deciding equality of variables.
_var≟_ : ∀ {Γ} → (x y : Γ ∋ ★) → Dec (x ≡ y) Z var≟ Z = yes refl Z var≟ (S _) = no λ() (S _) var≟ Z = no λ() (S x) var≟ (S y) with x var≟ y ...  yes refl = yes refl ...  no neq = no λ{refl → neq refl} var≟refl : ∀ {Γ} (x : Γ ∋ ★) → (x var≟ x) ≡ yes refl var≟refl Z = refl var≟refl (S x) rewrite var≟refl x = refl
Now we use var≟
to define constenv
.
constenv : ∀{Γ} → (x : Γ ∋ ★) → Value → Env Γ constenv x v y with x var≟ y ...  yes _ = v ...  no _ = ⊥
Of course, constenv x v
maps x
to value v
sameconstenv : ∀{Γ} {x : Γ ∋ ★} {v} → (constenv x v) x ≡ v sameconstenv {x = x} rewrite var≟refl x = refl
and constenv x v
maps y
to ⊥, so long as
x ≢ y`.
diffconstenv : ∀{Γ} {x y : Γ ∋ ★} {v} → x ≢ y  → constenv x v y ≡ ⊥ diffconstenv {Γ} {x} {y} neq with x var≟ y ...  yes eq = ⊥elim (neq eq) ...  no _ = refl
So we choose constenv x v
for δ
and obtain δ ⊢ x ↓ v
with the var
rule.
It remains to prove that γ ⊢ σ ↓ δ
and δ ⊢ M ↓ v
for any k
, given that
we have chosen constenv x v
for δ
. We shall have two cases to
consider, x ≡ y
or x ≢ y
.
Now to finish the two cases of the proof.
 In the case where
x ≡ y
, we need to show thatγ ⊢ σ y ↓ v
, but that’s just our premise.  In the case where
x ≢ y,
we need to show thatγ ⊢ σ y ↓ ⊥
, which we do via rule⊥intro
.
Thus, we have completed the variable case of the proof that simultaneous substitution reflects denotations. Here is the proof again, formally.
substreflectvar : ∀ {Γ Δ} {γ : Env Δ} {x : Γ ∋ ★} {v} {σ : Subst Γ Δ} → γ ⊢ σ x ↓ v  → Σ[ δ ∈ Env Γ ] γ `⊢ σ ↓ δ × δ ⊢ ` x ↓ v substreflectvar {Γ}{Δ}{γ}{x}{v}{σ} xv rewrite sym (sameconstenv {Γ}{x}{v}) = ⟨ constenv x v , ⟨ constenvok , var ⟩ ⟩ where constenvok : γ `⊢ σ ↓ constenv x v constenvok y with x var≟ y ...  yes x≡y rewrite sym x≡y  sameconstenv {Γ}{x}{v} = xv ...  no x≢y rewrite diffconstenv {Γ}{x}{y}{v} x≢y = ⊥intro
Substitutions and environment construction
Every substitution produces terms that can evaluate to ⊥
.
subst⊥ : ∀{Γ Δ}{γ : Env Δ}{σ : Subst Γ Δ}  → γ `⊢ σ ↓ `⊥ subst⊥ x = ⊥intro
If a substitution produces terms that evaluate to the values in
both γ₁
and γ₂
, then those terms also evaluate to the values in
γ₁ ⊔ γ₂
.
subst⊔ : ∀{Γ Δ}{γ : Env Δ}{γ₁ γ₂ : Env Γ}{σ : Subst Γ Δ} → γ `⊢ σ ↓ γ₁ → γ `⊢ σ ↓ γ₂  → γ `⊢ σ ↓ (γ₁ `⊔ γ₂) subst⊔ γ₁ok γ₂ok x = ⊔intro (γ₁ok x) (γ₂ok x)
The Lambda constructor is injective
lambdainj : ∀ {Γ} {M N : Γ , ★ ⊢ ★ } → _≡_ {A = Γ ⊢ ★} (ƛ M) (ƛ N)  → M ≡ N lambdainj refl = refl
Simultaneous substitution reflects denotations
In this section we prove a central lemma, that
substitution reflects denotations. That is, if γ ⊢ subst σ M ↓ v
, then
δ ⊢ M ↓ v
and γ ⊢ σ ↓ δ
for some δ
. We shall proceed by induction on
the derivation of γ ⊢ subst σ M ↓ v
. This requires a minor
restatement of the lemma, changing the premise to γ ⊢ L ↓ v
and
L ≡ subst σ M
.
split : ∀ {Γ} {M : Γ , ★ ⊢ ★} {δ : Env (Γ , ★)} {v} → δ ⊢ M ↓ v  → (init δ `, last δ) ⊢ M ↓ v split {δ = δ} δMv rewrite initlast δ = δMv substreflect : ∀ {Γ Δ} {δ : Env Δ} {M : Γ ⊢ ★} {v} {L : Δ ⊢ ★} {σ : Subst Γ Δ} → δ ⊢ L ↓ v → subst σ M ≡ L  → Σ[ γ ∈ Env Γ ] δ `⊢ σ ↓ γ × γ ⊢ M ↓ v substreflect {M = M}{σ = σ} (var {x = y}) eqL with M ...  ` x with var {x = y} ...  yv rewrite sym eqL = substreflectvar {σ = σ} yv substreflect {M = M} (var {x = y}) ()  M₁ · M₂ substreflect {M = M} (var {x = y}) ()  ƛ M′ substreflect {M = M}{σ = σ} (↦elim d₁ d₂) eqL with M ...  ` x with ↦elim d₁ d₂ ...  d′ rewrite sym eqL = substreflectvar {σ = σ} d′ substreflect (↦elim d₁ d₂) ()  ƛ M′ substreflect{Γ}{Δ}{γ}{σ = σ} (↦elim d₁ d₂) refl  M₁ · M₂ with substreflect {M = M₁} d₁ refl  substreflect {M = M₂} d₂ refl ...  ⟨ δ₁ , ⟨ substδ₁ , m1 ⟩ ⟩  ⟨ δ₂ , ⟨ substδ₂ , m2 ⟩ ⟩ = ⟨ δ₁ `⊔ δ₂ , ⟨ subst⊔ {γ₁ = δ₁}{γ₂ = δ₂}{σ = σ} substδ₁ substδ₂ , ↦elim (⊑env m1 (⊑envconjR1 δ₁ δ₂)) (⊑env m2 (⊑envconjR2 δ₁ δ₂)) ⟩ ⟩ substreflect {M = M}{σ = σ} (↦intro d) eqL with M ...  ` x with (↦intro d) ...  d′ rewrite sym eqL = substreflectvar {σ = σ} d′ substreflect {σ = σ} (↦intro d) eq  ƛ M′ with substreflect {σ = exts σ} d (lambdainj eq) ...  ⟨ δ′ , ⟨ extsσδ′ , m′ ⟩ ⟩ = ⟨ init δ′ , ⟨ ((λ x → renameincreflect (extsσδ′ (S x)))) , ↦intro (upenv (split m′) (varinv (extsσδ′ Z))) ⟩ ⟩ substreflect (↦intro d) ()  M₁ · M₂ substreflect {σ = σ} ⊥intro eq = ⟨ `⊥ , ⟨ subst⊥ {σ = σ} , ⊥intro ⟩ ⟩ substreflect {σ = σ} (⊔intro d₁ d₂) eq with substreflect {σ = σ} d₁ eq  substreflect {σ = σ} d₂ eq ...  ⟨ δ₁ , ⟨ substδ₁ , m1 ⟩ ⟩  ⟨ δ₂ , ⟨ substδ₂ , m2 ⟩ ⟩ = ⟨ δ₁ `⊔ δ₂ , ⟨ subst⊔ {γ₁ = δ₁}{γ₂ = δ₂}{σ = σ} substδ₁ substδ₂ , ⊔intro (⊑env m1 (⊑envconjR1 δ₁ δ₂)) (⊑env m2 (⊑envconjR2 δ₁ δ₂)) ⟩ ⟩ substreflect (sub d lt) eq with substreflect d eq ...  ⟨ δ , ⟨ substδ , m ⟩ ⟩ = ⟨ δ , ⟨ substδ , sub m lt ⟩ ⟩

Case
var
: We have substσ M ≡ y
, soM
must also be a variable, sayx
. We apply the lemmasubstreflectvar
to conclude.  Case
↦elim
: We havesubst σ M ≡ L₁ · L₂
. We proceed by cases onM
.
Case
M ≡ x
: We apply thesubstreflectvar
lemma again to conclude. 
Case
M ≡ M₁ · M₂
: By the induction hypothesis, we have someδ₁
andδ₂
such thatδ₁ ⊢ M₁ ↓ v₁ ↦ v₃
andγ ⊢ σ ↓ δ₁
, as well asδ₂ ⊢ M₂ ↓ v₁
andγ ⊢ σ ↓ δ₂
. By⊑env
we haveδ₁ ⊔ δ₂ ⊢ M₁ ↓ v₁ ↦ v₃
andδ₁ ⊔ δ₂ ⊢ M₂ ↓ v₁
(using⊑envconjR1
and⊑envconjR2
), and thereforeδ₁ ⊔ δ₂ ⊢ M₁ · M₂ ↓ v₃
. We conclude this case by obtainingγ ⊢ σ ↓ δ₁ ⊔ δ₂
by thesubst⊔
lemma.

 Case
↦intro
: We havesubst σ M ≡ ƛ L′
. We proceed by cases onM
.
Case
M ≡ x
: We apply thesubstreflectvar
lemma. 
Case
M ≡ ƛ M′
: By the induction hypothesis, we have(δ′ , v′) ⊢ M′ ↓ v₂
and(δ , v₁) ⊢ exts σ ↓ (δ′ , v′)
. From the later we have(δ , v₁) ⊢ # 0 ↓ v′
. By the lemmavarinv
we havev′ ⊑ v₁
, so by theupenv
lemma we have(δ′ , v₁) ⊢ M′ ↓ v₂
and thereforeδ′ ⊢ ƛ M′ ↓ v₁ → v₂
. We also need to show thatδ
⊢ σ ↓ δ′. Fix
k. We have
(δ , v₁) ⊢ rename S_ σ k ↓ δ k′. We then apply the lemma
renameincreflectto obtain
δ ⊢ σ k ↓ δ k′`, so this case is complete.


Case
⊥intro
: We choose⊥
forδ
. We have⊥ ⊢ M ↓ ⊥
by⊥intro
. We haveδ ⊢ σ ↓ ⊥
by the lemmasubstempty
.  Case
⊔intro
: By the induction hypothesis we haveδ₁ ⊢ M ↓ v₁
,δ₂ ⊢ M ↓ v₂
,δ ⊢ σ ↓ δ₁
, andδ ⊢ σ ↓ δ₂
. We haveδ₁ ⊔ δ₂ ⊢ M ↓ v₁
andδ₁ ⊔ δ₂ ⊢ M ↓ v₂
by⊑env
with⊑envconjR1
and⊑envconjR2
. So by⊔intro
we haveδ₁ ⊔ δ₂ ⊢ M ↓ v₁ ⊔ v₂
. Bysubst⊔
we conclude thatδ ⊢ σ ↓ δ₁ ⊔ δ₂
.
Single substitution reflects denotations
Most of the work is now behind us. We have proved that simultaneous
substitution reflects denotations. Of course, β reduction uses single
substitution, so we need a corollary that proves that single
substitution reflects denotations. That is,
given terms N : (Γ , ★ ⊢ ★)
and M : (Γ ⊢ ★)
,
if γ ⊢ N [ M ] ↓ w
, then γ ⊢ M ↓ v
and (γ , v) ⊢ N ↓ w
for some value v
. We have N [ M ] = subst (substzero M) N
.
We first prove a lemma about substzero
, that if
δ ⊢ substzero M ↓ γ
, then
γ ⊑ (δ , w) × δ ⊢ M ↓ w
for some w
.
substzeroreflect : ∀ {Δ} {δ : Env Δ} {γ : Env (Δ , ★)} {M : Δ ⊢ ★} → δ `⊢ substzero M ↓ γ  → Σ[ w ∈ Value ] γ `⊑ (δ `, w) × δ ⊢ M ↓ w substzeroreflect {δ = δ} {γ = γ} δσγ = ⟨ last γ , ⟨ lemma , δσγ Z ⟩ ⟩ where lemma : γ `⊑ (δ `, last γ) lemma Z = ⊑refl lemma (S x) = varinv (δσγ (S x))
We choose w
to be the last value in γ
and we obtain δ ⊢ M ↓ w
by applying the premise to variable Z
. Finally, to prove
γ ⊑ (δ , w)
, we prove a lemma by induction in the input variable.
The base case is trivial because of our choice of w
.
In the induction case, S x
, the premise
δ ⊢ substzero M ↓ γ
gives us δ ⊢ x ↓ γ (S x)
and then
using varinv
we conclude that γ (S x) ⊑ (δ
, w) (S x)`.
Now to prove that substitution reflects denotations.
substitutionreflect : ∀ {Δ} {δ : Env Δ} {N : Δ , ★ ⊢ ★} {M : Δ ⊢ ★} {v} → δ ⊢ N [ M ] ↓ v  → Σ[ w ∈ Value ] δ ⊢ M ↓ w × (δ `, w) ⊢ N ↓ v substitutionreflect d with substreflect d refl ...  ⟨ γ , ⟨ δσγ , γNv ⟩ ⟩ with substzeroreflect δσγ ...  ⟨ w , ⟨ ineq , δMw ⟩ ⟩ = ⟨ w , ⟨ δMw , ⊑env γNv ineq ⟩ ⟩
We apply the substreflect
lemma to obtain
δ ⊢ substzero M ↓ γ
and γ ⊢ N ↓ v
for some γ
.
Using the former, the substzeroreflect
lemma gives
us γ ⊑ (δ , w)
and δ ⊢ M ↓ w
. We conclude that
δ , w ⊢ N ↓ v
by applying the ⊑env
lemma, using
γ ⊢ N ↓ v
and γ ⊑ (δ , w)
.
Reduction reflects denotations
Now that we have proved that substitution reflects denotations, we can easily prove that reduction does too.
reflectbeta : ∀{Γ}{γ : Env Γ}{M N}{v} → γ ⊢ (N [ M ]) ↓ v → γ ⊢ (ƛ N) · M ↓ v reflectbeta d with substitutionreflect d ...  ⟨ v₂′ , ⟨ d₁′ , d₂′ ⟩ ⟩ = ↦elim (↦intro d₂′) d₁′ reflect : ∀ {Γ} {γ : Env Γ} {M M′ N v} → γ ⊢ N ↓ v → M —→ M′ → M′ ≡ N  → γ ⊢ M ↓ v reflect var (ξ₁ r) () reflect var (ξ₂ r) () reflect{γ = γ} (var{x = x}) β mn with var{γ = γ}{x = x} ...  d′ rewrite sym mn = reflectbeta d′ reflect var (ζ r) () reflect (↦elim d₁ d₂) (ξ₁ r) refl = ↦elim (reflect d₁ r refl) d₂ reflect (↦elim d₁ d₂) (ξ₂ r) refl = ↦elim d₁ (reflect d₂ r refl) reflect (↦elim d₁ d₂) β mn with ↦elim d₁ d₂ ...  d′ rewrite sym mn = reflectbeta d′ reflect (↦elim d₁ d₂) (ζ r) () reflect (↦intro d) (ξ₁ r) () reflect (↦intro d) (ξ₂ r) () reflect (↦intro d) β mn with ↦intro d ...  d′ rewrite sym mn = reflectbeta d′ reflect (↦intro d) (ζ r) refl = ↦intro (reflect d r refl) reflect ⊥intro r mn = ⊥intro reflect (⊔intro d₁ d₂) r mn rewrite sym mn = ⊔intro (reflect d₁ r refl) (reflect d₂ r refl) reflect (sub d lt) r mn = sub (reflect d r mn) lt
Reduction implies denotational equality
We have proved that reduction both preserves and reflects denotations. Thus, reduction implies denotational equality.
reduceequal : ∀ {Γ} {M : Γ ⊢ ★} {N : Γ ⊢ ★} → M —→ N  → ℰ M ≃ ℰ N reduceequal {Γ}{M}{N} r γ v = ⟨ (λ m → preserve m r) , (λ n → reflect n r refl) ⟩
We conclude with the soundness property, that multistep reduction to a lambda abstraction implies denotational equivalence with a lambda abstraction.
soundness : ∀{Γ} {M : Γ ⊢ ★} {N : Γ , ★ ⊢ ★} → M —↠ ƛ N  → ℰ M ≃ ℰ (ƛ N) soundness (.(ƛ _) ∎) γ v = ⟨ (λ x → x) , (λ x → x) ⟩ soundness {Γ} (L —→⟨ r ⟩ M—↠N) γ v = let ih = soundness M—↠N in let e = reduceequal r in ≃trans {Γ} e ih γ v
Unicode
This chapter uses the following unicode:
≟ U+225F QUESTIONED EQUAL TO (\?=)