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

常元域之间的函数作用于一阶语法的方式是：替换每个常元符号，而保持每个变量不变。本章在词项与公式上定义这个作用，证明它与复合相容，并把公式映射特殊化：以空类型为常元域的无参公式可由此进入任意常元域上的公式。

取公式 `var 0 ∈̇ con k` 这样的例子，它用两种方式指称两个对象：`var 0` 经自由变量指称，`con k` 则经常元域指称，这个常元域是某个类型 `K`。现在给定函数 `f : K → K'`，改名后的公式应当是什么样？自然的回答是：只有常元移动。`con k` 变为 `con (f k)`，而变量、属于关系与公式的整体形状保持原样。本章先在词项上、再在公式上定义这种改名，所用的类型 `Term` 与 `Formula` 及其全部构造子来自语法章：原子关系 `_∈̇_` 与 `_≐_`，联结词，以及包括有界形式 `∀̇∈`、`∃̇∈` 在内的量词。

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

module FOL.Manipulation.ConstantMapping where

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

有一种特殊的常元域值得单独注意：空类型 `⊥*`。常元域为 `⊥*` 的公式根本不含常元，本章末尾将研究这类公式如何映入任意 `K` 上的公式。在此之前，一切讨论都针对常元域之间的任意函数。

```agda
import Cubical.Data.Empty as Empty
```

## 语法层

语法对其常元域是函子式的：映射 `K → K'` 逐点穿过词项或公式，对常元改名，同时保持 de Bruijn 变量与逻辑结构不变。本节定义这个作用；复合法则在下一节证明。

在词项上，这个作用没有别的选择。`mapTm` 取改名函数 `f : K → K'` 和自由变量个数为 `n` 的词项，返回的词项仍有同样的个数 `n`：常元 `con k` 变为 `con (f k)`，变量 `var i` 原样返回。这只是对常元符号的改名，不是代入，对变量也没有任何作用。

```agda
mapTm : ∀ {ℓ ℓ'} {K : Type ℓ} {K' : Type ℓ'} {n}
      → (K → K') → Term K n → Term K' n
mapTm f (con k) = con (f k)
mapTm f (var i) = var i

mapFo : ∀ {ℓ ℓ'} {K : Type ℓ} {K' : Type ℓ'} {n}
```

原子公式显示了这一作用如何扩展到公式。`t ∈̇ u` 在 `mapFo` 下的像是 `mapTm f t ∈̇ mapTm f u`：同一关系施加于映射后的两个词项，自由变量个数仍是 `n`。于是我们的例子 `var 0 ∈̇ con k` 映为 `var 0 ∈̇ con (f k)`，其中只有常元移动了。

```agda
      → (K → K') → Formula K n → Formula K' n
mapFo f (t ∈̇ u)  = mapTm f t ∈̇ mapTm f u
mapFo f (t ≐ u)  = mapTm f t ≐ mapTm f u
mapFo f (φ ∧̇ ψ)  = mapFo f φ ∧̇ mapFo f ψ
mapFo f (φ ∨̇ ψ)  = mapFo f φ ∨̇ mapFo f ψ
```

量化公式表明逻辑结构不受影响。在 `mapFo` 下，量词前缀保持不变，其自由变量个数为 `suc n` 的主体被递归映射，个数仍是 `suc n`；每个联结词在映射后的子公式上重建。该操作既不增加也不删除约束词，任何构造子的形状都不会改变；不含常元的假 `⊥̇` 映到自身。

```agda
mapFo f (φ ⇒̇ ψ)  = mapFo f φ ⇒̇ mapFo f ψ
mapFo f ⊥̇        = ⊥̇
mapFo f (∃̇ φ)    = ∃̇ mapFo f φ
mapFo f (∀̇ φ)    = ∀̇ mapFo f φ
mapFo f (∀̇∈ t φ) = ∀̇∈ (mapTm f t) (mapFo f φ)
```

有界量词 `∀̇∈` 与 `∃̇∈` 是两种操作相遇的情形，因为它们同时结合词项与公式：约束词项 `t` 用 `mapTm` 改名，主体用 `mapFo` 映射。至此，`mapFo` 只变换语法，从不解释公式，也不触及环境。

```agda
mapFo f (∃̇∈ t φ) = ∃̇∈ (mapTm f t) (mapFo f φ)
```

连着两次这样的映射就是一次映射：先按 `f` 再按 `g` 映射，与按 `λ k → g (f k)` 一次映射，作为路径相等。常元域作用的这条函子性正是后续各章用来消去中间常元域的依据，它属于语法层，而不专属于任何一个应用。

复合法则是一个交换方阵。若一个词项先沿 `f : K → K'` 映射，再沿 `g : K' → K''` 映射，结果应当与沿复合函数 `λ k → g (f k)` 一次映射相一致。`mapTm-comp` 正是把这一点陈述为 `Term K'' n` 中的路径。在常元上，两边都计算为 `con (g (f k))`，一致已是定义等式，故该情形由 `refl` 证明；在变量上不出现常元，两边又是同一个词项。

```agda
mapTm-comp : ∀ {ℓ ℓ' ℓ''} {K : Type ℓ} {K' : Type ℓ'} {K'' : Type ℓ''} {n}
             (f : K → K') (g : K' → K'') (t : Term K n)
           → mapTm g (mapTm f t) ≡ mapTm (λ k → g (f k)) t
mapTm-comp f g (con k) = refl
mapTm-comp f g (var i) = refl
```

对公式，同一个方阵由 `mapFo-comp` 陈述：沿方阵两条路线的结果 `mapFo g (mapFo f φ)` 与 `mapFo (λ k → g (f k)) φ`，是同一类型 `Formula K'' n` 中的路径。由于方阵在词项上已证，原子情形无需对词项另作论证：同余 `cong₂` 把两条词项路径提升为重建的原子之间的路径。

```agda
mapFo-comp : ∀ {ℓ ℓ' ℓ''} {K : Type ℓ} {K' : Type ℓ'} {K'' : Type ℓ''} {n}
             (f : K → K') (g : K' → K'') (φ : Formula K n)
           → mapFo g (mapFo f φ) ≡ mapFo (λ k → g (f k)) φ
mapFo-comp f g (t ∈̇ u)  = cong₂ _∈̇_ (mapTm-comp f g t) (mapTm-comp f g u)
mapFo-comp f g (t ≐ u)  = cong₂ _≐_ (mapTm-comp f g t) (mapTm-comp f g u)
```

结构递归使方阵穿过联结词：每个子公式各携带方阵的一个实例，同余在两条子公式路径上重建联结词。假 `⊥̇` 既不含常元也不含子公式，两条路线都计算为同一公式，该情形就是 `refl`。

```agda
mapFo-comp f g (φ ∧̇ ψ)  = cong₂ _∧̇_ (mapFo-comp f g φ) (mapFo-comp f g ψ)
mapFo-comp f g (φ ∨̇ ψ)  = cong₂ _∨̇_ (mapFo-comp f g φ) (mapFo-comp f g ψ)
mapFo-comp f g (φ ⇒̇ ψ)  = cong₂ _⇒̇_ (mapFo-comp f g φ) (mapFo-comp f g ψ)
mapFo-comp f g ⊥̇        = refl
mapFo-comp f g (∃̇ φ)    = cong ∃̇_ (mapFo-comp f g φ)
```

量词情形结束归纳：前缀量词只作用于一个子公式，而有界形式 `∀̇∈` 与 `∃̇∈` 把词项与主体配对，同时用到词项路径与主体路径。由于 `Formula` 的每个构造子都已覆盖，复合法则方阵对每个公式成立。这条函子性是纯语法的事实，后续各章凡需消去中间常元域，皆可取用。

```agda
mapFo-comp f g (∀̇ φ)    = cong ∀̇_ (mapFo-comp f g φ)
mapFo-comp f g (∀̇∈ t φ) = cong₂ ∀̇∈ (mapTm-comp f g t) (mapFo-comp f g φ)
mapFo-comp f g (∃̇∈ t φ) = cong₂ ∃̇∈ (mapTm-comp f g t) (mapFo-comp f g φ)
```

这个映射最常用的实例从**没有**常元的域进入常元域。语法章介绍过**无参公式**，其常元域是空类型；类型 `Formula (⊥* {ℓ}) n` 已把定义说尽：这种类型的公式根本不含常元节点，但仍可使用其 `n` 个自由变量槽位中的任意一些。要改名进入类型 `K`，需要一个函数 `⊥* → K`，而空型正是这种函数唯一存在、且无需定义任何分支的类型：没有任何常元需要送往别处。这正是消去子 `Empty.rec*` 所提供的；沿它改名，就把无参公式映入任意常元域上的公式。

`embed` 正是 `mapFo Empty.rec*`：从空常元字母表出发的函数 `⊥* → K` 是唯一的，直接取它作改名，于是所有常元位置 (其实一个也没有) 都被送往某处。改变的只是常元域：长度为 `n` 的自由变量上下文与约束词都不变，因此 `embed` 既不封闭公式，也不为其中的变量提供环境。

```agda
embed : ∀ {ℓ ℓ'} {K : Type ℓ'} {n} → Formula (⊥* {ℓ}) n → Formula K n
embed = mapFo Empty.rec*
```

## 小结

`mapTm` 与 `mapFo` 表达常元域映射在语法层的作用：常元被改名，变量、约束词与个数均不变。`mapFo-comp` 证明该作用对复合是函子性的；`embed` 是无参实例，是后续常元改名与参数抽象的基础。