---
title: "满足关系图公式"
module: L.Coding.SatisfactionGraph
lang: zh
site: "Bedrock"
description: "满足关系图公式"
stage: "内部编码：表与统一满足关系"
reading_order: 67
canonical: https://bedrock.institute/zh/L.Coding.SatisfactionGraph.html
html: L.Coding.SatisfactionGraph.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/SatisfactionGraph.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Coding.Model, L.Coding.Closure, L.Coding.Quantification, L.Coding.EnvironmentTower, L.Coding.CodeDomain, L.Coding.SatisfactionClauses]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/en/L.Coding.SatisfactionGraph.md, https://bedrock.institute/ja/L.Coding.SatisfactionGraph.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 满足关系图公式

递归构造 `Sat` 为每条公式指定一个由满足环境组成的集合，但这项元理论赋值不能直接在 `L` 上的一阶定义中被点名。本章的任务是给出一条对象语言二元公式，使它随后能够充当这类查询所用的关系。公式的见证将描述足以在查询键周围满足递归方程的局部数据，而不预先假设已经得到一张典范或单值的表。

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

下文使用的环境塔接口携带相应宇宙层级上的排中律假设，所以本章也取得这一假设。不过，本章组装公式时并不按命题作排中分类；公式中的量词与联结词都由已经建立的一阶语义解释。

```agda
open import Base.Prelude
open import Base.Classical using ( LEM )
```

固定宇宙层级与这一项经典参数。要定义的关系在公式键 `x` 与集合 `y` 处成立，恰好表示某张载体上的局部合格候选满足关系表在 `x` 处记录了 `y`。此处只断言这样的局部数据存在，既不选定典范表，也不证明每个键都有唯一取值。

```agda
module L.Coding.SatisfactionGraph {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
```

公式语言提供变元、常元、相等、合取与存在量化。常元使标签所用的标准数码等固定可构造集合能够直接出现在公式中，`pr` 则编码作为图条目的有序对。周遭层级提供解释这些公式的语义。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; con; _≐_; _∧̇_; ∃̇_ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )
```

三种描述组织候选数据。`appAt` 把编码对读作图条目，`domAt T C` 说明表 `T` 的键定义域恰为 `C`，`closedAt C` 则要求 `C` 中的复合公式键所需的直接子公式键仍在 `C` 中。`domAt` 所说的是表的键定义域，与后来作为表值出现的环境集不同。

```agda
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Coding.Model {ℓ} using ( domAt; appAt; appAt-adequate )
open import L.Coding.Closure {ℓ} using ( closedAt )
open import L.Coding.Quantification {ℓ} using
  ( f0; f1; f2; f3; f4; f5; f6; f7; f8; f9; i0; i1; i2; i3; i4; i5; i6; i7; i8; i9; i10; i11; i12; i13; sh )
```

其余描述为局部递归方程作准备。`towerAt` 提供编码环境的候选各行，`Tags` 校准十个构造子标签槽，`tableAt` 则合并候选键集上的命题截断全定义性、表条目的键限于该集合这一条件，以及十条局部外延方程。这些材料仍然只描述一项候选关系。`PinnedRecursion` 证明真正公式键处所需的条件唯一性，`SatisfactionBridge` 则独立地把属于外部取值 `Sat` 解释为在限制结构中得到满足。随后，`UniformSatisfaction` 在 `AllCodes B` 上把存在性与钉扎所得的唯一性结合起来，得到一张一致的表。

```agda
open import L.Coding.EnvironmentTower {ℓ} lem using ( nn; towerAt )
open import L.Coding.CodeDomain {ℓ} using ( Tags )
open import L.Coding.SatisfactionClauses {ℓ} using ( tableAt )
open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.FinData using ( toℕ )
```

具有 `n` 个自由位置的公式，其解释环境是由 `n` 个载体元素组成的向量。`lookup` 读取某个位置所赋的元素，cons 则在环境最内端加入新元素。借助这一固定约定，可以在任意外围环境之前放入十四个辅助见证，同时仍保留原来的查询位置。

```agda
open import Cubical.Data.Vec using ( _∷_; []; lookup )
```

对象语言的存在由命题截断解释。因此，存在公式的证明只保留见证存在这一事实，而忘掉具体使用了哪个见证。这对满足关系图至关重要：公开读式可以确认合适的标签、塔、键集与表存在，却不会暴露能让使用者全局选定某张候选表的数据。

```agda
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )
```

从现在起，`S` 表示可构造结构的载体：它的元素由一个层级集合及其可构造性证据组成。结构中的关系取命题值，尖括号取出其底层命题，而证明就是该命题的元素。因此，底层层级集合的相等或隶属必须与对象语言中断言相等或隶属的公式区别开来。

```agda
open hPropStructure 𝒮ʟ
```

判断 `γ ⊨ φ` 表示对象语言公式 `φ` 在可构造环境 `γ` 下成立，它把语义值组成的有限向量与公式语法连接起来。尤其要注意，用来查询某个键及其候选值的外围环境是元理论赋值，并不是环境塔中排列的某个编码环境集。

```agda
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
```

## 带守卫的递归框架

前四个名称描述十四个新位置的结构核心。由最内向外，它们依次容纳载体 `b`、候选满足关系表 `T`、候选键集 `C` 与候选环境塔 `E`。区分这些角色可以避免两种常见混淆：`C` 的元素是公式键，`T` 的元素编码键值对，而由 `E` 表示的各行按元数组织编码环境。

```agda
Bi Ti Ci Ei : ∀ {n} → Fin (14 + n)
Bi = i0
Ti = i1
Ci = i2
Ei = i3
```

接下来的十个位置是构造子标签。`NN` 给出统一的位置映射，先把零至三号构造子指标送到 `i4` 至 `i7`。在校准之前，这些位置可以含有任意载体元素，所以局部子句暂时只把它们当作辨认码形状的参数。

```agda
NN : ∀ {n} → Fin 10 → Fin (14 + n)
NN zero = i4
NN (suc zero) = i5
NN (suc (suc zero)) = i6
NN (suc (suc (suc zero))) = i7
```

同一映射依次延伸到八号构造子。统一索引之所以重要，是因为封闭性条件与十条表方程必须就每种公式构造子由哪个数码标记达成一致。校准完成后，同一子句族便能涵盖原子式、三种二元联结词、假、两种无界量词与两种有界量词。

```agda
NN (suc (suc (suc (suc zero)))) = i8
NN (suc (suc (suc (suc (suc zero))))) = i9
NN (suc (suc (suc (suc (suc (suc zero)))))) = i10
NN (suc (suc (suc (suc (suc (suc (suc zero))))))) = i11
NN (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) = i12
```

最后一条方程把九号构造子放在 `i13`，由最内向外的布局 `b, T, C, E, N0, ..., N9` 至此完整。环境塔只以候选集合 `E` 占据一个位置；它按元数索引的各行是由 `towerAt` 描述的编码条目，并不是这个向量中的另外十个位置。

```agda
NN (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))) = i13
```

查询键与候选值仍留在这十四个位置之外的调用方环境中。移位 `sh14` 把原位置越过全部十四个绑定，所以后来出现的 `appAt Ti (sh14 x) (sh14 y)` 仍是在询问原来的对 `(x,y)` 是否记录于 `T`。

```agda
sh14 : ∀ {n} → Fin n → Fin (14 + n)
sh14 i = sh 14 i
```

函数 `ev` 是这张位置映射的语义实现。它把 `b`、`T`、`C`、`E` 以及 `ν` 给出的十个值依次放在外围环境 `γ` 之前。因此，`Tags`、`towerAt`、`closedAt`、`domAt` 与 `tableAt` 所用的每个具名槽，在整个论证中始终指向同一个见证。

```agda
ev : ∀ {n} → (Fin 10 → S) → S → S → S → S → S ^ n → S ^ (14 + n)
ev ν E C T b γ =
  b ∷ T ∷ C ∷ E ∷ ν f0 ∷ ν f1 ∷ ν f2 ∷ ν f3 ∷ ν f4 ∷ ν f5
    ∷ ν f6 ∷ ν f7 ∷ ν f8 ∷ ν f9 ∷ γ
```

在典范标签赋值中，构造子指标 `k` 被送到模型数码 `nn (toℕ k)`。其底层层级集合是表示 `k` 的有限序数，第二分量则证明它可构造。把数码包装成 `S` 的元素以后，对象语言便能用常元点名它。

```agda
numν : Fin 10 → S
numν k = nn (toℕ k)
```

`Tags γ NN` 对每个构造子指标 `k` 询问：位置 `NN k` 上元素的底层集合是否为 `k` 的数码。在由 `numν` 构成的环境中，前四种情形都由自反性成立，因为查找与第一投影计算后正是该数码。该陈述比较底层集合，并不要求可构造性证书本身定义相等。

```agda
numTags : ∀ {n} (E C T b : S) (γ : S ^ n) → Tags (ev numν E C T b γ) NN
numTags E C T b γ zero = refl
numTags E C T b γ (suc zero) = refl
numTags E C T b γ (suc (suc zero)) = refl
numTags E C T b γ (suc (suc (suc zero))) = refl
```

四至八号指标的情形同样由自反性证明。较长的后继形式只承担有限指标的记账：`NN k` 选中 `numν k` 所在的槽，而后者的第一投影就是所需数码。因此，这项证明始终是逐点计算，不会引入针对某个构造子的额外语义假设。

```agda
numTags E C T b γ (suc (suc (suc (suc zero)))) = refl
numTags E C T b γ (suc (suc (suc (suc (suc zero))))) = refl
numTags E C T b γ (suc (suc (suc (suc (suc (suc zero)))))) = refl
numTags E C T b γ (suc (suc (suc (suc (suc (suc (suc zero))))))) = refl
numTags E C T b γ (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) = refl
```

九号指标穷尽 `Fin 10`，同一项自反性论证因而完成典范赋值满足 `Tags` 的全函数证明。其他赋值仍可充当候选见证，但必须自行携带这项逐点一致的证明，十条构造子子句才能取得预期标签。

```agda
numTags E C T b γ (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))) = refl
```

对象语言公式 `numsAt` 以向右结合的等式合取表达同一校准。前八条等式说明位置 `i4` 至 `i11` 的值依次为常元 `nn 0` 至 `nn 7`。因此，后面的变元载体版本不会用常元点名载体，但图公式仍会点名这些固定的标准数码。

```agda
numsAt : ∀ {n} → Formula S (14 + n)
numsAt =
  (var i4 ≐ con (nn 0)) ∧̇ ((var i5 ≐ con (nn 1)) ∧̇ ((var i6 ≐ con (nn 2)) ∧̇
  ((var i7 ≐ con (nn 3)) ∧̇ ((var i8 ≐ con (nn 4)) ∧̇ ((var i9 ≐ con (nn 5)) ∧̇
  ((var i10 ≐ con (nn 6)) ∧̇ ((var i11 ≐ con (nn 7)) ∧̇
```

关于 `i12` 与 `i13` 的等式以八、九两个数码完成校准。因此，满足整个合取恰好携带 `Tags` 所需的十条等式；接下来的读引理将从嵌套合取中取出它们。这项校准只认同构造子标签，并不宣称候选键集就是完整的良构公式码集。

```agda
  ((var i12 ≐ con (nn 8)) ∧̇ (var i13 ≐ con (nn 9))))))))))
```

`nums-out` 把 `numsAt` 的满足转成宿主层的 `Tags` 族。合取被解释为对，所以零号标签情形取第一投影，一号与二号情形则先沿第二投影进入，再取下一层的第一投影。该引理适用于任意标签赋值 `ν`，因而能读出任何候选图见证所携带的校准。

```agda
nums-out : ∀ {n} (ν : Fin 10 → S) (E C T b : S) (γ : S ^ n)
         → ⟨ ev ν E C T b γ ⊨ numsAt ⟩ → Tags (ev ν E C T b γ) NN
nums-out ν E C T b γ h zero = h .fst
nums-out ν E C T b γ h (suc zero) = h .snd .fst
nums-out ν E C T b γ h (suc (suc zero)) = h .snd .snd .fst
```

对每个更高指标，`nums-out` 都沿向右结合之积的第二投影深入，直到取得相应等式。这只是对合取的消去，既不选择标签值，也不证明其唯一。后续在命题截断下消去十四个存在见证时，这些投影会恢复公式满足中原已包含的标签证书。

```agda
nums-out ν E C T b γ h (suc (suc (suc zero))) = h .snd .snd .snd .fst
nums-out ν E C T b γ h (suc (suc (suc (suc zero)))) = h .snd .snd .snd .snd .fst
nums-out ν E C T b γ h (suc (suc (suc (suc (suc zero))))) = h .snd .snd .snd .snd .snd .fst
nums-out ν E C T b γ h (suc (suc (suc (suc (suc (suc zero)))))) = h .snd .snd .snd .snd .snd .snd .fst
nums-out ν E C T b γ h (suc (suc (suc (suc (suc (suc (suc zero))))))) = h .snd .snd .snd .snd .snd .snd .snd .fst
```

向右结合的合取最深处是关于八号与九号标签的一对等式。取出它的两个投影便补全逐点等式族，所以 `numsAt` 的满足会一次给出 `Fin 10` 每个指标处的一致。这一步只重新打包十条等式，不会给候选键集或候选表添加任何条件。

```agda
nums-out ν E C T b γ h (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) = h .snd .snd .snd .snd .snd .snd .snd .snd .fst
nums-out ν E C T b γ h (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))) = h .snd .snd .snd .snd .snd .snd .snd .snd .snd
```

反向读法 `nums-in` 从 `Tags` 出发：对每个构造子指标，所选标签与相应标准数码具有相同底集。按右结合的次序把这十条等式组成合取，便得到 `numsAt` 的满足。`nums-out` 与 `nums-in` 合在一起，使后文可以在对象语言的校准公式与宿主层的等式族之间双向转换。

```agda
nums-in : ∀ {n} (ν : Fin 10 → S) (E C T b : S) (γ : S ^ n)
        → Tags (ev ν E C T b γ) NN → ⟨ ev ν E C T b γ ⊨ numsAt ⟩
nums-in ν E C T b γ tg =
    tg f0 , (tg f1 , (tg f2 , (tg f3 , (tg f4 , (tg f5
  , (tg f6 , (tg f7 , (tg f8 , tg f9))))))))
```

辅助公式族 `satGraphOn` 现在把完整框架组装起来。参数 `pin` 是扩张环境上的一条公式，只规定新绑定的载体如何与外围参照相关；查询位置 `x` 与 `y` 仍留在外围环境中。十四层嵌套存在量词依次绑定十个标签、塔、键集、表，最后在最内层绑定载体。它们的第一个合取项就是 `pin`，所以改变载体的固定方式不会改变候选图的其他任何条件。

```agda
private
  satGraphOn : ∀ {n} → Formula S (14 + n)
             → Fin n → Fin n → Formula S n
  satGraphOn pin x y =
    ∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (( pin
```

pin 之后的合取列出解释一个表项所需的条件。校准公式 `numsAt` 把十个标签槽认同为标准数码。子句 `towerAt Ei Bi (NN f0)` 要求候选塔在被绑定载体上具备递归子句所需的各行结构，但不声称该塔是典范的。`closedAt Ci` 要求候选键集对七种可能的直接子公式键封闭。随后，`domAt Ti Ci` 断言表的键定义域恰为 `C`，而 `appAt Ti (sh14 x) (sh14 y)` 断言原查询对在 `x` 与 `y` 越过全部十四个绑定后仍是表的一项。

```agda
      ∧̇ ( numsAt
      ∧̇ ( towerAt Ei Bi (NN f0)
      ∧̇ ( closedAt Ci
      ∧̇ ( domAt Ti Ci
      ∧̇ ( appAt Ti (sh14 x) (sh14 y)
```

最后的合取项 `tableAt Ti Bi Ci Ei NN` 给出局部递归规格。它的第一项域条件说，`C` 中每个键都在命题截断下有某个取值；第二项说，`T` 的每个成员都能再次在命题截断下分解为 `C` 中的键与一个取值之对。余下十条子句分别对应一个公式构造子，用外延方程刻画所有匹配的表项。这些条件只在局部描述一张候选关系，既不使 `T` 成为单值关系，也不为每个键选出一个取值。真实公式键处的唯一性要到后面的 `PinnedRecursion` 中通过结构归纳证明。

```agda
      ∧̇ tableAt Ti Bi Ci Ei NN ))))))))))))))))))))
```

## 满足关系图的见证

宿主层类型 `GraphWitOn` 把同一份信息摊平成五项数据 `ν`、`E`、`C`、`T`、`b`，再接七份证书。它们依次断言 `b` 与参照 `W` 的底集相等、十个标签全部一致、塔子句、闭包子句与精确键定义域子句在组装环境中得到满足、查询对属于表的底集，以及 `tableAt` 得到满足。两份域证书在后文用途不同：`domAt` 让使用者从查询条目推出查询键属于 `C`，而 `tableAt` 内的全定义性在结构归纳中为子键提供取值。公开读法只在命题截断下暴露这份具体记录，因而只确立候选表存在，不选定其中一张。

```agda
private
  GraphWitOn : ∀ {n} → S → Fin n → Fin n → S ^ n → Type (ℓ-suc ℓ)
  GraphWitOn W x y γ =
    Σ[ ν ∈ (Fin 10 → S) ] (Σ[ E ∈ S ] (Σ[ C ∈ S ] (Σ[ T ∈ S ] (Σ[ b ∈ S ] ((fst b ≡ fst W) × (Tags (ev ν E C T b γ) NN × (⟨ (ev ν E C T b γ) ⊨ towerAt Ei Bi (NN f0) ⟩ × (⟨ (ev ν E C T b γ) ⊨ closedAt Ci ⟩ × (⟨ (ev ν E C T b γ) ⊨ domAt Ti Ci ⟩ × (⟨ pr (fst (lookup x γ)) (fst (lookup y γ)) ∈ fst T ⟩ × ⟨ (ev ν E C T b γ) ⊨ tableAt Ti Bi Ci Ei NN ⟩))))))))))
```

为了比较 `satGraphOn` 的满足与平坦记录，先固定 pin、它所参照的 `W`、两个查询位置及外围环境。除载体等式外，记录中的每个字段都已经在框架的合取项中有固定解释。因此，唯一额外需要的假设是 pin 的读法 `rd`：内向蕴含把等式 `fst b ≡ fst W` 变成 `pin` 的满足，外向蕴含则把 `pin` 的满足读回该等式。

```agda
  module _ {n : ℕ} (pin : Formula S (14 + n)) (W : S)
           (x y : Fin n) (γ : S ^ n) where
```

内向读式把一份被截断的见证记录变成整条框架的满足。它的假设 `rd` 说 pin 应当如何理解：对十个标签值、塔、索引集、表与载体的任何选择，若载体与参照一致，则 pin 在装配出的环境处得到满足。输入是一个截断，输出是一次满足、本身也是截断，故整个证明是截断内部的一个映射：它把那份平坦记录逐分量匹配，送往公式所要求的十四层见证。全程没有任何见证被选取；截断之间的映射只运送「见证存在」这一事实。

```agda
    graphOn-in : ((ν : Fin 10 → S) (E C T b : S) → fst b ≡ fst W
                   → ⟨ ev ν E C T b γ ⊨ pin ⟩)
               → ∥ GraphWitOn W x y γ ∥₁ → ⟨ γ ⊨ satGraphOn pin x y ⟩
    graphOn-in rd = PT.map
      (λ { (ν , (E , (C , (T , (b , (eb , (tg , (hE , (hc , (hd , (ha , h12))))))))))) →
```

平坦记录按布局的逆序重新嵌套。最外层的存在量词收到第九号构造子的标签，下一个收到第八号，依此下去，直到最内层的存在量词收到载体；这恰是布局的 de Bruijn 次序，由外向内读。pin 的满足由 `rd` 供给：把它施于装配好的诸见证与记录所携带的载体等式。校准则由 `nums-in` 从宿主层的一致转换成十条等式的满足，使后文每个合取项遇到的都是标准数码。

```agda
          ν f9
        , ∣ ν f8 , ∣ ν f7 , ∣ ν f6 , ∣ ν f5 , ∣ ν f4
        , ∣ ν f3 , ∣ ν f2 , ∣ ν f1 , ∣ ν f0 , ∣ E , ∣ C , ∣ T , ∣ b
        , ( rd ν E C T b eb
          , ( nums-in ν E C T b γ tg
```

三份守卫证书原样通过：它们是恰在框架装配的那个环境处读取的公式之满足，因此可以站在合取项所在的地方。查询条目是唯一必须换语言的分量。在宿主一侧它是寻常的隶属：两个查询值的有序对属于表的底层集合。应用原子的充分性律把该原子的满足认同为恰是这个隶属，证明沿那条唯一的路径作运输。这是内向方向唯一的实质性桥梁；其余一切只是重新打包。

```agda
          , ( hE
          , ( hc
          , ( hd
          , ( subst ⟨_⟩
                (sym (appAt-adequate Ti (sh14 x) (sh14 y) (ev ν E C T b γ))) ha
```

把子句族的证书放入最后一个合取项后，只需恢复各层嵌套的截断。`PT.map` 的调用提供最外层截断，因为它的映射函数返回最外层存在量词所需的见证对；这对之内的十三次显式写入则依次提供余下各层，直到载体。于是，这个构造把被截断的平坦记录变为十四层存在量词的满足，同时没有让任何已选数据逸出命题截断。

```agda
            , h12 ))))))
          ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ })
```

向外读式反走这段旅程，其假设 `rd` 这次反向运转 pin：从装配环境中 pin 的一次满足，恢复出载体等式。输入是整条框架的一次满足，其十四层存在量词全被截断；输出是被截断的见证记录。证明逐层消去那些存在量词，而每次消去都以记录的截断、一个命题为目标，故每一次都合法：这条引理从不声称产出记录本身，只声称产出一个记录存在这一事实。

```agda
    graphOn-out : ((ν : Fin 10 → S) (E C T b : S)
                    → ⟨ ev ν E C T b γ ⊨ pin ⟩ → fst b ≡ fst W)
                → ⟨ γ ⊨ satGraphOn pin x y ⟩ → ∥ GraphWitOn W x y γ ∥₁
    graphOn-out rd h = PT.rec squash₁ (λ { (n9 , h9) →
      PT.rec squash₁ (λ { (n8 , h8) →
```

每次应用 `PT.rec` 都消去一个被截断的标签见证，同时保持同一个命题目标 `∥ GraphWitOn W x y γ ∥₁`。因此，从九号至三号槽读出的取值可以传给下一层续体，却不能逸出为未截断的数据。正是对这项合法消去的重复使用，使对象语言的嵌套存在量词能够与一份平坦的截断记录对应。

```agda
      PT.rec squash₁ (λ { (n7 , h7) →
      PT.rec squash₁ (λ { (n6 , h6) →
      PT.rec squash₁ (λ { (n5 , h5) →
      PT.rec squash₁ (λ { (n4 , h4) →
      PT.rec squash₁ (λ { (n3 , h3) →
```

读出全部十个标签值以后，同一种命题性消去继续取得候选塔 `E` 与键集 `C`。名字 `hE'` 与 `hC'` 表示仍含有表、载体及各项证书的截断尾部，并不是塔条件或闭包条件的证明。那些证明仍留在最内层合取中，要等 `T` 与 `b` 也在截断内部显露后才会进入记录。

```agda
      PT.rec squash₁ (λ { (n2 , h2) →
      PT.rec squash₁ (λ { (n1 , h1) →
      PT.rec squash₁ (λ { (n0 , h0) →
      PT.rec squash₁ (λ { (E , hE') →
      PT.rec squash₁ (λ { (C , hC') →
```

在最内层，证明作映射而不再继续消去。剩下的是一个以载体记录为内容的截断，一个映射把它逐分量送往被截断的平坦见证。标签函数由十个已命名的位置经一个小函数重建，该函数定义在读式之下；而 `rd` 施于重建的函数、三个结构见证、载体与 pin 的满足，交出领衔记录的载体等式。此处的每个运算都留在截断之内：映射运送「一份记录存在」的事实，并在另一侧构造出对应的事实。

```agda
      PT.rec squash₁ (λ { (T , hT') →
      PT.map (λ { (b , (hpin , (hnum , (hE , (hc , (hd , (ha , h12))))))) →
        let ν : Fin 10 → S
            ν = ν' n0 n1 n2 n3 n4 n5 n6 n7 n8 n9
        in ν , (E , (C , (T , (b , (rd ν E C T b hpin
```

余下字段按平坦记录所需的方向恢复。校准合取项由 `nums-out` 读成宿主层的 `Tags` 等式族；塔、闭包与精确键定义域的满足已经具有所需类型，因而原样保留。查询原子的满足是唯一需要换回寻常隶属关系的字段：沿 `appAt-adequate` 搬运后，便得到查询有序对属于 `T` 的底集。

```agda
           , ( nums-out ν E C T b γ hnum
           , ( hE
           , ( hc
           , ( hd
           , ( subst ⟨_⟩
```

`tableAt` 的满足给出记录的最后一份证书。随后依次施用已经积累的续体，便完成各层嵌套消去，并得到 `∥ GraphWitOn W x y γ ∥₁` 的一个元素。两条读法合起来表明，框架的满足与一份合格平坦记录在命题截断下的存在互相蕴含。这只是两个命题之间的一对蕴含，并不是选取典范表的过程，也没有断言表值唯一。

```agda
                 (appAt-adequate Ti (sh14 x) (sh14 y) (ev ν E C T b γ)) ha
             , h12 )))))))))) })
        hT' }) hC' }) hE' }) h0 }) h1 }) h2 }) h3 }) h4 }) h5 }) h6 })
        h7 }) h8 }) h9 }) h
      where
```

存在公式把十个标签呈现为十个彼此分开的绑定值，而 `GraphWitOn` 需要一项函数 `Fin 10 → S`。局部函数 `ν'` 按构造子指标分类，把这两种呈现对齐。前四个分支依次返回 `a0` 至 `a3`；此处不使用任何语义事实，只使用构造子指标与刚从公式中读出的槽之间已经固定的对应。

```agda
      ν' : S → S → S → S → S → S → S → S → S → S → Fin 10 → S
      ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 zero = a0
      ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc zero) = a1
      ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc (suc zero)) = a2
      ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc (suc (suc zero))) = a3
```

对四号至八号构造子指标，同一分类依次返回相应命名的取值 `a4` 至 `a8`。这些分支遵循索引映射 `NN`，所以 `nums-out` 取出的等式恰能在表子句与闭包子句所期待的槽位上应用于重建后的函数。

```agda
      ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc (suc (suc (suc zero)))) = a4
      ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc (suc (suc (suc (suc zero))))) = a5
      ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc (suc (suc (suc (suc (suc zero)))))) = a6
      ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc (suc (suc (suc (suc (suc (suc zero))))))) = a7
      ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) = a8
```

九号指标的情形穷尽 `Fin 10`，使 `ν'` 成为全函数。于是，十四份彼此分开的对象语言见证在宿主记录中恰被表示为一个十项标签函数连同 `E`、`C`、`T` 与 `b`。这只是呈现方式的改变，既不产生新标签，也不丢弃任何存在数据。

```agda
      ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))) = a9
```

## 由变元提供载体

变元载体的见证类型从周遭环境中取得参照。在 `GraphWitAt B x y γ` 中，内部载体 `b` 只需与 `lookup B γ` 具有相同底集，并不要求两个带证明包装的元素本身相等。由于参照来自环境查找，后续公式即使在图的外面增添绑定并相应平移载体槽，仍可使用同一个见证类型。

```agda
GraphWitAt : ∀ {n} → Fin n → Fin n → Fin n → S ^ n → Type (ℓ-suc ℓ)
GraphWitAt B x y γ = GraphWitOn (lookup B γ) x y γ
```

公式 `satGraphAt B x y` 用 pin `var Bi ≐ var (sh14 B)` 实现这一参照：新绑定的载体槽与越过全部十四个内部绑定后的原载体槽相等。因此，这个实例不把载体嵌入为常元，不过 `numsAt` 中的十个标准数码常元仍然存在。公式保持不透明，使更大的描述可以把它作为一项完整关系使用；其见证读法则提供公开接口，用来建立或使用该公式的满足。

```agda
opaque
  satGraphAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
  satGraphAt B x y = satGraphOn (var Bi ≐ var (sh14 B)) x y
```

`satGraphAt` 的主体只在建立两条见证蕴含时展开。在这个作用域内，证明可以逐字段比较大型公式与 `GraphWitAt`；离开该作用域后，后续数学只使用 `graphAt-in` 与 `graphAt-out` 的精确陈述，因此十四个绑定始终只是同一关系的内部呈现。

```agda
opaque
  unfolding satGraphAt
```

对内向读法而言，pin 的读法假设就是恒等函数：变元等式的满足，恰是 `GraphWitAt` 中已经保存的底集等式。因此，在任意周遭环境中，一份命题截断下的见证记录都能给出 `satGraphAt` 的满足。`DefAt` 中的 `DefBody` 把图放在元素槽与两个相邻存在量词之下，`DenoteBody` 则让图越过五个新增槽取得同一个载体，这两处都具体使用了这种灵活性。在两种情形中，载体始终留在调用方的环境里，没有作为常元代入图公式。

```agda
  graphAt-in : ∀ {n} (B x y : Fin n) (γ : S ^ n)
             → ∥ GraphWitAt B x y γ ∥₁ → ⟨ γ ⊨ satGraphAt B x y ⟩
  graphAt-in B x y γ =
    graphOn-in (var Bi ≐ var (sh14 B)) (lookup B γ) x y γ (λ _ _ _ _ _ e → e)
```

外向读式补全了变元载体接口。从 `satGraphAt B x y` 的满足证明出发，它在命题截断之下恢复 `GraphWitAt B x y γ` 所记录的同一组候选数据与证书。尤其是，内部绑定的载体在底层集合上与外围槽 `B` 的取值一致，而所查询的键和值仍分别从外围槽 `x` 与 `y` 读取。传给 `graphOn-out` 的恒等函数恰好反映这项变元与变元之间的固定条件。使用者在证明命题时可以消去所得截断，后文的唯一性论证正是如此，但不能从中保留一座选定的塔、一个对子码封闭的键集或一张选定的表。

```agda
  graphAt-out : ∀ {n} (B x y : Fin n) (γ : S ^ n)
              → ⟨ γ ⊨ satGraphAt B x y ⟩ → ∥ GraphWitAt B x y γ ∥₁
  graphAt-out B x y γ =
    graphOn-out (var Bi ≐ var (sh14 B)) (lookup B γ) x y γ (λ _ _ _ _ _ h → h)
```

## 把载体固定为常元

当载体已经作为元素 `B` 给出时，第二个实例不再引用外围载体槽，而是使用常元 `B`。它恰有两个自由位置：`suc zero` 是输入键，`zero` 是候选输出值。框架的其余部分保持不变，所以这条公式仍只表示某组局部合格的候选数据记录了这次查询。具体而言，`SatisfactionClauses` 提供候选表的全定义性、键域限制以及十条局部方程；无论这些子句还是这个实例本身，都没有使该图成为单值关系。

```agda
opaque
  satGraph : S → Formula S 2
  satGraph B = satGraphOn (var Bi ≐ con B) (suc zero) zero
```

见证类型把这个二元关系的方向写得明确。在环境 `y ∷ x ∷ []` 中，最内层位置容纳 `y`，其次容纳 `x`；因此 `GraphWit B x y` 表示候选表含有以 `x` 为键、以 `y` 为值的编码对。它所参照的载体是固定元素 `B`。记录还包含经过校准的标签、候选环境塔、对子码封闭的候选键集、键定义域恰为该集合的表，以及 `tableAt` 所要求的证书。这里的键集只有局部封闭性；此定义并未把它认同为全部真正公式键组成的集合。

```agda
GraphWit : (B x y : S) → Type (ℓ-suc ℓ)
GraphWit B x y = GraphWitOn B (suc zero) zero (y ∷ x ∷ [])
```

常元固定条件同样具有两条见证蕴含，只在这个作用域内展开 `satGraph` 来证明。它们把大型存在公式化为一条稳定的二元关系：`graph-in` 从一份经过命题截断的候选记录建立该关系，`graph-out` 则从该关系恢复恰好这样的截断。`UniformSatisfaction` 正以这种形式把 `satGraph B` 用作抽象递归的图参数。

```agda
opaque
  unfolding satGraph
```

内向读式把通用转换用于常元固定条件。一份记录首先给出其中被绑定载体与 `B` 的底层集合相等；对象语言等式 `var Bi ≐ con B` 的满足恰好具有这一内容，所以固定条件的读式就是恒等函数。其余字段已经证明标签校准、塔与封闭条件、恰好的键定义域、所查询的表条目，以及打包后的表条件。通过 `graphOn-in` 映射这份记录时，命题截断始终保留：结论只证明合适的数据存在，并不选定一份供以后使用。

```agda
  graph-in : (B x y : S) → ∥ GraphWit B x y ∥₁ → ⟨ (y ∷ x ∷ []) ⊨ satGraph B ⟩
  graph-in B x y =
    graphOn-in (var Bi ≐ con B) B (suc zero) zero (y ∷ x ∷ []) (λ _ _ _ _ _ e → e)
```

外向读式反转这项转换，并为本章收尾：二元公式的一次满足只给出一份含有所查询条目的候选记录之命题截断。这正是满足关系图公式在本章中的边界。随后，`PinnedRecursion` 对一条真正的公式作结构递归，证明只要它的键属于候选键集，而且候选表在该键处记录了一个值，该值就与外部定义的 `Sat` 取值具有相同底层集合。`SatisfactionBridge` 另行赋予该取值以语义，把其中的隶属关系与限制结构中的满足联系起来。最后，`UniformSatisfaction` 在真正的定义域 `AllCodes B` 上使用 `satGraph B`；该域上的存在性与钉扎所得的唯一性共同满足抽象递归定理的条件，从而组装出一张一致的表。本章的两条读式提供后续论证所使用的表示关系，但自身既不选取表，也不证明表唯一，更不解释表的语义。

```agda
  graph-out : (B x y : S) → ⟨ (y ∷ x ∷ []) ⊨ satGraph B ⟩ → ∥ GraphWit B x y ∥₁
  graph-out B x y =
    graphOn-out (var Bi ≐ con B) B (suc zero) zero (y ∷ x ∷ []) (λ _ _ _ _ _ h → h)
```