---
title: "变量改名"
module: FOL.Manipulation.Renaming
lang: zh
site: "Bedrock"
description: "变量改名"
stage: "一阶逻辑"
reading_order: 13
canonical: https://bedrock.institute/zh/FOL.Manipulation.Renaming.html
html: FOL.Manipulation.Renaming.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/FOL/Manipulation/Renaming.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Syntax, FOL.Semantics]
routes: [fol-operations]
translations: [https://bedrock.institute/en/FOL.Manipulation.Renaming.md, https://bedrock.institute/ja/FOL.Manipulation.Renaming.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 变量改名

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

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

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

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

module FOL.Manipulation.Renaming where

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

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

```agda
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ρ ρ`，它保证被约束变量从不被扰动。

```agda
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` 完全不指名任何自由变量，因此原样通过；常元属于字母表而非语境，其解释是另一回事。词项仅剩的另一种形式是变量，`ρ` 在此才真正起作用。

```agda
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)`。命题联结词与假值自身不带变量，由改名后的子公式递归重建。

```agda
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ρ ρ` 而非 `ρ`。这正是我们为例子描述的规则：被约束的槽位保持在第零位，外层改名只以移位后的形式到达公式体。

```agda
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 的被约束出现原封不动。语法层至此完成；下一节追问结果是否与我们出发的公式含义相同。

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

## 语义层

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

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

```agda
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 δ`，即大环境必须在像的位置与小环境匹配。

```agda
  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∷` 是语法提升在语义上的对应物。

```agda
  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 ρ γ δ` 正是使断言有实质内容的条件：环境之间没有任何关系时，指称的相等无从谈起。

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

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

```agda
              (γ : 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`。

```agda
             (γ : 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ρ ρ` 之下相符，而这恰是较小公式处的归纳假设。这正是整体设计的关键：相符关系本就为在扩展下存活而构造，递归调用因此畅通无阻。

```agda
  ⊨-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₂ _⇒_` 把二者焊成蕴涵之间所需的路径。

```agda
  ⊨-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` 陈述，因此把两个变量收缩到一处，如收缩；把变量拉开间距，如弱化；或调换次序，如交换；都是同样可采纳的。

```agda
  ⊨-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` 组成。选择不同语境映射，即可将这一统一接口特化为弱化、交换或收缩。