module plfa.part3.Denotational where

λ-演算是一种关于函数的语言，即从输入到输出的映射。在计算中， 我们通常认为这种映射是通过一系列将输入转换为输出的操作来执行的。 但函数也可以表示为数据。例如，可以将函数表格化，即创建一个表， 其中每行都有两个条目：一个输入和一个该函数对应的输出。 函数应用则是查找给定输入的行并读取输出的过程。

我们可按照「函数即表格」的思想为无类型 λ-演算创建语义。然而却碰上了两个难点： 首先，函数的定义域通常是无穷的，因此我们似乎需要无限长的表格来表示函数。 其次，在 λ-演算中，函数可应用于函数，它们甚至可以应用于自身！ 因而这些表格可能包含循环引用。你可能会担心需要高级技术来解决这些问题， 幸而情况并非如此！

第一个问题是带有无穷定义域的函数。注意到每一个 λ-抽象只会应用于数量有限的不同参数， 该问题因而得以解决（我们回头再讨论发散的程序）。这是看待 Dana Scott 见解的另一种方式，即对 λ-演算进行建模只需要用到连续函数。

第二个问题是自应用，可以通过放宽在函数表格中查找参数的方式来解决。 通常，人们会在表中查找输入条目与参数完全匹配的行。在自应用的情况下， 这样会要求表包含其自身的副本，当然这是不可能的 （至少，想要使用归纳数据类型定义来构建表是不可能的，而这就是我们要做的）。 其实只要找到一个输入，使得每一行输入都对应到一行参数（即，输入是参数的子集）。 在自应用的情况下，表只需要包含其自身的较小副本，这样就好了。

基于这两点观察，我们就能直接写出 λ-演算的指称语义。

导入

open import Data.Nat.Base using (ℕ; zero; suc)
open import Data.Product.Base using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; proj₂)
  renaming (_,_ to ⟨_,_⟩)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
open import Data.Vec.Base using (Vec; []; _∷_)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl)
open import Relation.Nullary.Negation using (¬_; contradiction)
open import Function.Base using (_∘_)
open import plfa.part2.Untyped
  using (Context; ★; _∋_; ∅; _,_; Z; S_; _⊢_; `_; _·_; ƛ_;
         #_; twoᶜ; ext; rename; exts; subst; subst-zero; _[_])
open import plfa.part2.Substitution using (Rename; extensionality; rename-id)

值

值数据类型 Value 表示函数的有限的一部分。我们将值视为表示「输入-输出」 映射的有限序对集合。Value 数据类型将集合表示为二叉树，其内部节点是并集运算符， 叶子节点表示单个映射或空集。

  • ⊥ 值不提供有关计算的信息。

  • 形如 v ↦ w 的值是从输入 v 到输出 w 的单个输入-输出映射。

  • 形如 v ⊔ w 的值是根据 v 和 w 将输入映射到输出的函数。 可将其视为两个集合的并集。

infixr 7 _↦_
infixl 5 _⊔_

data Value : Set where
  ⊥ : Value
  _↦_ : Value → Value → Value
  _⊔_ : Value → Value → Value

关系 ⊑ 将熟悉的子集概念适配到 Value 数据类型上。 这种关系在实现自我应用方面起到了关键作用。有两个特定于函数的规则 ⊑-fun 和 ⊑-dist，我们将在后面讨论。

infix 4 _⊑_

data _⊑_ : Value → Value → Set where

  ⊑-bot : ∀ {v} → ⊥ ⊑ v

  ⊑-conj-L : ∀ {u v w}
    → v ⊑ u
    → w ⊑ u
      -----------
    → (v ⊔ w) ⊑ u

  ⊑-conj-R1 : ∀ {u v w}
    → u ⊑ v
      -----------
    → u ⊑ (v ⊔ w)

  ⊑-conj-R2 : ∀ {u v w}
    → u ⊑ w
      -----------
    → u ⊑ (v ⊔ w)

  ⊑-trans : ∀ {u v w}
    → u ⊑ v
    → v ⊑ w
      -----
    → u ⊑ w

  ⊑-fun : ∀ {v w v′ w′}
    → v′ ⊑ v
    → w ⊑ w′
      -------------------
    → (v ↦ w) ⊑ (v′ ↦ w′)

  ⊑-dist : ∀{v w w′}
      ---------------------------------
    → v ↦ (w ⊔ w′) ⊑ (v ↦ w) ⊔ (v ↦ w′)

前五条规则很简单。规则 ⊑-fun 刻画了何时可以将高阶参数 v′ ↦ w′ 与输入为 v ↦ w 的表格条目相匹配。考虑一个高阶参数的调用，可以传入一个比预期更大的参数， 因此 v 可以大于 v′。此外，还可以忽略某些输出，因此 w 可以小于 w′。 （译注：即作为子类型的函数，其参数是逆变的，返回值是协变的。） 规则 ⊑-dist 表示，如果对同一个输入有两个条目相匹配， 则可以将它们合并成一个条目并连接两个输出。

⊑ 关系满足自反性：

⊑-refl : ∀ {v} → v ⊑ v
⊑-refl {⊥} = ⊑-bot
⊑-refl {v ↦ v′} = ⊑-fun ⊑-refl ⊑-refl
⊑-refl {v₁ ⊔ v₂} = ⊑-conj-L (⊑-conj-R1 ⊑-refl) (⊑-conj-R2 ⊑-refl)

⊔ 运算对 ⊑ 满足单调性，即给定两个较大的值，它会产生一个更大的值：

⊔⊑⊔ : ∀ {v w v′ w′}
  → v ⊑ v′  →  w ⊑ w′
    -----------------------
  → (v ⊔ w) ⊑ (v′ ⊔ w′)
⊔⊑⊔ d₁ d₂ = ⊑-conj-L (⊑-conj-R1 d₁) (⊑-conj-R2 d₂)

即使输入的值不相同，⊑-dist 规则也可用于合并两个条目。首先可以用 ⊔ 将两个输入合并起来，然后应用 ⊑-dist 规则来获得以下属性。

⊔↦⊔-dist : ∀{v v′ w w′ : Value}
  → (v ⊔ v′) ↦ (w ⊔ w′) ⊑ (v ↦ w) ⊔ (v′ ↦ w′)
⊔↦⊔-dist = ⊑-trans ⊑-dist (⊔⊑⊔ (⊑-fun (⊑-conj-R1 ⊑-refl) ⊑-refl)
                            (⊑-fun (⊑-conj-R2 ⊑-refl) ⊑-refl))

如果连接 u ⊔ v 小于另一个值 w，则 u 和 v 都小于 w：

⊔⊑-invL : ∀{u v w : Value}
  → u ⊔ v ⊑ w
    ---------
  → u ⊑ w
⊔⊑-invL (⊑-conj-L lt1 lt2) = lt1
⊔⊑-invL (⊑-conj-R1 lt) = ⊑-conj-R1 (⊔⊑-invL lt)
⊔⊑-invL (⊑-conj-R2 lt) = ⊑-conj-R2 (⊔⊑-invL lt)
⊔⊑-invL (⊑-trans lt1 lt2) = ⊑-trans (⊔⊑-invL lt1) lt2

⊔⊑-invR : ∀{u v w : Value}
  → u ⊔ v ⊑ w
    ---------
  → v ⊑ w
⊔⊑-invR (⊑-conj-L lt1 lt2) = lt2
⊔⊑-invR (⊑-conj-R1 lt) = ⊑-conj-R1 (⊔⊑-invR lt)
⊔⊑-invR (⊑-conj-R2 lt) = ⊑-conj-R2 (⊔⊑-invR lt)
⊔⊑-invR (⊑-trans lt1 lt2) = ⊑-trans (⊔⊑-invR lt1) lt2

环境

环境通过将变量映射到值来为项中的自由变量赋予含义：

Env : Context → Set
Env Γ = ∀ (x : Γ ∋ ★) → Value

我们有空环境，且可以扩展环境：

`∅ : Env ∅
`∅ ()

infixl 5 _`,_

_`,_ : ∀ {Γ} → Env Γ → Value → Env (Γ , ★)
(γ `, v) Z = v
(γ `, v) (S x) = γ x

我们可以从扩展的环境中恢复以前的环境以及最后添加的值。 将它们再次合并在一起能让我们回到开始：

init : ∀ {Γ} → Env (Γ , ★) → Env Γ
init γ x = γ (S x)

last : ∀ {Γ} → Env (Γ , ★) → Value
last γ = γ Z

init-last : ∀ {Γ} → (γ : Env (Γ , ★)) → γ ≡ (init γ `, last γ)
init-last {Γ} γ = extensionality lemma
  where lemma : ∀ (x : Γ , ★ ∋ ★) → γ x ≡ (init γ `, last γ) x
        lemma Z      =  refl
        lemma (S x)  =  refl

我们将 ⊑ 关系逐点（Point-wise）扩展到具有以下定义的环境：

_`⊑_ : ∀ {Γ} → Env Γ → Env Γ → Set
_`⊑_ {Γ} γ δ = ∀ (x : Γ ∋ ★) → γ x ⊑ δ x

我们定义了一个底环境和一个环境上的连接运算符，它接受它们的值的逐点连接：

`⊥ : ∀ {Γ} → Env Γ
`⊥ x = ⊥

_`⊔_ : ∀ {Γ} → Env Γ → Env Γ → Env Γ
(γ `⊔ δ) x = γ x ⊔ δ x

⊑-refl、⊑-conj-R1 和 ⊑-conj-R2 规则对环境也适用，因此两个环境 γ 和 δ 的连接大于第一个环境 γ 或第二个环境 δ：

`⊑-refl : ∀ {Γ} {γ : Env Γ} → γ `⊑ γ
`⊑-refl {Γ} {γ} x = ⊑-refl {γ x}

⊑-env-conj-R1 : ∀ {Γ} → (γ : Env Γ) → (δ : Env Γ) → γ `⊑ (γ `⊔ δ)
⊑-env-conj-R1 γ δ x = ⊑-conj-R1 ⊑-refl

⊑-env-conj-R2 : ∀ {Γ} → (γ : Env Γ) → (δ : Env Γ) → δ `⊑ (γ `⊔ δ)
⊑-env-conj-R2 γ δ x = ⊑-conj-R2 ⊑-refl

指称语义

我们用形如 ρ ⊢ M ↓ v 的判断来定义语义，其中 ρ 是环境，M 程序，v 是结果值。 对于熟悉大步语义的读者来说，这种表示法会感觉很自然，但不要让这种相似性欺骗了你。 二者之间存在细微但重要的差异！下面是语义的定义，我们将在后面的段落中详细讨论：

infix 3 _⊢_↓_

data _⊢_↓_ : ∀{Γ} → Env Γ → (Γ ⊢ ★) → Value → Set where

  var : ∀ {Γ} {γ : Env Γ} {x}
      ---------------
    → γ ⊢ (` x) ↓ γ x

  ↦-elim : ∀ {Γ} {γ : Env Γ} {L M v w}
    → γ ⊢ L ↓ (v ↦ w)
    → γ ⊢ M ↓ v
      ---------------
    → γ ⊢ (L · M) ↓ w

  ↦-intro : ∀ {Γ} {γ : Env Γ} {N v w}
    → γ `, v ⊢ N ↓ w
      -------------------
    → γ ⊢ (ƛ N) ↓ (v ↦ w)

  ⊥-intro : ∀ {Γ} {γ : Env Γ} {M}
      ---------
    → γ ⊢ M ↓ ⊥

  ⊔-intro : ∀ {Γ} {γ : Env Γ} {M v w}
    → γ ⊢ M ↓ v
    → γ ⊢ M ↓ w
      ---------------
    → γ ⊢ M ↓ (v ⊔ w)

  sub : ∀ {Γ} {γ : Env Γ} {M v w}
    → γ ⊢ M ↓ v
    → w ⊑ v
      ---------
    → γ ⊢ M ↓ w

考虑 λ-抽象的规则 ↦-intro，它表示 λ-抽象会生成一个单条目的表，该表将输入 v 映射到输出 w，前提是在 v 绑定到形参的环境中求值时会产生输出 w。 作为此规则的简单示例，我们可以看到恒等函数将 ⊥ 映射到 ⊥，同样也会将 ⊥ ↦ ⊥ 映射到 ⊥ ↦ ⊥：

id : ∅ ⊢ ★
id = ƛ # 0

denot-id1 : ∀ {γ} → γ ⊢ id ↓ ⊥ ↦ ⊥
denot-id1 = ↦-intro var

denot-id2 : ∀ {γ} → γ ⊢ id ↓ (⊥ ↦ ⊥) ↦ (⊥ ↦ ⊥)
denot-id2 = ↦-intro var

当然，我们需要多行表格来刻画 λ-抽象的含义。它们可以用 ⊔-intro 规则构建。如果项 M（通常是一个 λ-抽象）可以产生表格 v 和 w， 那么它也可以产生合并的表格 v ⊔ w。我们可以从操作的视角看待规则 ↦-intro 和 ⊔-intro。想象一下，当解释器首次遇到 λ-抽象时， 它会在许多随机选择的参数上预先对函数求值，使用多个 ↦-intro 规则的实例，然后再使用多个 ⊔-intro 规则将它们合并成一个大表格。 在接下来的内容中，我们将展示恒等函数产生一个包含上述两个结果的表格 ⊥ ↦ ⊥和(⊥ ↦ ⊥) ↦ (⊥ ↦ ⊥)。

denot-id3 : `∅ ⊢ id ↓ (⊥ ↦ ⊥) ⊔ (⊥ ↦ ⊥) ↦ (⊥ ↦ ⊥)
denot-id3 = ⊔-intro denot-id1 denot-id2

我们通常认为判断 γ ⊢ M ↓ v 以环境 γ 和项 M 为输入，产生结果 v。 然而重点在于，语义是一种关系。上述恒等函数的结果表明， 相同的环境和项可以映射为不同的结果。然而，对于给定的 γ 和 M ，它们的结果并不会有太大区别，毕竟它们都是同一个函数的有限近似。 或许考虑判断 γ ⊢ M ↓ v 更好的方法是将 γ、M 和 v 都视为输入， 其语义则是判定 v 是否为精确的环境 γ 中 M 的求值结果的部分描述。

接下来我们考虑 ↦-elim 规则给出的函数应用的含义。 以此规则为前提，我们有规则 L 将 v 映射到 w。 因此，如果 M 产生 v，那么将 L 应用于 M 会产生 w。

举一个函数应用和 ↦-elim 规则的例子，我们将恒等函数应用于自身。 实际上，我们有 ∅ ⊢ id ↓ (u ↦ u) ↦ (u ↦ u) 的同时还有 ∅ ⊢ id ↓ (u ↦ u)，因此我们可以应用规则 ↦-elim：

id-app-id : ∀ {u : Value} → `∅ ⊢ id · id ↓ (u ↦ u)
id-app-id {u} = ↦-elim (↦-intro var) (↦-intro var)

接着我们重新考虑丘奇数 2：λ f. λ u. (f (f u))。该函数有两个参数：f 和一个任意值 u，并将 f 应用两次。于是 f 必定将 u 映射到某个值， 我们将其命名为 v。接着，对于第二次应用，f 必定将 v 映射到某个值， 我们将其命名为 w。因此该函数的表格必定包含两个条目，即 u ↦ v 和 v ↦ w。 对于该表格的每一次应用，我们用 sub 规则提取对应的条目。具体来说， 就是用 ⊑-conj-R1 和 ⊑-conj-R2 从表格 u ↦ v ⊔ v ↦ w 中分别选出 u ↦ v 和 v ↦ w。所以 twoᶜ 的含义就是接受该表格和参数 u，然后返回 w。 实际上我们是通过以下过程把它推导出来的：

denot-twoᶜ : ∀{u v w : Value} → `∅ ⊢ twoᶜ ↓ ((u ↦ v ⊔ v ↦ w) ↦ u ↦ w)
denot-twoᶜ {u}{v}{w} =
  ↦-intro (↦-intro (↦-elim (sub var lt1) (↦-elim (sub var lt2) var)))
  where lt1 : v ↦ w ⊑ u ↦ v ⊔ v ↦ w
        lt1 = ⊑-conj-R2 (⊑-fun ⊑-refl ⊑-refl)

        lt2 : u ↦ v ⊑ u ↦ v ⊔ v ↦ w
        lt2 = (⊑-conj-R1 (⊑-fun ⊑-refl ⊑-refl))

接下来展示一个自应用的经典例子：Δ = λx. (x x)。 x 的输入值必须是一个表格，其中有一个条目将其自身较小的版本 v 映射到某个值 w，所以输入值类似于 v ↦ w ⊔ v。当然， Δ 的输出就是 w，推导过程如下所示。第一个 x 求值为 v ↦ w， 第二个 x 求值为 v，应用的结果为 w。

Δ : ∅ ⊢ ★
Δ = (ƛ (# 0) · (# 0))

denot-Δ : ∀ {v w} → `∅ ⊢ Δ ↓ ((v ↦ w ⊔ v) ↦ w)
denot-Δ = ↦-intro (↦-elim (sub var (⊑-conj-R1 ⊑-refl))
                          (sub var (⊑-conj-R2 ⊑-refl)))

你可能会担心这种语义是否可以处理发散的程序。值 ⊥ 和规则 ⊥-intro 提供了一种处理它们的方法（⊥-intro 规则也是 β-归约能够应用于不停机参数的原因）。 经典的 Ω 程序是一个特别简单的发散程序，它将 Δ 应用于自身，语义赋予 Ω 含义 ⊥。有多种方法可以得出它，我们将从使用 ⊔-intro 规则的方法开始。 首先，denot-Δ 告诉我们 Δ 的计算结果为 ((⊥ ↦ ⊥) ⊔ ⊥) ↦ ⊥（选择 v₁ = v2 = ⊥ ）。接着，Δ 还通过使用 ↦-intro 和 ⊥-intro 求值为 ⊥ ↦ ⊥，并通过 ⊥-intro 求值为 ⊥。正如我们之前所看到的， 只要我们能证明程序会求值出两个值，我们就能应用 ⊔-intro 将它们连接在一起， 于是 Δ 求值为 (⊥ ↦ ⊥) ⊔ ⊥，这与第一个 Δ 的输入相匹配， 因此可得应用的结果是 ⊥。

Ω : ∅ ⊢ ★
Ω = Δ · Δ

denot-Ω : `∅ ⊢ Ω ↓ ⊥
denot-Ω = ↦-elim denot-Δ (⊔-intro (↦-intro ⊥-intro) ⊥-intro)

同一结果的较短推导就是单纯使用 ⊥-intro 规则：

denot-Ω' : `∅ ⊢ Ω ↓ ⊥
denot-Ω' = ⊥-intro

仅凭对某个封闭项 M 可以推导出 ∅ ⊢ M ↓ ⊥ 并不意味着 M 必然发散。 可能还有其他可以推出 M 的推导过程，能产生包含更多信息的值。然而， 如果一个项求值的唯一结果是 ⊥，那么它确实发散。

细心的读者会发现，我们计划解决自应用问题的方式与实际应用的 ↦-elim 规则之间存在脱节。开头说过，我们会放宽查表的概念， 如果参数等于或大于输入条目，则允许参数匹配输入条目。然而，↦-elim 规则似乎需要精确匹配，但由于存在 sub 规则，应用确实可以允许更大的参数。

↦-elim2 : ∀ {Γ} {γ : Env Γ} {M₁ M₂ v₁ v₂ v₃}
  → γ ⊢ M₁ ↓ (v₁ ↦ v₃)
  → γ ⊢ M₂ ↓ v₂
  → v₁ ⊑ v₂
    ------------------
  → γ ⊢ (M₁ · M₂) ↓ v₃
↦-elim2 d₁ d₂ lt = ↦-elim d₁ (sub d₂ lt)

练习 denot-plusᶜ（实践）

plusᶜ 的指称是什么？即，找到一个值 v（排除 ⊥），使得 ∅ ⊢ plusᶜ ↓ v。 此外，对你选择的 v 给出 ∅ ⊢ plusᶜ ↓ v 的证明。

-- 请将代码写在此处

指称与指称相等

接下来我们基于上述语义来定义指称相等的概念，它的语句使用了「当且仅当」， 其定义如下

_iff_ : Set → Set → Set
P iff Q = (P → Q) × (Q → P)

看待指称语义的另一种方式是将它看作一个函数，它将项映射为一个从环境到值的关系， 即，项的指称（Denotation）是一个从环境到值的关系。

Denotation : Context → Set₁
Denotation Γ = (Env Γ → Value → Set)

下面的函数 ℰ 给出了语义的另一种视角，它相当于只改变了参数的顺序：

ℰ : ∀{Γ} → (M : Γ ⊢ ★) → Denotation Γ
ℰ M = λ γ v → γ ⊢ M ↓ v

一般来说，当两个指称在相同的环境中能够产生相同的值时，二者就是相等的。

infix 3 _≃_

_≃_ : ∀ {Γ} → (Denotation Γ) → (Denotation Γ) → Set
(_≃_ {Γ} D₁ D₂) = (γ : Env Γ) → (v : Value) → D₁ γ v iff D₂ γ v

指称相等是一种等价关系：

≃-refl : ∀ {Γ : Context} → {M : Denotation Γ}
  → M ≃ M
≃-refl γ v = ⟨ (λ x → x) , (λ x → x) ⟩

≃-sym : ∀ {Γ : Context} → {M N : Denotation Γ}
  → M ≃ N
    -----
  → N ≃ M
≃-sym eq γ v = ⟨ (proj₂ (eq γ v)) , (proj₁ (eq γ v)) ⟩

≃-trans : ∀ {Γ : Context} → {M₁ M₂ M₃ : Denotation Γ}
  → M₁ ≃ M₂
  → M₂ ≃ M₃
    -------
  → M₁ ≃ M₃
≃-trans eq1 eq2 γ v = ⟨ (λ z → proj₁ (eq2 γ v) (proj₁ (eq1 γ v) z)) ,
                        (λ z → proj₂ (eq1 γ v) (proj₂ (eq2 γ v) z)) ⟩

若两个项 M 和 N 的指称相等，我们就说它们是指称相等的，即 ℰ M ≃ ℰ N。

以下子模块引入了 ≃ 关系的等式推理：

module ≃-Reasoning {Γ : Context} where

  infix  1 start_
  infixr 2 _≃⟨⟩_ _≃⟨_⟩_
  infix  3 _☐

  start_ : ∀ {x y : Denotation Γ}
    → x ≃ y
      -----
    → x ≃ y
  start x≃y  =  x≃y

  _≃⟨_⟩_ : ∀ (x : Denotation Γ) {y z : Denotation Γ}
    → x ≃ y
    → y ≃ z
      -----
    → x ≃ z
  (x ≃⟨ x≃y ⟩ y≃z) =  ≃-trans x≃y y≃z

  _≃⟨⟩_ : ∀ (x : Denotation Γ) {y : Denotation Γ}
    → x ≃ y
      -----
    → x ≃ y
  x ≃⟨⟩ x≃y  =  x≃y

  _☐ : ∀ (x : Denotation Γ)
      -----
    → x ≃ x
  (x ☐)  =  ≃-refl

后续章节的路线图

后续章节证明了指称语义拥有几个期望的性质。首先我们证明了语义是可组合的， 即，一个项的指称是其子项的指称的函数。为此我们需要证明以下形式的等式：

ℰ (` x) ≃ ...
ℰ (ƛ M) ≃ ... ℰ M ...
ℰ (M · N) ≃ ... ℰ M ... ℰ N ...

组合性的性质并不平凡，因为我们定义的语义包含三个非语法制导的规则： ⊥-intro、⊔-intro 和 sub。上面的等式表明指称语义可以被定义为递归函数， 实际上，我们确实给出了这样的定义并证明它等价于 ℰ。

接下来我们研究指称语义和归约语义是否等价。回想一下，一个语言的语义的作用， 就是描述给定程序 M 的可观测行为。对于 λ-演算，我们可以做出多种选择， 但它们通常可以归结为一点信息：

  • 发散：程序 M 永远执行。
  • 停机：程序 M 停止。

我们可以用归约的项来刻画发散和停机：

  • 发散：对于任意项 N，有 ¬ (M —↠ ƛ N)。
  • 停机：对于某个项 N，有 M —↠ ƛ N 。

我们也可以用指称来刻画发散和停机：

  • 发散：对于任意 v 和 w，有 ¬ (∅ ⊢ M ↓ v ↦ w)。
  • 停机：对于某个 v 和 w，有 ∅ ⊢ M ↓ v ↦ w。

此外，我们还可以用指称函数 ℰ：

  • 发散：对于任意项 N，有 ¬ (ℰ M ≃ ℰ (ƛ N))。
  • 停机：对于某个项 N，有 ℰ M ≃ ℰ (ƛ N)。

所以问题在于归约语义和指称语义是否等价：

(∃ N. M —↠ ƛ N)  当且仅当  (∃ N. ℰ M ≃ ℰ (ƛ N))

我们将在第二章和第三章中讨论等价的每个方向。在第二章中，我们证明了 λ-抽象的归约蕴含 λ-抽象的指称相等。此性质在文献中被称为可靠性（Soundness）。

M —↠ ƛ N  蕴含  ℰ M ≃ ℰ (ƛ N)

在第三章中，我们证明了 λ-抽象的指称相等蕴含 λ-抽象的归约。 此性质在文献中被称为充分性（Adequacy）。

ℰ M ≃ ℰ (ƛ N)  蕴含 M —↠ ƛ N′ 对于某个 N′

第四章应用前三章的结果（组合性、可靠性和充分性）来证明指称相等蕴含一种称为 语境等价（Contextual Equivalence）的性质。这个性质很重要， 因为它保证了在证明程序变换（如性能优化）的正确性时使用指称相等的合理性。

我们会在本章剩下的部分中建立关于指称语义的一些基本结果， 所有这些性质的证明都依赖于此。我们先从一些关于重命名的引理开始， 它们与我们在前面的章节中见过的重命名引理非常相似。 我们以函数值小于关系的重要反演引理的证明作为结论。

重命名保持指称不变

我们将证明重命名变量并更改环境中对应的项仍能保持项的含义。 我们推广了重命名引理，以允许新环境中的值等于或大于原始值， 这种推广有助于证明归约蕴含了指称相等。

和以前一样，我们需要一个扩展引理来处理在 λ-抽象的情况下的证明。假设 ρ 是一个重命名，它将 γ 中的变量映射为 δ 中具有相等或更大值的变量。 这个引理说明了，扩展重命名会产生一个重命名 ext r，它将 γ , v 映射到 δ , v。

ext-⊑ : ∀ {Γ Δ v} {γ : Env Γ} {δ : Env Δ}
  → (ρ : Rename Γ Δ)
  → γ `⊑ (δ ∘ ρ)
    ------------------------------
  → (γ `, v) `⊑ ((δ `, v) ∘ ext ρ)
ext-⊑ ρ lt Z = ⊑-refl
ext-⊑ ρ lt (S n′) = lt n′

我们对 de Bruijn 索引 n 分情况来证明：

  • 若索引为 Z，那么我们只需证明 v ⊑ v，它根据 ⊑-refl 成立。

  • 若索引为 S n′，则目标简化为 γ n′ ⊑ δ (ρ n′)，它是前提的一个实例。

接着是重命名引理的证明。假设我们有一个重命名，它将 γ 中的变量映射为 δ 中具有相同值的变量。若在环境 γ 中 M 求值为 v，则对 M 应用重命名会生成一个程序，它在环境 δ 中求值会产生相同的值 v。

rename-pres : ∀ {Γ Δ v} {γ : Env Γ} {δ : Env Δ} {M : Γ ⊢ ★}
  → (ρ : Rename Γ Δ)
  → γ `⊑ (δ ∘ ρ)
  → γ ⊢ M ↓ v
    ---------------------
  → δ ⊢ (rename ρ M) ↓ v
rename-pres ρ lt (var {x = x}) = sub var (lt x)
rename-pres ρ lt (↦-elim d d₁) =
   ↦-elim (rename-pres ρ lt d) (rename-pres ρ lt d₁)
rename-pres ρ lt (↦-intro d) =
   ↦-intro (rename-pres (ext ρ) (ext-⊑ ρ lt) d)
rename-pres ρ lt ⊥-intro = ⊥-intro
rename-pres ρ lt (⊔-intro d d₁) =
   ⊔-intro (rename-pres ρ lt d) (rename-pres ρ lt d₁)
rename-pres ρ lt (sub d lt′) =
   sub (rename-pres ρ lt d) lt′

证明通过对 M 的语义进行归纳而得出。如你所见，除了变量和 λ-的情况外，其他情况都很简单。

  • 对于 x，我们根据前提来证明 γ x ⊑ δ (ρ x)。

  • 对于 λ-抽象，归纳假设需要我们扩展重命名。我们扩展了它并使用 ext-⊑ 引理来证明，扩展重命名会将变量映射到具有等价的值的变量。

环境增强与恒等重命名

我们还需要一个重命名引理的推论，即用更大（或更强）的环境替换当前环境， 并不会改变项 M 是否产生特定的值 v。具体来说，即若 γ ⊢ M ↓ v 且 γ ⊑ δ，则 δ ⊢ M ↓ v。那么这和重命名有何关联呢？ 它其实就是用恒等函数来重命名。我们以恒等重命名来应用重命名引理， 会得到 δ ⊢ rename (λ {A} x → x) M ↓ v，之后应用 rename-id 引理就会得到 δ ⊢ M ↓ v。

⊑-env : ∀ {Γ} {γ : Env Γ} {δ : Env Γ} {M v}
  → γ ⊢ M ↓ v
  → γ `⊑ δ
    ----------
  → δ ⊢ M ↓ v
⊑-env{Γ}{γ}{δ}{M}{v} d lt
      with rename-pres{Γ}{Γ}{v}{γ}{δ}{M} (λ {A} x → x) lt d
... | δ⊢id[M]↓v rewrite rename-id {Γ}{★}{M} =
      δ⊢id[M]↓v

在代换反映了指称的证明中，对于 λ-抽象这一情况，我们使用 ⊑-env 的一个小变体，其中只有环境中的最后一个元素变大：

up-env : ∀ {Γ} {γ : Env Γ} {M v u₁ u₂}
  → (γ `, u₁) ⊢ M ↓ v
  → u₁ ⊑ u₂
    -----------------
  → (γ `, u₂) ⊢ M ↓ v
up-env d lt = ⊑-env d (ext-le lt)
  where
  ext-le : ∀ {γ u₁ u₂} → u₁ ⊑ u₂ → (γ `, u₁) `⊑ (γ `, u₂)
  ext-le lt Z = lt
  ext-le lt (S n) = ⊑-refl

练习 denot-church（推荐）

在路径的表达上，丘奇数比自然数更通用。一条路径由 n 条边和 n + 1 个顶点构成。 我们将顶点逆序存储在长度为 n + 1 的向量中。路径中的边将第 i 个顶点映射到第 i + 1 个顶点。以下函数 D^suc（表示后继（successor）的指称）构造了一个表， 其中的条目是路径上所有的边：

D^suc : (n : ℕ) → Vec Value (suc n) → Value
D^suc zero (a[0] ∷ []) = ⊥
D^suc (suc i) (a[i+1] ∷ a[i] ∷ ls) =  a[i] ↦ a[i+1]  ⊔  D^suc i (a[i] ∷ ls)

我们用以下辅助函数来获取非空向量的第一个元素（就我们的目的而言，这种表示方式比 Agda 标准库中的更加方便）。

vec-last : ∀{n : ℕ} → Vec Value (suc n) → Value
vec-last {0} (a ∷ []) = a
vec-last {suc n} (a ∷ b ∷ ls) = vec-last (b ∷ ls)

函数 Dᶜ 计算给定的路径上第 n 个丘奇数的指称。

Dᶜ : (n : ℕ) → Vec Value (suc n) → Value
Dᶜ n (a[n] ∷ ls) = (D^suc n (a[n] ∷ ls)) ↦ (vec-last (a[n] ∷ ls)) ↦ a[n]

  • 0 的丘奇数忽略其第一个参数并返回第二个参数，因此对于只由 a[0] 构成的单例路径，其指称为

      ⊥ ↦ a[0] ↦ a[0]

  • suc n 的丘奇数接受两个参数：一个后继函数，其指称由 D^suc 给定， 以及一个路径的起点（向量的最后一个元素）。它返回路径中的第 n + 1 个节点。

      (D^suc (suc n) (a[n+1] ∷ a[n] ∷ ls)) ↦ (vec-last (a[n] ∷ ls)) ↦ a[n+1]

此练习证明了对于任意路径 ls，邱奇数 n 的含义是 Dᶜ n ls。

为了便于讨论任意丘奇数，以下 church 函数通过辅助函数 apply-n 来构建第 n 个丘奇数的项：

apply-n : (n : ℕ) → ∅ , ★ , ★ ⊢ ★
apply-n zero = # 0
apply-n (suc n) = # 1 · apply-n n

church : (n : ℕ) → ∅ ⊢ ★
church n = ƛ ƛ apply-n n

证明以下定理：

denot-church : ∀{n : ℕ}{ls : Vec Value (suc n)}
   → `∅ ⊢ church n ↓ Dᶜ n ls
-- 请将代码写在此处

函数小于关系的反演

已知函数 v ↦ w 小于某个值 u，我们可以推断出什么？关于 u 我们可以推断出什么？问题的答案被称为「函数小于」的反演性（Inversion）。 这个问题并不容易回答，因为 ⊑-dist 规则将左侧的函数与右侧的一对函数联系了起来。 因此，u 可能包含多个与 v ↦ w 相关的一组函数。此外，由于规则 ⊑-conj-R1 和 ⊑-conj-R2，u 中可能还有别的值（如 ⊥）与 v ↦ w 无关。但总的来说， 我们可以推断出 u 包含了一组函数，其中它们的定义域的连接小于 v，而它们的陪域的连接大于 w。

为了精确陈述并证明这种反演性，我们需要定义「一个值包含一组值的含义。 我们还需要定义如何计算它们的定义域和陪域的连接。

值的成员关系与包含关系

前面我们将值视作一个集合，它由条目以及类似并集的连接运算符 v ⊔ w 组成。 函数值 v ↦ w 和底值 ⊥ 构成了集合的两种元素（在其他语境下，人们可能将 ⊥ 视作空集，但在这里我们必须将它视为一个元素）。我们用 u ∈ v表示 u 是 v 的一个元素，定义如下：

infix 5 _∈_

_∈_ : Value → Value → Set
u ∈ ⊥ = u ≡ ⊥
u ∈ v ↦ w = u ≡ v ↦ w
u ∈ (v ⊔ w) = u ∈ v ⊎ u ∈ w

于是我们可以简单地将一组值表示为一个值。我们用 v ⊆ w 表示 v 的所有元素也都属于 w：

infix 5 _⊆_

_⊆_ : Value → Value → Set
v ⊆ w = ∀{u} → u ∈ v → u ∈ w

值的成员与包含关系的概念和小于关系密切相关， 它们是蕴含了小于关系的更狭义的关系，反之则不然。

∈→⊑ : ∀{u v : Value}
    → u ∈ v
      -----
    → u ⊑ v
∈→⊑ {.⊥} {⊥} refl = ⊑-bot
∈→⊑ {v ↦ w} {v ↦ w} refl = ⊑-refl
∈→⊑ {u} {v ⊔ w} (inj₁ x) = ⊑-conj-R1 (∈→⊑ x)
∈→⊑ {u} {v ⊔ w} (inj₂ y) = ⊑-conj-R2 (∈→⊑ y)

⊆→⊑ : ∀{u v : Value}
    → u ⊆ v
      -----
    → u ⊑ v
⊆→⊑ {⊥} s with s {⊥} refl
... | x = ⊑-bot
⊆→⊑ {u ↦ u′} s with s {u ↦ u′} refl
... | x = ∈→⊑ x
⊆→⊑ {u ⊔ u′} s = ⊑-conj-L (⊆→⊑ (λ z → s (inj₁ z))) (⊆→⊑ (λ z → s (inj₂ z)))

我们还需要一些值的包含关系的反演法则。如果 u 和 v 的并含于 w， 那么 u 和 v 自然都含于 w。

⊔⊆-inv : ∀{u v w : Value}
       → (u ⊔ v) ⊆ w
         ---------------
       → u ⊆ w  ×  v ⊆ w
⊔⊆-inv uvw = ⟨ (λ x → uvw (inj₁ x)) , (λ x → uvw (inj₂ x)) ⟩

在我们的值的表示中，v ↦ w 既是一个元素，又是一个单例集。因此如果 v ↦ w 是 u 的一个子集，那么 v ↦ w 必定是 u 的一个成员。

↦⊆→∈ : ∀{v w u : Value}
     → v ↦ w ⊆ u
       ---------
     → v ↦ w ∈ u
↦⊆→∈ incl = incl refl

函数值

为了识别函数的集合，我们定义了以下两个谓词。如果 u 是一个函数值， 即对于某些值 v 和 w，有 u ≡ v ↦ w，我们就记作 Fun u。 如果 v 中的所有元素都是函数，我们就记作 all-funs v。

data Fun : Value → Set where
  fun : ∀{u v w} → u ≡ (v ↦ w) → Fun u

all-funs : Value → Set
all-funs v = ∀{u} → u ∈ v → Fun u

值 ⊥ 不是函数：

¬Fun⊥ : ¬ (Fun ⊥)
¬Fun⊥ (fun ())

在「值作为集合」的表示中，集合总是包含至少一个元素。即，如果所有的元素都是函数， 那么至少存在一个函数。

all-funs∈ : ∀{u}
      → all-funs u
      → Σ[ v ∈ Value ] Σ[ w ∈ Value ] v ↦ w ∈ u
all-funs∈ {⊥} f with f {⊥} refl
... | fun ()
all-funs∈ {v ↦ w} f = ⟨ v , ⟨ w , refl ⟩ ⟩
all-funs∈ {u ⊔ u′} f
    with all-funs∈ (λ z → f (inj₁ z))
... | ⟨ v , ⟨ w , m ⟩ ⟩ = ⟨ v , ⟨ w , (inj₁ m) ⟩ ⟩

定义域与陪域

回到我们一开始的目标上来，即「小于一个函数」的反演法则。我们想要证明 v ↦ w ⊑ u 蕴含「u 包含一个函数值的集合，它们定义域的连接小于 v，陪域的连接大于 w」。

为此，我们定义了以下 ⨆dom 和 ⨆cod 函数。给定某个值 u（表示一个条目的集合）， ⨆dom u 返回其定义域的连接，⨆cod u 返回其陪域的连接：

⨆dom : (u : Value) → Value
⨆dom ⊥  = ⊥
⨆dom (v ↦ w) = v
⨆dom (u ⊔ u′) = ⨆dom u ⊔ ⨆dom u′

⨆cod : (u : Value) → Value
⨆cod ⊥  = ⊥
⨆cod (v ↦ w) = w
⨆cod (u ⊔ u′) = ⨆cod u ⊔ ⨆cod u′

对于 ⨆dom 和 ⨆cod 我们只需要一个性质。给定一个函数的的集合，表示为值 u，和一个条目 v ↦ w ∈ u，我们能够证明 v 包含在 u 的定义域中：

↦∈→⊆⨆dom : ∀{u v w : Value}
          → all-funs u  →  (v ↦ w) ∈ u
            ----------------------
          → v ⊆ ⨆dom u
↦∈→⊆⨆dom {⊥} fg () u∈v
↦∈→⊆⨆dom {v ↦ w} fg refl u∈v = u∈v
↦∈→⊆⨆dom {u ⊔ u′} fg (inj₁ v↦w∈u) u∈v =
   let ih = ↦∈→⊆⨆dom (λ z → fg (inj₁ z)) v↦w∈u in
   inj₁ (ih u∈v)
↦∈→⊆⨆dom {u ⊔ u′} fg (inj₂ v↦w∈u′) u∈v =
   let ih = ↦∈→⊆⨆dom (λ z → fg (inj₂ z)) v↦w∈u′ in
   inj₂ (ih u∈v)

对于 ⨆cod，假设我们有一个函数集合 u，但它们都只是 v ↦ w 的副本。 那么 ⨆cod u 包含在 w 中：

⊆↦→⨆cod⊆ : ∀{u v w : Value}
        → u ⊆ v ↦ w
          ---------
        → ⨆cod u ⊆ w
⊆↦→⨆cod⊆ {⊥} s refl with s {⊥} refl
... | ()
⊆↦→⨆cod⊆ {C ↦ C′} s m with s {C ↦ C′} refl
... | refl = m
⊆↦→⨆cod⊆ {u ⊔ u′} s (inj₁ x) = ⊆↦→⨆cod⊆ (λ {C} z → s (inj₁ z)) x
⊆↦→⨆cod⊆ {u ⊔ u′} s (inj₂ y) = ⊆↦→⨆cod⊆ (λ {C} z → s (inj₂ z)) y

有了 ⨆dom 和 ⨆cod 函数，我们就可以精确地得出函数的反演法则， 并将其封装到下面的谓词 factor 中。 如果 u′ 包含在 u 中， 我们就说 v ↦ w 将 u 分解（factor）为 u′，如果 u′ 中只包含函数，那么其定义域小于 v，其陪域大于 w。

factor : (u : Value) → (u′ : Value) → (v : Value) → (w : Value) → Set
factor u u′ v w = all-funs u′  ×  u′ ⊆ u  ×  ⨆dom u′ ⊑ v  ×  w ⊑ ⨆cod u′

因此函数的反演法则可被陈述为：

  v ↦ w ⊑ u
  ---------------
→ factor u u′ v w

我们通过在小于关系的推导上归纳证明了函数的反演法则。为了让归纳假设更强， 我们将前提 v ↦ w ⊑ u 推广为 u₁ ⊑ u₂ 并加强了结论，即对于每一个函数值 v ↦ w ∈ u₁，我们都有 v ↦ w 将 u₂ 分解为某个值 u₃。

→ u₁ ⊑ u₂
  ------------------------------------------------------
→ ∀{v w} → v ↦ w ∈ u₁ → Σ[ u₃ ∈ Value ] factor u₂ u₃ v w

函数小于的反演，⊑-trans 的情况

证明的重点在 ⊑-trans 的情况：

u₁ ⊑ u   u ⊑ u₂
--------------- (⊑-trans)
    u₁ ⊑ u₂

根据归纳假设 u₁ ⊑ u，我们证明了对某个值 u′，有 v ↦ w factors u into u′， 因此我们有 all-funs u′ 和 u′ ⊆ u。 根据归纳假设 u ⊑ u₂，我们证明了对于任意 v′ ↦ w′ ∈ u， v′ ↦ w′ 将 u₂ 分解为 u₃。 有了这些事实，我们就能对 u′ 进行归纳，证明 (⨆dom u′) ↦ (⨆cod u′) 将 u₂ 分解为 u₃。接下来我们讨论证明的每种情况。

sub-inv-trans : ∀{u′ u₂ u : Value}
    → all-funs u′  →  u′ ⊆ u
    → (∀{v′ w′} → v′ ↦ w′ ∈ u → Σ[ u₃ ∈ Value ] factor u₂ u₃ v′ w′)
      ---------------------------------------------------------------
    → Σ[ u₃ ∈ Value ] factor u₂ u₃ (⨆dom u′) (⨆cod u′)
sub-inv-trans {⊥} {u₂} {u} fu′ u′⊆u IH =
    contradiction (fu′ refl) ¬Fun⊥
sub-inv-trans {u₁′ ↦ u₂′} {u₂} {u} fg u′⊆u IH = IH (↦⊆→∈ u′⊆u)
sub-inv-trans {u₁′ ⊔ u₂′} {u₂} {u} fg u′⊆u IH
    with ⊔⊆-inv u′⊆u
... | ⟨ u₁′⊆u , u₂′⊆u ⟩
    with sub-inv-trans {u₁′} {u₂} {u} (λ {v′} z → fg (inj₁ z)) u₁′⊆u IH
       | sub-inv-trans {u₂′} {u₂} {u} (λ {v′} z → fg (inj₂ z)) u₂′⊆u IH
... | ⟨ u₃₁ , ⟨ fu21' , ⟨ u₃₁⊆u₂ , ⟨ du₃₁⊑du₁′ , cu₁′⊑cu₃₁ ⟩ ⟩ ⟩ ⟩
    | ⟨ u₃₂ , ⟨ fu22' , ⟨ u₃₂⊆u₂ , ⟨ du₃₂⊑du₂′ , cu₁′⊑cu₃₂ ⟩ ⟩ ⟩ ⟩ =
      ⟨ (u₃₁ ⊔ u₃₂) , ⟨ fu₂′ , ⟨ u₂′⊆u₂ ,
      ⟨ ⊔⊑⊔ du₃₁⊑du₁′ du₃₂⊑du₂′ ,
        ⊔⊑⊔ cu₁′⊑cu₃₁ cu₁′⊑cu₃₂ ⟩ ⟩ ⟩ ⟩
    where fu₂′ : {v′ : Value} → v′ ∈ u₃₁ ⊎ v′ ∈ u₃₂ → Fun v′
          fu₂′ {v′} (inj₁ x) = fu21' x
          fu₂′ {v′} (inj₂ y) = fu22' y
          u₂′⊆u₂ : {C : Value} → C ∈ u₃₁ ⊎ C ∈ u₃₂ → C ∈ u₂
          u₂′⊆u₂ {C} (inj₁ x) = u₃₁⊆u₂ x
          u₂′⊆u₂ {C} (inj₂ y) = u₃₂⊆u₂ y
  • 假设 u′ ≡ ⊥，那么我们可导出矛盾，因为它不满足 Fun ⊥ 的情况。
  • 假设 u′ ≡ u₁′ ↦ u₂′，那么 u₁′ ↦ u₂′ ∈ u，且我们可以应用前提 （归纳假设 u ⊑ u₂）来得到 u₁′ ↦ u₂′ 将 u₂ 分解为 u₃。 此情况是完整的，因为 ⨆dom u′ ≡ u₁′ 且 ⨆cod u′ ≡ u₂′。

  • 假设 u′ ≡ u₁′ ⊔ u₂′，那么 u₁′ ⊆ u 且 u₂′ ⊆ u。我们同样有 all-funs u₁′ 且 all-funs u₂′，于是我们可以对 u₁′ 和 u₂′ 应用归纳假设。因此存在值 u₃₁ 和 u₃₂ 使得 (⨆dom u₁′) ↦ (⨆cod u₁′) 将 u 分解为 u₃₁，以及 (⨆dom u₂′) ↦ (⨆cod u₂′) 将 u 分解为 u₃₂。 我们要证明 (⨆dom u) ↦ (⨆cod u) 将 u 分解为 u₃₁ ⊔ u₃₂，因此我们需要证明

      ⨆dom (u₃₁ ⊔ u₃₂) ⊑ ⨆dom (u₁′ ⊔ u₂′)
  ⨆cod (u₁′ ⊔ u₂′) ⊑ ⨆cod (u₃₁ ⊔ u₃₂)

然而二者可直接根据 ⊔ 对于 ⊑ 的单调性，从 u 分解为 u₃₁ 和 u₃₂ 得到。

函数小于的反演

我们来证明有关函数小于的反演的主要引理。我们要证明若 u₁ ⊑ u₂， 则对于任何 v ↦ w ∈ u₁，都可以根据 v ↦ w 将 u₂ 分解为 u₃。 我们对 u₁ ⊑ u₂ 的推导进行归纳，并在 Agda 证明过程后面描述证明中的每一种情况。

sub-inv : ∀{u₁ u₂ : Value}
        → u₁ ⊑ u₂
        → ∀{v w} → v ↦ w ∈ u₁
          -------------------------------------
        → Σ[ u₃ ∈ Value ] factor u₂ u₃ v w
sub-inv {⊥} {u₂} ⊑-bot {v} {w} ()
sub-inv {u₁₁ ⊔ u₁₂} {u₂} (⊑-conj-L lt1 lt2) {v} {w} (inj₁ x) = sub-inv lt1 x
sub-inv {u₁₁ ⊔ u₁₂} {u₂} (⊑-conj-L lt1 lt2) {v} {w} (inj₂ y) = sub-inv lt2 y
sub-inv {u₁} {u₂₁ ⊔ u₂₂} (⊑-conj-R1 lt) {v} {w} m
    with sub-inv lt m
... | ⟨ u₃₁ , ⟨ fu₃₁ , ⟨ u₃₁⊆u₂₁ , ⟨ domu₃₁⊑v , w⊑codu₃₁ ⟩ ⟩ ⟩ ⟩ =
      ⟨ u₃₁ , ⟨ fu₃₁ , ⟨ (λ {w} z → inj₁ (u₃₁⊆u₂₁ z)) ,
                                   ⟨ domu₃₁⊑v , w⊑codu₃₁ ⟩ ⟩ ⟩ ⟩
sub-inv {u₁} {u₂₁ ⊔ u₂₂} (⊑-conj-R2 lt) {v} {w} m
    with sub-inv lt m
... | ⟨ u₃₂ , ⟨ fu₃₂ , ⟨ u₃₂⊆u₂₂ , ⟨ domu₃₂⊑v , w⊑codu₃₂ ⟩ ⟩ ⟩ ⟩ =
      ⟨ u₃₂ , ⟨ fu₃₂ , ⟨ (λ {C} z → inj₂ (u₃₂⊆u₂₂ z)) ,
                                   ⟨ domu₃₂⊑v , w⊑codu₃₂ ⟩ ⟩ ⟩ ⟩
sub-inv {u₁} {u₂} (⊑-trans{v = u} u₁⊑u u⊑u₂) {v} {w} v↦w∈u₁
    with sub-inv u₁⊑u v↦w∈u₁
... | ⟨ u′ , ⟨ fu′ , ⟨ u′⊆u , ⟨ domu′⊑v , w⊑codu′ ⟩ ⟩ ⟩ ⟩
    with sub-inv-trans {u′} fu′ u′⊆u (sub-inv u⊑u₂)
... | ⟨ u₃ , ⟨ fu₃ , ⟨ u₃⊆u₂ , ⟨ domu₃⊑domu′ , codu′⊑codu₃ ⟩ ⟩ ⟩ ⟩ =
      ⟨ u₃ , ⟨ fu₃ , ⟨ u₃⊆u₂ , ⟨ ⊑-trans domu₃⊑domu′ domu′⊑v ,
                                    ⊑-trans w⊑codu′ codu′⊑codu₃ ⟩ ⟩ ⟩ ⟩
sub-inv {u₁₁ ↦ u₁₂} {u₂₁ ↦ u₂₂} (⊑-fun lt1 lt2) refl =
    ⟨ u₂₁ ↦ u₂₂ , ⟨ (λ {w} → fun) , ⟨ (λ {C} z → z) , ⟨ lt1 , lt2 ⟩ ⟩ ⟩ ⟩
sub-inv {u₂₁ ↦ (u₂₂ ⊔ u₂₃)} {u₂₁ ↦ u₂₂ ⊔ u₂₁ ↦ u₂₃} ⊑-dist
    {.u₂₁} {.(u₂₂ ⊔ u₂₃)} refl =
    ⟨ u₂₁ ↦ u₂₂ ⊔ u₂₁ ↦ u₂₃ , ⟨ f , ⟨ g , ⟨ ⊑-conj-L ⊑-refl ⊑-refl , ⊑-refl ⟩ ⟩ ⟩ ⟩
  where f : all-funs (u₂₁ ↦ u₂₂ ⊔ u₂₁ ↦ u₂₃)
        f (inj₁ x) = fun x
        f (inj₂ y) = fun y
        g : (u₂₁ ↦ u₂₂ ⊔ u₂₁ ↦ u₂₃) ⊆ (u₂₁ ↦ u₂₂ ⊔ u₂₁ ↦ u₂₃)
        g (inj₁ x) = inj₁ x
        g (inj₂ y) = inj₂ y

令 v 和 w 为任意值。

  • 情况 ⊑-bot：若 u₁ ≡ ⊥，我们有 v ↦ w ∈ ⊥，但这是不可能的。

  • 情况 ⊑-conj-L：

      u₁₁ ⊑ u₂   u₁₂ ⊑ u₂
  -------------------
  u₁₁ ⊔ u₁₂ ⊑ u₂

给定 v ↦ w ∈ u₁₁ ⊔ u₁₂，那么有两种子情况需要考虑：

  • 子情况 v ↦ w ∈ u₁₁：我们通过归纳假设 u₁₁ ⊑ u₂ 得出结论。

  • 子情况 v ↦ w ∈ u₁₂：我们通过归纳假设 u₁₂ ⊑ u₂ 得出结论。

  • 情况 ⊑-conj-R1：

      u₁ ⊑ u₂₁
  --------------
  u₁ ⊑ u₂₁ ⊔ u₂₂

给定 v ↦ w ∈ u₁，归纳假设 u₁ ⊑ u₂₁ 给出了对某个 u₃₁，v ↦ w 将 u₂₁ 分解为 u₃₁。为了证明 v ↦ w 也将 u₂₁ ⊔ u₂₂ 分解为 u₃₁， 我们只需证明 u₃₁ ⊆ u₂₁ ⊔ u₂₂，而这一点可直接从 u₃₁ ⊆ u₂₁ 得出。

  • 情况 ⊑-conj-R2：此情况的论证过程与情况 ⊑-conj-R1 类似。

  • 情况 ⊑-trans：

      u₁ ⊑ u   u ⊑ u₂
  ---------------
      u₁ ⊑ u₂

根据归纳假设 u₁ ⊑ u，我们可以证明对于某个值 u′，v ↦ w 将 u 分解为 u′， 于是我们有 all-funs u′ 和 u′ ⊆ u。跟举归纳假设 u ⊑ u₂，我们可以证明对于任意 v′ ↦ w′ ∈ u，v′ ↦ w′ 分解了 u₂。现在应用引理 sub-inv-trans， 它会给出 u₃ 使得 (⨆dom u′) ↦ (⨆cod u′) 将 u₂ 分解为 u₃。 我们证明了 v ↦ w 也将 u₂ 分解为 u₃。 从 ⨆dom u₃ ⊑ ⨆dom u′ 和 ⨆dom u′ ⊑ v，我们可得出 ⨆dom u₃ ⊑ v。 从 w ⊑ ⨆cod u′ 和 ⨆cod u′ ⊑ ⨆cod u₃，我们有 w ⊑ ⨆cod u₃，于是此情况就覆盖完整了。

  • 情况 ⊑-fun：

      u₂₁ ⊑ u₁₁  u₁₂ ⊑ u₂₂
  ---------------------
  u₁₁ ↦ u₁₂ ⊑ u₂₁ ↦ u₂₂

给定 v ↦ w ∈ u₁₁ ↦ u₁₂，我们有 v ≡ u₁₁ 和 w ≡ u₁₂。 我们证明了 u₁₁ ↦ u₁₂ 将 u₂₁ ↦ u₂₂ 分解为其自身。 我们还需证明 ⨆dom (u₂₁ ↦ u₂₂) ⊑ u₁₁ 和 u₁₂ ⊑ ⨆cod (u₂₁ ↦ u₂₂)， 然而这等价于前提 u₂₁ ⊑ u₁₁ 和 u₁₂ ⊑ u₂₂。

  • 情况 ⊑-dist：

      ---------------------------------------------
  u₂₁ ↦ (u₂₂ ⊔ u₂₃) ⊑ (u₂₁ ↦ u₂₂) ⊔ (u₂₁ ↦ u₂₃)

给定 v ↦ w ∈ u₂₁ ↦ (u₂₂ ⊔ u₂₃)，我们有 v ≡ u₂₁ 和 w ≡ u₂₂ ⊔ u₂₃。 我们证明了 u₂₁ ↦ (u₂₂ ⊔ u₂₃) 将 (u₂₁ ↦ u₂₂) ⊔ (u₂₁ ↦ u₂₃) 分解为其自身。 我们有 u₂₁ ⊔ u₂₁ ⊑ u₂₁，以及 u₂₂ ⊔ u₂₃ ⊑ u₂₂ ⊔ u₂₃，于是此证明就覆盖完整了。

我们用 sub-inv 引理的两个推论作为本节的结尾。首先，我们来证明以下性质， 方便在后面的证明中使用。我们将前提特化为 v ↦ w ⊑ u₁，并将结论修改为对于每个 v′ ↦ w′ ∈ u₂，我们有 v′ ⊑ v。

sub-inv-fun : ∀{v w u₁ : Value}
    → (v ↦ w) ⊑ u₁
      -----------------------------------------------------
    → Σ[ u₂ ∈ Value ] all-funs u₂ × u₂ ⊆ u₁
        × (∀{v′ w′} → (v′ ↦ w′) ∈ u₂ → v′ ⊑ v) × w ⊑ ⨆cod u₂
sub-inv-fun{v}{w}{u₁} abc
    with sub-inv abc {v}{w} refl
... | ⟨ u₂ , ⟨ f , ⟨ u₂⊆u₁ , ⟨ db , cc ⟩ ⟩ ⟩ ⟩ =
      ⟨ u₂ , ⟨ f , ⟨ u₂⊆u₁ , ⟨ G , cc ⟩ ⟩ ⟩ ⟩
   where G : ∀{D E} → (D ↦ E) ∈ u₂ → D ⊑ v
         G{D}{E} m = ⊑-trans (⊆→⊑ (↦∈→⊆⨆dom f m)) db

第二个推论是反演规则，即我们期望左侧函数小于右侧。

↦⊑↦-inv : ∀{v w v′ w′}
        → v ↦ w ⊑ v′ ↦ w′
          -----------------
        → v′ ⊑ v × w ⊑ w′
↦⊑↦-inv{v}{w}{v′}{w′} lt
    with sub-inv-fun lt
... | ⟨ Γ , ⟨ f , ⟨ Γ⊆v34 , ⟨ lt1 , lt2 ⟩ ⟩ ⟩ ⟩
    with all-funs∈ f
... | ⟨ u , ⟨ u′ , u↦u′∈Γ ⟩ ⟩
    with Γ⊆v34 u↦u′∈Γ
... | refl =
  let ⨆codΓ⊆w′ = ⊆↦→⨆cod⊆ Γ⊆v34 in
  ⟨ lt1 u↦u′∈Γ , ⊑-trans lt2 (⊆→⊑ ⨆codΓ⊆w′) ⟩

注记

本章中展示的操作语义是过滤器模型（filter model，@Barendregt:1983）的一个例子。 过滤器模型使用带有交集类型的类型系统来精确刻画运行时行为（Coppo, Dezani-Ciancaglini, and Salle’ (1979)）。 我们在本章中使用的记法并不是类型系统和交集类型的记法，但 Value 数据类型与这些类型同构（↦ 对应 →，⊔ 对应 ∧，⊥ 对应 ⊤）， ⊑ 关系是子类型 <: 的逆关系，并且求值关系 ρ ⊢ M ↓ v 与类型系统同构。 将 ρ 写成 Γ，将 v 写成 A，将 ↓ 替换为 :，就得到了一个类型判断 Γ ⊢ M : A。通过改变子类型的定义和使用类型原子的不同选择， 交集类型系统为许多不同的无类型 λ-演算提供语义，从完整的 beta-归约到惰性演算和按值调用演算（Alessi, Barbanera, and Dezani-Ciancaglini (2006)，Ronchi Della Rocca and Paolini (2004)）。 本章中的指称语义对应于 BCD 系统（H. Barendregt, Coppo, and Dezani-Ciancaglini (1983)）。 Lambda Calculus with Types 一书中的第三部分描述了一个交集类型系统的框架， 它可以实现与本章中类似的结果，但适用于整个交集类型系统族（H. Barendregt, Dekkers, and Statman (2013)）

使用有限的表格来表示函数，以及放宽表的查找以实现自我应用这两个想法首次出现在 Plotkin (1972) 的技术报告中，后来在《理论计算机科学》（Plotkin (1993)） 的一篇文章中进行了描述。在该项工作中，Value 的归纳定义与我们使用的有点不同：

Value = C + ℘f(Value) × ℘f(Value)

其中 C 是一组常量，℘f 表示有限幂集。℘f(Value) × ℘f(Value) 中的序对表示输入-输出映射，和本章中的一样。有限幂集用于使函数表能够出现在输入和输出中。 这些差异相当于改变了 Value 定义中递归出现的位置。Plotkin 的模型是无类型 λ-演算的图模型（graph model）的一个例子（H. P. Barendregt (1984)）。 在图模型中，语义被表示为从程序和环境到（可能是无限的）值的集合的函数。 本章中的语义被定义为关系，不过以集合为值的函数与关系同构。 实际上，我们将在下一章中将语义表示为函数，并证明它等价于关系的版本。

Scott (1976) 的 ℘(ω) 模型和 Engeler (1981) 的 B(A) 模型是图模型的另外两个例子。 二者都采用了以下 Value 的归纳定义。

Value = C + ℘f(Value) × Value

在输出中使用 Value 而非 ℘f(Value) 相对 Plotkin 的模型来说并不会限制表达能力， 因为使用了值的集合的语义和集合 (V, V′) 的序对可以表示为一个序对的集合 { (V, v′) | v′ ∈ V′ }。在 Scott 的 ℘(ω) 中， 上面的值通过一种哥德尔编码做了它和自然数的双向映射。

Unicode

本章使用了以下 Unicode：

⊥  U+22A5  UP TACK (\bot)
↦  U+21A6  RIGHTWARDS ARROW FROM BAR (\mapsto)
⊔  U+2294  SQUARE CUP (\lub)
⊑  U+2291  SQUARE IMAGE OF OR EQUAL TO (\sqsubseteq)
⨆ U+2A06  N-ARY SQUARE UNION OPERATOR (\Lub)
⊢  U+22A2  RIGHT TACK (\|- or \vdash)
↓  U+2193  DOWNWARDS ARROW (\d)
ᶜ  U+1D9C  MODIFIER LETTER SMALL C (\^c)
ℰ  U+2130  SCRIPT CAPITAL E (\McE)
≃  U+2243  ASYMPTOTICALLY EQUAL TO (\~- or \simeq)
∈  U+2208  ELEMENT OF (\in)
⊆  U+2286  SUBSET OF OR EQUAL TO (\sub= or \subseteq)

参考来源

Alessi, Fabio, Franco Barbanera, and Mariangiola Dezani-Ciancaglini. 2006. “Intersection Types and Lambda Models.” Theoretical Computer Science 355 (2): 108–26.
Barendregt, H. P. 1984. The Lambda Calculus. Vol. 103. Studies in Logic. Elsevier.
Barendregt, Henk, Mario Coppo, and Mariangiola Dezani-Ciancaglini. 1983. “A Filter Lambda Model and the Completeness of Type Assignment.” Journal of Symbolic Logic 48 (4): 931–40. https://doi.org/10.2307/2273659.
Barendregt, Henk, Wil Dekkers, and Richard Statman. 2013. Lambda Calculus with Types. Perspectives in Logic. Cambridge University Press.
Coppo, M., M. Dezani-Ciancaglini, and P. Salle’. 1979. “Functional Characterization of Some Semantic Equalities Inside Lambda-Calculus.” In Automata, Languages and Programming: Sixth Colloquium, edited by Hermann A. Maurer, 133–46. Berlin, Heidelberg: Springer Berlin Heidelberg.
Engeler, Erwin. 1981. “Algebras and Combinators.” Algebra Universalis 13 (1): 389–92.
Plotkin, Gordon D. 1972. “A Set-Theoretical Definition of Application.” MIP-R-95. University of Edinburgh.
———. 1993. “Set-Theoretical and Other Elementary Models of the λ-Calculus.” Theoretical Computer Science 121 (1): 351–409.
Ronchi Della Rocca, Simona, and Luca Paolini. 2004. The Parametric Lambda Calculus. Springer.
Scott, Dana. 1976. “Data Types as Lattices.” SIAM Journal on Computing 5 (3): 522–87.