变量改名

可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。

阅读指南 · 依赖地图

有限变量语境之间的映射通过改名自由变量作用于词项与公式，同时保持常元不变。环境上的相符关系给出一条语义定理，统一涵盖弱化、交换与收缩。

语法章提过一处缺席：没有替换，也没有弱化。量词子句直接取扩展语境中的公式体，因此经典的整套变量替换机制并无必要。本书确实需要的那一点变量调整，由一个操作完成：改名，即沿公式推送一个映射 ρ : Fin n → Fin m，并配一条正确性定理，弱化、交换、收缩都由此得出。

设想一个公式，其自由变量由 n 个槽位索引，而我们想在 m 个槽位的语境中看待它。映射 ρ : Fin n → Fin m 告诉我们每个变量去向何处，改名就是把这一映射作用到公式的每个自由变量上。唯一的复杂之处在量词：量词体活在多出一个槽位的语境中，因此 ρ 必须在每个约束子之下以不惊动被约束变量的方式扩展。

{-# OPTIONS --cubical --safe --guardedness #-}

module FOL.Manipulation.Renaming where

open import Base.Prelude
open import FOL.ZFStructure using ( ZFStructure )

随后由一条正确性定理来衡量改名：在旧环境与新环境之间一个合适的关系之下，改名后的公式与原公式指称相同的命题。由于该命题是在任意命题值集合论结构中计算的，定理与满足关系本身具有完全相同的普遍性；而序列演算惯用的结构规则，弱化、交换、收缩，都作为 ρ 的特定选取由此得出。

open import FOL.Syntax using
  ( Term; con; var
  ; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
import FOL.Semantics

语法层

renameTm 与 renameFo 将映射 Fin n → Fin m 贯穿语法。在约束子之下，liftρ 固定新约束的变量，并通过给定映射移动原有变量。

取一个在有界量词之下含自由变量的公式，例如双槽位语境中的 ∀̇∈ x₀ (var 1 ∈̇ var 0)：被约束变量是公式体的第零槽位，而公式体的第 1 槽位正是外层的自由变量 0。改名 ρ : Fin n → Fin m 移动外层变量；在约束子之下，我们需要 Fin (suc n) → Fin (suc m) 上的一个映射，把被约束的第零槽位送到第零槽位，并把每个旧槽位 suc i 送到 suc (ρ i)。这一扩展就是 liftρ ρ，它保证被约束变量从不被扰动。

liftρ : ∀ {n m} → (Fin n → Fin m) → Fin (suc n) → Fin (suc m)
liftρ ρ zero    = zero
liftρ ρ (suc i) = suc (ρ i)

有了提升，改名便可对词项、再对公式做结构递归地扩展。renameTm 的类型已经说出全部想法：含 n 个自由变量槽位的词项变为含 m 个槽位的词项。常元 con k 完全不指名任何自由变量，因此原样通过；常元属于字母表而非语境，其解释是另一回事。词项仅剩的另一种形式是变量，ρ 在此才真正起作用。

renameTm : ∀ {ℓc} {K : Type ℓc} {n m} → (Fin n → Fin m) → Term K n → Term K m
renameTm ρ (con k) = con k

公式的模式相同：renameFo 形状一致，把 n 个槽位上的公式变为 m 个槽位上的公式。两条原子子句对其词项参数改名，因此在我们的例子中，就外层槽位而言 var 1 ∈̇ var 0 变为 var (ρ 1) ∈̇ var (ρ 0)。命题联结词与假值自身不带变量，由改名后的子公式递归重建。

renameTm ρ (var i) = var (ρ i)

renameFo : ∀ {ℓc} {K : Type ℓc} {n m} → (Fin n → Fin m) → Formula K n → Formula K m
renameFo ρ (t ∈̇ u)  = renameTm ρ t ∈̇ renameTm ρ u
renameFo ρ (t ≐ u)  = renameTm ρ t ≐ renameTm ρ u
renameFo ρ (φ ∧̇ ψ)  = renameFo ρ φ ∧̇ renameFo ρ ψ

普通量词是递归调用首次改变的地方：公式体活在扩展语境中，因此递归调用传入的是 liftρ ρ 而非 ρ。这正是我们为例子描述的规则：被约束的槽位保持在第零位，外层改名只以移位后的形式到达公式体。

renameFo ρ (φ ∨̇ ψ)  = renameFo ρ φ ∨̇ renameFo ρ ψ
renameFo ρ (φ ⇒̇ ψ)  = renameFo ρ φ ⇒̇ renameFo ρ ψ
renameFo ρ ⊥̇        = ⊥̇
renameFo ρ (∃̇ φ)    = ∃̇ renameFo (liftρ ρ) φ
renameFo ρ (∀̇ φ)    = ∀̇ renameFo (liftρ ρ) φ

有界量词同时使用两个映射，我们的例子恰好落在这里。对 ∀̇∈ t φ，界限 t 住在外层语境，用 ρ 改名；公式体 φ 用 liftρ ρ 改名。于是 ∀̇∈ x₀ (var 1 ∈̇ var 0) 在 ρ 之下变为 ∀̇∈ (改名后的界限) (var (suc (ρ 0)) ∈̇ var 0)：对自由变量 0 的引用随移位跟随改名，而槽位 0 的被约束出现原封不动。语法层至此完成；下一节追问结果是否与我们出发的公式含义相同。

renameFo ρ (∀̇∈ t φ) = ∀̇∈ (renameTm ρ t) (renameFo (liftρ ρ) φ)
renameFo ρ (∃̇∈ t φ) = ∃̇∈ (renameTm ρ t) (renameFo (liftρ ρ) φ)

语义层

Agrees ρ γ δ 表示两个环境给经 ρ 对应的变量指派相等的取值。该条件在约束子下扩展环境时仍保持，结构归纳遂证明改名后词项释义与公式满足关系相等。

仅靠语法无法判断改名是否保持含义；我们需要比较环境。环境是结构载体的元素构成的向量，长度与语境匹配：大语境用 γ : S ^ m，小语境用 δ : S ^ n。问题于是变成：从 ρ 的角度看，γ 与 δ 何时算是同一个指派？

module Sat {ℓ} (𝒮 : ZFStructure ℓ)
           {ℓc} {K : Type ℓc} (ι : K → ZFStructure.S 𝒮) where

  open ZFStructure 𝒮

  private module Sem = FOL.Semantics 𝒮

答案就是关系 Agrees ρ γ δ：对小语境的每个索引 i，δ 在 i 处与 γ 在 ρ i 处必须取相等的元素，该相等是载体中的路径。注意查找的方向：ρ 从小语境走向大语境，因此 δ 在 i 处指派的正是 γ 在 ρ i 处指派的。在我们 n = 2 的运行例子中，公式体变量 1 上的相符读作 lookup (ρ 0) γ ≡ lookup 1 δ，即大环境必须在像的位置与小环境匹配。

  open Sem using ( _^_ )
  open Sem.At K ι using ( _⊨_; ⟦_⟧ )

  Agrees : ∀ {n m} → (Fin n → Fin m) → S ^ m → S ^ n → Type ℓ
  Agrees ρ γ δ = ∀ i → lookup (ρ i) γ ≡ lookup i δ

正确性定理：变换后的公式在大环境中的含义，与原公式在小环境中的相同。先处理词项，然后照例归纳，每个情形是一条同余，约束子情形依赖 agrees∷。弱化 (插入未用的变量)、交换、收缩都是特例，取相应的 ρ 即得。

定理将对公式做归纳，因此相符关系必须在量词之下这一步仍然成立。事实如此：若两个环境都在第零位添加同一元素 x，则 x ∷ γ 与 x ∷ δ 在 liftρ ρ 之下相符。索引零处两边经计算都读出 x；索引 suc i 处的要求归约为原有的 ag i。引理 agrees∷ 是语法提升在语义上的对应物。

  agrees∷ : ∀ {n m} {ρ : Fin n → Fin m} {γ : S ^ m} {δ : S ^ n}
            (x : S) → Agrees ρ γ δ → Agrees (liftρ ρ) (x ∷ γ) (x ∷ δ)
  agrees∷ x ag zero    = refl
  agrees∷ x ag (suc i) = ag i

一切都落在两条定理上。对词项：在环境 γ 与 δ 于 ρ 之下相符的前提下，在大环境中求值 renameTm ρ t 得到一条到在小环境中求值 t 的路径。对公式，类似的陈述比较满足关系的命题。前提 Agrees ρ γ δ 正是使断言有实质内容的条件：环境之间没有任何关系时，指称的相等无从谈起。

  ⟦⟧-rename : ∀ {n m} (ρ : Fin n → Fin m) (t : Term K n)

词项的证明很短，因为词项本身内容很少。常元的释义 ι k 与环境无关，两次求值经 refl 相同。变量 var i 在小侧释义为 lookup i δ，在大侧释义为 lookup (ρ i) γ，而索引 i 处的相符恰是二者之间的路径，故 ag i 了结此情形。真正的内容在上一层的公式定理中。

              (γ : S ^ m) (δ : S ^ n) → Agrees ρ γ δ
            → ⟦ renameTm ρ t ⟧ γ ≡ ⟦ t ⟧ δ
  ⟦⟧-rename ρ (con k) γ δ ag = refl
  ⟦⟧-rename ρ (var i) γ δ ag = ag i

  ⊨-rename : ∀ {n m} (ρ : Fin n → Fin m) (φ : Formula K n)

公式定理陈述两个命题之间的路径：大侧的 γ ⊨ renameFo ρ φ，小侧的 δ ⊨ φ。先看我们例子中的有界量词，其公式体不含更深的约束子；其余情形遵循同样的两种模式，同余或递归，在此一并描述。对原子公式，词项定理给出改名词项与原词项释义之间的路径，cong₂ 把这些路径经过集合的属于或相等传输过去。联结词情形同样对相应的逻辑运算用 cong₂，假值只需 refl。

             (γ : S ^ m) (δ : S ^ n) → Agrees ρ γ δ
           → (γ ⊨ renameFo ρ φ) ≡ (δ ⊨ φ)
  ⊨-rename ρ (t ∈̇ u)  γ δ ag = cong₂ _∈ˢ_ (⟦⟧-rename ρ t γ δ ag) (⟦⟧-rename ρ u γ δ ag)
  ⊨-rename ρ (t ≐ u)  γ δ ag = cong₂ _≈ˢ_ (⟦⟧-rename ρ t γ δ ag) (⟦⟧-rename ρ u γ δ ag)
  ⊨-rename ρ (φ ∧̇ ψ)  γ δ ag = cong₂ _⊓_ (⊨-rename ρ φ γ δ ag) (⊨-rename ρ ψ γ δ ag)

在无界存在量词 ∃̇ φ 之下，满足关系遍历载体的所有候选元素 x，因此证明须说明两侧关于 x 的函数逐点相等，funExt 正在此处登场。在每个 x 处，两侧环境是扩展 x ∷ γ 与 x ∷ δ，由 agrees∷ x ag 它们在 liftρ ρ 之下相符，而这恰是较小公式处的归纳假设。这正是整体设计的关键：相符关系本就为在扩展下存活而构造，递归调用因此畅通无阻。

  ⊨-rename ρ (φ ∨̇ ψ)  γ δ ag = cong₂ _⊔_ (⊨-rename ρ φ γ δ ag) (⊨-rename ρ ψ γ δ ag)
  ⊨-rename ρ (φ ⇒̇ ψ)  γ δ ag = cong₂ _⇒_ (⊨-rename ρ φ γ δ ag) (⊨-rename ρ ψ γ δ ag)
  ⊨-rename ρ ⊥̇        γ δ ag = refl
  ⊨-rename ρ (∃̇ φ)    γ δ ag = cong (λ P → ∃[ x ∶ S ] P x) (funExt (λ x →
    ⊨-rename (liftρ ρ) φ (x ∷ γ) (x ∷ δ) (agrees∷ x ag)))

无界全称量词 ∀̇ φ 是对偶情形，用 ∀[ x ] P x 替代 ∃[ x ] P x，funExt 与 agrees∷ 的步骤相同。有界全称量词 ∀̇∈ t φ 把两种成分结合起来：其满足是对 x 的 ∀[ x ] P x，从 x ∈ˢ ⟦ t ⟧ γ 到公式体满足的蕴涵。界限贡献一个经 x ∈ˢ_ 的 cong，由词项定理提供；公式体贡献在 liftρ ρ 处的递归调用；cong₂ _⇒_ 把二者焊成蕴涵之间所需的路径。

  ⊨-rename ρ (∀̇ φ)    γ δ ag = cong (λ P → ∀[ x ∶ S ] P x) (funExt (λ x →
    ⊨-rename (liftρ ρ) φ (x ∷ γ) (x ∷ δ) (agrees∷ x ag)))
  ⊨-rename ρ (∀̇∈ t φ) γ δ ag = cong (λ P → ∀[ x ∶ S ] P x) (funExt (λ x →
    cong₂ _⇒_ (cong (x ∈ˢ_) (⟦⟧-rename ρ t γ δ ag))
              (⊨-rename (liftρ ρ) φ (x ∷ γ) (x ∷ δ) (agrees∷ x ag))))

有界存在量词 ∃̇∈ t φ 以镜像结束归纳：对 x 的 ∃[ x ] P x，改名后的界限 x ∈ˢ ⟦ t ⟧ γ 经 ⊓ 与公式体满足相接，以及经 agrees∷ 的同一递归调用。注意什么从未被用到：ρ 的单射性。定理对任意映射 Fin n → Fin m` 陈述，因此把两个变量收缩到一处，如收缩；把变量拉开间距，如弱化；或调换次序，如交换；都是同样可采纳的。

  ⊨-rename ρ (∃̇∈ t φ) γ δ ag = cong (λ P → ∃[ x ∶ S ] P x) (funExt (λ x →
    cong₂ _⊓_ (cong (x ∈ˢ_) (⟦⟧-rename ρ t γ δ ag))
              (⊨-rename (liftρ ρ) φ (x ∷ γ) (x ∷ δ) (agrees∷ x ag))))

小结

变量改名由语法映射、环境相符关系与定理 ⊨-rename 组成。选择不同语境映射，即可将这一统一接口特化为弱化、交换或收缩。