名前の比較を表す論理式

同じ定義可能な部分集合が複数の名前をもつことがあります。メタ言語における名前は、アリティ k、suc k 個の変数位置をもつ無パラメータ論理式、そして台から取った k 個のパラメータのベクトルから成ります。名前の指示対象は、この三つのデータから導かれます。余分な一つの変数が候補となる要素を表し、残りの変数がパラメータベクトルを受け取ります。したがって、指示対象は名前の第四の成分ではありません。

このデータを L の内部で表すために、本章はパラメータベクトルを有限な環境グラフで表し、論理式の評価を充足関係グラフで表します。正しい論理式キーにおいて、satGraphAt はそのキーを、論理式を満たす環境全体の集合に関係づけます。その出力は、まさにこの充足環境の集合です。NameAt はアリティ、無パラメータ論理式の符号、パラメータ環境を、それらから導かれる指示対象に結び付けます。後で競合する名前を量化するとき、それらは同じ指示対象をもたなければなりません。

名前は辞書式に比較されます。まず極限段階の順序で論理式の符号を比較し、次にアリティを比較し、最後に台上の与えられた順序でパラメータベクトルを比較します。論理式 ≺At はこの三つの場合を表します。LeastNameAt は、同じ指示対象をもち、現在の名前より小さい名前がないことを述べるだけです。最小名を実際に選ぶのは、先に構成された CanonicalNames.leastName です。StepAt は二つの最小名を局所的に量化して比較します。本章で証明する妥当性は、ちょうど ≺At とメタ言語の関係 _≺ₙ_ との対応までです。NameAt、LeastNameAt、StepAt の完全な妥当性は後続の展開で証明されます。

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

基礎となる言語は、宇宙レベル、有限添字、ベクトル、命題値の主張を与えます。古典的推論は、明示された一つの仮定 LEM (ℓ-suc ℓ) を通して入ります。そのレベルは、以下で使う充足関係の構成と整列順序を扱うのに十分です。この仮定を明示しておくことで、性質を述べるだけの記述と、証人を実際に選ぶ先行の構成とを区別できます。

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

宇宙レベル ℓ と、必要な一段高いレベルでの排中律を固定します。これは本章が引き継ぐ古典論理のインターフェースです。以下の論理式構成子は構文を組み立てるだけですが、そこで用いる自然数対象、充足関係グラフ、極限段階の符号順序、正準名の理論は、いずれも同じ仮定のもとで構成されています。したがって、このモジュールはこれらの意味論的依存関係を記録しますが、改めて選択を行うことはありません。LeastNameAt は最小性を表し、最小名を選ぶ構成は引き続き CanonicalNames.leastName です。

module L.Choice.NameComparison {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

対象言語は所属と等号を述べ、命題を組み合わせ、台全体または一つの集合の上で量化できます。その意味論は命題値の構造で読み取られます。定数の写像は、後で必要となる三つの表示を結び付けます。すなわち、本当にパラメータをもたない論理式、空のアルファベット上の論理式、構成可能な台上で解釈された同じ構文です。これらの写像は論理式の構造を保つので、無パラメータ骨格の符号を内部で認識できるようになります。

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using
  ( Formula; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
import FOL.Absoluteness
open import FOL.Manipulation.ConstantMapping using ( mapFo; mapFo-comp; embed )

論理式の符号、順序対、数項は、それ自身が累積階層の集合です。構成可能部分構造は論理式を読む台を与え、推移性は構成可能な符号集合への所属から、その成分に必要な構成可能性を与えます。対の符号化と数項の符号化の単射性によって、後に等しいキーからアリティと骨格符号を復元できます。各 Lset 段階は極限段階の符号順序の舞台となります。

open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr; pr-inj; #mono; #-inj′; module VCode )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; Lset )
open import L.Ordinal {ℓ} using ( ∈#-elim; #∈#-elim )
open import L.Axioms.Basic {ℓ} using ( ∅ʟ; extensionalL )

アリティは内部の自然数集合に属する数項で表し、パラメータベクトルは有限環境のグラフで表します。対象言語の論理式は、順序対、適用、定義域を調べ、候補となる要素を環境に追加し、外延的に部分集合を定義できます。ある台上の論理式に対して、Sat はその論理式を満たす環境全体の集合です。後で充足関係グラフから復元する意味論的な値は、この集合です。

open import L.Axioms.Infinity {ℓ} lem using ( ωʟ )
open import L.Coding.Environment {ℓ} using ( env; lookup-spec )
open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; appAt; appAt-adequate; domAt; domAt-in; domAt-out; domAt-intro; envOverAt )
open import L.Coding.Expressions {ℓ} using ( extAt; extAt-in-both; numL; sucAtL; sucAtL-adequate; consAtL )
open import L.Coding.Satisfaction {ℓ} lem using ( Sat )

充足関係はすでに表として構成されており、各項目は部分式のキーと、再帰的に定まる充足環境の集合を対にしています。スロットの閉性と全性により、再帰で必要となるすべての正しいキーに項目が与えられ、充足関係の橋渡しが論理式の定数を選ばれた台の要素として同定します。したがって本章では、充足関係の再帰を再実行せずに、キーに保存された集合値を読み取れます。

open import L.Coding.SatisfactionTable {ℓ} lem
  using ( slot; satTable; total; inSlot; entry-in )
open import L.Coding.SlotClosure {ℓ} lem using ( slotClosed )
open import L.Coding.SatisfactionBridge {ℓ} lem using ( asConst )
open import L.Coding.CodeSet {ℓ} lem

各台について、AllCodes はその台上の正しい論理式キーをちょうど集め、その二方向の読みは所属と元の論理式を結び付けます。統一充足関係の橋渡しは、関係を表す論理式 satGraphAt B x y を支えます。x がスロット B の台上の正しいキーであるとき、y は対応する充足環境の集合です。GraphWitAt と二つのグラフの読みは、この集合値の関係を新しい再帰なしに示します。

  using ( keyS; AllCodes; AllCodes-out; key∈AllCodes )
open import L.Coding.UniformSatisfaction {ℓ} lem using ( keyBridge )
open import L.Coding.SatisfactionGraph {ℓ} lem using
  ( satGraphAt; GraphWitAt; graphAt-in; graphAt-out
  ; Bi; Ti; Ci; Ei; NN; ev; numν; numTags )

環境の塔とタグ付き再帰データは、充足関係グラフの読みが各構文要素について成り立つことを保証します。この内部の仕組みに対し、正準名の理論は名前比較の基準となるメタ言語の対象を与えます。メタ言語の Name が保存するのは、アリティ、無パラメータ論理式、パラメータベクトルです。limitCode は論理式から第一の比較キーを導き、指示対象は充足関係から別に導かれます。後のスロット論理式も、この区別を保たなければなりません。

open import L.Coding.EnvironmentTower {ℓ} lem using ( towerAt; module Tower; module TowerHolds )
open import L.Coding.Quantification {ℓ} using ( f0; f1; f2; f3; f4; f5; f6; f7; f8; f9 )
open import L.Coding.CodeDomain {ℓ} using ( Tags )
open import L.Coding.PinnedRecursion {ℓ} lem using ( module SatSoundC; module SlotHolds )
open import L.Choice.CanonicalNames {ℓ} lem using ( module Naming; limitCode )

名前の符号は極限段階の要素であり、limitOrder によって比較されます。第三のキーは、台上に与えられた任意の狭義整列順序から来ます。正準名の理論は、これらと自然数のアリティをすでに _≺ₙ_ にまとめ、その関係の整礎性を証明し、leastName で用いています。本章では二つの非数値的な順序を、表示法則を伴う関係スロットによって受け取ります。したがって、どちらの順序も再構成せず、それらによる比較を記述します。

open import L.Choice.FiniteStageOrders {ℓ} lem using ( Limit; limitOrder )
open import L.WellOrder.Base {ℓ-suc ℓ} using ( SWO )

自然数の順序が第二の比較キーを与えます。アリティが数項で表されるとき、一方の数項が他方に所属することは狭義の不等号を表します。有限添字は、パラメータベクトルの成分と、二つのベクトルが最初に異なる位置を指定します。後の妥当性の議論では、共通の長さに関する帰納法により、この最初の相違による記述が _≺ₙ_ で使われる再帰的なベクトル順序と一致することを証明します。

open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.Nat.Order
  using ( _<_; zero-≤; suc-≤-suc; pred-≤-pred; ¬-<-zero; <-trans )
open import Cubical.Data.FinData using ( toℕ )
open import Cubical.Data.FinData.Properties using ( toℕ<n; fromℕ'; toFromId' )

証明データは辞書式順序の形に従います。依存対は位置とその証拠を運び、直和は符号、アリティ、パラメータの三つの場合を分けます。先行するキーの等しさにより、依存する論理式とベクトルを共通のアリティへ輸送してから、次のキーを比較できます。空の型は、定数をもたない論理式に必要な定数解釈を一意に与えます。

open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
import Cubical.Data.Empty as Empty
open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.Foundations.Prelude using ( subst2 )

存在式と選言式の充足意味論は命題的に切り詰められています。証人が存在することは保ちますが、どの証人が与えられたかは忘れます。そのため、論理式の符号や名前比較を外向きに読むと、結論にも切り詰められた存在が残り、消去先は命題に限られます。ここで使われるのは命題的切り詰めであり、命題のリサイズではありません。累積階層は集合値の所属関係と、その読みの後で必要となる外延的な等しさの原理を与えます。

open import Cubical.Foundations.Transport using ( constSubstCommSlice )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties

階層集合の小さな要素は周囲の階層へ埋め込まれ、その埋め込みの単射性によって、後に表現されたパラメータの等しさから台の中での等しさを復元できます。空集合は空のアルファベットとして働きます。定数がないので、そこから出る写像は一意に定まり、無パラメータ論理式は必要な付け替えの下で同じ符号を保ちます。フォン・ノイマン数項 # k、その後者、そして ω が、環境の定義域と名前比較に使う内部のアリティを与えます。

  using ( ⟪_⟫; ⟪_⟫↪; isEmb⟪_⟫↪; ∈∈ₛ; ∈ₛ⟪_⟫↪_ )
open import Cubical.Functions.Embedding using ( isEmbedding→Inj )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; ∅-empty; module InfinitySet )
open InfinitySet using ( #_; ω; sucV )

以下の論理式は構成可能宇宙で解釈されます。hPropStructure 𝒮ʟ を開くことで、その台 S が定まります。台の要素は、周囲の宇宙にある集合と、それが構成可能であるという証拠の組です。また、この構造の命題値をとる等号関係と所属関係もスコープに入ります。したがって自由変数と定数は構成可能集合の中を動き、証明で等号や所属の証拠が必要なときには、⟨_⟩ がその命題の基礎型を取り出します。

open hPropStructure 𝒮ʟ

同じ構文には、互いに両立する二つの読み方があります。この絶対性の実例は、周囲の宇宙の構造 𝒮ᵥ から出発し、それを推移的クラス isL に制限します。外側の読みでは構成可能集合をその基礎にある周囲の集合として扱い、内側の読みでは定数がそれを名指す構成可能集合を表し、制限された構造が等号と所属を解釈します。本章では内側の充足関係を ⊨ と書きます。したがって γ : S ^ n に対する判断 γ ⊨ F は、有限環境 γ のもとで F が L の内部に成り立つことを意味します。これは、L 自身が名前を識別して比較する論理式に必要な読み方です。

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

これらの論理式は、環境内の位置によって先に与えられたデータを参照します。新しい束縛子の下では、もとの位置は新たに束縛された値を越えなければなりません。二つの束縛子の下では、位置 i は suc (suc i) になります。sh2 はこの移動を表す略記です。FreeAt が後続のアリティとその符号鍵を束縛してから骨格と空のアルファベットの符号集合を参照するとき、また表示の条件が候補要素と拡張環境を束縛してからもとのパラメータ環境を参照するときに使われます。

private
  sh2 : ∀ {n} → Fin n → Fin (suc (suc n))
  sh2 i = suc (suc i)

表示の条件の内部では、四つの値が環境に加わった後で初めて、骨格と台の符号集合を参照します。その四つは、候補要素 z、拡張環境 c、その定義域 k、そして考察中の鍵です。したがって、もとの位置を四回持ち上げる必要があります。sh4 はまさにこの移動を行い、その鍵が台の符号集合に属することと、k と骨格から作られる対に等しいことの両方を述べられるようにします。

  sh4 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc n))))
  sh4 i = suc (suc (suc (suc i)))

さらに一つの存在量化子が鍵に対応する値 v を束縛するため、satGraphAt を用いる時点では台が五つ先の位置にあります。ここで v は符号化された論理式を充足する環境全体の集合であり、真理値ではありません。続く所属原子は、拡張環境がその集合に属するかを問います。同じ移動は LexAt にも現れます。一つの添字、その位置で二つの環境から得られる値、より前の添字、そして両者の一致を証す共通の値を順に束縛すると、もとのパラメータ環境はやはり五つ先にあります。sh5 は両方の論理式に共通する添字計算を記録します。

  sh5 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc (suc n)))))
  sh5 i = suc (suc (suc (suc (suc i))))

空のアルファベットでも同じ符号

空のアルファベットは、空集合の要素の小さな表示 ⟪ ∅ ⟫ です。もし m がその記号の一つなら、埋め込み ⟪ ∅ ⟫↪ によって周囲の集合が得られ、表示の法則はそれが ∅ に属すると述べます。定理 ∅-empty はまさにそのような証拠を否定するので、noAlpha m が従います。したがって、このアルファベット上の論理式は定数の節を含めません。これは無パラメータ論理式の一つの構文的表示です。メタ言語の名前が用いる空の定数域 ⊥* と比較するには、この二つの空型を結び付ければ十分です。

private
  noAlpha : ⟪ ∅ {ℓ} ⟫ → Empty.⊥
  noAlpha m = ∅-empty (⟪ ∅ ⟫↪ m) (∈ₛ⟪ ∅ ⟫↪ m)

Fo∅ n は、n 個の変数位置を使える空のアルファベット上の論理式の族 Formula ⟪ ∅ ⟫ n を表す略記です。定数を含まないことは、論理式に別の述語を課すのではなく、定数記号の型そのものから従います。メタ言語の名前は、これに対応する族 Formula ⊥* n を使います。より正確には、Name が格納するのはアリティ、この族に属して変数位置を一つ余分にもつ無パラメータ論理式、そしてそのアリティのパラメータ列です。表示はこの三つから導かれるものであり、別の格納成分ではありません。

  Fo∅ : ℕ → Type ℓ
  Fo∅ = Formula ⟪ ∅ {ℓ} ⟫

写像 ε は、空のアルファベット ⟪ ∅ ⟫ から空の定数域 ⊥* への移行を与えます。仮に始域の記号 m が与えられれば、noAlpha m が矛盾を導き、空型の消去によって必要な終域の値が得られます。したがって mapFo ε は ⟪ ∅ ⟫ 上の論理式を ⊥* 上の論理式へ改名します。逆向きには、embed を ⊥* から ⟪ ∅ ⟫ への改名として特殊化できます。もともと定数の出現がないので、どちらの操作も定数の出現を変えません。そこで改名の合成則から、空のアルファベットによる特徴付けに必要な論理式の符号の等式が得られます。

  ε : ⟪ ∅ {ℓ} ⟫ → ⊥* {ℓ}
  ε m = Empty.rec (noAlpha m)

モデルの内部で無パラメータ論理式のコードを認識するには、まず「定数を持たない」ことの二つの表し方を結び付ける必要があります。⟪ ∅ ⟫ 上の論理式ψ では、定数域は空集合の要素の型です。一方、mapFo ε ψ は同じ構文を空型⊥* の上で表します。空集合の要素を仮定すれば矛盾が得られるため、写像 εを定義できます。したがって、ψ を直接宇宙へ読む経路と、ε に沿って改名してから宇宙へ埋め込む経路の違いは、空型から出る写像の違いだけです。関数外延性がそれらの写像を同一視し、mapFo-comp が改名の合成を同一視します。このように sameCode は、まず得られる宇宙上の論理式そのものの等式を証明します。後でこの等式にコード化写像を適用すれば、対応するコードの等式が得られます。

  sameCode : ∀ {n} (ψ : Fo∅ n) → mapFo ⟪ ∅ ⟫↪ ψ ≡ embed (mapFo ε ψ)
  sameCode ψ = cong (λ f → mapFo f ψ) (funExt (λ m → Empty.rec (noAlpha m)))
             ∙ sym (mapFo-comp ε Empty.rec* ψ)

逆向きの比較は、無パラメータ論理式 χ : Formula ⊥* n から始まります。まず χ を ⟪ ∅ ⟫ 上の論理式へ埋め込み、そのアルファベットから宇宙への包含写像に沿って改名することも、初めから宇宙上の論理式へ埋め込むこともできます。mapFo-comp によれば、前者は ⊥* からの一回の改名です。⊥*からの任意の二つの関数は等しいので、この改名は直接の埋め込みで使われるものと一致します。sameCode' の等式は、AllCodes ∅ʟ が埋め込まれた論理式に与えるキーを、χ の通常の宇宙上の論理式コードからなるキーへ移すのに必要な向きを持っています。

  sameCode' : ∀ {n} (χ : Formula (⊥* {ℓ}) n)
            → mapFo ⟪ ∅ {ℓ} ⟫↪ (embed χ) ≡ embed χ
  sameCode' χ = mapFo-comp Empty.rec* ⟪ ∅ ⟫↪ χ
              ∙ cong (λ f → mapFo f χ) (funExt (λ b → Empty.rec* b))

もう一つ、依存型に由来する問題があります。アリティは論理式の型の一部なので、等式 e : i ≡ j は ψ : Fo∅ i を subst Fo∅ e ψ : Fo∅ j へ移します。しかし、この移動の後もキーに入る論理式コードは同じでなければなりません。論理式を読み、コード化する関数の終域は固定された宇宙 V ℓ であり、アリティの添字には依存しません。したがって、一般の置換計算 constSubstCommSlice により、論理式を輸送してもコードは変わりません。codeShift はこの等式を、輸送後の論理式のコードから元のコードへ向かう形で記録し、復号の議論で行うアリティの調整に備えます。

  codeShift : {i j : ℕ} (e : i ≡ j) (ψ : Fo∅ i)
            → VCode.⌜ mapFo ⟪ ∅ ⟫↪ (subst Fo∅ e ψ) ⌝
            ≡ VCode.⌜ mapFo ⟪ ∅ ⟫↪ ψ ⌝
  codeShift e ψ = sym (constSubstCommSlice
    Fo∅ (V ℓ) (λ _ u → VCode.⌜ mapFo ⟪ ∅ ⟫↪ u ⌝) e ψ)

これで、コード集合との橋の直接な向きを証明できます。無パラメータな k 項論理式 χ を ⟪ ∅ ⟫ 上へ埋め込むと、その論理式のキーはkey∈AllCodes により AllCodes ∅ʟ に属します。このキーは、数項 # k と、埋め込まれた論理式を空のアルファベットを通して読んだコードとの対です。sameCode' はその論理式を χ の宇宙への直接の埋め込みと同一視し、後者のコードはちょうど fst (limitCode χ) です。この等式に沿って所属の証明を輸送すると freeCode-in が得られます。すなわち、コード集合はすべての無パラメータ論理式について、アリティとコードからなるキーを含みます。

freeCode-in : (k : ℕ) (χ : Formula (⊥* {ℓ}) k)
            → ⟨ pr (# k) (fst (limitCode χ)) ∈ fst (AllCodes ∅ʟ) ⟩
freeCode-in k χ =
  subst (λ u → ⟨ pr (# k) VCode.⌜ u ⌝ ∈ fst (AllCodes ∅ʟ) ⟩) (sameCode' χ)
    (key∈AllCodes ∅ʟ (embed χ))

逆向きでは、pr (# k) c が AllCodes ∅ʟ に属すると仮定します。除去定理AllCodes-out は、要素を命題的切り詰めの下でのみ復号し、入力には S の要素、すなわち集合とその構成可能性の証明を要求します。必要な入力の台集合はすでに pr (# k) c なので、残るのはその構成可能性の証明です。それが得られれば、PT.map read は切り詰められた各復号データを、求める k 項の無パラメータなデータへ変換します。この操作が命題的切り詰めを取り除くことはありません。

freeCode-out : (k : ℕ) (c : V ℓ) → ⟨ pr (# k) c ∈ fst (AllCodes ∅ʟ) ⟩
             → ∥ Σ[ χ ∈ Formula (⊥* {ℓ}) k ] (c ≡ fst (limitCode χ)) ∥₁
freeCode-out k c h = PT.map read (AllCodes-out ∅ʟ (pr (# k) c , cL) h)
  where
  cL : ⟨ isL (pr (# k) c) ⟩

不足していた証明書は、構成可能性の推移性から得られます。AllCodes ∅ʟ .snd はコード集合が構成可能であることを述べ、h はキーがその集合に属することを述べます。したがってisL-trans h (AllCodes ∅ʟ .snd) により、キー自身の構成可能性が証明されます。この証明書を pr (# k) c と組にすれば、AllCodes-out が要求する S の要素が得られます。ここでは新たな復号も選択も行われません。

  cL = isL-trans h (AllCodes ∅ʟ .snd)

命題的切り詰めの内部で、AllCodes-out はアリティ n、論理式ψ : Fo∅ n、そして与えられたキーが ψ のキーであることを示す等式を与えます。局所関数 read は、そのような各データを、要求されたアリティk の無パラメータ論理式と、c がそのコードに等しいことの証明へ変換します。まず ψ を ψ' : Fo∅ k へ輸送し、次に、現れ得ない定数を ε に沿って改名します。したがって構成される証人は mapFo ε ψ' です。対の等式は、輸送に必要なアリティの等式と、返される依存対に必要なコードの等式をともに与えます。

  read : Σ[ n ∈ ℕ ] Σ[ ψ ∈ Fo∅ n ] (pr (# k) c ≡ fst (keyS ∅ʟ ψ))
       → Σ[ χ ∈ Formula (⊥* {ℓ}) k ] (c ≡ fst (limitCode χ))
  read (n , (ψ , q)) = mapFo ε ψ' , (pr-inj q .snd ∙ step)
    where
    e : n ≡ k

キーの等式の二つの成分が構成を完成させます。第一成分の型は # k ≡ # nです。数項の単射性と対称性から e : n ≡ k が得られ、ψ はそれに沿ってψ' へ輸送されます。第二成分は、c が元の ψ から得られる宇宙上の論理式コードに等しいことを述べます。codeShift により、そのコードは輸送後の ψ' のコードと一致します。さらに sameCode により、後者はembed (mapFo ε ψ') のコードと一致します。これらの等式を合成すると、証人と組にすべき証明がちょうど得られます。read は PT.map を通してのみ使われるため、freeCode-out の結論は、そのような無パラメータ論理式が命題的切り詰めの下で存在するということだけです。コード集合から論理式を選び出してはいません。

    e = sym (#-inj′ (pr-inj q .fst))
    ψ' : Fo∅ k
    ψ' = subst Fo∅ e ψ
    step : VCode.⌜ mapFo ⟪ ∅ ⟫↪ ψ ⌝ ≡ VCode.⌜ embed (mapFo ε ψ') ⌝
    step = sym (codeShift e ψ) ∙ cong VCode.⌜_⌝ (sameCode ψ')

無パラメータ性を一つの原子で述べる

符号集合では、論理式はアリティと骨格からなるキーのもとに格納されます。このことを一つの所属原子で表すため、FreeAt はまずアリティ位置の値の後続を束縛し、次にその後続と骨格との対を束縛して、最後にその対が符号集合位置に属するかを問います。したがってメタ言語の記法では ∃[ z ] ∃[ y ] という形をもち、z が後続アリティ、y がキーです。各シフトは、一つまたは二つの束縛子の下から元のどの位置を参照するかを正確に記録します。この段階で論理式が述べるのは C₀ に置かれた集合への所属だけです。その位置を空のアルファベットの符号集合と同定して初めて、無パラメータ性という意味が得られます。

FreeAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
FreeAt C₀ s a =
  ∃̇ ( sucAtL (suc a) zero
    ∧̇ ∃̇ ( prAtL zero (suc zero) (sh2 s)
         ∧̇ (var zero ∈̇ var (sh2 C₀)) ) )

最初の一対の読みは、任意の環境 γ に対して成り立ちます。外側から与えられる等式 qa は、アリティ位置の値を数項 # k と同定します。これは意味論的な読みの仮定であり、FreeAt の内部にある別の節ではありません。骨格位置と符号集合位置はまだ任意なので、これらの補題は特定の符号集合を選ぶ前に、二つの束縛子の論理的内容だけを取り出しています。

module _ {n : ℕ} (C₀ s a : Fin n) (γ : S ^ n) (k : ℕ)
         (qa : fst (lookup a γ) ≡ # k) where

順方向の構成では、意図したキー pr (# (suc k)) (fst (lookup s γ)) がすでに C₀ 位置の集合に属すると仮定します。このキーから FreeAt が要求する二つの存在証人が得られます。最初は数項 # (suc k)、次はそれと骨格との対です。残るのは、これらの証人がそれぞれ後続と対の記述を満たすことの確認だけであり、最後の原子は仮定した所属そのものです。

  FreeAt-in : ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ fst (lookup C₀ γ) ⟩
            → ⟨ γ ⊨ FreeAt C₀ s a ⟩
  FreeAt-in h = ∣ numAt , ( hsuc , ∣ keyAt , ( hpr , h ) ∣₁ ) ∣₁
    where
    numAt : S

内部言語の存在証人は S の要素なので、その台となる集合には構成可能性の証明が伴わなければなりません。第一の証人 numAt には、すべての数項が L に属することからこの証明が得られます。第二の証人 keyAt については、所属の仮定がキーを C₀ 位置の構成可能集合に入れ、L の推移性がキー自身の構成可能性を与えます。これらの証明は数項とキーを束縛値として使えるようにするものであり、FreeAt に新たな数学的条件を加えるものではありません。

    numAt = # (suc k) , numL (suc k)
    keyAt : S
    keyAt = pr (# (suc k)) (fst (lookup s γ)) , isL-trans h (lookup C₀ γ .snd)
    hsuc : ⟨ (numAt ∷ γ) ⊨ sucAtL (suc a) zero ⟩
    hsuc = subst ⟨_⟩ (sym (sucAtL-adequate (suc a) zero (numAt ∷ γ)))

二つの補助論理式に対する妥当性の等式が、必要な確認を行います。hsuc では、等式 qa によってアリティ位置の値を # k に置き換え、その数項の後続が # (suc k) であることを使います。hpr では、prAtL の妥当性により、充足関係は二つの成分位置が指定する順序対との等しさに帰着します。keyAt はまさにその対として定義されています。こうして二つの意味論的事実が、選んだ証人を最後の所属原子へ結び付けます。

      (cong sucV (sym qa))
    hpr : ⟨ (keyAt ∷ numAt ∷ γ) ⊨ prAtL zero (suc zero) (sh2 s) ⟩
    hpr = subst ⟨_⟩
      (sym (prAtL-adequate zero (suc zero) (sh2 s) (keyAt ∷ numAt ∷ γ))) refl

逆方向の読みは、FreeAt の充足関係から所属を取り出します。存在論理式の充足関係は証人を命題的切り詰めの内側でしか与えないため、証明は外側の切り詰めを目標の所属命題へ消去します。外側の存在量化の一つの代表は、後続の証人と内側の存在論理式の充足関係を含みます。後者にはそれ自身の命題的切り詰めが残っており、次にもう一度消去されます。

  FreeAt-out : ⟨ γ ⊨ FreeAt C₀ s a ⟩
             → ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ fst (lookup C₀ γ) ⟩
  FreeAt-out = PT.rec (snd (pr (# (suc k)) (fst (lookup s γ))
                            ∈ fst (lookup C₀ γ))) atNum
    where

二回の切り詰め消去は同じ終域をもつので、証明はそれを Target と名付けます。その内容は、意図したキーが C₀ 位置の集合に属することです。集合への所属は命題値なので、この型は命題です。この事実こそ各切り詰め消去を使うための根拠であり、存在証人から特定の代表を選んでいるわけではありません。

    Target : Type (ℓ-suc ℓ)
    Target = ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ fst (lookup C₀ γ) ⟩

分岐 atKey は、内側の存在量化の一つの代表を扱います。外側の証人 z と、z がアリティ値の後続であるという等式を受け取り、さらに内側の証人 y と二つの事実を受け取ります。その二つは、y が対の論理式を満たすことと、その台となる集合が C₀ 位置の集合に属することです。内側の存在量化は命題的に切り詰められていますが、この消去分岐の内部では、その代表を用いて命題 Target を証明できます。

    atKey : (z : S) → fst z ≡ sucV (fst (lookup a γ))
          → Σ[ y ∈ S ] ( ⟨ (y ∷ z ∷ γ) ⊨ prAtL zero (suc zero) (sh2 s) ⟩
                       × ⟨ fst y ∈ fst (lookup C₀ γ) ⟩ )
          → Target
    atKey z qz (y , (hp , hy)) =

prAtL の妥当性は、y の台となる集合を、第一成分が z の台となる集合、第二成分が骨格である対と同定します。z に関する等式に続けて qa を用いると、その第一成分は # (suc k) と同定されます。したがって y は意図したキーです。与えられた y の所属をこの等式に沿って移送すれば、pr (# (suc k)) (fst (lookup s γ)) の所属、すなわち Target が得られます。

      subst (λ u → ⟨ u ∈ fst (lookup C₀ γ) ⟩)
        (subst ⟨_⟩ (prAtL-adequate zero (suc zero) (sh2 s) (y ∷ z ∷ γ)) hp
         ∙ cong (λ u → pr u (fst (lookup s γ))) (qz ∙ cong sucV qa)) hy

外側の消去分岐 atNum は、一つの代表 z と二つの証拠を受け取ります。第一の証拠は z が後続の論理式を満たすことを述べ、第二の hk は、まだ命題的に切り詰められた内側の存在論理式の充足関係です。したがって atNum はキーの第一成分を定める情報をすでにもつ一方、内側の証人は Target へ消去できる段階まで切り詰めの中に保ちます。

    atNum : Σ[ z ∈ S ] ( ⟨ (z ∷ γ) ⊨ sucAtL (suc a) zero ⟩
                       × ⟨ (z ∷ γ) ⊨ ∃̇ ( prAtL zero (suc zero) (sh2 s)
                                       ∧̇ (var zero ∈̇ var (sh2 C₀)) ) ⟩ )
          → Target
    atNum (z , (hs , hk)) = PT.rec (snd (pr (# (suc k)) (fst (lookup s γ))

sucAtL の妥当性は、第一の証拠を atKey が必要とする等式へ読み替えます。すなわち、z はアリティ位置の値の後続です。そこで証明は hk を命題 Target へ消去し、各代表に atKey を適用します。FreeAt-out にすでに組み込まれた外側の消去と合わせて、これで二層の存在量化が処理され、命題的切り詰めの境界も保たれます。

                                         ∈ fst (lookup C₀ γ)))
      (atKey z (subst ⟨_⟩ (sucAtL-adequate (suc a) zero (z ∷ γ)) hs)) hk

続く二つの読みでは、それまで任意だった二つの位置を具体化します。等式 q₀ は C₀ 位置の集合を AllCodes ∅ʟ と同定します。その要素は空のアルファベット上の論理式のキーです。また qa は、アリティ値を再び # k と同定します。これらの仮定のもとで、FreeAt-in と FreeAt-out が特徴付けた所属を、アリティ suc k の無パラメータ論理式についての具体的な主張へ変換できます。

module _ {n : ℕ} (C₀ s a : Fin n) (γ : S ^ n) (k : ℕ)
         (q₀ : fst (lookup C₀ γ) ≡ fst (AllCodes ∅ʟ))
         (qa : fst (lookup a γ) ≡ # k) where

FreeAt の充足関係から出発すると、FreeAt-out はキーが現在 C₀ 位置に置かれた集合に属することを与えます。q₀ に沿って移送すると、この所属は AllCodes ∅ʟ への所属になります。先に証明した復号補題 freeCode-out は、アリティ suc k の無パラメータ論理式 χ で、その極限段階の符号が骨格位置の値であるものを、命題的切り詰めのもとで返します。これが一つの所属原子の外向きの意味論的な読みです。

  codeFree-out : ⟨ γ ⊨ FreeAt C₀ s a ⟩
               → ∥ Σ[ χ ∈ Formula (⊥* {ℓ}) (suc k) ]
                     (fst (lookup s γ) ≡ fst (limitCode χ)) ∥₁
  codeFree-out h = freeCode-out (suc k) (fst (lookup s γ))
    (subst (λ u → ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ u ⟩) q₀

ここでアリティが suc k なのは、定義可能な部分集合の名前に使う論理式が、k 個のパラメータ位置に加えて、候補要素のための変数位置を一つ必要とするからです。codeFree-out が与える論理式の証人は、命題的に切り詰められたままです。FreeAt-out は所属が命題であるため自身の束縛された証人を局所的に消去できますが、最後の復号段階で freeCode-out が切り詰められた論理式の証人を与えます。したがって結論は、そのような論理式の存在だけを述べ、特定の一つを選びません。

      (FreeAt-out C₀ s a γ k qa h))

逆に codeFree-in は、アリティ suc k の具体的な無パラメータ論理式 χ と、その極限段階の符号を骨格位置の値と同定する等式から始めます。補題 freeCode-in は対応するキーを AllCodes ∅ʟ に入れます。次に符号の等式と q₀ の逆向きに沿って移送すると、その所属は実際の骨格位置と符号集合位置に移ります。最後に FreeAt-in が、得られた所属を二つの存在証人とともにまとめます。この方向では χ 自身が入力として与えられているため、命題的に切り詰められた論理式の証人を作る必要はありません。

  codeFree-in : (χ : Formula (⊥* {ℓ}) (suc k))
              → fst (lookup s γ) ≡ fst (limitCode χ) → ⟨ γ ⊨ FreeAt C₀ s a ⟩
  codeFree-in χ q = FreeAt-in C₀ s a γ k qa
    (subst (λ u → ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ u ⟩) (sym q₀)
      (subst (λ u → ⟨ pr (# (suc k)) u ∈ fst (AllCodes ∅ʟ) ⟩) (sym q)

アリティのスロットと空のアルファベットの符号集合のスロットを同定すれば、codeFree-out と codeFree-in がそろって FreeAt の意図した読みを与えます。外向きには、骨格が suc k 個の変数をもつ無パラメータ論理式の符号であることが、命題的切り詰めのもとで得られます。内向きには具体的な論理式が初めから与えられているので、そのような切り詰めは要りません。これで名前の論理式を認識できました。次の問いは、その有限なパラメータ環境が数 k をどのように記録するかです。

        (freeCode-in (suc k) χ)))

列の長さを読む

まず、集合として符号化されたグラフへの任意の所属を特徴づけます。g が Fin k で添字づけられ、pr x y が env g に属するなら、x ≡ # (toℕ i) かつ y ≡ g i となる添字 i が単に存在します。階層の集合への所属が記録するのは、生成元となる項目の単なる存在だけなので、結果は命題的切り詰めのもとに留まります。したがって memberOf は可能な添字を明らかにしますが、その一つを選び出しはしません。

private
  memberOf : (k : ℕ) (g : Fin k → V ℓ) (x y : V ℓ) → ⟨ pr x y ∈ env g ⟩
           → ∥ Σ[ i ∈ Fin k ] ((x ≡ # (toℕ i)) × (y ≡ g i)) ∥₁
  memberOf k g x y = PT.map
    (λ { (li , e) → lower li

所属の証人は、グラフに格納された項目と問い合わせた順序対との等式を含みます。順序対の構成子の単射性により、この一つの等式は二つの成分の等式に分かれます。証人では格納された項目が先に書かれているため、両方の成分のパスを逆向きにして、memberOf が必要とする向きにします。すなわち、x と y から、それぞれ数項の鍵と g の与える値へ向かう等式です。

       , (sym (pr-inj e .fst) , sym (pr-inj e .snd)) })

逆に、指定された各添字は一つの項目を与えます。i : Fin k に対して、順序対 pr (# (toℕ i)) (g i) は env g に属します。持ち上げられた添字が所属の証人となり、項目の等式は反射性です。こうして memberOf と entryOfは、この有限グラフの第一成分を認識するために必要な二つの向きを与えます。

  entryOf : (k : ℕ) (g : Fin k → V ℓ) (i : Fin k)
          → ⟨ pr (# (toℕ i)) (g i) ∈ env g ⟩
  entryOf k g i = ∣ lift i , refl ∣₁

定義域の順向きの包含は、pr x (fst y) がグラフに入るようなモデルの元y が単に存在することから始まります。目標は所属命題 x ∈ # k なので、外側の命題的切り詰めをこの目標へ消去できます。代表 y を一つ固定した後は、グラフへの所属から添字を復元し、その数項が # k に属することを示せば十分です。

  dom-into : (k : ℕ) (g : Fin k → V ℓ) (x : V ℓ)
           → ⟨ ∃[ y ∶ S ] pr x (fst y) ∈ env g ⟩ → ⟨ x ∈ # k ⟩
  dom-into k g x = PT.rec (snd (x ∈ # k)) atEntry
    where
    atIndex : (u : V ℓ) → Σ[ i ∈ Fin k ] ((x ≡ # (toℕ i)) × (u ≡ g i))

具体的な添字 i に対して、定義域が必要とするのは第一成分の等式だけです。toℕ i < k なので、数項に関する補題 #mono は # (toℕ i) を # k に入れます。さらに x ≡ # (toℕ i) に沿って輸送すれば、x もそこに属します。第二成分の等式はグラフの値を同定しますが、この包含には不要です。補助関数atEntry は値 y を固定してから、残る切り詰められた添字の情報を消去します。

            → ⟨ x ∈ # k ⟩
    atIndex u (i , (qx , _)) = subst (λ v → ⟨ v ∈ # k ⟩) (sym qx)
      (#mono (toℕ i) k (toℕ<n i))
    atEntry : Σ[ y ∈ S ] ⟨ pr x (fst y) ∈ env g ⟩ → ⟨ x ∈ # k ⟩
    atEntry (y , p) = PT.rec (snd (x ∈ # k)) (atIndex (fst y))

グラフへの所属に memberOf を適用すると、必要な添字の情報がちょうど得られますが、それはまだ命題的切り詰めのもとにあります。x ∈ # k は命題なので、PT.rec は各代表を atIndex に渡せます。これで添字を通常のデータとして取り出すことなく、順向きの包含が閉じます。

      (memberOf k g x (fst y) p)

逆向きの包含では x ∈ # k と仮定します。von Neumann 数項の消去により、ある自然数 m < k について x ≡ # m であることが、命題的切り詰めのもとで得られます。そのような m は Fin k の添字を定めます。結論もグラフの値の存在を命題的に切り詰めたものなので、PT.map はいずれかを選ぶことなく、各数項の証人を変換できます。仮定 cg は、その値をモデルの元として提示するために必要な構成可能性の証明を供給します。

  dom-from : (k : ℕ) (g : Fin k → V ℓ) → ((i : Fin k) → ⟨ isL (g i) ⟩)
           → (x : V ℓ) → ⟨ x ∈ # k ⟩ → ⟨ ∃[ y ∶ S ] pr x (fst y) ∈ env g ⟩
  dom-from k g cg x h = PT.map atNumeral (∈#-elim k x h)
    where
    atNumeral : Σ[ m ∈ ℕ ] ((m < k) × (x ≡ # m))

代表 m < k に対し、i を対応する有限添字とします。存在量化の証人はモデルの元 (g i , cg i)、すなわちその添字での値と構成可能性の証明です。グラフについての事実は entryOf から得られます。標準的な第一成分# (toℕ i) をもつ対が一つの項目だからです。この第一成分を x へ輸送すれば、pr x (g i) がグラフに属するという必要な所属が得られます。

              → Σ[ y ∈ S ] ⟨ pr x (fst y) ∈ env g ⟩
    atNumeral (m , (p , qx)) = (g i , cg i)
      , subst (λ u → ⟨ pr u (g i) ∈ env g ⟩) (sym qi) (entryOf k g i)
      where
      i : Fin k

変換 fromℕ' k m p は境界の証明 p : m < k から添字 i を作ります。その往復則 toFromId' は toℕ i ≡ m を証明します。x ≡ # m と、往復の等式を逆向きにして数項へ写したパスとを合成すると、qi : x ≡ # (toℕ i) が得られます。これは標準的な項目を問い合わせた第一成分へ移すためのパスそのものです。これで定義域の逆向きの包含も完成します。

      i = fromℕ' k m p
      qi : x ≡ # (toℕ i)
      qi = qx ∙ cong #_ (sym (toFromId' k m p))

これで、二つの集合レベルの包含を対象言語の定義域の論理式と対応させられます。環境 γ、族 g : Fin k → V ℓ、そしてスロット e の台集合を env g と同定する等式 qe を固定し、スロット d は定義域の候補として残します。各 cg i は g i が構成可能モデルの元であることを証明します。これは逆向きの包含が存在の証人を作るときに、まさに必要となる条件です。この文脈で、次の二つの補題が domAt e d を読み出し、また充填します。

module _ {n : ℕ} (e d : Fin n) (γ : S ^ n)
         (k : ℕ) (g : Fin k → V ℓ) (cg : (i : Fin k) → ⟨ isL (g i) ⟩)
         (qe : fst (lookup e γ) ≡ env g) where

γ が domAt e d を充足すると仮定します。スロット d の台集合が# k であることを示すため、domAt-numeral はモデルの元 lookup d γ と(# k , numL k) に L 内部の外延性を適用し、得られた等式を台集合へ射影します。したがって、構成可能な各試験要素 x について、定義域の候補への所属と数項への所属が同じ命題であることを示せば十分です。順向きの含意は、まず domAt-in によって定義域への所属を読み出します。

  domAt-numeral : ⟨ γ ⊨ domAt e d ⟩ → fst (lookup d γ) ≡ # k
  domAt-numeral h = cong fst (extensionalL {a = lookup d γ} {b = # k , numL k} pt)
    where
    fwd : (x : S) → ⟨ fst x ∈ fst (lookup d γ) ⟩ → ⟨ fst x ∈ # k ⟩
    fwd x hx = dom-into k g (fst x)

順向きの含意では、domAt-in がスロット d への所属を、x と対をなしてスロット e の集合に入る値の単なる存在へ変えます。qe に沿って輸送するとその項目は env g に入り、dom-into が x ∈ # k を与えます。逆に、dom-from は x ∈ # k を env g の項目の単なる存在へ変えます。定義域の候補への所属は命題なので、この切り詰めを消去できます。局所関数 put が、提示された各項目を処理します。

      (subst (λ u → ⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ u ⟩) qe
        (domAt-in e d γ h x hx))
    bwd : (x : S) → ⟨ fst x ∈ # k ⟩ → ⟨ fst x ∈ fst (lookup d γ) ⟩
    bwd x hx = PT.rec (snd (fst x ∈ fst (lookup d γ))) put (dom-from k g cg (fst x) hx)
      where

提示された一つの項目について、put はその所属を qe の逆向きに沿ってスロット e に格納されたグラフへ戻し、domAt-out によって第一成分のスロット d への所属を得ます。こうして二つの含意は ⇔toPath により、各 x で二つの所属命題の間のパスになります。外延性はそれらの点ごとのパスを、定義域の候補と # k との等式へ組み立てます。切り詰められたグラフの証人は所属を証明するためだけに用いられ、そこから値を選び出すことはありません。

      put : Σ[ y ∈ S ] ⟨ pr (fst x) (fst y) ∈ env g ⟩ → ⟨ fst x ∈ fst (lookup d γ) ⟩
      put (y , p) = domAt-out e d γ h x y
        (subst (λ u → ⟨ pr (fst x) (fst y) ∈ u ⟩) (sym qe) p)
    pt : (x : S) → (fst x ∈ fst (lookup d γ)) ≡ (fst x ∈ # k)
    pt x = ⇔toPath (fwd x) (bwd x)

逆向きは、スロット d の集合が実際に # k であるという等式から始まります。domAt e d を示すために、domAt-intro は定義域を規定する二つの含意を各要素について要求します。グラフに値が単に存在すれば d に属し、d に属すればグラフに値が単に存在する、という二つです。等式 qe と qdによって、これらはそれぞれ dom-into と dom-from に帰着します。したがって論理式の充填には、読み出しで用いた二つの集合レベルの包含を逆向きにして、そのまま用います。

  domAt-fill : fst (lookup d γ) ≡ # k → ⟨ γ ⊨ domAt e d ⟩
  domAt-fill qd = domAt-intro e d γ step
    where
    step : (x : S)
         → (⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ fst (lookup e γ) ⟩

定義域の論理式を充足させるには、各点で二つの含意を示せば十分です。まず、ある値と fst x の対がスロット e のグラフに属するとします。qe に沿って輸送すると、この項目は env g に入り、dom-into によって fst x が数項 # k に属することが分かります。さらに qd を逆向きに使って輸送すれば、スロット d の定義域候補への所属が得られます。

            → ⟨ fst x ∈ fst (lookup d γ) ⟩)
         × (⟨ fst x ∈ fst (lookup d γ) ⟩
            → ⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ fst (lookup e γ) ⟩)
    step x =
        (λ hy → subst (λ u → ⟨ fst x ∈ u ⟩) (sym qd) (dom-into k g (fst x)

逆向きの含意は、同じ道筋を反対にたどります。スロット d への所属を qd によって # k への所属へ移し、dom-from から、fst x と対をなして env g に入る値の単なる存在を得ます。最後に qe の逆向きに沿って、その項目をスロット e へ戻します。これで domAt-fill の二方向がそろい、有限グラフから特定の値を選び出す必要はありません。

          (subst (λ u → ⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ u ⟩) qe hy)))
      , (λ hx → subst (λ u → ⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ u ⟩) (sym qe)
          (dom-from k g cg (fst x) (subst (λ u → ⟨ fst x ∈ u ⟩) qd hx)))

充足関係グラフが割り当てる値

次に、充足関係グラフが実際の論理式の鍵で何を割り当てるかを調べます。周囲の環境 γ を固定し、スロット B から台を、x と y から鍵と値の候補を受け取ります。略記 Bs = lookup B γ により、以下の証明はこの三つのスロットについて一様に述べられます。ここで扱う論理式の定数は、台集合 fst Bs の要素によって添字づけられます。

module _ {n : ℕ} (B x y : Fin n) (γ : S ^ n) where
  private
    Bs : S
    Bs = lookup B γ

グラフの論理式は、十四個の束縛されたスロットを通して充足関係の再帰をまとめます。モデル言語の論理式 φ に対し、fr φ はそれらのスロットへ、台 Bs、その正準な充足関係表、子論理式の鍵からなるスロット、環境の塔、そして十個の構成子タグの数項を順に置き、その後ろに周囲の環境 γ を続けます。どの成分も、この台と論理式についてすでに構成された正準な対象です。

    fr : ∀ {m} (φ : Formula S m) → S ^ ( + n)
    fr φ = ev numν (Tower.tower Bs) (slot Bs φ) (satTable Bs φ) Bs γ

この十個の数項は符号領域の添字ではなく、表の仕様にある零から九までの十個の構成子節を表すタグです。tgs φ は、fr φ の各タグ用スロットが対応する構成子の数項をもつことを記録します。この対応により、まとめられた表の論理式は各構文の形に適切な節を選べます。

    tgs : ∀ {m} (φ : Formula S m) → Tags (fr φ) NN
    tgs φ = numTags (Tower.tower Bs) (slot Bs φ) (satTable Bs φ) Bs γ

充足関係表には、各アリティに対応する正しい環境の族も必要です。htow φ は、すでに得られている塔の定理を fr φ の各成分に適用します。塔のスロットには Tower.tower Bs、台のスロットには Bs、零番のタグ用スロットには必要な数項が入っています。したがって拡張された環境で towerAt が成り立ち、ここで塔について新たな議論を行う必要はありません。

    htow : ∀ {m} (φ : Formula S m) → ⟨ fr φ ⊨ towerAt Ei Bi (NN f0) ⟩
    htow φ = TowerHolds.holds Ei Bi (NN f0) (fr φ) Bs refl refl refl

正準な表の定義域は、論理式の鍵からなるスロットと一致します。一方では表の項目から始め、inSlot によってその鍵を slot Bs φ に入れます。項目は命題的切り詰めのもとで得られるので、その消去先は所属命題です。他方では total を使い、スロット内の各鍵に表の値が単に存在することを示します。domAt-intro がこの二つの含意を hdom φ にまとめます。

    hdom : ∀ {m} (φ : Formula S m) → ⟨ fr φ ⊨ domAt Ti Ci ⟩
    hdom φ = domAt-intro Ti Ci (fr φ)
      (λ z → (λ h → PT.rec (snd (fst z ∈ fst (slot Bs φ)))
                 (λ { (w , hw) → inSlot Bs φ (fst z) (fst w) hw }) h)
           , (λ h → total Bs φ (fst z) h))

これで順方向の読みを正確に述べられます。ψ を、定数が fst Bs の要素である論理式とします。スロット x が実際の鍵 keyS Bs ψ をもち、スロット y がモデル言語へ移した論理式 mapFo (asConst Bs) ψ の充足集合をもつなら、satGraphAt B x y が成り立ちます。この値は論理式を充足する環境の集合であり、一つの真理値ではありません。graphAt-value は正準な再帰の証人を graphAt-in に与えて、この主張を示します。

  graphAt-value : ∀ {m} (ψ : Formula ⟪ fst Bs ⟫ m)
                → fst (lookup x γ) ≡ fst (keyS Bs ψ)
                → fst (lookup y γ) ≡ fst (Sat Bs (mapFo (asConst Bs) ψ))
                → ⟨ γ ⊨ satGraphAt B x y ⟩
  graphAt-value {m} ψ qx qy = graphAt-in B x y γ

存在の証人は GraphWitAt が要求する順に、五つの正準な成分から組み立てられます。数項の割り当て numν、塔、スロット、充足関係表、そして台です。証人全体は、グラフの論理式における存在量化の意味に合わせて命題的切り詰めで包まれます。残るのは、選んだ成分が台、タグ、塔、閉包、定義域、項目、表の仕様を満たすことの確認です。

    ∣ numν
    , (Tower.tower Bs
    , (slot Bs φ
    , (satTable Bs φ
    , (Bs

台についての等式は反射性です。続く三つの証明は、十個のタグ用スロットが所定の数項をもち、環境のスロットが Bs 上の塔であり、slot Bs φ が直下の子論理式をもつ構成子について閉じていることを示します。最後の性質により、再帰的な表の節は、複合論理式の鍵で直下の子論理式の鍵にある項目を参照できます。

    , (refl
    , (tgs φ
    , (htow φ
    , (slotClosed Bs φ (Tower.tower Bs ∷ numν f0 ∷ numν f1 ∷ numν f2 ∷ numν f3
         ∷ numν f4 ∷ numν f5 ∷ numν f6 ∷ numν f7 ∷ numν f8 ∷ numν f9 ∷ γ)

最後の三つの条件は、表の定義域、選んだ項目、そして構成子節の仕様を確定します。すでに示した hdom φ が定義域の論理式を与えます。表の項目については、keyBridge Bs ψ が台の言語の論理式と φ の鍵を結び、qx と qy が正準な項目をスロット x と y の鍵と値へ輸送します。最後に SlotHolds.holds が、同じ台、タグ、塔、スロット、表から、正準な表が tableAt を充足することを示します。これで組み立てた証人がグラフの論理式を確立します。

    , (hdom φ
    , (subst2 (λ u v → ⟨ pr u v ∈ fst (satTable Bs φ) ⟩)
         (sym (qx ∙ keyBridge Bs ψ)) (sym qy) (entry-in Bs φ)
    , SlotHolds.holds Bs Ti Bi Ci Ei NN (fr φ) refl (tgs φ) (htow φ) ψ refl refl)))))))))) ∣₁
    where

ここで φ は ψ をモデル言語へ移したものです。ψ の定数は台集合の要素であり、asConst Bs はそれに、S の要素とみなすために必要な構成可能性の証明を添えます。mapFo はこの定数写像を論理式全体に適用します。上で別に用いた keyBridge により、翻訳前に直接符号化した鍵と、翻訳後にモデル内部で符号化した鍵の台集合が一致します。

    φ : Formula S m
    φ = mapFo (asConst Bs) ψ

逆方向では、satGraphAt B x y が成り立ち、スロット x が ψ の実際の鍵であると仮定します。graphAt-out が十四個の存在成分を与えるのは、命題的切り詰めのもとだけです。求める結論は累積階層 V における等式であり、setIsSet によってその等式型は命題です。したがって PT.rec は、グラフの証人を大域的に選ぶことなく、提示された各証人を局所的に調べられます。

  graphAt-only : ∀ {m} (ψ : Formula ⟪ fst Bs ⟫ m)
               → fst (lookup x γ) ≡ fst (keyS Bs ψ)
               → ⟨ γ ⊨ satGraphAt B x y ⟩
               → fst (lookup y γ) ≡ fst (Sat Bs (mapFo (asConst Bs) ψ))
  graphAt-only {m} ψ qx h = PT.rec (setIsSet _ _) read (graphAt-out B x y γ h)

一つのグラフの証人をほどくと、表の候補 T、符号領域 C、環境の塔 E、台 b、およびそれらの証明が得られます。ここで C が正準なスロットである必要はありません。必要なのは、C が子符号について閉じ、T がまとめられた表の節を充足し、実際の鍵が C に属することです。最後の所属は、提示された表の項目 ha に domAt-out を適用して得られます。この鍵の所属と同じ表の項目を SatSoundC.pinned に渡すと、ψ について表に記録された値が正準な充足集合に定まります。

    where
    read : GraphWitAt B x y γ → fst (lookup y γ) ≡ fst (Sat Bs (mapFo (asConst Bs) ψ))
    read (ν , (E , (C , (T , (b , (eb , (tg , (hE , (hc , (hd , (ha , h12))))))))))) =
      SatSoundC.pinned Ti Bi Ci Ei NN (ev ν E C T b γ) Bs eb tg hE hc h12
        ψ (subst (λ u → ⟨ u ∈ fst C ⟩) qx

固定の定理に必要な二つの前提は、初めは周囲の環境のスロット x で読まれます。qx に沿って輸送すると、hd と ha から得た定義域への所属は keyS Bs ψ が C に属するという所属になり、ha 自身は、その鍵とスロット y の値における T の項目になります。そこで固定の定理が必要な等式を返します。実際の論理式の鍵では、グラフが許すどの値も、翻訳された論理式の充足集合に一致します。

             (domAt-out Ti Ci (ev ν E C T b γ) hd (lookup x γ) (lookup y γ) ha))
        (lookup y γ)
        (subst (λ u → ⟨ pr u (fst (lookup y γ)) ∈ fst T ⟩) qx ha)

名前をスロット上で記述する

表示を定める本体は、候補 z を一つずつ調べます。最初の連言 z ∈ B は、記述される集合を台の内部に制限します。次に環境 c を束縛し、c がパラメータ環境 e の先頭に z を加えて得られる符号化環境であることを要求します。この時点では c と z が周囲の割り当ての前に置かれているので、e への参照は二つの束縛子を越えて移されます。

DenoteBody : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S (suc n)
DenoteBody B C s e =
  (var zero ∈̇ var (suc B))
  ∧̇ ∃̇ ( consAtL zero (suc zero) (sh2 e)
       ∧̇ ∃̇ ( domAt (suc zero) zero

残る三つの証人は、骨格をどのように解釈するかを定めます。まず k が拡張環境 c の定義域であることを要求します。次に key はスロット C の符号集合に属し、k と骨格の符号 s の対に等しくなければなりません。最後に v は、台 B の充足関係グラフがその鍵で許す値であり、末尾の所属は c ∈ v を述べます。C に台の実際の符号集合が入ると、これらの条件は、任意の鍵でグラフを参照するだけではなく、拡張環境が骨格を充足することを表します。

            ∧̇ ∃̇ ( (var zero ∈̇ var (sh4 C))
                 ∧̇ ( prAtL zero (suc zero) (sh4 s)
                   ∧̇ ∃̇ ( satGraphAt (sh5 B) (suc zero) zero
                        ∧̇ (var (suc (suc (suc zero))) ∈̇ var zero) ) ) ) ) )

メタ言語の名前は、アリティ、無パラメータ論理式、パラメータベクトルからなります。NameAt はそれらをアリティのスロット a、骨格の符号のスロット s、環境のスロット e で表し、表示のスロット d にはそのデータから導かれる集合を記録します。最初の連言は、a の後続と s から作った対が空のアルファベットの符号集合に属することを確かめます。この後続は欠かせません。a 個のパラメータをもつ名前には、候補となる要素を置く変数がもう一つ必要だからです。次の連言は、a がモデルの自然数の集合に属することを要求します。

NameAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n
       → Formula S n
NameAt B C C₀ s a e d =
  FreeAt C₀ s a
  ∧̇ ( (var a ∈̇ con ωʟ)

第三の連言は、e が定義域をちょうど a とし、B に値をとる環境であることを要求します。これにより、パラメータベクトルが一つ前のスロットに記録されたアリティと結び付きます。最後の連言は d を外延的に特徴づけます。各候補について、d への所属は DenoteBody の充足と同値であり、その本体の最初の連言がすでに候補を B の中に制限しています。したがって d は名前の三つのデータから導かれるもので、メタ言語の名前に追加で保存される成分ではありません。

    ∧̇ ( envOverAt e a B ∧̇ extAt d (DenoteBody B C s e) ) )

DenoteOf z は、DenoteBody の四層の存在量化に対応するメタ言語の中身です。拡張環境 c、その定義域の候補 k、論理式の鍵、グラフの値 v と、それらを結ぶすべての条件を記録します。これらを一つの依存対にまとめることで、対象言語の論理式を組み立てるのに必要な証人を明示しながら、後の条件が先に選んだ値に依存することも保たれます。

module _ {n : ℕ} (B C s e : Fin n) (γ : S ^ n) where
  DenoteOf : (z : S) → Type (ℓ-suc ℓ)
  DenoteOf z = Σ[ c ∈ S ] Σ[ k ∈ S ] Σ[ key ∈ S ] Σ[ v ∈ S ]
    ( ⟨ (c ∷ z ∷ γ) ⊨ consAtL zero (suc zero) (sh2 e) ⟩
    × ( ⟨ (k ∷ c ∷ z ∷ γ) ⊨ domAt (suc zero) zero ⟩

この中身は意味の連鎖をそのままたどります。最初の二つの充足の証明は、c がもとの環境を拡張することと、k がその定義域であることを述べます。C を AllCodes B で具体化すると、key が C に属するという条件により、続くグラフの参照が実際の論理式の符号で行われることが保証されます。次の明示的な等式は、その鍵を k と s の対と同一視します。最後の二つの証明は、v がこの鍵でのグラフの値であり、c が v に属することを述べます。ここで v は充足する環境の集合であって、ブール値の真理値ではありません。

      × ( ⟨ fst key ∈ fst (lookup C γ) ⟩
        × ( (fst key ≡ pr (fst k) (fst (lookup s γ)))
          × ( ⟨ (v ∷ key ∷ k ∷ c ∷ z ∷ γ) ⊨ satGraphAt (sh5 B) (suc zero) zero ⟩
            × ⟨ fst c ∈ fst v ⟩ ) ) ) ) )

DenoteBody-in は、この明示的な中身を本体の充足へ変えます。台への所属は外側の連言として残り、証人 c、k、key、v は四つの存在量化子と同じ順序で導入されます。ほとんどの条件は、初めから充足の証明として述べられています。例外は key を定める等式です。対の論理式の妥当性を表すパスが、この集合論的な等式を prAtL の充足へ変換します。

  DenoteBody-in : (z : S) → ⟨ fst z ∈ fst (lookup B γ) ⟩ → DenoteOf z
                → ⟨ (z ∷ γ) ⊨ DenoteBody B C s e ⟩
  DenoteBody-in z hz (c , (k , (key , (v , (hc , (hk , (hi , (hp , (hg , hm)))))))))
    = hz , ∣ c , (hc , ∣ k , (hk , ∣ key , (hi
    , ( subst ⟨_⟩ (sym (prAtL-adequate zero (suc zero) (sh4 s) (key ∷ k ∷ c ∷ z ∷ γ))) hp

対象言語の各存在量化子は命題的切り詰めによって解釈されるので、この構成は証明を閉じる前に四つの証人を一層ずつ切り詰めます。最後の行は、グラフの値から拡張環境まで、この四層を内側から順に閉じます。したがって得られる充足が記録するのは適切なデータの存在であり、切り詰められていない証人は、構成に用いた入力 DenoteOf z の側にだけ残ります。

      , ∣ v , (hg , hm) ∣₁ )) ∣₁) ∣₁) ∣₁

DenoteBody-out は、逆向きに読むときにも同じ境界を保ちます。台への所属はすべての存在量化子の外側にあるので、直接取り出せます。しかし四つの証人は、入れ子になった命題的切り詰めの内側でしか現れません。切り詰めの消去先は毎回 ∥ DenoteOf z ∥₁ であり、これも命題です。そのため、各局所的な証人の組を変換することはできますが、一つの組を大域的に選ぶことはありません。

  DenoteBody-out : (z : S) → ⟨ (z ∷ γ) ⊨ DenoteBody B C s e ⟩
                 → ⟨ fst z ∈ fst (lookup B γ) ⟩ × ∥ DenoteOf z ∥₁
  DenoteBody-out z (hz , hc) = hz , PT.rec squash₁
    (λ { (c , (hc , hk)) → PT.rec squash₁
      (λ { (k , (hk , hkey)) → PT.rec squash₁

鍵の層では、本体は対の論理式の充足を与えますが、DenoteOf が要求するのは、復号された等式 fst key ≡ pr (fst k) (fst (lookup s γ)) です。対の論理式の妥当性を表すパスを順方向に読むと、ちょうどこの等式が得られます。最も内側の写像は、証人 v とともにグラフの証明と所属の証明を保ち、外側の消去が中身全体を一つの命題的切り詰めの下で組み立て直します。

        (λ { (key , (hi , (hp , hv))) → PT.map
          (λ { (v , (hg , hm)) → c , (k , (key , (v , (hc , (hk , (hi
            , ( subst ⟨_⟩
                  (prAtL-adequate zero (suc zero) (sh4 s) (key ∷ k ∷ c ∷ z ∷ γ)) hp
              , (hg , hm) ))))))) }) hv }) hkey }) hk }) hc

NameAt-in は五つの入力を取ります。最初の三つは固定された連言を示します。すなわち、骨格が指定されたアリティで無パラメータであること、アリティがモデルの自然数の集合に属すること、パラメータのグラフが台の上の環境であることです。残る二つは、表示を特徴づけるための点ごとの二方向を与えます。一方は z ∈ d から z ∈ B と明示的な DenoteOf z を返し、他方は z ∈ B と明示的な DenoteOf z から z ∈ d を導きます。

module _ {n : ℕ} (B C C₀ s a e d : Fin n) (γ : S ^ n) where
  NameAt-in : ⟨ γ ⊨ FreeAt C₀ s a ⟩
            → ⟨ fst (lookup a γ) ∈ ω ⟩
            → ⟨ γ ⊨ envOverAt e a B ⟩
            → ((z : S) → ⟨ fst z ∈ fst (lookup d γ) ⟩

二つの方向は、どちらも候補ごとに述べられます。extAt が集合の等しさを点ごとの所属で表すからです。ここでは意図的に、切り詰められていない DenoteOf z を使います。この補題は導入規則なので、呼び出す側が本体の充足を組み立てるための具体的なデータを与えます。NameAt の任意の充足からそのデータを復元する仕事は別の妥当性の議論に属し、次章で得られる復元結果も命題的切り詰めの下に残ります。

               → ⟨ fst z ∈ fst (lookup B γ) ⟩ × DenoteOf B C s e γ z)
            → ((z : S) → ⟨ fst z ∈ fst (lookup B γ) ⟩ → DenoteOf B C s e γ z
               → ⟨ fst z ∈ fst (lookup d γ) ⟩)
            → ⟨ γ ⊨ NameAt B C C₀ s a e d ⟩
  NameAt-in hf ha he into back =

証明は、この二方向を extAt の導入規則へ渡します。z ∈ d からは、一方の入力が台への所属と中身を与え、DenoteBody-in がそれらを本体の充足へ変換します。逆に、本体の充足は DenoteBody-out によって、台への所属と命題的に切り詰められた中身として読まれます。目標の z ∈ d は命題なので、この切り詰めを消去してもう一方の入力を適用できます。こうして得た外延的な特徴づけを最初の三入力と組み合わせると、名前の論理式全体が充足されます。

    hf , (ha , (he , extAt-in-both d (DenoteBody B C s e) γ
      (λ z hz → DenoteBody-in B C s e γ z (into z hz .fst) (into z hz .snd))
      (λ z h → PT.rec (snd (fst z ∈ fst (lookup d γ)))
                 (back z (DenoteBody-out B C s e γ z h .fst))
                 (DenoteBody-out B C s e γ z h .snd))))

再帰をもたない順序

続く比較の論理式はデータをまとまった束縛子で導入するため、周囲の割り当てへの参照を一様に移す必要があります。sh3 は、周囲のスロットを三つの新しい束縛子の先へ移します。LexAt では、この三つに添字 i と、二つのパラメータ環境から i で読み出した値が入ります。その下でも、もとの二つの環境とパラメータ順序のスロットを参照できます。後の LeastNameAt でも同じ移動を使い、競合する名前の骨格、アリティ、環境を束縛した先へ周囲のスロットを運びます。

private
  sh3 : ∀ {n} → Fin n → Fin (suc (suc (suc n)))
  sh3 i = suc (suc (suc i))

sh6 は、対応する移動を六つの束縛子について行います。StepBody が二つの名前を束縛するときに使われ、各名前は骨格、アリティ、パラメータ環境によって表されます。そのため、完全に拡張された割り当てでは六つの新しい値がもとの割り当ての前に置かれますが、台、二つの順序関係、二つの符号集合、比較する二つの表示は周囲のスロットとして残ります。これらの移動は参照先を保つだけであり、順序の仮定を加えたり、それ自体で比較を行ったりはしません。

  sh6 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc (suc (suc n))))))
  sh6 i = suc (suc (suc (suc (suc (suc i)))))

パラメータの鍵は、二つのパラメータ環境が最初に異なる位置を求めます。LexAt はまず、アリティのスロットにある集合の元 i を束縛します。そのスロットにアリティの数項が入っていれば、その元はちょうど、それより小さい位置を表す数項です。したがって、この有界存在量化子だけで可能な添字をすべて動かせ、添字のための別の順序は必要ありません。

LexAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S n
LexAt P a e₁ e₂ =
  ∃̇∈ (var a) (
    ∃̇ ( ∃̇ ( appAt (sh3 e₁) (suc (suc zero)) (suc zero)
           ∧̇ ( appAt (sh3 e₂) (suc (suc zero)) zero

i を選ぶと、続く二つの存在量化子が値 u と v を与え、e₁(i)=u と e₂(i)=v を述べます。第三の適用は、u と v の順序対がパラメータ関係 P に属すことを主張します。次の有界全称量化子は各 j ∈ i を調べ、それぞれについて、二つの環境グラフがともに j で取る値 x が単に存在することを要求します。したがって論理式の内容は、「この位置では厳密に小さく、それ以前の各位置では共通の値をもつ」です。共通の値から対応するパラメータの等しさを導けるのは、二つの環境を一価なグラフと同定した後です。後の妥当性証明では、グラフの参照に関する性質と台の埋め込みの単射性が、まさにこの含意を与えます。論理式そのものは再帰を行いません。

             ∧̇ ( appAt (sh3 P) (suc zero) zero
               ∧̇ ∀̇∈ (var (suc (suc zero))) (
                    ∃̇ ( appAt (sh5 e₁) (suc zero) zero
                      ∧̇ appAt (sh5 e₂) (suc zero) zero ) ) ) ) ) ) )

名前全体の比較は、骨格の符号、アリティ、パラメータ環境という三つの鍵を辞書式の優先順位で組み合わせます。第一の選言は、スロット R の関係を s₁ と s₂ に適用します。適用の妥当性により、これは二つの骨格の符号からなる順序対が R に属すという意味です。R をスロットのままにすることで、同じ論理式を異なる割り当てに使えます。後の妥当性定理では、極限段階の符号順序を表す関係がここに入ります。

≺At : ∀ {n} → Fin n → Fin n
    → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Formula S n
≺At R P s₁ a₁ e₁ s₂ a₂ e₂ =
      appAt R s₁ s₂
  ∨̇ ( (var s₂ ≐ var s₁)

第二の選言は、骨格の符号が等しい場合を扱います。まず等しさを s₂ = s₁ の向きで記録し、その後に残る二つの辞書式の場合を並べます。両方のアリティのスロットが数項なら、a₁ ∈ a₂ は第一のアリティが小さいことを意味します。もう一つの分岐は a₂ = a₁ を要求し、LexAt P a₁ e₁ e₂ が最初に異なるパラメータで比較を決めます。s₂ = s₁ と a₂ = a₁ という向きは、第二の名前の符号とパラメータベクトルを第一の名前のデータへ移す、後の輸送の向きに合っています。

    ∧̇ ( (var a₁ ∈̇ var a₂)
      ∨̇ ( (var a₂ ≐ var a₁) ∧̇ LexAt P a₁ e₁ e₂ ) ) )

LexAt の読みを繰り返し使える形で証明するため、一致を述べる存在量化子の下にある本体を取り出して名前を付けます。先行する位置 j で、Body は同じ値 x が二つの適用をともに満たすこと、すなわち二つの環境グラフがともに j で値 x をもつことを要求します。拡張された割り当てには x、j、v、u、i の五項が新しく並ぶので、周囲の環境スロットへの参照は五つの束縛子を越えて移されます。

module _ {n : ℕ} (P a e₁ e₂ : Fin n) (γ : S ^ n) where
  private
    Body : Formula S (suc (suc (suc (suc (suc n)))))
    Body = appAt (sh5 e₁) (suc zero) zero ∧̇ appAt (sh5 e₂) (suc zero) zero

i、u、v を固定すると、Inner i u v は最初の三つの存在束縛子の後に残る本体を記録します。最初の二成分は、グラフ e₁ と e₂ がそれぞれ対 (i,u) と (i,v) を含むことを述べます。第三の成分は、対 (u,v) が関係 P に属すことを述べます。これらはまだ appAt の充足を表す主張です。二つの表示を明示的に結べるように、解読後の所属の形は別に記録します。

    Inner : (i u v : S) → Type (ℓ-suc ℓ)
    Inner i u v =
      ⟨ (v ∷ u ∷ i ∷ γ) ⊨ appAt (sh3 e₁) (suc (suc zero)) (suc zero) ⟩
      × ( ⟨ (v ∷ u ∷ i ∷ γ) ⊨ appAt (sh3 e₂) (suc (suc zero)) zero ⟩
        × ( ⟨ (v ∷ u ∷ i ∷ γ) ⊨ appAt (sh3 P) (suc zero) zero ⟩

Inner の第四成分は、i より下での一致です。i に属するモデルの各要素 j に対し、一つの x が Body を満たすという意味論上の存在式 ∃[ x ∶ S ] を与えます。この存在式は命題的切り詰めです。j で共通の値が存在することは保ちますが、選ばれた値をデータとして外へ出しません。したがって有界全称量化子は、各 j ∈ i に対して、そのように切り詰められた存在を一つ与える関数として読まれます。

          × ((j : S) → ⟨ fst j ∈ fst i ⟩
             → ⟨ ∃[ x ∶ S ] (x ∷ j ∷ v ∷ u ∷ i ∷ γ) ⊨ Body ⟩) ) )

Agrees i は、二つの適用を解読した形で同じ一致を述べます。各 j ∈ i について、j と x の底にある集合から作った対がグラフ e₁ と e₂ の両方に属すような元 x : S が単に存在します。i がアリティの数項なら、その元はちょうど先行する位置を表します。この定義が記録するのは共通のグラフ値だけです。対応するメタレベルのパラメータの等しさは、既知の環境グラフと台の埋め込みの単射性から後で導かれます。

  Agrees : (i : S) → Type (ℓ-suc ℓ)
  Agrees i = (j : S) → ⟨ fst j ∈ fst i ⟩
           → ∥ Σ[ x ∈ S ] ( ⟨ pr (fst j) (fst x) ∈ fst (lookup e₁ γ) ⟩
                          × ⟨ pr (fst j) (fst x) ∈ fst (lookup e₂ γ) ⟩ ) ∥₁

Differs は、最初の相違を示す証人を解読した完全な形でまとめます。添字 i、値 u と v、アリティのスロットにある集合への i の所属、対 (i,u) と (i,v) のグラフへの所属、その位置での厳密なパラメータ比較、そして Agrees i が含まれます。アリティのスロットが数項で、二つのグラフのスロットがそのアリティのパラメータ環境なら、これらは辞書式の最初の相違に必要なデータそのものです。

  Differs : Type (ℓ-suc ℓ)
  Differs = Σ[ i ∈ S ] Σ[ u ∈ S ] Σ[ v ∈ S ]
    ( ⟨ fst i ∈ fst (lookup a γ) ⟩
    × ( ⟨ pr (fst i) (fst u) ∈ fst (lookup e₁ γ) ⟩
      × ( ⟨ pr (fst i) (fst v) ∈ fst (lookup e₂ γ) ⟩

厳密な比較のフィールドは、≺At の符号の場合と同じ関係の形を取ります。u と v の底にある値から作った順序対が、スロット P の集合に属すという形です。最後の Agrees i は、それ以前の各位置で共通の値があることを記録します。意図した一価な環境グラフについては、これが、それ以前のパラメータに相違がないことを保証します。こうして Differs は、最初の相違を示す証人の数学的内容を、それを表す対象言語の束縛構造から分けて記録します。

        × ( ⟨ pr (fst u) (fst v) ∈ fst (lookup P γ) ⟩ × Agrees i ) ) ) )

写像 pack が変換するのは、Inner の一致の成分だけです。最初の三成分は、この局所的な変換には使いません。j ∈ i を固定すると、意味論上の存在式の証人 x には、appAt を充足する二つの証明が伴います。それぞれに appAt-adequate を適用すれば、同じ証人 x を保ったまま、Agrees が要求する二つのグラフ所属が得られます。

  private
    pack : (i u v : S) → Inner i u v → Agrees i
    pack i u v (_ , (_ , (_ , hj))) j hj' = PT.map
      (λ { (x , (p₁ , p₂)) → x
         , ( subst ⟨_⟩

この変換は、すでにある命題的切り詰めの内部で行われます。PT.map は、可能な各証人と二つの適用の証明を、同じ証人と二つの所属の証明へ写します。目標も切り詰められた存在なので、代表を取り出す必要はなく、選択原理も使いません。各点で写すだけで、すべての先行する位置について Agrees i に必要な結論が得られます。

               (appAt-adequate (sh5 e₁) (suc zero) zero (x ∷ j ∷ v ∷ u ∷ i ∷ γ)) p₁
           , subst ⟨_⟩
               (appAt-adequate (sh5 e₂) (suc zero) zero (x ∷ j ∷ v ∷ u ∷ i ∷ γ)) p₂ ) })
      (hj j hj')

unpack は、もとの論理式を充足するために必要な逆向きの変換を与えます。Agrees i と位置 j ∈ i から、切り詰められた共通値の証人を受け取ります。それぞれの代表 x をそのまま保ち、二つのグラフ所属を Body にある二つの適用の充足へ戻します。

    unpack : (i u v : S) → Agrees i
           → (j : S) → ⟨ fst j ∈ fst i ⟩
           → ⟨ ∃[ x ∶ S ] (x ∷ j ∷ v ∷ u ∷ i ∷ γ) ⊨ Body ⟩
    unpack i u v hj j hj' = PT.map
      (λ { (x , (p₁ , p₂)) → x

ここでは同じ妥当性のパスを逆向きに使います。各所属の証明を appAt-adequate の対称なパスに沿って輸送すると、Body の対応する連言が得られます。ここでも PT.map によって構成全体が切り詰められた存在の内部に留まるため、unpack は共通の値を大域的に選ぶことなく、必要な意味論上の存在を証明できます。

         , ( subst ⟨_⟩
               (sym (appAt-adequate (sh5 e₁) (suc zero) zero (x ∷ j ∷ v ∷ u ∷ i ∷ γ))) p₁
           , subst ⟨_⟩
               (sym (appAt-adequate (sh5 e₂) (suc zero) zero (x ∷ j ∷ v ∷ u ∷ i ∷ γ))) p₂ ) })
      (hj j hj')

LexAt-in は、Differs にある明示的なデータから始めます。添字 i と値 u、v は、有界存在量化子と、それに続く二つの存在量化子の証人になり、hi が i が限界内にあることを証明します。拡張された割り当て γ₃ = v ∷ u ∷ i ∷ γ では、最初の二つのグラフ所属を appAt-adequate に沿って逆向きに輸送し、e₁(i)=u と e₂(i)=v を表す二つの適用を充足させます。残る関係と一致のフィールドも同じ連言構造に入り、有界全称の成分は unpack が与えます。

  LexAt-in : Differs → ⟨ γ ⊨ LexAt P a e₁ e₂ ⟩
  LexAt-in (i , (u , (v , (hi , (h₁ , (h₂ , (hp , hj)))))))
    = ∣ i , (hi , ∣ u , ∣ v
    , ( subst ⟨_⟩ (sym (appAt-adequate (sh3 e₁) (suc (suc zero)) (suc zero) γ₃)) h₁
      , ( subst ⟨_⟩ (sym (appAt-adequate (sh3 e₂) (suc (suc zero)) zero γ₃)) h₂

Differs の最後の二つの成分が導入の証明を完成させます。(u,v) が Pに属すという証明を appAt-adequate に沿って逆向きに輸送すると、第三の適用についての充足関係の証明になり、unpack は i より前での一致を有界全称量化子の意味論的な形へ変えます。割り当てγ₃ = v ∷ u ∷ i ∷ γ は三つの束縛の順序を明示しており、周囲の構成子がv、u、i の存在量化子を内側から順に閉じます。

        , ( subst ⟨_⟩ (sym (appAt-adequate (sh3 P) (suc zero) zero γ₃)) hp
          , unpack i u v hj ) ) ) ∣₁ ∣₁) ∣₁
    where
    γ₃ : S ^ (suc (suc (suc n)))
    γ₃ = v ∷ u ∷ i ∷ γ

LexAt を外向きに読むときは、その存在量化子が設けた証人の境界を保たなければなりません。そのため LexAt-out の行き先は命題 ∥ Differs ∥₁ であり、外側の切り詰めはこの行き先の中へだけ消去されます。局所関数 atValue が実際の数学的な復号を担います。各消去の局所的な範囲で、具体的な i、u、v、境界の証明、残りの充足関係のデータが得られれば、切り詰められていないDiffers の記録を作れます。その記録を局所的な範囲の外へ選び出すことはありません。

  LexAt-out : ⟨ γ ⊨ LexAt P a e₁ e₂ ⟩ → ∥ Differs ∥₁
  LexAt-out = PT.rec squash₁ atIndex
    where
    atValue : (i u v : S) → ⟨ fst i ∈ fst (lookup a γ) ⟩ → Inner i u v → Differs
    atValue i u v hi h@(h₁ , (h₂ , (hp , _))) = i , (u , (v

atValue の前半は、添字と二つのグラフ参照を復元します。境界の証明 hiは、すでに Differs が要求する形です。二つの妥当性のパスを順方向に読むと、適用についての充足関係は、(i,u) の e₁ への所属と (i,v) の e₂ への所属にそれぞれ変わります。したがって二つの値は、論理式がそれらを見つけた同じ添字に結び付いたままです。

      , ( hi
        , ( subst ⟨_⟩
              (appAt-adequate (sh3 e₁) (suc (suc zero)) (suc zero) (v ∷ u ∷ i ∷ γ)) h₁
          , ( subst ⟨_⟩
                (appAt-adequate (sh3 e₂) (suc (suc zero)) zero (v ∷ u ∷ i ∷ γ)) h₂

第三の適用も同じように復号され、(u,v) がパラメータ関係 P に属すことが得られます。関数 pack は、有界な範囲で適用の形を取っていた一致をAgrees i が要求する二つのグラフ所属へ翻訳し、最後の成分を与えます。これらのデータは atValue の内部で明示的な Differs の記録をなしますが、周囲の消去が最終的に保つのはその命題的切り詰めだけです。

            , ( subst ⟨_⟩
                  (appAt-adequate (sh3 P) (suc zero) zero (v ∷ u ∷ i ∷ γ)) hp
              , pack i u v h ) ) ) ) ))

最も内側の存在量化子は、第二の値 v と Inner i u v を与えますが、両者を使えるのはその切り詰めの内部だけです。処理関数 atSecond は、局所的に得られた各組 (v,h) から atValue で Differs を作り、ただちに∥ Differs ∥₁ へ入れます。これは命題的切り詰めに許された消去そのものです。証人は命題を証明するために使われますが、結果から外へ現れることはありません。

    atSecond : (i u : S) → ⟨ fst i ∈ fst (lookup a γ) ⟩
             → Σ[ v ∈ S ] Inner i u v → ∥ Differs ∥₁
    atSecond i u hi (v , h) = ∣ atValue i u v hi h ∣₁

一つ外の層で、atFirst は具体的な第一の値 u と、第二の値の存在を切り詰めたものを受け取ります。その内側の切り詰めを atSecond で消去すると、行き先は再び ∥ Differs ∥₁ です。したがって、第一の値から完成した最初の相違の記録へ進むあいだも、大域的に使える v を取り出す必要はありません。

    atFirst : (i : S) → ⟨ fst i ∈ fst (lookup a γ) ⟩
            → Σ[ u ∈ S ] ∥ Σ[ v ∈ S ] Inner i u v ∥₁ → ∥ Differs ∥₁
    atFirst i hi (u , h) = PT.rec squash₁ (atSecond i u hi) h

最後に atIndex は、添字 i、それがアリティより小さいことを示す hi、そして u から始まる残りを切り詰めたものを受け取ります。その残りをatFirst で消去すれば、外向きの読みは完成します。三つの処理関数は合わせて、i、u、v という存在量化子の入れ子をたどり、どの消去も同じ命題を行き先とします。したがって LexAt-out が示すのは、最初の相違の記録が単に存在することだけであり、その添字や値を選ぶことではありません。

    atIndex : Σ[ i ∈ S ] ( ⟨ fst i ∈ fst (lookup a γ) ⟩
                         × ∥ Σ[ u ∈ S ] ∥ Σ[ v ∈ S ] Inner i u v ∥₁ ∥₁ )
            → ∥ Differs ∥₁
    atIndex (i , (hi , h)) = PT.rec squash₁ (atFirst i hi) h

比較と順序族の一ステップを読む

メタレベルの中身 Below は、三つの比較の鍵を ≺At と同じ優先順位で並べます。外側の直和は、骨格の符号からなる順序対 (s₁,s₂) がスロット R の関係に属すか、または符号が等しく、後の鍵が比較を決めることを表します。この直和の要素は、どの枝に入るかを明示してその証拠を運びますが、任意のスロットの値について枝を判定できると主張する定義ではありません。この区別が必要なのは、対象言語の選言が命題的切り詰めによって解釈されるからです。

module _ {n : ℕ} (R P s₁ a₁ e₁ s₂ a₂ e₂ : Fin n) (γ : S ^ n) where
  Below : Type (ℓ-suc ℓ)
  Below = ⟨ pr (fst (lookup s₁ γ)) (fst (lookup s₂ γ)) ∈ fst (lookup R γ) ⟩
        ⊎ ( (fst (lookup s₂ γ) ≡ fst (lookup s₁ γ))
          × ( ⟨ fst (lookup a₁ γ) ∈ fst (lookup a₂ γ) ⟩

骨格の符号が等しい場合、内側の直和はまずアリティの比較 a₁ ∈ a₂ を提示します。二つのスロットがアリティの数項を含むとき、この所属は第一のアリティのほうが小さいことを意味します。アリティも等しければ、Differs がパラメータの鍵について最初の相違の証拠を与えます。二つの等しさは意図的に s₂ = s₁ とa₂ = a₁ の向きに置かれ、後で第二の名前のデータを第一の名前の型へ輸送する向きに合っています。

            ⊎ ( (fst (lookup a₂ γ) ≡ fst (lookup a₁ γ))
              × Differs P a₁ e₁ e₂ γ ) ) )

≺At-in は、明示的な Below のデータを比較の論理式の充足関係へ翻訳します。符号の枝では、関係への所属を appAt-adequate に沿って逆向きに輸送し、外側の左の選言として導入します。アリティの枝では、符号の等しさとともに外側の右の選言へ入り、アリティの所属を内側の左の選言へ入れます。ここで行うのは導入だけです。与えられた枝の証拠を、対象言語の各選言に伴う切り詰められた意味へ包みます。

  ≺At-in : Below → ⟨ γ ⊨ ≺At R P s₁ a₁ e₁ s₂ a₂ e₂ ⟩
  ≺At-in (inl h) =
    ∣ inl (subst ⟨_⟩ (sym (appAt-adequate R s₁ s₂ γ)) h) ∣₁
  ≺At-in (inr (q , inl h)) = ∣ inr (q , ∣ inl h ∣₁) ∣₁
  ≺At-in (inr (q , inr (q' , h))) =

パラメータの枝は、二つの選言の右側を順に進みます。符号とアリティの等しさをそれぞれの右の枝へ運び、与えられた Differs の記録を LexAt-in に渡します。こうして、すでに復号された最初の相違のデータがパラメータの節の充足関係になります。したがって Below の三つの場合はすべて、枝を探索したり存在証人を取り出したりせずに ≺At へ導入できます。

    ∣ inr (q , ∣ inr (q' , LexAt-in P a₁ e₁ e₂ γ h) ∣₁) ∣₁

逆向きの読みの行き先は、必然的に弱い ∥ Below ∥₁ です。外側の対象言語の選言についての充足関係自体が切り詰められているため、PT.rec が枝を調べられるのは、この命題を構成する局所的な範囲に限られます。局所関数 outer は符号の場合と符号が等しい場合を分けます。後者では等しさ s₂ = s₁ を保ち、まだ分類されていない内側の選言を inner に渡します。

  ≺At-out : ⟨ γ ⊨ ≺At R P s₁ a₁ e₁ s₂ a₂ e₂ ⟩ → ∥ Below ∥₁
  ≺At-out = PT.rec squash₁ outer
    where
    inner : (fst (lookup s₂ γ) ≡ fst (lookup s₁ γ))
          → ⟨ fst (lookup a₁ γ) ∈ fst (lookup a₂ γ) ⟩

符号の等しさが与えられると、inner は残る二つの鍵を読みます。アリティの所属が得られれば、ただちに Below の中間の場合になります。もう一方の中身には、アリティの等しさ a₂ = a₁ と LexAt の充足関係があり、復号すべきものは最初の相違の成分だけです。関数の型は、二つの場合に共通する符号の等しさを固定したまま、これらの選択肢を明示しています。

          ⊎ ( (fst (lookup a₂ γ) ≡ fst (lookup a₁ γ))
            × ⟨ γ ⊨ LexAt P a₁ e₁ e₂ ⟩ )
          → ∥ Below ∥₁
    inner q (inl h) = ∣ inr (q , inl h) ∣₁
    inner q (inr (q' , h)) =

パラメータの場合、LexAt-out が与えるのは ∥ Differs ∥₁ だけであり、存在の意味論が要求する境界を正確に保っています。PT.map は、その中で局所的に表された各 Differs の記録を Below の第三の場合へ写し、すでに得られた符号とアリティの等しさを付け加えます。結果は一つの命題的切り詰めの下に留まるので、この変換は存在を存在へ移すだけで、最初の相違の証人を選ぶことはありません。

      PT.map (λ u → inr (q , inr (q' , u))) (LexAt-out P a₁ e₁ e₂ γ h)

outer の型は、最初の比較の鍵で生じる意味論的な分岐をそのまま表します。左側は関係 R を二つの骨格のスロットへ適用した論理式の充足関係であり、右側は等しさs₂ = s₁ と、残る「アリティまたはパラメータ」の選言の充足関係を保ちます。左側を復号すれば Below の符号の場合が得られ、内側の選言の消去には inner を使います。この二段階の読みは ≺At の入れ子に対応し、最終結果を∥ Below ∥₁ に留めるので、どちらの選言も選ばれた枝として外へ出ません。

    outer : ⟨ γ ⊨ appAt R s₁ s₂ ⟩
          ⊎ ( (fst (lookup s₂ γ) ≡ fst (lookup s₁ γ))
            × ⟨ γ ⊨ ( (var a₁ ∈̇ var a₂)
                    ∨̇ ( (var a₂ ≐ var a₁) ∧̇ LexAt P a₁ e₁ e₂ ) ) ⟩ )
          → ∥ Below ∥₁

最後の二つの節で、比較を外向きに読む仕事が完了します。符号の場合には、appAt-adequate が関係の適用についての充足関係を、骨格の二つの符号からなる順序対が R に属すという主張へ変換し、Below の第一の場合を与えます。符号が等しい場合には、内側の対象言語の選言がなお命題的切り詰めの下にあるため、それを消去できる行き先は ∥ Below ∥₁ だけです。したがって三つの比較の鍵のどの場合も読み戻せますが、切り詰めの外で、どの鍵が比較を決めたかを取り出すことはありません。

    outer (inl h) = ∣ inl (subst ⟨_⟩ (appAt-adequate R s₁ s₂ γ) h) ∣₁
    outer (inr (q , h)) = PT.rec squash₁ (inner q) h

二つの最小の名前を比較する記述には、本体の中に六つの新しいスロットが必要です。ここでは最初の三つの添字を定めます。s6a、a6a、e6a はそれぞれ、第一の名前の骨格の符号、アリティの数項、パラメータ環境を指します。六つの束縛子をすべて通過した後では、これらは de Bruijn 添字の第五、第四、第三の位置にあります。位置に名前を付けておけば、後の最小性と比較の論理式を読みやすく保ちながら、束縛位置の計算を一か所に集められます。

private
  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、a6b、e6b は第二、第一、第零の位置を指し、そこに第二の名前のデータが置かれます。この反転は de Bruijn 表現に伴う通常の現象です。証人は s₁,a₁,e₁,s₂,a₂,e₂ の順に束縛されますが、新しい証人はそのたびに環境の先頭へ加えられます。したがって、すべての束縛を加えた環境は e₂ ∷ a₂ ∷ s₂ ∷ e₁ ∷ a₁ ∷ s₁ ∷ γ となり、六つの添字が意図した二つの三つ組を正確に選びます。

  s6b = suc (suc zero)
  a6b = suc zero
  e6b = zero

最小の名前は、すでに s、a、e のスロットを占める名前のデータが満たす性質として表されます。第一の連言は、そのデータが NameAt を満たし、したがって d を表示することを要求します。第二の連言は、競合する骨格の符号、アリティの数項、パラメータ環境を全称量化します。三つの全称量化子は競合する三つ組を第二、第一、第零の位置に置き、sh3 は台、二つの符号集合、表示 d への参照を元のスロットに保ちます。

LeastNameAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Fin n
            → Fin n → Fin n → Fin n → Fin n → Formula S n
LeastNameAt R P B C C₀ s a e d =
  NameAt B C C₀ s a e d
  ∧̇ ∀̇ (∀̇ (∀̇ ( NameAt (sh3 B) (sh3 C) (sh3 C₀)

含意の前件は、同じ d を表示する競合する名前だけに対象を限ります。別の集合を表示する名前は、この最小性には関係しません。後件は ≺At competitor current を否定するので、d のどの競合する名前も、三つの鍵による順序で現在の名前に狭義に先行しません。この論理式は最小性を述べるだけです。名前を探索することも、命題的切り詰めを消去して一つを選ぶこともありません。明示的な最小の名前の構成はメタ言語の命名理論に属し、そこで排中律の仮定を用います。

                      (suc (suc zero)) (suc zero) zero (sh3 d)
             ⇒̇ ¬̇ (≺At (sh3 R) (sh3 P) (suc (suc zero)) (suc zero) zero
                        (sh3 s) (sh3 a) (sh3 e)) )))