Bedrock閉じた論理式符号の定義域を記述する
この章を読むか、読書案内と依存マップで別のルートを選べます。
読書案内 · 依存マップAgda にはすでに論理式の帰納型と、集合をその符号として外部で割り当てる演算があります。しかし集合論の内部で構文を扱うには、論理式キーの候補集合をモデル自身の言語で記述する論理式が必要です。本章では、その有界な記述を構成します。形の半分は候補領域にすでにあるキーの直下の構造を読み、閉性の半分は正当な構成要素から複合キーを生成します。
{-# OPTIONS --cubical --safe --guardedness #-}
この記述は構成的です。記録するのは有界な所属、対、タグ、および論理式キーの直下の構成要素だけなので、排中律の仮定は必要ありません。
open import Base.Prelude
宇宙レベルを一つ固定します。以下の主なパラメータは、候補符号領域 C、定数を与える作業集合 w、環境の塔の項目を収めるものとして用いる集合 E、そして十個の構成子タグを指す名前付きの位置 N です。意図した E の項目はアリティと対応する環境集合の対ですが、ここで定義する論理式だけでは E が正準な塔であるとは主張しません。その事実は後の妥当性証明の仮定から与えられます。
module L.Coding.CodeDomain {ℓ : Level} where
目標は、所属、等号、結合子、有界量化子からなる対象言語の論理式です。量化子は、記述の中ですでに名付けられた集合か、対を分解するための小さな容器だけを動きます。この統語上の制限により、最後の論理式を Δ₀ と認定できます。
open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; var; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇∈; ∀̇∈ ) open import FOL.LevyHierarchy using ( checkΔ₀; Δ₀ )
すべての論理式は構成可能な台の上で解釈されます。順序対の述語と符号化されたグラフの適用述語により、集合で符号化した対に原始的な射影を仮定せず、内部言語から「アリティとタグ付きペイロードの対」というキーを調べられます。
import FOL.Absoluteness open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans ) open import L.Coding.Model {ℓ} using ( prAtL; appAt ) open import L.Coding.Expressions {ℓ} using ( sucAtL )
入れ子の有界量化子は、環境の先頭に一時的な証人を加えます。名前付きの有限スロットとそのずらしによって、それらの証人を分解している間も、C、w、アリティ、十個すべてのタグが同じ値を指し続けます。
import L.Coding.Expressions {ℓ} as CodingExpressions module E = CodingExpressions.PairExpression open import L.Coding.Quantification {ℓ} using ( i0; i1; i2; i3; i4; i5; i6; i7; i8; sh ; f0; f1; f2; f3; f4; f5; f6; f7; f8; f9
対の読みは、すべての証人を有界に保ったまま二つの成分を取り出します。その後、有限選言が十通りの最外側の構成子を一つの形の検査にまとめ、対応する有界全称の読みがすべての正当な入力について閉性を表します。
; sndEx; sndAll; bothEx; bothAll; bigOr )
有限添字と集合論的な数項は、ここでは異なる役割をもちます。写像 N は周囲の環境にある十個の位置を指し、toℕ は各タグ位置に 0 から 9 までのどの数項を置くかを定めます。有界な証人で環境が拡張されても、位置をずらすことでこれらの参照は保たれます。この段階では、E の項目に記録されたアリティが自然数の数項であるとはまだ認定されません。その同定は、後の環境の塔に関する仮定から得られます。
open import Cubical.Data.Nat using ( _+_ ) open import Cubical.Data.FinData using ( toℕ ) open import Cubical.Data.Unit using ( tt ) open import Cubical.Data.Vec using ( lookup ) open import Cubical.HITs.CumulativeHierarchy.Constructions
十個の構成子タグは、0 から 9 までのフォン・ノイマン数項で表されます。数項の違いによって、後で二つの原子関係、三つの二項結合子、偽、四つの量化子を区別します。
using ( module InfinitySet ) open InfinitySet {ℓ} using ( #_ )
構成可能集合の台を S と書きます。対象言語の論理式を解釈するとき、候補領域、そのキー、作業集合、環境の塔の要素は、すべてこの同じ台の要素です。
open hPropStructure 𝒮ʟ using ( S )
したがって、以下で作る論理式は、構成可能な要素からなる有限環境で読めます。まず最も局所的な問いから始めます。固定したアリティで、どのタグ付き集合を項の符号として認めるのでしょうか。
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _^_; _⊨ᵐ_ ) open AbsL using ( _^_ )
形と閉性の記述
項の述語は二種類の表示を受け入れます。スロット N0 のタグをもちペイロードが作業集合 w に属する対と、スロット N1 のタグをもちペイロードがアリティ集合 ar に属する対です。意図したタグの割当てのもとで、それぞれ定数と自由変数を表します。この段階の ar はまだ単なる集合であり、自然数の数項と同定するには後で使う環境の塔の事実が必要です。
isTm : ∀ {m} → Fin m → Fin m → Fin m → Fin m → Fin m → Formula S m isTm t ar w N0 N1 = sndEx t N0 (var i0 ∈̇ var (sh 2 w)) ∨̇ sndEx t N1 (var i0 ∈̇ var (sh 2 ar))
固定したペイロード r に対し、keyUp C ar r は完全なキー (ar + 1, r) が C に属することを述べます。ここで ar + 1 は内部の関係で表現されます。量化子の形の節は、本体についてこの述語を使います。この述語だけでは r の形を検査せず、ar が数項であることも証明しません。
keyUp : ∀ {m} → Fin m → Fin m → Fin m → Formula S m keyUp C ar r = ∃̇∈ (var C) (∃̇∈ (var i0) (∃̇∈ (var i0) (prAtL i2 i0 (sh 3 r) ∧̇ sucAtL (sh 3 ar) i0)))
論理式キーは一様に (ar, (N, p)) という形をもちます。ar はアリティ、N は構成子タグ、p はペイロードです。まず内側のタグ付きペイロード (N, p) を作り、次にそれをアリティと対にします。構成子ごとに変わるのは p の構造であり、この外側の配置は共通です。
keyExpr : ∀ {m} → Fin m → Fin m → E.Expr m → E.Expr m keyExpr ar N p = E.pair (E.slot ar) (E.pair (E.slot N) p)
どちらの原子関係でも、ペイロードは ((Nx, x), (Ny, y)) という形です。各内側の対は項の種類とそのペイロードをともに記録するので、左右の項はそれぞれ独立に定数または変数となりながら、原子論理式は一様なキーの形を保てます。
atomKeyExpr : ∀ {m} → Fin m → Fin m → Fin m → Fin m → Fin m → Fin m → E.Expr m atomKeyExpr ar N Nx x Ny y = keyExpr ar N (E.pair (E.pair (E.slot Nx) (E.slot x)) (E.pair (E.slot Ny) (E.slot y)))
有界量化子のペイロードは、タグ付きの上界項 (Nx, x) と本体のペイロード a を対にします。外側のキーが現在のアリティを記録し、別の keyUp 条件が、本体の完全なキー (アリティ + 1, a) が領域に属することを要求します。
bndKeyExpr : ∀ {m} → Fin m → Fin m → Fin m → Fin m → Fin m → E.Expr m bndKeyExpr ar N Nx x a = keyExpr ar N (E.pair (E.pair (E.slot Nx) (E.slot x)) (E.slot a))
最初の所属テンプレートは、入れ子の対 (ar, (N, a)) が候補領域に属することを述べます。ここで記録するのは集合への所属だけです。N が適切な一項構成子のタグであることや、a が正当な構成要素であることは、外側の節が別に課します。
unKey : ∀ {m} → Fin m → Fin m → Fin m → Fin m → Formula S m unKey C ar N a = E.member (keyExpr ar N (E.slot a)) (var C)
二項テンプレートは、一項のペイロードを対 (a, b) に置き換えます。後の節では、同じアリティの二つの部分キーが C に属することを別に要求したうえで、このテンプレートを論理積、論理和、含意に使います。
binKey : ∀ {m} → Fin m → Fin m → Fin m → Fin m → Fin m → Formula S m binKey C ar N a b = E.member (keyExpr ar N (E.pair (E.slot a) (E.slot b))) (var C)
原子テンプレートは、二つのタグ付き項ペイロードをキーに入れます。ここでも主張するのは C への所属だけです。原子の形と閉性の節が項の境界を与え、最外側の関係にタグ 0 または 1 を選びます。
atomKey : ∀ {m} → Fin m → Fin m → Fin m → Fin m → Fin m → Fin m → Fin m → Formula S m atomKey C ar N Nx x Ny y = E.member (atomKeyExpr ar N Nx x Ny y) (var C)
有界量化子は、本体に加えて境界を表す項も運ぶ点で非有界量化子と異なります。ペイロード ((Nx, x), a) はタグ付きの境界項と本体のペイロードを記録しますが、この所属テンプレートだけでは両者の正当性を主張しません。外側の形の条件が、項を現在のアリティで、本体の完全なキーを後続アリティで検査します。閉性の条件は、同じ二つの構成要素を生成する向きに用います。
bndKey : ∀ {m} → Fin m → Fin m → Fin m → Fin m → Fin m → Fin m → Formula S m bndKey C ar N Nx x a = E.member (bndKeyExpr ar N Nx x a) (var C)
タグの一致は、十の枠がちょうど数項の 0 から 9 を運ぶことを要求します。それぞれの枠がその位置に対応します。これにより、後のどの論理式も「所属のアトムのタグ」と言えば、常に同じ枠を指します。
Tags : ∀ {m} (γ : S ^ m) (N : Fin 10 → Fin m) → Type (ℓ-suc ℓ) Tags γ N = (k : Fin 10) → fst (lookup (N k) γ) ≡ # (toℕ k)
論理式を、束縛変数が加わった環境のもとで読むときは、十のタグの枠も環境とともにずれます。ずらされた名前付けによって、すべての節が同じタグと整列し続けます。
shN : ∀ {m} (j : ℕ) → (Fin 10 → Fin m) → Fin 10 → Fin (j + m) shN j N k = sh j (N k)
ここで、候補領域の要素を内向きに読む問いを立てられます。そのペイロードが許された構成子形の一つであることを、どのような証拠が示すのでしょうか。構成子タグは十個ありますが、必要なペイロード条件は五種類だけです。二つの原子関係、三つの二項結合子、二つの非有界量化子、二つの有界量化子が、それぞれ同じ構成要素の形を共有するからです。
module Shape {m : ℕ} (C w : Fin m) (N : Fin 10 → Fin m) where private C9 w9 : Fin (9 + m) C9 = sh 9 C w9 = sh 9 w
五つのペイロードの形が書き出されます。アトムのペイロードは二つの正当な項を要求し、二項のペイロードは、すでに定義域にある同じアリティの二つの部分キーを要求します。偽のペイロードは数項ゼロであり、非有界の量化子のペイロードは後続のアリティでの本体のキーを要求します。
atomPay binPay conPay quPay bqPay : Formula S (9 + m) atomPay = bothEx i0 (isTm i1 i8 (sh 12 w) (sh 12 (N f0)) (sh 12 (N f1)) ∧̇ isTm i0 i8 (sh 12 w) (sh 12 (N f0)) (sh 12 (N f1))) binPay = bothEx i0 (appAt (sh 12 C) i8 i1 ∧̇ appAt (sh 12 C) i8 i0) conPay = var i0 ≐ var (sh 9 (N f0)) quPay = keyUp C9 i5 i0
有界量化子のペイロードには、現在のアリティで正当な上界項と、アリティを一つ増やした位置で完全なキーが領域に属する本体ペイロードが入ります。連言はこの二つの条件をともに記録しますが、復号された本体論理式を選び出すものではありません。
bqPay = bothEx i0 (isTm i1 i8 (sh 12 w) (sh 12 (N f0)) (sh 12 (N f1)) ∧̇ keyUp (sh 12 C) i8 i0)
最初の四つのタグは、二つの原子関係と最初の二つの二項結合子を区別します。タグ 0 は所属、タグ 1 は等号、タグ 2 は論理積、タグ 3 は論理和です。最初の二つは同じ原子ペイロード条件を使い、次の二つは同じ二項ペイロード条件を使いますが、数項の違いによって最外側の構成子は区別されたままです。
payN : ℕ → Formula S (9 + m) payN 0 = atomPay payN 1 = atomPay payN 2 = binPay payN 3 = binPay
タグ 4 は含意、タグ 5 は偽、タグ 6 と 7 はそれぞれ非有界存在量化子と非有界全称量化子、タグ 8 は有界全称量化子です。対応するペイロード条件は順に、同じアリティの二つの部分キー、固定された数項 0、後続アリティにある本体キー、そして現在のアリティにある境界項とそのような本体の組です。
payN 4 = binPay payN 5 = conPay payN 6 = quPay payN 7 = quPay payN 8 = bqPay
タグ 9 は有界存在量化子で、タグ 8 と同じ有界量化子のペイロード条件を使います。最後の等式は 9 より大きい入力で偽を返し、payN を自然数上の全域関数にします。pay は Fin 10 の添字を通してしかこれを呼ばないので、この予備の分岐は十通りの形の検査では到達しません。
payN 9 = bqPay payN (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc _)))))))))) = ⊥̇
これで十個のタグのそれぞれにペイロードの検査が対応しました。次は、k で添字づけられた検査を実際のタグ付きペイロードと結び、その十通りの選択肢を形の条件へまとめます。
pay : Fin 10 → Formula S (9 + m) pay k = payN (toℕ k)
選んだ構成子添字 k に対し、外側のペイロードは (N k, r) と分解され、残りの成分 r はそのタグのペイロード条件を満たさなければなりません。アリティは外側の形の論理式ですでに取り出されています。この節が分解するのはタグ付きペイロードであり、アリティの要素を量化するのではありません。
at : Fin 10 → Formula S (7 + m) at k = sndEx i0 (sh 7 (N k)) (pay k)
十個の形の節は、一つの有限選言にまとめられます。したがって、一つの論理式だけで、タグ付きペイロードが十種類の構成子形の少なくとも一つに合うことを述べられ、追加の非有界量化子は導入されません。
ten : Formula S (7 + m) ten = bigOr 9 at
形の半分は、候補領域の既存要素 c ごとに出発します。E から要素 (ar, F) を取り、c を (ar, p) と分解し、p が十通りのタグ付きペイロード形のいずれかに合うことを要求します。複合形では、直下の論理式部分キーがすでに C に属することも要求されます。意味論では、これらの有界存在の証人は命題的切り詰めのもとにあるため、この条件は選ばれた分解を与えず、復号の一意性も主張しません。
shapeAt : ∀ {m} → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m shapeAt C w E N = ∀̇∈ (var C) (∃̇∈ (var (sh 1 E)) (bothEx i0 (sndEx i4 i1 (Shape.ten C w N))))
後半では、外向きの問いへ移ります。E の項目を一つ固定し、その第一成分を共通のアリティとして使います。閉性の各節は、項がそのアリティで正当であり、直下の論理式キーが必要な現在または後続のアリティですでに C に属するとき、どの複合キーが C に入らなければならないかを述べます。
module Close {m : ℕ} (C w : Fin m) (N : Fin 10 → Fin m) where private C4 w4 : Fin (4 + m) C4 = sh 4 C w4 = sh 4 w
原子の生成節は、最外側の関係タグと二つの項それぞれのタグを固定します。二つのペイロードを対応する境界 X と Y の中で動かし、得られる原子キーを C に入れます。後の八つの具体例では、各項のタグを定数または変数から選び、それに応じて X と Y を作業集合または現在のアリティにします。
atomClose : (k Nx Ny : Fin 10) (X : Fin (4 + m)) (Y : Fin (5 + m)) → Formula S (4 + m) atomClose k Nx Ny X Y = ∀̇∈ (var X) (∀̇∈ (var Y) (atomKey (sh 6 C) i3 (sh 6 (N k)) (sh 6 (N Nx)) i1 (sh 6 (N Ny)) i0))
二項の閉性は、定義域の同じアリティの任意の二つの要素が、それらを部分キーとする各二項の結合子のキーを生成することを要求します。
binClose : (k : Fin 10) → Formula S (4 + m) binClose k = ∀̇∈ (var C4) (sndAll i0 i2 (∀̇∈ (var (sh 7 C)) (sndAll i0 i5 (binKey (sh 10 C) i7 (sh 10 (N k)) i3 i0))))
偽の閉性は、ゼロのペイロードをもつ偽の記号のキーを、定義域の中に置きます。
conClose : (k : Fin 10) → Formula S (4 + m) conClose k = unKey C4 i1 (sh 4 (N k)) (sh 4 (N f0))
非有界量化子について、C の任意の要素がアリティ ar + 1 の本体キーとして分解されるとします。この節は、対応する量化されたキーがアリティ ar で C に属することを要求します。これは既存の直下の構成要素から複合論理式へ進む生成方向です。
quClose : (k : Fin 10) → Formula S (4 + m) quClose k = ∀̇∈ (var C4) (bothAll i0 (sucAtL i5 i1 ⇒̇ unKey (sh 8 C) i5 (sh 8 (N k)) i0))
有界量化子の節は、現在のアリティに上界項を加えます。C の要素がアリティ ar + 1 の本体キーと認められると、選んだ項の境界 X の各ペイロードから、アリティ ar の有界量化子キーが生成されます。後の具体例が定数と変数の場合を分けて選びます。
bqClose : (k Nx : Fin 10) (X : Fin (8 + m)) → Formula S (4 + m) bqClose k Nx X = ∀̇∈ (var C4) (bothAll i0 (sucAtL i5 i1 ⇒̇ ∀̇∈ (var X) (bndKey (sh 9 C) i6 (sh 9 (N k)) (sh 9 (N Nx)) i0 i1)))
閉性の連言は、八つのアトムの節から始まります。二つのアトムの記号がそれぞれ二つの項の枠をもち、各枠が定数か変数のどちらかを取るので、八通りの組み合わせになります。
all : Formula S (4 + m) all = atomClose f0 f0 f0 w4 (sh 1 w4) ∧̇ (atomClose f0 f0 f1 w4 i2 ∧̇ (atomClose f0 f1 f0 i1 (sh 1 w4) ∧̇ (atomClose f0 f1 f1 i1 i2 ∧̇ (atomClose f1 f0 f0 w4 (sh 1 w4) ∧̇ (atomClose f1 f0 f1 w4 i2
この連言は最後の二つの原子節から続き、等号原子について四通りの項の形を完成させます。その後に、三つの二項節、一つの偽の節、二つの非有界量化子の節、四つの有界量化子の節を加えます。したがって内訳は、原子が八、二項が三、偽が一、非有界が二、有界が四で、合計十八節です。
∧̇ (atomClose f1 f1 f0 i1 (sh 1 w4) ∧̇ (atomClose f1 f1 f1 i1 i2 ∧̇ (binClose f2 ∧̇ (binClose f3 ∧̇ (binClose f4 ∧̇ (conClose f5 ∧̇ (quClose f6 ∧̇ (quClose f7 ∧̇ (bqClose f8 f0 (sh 8 w) ∧̇ (bqClose f8 f1 i5 ∧̇ (bqClose f9 f0 (sh 8 w) ∧̇ bqClose f9 f1 i5))))))))))))))))
閉性の半分は、E が指す集合の各項目で十八の生成節すべてを課します。項目を分解すると、その第一成分が各構成規則に共通のアリティを与えます。この論理式だけでは、それらの項目が正準な環境の塔をなすことも、記録された各アリティが自然数の数項であることも認定しません。それらの事実は後の仮定から与えられます。正しい塔の項目では、向きは常に正当な構成要素から対応する複合キーへ進み、C の任意の要素からその部分へ戻る向きではありません。
closeAt : ∀ {m} → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m closeAt C w E N = ∀̇∈ (var E) (bothAll i0 (Close.all C w N))
記述全体は二つの方向を連言します。shapeAt は既存の各要素を内向きに読み、その直下の部分キーが候補領域に残ることを要求します。closeAt は正当な構成要素から出発し、対応する複合キーを生成します。どちらか一方だけでは足りません。形だけでは真正なキーを欠くことがあり、閉性だけでは余分な要素を許すことがあります。この連言はなお w、E、N に相対的な仕様にすぎず、それ自体で領域を構成したり、正準な領域との一致を証明したりはしません。
codesAt : ∀ {m} → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m codesAt C w E N = shapeAt C w E N ∧̇ closeAt C w E N
最後の計算は、codesAt のすべての量化子が有界であるという証明を与えるので、codesAt は Δ₀ クラスに属します。これは候補領域を記述する対象言語の論理式についての分類です。個々の符号を Δ₀ の対象として分類するものではなく、記述された領域の存在、正準性、絶対性の定理をそれだけで証明するものでもありません。
Δ₀-codesAt : ∀ {m} (C w E : Fin m) (N : Fin 10 → Fin m) → Δ₀ (codesAt C w E N) Δ₀-codesAt C w E N = checkΔ₀ (codesAt C w E N) tt
まとめ
候補符号領域の仕様には、相補的な二つの向きがあります。shapeAt は既存の各要素を十種類のタグ付き構成子形の一つとして読み、その形が必要とする直下の論理式キーがすべて C に属することを要求します。closeAt は十八の生成節をまとめ、正当な項と、現在または後続のアリティにある既存の部分キーから、対応する論理式キーを構成します。両者の連言は、w、E、N に相対的な有界仕様です。
有界存在量化子が隠す意味論的な証人は命題的切り詰めのもとでしか得られないため、この仕様は分解も復号関数も選びません。次章では、正しいアルファベット、タグ、環境の塔に関する仮定と排中律のもとで、二つの妥当性の議論を別々に行います。候補領域の各要素は真正な論理式キーへ単に復号でき、外部の論理式に関する帰納法はすべての真正なキーを候補領域へ入れます。その後、外部符号化の単射性から、固定した一つのアリティで復元された二つの論理式が一致することは示せますが、この別の結果によって codesAt が選択された、または大域的に一意な構文復号器になるわけではありません。