この章を読むか、対話型目次と依存グラフで別のルートを選べます。

対話型目次 · 依存グラフ

この章のすべては、ただ一度だけ固定され章全体を通じて用いられる単一の型論的宇宙レベル ℓ の上で行われる。このレベルの集合の階層 V ℓ が最終的な符号化の目標であり、一階言語はパラメータが置かれる舞台である。方針は一様である。構成可能集合 W が与えられれば、その要素を定数記号として読み、抽象的なインデックスで名前を付け、各名前を V ℓ の中でそれが指す集合へ輸送する。この方針はどの W を選ぶかに依存しないので、任意の W に対して通用する。

module L.Coding.CodeAlphabet {ℓ : Level} where

構成可能集合 W についての主張は、しばしば W の要素に言及する。たとえば W に属するある x が性質を満たすと言うには、論理式は x をパラメータとして伴わなければならない。集合論の内部では、このようなパラメータは一階言語の定数記号として現れる。しかし周囲の構文符号化は、定数が任意の集合の要素への抽象的な参照ではなく、階層 V ℓ の集合であることを要求する。そこで橋渡しが必要になる。アルファベットが W の要素を索引づけ、各インデックスに集合としての指示対象を与える埋め込みをそろえた言語である。

この章では、固定された W に対しその橋を構築する。アルファベットは W の台集合の要素へのインデックスの型であり、埋め込みは各インデックスをそれが指す集合へ送り、その集合が W に属することの証拠を添える。埋め込みに沿って各定数を書き換えれば、アルファベット上のすべての項と論理式は集合を定数とする構文になり、既存の V 値の符号化が適用できて、項の符号 ct と論理式の符号 cd が得られる。符号化はアリティを調べないので、アリティの相等の経路に沿って論理式を輸送しても符号は変わらず、これが cd-subst の記録する事実である。

open import Cubical.Foundations.Prelude using ( J; substRefl )

対象言語の構文はアルファベットに対して汎用である。定数の型 K とアリティ n に対する論理式の型 Formula K n は、定数が何であるかを決して調べず、それらを論理構造へ配置するだけである。したがって、アルファベット上の任意の関数は構文の書き換えへ拡張される。各定数をその関数を通して写せば、すべての出現が書き換えられ、論理結合子・量化子・変数はそのまま保たれる。ここで使う関数は要素のインデックスを V ℓ へ埋め込む写像であり、書き換え後の論理式は集合を定数とするので、階層上の集合値の構文符号化が要求する入力の形式にちょうど合う。残るのは、これらの定数が実際に W の要素になるようにアルファベットと埋め込みを選ぶことである。

二つの区別が構成を組織する。第一に、階層の集合の要素は ⟪ a ⟫ の抽象的なインデックス q によって提示され、埋め込み ⟪ a ⟫↪ はそのインデックスを指された集合へ送る。インデックスは名前であり、値 ⟪ a ⟫↪ q は V ℓ における指示対象であり、この二つの役割は終始区別される。第二に、W は任意の集合ではなく、構成可能な構造の台 S の要素なので、階層における台集合 W .fst と構成可能性の証拠を伴う。まさにこのおかげで、その要素を構成可能集合についての言語のパラメータとして読むことができる。アルファベットは ⟪ W .fst ⟫ そのものにとられ、次の節でこれらの部品が符号 ct と cd へと組み上げられる。

open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Properties using
  ( ∈∈ₛ; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_ )

open hPropView 𝒮ʟ using ( S )

定数を埋め込んで構文を符号化する

この節では、構成可能集合 W を台 S の要素として取り、W 上の構文をどのように集合へ符号化するかを考える。構成は三段階の合成である。まず利用可能な定数記号の型 Ab を取り出し、次に各記号を階層 V ℓ へ埋め込み、それが実際に W に属することの証拠を添え、最後に書き換え後の項と論理式に集合値の符号化を施す。最後の補題は、論理式がアリティで索引づけられることに由来する簿記上の問題を片づける。

要素 W : S は、階層のある集合を構造のデータとともに束ねたものである。W .fst がその台集合になる。したがって Ab は ⟪ W .fst ⟫、つまりその集合の要素へのインデックスの型であり、ι は埋め込み ⟪ W .fst ⟫↪ で、各インデックスを V ℓ 内の指された要素へ送る。つまり Ab の要素こそが利用可能な定数記号であり、ι は集合としてのその指示対象を計算する。

module Alphabet (W : S) where

Ab : Type ℓ
Ab = ⟪ W .fst ⟫

ι : Ab → V ℓ
ι = ⟪ W .fst ⟫↪

所属の証拠 ι∈ は、各定数記号 q に対して集合 ι q が実際に W .fst の要素であることを述べる。これは、所属関係と分類つきの所属関係 ∈ₛ との間のライブラリの同値からそのまま読み取れる。アルファベットが整うと、cd と ct はほとんど自動的に決まる。mapFo ι と mapTm ι が各定数 con q を con (ι q) に置き換えて論理式や項を書き換え、階層符号化の括弧 ⌜_⌝ と ⌜_⌝ᵗ がその結果を集合としてまとめるのである。書き換えの後も論理式の論理的な骨格はそのまま保たれるので、既存の符号化をそのまま再利用できる。

ι∈ : (q : Ab) → ⟨ ι q ∈ W .fst ⟩
ι∈ q = ∈∈ₛ {a = ι q} {b = W .fst} .snd (∈ₛ⟪ W .fst ⟫↪ q)

cd : ∀ {n} → Formula Ab n → V ℓ
cd ψ = VCode.⌜ mapFo ι ψ ⌝

ct : ∀ {n} → Term Ab n → V ℓ

型 Formula Ab n の論理式はアリティ n を伴い、依存型理論ではこのインデックスが型の一部である。後の証明で n と n' の相等が必要になると、経路 e : n ≡ n' に沿って論理式を輸送する。輸送された論理式は、元の論理式が同じでも、構文の上では別の要素である。補題 cd-subst は、これが符号化には何の影響も与えないことを示す。輸送後の論理式に適用した cd は、元の論理式に適用した cd と等しいのである。証明は e に対する J によるもので、反射的な場合は refl に沿った輸送が恒等写像であり、substRefl がこの簡約を明示するため成立し、残りは cong cd で二つの適用を結ぶ。

ct t = VCode.⌜ mapTm ι t ⌝ᵗ

cd-subst : ∀ {n n'} (e : n ≡ n') (ψ : Formula Ab n) → cd (subst (Formula Ab) e ψ) ≡ cd ψ
cd-subst {n} e ψ = J (λ n' e' → cd (subst (Formula Ab) e' ψ) ≡ cd ψ)
  (cong cd (substRefl {B = Formula Ab} ψ)) e

まとめ

Alphabet W は構成可能集合 W の要素を一階言語の定数記号とみなし、それぞれを証拠 ι∈ とともに周囲の階層へ埋め込み、ct と cd によって項と論理式の集合としての符号を与える。符号化がアリティを決して調べないため、cd-subst は、アリティの相等の経路に沿って論理式を輸送してもその符号が変わらないことを保証する。