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

対話型目次 · 依存グラフ

パラメータ抽象には論理式の定数の有限リストが必要であるが、定数域の等号が判定可能とは仮定できない。そこで本章では重複を残したまま定数の出現を数えて列挙し、その置換変数を既存の自由変数の後ろへ配置する添字計算を整える。

論理式の定数は、出現の順序付きリストをなす。本章はそれらを数えて列挙し、抽象で使う添字計算を与え、リストが空になる境界の場合を扱う。

パラメータの抽象化は、定数に言及する論理式を、より高いアリティの無パラメータ論理式へと組み替え、新しい変数が代わりを務める定数のリストを同時に与える。このリストは有限でなければならないが、定数域の等号が判定可能であるとは仮定できないため、項目を統合したり重複を取り除いたりすることはできない。同じ定数の二つの出現は二つの独立した位置のままであり、後でそれぞれが専用の置換変数を受け取る。仕事は三段階に分かれる。出現を数えること、出現を順に列挙すること、そして新しい変数を既存の自由変数の後ろへ置く添字計算を整えることである。

open import Cubical.Data.Nat using ( snotz )
open import Cubical.Data.Vec using ( _++_ )

具体的には、論理式の定数は出現の順序付きリストとして読み出される。定数は項のどこに現れても、またどの量化子の下に現れても、リストの次の位置を占める。したがって数え上げと列挙は並んで進む。数は出現がいくつあるかを記録する自然数であり、列挙はちょうどその長さのベクトルで、論理式が定数に言及した順にそれらを保持する。重複は解消されずにそのまま残るので、定数同士の比較は一切行われない。章の最後は、出現リストが空である境界の場合である。そこでは論理式が空の定数アルファベットの上で表せることが示される。

出現ごとの数え上げ

countTm と countFo は定数が現れるたびに一つ数え、constantsTm と constantsFo は同じ順序で定数のベクトルを作る。同じ定数の複数回の出現も別々に残す。

本章の設計上の要点は、構文を動かす前にここで決まる。論理式の定数は値ごとではなく出現ごとに数える。定数が k 回現れる論理式は長さ k のベクトルを与え、同じ定数の二つの出現はそのベクトルの二つの項目であり、同じ集合を二度保持する。

論理式が言及する定数の集合を期待する読者は、同じ定数の二つの出現を一つと認めるための判定可能な等号を探すであろうが、見つからない。そもそも存在しないのである。定数域は任意の型であり、その等号が判定可能である必然性はなく、想定する集合の台にも判定可能な等号を仮定しない。出現ごとの数え上げこそが、この章全体をその要求から解放する。代償は、抽象のアリティが厳密に必要なものより高くなること、つまり同じ値を二度受ける変数が現れることであるが、下流でそれを区別するものはない。パラメータのベクトルはパラメータのベクトルである。

数え上げは十個の構成子に対する構造的再帰で、入力は各部分の数である。定数は一回の出現、変数は零回。二つの部分を持つ構成子では数を足し、左の部分が先である。

小さな例が規約を決める。∀̇∈ (con a) ((con a) ∈̇ (var f0)) では、有界量化子が項 con a を伴い、原子の左辺が同じ con a を繰り返し、右辺は変数である。出現は二つであり、どちらも同じ定数なので、数は左から右の読み順で二にならなければならない。まず項を数える。定数 con c は一回の出現、変数 var i は零回であり、項はこの二つの形式しかなく、自由変数の添字は調べない。二つの原子関係はさらにそれぞれの二項の数を足し、左の項を先に書くので、例の合計が読み順に現れる。列挙は [a, a]、つまり同じ定数を二度並べたものを返す。

countTm : ∀ {ℓc} {K : Type ℓc} {n} → Term K n → ℕ
countTm (con c) = 1
countTm (var i) = zero

countFo : ∀ {ℓc} {K : Type ℓc} {n} → Formula K n → ℕ
countFo (t ∈̇ u)  = countTm t + countTm u

命題構成子は、一つ一つ読むよりも役割ごとに分けるのが分かりやすい。枝を組み合わせるもの、すなわち連言・選言・含意はそれぞれ二つの部分論理式の数を足し、やはり左が先である。矛盾記号は項を運ばず、零を寄与する。したがって論理式全体の数は、項を保持する節点ちょうどに対する和であり、二項節点で二つの枝の数が加わるほか、この数は動かない。

countFo (t ≐ u)  = countTm t + countTm u
countFo (φ ∧̇ ψ)  = countFo φ + countFo ψ
countFo (φ ∨̇ ψ)  = countFo φ + countFo ψ
countFo (φ ⇒̇ ψ)  = countFo φ + countFo ψ
countFo ⊥̇        = zero

量化子は項を伴うかどうかで分かれる。非有界の ∃̇ と ∀̇ は変数を束縛するだけで定数を含まないため、本体の数をそのまま通す。束縛は出現を作らない。有界の ∀̇∈ と ∃̇∈ は上の例のように項を一つ伴うので、その数は本体の数の前に countTm t を加えたものである。これにより左から右の読み順が保たれ、後の列挙が項ごとにその順を再現する。

countFo (∃̇ φ)    = countFo φ
countFo (∀̇ φ)    = countFo φ
countFo (∀̇∈ t φ) = countTm t + countFo φ
countFo (∃̇∈ t φ) = countTm t + countFo φ

収集は同じ再帰をもう一度書いたものであり、両方を一度に返す一つの再帰にはできない。返すベクトルの長さこそ最初の再帰が計算するものだからで、収集の返り値の型が付けられるためには、あらかじめ数が存在していなければならない。各節は上の計数の節と対応し、+ の代わりに ++ を使うので、定数は論理式が言及する順序、左から右へ並ぶ。

収集は一つの不変式によって数え上げと結び付いている。ここでの再帰は依存しており、結果の型 Vec K (countTm t) は、返されるベクトルの長さがその項自身の出現数に定義上等しく、項目が左から右の順に並ぶことを要求する。定数は単一項目のベクトル c ∷ [] を、変数は空ベクトルを与え、論理式の場合は二つの項のベクトルを連結する。左の項が先である。

constantsTm : ∀ {ℓc} {K : Type ℓc} {n} (t : Term K n) → Vec K (countTm t)
constantsTm (con c) = c ∷ []
constantsTm (var i) = []

constantsFo : ∀ {ℓc} {K : Type ℓc} {n} (φ : Formula K n) → Vec K (countFo φ)
constantsFo (t ∈̇ u)  = constantsTm t ++ constantsTm u

同じ不変式が命題構成子全体を貫く。二項の論理式は、数え上げが二つの加数を足した節点で正確に二つの部分リストを連結し、矛盾記号は数が零を寄与する場所で空ベクトルを与える。連結が節点ごとに加法を置き換えるため、結果の長さは定義により数に計算され、別途の管理は不要である。

constantsFo (t ≐ u)  = constantsTm t ++ constantsTm u
constantsFo (φ ∧̇ ψ)  = constantsFo φ ++ constantsFo ψ
constantsFo (φ ∨̇ ψ)  = constantsFo φ ++ constantsFo ψ
constantsFo (φ ⇒̇ ψ)  = constantsFo φ ++ constantsFo ψ
constantsFo ⊥̇        = []

量化子の節が再帰を閉じ、順序を確定させる。非有界量化子は本体のリストをそのまま通し、有界量化子は項のリストを本体のリストの前に付ける。これは数え上げがすでに用いた読み順と一致する。上の例では結果は [a, a] で、長さは論理式の数そのものであり、このベクトルこそパラメータ抽象が入力として受け取るものである。

constantsFo (∃̇ φ)    = constantsFo φ
constantsFo (∀̇ φ)    = constantsFo φ
constantsFo (∀̇∈ t φ) = constantsTm t ++ constantsFo φ
constantsFo (∃̇∈ t φ) = constantsTm t ++ constantsFo φ

新しいパラメータ変数の配置

パラメータの抽象化では、アリティ n の環境に定数の出現に対応する k 個の位置を追加する。元の変数は先頭の n 個、パラメータは続く k 個の位置を占める。二つの添字の埋め込みと参照の法則により、連結した環境でも両部分の値が保たれることを示す。

二つの配置関数が添字計算を担い、それぞれ三行である。padRight b は a + b の先頭 a 個の位置の添字を読み、padLeft a は末尾 b 個の位置の添字を読む。両者は互いの鏡像であり、引数の非対称性は再帰の非対称性そのものである。padRight は添字について再帰し、padLeft はまたぐ位置の個数について再帰する。

数値の例で、埋め込みが何をすべきかを示す。a = 2、b = 3 のとき、五つの位置からなる環境は、元の変数を格納する先頭二つと、パラメータを格納する末尾三つに分かれる。padRight は Fin a を Fin (a + b) に埋め込む。連結の先頭 a 個の位置が元の a 個であるため、添字はその場に留まる。前半の添字は五つの位置の中で同じ場所にある。界 b は暗黙で全体を通じて固定されるので、各再帰段階は添字をもう一重の suc で包むだけである。零は零のままで、suc i は suc (padRight b i) になる。

padRight : ∀ {a} b → Fin a → Fin (a + b)
padRight b zero    = zero
padRight b (suc i) = suc (padRight b i)

padLeft : ∀ a {b} → Fin b → Fin (a + b)
padLeft 0    j = j

padLeft は Fin b を Fin (a + b) に埋め込む。添字を先頭の a 個の位置の先へ移すので、ここでは界 a が明示的で、再帰もそれについて回る。例では、padLeft 2 はパラメータの添字 0 を位置 2、すなわち元の変数の直後の最初の位置へ送る。a が零のとき連結は後半そのものであり、j はすでに正しい位置を指す。前の位置が一つ増えるごとに suc が一つ加わり、後半が前半の後ろに置かれる。

padLeft (suc a) j = suc (padLeft a j)

それぞれの配置には一つの法則が付き、それは環境が従う法則そのものである。連結されたベクトルの中で配置済みの添字を参照することは、対応する半分の中で元の添字を参照することに他ならない。これらと並ぶ第三の同じ形の法則は、参照が map を通り抜けるというもので、定数の解釈が出現のベクトルを通り抜けられるのはこの法則による。三つの法則はどれもベクトルと添字への同時の構造的帰納で証明され、各基底場合と各帰納段階は refl または帰納の仮定に帰着する。

心に描く図は、連結 p ++ q と書かれた環境である。p は元の自由変数の値を、q は定数の出現に割り当てられた値を格納する。二つの埋め込みが答えるのは同じ一つの問いである。接合した環境での参照が、接合前に読んでいた値をまだ読み出せるかどうか。前半への添字 i : Fin a を持つ元の変数については、第一の法則は lookup (padRight b i) (p ++ q) ≡ lookup i p と述べる。padRight b i は連結の中で同じ位置を指すので、読まれる項目は変わらない。

lookup-padRight : ∀ {ℓa} {A : Type ℓa} {a b} (p : Vec A a) (q : Vec A b) (i : Fin a)
                → lookup (padRight b i) (p ++ q) ≡ lookup i p
lookup-padRight []      q ()
lookup-padRight (x ∷ p) q zero    = refl
lookup-padRight (x ∷ p) q (suc i) = lookup-padRight p q i

第二の法則は、後半への自然な添字 j : Fin b を持つパラメータを扱う。lookup (padLeft a j) (p ++ q) ≡ lookup j q、すなわち移された添字が読む値は、lookup j q が q の中で読む値にちょうど一致する。二つの法則を合わせると、環境が満たすべきことが述べられる。連結された環境の各半分は、単独であったときの値を保つ、ということである。どちらの証明もベクトルと添字を共にたどり、各段階で一つの項目と一つの構成子を剥がしながら基底の場合まで降りる。

lookup-padLeft : ∀ {ℓa} {A : Type ℓa} a {b} (p : Vec A a) (q : Vec A b) (j : Fin b)
               → lookup (padLeft a j) (p ++ q) ≡ lookup j q
lookup-padLeft 0    []      q j = refl
lookup-padLeft (suc a) (x ∷ p) q j = lookup-padLeft a p q j

lookup-map : ∀ {ℓa ℓb} {A : Type ℓa} {B : Type ℓb} {n}

第三の法則は、名前の付け替えられたベクトルに関するものである。lookup j (map f v) ≡ f (lookup j v)。写像済みのベクトルを読んでから f を施すことは、先に f を施してから読むことと同じである。パラメータ抽象では、この法則によって定数の解釈が出現と共に進む。f が各定数に、その置換変数が取るべき値を割り当て、v が論理式から収集した出現のベクトルなら、map f v の任意の位置を参照することは、その位置の定数に f を施した値を計算する。証明は二つの配置の法則と同じ形で、ベクトルと添字を共に降りていく。

             (f : A → B) (v : Vec A n) (j : Fin n)
           → lookup j (map f v) ≡ f (lookup j v)
lookup-map f []      ()
lookup-map f (x ∷ v) zero    = refl
lookup-map f (x ∷ v) (suc j) = lookup-map f v j

定数が出現しない論理式

数え上げと収集の仕組みは、すべての論理式に有限な出現のデータを添付する。この節はそのインターフェースの境界場合を扱う。個数が零なら論理式のどこにも定数が現れず、したがって含まれる項はすべて変数である。そのような論理式は空の定数アルファベット ⊥* の上で、同じアリティの無パラメータ論理式として表せる。モジュール ZeroOccurrences は元の定数域 K をパラメータとし、まず countFo φ ≡ 0 の証明を和の両側に分けるための算術を整え、次に二つの写像、つまり定数域を消す erase と、K へ写し戻すと元の論理式がちょうど復元されることを示す erase-inv を与える。

出現というインターフェースの境界の問いは、数が零であることは構文に対して何を強制するのか、というものである。この節は、任意の定数型 K に対してこの問いに答える。入力は論理式 φ と、その出現数が零である証明である。答えが K がどの型であるかに依存してはならず、とりわけ K 上の判定可能な等号を用いてはならないので、議論は一度だけ展開され、レベル ℓ のすべてのそのような K に対して一様に成り立つ。

module ZeroOccurrences {ℓ : Level} (K : Type ℓ) where

この節は境界場合を形式化する。入力は論理式 φ と証明 p : countFo φ ≡ 0 の対であり、構成はまず p から各部分項・部分論理式に対してその個数が零である証明を取り出し、その上で空の定数アルファベットの上に同じ構文を組み立て直す。写像 eraseTm と erase は K から ⊥* へ進み、写像 eraseTm-inv と erase-inv は、空型から定数を読み出す消去子 ⊥*-rec に沿って改名すると、元の項や論理式がパスとして返ることを示す。両者を合わせて、K の上では定数が出現しない論理式が無パラメータ論理式の像とちょうど一致し、K に対する判定可能性の仮定が一切不要であることが分かる。

最初の材料は算術的なものである。和が零であるのは、両方の加数が零のときに限る。複合論理式の数は常に部分の数の和なので、countFo φ ≡ 0 の証明は各部分の数が零である証明に分割できなければならず、plus-zero-l と plus-zero-r がまさにこの分割を行い、a + b ≡ 0 からそれぞれ a ≡ 0 と b ≡ 0 を取り出す。分割が機能するのは、非零の左加数が後続数に計算されるからである。suc a + b は suc (a + b) であり、補題 snotz が後続数と 0 の等式を矛盾に変え、そこから任意の結論が従う。左の加数が zero のときは zero + b が b に計算され、両方の主張は直ちに得られる。

plus-zero-l : {a b : ℕ} → a + b ≡ 0 → a ≡ 0
plus-zero-l {0} {b} p = refl
plus-zero-l {suc a} {b} p = ⊥₀-rec (snotz p)

plus-zero-r : {a b : ℕ} → a + b ≡ 0 → b ≡ 0
plus-zero-r {0} {b} p = p

個数が零であることは構文についての定理である。定数の構成子は現れえない、という主張である。項についてはこれは直接に述べられる。項の数が零であるのは、それが変数であるときちょうどであり、eraseTm はこれを一つの写像にする。t と証明 p : countTm t ≡ 0 から、空のアルファベット ⊥* の上の同じアリティ n の項を得る。定数の場合は排除される。countTm (con a) は 1 に計算され、p は suc _ ≡ 0 の証明になるからである。この矛盾が必要な項を供給する。変数の場合は添字をそのまま保ち var i を返す。自由変数は触られず、空のアルファベットが禁じるのは定数だけである。

plus-zero-r {suc a} {b} p = ⊥₀-rec (snotz p)

eraseTm : {n : ℕ} (t : Term K n) → countTm t ≡ 0 → Term (⊥* {ℓ}) n
eraseTm (con a) p = ⊥₀-rec {A = Term (⊥* {ℓ}) _} (snotz p)
eraseTm (var i) _ = var i

erase : {n : ℕ} (φ : Formula K n) → countFo φ ≡ 0 → Formula (⊥* {ℓ}) n

同じ組み立て直しが erase 全体を貫き、原子関係がその最も単純な形で型を示す。t ∈̇ u を取ると、その数は countTm t + countTm u なので、plus-zero-l と plus-zero-r が p を t と u それぞれの数が零である証明に分け、erase は両側で再帰して ⊥* の上に関係を組み立て直す。等号原子 ≐ もまったく同じように扱われる。全体を通して、自由変数のアリティ n は決して触られない。定数を消すのは定数域だけを変え、自由変数の構造は変えないからである。

erase (t ∈̇ u) p = eraseTm t (plus-zero-l p) ∈̇ eraseTm u (plus-zero-r p)
erase (t ≐ u) p = eraseTm t (plus-zero-l p) ≐ eraseTm u (plus-zero-r p)
erase (φ ∧̇ ψ) p = erase φ (plus-zero-l p) ∧̇ erase ψ (plus-zero-r p)
erase (φ ∨̇ ψ) p = erase φ (plus-zero-l p) ∨̇ erase ψ (plus-zero-r p)
erase (φ ⇒̇ ψ) p = erase φ (plus-zero-l p) ⇒̇ erase ψ (plus-zero-r p)

量化子の一つの場合が、束縛と数の相互作用を示す。∃̇ φ のような非有界量化子では、全体の数は本体の数に等しいので、同じ p をそのまま再帰呼び出しに持ち込み、結果は消去後の本体に ∃̇ を施したものである。矛盾記号は部分も出現もないので、消去しても自分自身である。有界量化子 ∀̇∈ と ∃̇∈ は項と論理式を組み合わせるので、ここでは原子の場合と同じように和を分ける。項は eraseTm を、本体は再帰的な erase を通る。どの節も元の論理式の形を保ち、定数だけを置き換える。

erase ⊥̇ _ = ⊥̇
erase (∃̇ φ) p = ∃̇ erase φ p
erase (∀̇ φ) p = ∀̇ erase φ p
erase (∀̇∈ t φ) p = ∀̇∈ (eraseTm t (plus-zero-l p)) (erase φ (plus-zero-r p))
erase (∃̇∈ t φ) p = ∃̇∈ (eraseTm t (plus-zero-l p)) (erase φ (plus-zero-r p))

この構成を単なる翻訳以上のものにするのは往復である。K へ写し戻せば元の論理式が返らなければならない。まず項レベルの主張 eraseTm-inv である。t の数が零なら、⊥*-rec に沿って eraseTm t p の名前を替えると、K 上の項の間のパスとして t 自身が返る。名前替えの関数 ⊥*-rec : ⊥* → K は空の型の消去子であり、K の定数を一つ作るよう求められると ⊥* の元を要求する。しかし eraseTm が組み立てた項には定数の節点が含まれないので、この関数が実際に適用されることはない。したがって帰納には矛盾の場合と変数の場合しか残らず、後者は mapTm の計算規則、すなわち var i から var i を再構成する規則で閉じる。

eraseTm-inv : {n : ℕ} (t : Term K n) (p : countTm t ≡ 0)
            → mapTm ⊥*-rec (eraseTm t p) ≡ t
eraseTm-inv (con a) p = ⊥₀-rec (snotz p)
eraseTm-inv (var i) _ = refl

erase-inv : {n : ℕ} (φ : Formula K n) (p : countFo φ ≡ 0)

論理式レベルでは、往復則 erase-inv は構文木についての構造的帰納によって証明され、項レベルの逆を再帰的に組み合わせる。二つの原子関係が、二つの部分を持つ基底の場合を示す。mapFo が名前替えを消去された二つの項へ分配するので、ゴールは同じ構成子の二つの応用の間のパスであり、cong₂ が項レベルの二つのパス eraseTm-inv t _ と eraseTm-inv u _ をそのパスへ引き上げる。部分項の数が零である証明は、erase 自身とまったく同様に、p に plus-zero-l と plus-zero-r を施して得られる。

          → mapFo ⊥*-rec (erase φ p) ≡ φ
erase-inv (t ∈̇ u) p =
  cong₂ _∈̇_ (eraseTm-inv t (plus-zero-l p)) (eraseTm-inv u (plus-zero-r p))
erase-inv (t ≐ u) p =
  cong₂ _≐_ (eraseTm-inv t (plus-zero-l p)) (eraseTm-inv u (plus-zero-r p))

erase がすべての節点で論理式の形を保つため、各節点で使える帰納の仮定は、そこで往復則が必要とする形をすでにちょうど持っている。三つの二項結合子は二部分の型を繰り返す。∧̇、∨̇、⇒̇ のいずれでも、全体の数は二つの部分論理式の間で分かれ、cong₂ が一対の帰納の仮定を再構成された結合子の間のパスへ引き上げる。この一様さは偶然ではなく構造的なものである。往復則は構文木の性質であり、一節点ずつ検査されるからである。

erase-inv (φ ∧̇ ψ) p =
  cong₂ _∧̇_ (erase-inv φ (plus-zero-l p)) (erase-inv ψ (plus-zero-r p))
erase-inv (φ ∨̇ ψ) p =
  cong₂ _∨̇_ (erase-inv φ (plus-zero-l p)) (erase-inv ψ (plus-zero-r p))
erase-inv (φ ⇒̇ ψ) p =

部分を一つだけ持つ節点はそれに応じて軽くなる。矛盾記号は refl だけで足りる。両辺とも構成子 ⊥̇ 自身に簡約されるからである。二つの非有界量化子は部分論理式を一つしか持たないため、cong₂ ではなく cong を用いる。mapFo の計算規則が展開された後、ゴールは ∃̇_ の下のパスであり、cong ∃̇_ (erase-inv φ p) が与えるのはまさにそれである。同じ p がそのまま渡される。

  cong₂ _⇒̇_ (erase-inv φ (plus-zero-l p)) (erase-inv ψ (plus-zero-r p))
erase-inv ⊥̇ _ = refl
erase-inv (∃̇ φ) p = cong ∃̇_ (erase-inv φ p)
erase-inv (∀̇ φ) p = cong ∀̇_ (erase-inv φ p)
erase-inv (∀̇∈ t φ) p =

有界量化子がこの帰納を閉じる。原子と同じく項と論理式を混ぜる。cong₂ が、項レベルのパス eraseTm-inv t (plus-zero-l p) と論理式レベルのパス erase-inv φ (plus-zero-r p) の対を引き上げる。この節で定理は完成である。個数が零のすべての論理式は、消去された無パラメータ形の、パスの差を除けば正確な像である。これで出現というインターフェースの境界の場合が完全に説明された。K の上では、定数を含まない論理式は無パラメータ論理式とちょうど一致し、どこにも判定可能性の仮定は要らない。

  cong₂ ∀̇∈ (eraseTm-inv t (plus-zero-l p)) (erase-inv φ (plus-zero-r p))
erase-inv (∃̇∈ t φ) p =
  cong₂ ∃̇∈ (eraseTm-inv t (plus-zero-l p)) (erase-inv φ (plus-zero-r p))

まとめ

出現は、論理式の定数に対して、定数域の二つの記号が等しいかを問わない有限のインターフェースを与える。個数 countFo は出現の列挙の添字であると同時に、後のパラメータ抽象の添字でもある。そこでは出現ごとに専用の置換変数が割り当てられ、配置とその参照法則が連結環境に対する添字計算を補う。個数が零のとき、ZeroOccurrences はその論理式が無パラメータ論理式の正確な像であることを示し、構文を何も失わずに空の定数域を採用できるのである。