出現ごとに扱う定数

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

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

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

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

module FOL.Manipulation.ConstantOccurrences where

open import Base.Prelude
open import FOL.Syntax using
  ( Term; con; var; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )

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

open import FOL.Manipulation.ConstantMapping using ( mapTm; mapFo )
open import Cubical.Data.Nat using ( _+_; snotz )
open import Cubical.Data.Vec using ( _++_; map )
import Cubical.Data.Empty as Empty

出現ごとの数え上げ

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) = suc zero
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 zero    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 zero    []      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 は、空型から定数を読み出す消去子 Empty.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 ≡  → a ≡ 
  plus-zero-l {zero} {b} p = refl
  plus-zero-l {suc a} {b} p = Empty.rec (snotz p)

  plus-zero-r : {a b : ℕ} → a + b ≡  → b ≡ 
  plus-zero-r {zero} {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 = Empty.rec (snotz p)

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

  erase : {n : ℕ} (φ : Formula K n) → countFo φ ≡  → 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 の数が零なら、Empty.rec* に沿って eraseTm t p の名前を替えると、K 上の項の間のパスとして t 自身が返ります。名前替えの関数 Empty.rec* : ⊥* → K は空の型の消去子であり、K の定数を一つ作るよう求められると ⊥* の元を要求します。しかし eraseTm が組み立てた項には定数の節点が含まれないので、この関数が実際に適用されることはありません。したがって帰納には矛盾の場合と変数の場合しか残らず、後者は mapTm の計算規則、すなわち var i から var i を再構成する規則で閉じます。

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

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

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

            → mapFo Empty.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 はその論理式が無パラメータ論理式の正確な像であることを示し、構文を何も失わずに空の定数域を採用できるのです。