映射常元

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

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

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

module FOL.Manipulation.ConstantMapping where

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

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

import Cubical.Data.Empty as Empty

语法层

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

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

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)，其中只有常元移动了。

      → (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；每个联结词在映射后的子公式上重建。该操作既不增加也不删除约束词，任何构造子的形状都不会改变；不含常元的假 ⊥̇ 映到自身。

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 只变换语法，从不解释公式，也不触及环境。

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 证明；在变量上不出现常元，两边又是同一个词项。

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₂ 把两条词项路径提升为重建的原子之间的路径。

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。

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 的每个构造子都已覆盖，复合法则方阵对每个公式成立。这条函子性是纯语法的事实，后续各章凡需消去中间常元域，皆可取用。

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 既不封闭公式，也不为其中的变量提供环境。

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

小结

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