---
title: "公式码的字母表"
module: L.Coding.CodeAlphabet
lang: zh
site: "Bedrock"
description: "公式码的字母表"
stage: "内部编码：表与统一满足关系"
reading_order: 64
canonical: https://bedrock.institute/zh/L.Coding.CodeAlphabet.html
html: L.Coding.CodeAlphabet.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/CodeAlphabet.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Syntax, FOL.Manipulation.ConstantMapping, V.Coding, L.Constructible]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/en/L.Coding.CodeAlphabet.md, https://bedrock.institute/ja/L.Coding.CodeAlphabet.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 公式码的字母表

关于可构造集合 `W` 的陈述往往会提到 `W` 的成员：比如说，要断言 `W` 中某个 `x` 满足一条性质，公式就要带着 `x` 作为参数。在集合论内部，这样的参数以一阶语言的常元符号出现。然而，外围的语法编码要求常元是层级 `V ℓ` 中的集合，而不是对任意集合成员的抽象指称。因此需要一座桥：一种字母表可索引 `W` 成员的语言，连同把每个索引送到其集合指称的嵌入。

本章对固定的 `W` 搭建这座桥。字母表是 `W` 底层集合的成员索引类型；嵌入把每个索引送到它所指称的集合，并附上该集合属于 `W` 的证书。沿嵌入改标每个常元后，字母表上的每个词项与每条公式都成为以集合为常元的语法，从而适用已有的取值于 `V` 的编码，得到词项码 `ct` 与公式码 `cd`。由于该编码不查看元数，沿元数相等路径传输公式不会改变其码，这正是 `cd-subst` 所记录的事实。

本章的一切都在唯一一个类型论宇宙层级 `ℓ` 上进行，它只固定一次并贯穿全章。该层级上的集合层级 `V ℓ` 是最终编码的目标，而一阶语言则是参数所处的舞台。方案是统一的：给定可构造集合 `W`，把其成员读作常元符号，用抽象索引为它们命名，再把每个名字传输到它在 `V ℓ` 中指称的集合。这一方案不依赖于所选的 `W`，因此对任意的 `W` 通用。

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

open import Base.Prelude

module L.Coding.CodeAlphabet {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )
```

对象语言的语法对字母表是泛的。常元类型为 `K`、元数为 `n` 的公式类型 `Formula K n` 从不查看常元本身是什么，只把它们安排进逻辑结构中。因此，字母表上的任何函数都能扩充为语法的改标：把每个常元沿该函数映射，即可改写每一处出现，而联结词、量词与变量保持不变。这里所用的函数将是把成员索引嵌入 `V ℓ` 的映射，改标后的公式以集合为常元，恰好是层级上取值于集合的语法编码所要求的输入格式。剩下的只是选好字母表与嵌入，使这些常元确实是 `W` 的成员。

```agda
open import FOL.Syntax using ( Formula; Term )
open import FOL.Manipulation.ConstantMapping using ( mapFo; mapTm )
open import V.Coding {ℓ} using ( module VCode )
open import L.Constructible {ℓ} using ( 𝒮ʟ )

open import Cubical.Foundations.Prelude using ( J; substRefl )
```

两个区分组织了整个构造。其一，层级的集合的成员由 `⟪ a ⟫` 中的抽象索引 `q` 呈现，嵌入 `⟪ a ⟫↪` 把该索引送到它所指称的集合；索引是名字，值 `⟪ a ⟫↪ q` 是它在 `V ℓ` 中的指称，两种角色始终分开。其二，`W` 不是任意集合，而是可构造结构载体 `S` 的元素，因而带有层级中的底层集合 `fst W` 与可构造性证书；正是这一点使我们能把它的成员读作关于可构造集合的语言的参数。字母表将取为 `⟪ fst W ⟫` 本身，下一节把这些部件装配成码 `ct` 与 `cd`。

```agda
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Properties using
  ( ∈∈ₛ; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_ )

open hPropStructure 𝒮ʟ using ( S )
```

## 嵌入常元并编码语法

本节把可构造集合 `W` 取为载体 `S` 的一个元素，考察如何把 `W` 上的语法编码为集合。构造由三步复合而成：提取可用常元符号的类型 `Ab`，把每个符号嵌入层级 `V ℓ` 并附上它确实属于 `W` 的证书，然后对换标后的词项与公式施以取值于集合的编码。末尾的引理处理一个因公式按元数索引而产生的记账问题。

元素 `W : S` 把层级中的一个集合与结构数据打包在一起；`fst W` 是其底层集合。于是 `Ab` 就是 `⟪ fst W ⟫`，即该集合成员的索引类型，而 `ι` 是嵌入 `⟪ fst W ⟫↪`，把每个索引送到它在 `V ℓ` 中所指称的成员。因此 `Ab` 的元素恰好就是一个可用常元符号，`ι` 则算出它作为集合的指称。

```agda
module Alphabet (W : S) where
  Ab : Type ℓ
  Ab = ⟪ fst W ⟫

  ι : Ab → V ℓ
  ι = ⟪ fst W ⟫↪
```

隶属证书 `ι∈` 说明：对每个常元符号 `q`，集合 `ι q` 确实是 `fst W` 的成员；它由库中隶属关系与带分类的隶属关系 `∈ₛ` 之间的等价直接读出。字母表就位后，`cd` 与 `ct` 几乎是被逼出来的：`mapFo ι` 与 `mapTm ι` 把每处常元 `con q` 替换为 `con (ι q)` 来改写公式或词项，随后层级编码的括号 `⌜_⌝` 与 `⌜_⌝ᵗ` 把所得结果打包为集合。改标后公式的逻辑骨架原样保留，这正是能够复用该编码的原因。

```agda
  ι∈ : (q : Ab) → ⟨ ι q ∈ fst W ⟩
  ι∈ q = ∈∈ₛ {a = ι q} {b = fst W} .snd (∈ₛ⟪ fst W ⟫↪ q)

  cd : ∀ {n} → Formula Ab n → V ℓ
  cd ψ = VCode.⌜ mapFo ι ψ ⌝

  ct : ∀ {n} → Term Ab n → V ℓ
```

类型 `Formula Ab n` 的公式带有元数 `n`，而在依值类型论中该索引是类型的一部分。若某个证明稍后需要 `n` 与 `n'` 相等，它会沿路径 `e : n ≡ n'` 对公式作传输；传输后的公式在语法上是另一个居民，即便底层的公式未变。引理 `cd-subst` 表明这对编码毫无影响：作用于传输后公式的 `cd` 等于作用于原公式的 `cd`。证明对 `e` 使用 `J`，自反情形成立是因为沿 `refl` 的传输是恒等，而 `substRefl` 把这一化简显式化，剩下由 `cong cd` 把两次作用等同起来。

```agda
  ct t = VCode.⌜ mapTm ι t ⌝ᵗ

  cd-subst : ∀ {n n'} (e : n ≡ n') (ψ : Formula Ab n) → cd (subst (Formula Ab) e ψ) ≡ cd ψ
  cd-subst {n} e ψ = J (λ n' e' → cd (subst (Formula Ab) e' ψ) ≡ cd ψ)
    (cong cd (substRefl {B = Formula Ab} ψ)) e
```

## 小结

`Alphabet W` 把可构造集合 `W` 的成员看作一阶语言的常元符号，将每个成员嵌入外围层级并附上证书 `ι∈`，再通过 `ct` 与 `cd` 给出词项与公式所得的集合码。由于编码从不查看元数，`cd-subst` 保证了沿元数相等的路径传输公式不会改变其码。