--- title: "名前の比較の妥当性" module: L.Choice.NameComparisonAdequacy lang: ja site: "Bedrock" description: "名前の比較の妥当性" stage: "正準整列順序と選択公理" reading_order: 80 canonical: https://bedrock.institute/ja/L.Choice.NameComparisonAdequacy.html html: L.Choice.NameComparisonAdequacy.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Choice/NameComparisonAdequacy.lagda.md prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, FOL.Manipulation.ConstantMapping, V.Hierarchy, V.Coding, L.Constructible, L.Ordinal, L.Axioms.Basic, L.Coding.Environment, L.Coding.Model, L.Coding.Expressions, L.Coding.EnvironmentSet, L.Coding.SatisfactionGraph, L.Coding.Satisfaction, L.Coding.SatisfactionBridge, L.Coding.CodeSet, L.Coding.UniformSatisfaction, L.Choice.CanonicalNames, L.Choice.FiniteStageOrders, L.Choice.NameComparison, L.WellOrder.Base] routes: [choice-completion] translations: [https://bedrock.institute/en/L.Choice.NameComparisonAdequacy.md, https://bedrock.institute/zh/L.Choice.NameComparisonAdequacy.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # 名前の比較の妥当性 同じ定義可能な部分集合が複数の名前をもつことがあります。したがって内部の比較には、論理式とそのパラメータを認識するだけでなく、表示された各集合をそれを指示する名前に結び付け、同じ集合を指示するすべての名前の中での最小性を表し、得られた最小名を比較することが必要です。本章では、対象言語の記述がこれらの役割を正確に果たすことを証明します。逆向きに読み取った名前は、命題的切り詰めの中に保たれます。 ```agda {-# OPTIONS --cubical --safe --guardedness #-} ``` 共通のプレリュードは、本書における宇宙、命題、有限添字、ベクトルの規約を与える。本章が明示する唯一の古典的仮定は排中律である。これは通常の型として取り込まれ、必要とする構成へ明示的に渡される。そのため、後で充足関係表や名前の順序を使っても、依存する仮定の境界を追跡できる。 ```agda open import Base.Prelude open import Base.Classical using ( LEM ) ``` したがって、モジュール全体が後続宇宙レベルの `lem` を携える。この仮定は、命名、有限構文コードの順序、統一充足関係を通して議論に入るが、命題的切り詰めから任意の証人を取り出す許可ではない。以下で示す妥当性は意図的に非対称である。具体的な名前から論理式を充足できる一方、充足する割り当てから読み戻せるのは、適切な名前が存在するという命題的に切り詰められた主張だけである。 ```agda module L.Choice.NameComparisonAdequacy {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where ``` この意味論的比較には、一つの構文と密接に関係する二つの構造が必要である。`Formula` は共通の対象言語であり、定数の改名によって、空の定数域、台の要素、外側の集合宇宙のあいだで論理式を移す。`V` 上の構造が外側の解釈を与え、その外延性は後に、所属命題の点ごとの一致を、二つの表示が指す集合の等しさへ変える。 ```agda open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula ) import FOL.Absoluteness open import FOL.Manipulation.ConstantMapping using ( mapFo; mapFo-comp; embed ) open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV ) ``` 名前は構成可能な台の上で解釈される有限な構文データなので、証明は符号化と `L` を結ばなければならない。論理式のコードは数項と対から組み立てられ、無パラメータ論理式のコードはすでに極限段階に属するため、`limitOrder` で比較できる。意味論の側では、構成可能性とその推移性が外側の集合を `L` 上の構造の要素として包み、内部の数項、空の構成可能集合、環境グラフが名前の論理式に現れる具体的な対象を与える。 ```agda open import V.Coding {ℓ} using ( pr; module VCode ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans ) open import L.Ordinal {ℓ} using ( #∈ω; ω-ord ) open import L.Axioms.Basic {ℓ} using ( ∅ʟ; LsetS ) open import L.Coding.Environment {ℓ} using ( env ) ``` モデル側の語彙は、まず名前のデータを表現し、まだ名前そのものを復元しない。`envOverAt` は、候補となる集合が、指定された定義域をもち、値が台に属し、対でない余分な要素を含まない一価グラフであることを述べる。その輸送補題により、これら三つの指定された集合をスロットの等式に沿って置き換えられる。`consAtL` は候補要素を環境へ加える方法を表し、`domAt` はその長さを記録し、`extAt` は要素によって指示対象を特徴づける。逆向きでは、環境グラフのこれらの条件が各パラメータ値を一意に定めるため、復元モジュールが決定的な役割を担う。 ```agda open import L.Coding.Model {ℓ} using ( envOverAt; envOverAt-transport; domAt ) open import L.Coding.Expressions {ℓ} using ( extAt-in; extAt-out; numL; consAtL ) open import L.Coding.EnvironmentSet {ℓ} lem using ( module Recover; envS; envOver ) open import L.Coding.SatisfactionGraph {ℓ} lem using ( satGraphAt ) open import L.Coding.Satisfaction {ℓ} lem using ( Sat ) ``` 次の橋は、台の上の論理式が統一充足関係表の値になる仕組みを説明する。台の要素を名指す定数はモデルへ定数改名され、その割り当ては環境と内部グラフの両方で表され、論理式は台のコード集合に属する真正な鍵で参照される。その鍵が `AllCodes` に属するという条件は欠かせない。そのような鍵で初めて、グラフの読みが記録値と実際の充足関係との一致を強制するからである。 ```agda open import L.Coding.SatisfactionBridge {ℓ} lem using ( consAtL-in; consAtL-out; asConst; values; envFor; envFor-graph ) renaming ( graph to envGraph ) open import L.Coding.CodeSet {ℓ} lem using ( keyS; AllCodes ) open import L.Coding.UniformSatisfaction {ℓ} lem ``` ここで数学的なインターフェースの全体像が見える。`CanonicalNames` はメタ言語の名前、そのコード、パラメータ・ベクトル、指示対象、三つの鍵による名前の順序を与え、`FiniteStageOrders` は第一の鍵を比較する順序を与える。`NameComparison` は、これから妥当性を示す対象言語の記述を与える。特に `NameAt` は、無パラメータな骨格、`ω` に属するアリティの数項、そのアリティを定義域として台に値を取るパラメータ・グラフ、指示対象の外延的な特徴づけという、ちょうど四つの概念的な連言項からなる。 ```agda using ( val-at; val-sat; keyIn; keyIn≡; keyIn∈; module Table ) open import L.Choice.CanonicalNames {ℓ} lem using ( module Naming; limitCode ) open import L.Choice.FiniteStageOrders {ℓ} lem using ( Limit; limitOrder ) open import L.Choice.NameComparison {ℓ} lem using ( NameAt; NameAt-in; LeastNameAt; ≺At; StepAt; StepOf; StepAt-in; StepAt-out; DenoteOf; DenoteBody; DenoteBody-in; DenoteBody-out ``` 残りのインターフェースは、混同してはならない三つの仕事を分ける。コード、グラフ、定義域の読みは、スロットに表現されたデータを復元する。`Adequacy` モジュールは、すでに与えられた二つの名前を、コード、アリティ、パラメータによって比較する。本章はさらに、任意の充足するスロット・データが名前に由来し、復元された名前が述べられた最小性をもつことを示す。ただし名前は命題的切り詰めの中に留まるので、ここでの読みの補題は証人を選ばない。具体的な最小名を得るのは下流だけであり、`InternalWellOrder` が充足を組み立てる向きで、既存の整列順序から構成された `leastNameOf` を使う。 ```agda ; FreeAt; codeFree-in; codeFree-out ; graphAt-value; graphAt-only ; domAt-numeral; domAt-fill; module Adequacy ) open import L.WellOrder.Base {ℓ-suc ℓ} using ( SWO ) ``` 証明では三種類の表示の変換を繰り返し用います。`Fin k` で添字づけられた族を長さつきベクトルとして表にまとめ、各成分を再び読み取ります。所属命題の論理的同値は、集合の外延性に必要なパスへ変換されます。さらに、証明を伴う台の間のパスに沿って、型がその台に依存する論理式の符号と充足関係集合を輸送します。これらの比較によって不可能だと分かる分岐は空型から除去します。 ```agda open import Cubical.Data.Vec.Properties using ( FinVec→Vec; FinVec→Vec→FinVec ) open import Cubical.Data.Vec using ( map ) open import Cubical.Functions.Logic using ( ⇔toPath ) open import Cubical.Foundations.Transport using ( constSubstCommSlice ) import Cubical.Data.Empty as Empty ``` 命題的切り詰めは、逆向きの読みがもつ強さを正確に記録する。証人が存在することは保つが、それがどの証人だったかは忘れ、除去できるのは行き先が命題である場合である。階層の操作はこの規律を補う。`⟪ A ⟫` は集合 `A` の要素を添字づける小さい型で、その埋め込みは添字を対応する要素へ送り、`∈-asFiber` は所属からそのような添字を復元する。したがって、一価性によって一意に定まる環境の成分はデータとして復元できるが、単に存在する論理式や名前を選択済みのデータへ変えることはできない。 ```agda import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁; squash₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ ) open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪; ∈∈ₛ; ∈ₛ⟪_⟫↪_; ∈-asFiber ) ``` アリティは von Neumann 自然数を通して意味論の境界を越える。メタ言語の自然数 `k` は集合論的な数項 `# k` で表され、`ω` はちょうどそれらの数項を含む。したがって、名前のアリティ条件は双方向に読め、名前比較の中央の鍵も、別の関係パラメータを加えず、一方の数項が他方に属することとして内部に表せる。 ```agda open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet ) open InfinitySet using ( #_; ω ) ``` `L` 上の命題値構造を開くことで、モデル要素の型 `S` と、以後すべての論理式が使う集合論的語彙が固定される。`S` の要素は、外側の集合と、それが構成可能であることの証拠からなる。したがって環境は証明を伴う構成可能集合を保存し、論理式の所属と等号は構造を通してその基礎となる外側の集合を調べる。 ```agda open hPropStructure 𝒮ʟ ``` 絶対性モジュールは、`V` 上の外側の構造と、構成可能集合を要素とする構造を結びます。以下の記法 `γ ⊨ φ` は、この構成可能な構造における環境 `γ` のもとでの充足関係を表します。したがって `γ` の各成分は、基礎となる集合とその構成可能性の証明をともにもち、既に得られた妥当性と絶対性の補題が、論理式の充足を基礎集合の所属および等しさに結び付けます。 ```agda module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ ) ``` ## ベクトルに関する一つの補題 残りの非公開添字は、外側のスロットが新しい量化子を越えてどのように残るかを記録する。論理式が二つの証人を導入してから元のスロットを参照するなら、de Bruijn 添字を二度持ち上げなければならない。`sh2` はまさにこの移動を行う。指示対象の議論で候補要素と拡張環境を順に束縛した後、元のパラメータ・グラフのスロットを参照するために使われる。 ```agda private sh2 : ∀ {n} → Fin n → Fin (suc (suc n)) sh2 i = suc (suc i) ``` 最小性は別の局所文脈を導入する。現在の名前が最小かを調べるため、対象言語は競合する骨格コード、アリティの数項、パラメータ・グラフを全称量化する。それまで使えた各スロットは三つ遠くなり、`sh3` が競合相手の三つのデータの下でそれらの参照を保つ一様な埋め込みとなる。 ```agda sh3 : ∀ {n} → Fin n → Fin (suc (suc (suc n))) sh3 i = suc (suc (suc i)) ``` 充足関係グラフを通して指示対象を読むと、この議論で最も深い局所文脈が生じる。元の環境の前には、候補要素、その拡張環境、環境の長さ、論理式の鍵、その鍵における表の値という五つの新しい値が置かれる。`sh5` は外側のスロットをこの五項すべての向こうへ運び、グラフの条件から元の台を参照できるようにする。 ```agda sh5 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc (suc n))))) sh5 i = suc (suc (suc (suc (suc i)))) ``` ステップの論理式は、比較を始める前に二組の完全な名前データを束縛する。各組は骨格コード、アリティの数項、パラメータ・グラフからなり、合わせて六つの新しい成分になる。`sh6` はすべての外側のスロットをこの枠の下へ埋め込み、二つの最小名条件と最後の名前比較が、同じ台、コード集合、関係スロット、比較対象について語り続けられるようにする。 ```agda sh6 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc (suc (suc n)))))) sh6 i = suc (suc (suc (suc (suc (suc i))))) ``` 六つの固定添字は、この局所的な枠の成分に名前を与える。存在証人は導入されるたびに環境の先頭へ積まれるので、第一の名前の骨格コード、アリティ、パラメータ・グラフは添字 5、4、3 にあり、第二の名前の骨格コードは添字 2 にある。これらの位置を一度記録しておけば、後のすべての参照を証人の導入順序と一致させられる。 ```agda s6a a6a e6a s6b a6b e6b : ∀ {n} → Fin (suc (suc (suc (suc (suc (suc n)))))) s6a = suc (suc (suc (suc (suc zero)))) a6a = suc (suc (suc (suc zero))) e6a = suc (suc (suc zero)) s6b = suc (suc zero) ``` 添字 1 と 0 には第二の名前のアリティとパラメータ・グラフが入り、局所環境は近い方から `p₂, k₂, s₂, p₁, k₁, s₁` という順序で完成する。この六つの束縛は `StepAt` 内部の二つの名前のデータであり、後に `InternalWellOrder.Stp` が束縛する六つの外側の証人とは別である。後者は、段階の塔、その定義可能冪集合、表の値、コード集合、コード順序、空アルファベットのコード集合を表す。内側の論理式がその使用側へ与えるのは局所的な名前比較であり、この時点では内部の整列順序を主張していない。 ```agda a6b = suc zero e6b = zero ``` 最初のベクトル補題は、成分ごとの写像の後に行う参照を正規化する。`map f v` の添字 `i` にある成分は、`v` の `i` 番目の成分へ `f` を適用したものにちょうど等しい。ベクトルについて帰納すると、先頭の場合は反射性で成り立ち、後尾の場合は帰納法の仮定へ帰着する。後ではこの等式により、台の添字と、それをモデル要素へ写した像とのあいだを曖昧さなく移動できる。 ```agda lookup-map : {ℓ' ℓ'' : Level} {X : Type ℓ'} {Y : Type ℓ''} (f : X → Y) {k : ℕ} (v : Vec X k) (i : Fin k) → lookup i (map f v) ≡ f (lookup i v) lookup-map f (x ∷ v) zero = refl lookup-map f (x ∷ v) (suc i) = lookup-map f v i ``` 第二のベクトル補題は、復元で使うもう一つの表示を正規化する。族 `g : Fin k → X` を `FinVec→Vec g` としてベクトル化し、添字 `i` を参照すると `g i` が返る。これは `lookup-map` の逆向きではない。二つの補題は異なる二つの表示層を取り除く。一方は成分ごとの写像を通した成分を露わにし、他方は表への変換を通した成分を露わにする。両者を合わせることで、復元された有限族と、名前に保存されたパラメータ・ベクトルが結ばれる。 ```agda lookup-tab : {ℓ' : Level} {X : Type ℓ'} {k : ℕ} (g : Fin k → X) (i : Fin k) → lookup i (FinVec→Vec g) ≡ g i lookup-tab g i j = FinVec→Vec→FinVec g j i ``` ## 本章のフレーム ここで局所モジュールは、以後のすべての読みに共通する数学的設定を固定する。外側の集合 `A` は `pA` と組み合わされ、構成可能構造の要素 `Aʟ` となる。`w` は、その要素を添字づける小さい型 `⟪ A ⟫` 上の整列順序である。台に関するスロットの等式では、証明を伴う要素 `Aʟ` を使う。後の論理式と輸送が依存するのはモデル要素全体であり、その第一射影だけではないからである。 ```agda module At (A : V ℓ) (pA : ⟨ isL A ⟩) (w : SWO ⟪ A ⟫) where private Aʟ : S Aʟ = A , pA ``` `Naming A w` を開くことで、妥当性の基準となるメタ言語の対象が固定される。名前は依存的な三つ組であり、アリティ `k`、`suc k` 個の変数位置をもつ無パラメータ論理式、`A` の要素をちょうど `k` 個並べたベクトルからなる。コードは論理式から得られ、指示対象は、そのパラメータのもとで論理式が `A` から切り出す部分集合である。名前の順序は、まず論理式コードを `limitOrder` で比較し、次にアリティを自然数の順序で比較し、長さが等しい場合にパラメータ・ベクトルを `w` によって辞書式に比較する。本章の残りは、スロットによる記述が命題の水準でこの比較を正確に復元することを、命題的切り詰めと所定の最小性条件を保ったまま証明する。 ```agda module NM = Naming A w ``` 構成可能な台とその整列順序を固定すると、相補的な二つのインターフェースが並びます。`Adequacy` は台の要素の埋め込み、名前のパラメータ族、比較を扱うモジュール `Keys` を与えます。`Naming` は名前、そのアリティ、無パラメータ論理式、パラメータ・ベクトル、さらにそれらから導かれるコード、拡張環境、指示対象を与えます。関係 `_≺ₙ_` は三つの鍵によって名前を比較します。 この区別は本章の結論の論理的な強さも定めます。`NameAt` の概念的な連言項は、骨格、アリティ、パラメータ・グラフ、指示対象の四つです。妥当性の内向きは与えられた名前からこれらを満たし、外向きは名前の存在を命題的に切り詰めた形でのみ返します。最小性は後で復元された名前の性質として現れ、特定の最小名を選ぶ操作は下流で行われます。`InternalWellOrder` がこの結果を使うときも、`StepAt` 内部の六つの束縛は二つの名前の三項組であり、`Stp` 外側の六つの基盤的な証人とは別の環境に属します。 ```agda open Adequacy A pA w using ( ix; pfam; module Keys ) open NM using ( Name; arity; formula; params; codeOf; denote; environment ; _≺ₙ_ ) ``` ## パラメータ列を埋める パラメータ・ベクトルは、まずメタ言語のデータから対象言語の環境へ移されます。族 `g : Fin k → ⟪ A ⟫` は、`k` 個の各添字に台の要素を一つ与えます。スロット `e`、`a`、`B` がそれぞれ、その要素を埋め込んだ値のグラフ、数項 `# k`、台 `A` を保持するなら、`envOverAt e a B` が充足されます。その四条件は、グラフが一価であり、定義域がちょうどその有限な数項であり、値が台に属し、順序対以外の要素を含まないことを述べます。 ```agda paramSeq-in : ∀ {n} (e a B : Fin n) (γ : S ^ n) (k : ℕ) (g : Fin k → ⟪ A ⟫) → fst (lookup e γ) ≡ env (λ i → ix (g i)) → fst (lookup a γ) ≡ # k → fst (lookup B γ) ≡ A → ⟨ γ ⊨ envOverAt e a B ⟩ ``` 三つの集合を任意のスロットへ置いた後で、四つのグラフ条件を証明し直す必要はありません。`Aʟ`、`# k`、`envS Aʟ g` を並べた標準的な環境は、添字二、一、零ですでにそれらを充足しています。`envOverAt-transport` は、与えられた三つの等しさに沿って、その充足関係を `γ` へ運びます。呼び出しで等しさの向きが反転しているのは、標準的な集合から出発して、指定されたスロットに保存された集合へ移るためです。 ```agda paramSeq-in e a B γ k g qe qa qB = envOverAt-transport (Aʟ ∷ (# k , numL k) ∷ envS Aʟ g ∷ []) γ (suc (suc zero)) (suc zero) zero e a B (sym qe) (sym qa) (sym qB) (envOver Aʟ g) ``` ## ベクトルとして読み戻す 逆向きの読みでは、`qa` と `qB` がアリティのスロットと台のスロットを固定し、`h` はスロット `e` の集合が環境条件を充足すると述べます。`e` のグラフ表示はあらかじめ仮定されていません。それを見つけることこそ、ここでの課題です。これらのデータで `Recover` を開くと、`Fin k` で添字づけられた族と、その標準的なグラフがもとの集合に等しいという証明が得られます。 ```agda module _ {n : ℕ} (e a B : Fin n) (γ : S ^ n) (k : ℕ) (qa : fst (lookup a γ) ≡ # k) (qB : fst (lookup B γ) ≡ A) (h : ⟨ γ ⊨ envOverAt e a B ⟩) where private module R = Recover Aʟ k γ e a B qa qB h ``` 復元された族は実際のデータなので、長さ `k` のベクトルに表としてまとめられます。ここで選択によって切り詰めを外しているわけではありません。各添字について、定義域条件は成分の単なる存在しか与えませんが、一価性により成分の型は命題になります。したがって、命題的切り詰めをその命題へ除去して、一意な成分を得られます。その値は `A` に属し、台の所属ファイバーが対応する `⟪ A ⟫` の要素を切り詰めなしで与えます。これらの要素に `FinVec→Vec` を適用したものが `paramSeq-out` です。 ```agda paramSeq-out : Vec ⟪ A ⟫ k paramSeq-out = FinVec→Vec R.g ``` 表への変換は族の表示を変えるため、グラフの等しさによって往復を閉じます。`R.recovers` は、スロット `e` の集合を復元された有限族のグラフと同一視します。続いて `FinVec→Vec` の参照則が、表にしたベクトルの各成分を対応する族の値と同一視します。関数外延性と `env` の合同性により、これらの点ごとのパスはグラフの等しさへ持ち上がります。したがって、復元されたベクトルはもとの環境集合を正確に表示し、順序対条件が排除する余分な要素も含みません。 ```agda paramSeq-graph : fst (lookup e γ) ≡ env (λ i → ix (lookup i paramSeq-out)) paramSeq-graph = R.recovers ∙ cong env (funExt (λ i → cong ix (sym (lookup-tab R.g i)))) ``` ## 四つの要素を構成箇所で不透明化する 指示対象の条件には、それ自身の四つの存在証人があります。これは `NameAt` の四つの概念的な連言項とは別です。第一の証人は、名前 `t` と候補となる台の要素 `m` から得られる環境です。`m` を `t` のパラメータ・ベクトルの先頭に置き、その拡張された割り当てをモデルの要素として表します。構成 `envFor Aʟ` は必要な構成可能性の証明も含むので、`envAt t m` は対象言語のスロットを占めることができます。 ```agda opaque envAt : Name → ⟪ A ⟫ → S envAt t m = envFor Aʟ (environment t m) ``` 対象言語の論理式が調べるのは、このモデル要素の基礎集合です。等式 `envAt-fst` はそれを `envGraph Aʟ (environment t m)`、すなわち候補をパラメータの前に置いた標準的なグラフと同一視します。この表示は、候補をもとのパラメータ環境へ加える論理式と、拡張環境の定義域を調べる論理式の両方に必要な形です。 ```agda envAt-fst : (t : Name) (m : ⟪ A ⟫) → fst (envAt t m) ≡ envGraph Aʟ (environment t m) envAt-fst t m = envFor-graph Aʟ (environment t m) ``` 第二の証人は、自然数を構成可能モデルの内部で表します。`numAt j` は von Neumann 数項 `# j` と、その構成可能性の証明 `numL j` を組にしてモデル要素を作ります。指示対象の議論では `j = suc (arity t)` として使われます。拡張環境には `arity t` 個のパラメータに加えて候補が一つ入るからです。 ```agda numAt : ℕ → S numAt j = # j , numL j ``` `numAt j` の基礎集合を射影すると定義によって `# j` が得られるので、`numAt-fst` は反射性で証明されます。この単純な等式が、拡張ベクトルのメタ言語での長さと `domAt` が見る集合論的な数項を結びます。この内向きでは数項を復号する必要はありません。 ```agda numAt-fst : (j : ℕ) → fst (numAt j) ≡ # j numAt-fst j = refl ``` 第三の証人は、統一充足関係が名前の論理式を保存する鍵です。`formula t` は定数をもたないので、`embed (formula t)` はそれを `A` の要素型を定数アルファベットとする論理式として見直すだけで、実際に定数を導入しません。`keyIn Aʟ` は得られた論理式の鍵を構成可能なモデル要素として包み、`keyAt t` を与えます。 ```agda keyAt : Name → S keyAt t = keyIn Aʟ (embed (formula t)) ``` 包まれた鍵とコード集合のインターフェースが使う鍵は、同じ基礎集合をもちます。等式 `keyAt-fst` は、`fst (keyAt t)` が `fst (keyS Aʟ (embed (formula t)))` に等しいことを正確に述べます。これにより、後の所属とグラフの議論では抽象的なモデル要素をスロットに置きながら、`keyS` が与える具体的な順序対コードについて推論できます。 ```agda keyAt-fst : (t : Name) → fst (keyAt t) ≡ fst (keyS Aʟ (embed (formula t))) keyAt-fst t = keyIn≡ Aʟ (embed (formula t)) ``` 同じ鍵が `AllCodes Aʟ` に属することも証明されます。この所属は意味論的な条件であり、余分な帳尻合わせではありません。充足関係のグラフが意図した値をもつことを要求されるのは真正な論理式の鍵においてであり、コード領域の外での振る舞いは問題にされないからです。したがって、表の `keyAt t` における値を `t` の論理式の充足関係として読めるのは `keyAt-∈` によります。 ```agda keyAt-∈ : (t : Name) → ⟨ keyAt t ∈ˢ AllCodes Aʟ ⟩ keyAt-∈ t = keyIn∈ Aʟ (embed (formula t)) ``` 第四の証人は、統一充足関係の表がその真正な鍵で与える値です。`Table.val Aʟ Aʟ` は鍵と、それがコード領域に属する証明を受け取り、構成可能なモデル要素を返します。後で `val-sat` により、その基礎集合は `embed (formula t)` を充足する `A` 上の符号化環境全体と同一視されます。ここで `valAt` は、その同一視に必要な表の参照を記録します。 ```agda valAt : Name → S valAt t = Table.val Aʟ Aʟ (keyAt t) (keyAt-∈ t) ``` `valAt t` はこの表の参照そのものとして定義されているので、`valAt-val` は反射性で成り立ちます。この等式を明示することで、指示対象の議論は、第四の名前つき証人と `Table.val` に関する一般定理のあいだを直接移れます。これで四つの構成は、`DenoteOf` が束縛する証人をちょうど与えます。すなわち、拡張環境、その長さの数項、真正な論理式の鍵、その鍵における表の値です。 ```agda valAt-val : (t : Name) → valAt t ≡ Table.val Aʟ Aʟ (keyAt t) (keyAt-∈ t) valAt-val t = refl ``` ## 名前の論理式の鍵 記述が作る鍵と表が使う鍵を比較するため、まず無パラメータ論理式に対する定数の付け替えを調べます。論理式 `χ` の定数は空型から取られます。これを周囲の宇宙へ直接埋め込む場合と、いったん台へ埋め込んでから台の要素を宇宙へ写す場合に使う関数は、どちらも空型を定義域とします。関数外延性により両者は等しくなり、`mapFo` の合成則から `sameEmbed χ` が得られます。これは空の定数アルファベットについての事実であり、任意の論理式が任意の定数の付け替えで不変だという主張ではありません。 ```agda private sameEmbed : ∀ {m} (χ : Formula (⊥* {ℓ}) m) → mapFo ⟪ A ⟫↪ (embed χ) ≡ embed χ sameEmbed χ = mapFo-comp Empty.rec* ⟪ A ⟫↪ χ ∙ cong (λ f → mapFo f χ) (funExt (λ b → Empty.rec* b)) ``` `m` 個の変数位置をもつ論理式の表の鍵は、数項 `# m` と、定数を周囲の宇宙へ写した後の論理式コードとの順序対です。`sameEmbed` により、その付け替えられた論理式は `χ` の直接の埋め込みであり、そのコードは `limitCode χ` の基礎集合です。そこで符号化操作の合同性を使うと `keyCode` が得られます。名前については `m = suc (arity t)` なので、この等式は表の鍵を、拡張環境の長さと骨格コードからなる対にちょうど合わせます。 ```agda keyCode : ∀ {m} (χ : Formula (⊥* {ℓ}) m) → fst (keyS Aʟ (embed χ)) ≡ pr (# m) (fst (limitCode χ)) keyCode χ = cong (λ u → pr (# _) VCode.⌜ u ⌝) (sameEmbed χ) ``` 指示対象の証明には、パラメータ環境の二つの同値な表示も必要です。族 `pfam t` は各有限添字を、対応するパラメータの基礎となる周囲の集合へ送ります。もう一つの表示では、命名モジュールの埋め込み `NM.DA.ι` を `params t` に成分ごとに施してモデル要素のベクトルを作り、その標準的なグラフ `envGraph Aʟ` を取ります。ベクトルの写像に関する参照則が両者の値を点ごとに同一視し、関数外延性と `env` の合同性から、二つの環境グラフの等しさ `valuesOf t` が得られます。 ```agda valuesOf : (t : Name) → env (pfam t) ≡ envGraph Aʟ (map NM.DA.ι (params t)) valuesOf t = cong env (funExt (λ i → sym (cong fst (lookup-map NM.DA.ι (params t) i)))) ``` 拡張環境の各成分は構成可能です。添字 `i : Fin (suc (arity t))` は候補またはパラメータの一つを選びます。どちらの場合も、`lookup i (environment t m)` は、その基礎集合が `A` に属するという証明をすでに伴っています。`A` が構成可能なので、構成可能性の推移性から `valuesL t m i` が得られます。この点ごとの事実が、`domAt` が拡張環境の定義域を確かめる際に必要な構成可能性の前提を与えます。 ```agda valuesL : (t : Name) (m : ⟪ A ⟫) (i : Fin (suc (arity t))) → ⟨ isL (values Aʟ (environment t m) i) ⟩ valuesL t m i = isL-trans (snd (lookup i (environment t m))) pA ``` ## 表示を双方向に読む 指示対象への所属を対象言語の条件と比較する前に、`denote t` のすべての要素が台に属することを確かめます。この指示対象への所属は、その拡張環境が論理式を充足する台の添字 `mm` と、表された台の要素から周囲の集合 `y` へのパスが単に存在することを与えます。この証人は命題的に切り詰められていますが、目標 `y ∈ A` 自体が命題なので、`PT.rec` は添字を選択して保持することなく、その証人を利用できます。 ```agda private denoteMem : (t : Name) (y : V ℓ) → ⟨ y ∈ denote t ⟩ → ⟨ y ∈ A ⟩ denoteMem t y = PT.rec (snd (y ∈ A)) step where step : Σ[ p ∈ Σ[ mm ∈ ⟪ A ⟫ ] ⟨ NM.satAt t mm ⟩ ] (⟪ A ⟫↪ (p .fst) ≡ y) ``` 許された切り詰めの除去の内部では、復元されたデータは対 `p` と等式 `q` です。`p` の第一成分は `A` の具体的な要素添字なので、標準的な小さい所属の証人を `∈∈ₛ` で変換すれば、その埋め込み像が `A` に属することが分かります。この所属を `q` に沿って輸送すると `y ∈ A` が得られます。ここで使うのは所属の表示と、行き先が命題であるという事実だけです。選択関数も新たな古典的推論も導入しません。 ```agda → ⟨ y ∈ A ⟩ step (p , q) = subst (λ u → ⟨ u ∈ A ⟩) q (∈∈ₛ {a = ⟪ A ⟫↪ (p .fst)} {b = A} .snd (∈ₛ⟪ A ⟫↪ (p .fst))) ``` モジュール `Named` はここで、`NameAt` の四つのデータをメタ言語の名前と比較するためのスロットを固定します。台 `B`、台のコード集合 `C`、空のアルファベットに対するコード集合 `C₀`、骨格 `s`、アリティ `a`、パラメータ・グラフ `e`、指示対象 `d` です。台についての等式 `qB` は構成可能性の証明を含むモデル要素全体の等しさですが、`qC` と `q₀` は基礎集合だけを同一視します。この違いは用途から生じます。以下の論理式はスロット `B` にあるモデル要素の要素型の上で型づけられますが、`C` と `C₀` へのコード集合の所属が見るのは基礎集合だけです。 ```agda module Named {n : ℕ} (B C C₀ s a e d : Fin n) (γ : S ^ n) (qB : lookup B γ ≡ Aʟ) (qC : fst (lookup C γ) ≡ fst (AllCodes Aʟ)) (q₀ : fst (lookup C₀ γ) ≡ fst (AllCodes ∅ʟ)) where private ``` `Fo` は、論理式の台へのこの依存を切り出します。モデル要素 `X` とアリティ `j` に対して、`Fo X j` は、小さい要素型 `⟪ fst X ⟫` から定数を取る論理式の型です。したがって、スロットに保存された台の上で読む論理式は、意味論的な比較を始める前から正しい型をもちます。後になって基礎集合の等しさだけで、この依存する台を置き換えることはできません。 ```agda Fo : S → ℕ → Type ℓ Fo X j = Formula ⟪ fst X ⟫ j ``` 名前 `t` に対して、まず無パラメータ論理式 `formula t` を、固定した台 `A` の要素を定数として許す論理式へ埋め込みます。もとの定数域は空なので、実際のパラメータは追加されません。次に、その型を `sym qB` に沿って `Fo Aʟ` から `Fo (lookup B γ)` へ輸送し、`ψAt t` を得ます。この輸送が可能なのは、`qB` が台のモデル要素全体を同一視するからです。こうして得られたスロット相対的な論理式について、その鍵と充足関係の値を、上で作った固定台上の構成と比較できるようになります。 ```agda ψAt : (t : Name) → Fo (lookup B γ) (suc (arity t)) ψAt t = subst (λ X → Fo X (suc (arity t))) (sym qB) (embed (formula t)) ``` 記述で使う論理式は、まず固定された台 `Aʟ` からスロット `B` に格納された台へ輸送されます。論理式の型そのものが台に依存するため、`qB` は基礎集合だけでなく、証明を伴う台全体を同一視しなければなりません。`qB` に関するパス帰納法により、符号集合の鍵を作る操作がこの輸送と可換であることが分かります。したがって、スロットの台で `ψAt t` から得る鍵と、`Aʟ` で `embed (formula t)` から得る鍵は同じ集合です。 ```agda keyψ : (t : Name) → fst (keyS (lookup B γ) (ψAt t)) ≡ fst (keyS Aʟ (embed (formula t))) keyψ t = sym (constSubstCommSlice (λ X → Fo X (suc (arity t))) (V ℓ) (λ X ψ → fst (keyS X ψ)) (sym qB) (embed (formula t))) ``` 統一充足関係の値にも同じ依存性があります。スロットの台では、輸送された論理式の定数をその台へ改名してから `Sat` を適用します。`Aʟ` では、対応する埋め込み済みの論理式を改名して `Sat` を適用します。`qB` に沿う代入はこの構成全体と可換なので、二つの充足関係集合の基礎集合は等しくなります。 ```agda satψ : (t : Name) → fst (Sat (lookup B γ) (mapFo (asConst (lookup B γ)) (ψAt t))) ≡ fst (Sat Aʟ (mapFo (asConst Aʟ) (embed (formula t)))) satψ t = sym (constSubstCommSlice (λ X → Fo X (suc (arity t))) (V ℓ) (λ X ψ → fst (Sat X (mapFo (asConst X) ψ))) ``` パス帰納法の原理へ最後に渡す引数は、埋め込まれた論理式そのものです。これで `satψ` の証明が閉じます。ここに独立な意味論的選択はなく、等式は依存的な構成で台を代入することだけから従います。`keyψ` と `satψ` を合わせると、後の表示の議論は、論理式の鍵とその充足関係集合を揃えたまま、スロットの台と `Aʟ` の間を移動できます。 ```agda (sym qB) (embed (formula t))) ``` 固定したメタ言語の名前 `t` に対して、`Data t` はそれを表すために必要な四つのスロット等式を記録します。骨格のスロットは `codeOf t` の基礎集合を、アリティのスロットは `# (arity t)` を、パラメータのスロットは環境グラフ `env (pfam t)` を、表示のスロットは `denote t` を保持します。この四つの等式は `NameAt` の四つの概念的な連言項に対応します。ここで述べるのは現在のスロットがこの特定の名前と揃っていることであり、同じ指示対象をもつすべての名前の一意性ではありません。 ```agda Data : Name → Type (ℓ-suc ℓ) Data t = (fst (lookup s γ) ≡ fst (codeOf t)) × ( (fst (lookup a γ) ≡ # (arity t)) × ( (fst (lookup e γ) ≡ env (pfam t)) × (fst (lookup d γ) ≡ denote t) ) ) ``` 表示の条件を `denote t` と比較するため、モジュール `Body` は `t` と `Data t` の最初の三成分を固定します。骨格の等式 `qs` が論理式の鍵をそろえ、パラメータの等式 `qe` がパラメータ・グラフをそろえます。アリティの等式 `qa` は同じ名前について残るスロットの対応を記録しますが、`t` が固定された後の表示の議論では、拡張環境の長さを `suc (arity t)` として直接得ます。非公開のベクトル `δp` は、充足関係の橋が要求する制限された意味論的な台の中でパラメータを表します。 ```agda module Body (t : Name) (qs : fst (lookup s γ) ≡ fst (codeOf t)) (qa : fst (lookup a γ) ≡ # (arity t)) (qe : fst (lookup e γ) ≡ env (pfam t)) where private δp : Vec NM.DA.SM (arity t) ``` 名前のパラメータは、すでに小さな要素型 `⟪ A ⟫` に属しています。それぞれに `NM.DA.ι` を写す操作は、添字を保つだけではありません。各添字が表す集合に、その集合が `A` に属する証明を組み合わせて、制限モデルの台 `NM.DA.SM` の要素にします。得られるベクトル `δp` の長さは `arity t` であり、名前の論理式を評価する内側の環境の尾部そのものです。 ```agda δp = map NM.DA.ι (params t) ``` スロット等式 `qe` は外側のパラメータ族 `pfam t` によって同じパラメータを記述しますが、充足関係の橋が必要とするのは、制限された台のベクトル `δp` のグラフです。等式 `valuesOf t` は二つの表現を成分ごとに同一視します。これを `qe` と合成して得る `qd'` は、パラメータのスロットがちょうど `envGraph Aʟ δp` を含むことを述べます。この形は、拡張環境を作るときにも、後で与えられた拡張環境を識別するときにも使われます。 ```agda qd' : fst (lookup e γ) ≡ envGraph Aʟ δp qd' = qe ∙ valuesOf t ``` 表示の中身にある第四の条件は、その鍵を同一視します。封印された要素 `keyAt t` から始めると、`keyAt-fst` が埋め込まれた論理式の符号集合の鍵を取り出し、`keyCode` がその鍵を `# (suc (arity t))` と論理式の極限段階コードとの順序対として計算します。骨格の等式 `qs` は第二成分をスロット `s` の集合で置き換えます。残るのは、第一成分を封印された長さの数項によって表すことです。 ```agda qkey : fst (keyAt t) ≡ pr (fst (numAt (suc (arity t)))) (fst (lookup s γ)) qkey = keyAt-fst t ∙ keyCode (formula t) ∙ cong (pr (# (suc (arity t)))) (sym qs) ∙ cong (λ u → pr u (fst (lookup s γ))) ``` 最後の合同性では `numAt-fst` を逆向きに使い、順序対の中の集合論的な数項を `numAt (suc (arity t))` の基礎集合で置き換えます。完成した `qkey` は `DenoteOf` が要求する形そのものです。選んだ鍵は、選んだ定義域の数項と骨格のスロットとの対です。逆向きの証明では、中身に含まれる鍵の等式から同じ計算を組み立て直します。 ```agda (sym (numAt-fst (suc (arity t)))) ``` 順方向では、実際の要素 `m : ⟪ A ⟫`、それと同じ基礎集合を表す外側の要素 `z`、そしてその集合が `denote t` に属するという証明から始めます。`DenoteOf` の四つの証人を意味の順に与えます。すなわち、パラメータの前に `m` を加えた環境、その長さの数項、論理式の鍵、その鍵での表の値です。これらを結ぶ条件は六つあります。最初の五つは形と対応を記述し、最後の一つが、仮定した表示への所属を、環境が表の値に属するという所属へ変換します。 ```agda denote-fill : (z : S) (m : ⟪ A ⟫) → ⟪ A ⟫↪ m ≡ fst z → ⟨ ⟪ A ⟫↪ m ∈ denote t ⟩ → DenoteOf B C s e γ z denote-fill z m qm hz = envAt t m , (numAt (suc (arity t)) , (keyAt t , (valAt t , ( hcons , (hdom , (hkey , (qkey , (hgraph , hmem)))))))) ``` 第一の条件は、選んだ環境が候補の要素をパラメータ環境へ加えて得られることを述べます。`consAtL` の内向きの読みには、元のパラメータグラフを与える `qd'`、スロット `z` の候補集合を同一視する `sym qm`、新しく作った環境グラフを与える `envAt-fst t m` を渡します。すると対象言語の拡張論理式が証明されます。これにより、論理式の余分な変数スロットには候補の要素が入り、その後に元のパラメータが続くことが保証されます。 ```agda where hcons : ⟨ (envAt t m ∷ z ∷ γ) ⊨ consAtL zero (suc zero) (sh2 e) ⟩ hcons = consAtL-in Aʟ δp (NM.DA.ι m) (envAt t m ∷ z ∷ γ) zero (suc zero) (sh2 e) qd' (sym qm) (envAt-fst t m) ``` 第二の条件は、拡張環境の定義域を定めます。その長さは `suc (arity t)` です。候補の要素のための一つの位置に、`arity t` 個のパラメータ位置が続きます。`domAt` の内向きの妥当性補題には、`environment t m` の基礎となる値と、それぞれの値が構成可能であることの証明を渡します。後者は、それらの値が構成可能な台に属することと、`L` の推移性から従います。 ```agda hdom : ⟨ (numAt (suc (arity t)) ∷ envAt t m ∷ z ∷ γ) ⊨ domAt (suc zero) zero ⟩ hdom = domAt-fill (suc zero) zero (numAt (suc (arity t)) ∷ envAt t m ∷ z ∷ γ) (suc (arity t)) (values Aʟ (environment t m)) (valuesL t m) ``` 同じ定義域の補題は、選んだ証人を、それが比較すべき基礎集合としても見る必要があります。等式 `envAt-fst t m` は `envAt t m` の下にある環境グラフを取り出し、`numAt-fst (suc (arity t))` は長さの証人の下にある期待された von Neumann 数項を取り出します。この二つの射影等式により、定義域の論理式は、その数項が選んだ環境の長さを符号化することを正確に述べます。 ```agda (envAt-fst t m) (numAt-fst (suc (arity t))) ``` 第三の条件は、選んだ鍵を真正な符号領域に置きます。構成 `keyAt` はすでに、その鍵が `AllCodes Aʟ` に属することを与えます。スロット等式 `qC` に沿ってこの所属を輸送すれば、スロット `C` に格納された集合への所属が得られます。この仮定は省けません。充足関係グラフが論理式の意味論的な値を与えることを強制されるのは真正な符号の鍵においてであり、符号領域の外での振る舞いはそのような値を定める必要がないからです。 ```agda hkey : ⟨ fst (keyAt t) ∈ fst (lookup C γ) ⟩ hkey = subst (λ u → ⟨ fst (keyAt t) ∈ u ⟩) (sym qC) (keyAt-∈ t) ``` 第五の条件は、選んだ値が、選んだ鍵で充足関係グラフに許される値であることを述べます。グラフの論理式を評価するとき、外側の割り当ての前には、値、鍵、長さの数項、拡張環境、候補の要素という五項が順に置かれています。第一の対応条件は、`keyAt t` の基礎集合を、スロットの台における `ψAt t` の鍵と同一視します。先に示した `keyψ` は、まさにここで鍵の計算を `qB` に沿って台の境界の向こうへ運びます。 ```agda hgraph : ⟨ (valAt t ∷ keyAt t ∷ numAt (suc (arity t)) ∷ envAt t m ∷ z ∷ γ) ⊨ satGraphAt (sh5 B) (suc zero) zero ⟩ hgraph = graphAt-value (sh5 B) (suc zero) zero (valAt t ∷ keyAt t ∷ numAt (suc (arity t)) ∷ envAt t m ∷ z ∷ γ) (ψAt t) ``` 第二の対応条件は、選んだ値を同一視します。まず `valAt-val` が、それを `keyAt t` における表の値として取り出します。法則 `val-at` は、その表の値を `Aʟ` 上の埋め込まれた論理式の `Sat` 集合と同一視します。最後に `satψ` を必要な向きに読んで、この集合をスロットの台へ輸送します。二つの対応等式が揃うと、`graphAt-value` は論理式の鍵とその意味論的な値を変えることなく、グラフの条件を証明できます。 ```agda (keyAt-fst t ∙ sym (keyψ t)) ( cong fst (valAt-val t) ∙ cong fst (val-at Aʟ Aʟ (embed (formula t)) (keyAt t) (keyAt-∈ t) (keyAt-fst t)) ∙ sym (satψ t) ) ``` 第六の条件は決定的な所属です。符号化された拡張環境は、選んだグラフの値に属さなければなりません。仮定は、`m` が表す要素が `denote t` に属することを述べます。特徴づけ `NM.denote-mem t m` は、これを `environment t m` が `embed (formula t)` を内側で充足することへ変えます。したがって表示への所属は、統一充足関係表が記録すべき意味論的な事実をちょうど与えます。 ```agda hmem : ⟨ fst (envAt t m) ∈ fst (valAt t) ⟩ hmem = subst (λ u → ⟨ envAt t m ∈ˢ u ⟩) (sym (valAt-val t)) inTable where inner : ⟨ NM.DA._⊨ᵐ_ (environment t m) (embed (formula t)) ⟩ inner = subst ⟨_⟩ (NM.denote-mem t m) hz ``` 法則 `val-sat` は、この内側の充足関係を、`envAt t m` が `keyAt t` における表の値に属することと同一視します。ここでは充足関係から始めるため、この法則を逆向きに読みます。次に `valAt-val` に沿って輸送し、明示的な表の値を封印された証人 `valAt t` で置き換えます。これで第六の条件が証明され、`denote-fill` が完成します。四つの証人とそれらを結ぶ六つの関係は、すべて名前 `t` のデータと、その指示対象への仮定された所属から得られました。 ```agda inTable : ⟨ envAt t m ∈ˢ Table.val Aʟ Aʟ (keyAt t) (keyAt-∈ t) ⟩ inTable = subst ⟨_⟩ (sym (val-sat Aʟ (embed (formula t)) (keyAt t) (keyAt-∈ t) (keyAt-fst t) (environment t m) (envAt t m) (envAt-fst t m))) inner ``` 逆向きでは、`z` に対する明示的な `DenoteOf` の中身、すなわち四つの束縛された要素と先の六条件が与えられているとします。目標は、`z` が表す要素 `m` が `denote t` に属することです。`NM.denote-mem` を逆向きに読めば、埋め込まれた論理式が `environment t m` で内側の充足関係を満たすことを復元すれば十分です。残る等式は、中身が任意に与えた環境、数項、鍵、値を順に識別します。 ```agda denote-read : (z : S) (m : ⟪ A ⟫) → ⟪ A ⟫↪ m ≡ fst z → DenoteOf B C s e γ z → ⟨ ⟪ A ⟫↪ m ∈ denote t ⟩ denote-read z m qm (c , (k , (key , (v , (hc , (hk , (hi , (hp , (hg , hm))))))))) = subst ⟨_⟩ (sym (NM.denote-mem t m)) inner where ``` まず拡張の条件を読みます。その外向きの妥当性定理は、元のグラフ `qd'`、候補の要素を同一視する `sym qm`、充足証明 `hc` を比較します。その結果、任意に与えられた証人 `c` の基礎集合は、ちょうど `envGraph Aʟ (environment t m)` だと分かります。したがって、最初の存在証人はパラメータグラフの単なる何らかの拡張ではなく、`m` を名前 `t` のパラメータの前に置いて得る正準な環境のグラフです。 ```agda qcg : fst c ≡ envGraph Aʟ (environment t m) qcg = consAtL-out Aʟ δp (NM.DA.ι m) (c ∷ z ∷ γ) zero (suc zero) (sh2 e) qd' (sym qm) hc ``` 次に定義域の条件が数項の証人を決定します。`qcg` が `c` を `environment t m` のグラフと同一視しているので、`domAt-numeral` は `hk` を、`k` の基礎集合とその環境の長さを表す数項との等式として読めます。この長さは `suc (arity t)` であり、`valuesL` が定義域の妥当性定理に必要な構成可能性を与えます。したがって `fst k ≡ # (suc (arity t))` が得られます。 ```agda qk : fst k ≡ # (suc (arity t)) qk = domAt-numeral (suc zero) zero (k ∷ c ∷ z ∷ γ) (suc (arity t)) (values Aʟ (environment t m)) (valuesL t m) qcg hk ``` 中身の第四の条件 `hp` は、その鍵が自身の定義域の証人 `k` と骨格のスロットとの対であることを述べます。第一成分を `qk` で、第二成分を `qs` で書き換えると、`# (suc (arity t))` と論理式コードとの対が得られます。最後に `keyCode (formula t)` を逆向きに読み、この対を `embed (formula t)` の符号集合の鍵として認識します。こうして得た等式 `qkey'` は、中身が任意に与えた鍵を真正な論理式の鍵と同一視します。 ```agda qkey' : fst key ≡ fst (keyS Aʟ (embed (formula t))) qkey' = hp ∙ cong (λ u → pr u (fst (lookup s γ))) qk ∙ cong (pr (# (suc (arity t)))) qs ∙ sym (keyCode (formula t)) ``` 所属条件 `hi` は、復元された鍵がスロット `C` に格納された集合に属することを述べます。`qC` に沿って輸送すると、`AllCodes Aʟ` への所属 `key∈` が得られます。これは所属の証明であって、新しい鍵の選択ではありません。鍵そのものはすでに `DenoteOf` の中身から与えられ、`qkey'` によって同一視されています。この証明の役割は、その鍵を、統一表と充足関係グラフの意味論的な仕様が成り立つ領域に置くことです。 ```agda key∈ : ⟨ key ∈ˢ AllCodes Aʟ ⟩ key∈ = subst (λ u → ⟨ fst key ∈ u ⟩) qC hi ``` 最後に、任意に与えられた値の証人 `v` を同一視します。`qkey'` と `keyψ` によって、その鍵をスロットの台における `ψAt t` の鍵と揃えると、グラフの証明 `hg` に一意性の読み `graphAt-only` を適用できます。これにより、まず `fst v` が対応する `Sat` 集合と同一視されます。輸送 `satψ` がその集合を `Aʟ` へ戻し、`val-at` を逆向きに読むことで `Table.val Aʟ Aʟ key key∈` と同一視します。こうして `qval` が必要な表の値を復元し、次の段階で最後の所属 `hm` を内側の充足関係へ変換できるようになります。 ```agda qval : fst v ≡ fst (Table.val Aʟ Aʟ key key∈) qval = graphAt-only (sh5 B) (suc zero) zero (v ∷ key ∷ k ∷ c ∷ z ∷ γ) (ψAt t) (qkey' ∙ sym (keyψ t)) hg ∙ satψ t ∙ sym (cong fst (val-at Aʟ Aʟ (embed (formula t)) key key∈ qkey')) ``` `DenoteOf` の最後の成分は、拡張された環境 `c` が復元された値 `v` に属することを述べます。パス `qval` は、この値を復元された論理式符号のキーにおける一様充足表の値と同定します。このパスに沿って所属を移送すると、次の意味論的な読みに必要な表への所属が得られます。 ```agda inTable : ⟨ c ∈ˢ Table.val Aʟ Aʟ key key∈ ⟩ inTable = subst (λ u → ⟨ fst c ∈ u ⟩) qval hm ``` 妥当性の等式 `val-sat` は、この表の値への所属を埋め込まれた論理式の充足として読みます。その仮定では、`qkey'` が復元されたキーを同定し、`qcg` が `c` を拡張された環境のグラフと同定します。したがって `inner` は、`environment t m` が名前 `t` の論理式を満たすことを述べます。外側の結果では、さらに `denote-mem` を逆向きに用いて `denote t` への所属を得ます。 ```agda inner : ⟨ NM.DA._⊨ᵐ_ (environment t m) (embed (formula t)) ⟩ inner = subst ⟨_⟩ (val-sat Aʟ (embed (formula t)) key key∈ qkey' (environment t m) c qcg) inTable ``` ここまでの読みは、台の元 `m` に対して述べられていました。補題 `member-fill` は順方向の読みを任意の構成可能な要素 `z` に言い換えます。その台集合が `denote t` に属するなら、台のスロットへの所属と、証人の組 `DenoteOf` の両方が得られます。第一の結論は、集合 `A` への実際の所属から得た後、スロットの等式 `qB` に沿って移送されます。 ```agda member-fill : (z : S) → ⟨ fst z ∈ denote t ⟩ → ⟨ fst z ∈ fst (lookup B γ) ⟩ × DenoteOf B C s e γ z member-fill z hz = subst (λ u → ⟨ fst z ∈ u ⟩) (sym (cong fst qB)) hA , denote-fill z (fib .fst) (fib .snd) (subst (λ u → ⟨ u ∈ denote t ⟩) (sym (fib .snd)) hz) ``` 元に対する補題を適用するには、`z` が表す台の元をまず復元する必要があります。包含補題 `denoteMem` は、表示への所属を `A` への所属に変えます。次に、所属のファイバー表示から `m : ⟪ A ⟫` と等式 `⟪ A ⟫↪ m ≡ fst z` が得られます。これは通常の依存データなので、選択原理も命題的切り詰めの除去も使いません。 ```agda where hA : ⟨ fst z ∈ A ⟩ hA = denoteMem t (fst z) hz fib : Σ[ mm ∈ ⟪ A ⟫ ] (⟪ A ⟫↪ mm ≡ fst z) fib = ∈-asFiber {a = fst z} {b = A} hA ``` 逆向きの言い換えは、`z` の台のスロットへの所属と `DenoteOf` の証人の組から始まります。`z` が表す台の元を復元した後、先の補題 `denote-read` はその証人の組を、埋め込まれた元の `denote t` への所属として読みます。最後にファイバーの等式に沿って移送し、`fst z` の所属へ戻します。 ```agda member-read : (z : S) → ⟨ fst z ∈ fst (lookup B γ) ⟩ → DenoteOf B C s e γ z → ⟨ fst z ∈ denote t ⟩ member-read z hz hDen = subst (λ u → ⟨ u ∈ denote t ⟩) (fib .snd) (denote-read z (fib .fst) (fib .snd) hDen) where ``` ここで必要なファイバーは、台のスロットへの所属という仮定から得られます。等式 `qB` はそのスロットの台集合を `A` と同定するので、移送によってまず `fst z ∈ A` が得られます。続いて `∈-asFiber` が `⟪ A ⟫` の対応する元と、その埋め込みの等式を返します。したがって二つの補題は、小さな台の型の元としてあらかじめ与えられた場合だけでなく、必要な所属を満たすモデルの任意の要素に適用できます。 ```agda fib : Σ[ mm ∈ ⟪ A ⟫ ] (⟪ A ⟫↪ mm ≡ fst z) fib = ∈-asFiber {a = fst z} {b = A} (subst (λ u → ⟨ fst z ∈ u ⟩) (cong fst qB) hz) ``` ## 名前を組み立てる 固定した名前 `t` に対して、`Data t` は四つの等式を記録します。骨格のスロットはその論理式の符号、アリティのスロットはその数項、環境のスロットはそのパラメータのグラフ、表示のスロットは `denote t` です。`NameAt-fill` はこれらの等式を用いて、`NameAt` の四つの概念的な連言、すなわち定数を含まないこと、アリティが `ω` に属すること、環境条件、表示の外延的な特徴付けを証明します。最後の連言は、所属の二方向 `into` と `back` によって与えられます。 ```agda NameAt-fill : (t : Name) → Data t → ⟨ γ ⊨ NameAt B C C₀ s a e d ⟩ NameAt-fill t (qs , (qa , (qe , qd))) = NameAt-in B C C₀ s a e d γ hf ha he into back where module Bt = Body t qs qa qe ``` 最初の連言は、名前 `t` がもつ具体的な無パラメータ論理式から得られます。この論理式には `suc (arity t)` 個の変数位置があり、`qs` はその極限段階での符号を骨格のスロットと同定します。さらに `qa` がアリティのスロットを、`q₀` が空のアルファベットの符号集合を同定するので、`codeFree-in` はこの論理式と符号の等式をそのまま `FreeAt` の充足へ変換します。 ```agda hf : ⟨ γ ⊨ FreeAt C₀ s a ⟩ hf = codeFree-in C₀ s a γ (arity t) q₀ qa (formula t) qs ``` アリティの連言が要求するのは `ω` への所属だけです。標準的な事実 `#∈ω (arity t)` がその数項の `ω` への所属を与え、等式 `qa` がそれをアリティのスロットに格納された値へ移送します。この部分の記述では比較関係を使いません。 ```agda ha : ⟨ fst (lookup a γ) ∈ ω ⟩ ha = subst (λ u → ⟨ u ∈ ω ⟩) (sym qa) (#∈ω (arity t)) ``` 環境の連言では、名前 `t` のパラメータベクトルを族 `i ↦ lookup i (params t)` とみなします。そのグラフの等式は `qe`、定義域の数項についての等式は `qa` であり、`qB` は終域の台を `Aʟ` と同定します。`paramSeq-in` はこの族の標準的な環境の性質を三つのスロットへ移送し、`envOverAt` の充足を与えます。 ```agda he : ⟨ γ ⊨ envOverAt e a B ⟩ he = paramSeq-in e a B γ (arity t) (λ i → lookup i (params t)) qe qa (cong fst qB) ``` 表示を外延的に特徴付ける連言の順方向は、表示のスロットの元から始まります。`qd` に沿って移送すると、その元は `denote t` の元になります。そこで `Bt.member-fill` が、表示の本体をなす二つの部分、すなわち台のスロットへの所属と証人の組 `DenoteOf` をちょうど与えます。 ```agda into : (z : S) → ⟨ fst z ∈ fst (lookup d γ) ⟩ → ⟨ fst z ∈ fst (lookup B γ) ⟩ × DenoteOf B C s e γ z into z hz = Bt.member-fill z (subst (λ u → ⟨ fst z ∈ u ⟩) qd hz) ``` 逆に、`Bt.member-read` は台への所属と `DenoteOf` を合わせて、`denote t` への所属として読みます。さらに `qd` の逆向きに沿って移送すると、その要素は表示のスロットへ戻ります。この二つの関数が、`NameAt` にある一つの外延的な連言に必要な二方向です。 ```agda back : (z : S) → ⟨ fst z ∈ fst (lookup B γ) ⟩ → DenoteOf B C s e γ z → ⟨ fst z ∈ fst (lookup d γ) ⟩ back z hzB hDen = subst (λ u → ⟨ fst z ∈ u ⟩) (sym qd) (Bt.member-read z hzB hDen) ``` `NameAt` の逆方向の読みが返すのは、名前とその四つのデータの等式の命題的切り詰めだけです。アリティの連言 `ha` は `ω` への所属であり、その意味論的な表示は、命題的切り詰めのもとで自然数 `k` と、アリティのスロットを `# k` と同定する等式を与えます。最終結果も命題的に切り詰められた型なので、`PT.rec` はその結果を構成する範囲でこの証人を使えます。 ```agda NameAt-read : ⟨ γ ⊨ NameAt B C C₀ s a e d ⟩ → ∥ Σ[ t ∈ Name ] Data t ∥₁ NameAt-read (hf , (ha , (he , hd))) = PT.rec squash₁ atArity ha where atCode : (k : ℕ) (qa : fst (lookup a γ) ≡ # k) ``` `k` とアリティの等式 `qa` を固定すると、`codeFree-out` が定数を含まないという連言を読みます。そこからは、なお命題的切り詰めのもとで、論理式 `χ : Formula ⊥* (suc k)` と、骨格のスロットからその極限段階での符号への等式 `qs` が得られます。この分岐の中で `atCode` が名前とそのデータを組み立て、`qs` が第一の等式、`qa` が第二の等式になります。 ```agda → Σ[ χ ∈ Formula (⊥* {ℓ}) (suc k) ] (fst (lookup s γ) ≡ fst (limitCode χ)) → Σ[ t ∈ Name ] Data t atCode k qa (χ , qs) = t , (qs , (qa , (qe , qd))) where ``` アリティが定まると、パラメータ成分は直接復元できます。`paramSeq-out` は `qa` と台の等式 `qB` を用いて `he` を読み、`⟪ A ⟫` に値を取る長さ `k` のベクトルを得ます。このベクトルを `k` と `χ` に組み合わせて名前 `t` を定義します。ベクトル自体の復元には命題的切り詰めがありませんが、構成全体はアリティと論理式の読みによる切り詰めの内側にあります。 ```agda t : Name t = k , (χ , paramSeq-out e a B γ k qa (cong fst qB) he) ``` 復元されたベクトルは、`Data t` に記録される環境の等式も満たさなければなりません。対応する補題 `paramSeq-graph` は、もとの環境のスロットがこのベクトルの符号化されたグラフ `env (pfam t)` に等しいことを述べます。このパスが第三のデータの等式 `qe` です。 ```agda qe : fst (lookup e γ) ≡ env (pfam t) qe = paramSeq-graph e a B γ k qa (cong fst qB) he ``` 局所モジュール `Bt` は、復元された名前と、その最初の三つのデータの等式 `qs`、`qa`、`qe` において、表示の本体の読みを具体化します。したがって `Data t` に残る成分は、表示のスロットと `denote t` の間の集合の等式です。これは両者の元を二方向に比較して証明します。 ```agda module Bt = Body t qs qa qe ``` まず順方向の包含を示します。`y` が表示のスロットに属するとします。そのスロットはモデルの要素なので、`L` の推移性から `y` は構成可能であり、`z : S` としてまとめられます。外延的な連言 `hd` を外向きに読むと、台への所属と、命題的に切り詰められた `DenoteOf` の証人が得られます。目標 `y ∈ denote t` は命題なので、`PT.rec` によってその証人の各代表へ `Bt.member-read` を適用できます。 ```agda fwd : (y : V ℓ) → ⟨ y ∈ fst (lookup d γ) ⟩ → ⟨ y ∈ denote t ⟩ fwd y hy = PT.rec (snd (y ∈ denote t)) (Bt.member-read z (body .fst)) (body .snd) where z : S ``` `body` は二段階の意味論的な読みから得られます。まず `extAt-out` が表示のスロットへの所属を `DenoteBody` の充足に変え、次に `DenoteBody-out` がその台についての連言と、`DenoteOf` にまとめられた四つの存在証人を取り出します。存在量化の意味論に従って、これらの証人は命題的に切り詰められたままであり、上の命題値をもつ所属の証明の中だけで使われます。 ```agda z = y , isL-trans hy (snd (lookup d γ)) body : ⟨ fst z ∈ fst (lookup B γ) ⟩ × ∥ DenoteOf B C s e γ z ∥₁ body = DenoteBody-out B C s e γ z (extAt-out d (DenoteBody B C s e) γ hd z hy) ``` 逆方向の包含では `y ∈ denote t` を仮定します。証明はまず `y` を要素 `z : S` とみなし、次に `Bt.member-fill` を用いて `z` における表示の本体を構成します。導入補題 `DenoteBody-in` と `extAt-in` が、本体の充足と表示のスロットへの所属を順に組み立て直します。 ```agda bwd : (y : V ℓ) → ⟨ y ∈ denote t ⟩ → ⟨ y ∈ fst (lookup d γ) ⟩ bwd y hy = extAt-in d (DenoteBody B C s e) γ hd z (DenoteBody-in B C s e γ z (body .fst) (body .snd)) where z : S ``` `z` の構成可能性は、すでに分かっている二つの包含関係から得られます。`denoteMem` は `denote t` の各要素を `A` に入れ、`pA` は `A` が構成可能であることを述べます。この `z` に対して、`Bt.member-fill` は台への所属と、切り詰められていない `DenoteOf` の証人の組を与えます。したがって逆方向の包含では命題的切り詰めを除去する必要がありません。 ```agda z = y , isL-trans (denoteMem t y hy) pA body : ⟨ fst z ∈ fst (lookup B γ) ⟩ × DenoteOf B C s e γ z body = Bt.member-fill z hy ``` 各集合 `y` に対して、関数 `fwd y` と `bwd y` は二つの所属命題の間の両方向の含意を与えます。両辺は命題なので、`⇔toPath` はこの二つの含意を真理値の等式に変えます。さらに `V` の外延性が、点ごとの所属の等式を `fst (lookup d γ) ≡ denote t`、すなわち第四の等式 `qd` に変えます。 ```agda qd : fst (lookup d γ) ≡ denote t qd = extensionalV (λ y → ⇔toPath (fwd y) (bwd y)) ``` 分岐 `atArity` は、大域的な証人を選ぶことなく二つの切り詰めを処理します。その入力はアリティを持ち上げられた自然数として表し、`qk` を逆向きにすると `atCode` が要求する等式になります。続いて `codeFree-out` が命題的切り詰めのもとで論理式と符号の等式を与え、`PT.map` がその切り詰めの内側で `atCode` を適用します。結果は、四つのデータの等式をすべて満たす名前が存在するという命題的に切り詰められた主張であり、ちょうど `NameAt-read` の終域です。 ```agda atArity : Σ[ lk ∈ Lift {ℓ-zero} {ℓ} ℕ ] (# (lower lk) ≡ fst (lookup a γ)) → ∥ Σ[ t ∈ Name ] Data t ∥₁ atArity (lk , qk) = PT.map (atCode (lower lk) (sym qk)) (codeFree-out C₀ s a γ (lower lk) q₀ (sym qk) hf) ``` ## 最小性の記述と意味 最小の名前の論理式は、競合する名前を記述する三つのデータを量化します。最初にまとめられる要素 `codeEl t` は、名前 `t` の論理式符号をモデルに入れます。`codeOf t` は極限段階 `Lset ω` に属し、その段階は構成可能なので、`L` の推移性から符号自身も構成可能です。不透明な定義が公開するのは台集合の等式 `codeEl-fst` だけです。後で特定の競合相手について全称節を具体化する際、充足の証明が必要とするのはこの等式だけです。 ```agda opaque codeEl : Name → S codeEl t = fst (codeOf t) , isL-trans (snd (codeOf t)) (snd (LsetS ω ω-ord)) ``` 要素 `codeEl t` は名前の論理式の符号をモデルへ持ち込みます。その第一射影は定義上 `codeOf t` の基礎集合そのものなので、全称節の具体化に必要な等式は反射律で得られます。第二射影に収められた構成可能性の証明は、この符号を変えません。 ```agda codeEl-fst : (t : Name) → fst (codeEl t) ≡ fst (codeOf t) codeEl-fst t = refl ``` 名前のパラメータデータは、もう一つのモデル要素で表されます。`t` に対する族`i ↦ lookup i (params t)` は `arity t` 個の各位置で台の要素を選び、`envS Aʟ` はその族を符号化された環境グラフにします。したがって `envEl t` は`NameAt` の環境スロットが要求する形を正確に備えています。 ```agda envEl : Name → S envEl t = envS Aʟ (λ i → lookup i (params t)) ``` 環境の包装を展開するとグラフ `env (pfam t)` が得られます。`pfam t` は`params t` の成分を順に読み出して得る族そのものだからです。したがって`envEl-fst` も反射律で証明されます。これは `codeEl-fst` および先に得た`numAt` の等式と合わせて、具体的な名前を量化された競合名へ代入するための三つのスロット等式を与えます。 ```agda envEl-fst : (t : Name) → fst (envEl t) ≡ env (pfam t) envEl-fst t = refl ``` ## 記述された最小の名前は最小の名前である 名前比較には二つの狭義整列順序が入ります。記法 `_≺ˡ_` は論理式の符号上の`limitOrder` を表し、`_≺ₚ_` は台のパラメータ上に与えられた順序 `w` を表します。`_≺ₙ_` では符号、アリティ、パラメータベクトルの順に比較します。対象言語で関係集合を必要とするのは第一と第三のキーだけであり、アリティの比較は数項の所属で表されます。 ```agda open SWO limitOrder using () renaming ( _<∙_ to _≺ˡ_ ) open SWO w using () renaming ( _<∙_ to _≺ₚ_ ) ``` 集合 `Rs` と `Ps` は、この二つの順序をモデル内部で表します。極限段階の要素`u,v` に対し、`Rrep` は順序対の `Rs` への所属を `u ≺ˡ v` と読み、`Rfill` はその比較から所属を証明します。`Prep` と `Pfill` は台の要素と`Ps` について同じ二方向を与えます。この四つの表現法則が妥当性結果の仮定です。 ```agda module Least (Rs Ps : S) (Rrep : (u v : Limit) → ⟨ pr (fst u) (fst v) ∈ fst Rs ⟩ → u ≺ˡ v) (Rfill : (u v : Limit) → u ≺ˡ v → ⟨ pr (fst u) (fst v) ∈ fst Rs ⟩) (Prep : (u v : ⟪ A ⟫) → ⟨ pr (ix u) (ix v) ∈ fst Ps ⟩ → u ≺ₚ v) (Pfill : (u v : ⟪ A ⟫) → u ≺ₚ v → ⟨ pr (ix u) (ix v) ∈ fst Ps ⟩) ``` 非公開モジュール `K` は、三つのキーによる比較の妥当性を `Rs`、`Ps` とそれらの表現法則に特殊化します。`order-in` はメタ言語の名前比較の証明を`_≺At_` の充足へ変え、`order-out` は命題的切り詰めのもとで比較を回復します。以下では、比較する具体的な名前について符号、数項、環境の等式を与えます。 ```agda where private module K = Keys Rs Ps Rrep Rfill Prep Pfill ``` モジュール `Min` は最小名の論理式で使う九つの位置を固定します。二つの関係`R,P`、台 `B`、二つの符号集合 `C,C₀`、現在の名前の符号、アリティ、環境`s,a,e`、そしてその指示対象 `d` です。等式 `qR` と `qP` は関係の基礎集合を同一視します。後の論理式は台に依存するため、`qB` はモデル要素そのものの等式です。`qC` は台に対する符号集合の基礎集合を同一視します。 ```agda module Min {n : ℕ} (R P B C C₀ s a e d : Fin n) (γ : S ^ n) (qR : fst (lookup R γ) ≡ fst Rs) (qP : fst (lookup P γ) ≡ fst Ps) (qB : lookup B γ ≡ Aʟ) (qC : fst (lookup C γ) ≡ fst (AllCodes Aʟ)) ``` 残る等式 `q₀` は、`C₀` を空のアルファベット上の符号集合の基礎集合と同一視します。`qB`、`qC`、`q₀` を固定すると、非公開モジュール `N` はここで使う各スロットにおける `NameAt` の既証明の充填原理と読み取り原理を与えます。そこで最小名の妥当性では、現在のデータが名前をなすという主張と、追加の最小性を分けて扱えます。 ```agda (q₀ : fst (lookup C₀ γ) ≡ fst (AllCodes ∅ʟ)) where private module N = Named B C C₀ s a e d γ qB qC q₀ ``` 名前 `t` に対し、`IsMin t` は、スロット `d` の集合を指示するより早い名前がないことを述べます。任意の競合名 `t'` について、そのスロットを `denote t'` と同一視する等式と `t' ≺ₙ t` の証明から矛盾を導かなければなりません。したがって競合名となるのは同じ集合を指示する名前だけであり、「より早い」は名前の完全な辞書式順序を意味します。 ```agda IsMin : Name → Type (ℓ-suc ℓ) IsMin t = (t' : Name) → fst (lookup d γ) ≡ denote t' → t' ≺ₙ t → Empty.⊥ ``` 述語 `Least t` は `N.Data t` と `IsMin t` を対にします。第一成分は、符号、アリティの数項、パラメータ環境、指示対象の各スロットを `t` のデータと同一視する四つの等式の記録です。第二成分は、同じ指示対象をもつより小さい名前をすべて排除します。これは `LeastNameAt` の二つの連言、すなわち命名条件と全称的な最小性条件に対応します。 ```agda Least : Name → Type (ℓ-suc ℓ) Least t = N.Data t × IsMin t ``` `LeastNameAt` を充填するため、まず `N.NameAt-fill` が具体的な名前 `t` と記録 `dt` から命名の連言を証明します。残る連言は三重の全称量化を実現する関数です。任意の集合 `s'`、`a'`、`e'` について、それらが同じ `d` を指示する競合名を記述し、さらにその競合名が現在の名前に先立つと仮定して、矛盾を導きます。 ```agda LeastAt-fill : (t : Name) → Least t → ⟨ γ ⊨ LeastNameAt R P B C C₀ s a e d ⟩ LeastAt-fill t (dt , mt) = N.NameAt-fill t dt , univ where univ : (s' a' e' : S) ``` 競合名の三つのデータを加えた環境は `e' ∷ a' ∷ s' ∷ γ` です。したがって各データは零、一、二番のスロットに入り、もとの各スロットは `sh3` で移動します。第一の前提は共有する指示対象 `sh3 d` に対する競合名の `NameAt` の充足です。第二の前提は、その競合名から移動後の現在の三つ組への `_≺At_` の充足です。結果の `Lift Empty.⊥` は、論理式の意味論が要求する宇宙レベルに置かれた矛盾です。 ```agda → ⟨ (e' ∷ a' ∷ s' ∷ γ) ⊨ NameAt (sh3 B) (sh3 C) (sh3 C₀) (suc (suc zero)) (suc zero) zero (sh3 d) ⟩ → ⟨ (e' ∷ a' ∷ s' ∷ γ) ⊨ ≺At (sh3 R) (sh3 P) (suc (suc zero)) (suc zero) zero (sh3 s) (sh3 a) (sh3 e) ⟩ → Lift {j = ℓ-suc ℓ} Empty.⊥ ``` 証明はまず、競合名の命名の充足に `Named.NameAt-read` を適用します。その結果は命題的切り詰めのもとにある名前 `t'` と、その `Named.Data` 記録の四つの等式です。求める結果は命題である矛盾なので、`PT.rec` によってこの命題的切り詰めを除去できます。競合名を選択して保持するわけではなく、回復した名前はこの不可能性の証明の内部だけで使われます。 ```agda univ s' a' e' hn hlt = lift (PT.rec Empty.isProp⊥ step (Named.NameAt-read (sh3 B) (sh3 C) (sh3 C₀) (suc (suc zero)) (suc zero) zero (sh3 d) (e' ∷ a' ∷ s' ∷ γ) qB qC q₀ hn)) where step : Σ[ t' ∈ Name ] Named.Data (sh3 B) (sh3 C) (sh3 C₀) ``` 回復した競合名について、四つのデータ等式を `qs'`、`qa'`、`qe'`、`qd'`と名付けます。最後の等式は共有する指示対象スロットが `denote t'` であると述べるので、`mt t' qd'` は `t' ≺ₙ t` の証明を反駁できます。その比較自体も命題的切り詰めのもとで得られますが、目標は再び矛盾なので、二度目の `PT.rec` による除去が許されます。 ```agda (suc (suc zero)) (suc zero) zero (sh3 d) (e' ∷ a' ∷ s' ∷ γ) qB qC q₀ t' → Empty.⊥ step (t' , (qs' , (qa' , (qe' , qd')))) = PT.rec Empty.isProp⊥ (mt t' qd') ``` `K.order-out` の呼び出しが切り詰められた比較を与えます。そこでは関係の等式`qR,qP`、回復した競合名の符号、数項、環境の等式、`dt` にある現在の名前の対応する三つの等式、そして仮定した充足 `hlt` を使います。結果は`∥ t' ≺ₙ t ∥₁` です。これを `mt t' qd'` が与える矛盾へ除去すると、全称的な最小性の節が完成します。 ```agda (K.order-out (sh3 R) (sh3 P) (suc (suc zero)) (suc zero) zero (sh3 s) (sh3 a) (sh3 e) (e' ∷ a' ∷ s' ∷ γ) t' t qR qP qs' (dt .fst) qa' (dt .snd .fst) qe' (dt .snd .snd .fst) hlt) ``` 逆に、`LeastNameAt` の充足は命名の証拠 `hn` と全称節 `hu` に分かれます。`hn` を読むと `∥ Σ[ t ∈ Name ] N.Data t ∥₁` が得られます。ここでの写像は外側の命題的切り詰めを保ち、回復した各 `t` と `dt` に `IsMin t` の証明を加えます。したがって `LeastAt-read` が証明するのは、最小名の命題的に切り詰められた存在だけです。 ```agda LeastAt-read : ⟨ γ ⊨ LeastNameAt R P B C C₀ s a e d ⟩ → ∥ Σ[ t ∈ Name ] Least t ∥₁ LeastAt-read (hn , hu) = PT.map step (N.NameAt-read hn) where step : Σ[ t ∈ Name ] N.Data t → Σ[ t ∈ Name ] Least t ``` `IsMin t` を証明するため、明示的な競合名 `t'`、それがスロット `d` の集合を指示することを示す等式 `qd'`、および比較 `lt : t' ≺ₙ t` を固定します。全称節 `hu` を `codeEl t'`、先に定義した `numAt (arity t')`、`envEl t'`で具体化します。したがって、ここで新たに定義された包装は符号と環境だけであり、数項の包装は再利用されています。 ```agda step (t , dt) = t , (dt , mt) where mt : IsMin t mt t' qd' lt = lower (hu (codeEl t') (numAt (arity t')) (envEl t') (Named.NameAt-fill (sh3 B) (sh3 C) (sh3 C₀) (suc (suc zero)) ``` `hu` の第一の前提は `Named.NameAt-fill` で構成します。等式 `codeEl-fst`、`numAt-fst`、`envEl-fst` が競合名の三つのデータスロットを同一視し、仮定`qd'` が共有する指示対象スロットを同一視します。第二の前提は `K.order-in`から始まり、明示的な比較 `lt` を比較論理式の充足へ移します。 ```agda (suc zero) zero (sh3 d) (envEl t' ∷ numAt (arity t') ∷ codeEl t' ∷ γ) qB qC q₀ t' (codeEl-fst t' , (numAt-fst (arity t') , (envEl-fst t' , qd')))) (K.order-in (sh3 R) (sh3 P) (suc (suc zero)) (suc zero) zero ``` `K.order-in` の呼び出しには、`dt` にある現在の名前の三つの等式と関係の等式`qR,qP` も渡します。これにより、拡張された環境で `hu` が要求する比較の前提が正確に証明されます。`hu` を適用すると持ち上げられた矛盾が得られ、`lower` がそれを `IsMin` の要求する宇宙レベルへ戻します。この持ち上げと引き下げは宇宙の配置に関するものであり、命題的切り詰めの除去ではありません。 ```agda (sh3 s) (sh3 a) (sh3 e) (envEl t' ∷ numAt (arity t') ∷ codeEl t' ∷ γ) t' t qR qP (codeEl-fst t') (dt .fst) (numAt-fst (arity t')) (dt .snd .fst) (envEl-fst t') (dt .snd .snd .fst) lt)) ``` ## 一つのステップの記述と意味 モジュール `Step` は同じ二つの表現された関係、台、符号集合を保ち、比較する集合のスロット `x` と `y` を加えます。五つの等式の役割は `Min` と同じです。`qR,qP` は二つの関係スロットを解釈し、`qB` は依存するモデル要素の等式として台を同一視し、`qC,q₀` は二つの符号集合の基礎集合を同一視します。この局所的な主張は`x` と `y` の名前の比較だけを扱い、段階順序との接続はこのモジュールの外で証明されます。 ```agda module Step {n : ℕ} (R P B C C₀ x y : Fin n) (γ : S ^ n) (qR : fst (lookup R γ) ≡ fst Rs) (qP : fst (lookup P γ) ≡ fst Ps) (qB : lookup B γ ≡ Aʟ) (qC : fst (lookup C γ) ≡ fst (AllCodes Aʟ)) ``` `LeastOf i t` はステップの各端点に必要なメタ言語の性質です。第一成分はスロット`i` が `denote t` を含むことを述べます。第二成分は、指示対象が同じスロットである任意の名前 `t'` が `t` に先立つことを否定します。したがって、`t` がスロット `i` の特定の集合に対する最小名であると主張しますが、それ自体は論理式の充足証明を含みません。 ```agda (q₀ : fst (lookup C₀ γ) ≡ fst (AllCodes ∅ʟ)) where LeastOf : Fin n → Name → Type (ℓ-suc ℓ) LeastOf i t = (fst (lookup i γ) ≡ denote t) × ((t' : Name) → fst (lookup i γ) ≡ denote t' → t' ≺ₙ t → Empty.⊥) ``` `StepAt-fill` は明示的な名前 `t₁,t₂`、それらがそれぞれ `x,y` に対して最小であることの証明、明示的な比較 `t₁ ≺ₙ t₂` から始まります。`StepAt-in` には束縛順に六つの証人を渡します。まず `t₁` の符号、アリティの数項、パラメータ環境、続いて `t₂` の対応する三つのデータです。論理式本体には二つの最小名の充足と一つの比較の充足が必要です。この充填定理の入力は命題的に切り詰められていません。 ```agda StepAt-fill : (t₁ t₂ : Name) → LeastOf x t₁ → LeastOf y t₂ → t₁ ≺ₙ t₂ → ⟨ γ ⊨ StepAt R P B C C₀ x y ⟩ StepAt-fill t₁ t₂ l₁ l₂ lt = StepAt-in R P B C C₀ x y γ ( codeEl t₁ , (numAt (arity t₁) , (envEl t₁ , ( codeEl t₂ , (numAt (arity t₂) , (envEl t₂ ``` 存在証人は環境の先頭へ積まれるため、六つの証人は束縛順とは逆に現れます。`envEl t₂`、その数項と符号、次に `envEl t₁`、その数項と符号、最後にもとの環境 `γ` が続きます。この環境で `s6a,a6a,e6a` は第一の名前の符号、数項、環境を指します。証明 `ln₁` は、第一の名前の三つのデータ等式、指示対象の等式`l₁ .fst`、最小性の証明 `l₁ .snd` を `LeastAt-fill` に渡します。 ```agda , ( ln₁ , (ln₂ , cmp) ))))))) where ln₁ = Min.LeastAt-fill (sh6 R) (sh6 P) (sh6 B) (sh6 C) (sh6 C₀) s6a a6a e6a (sh6 x) (envEl t₂ ∷ numAt (arity t₂) ∷ codeEl t₂ ``` 最初の `LeastAt-fill` に渡す記録には、要求どおり二つの部分があります。`N.Data` 成分は `codeEl-fst`、`numAt-fst`、`envEl-fst`、およびスロット `x`を `t₁` の指示対象と同一視する等式 `l₁ .fst` からなります。`IsMin` 成分は`l₁ .snd` です。したがって `ln₁` は、最初の束縛された三つ組が `x` の最小名であることを証明します。`t₂` に対する同様の構成と比較の証明が、`StepAt-in`に必要な残りの成分を与えます。 ```agda ∷ envEl t₁ ∷ numAt (arity t₁) ∷ codeEl t₁ ∷ γ) qR qP qB qC q₀ t₁ ( (codeEl-fst t₁ , (numAt-fst (arity t₁) , (envEl-fst t₁ , l₁ .fst))) , l₁ .snd ) ``` 第二の最小の名前の条件は、第一の場合と同じ妥当性の写像によって満たされます。ただし、今度使うスロットは `s6b`、`a6b`、`e6b` です。共通の六証人環境は、これらのスロットを `t₂` の符号、アリティの数項、パラメータ環境とそれぞれ同一視し、`sh6 y` は `t₂` が表示すべき集合を指定します。したがって残る引数は、その表示と `t₂` の最小性の両方を示さなければなりません。 ```agda ln₂ = Min.LeastAt-fill (sh6 R) (sh6 P) (sh6 B) (sh6 C) (sh6 C₀) s6b a6b e6b (sh6 y) (envEl t₂ ∷ numAt (arity t₂) ∷ codeEl t₂ ∷ envEl t₁ ∷ numAt (arity t₁) ∷ codeEl t₁ ∷ γ) qR qP qB qC q₀ t₂ ``` この入れ子の対は、`LeastAt-fill` が要求する型を正確に持ちます。まず `t₂` に関する四つのデータの等しさがあり、その後に最小性の証明が続きます。最初の三つの等しさは、封じた符号、数項、環境の各要素から得られます。`l₂ .fst` は表示対象をスロット `y` の値と同一視し、`l₂ .snd` は、同じ集合を表示して `t' ≺ₙ t₂` を満たす任意の `t'` を排除します。したがって最小性の向きは、`t₂` に先行するより小さな競合名がない、という向きです。 ```agda ( (codeEl-fst t₂ , (numAt-fst (arity t₂) , (envEl-fst t₂ , l₂ .fst))) , l₂ .snd ) ``` 比較条件が使うのは、各名前を順序づける三つの鍵だけです。`order-in` の呼び出しは、二つの関係スロットを解釈する `qR` と `qP` から始まり、続いて二つの符号の等しさと二つのアリティの数項の等しさを渡します。次の行にある二つの環境の等しさを合わせると、この呼び出しが要求する八つの等しさになります。`_≺ₙ_` はこの三つの鍵だけで名前を比較するので、表示と最小性は含まれません。 ```agda cmp = K.order-in (sh6 R) (sh6 P) s6a a6a e6a s6b a6b e6b (envEl t₂ ∷ numAt (arity t₂) ∷ codeEl t₂ ∷ envEl t₁ ∷ numAt (arity t₁) ∷ codeEl t₁ ∷ γ) t₁ t₂ qR qP (codeEl-fst t₁) (codeEl-fst t₂) (numAt-fst (arity t₁)) (numAt-fst (arity t₂)) ``` 二つの環境の等しさによってスロットの同一視がそろい、最後の引数 `lt` が実際の比較 `t₁ ≺ₙ t₂` を与えます。したがって `cmp` は、二つの三つ組の間にある対象言語の比較論理式の充足証明です。これは `ln₁`、`ln₂` と合わせて、`StepAt-in` が包む三つの連言を与えます。この充填の向きでは、指定された二つの名前と指定された比較から出発するため、六つの存在証人を直接導入できます。 ```agda (envEl-fst t₁) (envEl-fst t₂) lt ``` 逆向きの定理は、証人を取り出せる境界を正確に示します。`StepAt` の充足から返されるのは、`∥ Σ[ t₁ ∈ Name ] Σ[ t₂ ∈ Name ] (LeastOf x t₁ × (LeastOf y t₂ × (t₁ ≺ₙ t₂))) ∥₁` だけです。外側の依存和では `t₁` がすべての名前を動き、その各 `t₁` に対して内側の依存和では `t₂` がすべての名前を動きます。中身が正確に述べるのは、`t₁` がスロット `x` の値に対する最小名であり、`t₂` がスロット `y` の値に対する最小名であり、さらに `t₁ ≺ₙ t₂` であることです。最初の `PT.rec` は `StepAt-out` が与える六証人の命題的切り詰めを開きますが、除去先はこの切り詰められた結論のままです。 ```agda StepAt-read : ⟨ γ ⊨ StepAt R P B C C₀ x y ⟩ → ∥ Σ[ t₁ ∈ Name ] Σ[ t₂ ∈ Name ] (LeastOf x t₁ × (LeastOf y t₂ × (t₁ ≺ₙ t₂))) ∥₁ StepAt-read h = PT.rec squash₁ atSix (StepAt-out R P B C C₀ x y γ h) where ``` `Goal` はこの余域に一度だけ名前を付け、すべての切り詰めの消去先を同じ型にします。`Goal` 自身が命題的切り詰めなので、`squash₁` はそれが命題であることを示します。外側の六証人に関する切り詰めと、後に現れる二つの最小の名前に関する切り詰めをすべて消去でき、それでも最終的な名前の対が一つの命題的切り詰めに隠れたままである理由は、正確にここにあります。 ```agda Goal : Type (ℓ-suc ℓ) Goal = ∥ Σ[ t₁ ∈ Name ] Σ[ t₂ ∈ Name ] (LeastOf x t₁ × (LeastOf y t₂ × (t₁ ≺ₙ t₂))) ∥₁ ``` この許された消去の内側で、`atSix` は通常の `StepOf` の証人を受け取り、それを `(s₁,k₁,p₁)` と `(s₂,k₂,p₂)` の二つの三つ組に分けます。存在証人は環境の先頭へ順に加えられるので、本体は逆順の環境 `p₂ ∷ k₂ ∷ s₂ ∷ p₁ ∷ k₁ ∷ s₁ ∷ γ` で評価されます。したがって最初の `LeastAt-read` は、第一の三つ組の固定位置 `s6a`、`a6a`、`e6a` を用いて、スロット `x` の値を表示する最小の名前を読み取ります。 ```agda atSix : StepOf R P B C C₀ x y γ → Goal atSix (s₁ , (k₁ , (p₁ , (s₂ , (k₂ , (p₂ , hb)))))) = PT.rec squash₁ atFirst (Min.LeastAt-read (sh6 R) (sh6 P) (sh6 B) (sh6 C) (sh6 C₀) s6a a6a e6a (sh6 x) ``` 本体の証明 `hb` は三つの連言を含みます。その射影を順に `h₁`、`h₂`、`hc` と名付けます。最初の二つは第一と第二の三つ組についての `LeastNameAt` の充足であり、三つ目は第一の三つ組から第二の三つ組への `≺At` の充足です。証明はまず `h₁` を `LeastAt-read` に渡します。残る二つは、メタ言語の二つの名前がともに復元されるまで保たれます。その時点で初めて、`hc` をそれらの名前の比較として解釈できるからです。 ```agda (p₂ ∷ k₂ ∷ s₂ ∷ p₁ ∷ k₁ ∷ s₁ ∷ γ) qR qP qB qC q₀ h₁) where h₁ = hb .fst h₂ = hb .snd .fst hc = hb .snd .snd ``` `atSecond` は、第一の最小の名前を読み取った後に残る仕事を表します。特定の `t₁` とその完全な `Min.Least` の記録を受け取り、続いて特定の `t₂` と同様の記録を受け取って、`Goal` を構成しなければなりません。各記録には四つのデータの等しさと、正しい向きの最小性の主張が含まれます。したがって、この継続は二つの `LeastOf` の事実を復元し、まだ対象言語の側にある比較 `hc` を解釈するために十分な情報を持っています。 ```agda atSecond : (t₁ : Name) → Min.Least (sh6 R) (sh6 P) (sh6 B) (sh6 C) (sh6 C₀) s6a a6a e6a (sh6 x) (p₂ ∷ k₂ ∷ s₂ ∷ p₁ ∷ k₁ ∷ s₁ ∷ γ) qR qP qB qC q₀ t₁ → Σ[ t₂ ∈ Name ] Min.Least (sh6 R) (sh6 P) (sh6 B) (sh6 C) ``` 二つの記録がそろうと、最終的な主張に足りないのは `lt : t₁ ≺ₙ t₂` の証明だけです。その比較上で写される関数は、各データの記録から表示の等しさ `dᵢ .snd .snd .snd` だけを取り、それを最小性の証明 `mᵢ` と組にします。この二つがちょうど `LeastOf` の成分です。次に、得られた二つの最小の名前に関する事実を `lt` と合わせ、外側の命題的切り詰めを取り除くことなく、名前の完全な対を `Goal` に入れます。 ```agda (sh6 C₀) s6b a6b e6b (sh6 y) (p₂ ∷ k₂ ∷ s₂ ∷ p₁ ∷ k₁ ∷ s₁ ∷ γ) qR qP qB qC q₀ t₂ → Goal atSecond t₁ (d₁ , m₁) (t₂ , (d₂ , m₂)) = PT.map (λ lt → t₁ , (t₂ , ( (d₁ .snd .snd .snd , m₁) ``` ここで `order-out` が `hc` を解釈します。`qR` と `qP` に加えて、復元された二つの名前について、符号、アリティの数項、パラメータ環境の等しさを `d₁` と `d₂` から受け取ります。この三鍵比較には、表示の等しさは必要ありません。得られるのは `∥ t₁ ≺ₙ t₂ ∥₁` だけです。`PT.map` は、その命題的切り詰めの内側にある各比較を、`Goal` が要求する完全な証人へ変換します。 ```agda , ( (d₂ .snd .snd .snd , m₂) , lt )))) (K.order-out (sh6 R) (sh6 P) s6a a6a e6a s6b a6b e6b (p₂ ∷ k₂ ∷ s₂ ∷ p₁ ∷ k₁ ∷ s₁ ∷ γ) t₁ t₂ qR qP (d₁ .fst) (d₂ .fst) (d₁ .snd .fst) (d₂ .snd .fst) (d₁ .snd .snd .fst) (d₂ .snd .snd .fst) hc) ``` `atFirst` は、第一の最小の名前を読み取るための継続です。復元された対 `(t₁,l₁)` を受け取ると、第二の三つ組のスロットで `h₂` に `LeastAt-read` を適用し、第二の対を命題的切り詰めの下でだけ得ます。消去先が命題 `Goal` なので、続く `PT.rec` はその対を `atSecond t₁ l₁` に渡せます。したがって第二の切り詰めは、最終的な切り詰められた存在命題を構成する間に限って消去されます。 ```agda atFirst : Σ[ t₁ ∈ Name ] Min.Least (sh6 R) (sh6 P) (sh6 B) (sh6 C) (sh6 C₀) s6a a6a e6a (sh6 x) (p₂ ∷ k₂ ∷ s₂ ∷ p₁ ∷ k₁ ∷ s₁ ∷ γ) qR qP qB qC q₀ t₁ → Goal atFirst (t₁ , l₁) = PT.rec squash₁ (atSecond t₁ l₁) ``` 最後の呼び出しは、第二の三つ組の固定スロット、同じ逆順の六証人環境、および `h₂` を渡します。これにより、`StepAt-out`、二回の `LeastAt-read`、`order-out` という四つの切り詰められたインターフェースの合成が完成します。この合成が正確に証明するのは、`StepAt` の充足から、`t₁` が `x` の最小の名前であり、`t₂` が `y` の最小の名前であり、さらに `t₁ ≺ₙ t₂` であるような名前 `t₁,t₂` の存在が、命題的切り詰めの下で従うことです。特定の名前の対がこの切り詰めの外へ取り出されることはありません。 ```agda (Min.LeastAt-read (sh6 R) (sh6 P) (sh6 B) (sh6 C) (sh6 C₀) s6b a6b e6b (sh6 y) (p₂ ∷ k₂ ∷ s₂ ∷ p₁ ∷ k₁ ∷ s₁ ∷ γ) qR qP qB qC q₀ h₂) ``` ## まとめ 本章では、名前の意味論的な対応について二つの方向を確立した。妥当性の向きでは、具体的な名前の論理式符号、アリティ、パラメータ環境、指示対象から `NameAt` を充足できる。その名前が同じ指示対象をもつ名前の中で最小であることを加えれば `LeastNameAt` を充足でき、さらに二つの最小の名前と `t₁ ≺ₙ t₂` から `StepAt` を充足できる。完全性の向きでは、充足関係からこれらと同じデータを逆に復元する。したがって、二つの最小の記述を比較する論理式はメタ言語の比較と一致し、まず論理式符号を比較し、それが等しければアリティを比較し、最初の二つのキーがともに等しければパラメータベクトルを比較する。 完全性の各主張には命題的切り詰めが残る。一意性により、パラメータグラフからそのベクトルだけは切り詰めなしで定まるが、名前全体、最小の名前、または比較された最小の名前の対を読み取る結果は、適切な証人が存在することだけを述べる。切り詰めは常に命題を目標として除去され、特定の名前や名前の対が外へ取り出されることはない。ここでは命題リサイズも行われない。この境界のまま、後続の議論は `StepAt` をホスト側のステップ順序へ接続する。