Soundness: 指称语义归约的可靠性
module plfa.part3.Soundness where
简介
本章中我们会证明指称语义的归约语义是可靠（Sound）的，即对于任意项 L：
L —↠ ƛ N 蕴含 ℰ L ≃ ℰ (ƛ N)证明可通过对归约序列进行归纳得出，因此主引理涉及单个归约步骤。 我们需要证明，如果任何项 M 步进到项 N，则 M 和 M 的指称相等。 我们将分别证明「当且仅当」的两个方向，一个方向类似于保型性（type preservation）的证明， 另一个方向类似于反向归约（即展开）的保型性证明。回想一下， 保型性有时称为主体归约（subject reduction）。 反向的保型性是一个众所周知的属性，称为主体展开（subject expansion）。 众所周知，大多数类型化 λ-演算都不满足主体展开！ （译注：一个 subject 是形如 (1*2+3) : Int 这样已经确定类型的项。 大多数类型化 λ-演算会失去保型性的原因参见类型不变性。）
导入
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; sym; cong; cong₂; cong-app) 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; _[_]; subst-zero; ext; rename; exts; _—→_; ξ₁; ξ₂; β; ζ; _—↠_; _—→⟨_⟩_; _∎) open import plfa.part2.Substitution using (Rename; Subst; ids) open import plfa.part3.Denotational using (Value; ⊥; Env; _⊢_↓_; _`,_; _⊑_; _`⊑_; `⊥; _`⊔_; init; last; init-last; ⊑-refl; ⊑-trans; `⊑-refl; ⊑-env; ⊑-env-conj-R1; ⊑-env-conj-R2; up-env; var; ↦-elim; ↦-intro; ⊥-intro; ⊔-intro; sub; rename-pres; ℰ; _≃_; ≃-trans) open import plfa.part3.Compositional using (lambda-inversion; var-inv)
向前归约保持指称不变
本节中对指称不变性的证明使用了前一章中的技术。和 STLC 的不变性证明一样，我们保留了独立于语法定义的关系，这与内在类型项相反。 另一方面，我们对变量使用了 de Bruijn 索引。
证明的大纲保持不变，因为我们必须证明归约关系中使用的所有辅助函数的引理： 代换、重命名和扩展。
同时代换保持指称不变
我们接下来的目标是证明同时代换变量和环境会保持含义不变。也就是说，若 M 在环境 γ 中的结果是 v，那么代换 σ 应用到 M 所得的程序，其结果仍然是 v， 但环境转移到了 δ 中。该环境中对于每一个变量 x，σ x 产生的结果值与原始环境 γ 中的 x 的值相同。我们将这种情况写作 δ `⊢ σ ↓ γ。
infix 3 _`⊢_↓_ _`⊢_↓_ : ∀{Δ Γ} → Env Δ → Subst Γ Δ → Env Γ → Set _`⊢_↓_ {Δ}{Γ} δ σ γ = (∀ (x : Γ ∋ ★) → δ ⊢ σ x ↓ γ x)
和之前一样，为了证明 λ-抽象，我们需要证明一个扩展引理， 该引理说明了将 exts 函数应用于代换会产生一个新的代换，该代换将变量映射到项， 使得当对 δ , v 求值时会产生 γ , v 中的值。
subst-ext : ∀ {Γ Δ v} {γ : Env Γ} {δ : Env Δ} → (σ : Subst Γ Δ) → δ `⊢ σ ↓ γ -------------------------- → δ `, v `⊢ exts σ ↓ γ `, v subst-ext σ d Z = var subst-ext σ d (S x′) = rename-pres S_ (λ _ → ⊑-refl) (d x′)
该证明通过对 de Bruijn 索引 x 进行情况分析来论证：
若索引为
Z，那么我们需要证明δ , v ⊢ # 0 ↓ v， 它可通过规则var得证。若索引为
S x′那么我们需要证明δ , v ⊢ rename S_ (σ x′) ↓ γ x′， 它可通过rename-pres引理证明。
有了这个扩展引理，同时代换会保持含义不变的证明就很直白了，我们继续深入：
subst-pres : ∀ {Γ Δ v} {γ : Env Γ} {δ : Env Δ} {M : Γ ⊢ ★} → (σ : Subst Γ Δ) → δ `⊢ σ ↓ γ → γ ⊢ M ↓ v ------------------ → δ ⊢ subst σ M ↓ v subst-pres σ s (var {x = x}) = s x subst-pres σ s (↦-elim d₁ d₂) = ↦-elim (subst-pres σ s d₁) (subst-pres σ s d₂) subst-pres σ s (↦-intro d) = ↦-intro (subst-pres (λ {A} → exts σ) (subst-ext σ s) d) subst-pres σ s ⊥-intro = ⊥-intro subst-pres σ s (⊔-intro d₁ d₂) = ⊔-intro (subst-pres σ s d₁) (subst-pres σ s d₂) subst-pres σ s (sub d lt) = sub (subst-pres σ s d) lt
我们通过对 M 的语义进行归纳来证明。两个有趣的情况分别对应于变量和 λ-抽象：
对于变量
x，我们有v = γ x，于是需要证明δ ⊢ σ x ↓ v。 将前提应用到x，我们有δ ⊢ σ x ↓ γ x，即δ ⊢ σ x ↓ v.对于 λ-抽象，我们必须为归纳假设扩展代换。应用
subst-ext引理可证明扩展的代换会将变量映射到产生对应值的项。
单一代换保持指称不变
对于 β-规约 (ƛ N) · M —→ N [ M ]，我们需要证明当用 M 代换项 N 中的 de Bruijn 索引 0 时，语义保持不变。通过对规则 ↦-elim 和 ↦-intro 进行反演，我们可得到 γ , v ⊢ M ↓ w 和 γ ⊢ N ↓ v。因此，我们需要证明 γ ⊢ M [ N ] ↓ w，或等价地证明 γ ⊢ subst (subst-zero N) M ↓ w。
substitution : ∀ {Γ} {γ : Env Γ} {N M v w} → γ `, v ⊢ N ↓ w → γ ⊢ M ↓ v --------------- → γ ⊢ N [ M ] ↓ w substitution{Γ}{γ}{N}{M}{v}{w} dn dm = subst-pres (subst-zero M) sub-z-ok dn where sub-z-ok : γ `⊢ subst-zero M ↓ (γ `, v) sub-z-ok Z = dm sub-z-ok (S x) = var
这个结果是同时代换引理的推论。要使用该引理，我们只需要证明 subst-zero M 会将变量映射到某个项，该项产生的值与 γ , v 中产生的值相同。令 y 为任意变量（即 de Bruijn 索引）：
若索引为
Z，则(subst-zero M) y = M且(γ , v) y = v， 根据前提可得γ ⊢ M ↓ v。若索引为
S x，则(subst-zero M) (S x) = x且(γ , v) (S x) = γ x， 根据规则var可得γ ⊢ x ↓ γ x。
归约保持指称不变
有了代换引理，就能直接证明归约保持指称不变：
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 (lambda-inversion 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
我们通过对 M 的语义进行归纳，并对归约进行情况分析来证明：
若
M为变量，则无需归约。若
M为应用，则归约要么满足合同性（ξ₁ 或 ξ₂），要么是 β-归约。 对于每一种合同性，我们使用归纳假设。对于 β-归约，我们使用代换引理和sub规则。其余的情况都很直白。
归约反映了指称不变
本节中将证明归约反映了项的指称不变，换言之，若 N 的结果是 v，且若 M 可归约为 N，则 M 的结果也是 v。虽然此证明和前面的语义保持不变的证明 之间存在一些广泛的相似之处，但我们仍需更多的技术引理才能得到这个结果。
最主要挑战是处理 β-归约中的代换：
(ƛ N) · M —→ N [ M ]我们有 γ ⊢ N [ M ] ↓ v 且需要证明 γ ⊢ (ƛ N) · M ↓ v。现在考虑 γ ⊢ N [ M ] ↓ v 的推导过程。项 M 在 N [ M ] 中可能会出现 0、1 或多次。 对于它可能出现的任意次数，M 都可能产生不同的值。不过为了构建出 (ƛ N) · M 的推导过程，我们需要单个的 M 值。若 M 出现了超过 1 次，那么我们就能将不同的值用 ⊔ 连接到一起。若 M 出现了 0 次，那么我们就无需任何关于 M 的信息， 并直接使用 ⊥ 作为 M 的值。
重命名反映了含义不变
首先，我们需要一个前面给出的引理的变体：
ext-`⊑ : ∀ {Γ Δ v} {γ : Env Γ} {δ : Env Δ} → (ρ : Rename Γ Δ) → (δ ∘ ρ) `⊑ γ ------------------------------ → ((δ `, v) ∘ ext ρ) `⊑ (γ `, v) ext-`⊑ ρ lt Z = ⊑-refl ext-`⊑ ρ lt (S x) = lt x
然后证明如下：
rename-reflect : ∀ {Γ Δ v} {γ : Env Γ} {δ : Env Δ} { M : Γ ⊢ ★} → {ρ : Rename Γ Δ} → (δ ∘ ρ) `⊑ γ → δ ⊢ rename ρ M ↓ v ------------------------------------ → γ ⊢ M ↓ v rename-reflect {M = ` x} all-n d with var-inv d ... | lt = sub var (⊑-trans lt (all-n x)) rename-reflect {M = ƛ N}{ρ = ρ} all-n (↦-intro d) = ↦-intro (rename-reflect (ext-`⊑ ρ all-n) d) rename-reflect {M = ƛ N} all-n ⊥-intro = ⊥-intro rename-reflect {M = ƛ N} all-n (⊔-intro d₁ d₂) = ⊔-intro (rename-reflect all-n d₁) (rename-reflect all-n d₂) rename-reflect {M = ƛ N} all-n (sub d₁ lt) = sub (rename-reflect all-n d₁) lt rename-reflect {M = L · M} all-n (↦-elim d₁ d₂) = ↦-elim (rename-reflect all-n d₁) (rename-reflect all-n d₂) rename-reflect {M = L · M} all-n ⊥-intro = ⊥-intro rename-reflect {M = L · M} all-n (⊔-intro d₁ d₂) = ⊔-intro (rename-reflect all-n d₁) (rename-reflect all-n d₂) rename-reflect {M = L · M} all-n (sub d₁ lt) = sub (rename-reflect all-n d₁) lt
我们无法通过对 δ ⊢ rename ρ M ↓ v 的推导过程进行归纳来证明此引理， 所以我们转而通过对 M 进行归纳来证明：
若它是一个变量，我们可通过对它应用反演引理得到
v ⊑ δ (ρ x)。 将前提实例化为x，我们有δ (ρ x) ⊑ γ x，于是我们可通过var规则证明。若它是一个 λ-抽象
ƛ N，我们有重命名ρ (ƛ N) = ƛ (rename (ext ρ) N)。 可通过对δ ⊢ ƛ (rename (ext ρ) N) ↓ v进行情况分析来论证：规则
↦-intro：为了满足归纳假设的前提，我们证明了重命名可扩展为从γ , v到δ , v的映射。规则
⊥-intro：直接应用⊥-intro。规则
⊔-intro：应用归纳假设和⊔-intro。规则
sub：应用归纳假设和sub。
若它是一个应用
L · M，我们有rename ρ (L · M) = (rename ρ L) · (rename ρ M)， 于是可通过对δ ⊢ (rename ρ L) · (rename ρ M) ↓ v进行情况分析来论证， 而所有的情况都很直白。
在以后使用 rename-reflect 的情况中，重命名始终都是增量函数， 于是我们先在这里为这些特殊情况证明以下推论：
rename-inc-reflect : ∀ {Γ v′ v} {γ : Env Γ} { M : Γ ⊢ ★} → (γ `, v′) ⊢ rename S_ M ↓ v ---------------------------- → γ ⊢ M ↓ v rename-inc-reflect d = rename-reflect `⊑-refl d
代换反映了指称不变：变量的情况
我们基本上准备好证明同时代换反映指称不变了，也就是说，若 γ ⊢ (subst σ M) ↓ v，则对于任意 k 和某些 δ，有 γ ⊢ σ k ↓ δ k 且 δ ⊢ M ↓ v。我们首先从 M 是一个变量 x 的情况开始， 已知前提是 γ ⊢ σ x ↓ v，我们需要证明对于某个 δ，有 δ ⊢ ` x ↓ v。 我们选择的环境 δ 应当将 x 映射到 v，将任何其他变量映射到 ⊥。
接下来我们定义将 x 映射到 v，将其他变量映射到 ⊥ 的环境，即 const-env x v。为了区分变量，我们定义以下函数来确定变量的相等性：
_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
接着我们用 var≟ 来定义 const-env：
const-env : ∀{Γ} → (x : Γ ∋ ★) → Value → Env Γ const-env x v y with x var≟ y ... | yes _ = v ... | no _ = ⊥
当然，const-env x v 将 x 映射到值 v：
same-const-env : ∀{Γ} {x : Γ ∋ ★} {v} → (const-env x v) x ≡ v same-const-env {x = x} rewrite var≟-refl x = refl
以及 const-env x v 将 y 映射到 ⊥，且 x ≢ y。
diff-const-env : ∀{Γ} {x y : Γ ∋ ★} {v} → x ≢ y ------------------- → const-env x v y ≡ ⊥ diff-const-env {Γ} {x} {y} neq with x var≟ y ... | yes eq = ⊥-elim (neq eq) ... | no _ = refl
于是我们为 δ 选择 const-env x v 并通过 var 规则得到了 δ ⊢ ` x ↓ v。
剩下的就是证明 γ `⊢ σ ↓ δ，以及对于任意 k 有 δ ⊢ M ↓ v，据此我们 就能为 δ 选择 const-env x v。我们有两种情况需要考虑：x ≡ y 或 x ≢ y。
现在完成该证明的两种情况：
- 对于
x ≡ y的情况，我们需要证明γ ⊢ σ y ↓ v，不过这就是我们的前提。 - 对于
x ≢ y,的情况， we need to show thatγ ⊢ σ y ↓ ⊥, which we do via rule⊥-intro.
这样，我们就完成了同时代换反映指称不变的证明中变量的情况。 以下是正式的证明：
subst-reflect-var : ∀ {Γ Δ} {γ : Env Δ} {x : Γ ∋ ★} {v} {σ : Subst Γ Δ} → γ ⊢ σ x ↓ v ----------------------------------------- → Σ[ δ ∈ Env Γ ] γ `⊢ σ ↓ δ × δ ⊢ ` x ↓ v subst-reflect-var {Γ}{Δ}{γ}{x}{v}{σ} xv rewrite sym (same-const-env {Γ}{x}{v}) = ⟨ const-env x v , ⟨ const-env-ok , var ⟩ ⟩ where const-env-ok : γ `⊢ σ ↓ const-env x v const-env-ok y with x var≟ y ... | yes x≡y rewrite sym x≡y | same-const-env {Γ}{x}{v} = xv ... | no x≢y rewrite diff-const-env {Γ}{x}{y}{v} x≢y = ⊥-intro
代换与环境的构造
每一个代换都能产生可求值为 ⊥ 的项。
subst-⊥ : ∀{Γ Δ}{γ : Env Δ}{σ : Subst Γ Δ} ----------------- → γ `⊢ σ ↓ `⊥ subst-⊥ x = ⊥-intro
若代换产生的项的求值结果为 γ₁ 或 γ₂ 中的值，那么这些项的求值结果也是 γ₁ ⊔ γ₂ 中的值。
subst-⊔ : ∀{Γ Δ}{γ : Env Δ}{γ₁ γ₂ : Env Γ}{σ : Subst Γ Δ} → γ `⊢ σ ↓ γ₁ → γ `⊢ σ ↓ γ₂ ------------------------- → γ `⊢ σ ↓ (γ₁ `⊔ γ₂) subst-⊔ γ₁-ok γ₂-ok x = ⊔-intro (γ₁-ok x) (γ₂-ok x)
λ 构造子是单射的
lambda-inj : ∀ {Γ} {M N : Γ , ★ ⊢ ★ } → _≡_ {A = Γ ⊢ ★} (ƛ M) (ƛ N) --------------------------- → M ≡ N lambda-inj refl = refl
同时代换反映了指称相等
本节中我们要证明一个核心引理，即代换反映了指称不变。也就是说，若 γ ⊢ subst σ M ↓ v，则 δ ⊢ M ↓ v 且对于某个 δ 有 γ `⊢ σ ↓ δ。 我们通过对 γ ⊢ subst σ M ↓ v 的推导过程进行归纳来证明， 为此需要稍微重述一下该引理，将前提更改为 γ ⊢ L ↓ v 和 L ≡ subst σ M。
split : ∀ {Γ} {M : Γ , ★ ⊢ ★} {δ : Env (Γ , ★)} {v} → δ ⊢ M ↓ v -------------------------- → (init δ `, last δ) ⊢ M ↓ v split {δ = δ} δMv rewrite init-last δ = δMv subst-reflect : ∀ {Γ Δ} {δ : Env Δ} {M : Γ ⊢ ★} {v} {L : Δ ⊢ ★} {σ : Subst Γ Δ} → δ ⊢ L ↓ v → subst σ M ≡ L --------------------------------------- → Σ[ γ ∈ Env Γ ] δ `⊢ σ ↓ γ × γ ⊢ M ↓ v subst-reflect {M = M}{σ = σ} (var {x = y}) eqL with M ... | ` x with var {x = y} ... | yv rewrite sym eqL = subst-reflect-var {σ = σ} yv subst-reflect {M = M} (var {x = y}) () | M₁ · M₂ subst-reflect {M = M} (var {x = y}) () | ƛ M′ subst-reflect {M = M}{σ = σ} (↦-elim d₁ d₂) eqL with M ... | ` x with ↦-elim d₁ d₂ ... | d′ rewrite sym eqL = subst-reflect-var {σ = σ} d′ subst-reflect (↦-elim d₁ d₂) () | ƛ M′ subst-reflect{Γ}{Δ}{γ}{σ = σ} (↦-elim d₁ d₂) refl | M₁ · M₂ with subst-reflect {M = M₁} d₁ refl | subst-reflect {M = M₂} d₂ refl ... | ⟨ δ₁ , ⟨ subst-δ₁ , m1 ⟩ ⟩ | ⟨ δ₂ , ⟨ subst-δ₂ , m2 ⟩ ⟩ = ⟨ δ₁ `⊔ δ₂ , ⟨ subst-⊔ {γ₁ = δ₁}{γ₂ = δ₂}{σ = σ} subst-δ₁ subst-δ₂ , ↦-elim (⊑-env m1 (⊑-env-conj-R1 δ₁ δ₂)) (⊑-env m2 (⊑-env-conj-R2 δ₁ δ₂)) ⟩ ⟩ subst-reflect {M = M}{σ = σ} (↦-intro d) eqL with M ... | ` x with (↦-intro d) ... | d′ rewrite sym eqL = subst-reflect-var {σ = σ} d′ subst-reflect {σ = σ} (↦-intro d) eq | ƛ M′ with subst-reflect {σ = exts σ} d (lambda-inj eq) ... | ⟨ δ′ , ⟨ exts-σ-δ′ , m′ ⟩ ⟩ = ⟨ init δ′ , ⟨ ((λ x → rename-inc-reflect (exts-σ-δ′ (S x)))) , ↦-intro (up-env (split m′) (var-inv (exts-σ-δ′ Z))) ⟩ ⟩ subst-reflect (↦-intro d) () | M₁ · M₂ subst-reflect {σ = σ} ⊥-intro eq = ⟨ `⊥ , ⟨ subst-⊥ {σ = σ} , ⊥-intro ⟩ ⟩ subst-reflect {σ = σ} (⊔-intro d₁ d₂) eq with subst-reflect {σ = σ} d₁ eq | subst-reflect {σ = σ} d₂ eq ... | ⟨ δ₁ , ⟨ subst-δ₁ , m1 ⟩ ⟩ | ⟨ δ₂ , ⟨ subst-δ₂ , m2 ⟩ ⟩ = ⟨ δ₁ `⊔ δ₂ , ⟨ subst-⊔ {γ₁ = δ₁}{γ₂ = δ₂}{σ = σ} subst-δ₁ subst-δ₂ , ⊔-intro (⊑-env m1 (⊑-env-conj-R1 δ₁ δ₂)) (⊑-env m2 (⊑-env-conj-R2 δ₁ δ₂)) ⟩ ⟩ subst-reflect (sub d lt) eq with subst-reflect d eq ... | ⟨ δ , ⟨ subst-δ , m ⟩ ⟩ = ⟨ δ , ⟨ subst-δ , sub m lt ⟩ ⟩
- 情况
var：我们有subst σ M ≡ y，因此M也必须是一个变量，称为x。 我们应用引理subst-reflect-var得出结论。
- 情况
↦-elim：我们有subst σ M ≡ L₁ · L₂，需要对M进行情况分析：情况
M ≡ ` x：我们再次应用subst-reflect-var得出结论。情况
M ≡ M₁ · M₂：根据归纳假设，我们有某个δ₁和δ₂使得δ₁ ⊢ M₁ ↓ v₁ ↦ v₃和γ `⊢ σ ↓ δ₁，以及δ₂ ⊢ M₂ ↓ v₁和γ `⊢ σ ↓ δ₂。 根据⊑-env我们有δ₁ ⊔ δ₂ ⊢ M₁ ↓ v₁ ↦ v₃和δ₁ ⊔ δ₂ ⊢ M₂ ↓ v₁（使用⊑-env-conj-R1和⊑-env-conj-R2得出），因此δ₁ ⊔ δ₂ ⊢ M₁ · M₂ ↓ v₃。 我们通过subst-⊔引理得出γ `⊢ σ ↓ δ₁ ⊔ δ₂从而证明此情况。
- 情况
↦-intro：我们有subst σ M ≡ ƛ L′，需要对M进行情况分析：情况
M ≡ x：我们应用subst-reflect-var引理。情况
M ≡ ƛ M′：根据归纳假设，我们有(δ′ , v′) ⊢ M′ ↓ v₂和(δ , v₁) ⊢ exts σ ↓ (δ′ , v′)。根据后者可得(δ , v₁) ⊢ # 0 ↓ v′。 根据引理var-inv我们有v′ ⊑ v₁，于是根据up-env引理我们有(δ′ , v₁) ⊢ M′ ↓ v₂，因此δ′ ⊢ ƛ M′ ↓ v₁ → v₂。我们还需要证明δ ⊢ σ ↓ δ′。固定k，我们有(δ , v₁) ⊢ rename S_ σ k ↓ δ k′， 接着应用引理rename-inc-reflect可得δ ⊢ σ k ↓ δ k′，于是此情况证明完毕。
- 情况
⊥-intro：我们为δ选择⊥。 根据⊥-intro我们有⊥ ⊢ M ↓ ⊥。 根据subst-⊥引理有δ `⊢ σ ↓ `⊥。
- 情况
⊔-intro：根据归纳假设我们有δ₁ ⊢ M ↓ v₁、δ₂ ⊢ M ↓ v₂、δ `⊢ σ ↓ δ₁和δ `⊢ σ ↓ δ₂。 根据⊑-env、⊑-env-conj-R1和⊑-env-conj-R2我们有δ₁ ⊔ δ₂ ⊢ M ↓ v₁和δ₁ ⊔ δ₂ ⊢ M ↓ v₂，因此根据⊔-intro可得δ₁ ⊔ δ₂ ⊢ M ↓ v₁ ⊔ v₂。 根据subst-⊔可得δ `⊢ σ ↓ δ₁ ⊔ δ₂。
单一代换反映了指称不变
现在大部分工作已经完成，我们已经证明了同时代换反映了指称不变。当然，β-归约使用单一代换， 因此我们需要一个推论来证明单一代换反映了指称不变。也就是说，给定项 N : (Γ , ★ ⊢ ★) 和 M : (Γ ⊢ ★)，若 γ ⊢ N [ M ] ↓ w，则对于某个值 v 有 γ ⊢ M ↓ v 且 ( γ , v) ⊢ N ↓ w 。于是我们有 N [ M ] = subst (subst-zero M) N。
我们首先证明一个关于 subst-zero 的引理，即若 δ ⊢ subst-zero M ↓ γ，则对某个值 w，有 γ `⊑ (δ , w) × δ ⊢ M ↓ w。
subst-zero-reflect : ∀ {Δ} {δ : Env Δ} {γ : Env (Δ , ★)} {M : Δ ⊢ ★} → δ `⊢ subst-zero M ↓ γ ---------------------------------------- → Σ[ w ∈ Value ] γ `⊑ (δ `, w) × δ ⊢ M ↓ w subst-zero-reflect {δ = δ} {γ = γ} δσγ = ⟨ last γ , ⟨ lemma , δσγ Z ⟩ ⟩ where lemma : γ `⊑ (δ `, last γ) lemma Z = ⊑-refl lemma (S x) = var-inv (δσγ (S x))
我们选择 w 作为 γ 中的最后一个值，通过将前提应用到 Z 可得 δ ⊢ M ↓ w。 最后，要证明 γ `⊑ (δ , w)，我们需要在输入项中通过归纳来证明一个引理。 由于我们选择了 w，因此基本的情况是平凡的。在归纳的情况中 S x 中， 前提 δ ⊢ subst-zero M ↓ γ 给出了 δ ⊢ x ↓ γ (S x)，接着使用 var-inv 可得 γ (S x) ⊑ (δ `, w) (S x)。
现在证明代换反映了指称不变：
substitution-reflect : ∀ {Δ} {δ : Env Δ} {N : Δ , ★ ⊢ ★} {M : Δ ⊢ ★} {v} → δ ⊢ N [ M ] ↓ v ------------------------------------------------ → Σ[ w ∈ Value ] δ ⊢ M ↓ w × (δ `, w) ⊢ N ↓ v substitution-reflect d with subst-reflect d refl ... | ⟨ γ , ⟨ δσγ , γNv ⟩ ⟩ with subst-zero-reflect δσγ ... | ⟨ w , ⟨ ineq , δMw ⟩ ⟩ = ⟨ w , ⟨ δMw , ⊑-env γNv ineq ⟩ ⟩
我们应用 subst-reflect 引理可得对于某个 γ 有 δ ⊢ subst-zero M ↓ γ 和 γ ⊢ N ↓ v。通过使用前者，subst-zero-reflect 给出了 γ `⊑ (δ , w) 和 δ ⊢ M ↓ w。我们通过应用 ⊑-env 引理，使用 γ ⊢ N ↓ v 和 γ `⊑ (δ , w) 可得 δ , w ⊢ N ↓ v。
归约反映了指称不变
现在我们已经证明了代换反映了指称不变，可以很容易地证明归约也拥有此性质：
reflect-beta : ∀{Γ}{γ : Env Γ}{M N}{v} → γ ⊢ (N [ M ]) ↓ v → γ ⊢ (ƛ N) · M ↓ v reflect-beta d with substitution-reflect 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 = reflect-beta 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 = reflect-beta 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 = reflect-beta 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
归约蕴含指称等价
我们已经证明了归约保持并反映了指称不变，因此归约蕴含指称等价：
reduce-equal : ∀ {Γ} {M : Γ ⊢ ★} {N : Γ ⊢ ★} → M —→ N --------- → ℰ M ≃ ℰ N reduce-equal {Γ}{M}{N} r γ v = ⟨ (λ m → preserve m r) , (λ n → reflect n r refl) ⟩
最终我们就得到了可靠性（Soundness Property），即多步归约到一个 λ-抽象，蕴含指称等价于该 λ-抽象。
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 = reduce-equal r in ≃-trans {Γ} e ih γ v
Unicode
本章使用了以下 Unicode：
≟ U+225F QUESTIONED EQUAL TO (\?=)