形式仕様の変更履歴

今回の目標と範囲

目標: 仕様を確定させ、INST_TYPE と DefOK/TypeDefOK の構造的なつながりを規則レベルで明示し、査読者が健全性の根拠を見つけるために複数の節を横断して読む必要がないようにすること。
範囲:
- 原稿の一貫性の総点検(用語、状態モデル、非空の型の意味論)
- INST_TYPE 規則の書き直し(前提、失敗の分類、ブリッジ注記)
- 査読用の完全なパッケージ(本原稿 + PDF + 本変更履歴)の作成。
範囲外: カーネル実装コードの変更。

節ごとの変更

== Global Theory State vs Local Scope State (doc/attachments/qed_formal_spec.typ:208)
- 2 層の状態モデル (T, S) を明示した。T はグローバルな理論の履歴、S はローカルで pop 可能な可視性の層である。
- DefHeads(T) が単調であり、pop は定義の履歴を巻き戻さないことを述べる命題を追加した。
- 同等の実装上の見方「墓標レジストリとして実現できる」を追加した。
== Type Constructor Extension Discipline (doc/attachments/qed_formal_spec.typ:257)
- 型拡張に対する TypeDefOK の受理条件と規則ステップを追加した。
- 「空の型からの逃げ道なし」という構築不変条件を導入し、非空性を単なる仮定から監査可能なゲート制約へと変えた。
= Definitional Extension Discipline および == Definition Admissibility Judgment(doc/attachments/qed_formal_spec.typ:694、doc/attachments/qed_formal_spec.typ:731)
- 定義ヘッドの新規性を c ∉ DefHeads(T) に統一した(現在の可視性に対するあいまいな検査を置き換える)。
- TVars(r) ⊆ TVars(tau) を規範的な条件として維持・強化し、ゴースト型の抜け穴を引き続き塞ぐ。
= Global Admissibility Envelope (doc/attachments/qed_formal_spec.typ:763)
- エンベロープを拡張した。DefOK に加えて、型拡張の必須ゲートとして TypeDefOK を追加した。
== Rule Schema: INST_TYPE (doc/attachments/qed_formal_spec.typ:1052)
- 一般的な valid(theta) を構造化された前提に書き直した。
  - valid_ty_subst(theta);
  - admissible_ty_image(T, theta);
  - def_inst_coherent(theta, A_p ⊢ p).
- 失敗の分類を 5 項目に拡張し、それぞれが上記の前提と一対一に対応する。
- この規則が DefOK/TypeDefOK/グローバルエンベロープとどのようにループを閉じるかを明示するブリッジ注記を追加した。
== Signatures and Symbols / == Constant Type Schemes and Instance Relation (doc/attachments/qed_formal_spec.typ:104)
- 定数の主型スキーム kappa_c : tau_gen とインスタンス関係 tau preceq tau_gen を導入した。
- 定数のインスタンス化が仕様レベルで第一級の関係であることを述べた。「項中の型 == 登録された型」というリテラルな同一性はもはや要求されない。
== Core Typing over Resolved Terms (doc/attachments/qed_formal_spec.typ:372)
- RConst 規則を、「厳密な型の等しさ」による照合から「主スキーム + インスタンス関係」による照合へ変更した。
- 多相定数のインスタンス化の利用可能性に関する補題を追加し、システムが単相に固定されていないことを述べた。
= Soundness Strategy と依存関係グラフ(doc/attachments/qed_formal_spec.typ:1132、doc/attachments/qed_formal_spec.typ:1152)
- 義務を 4 から 5 に拡張し、「型レベルの非空性保存」を別立てにした。
- 依存関係グラフにノード Type Admissibility + TypeDefOK と Type Non-Emptiness Preservation を追加した。
== Semantic Assumptions (doc/attachments/qed_formal_spec.typ:1190)
- 「すべての型は非空である」を、単一のグローバルな仮定から次のものへ絞り込んだ。
  - 基底 prelude に対する非空性の仮定
  - TypeDefOK の前提の下でのグローバルな非空性保存定理
付録の更新(doc/attachments/qed_formal_spec.typ:1301 以降)
- 付録 A: INST_TYPE の依存関係に TypeDefOK と定義の整合性が含まれるようになった。
- 付録 B: チェック項目が型ゲートと状態履歴の分離をカバーするようになった。
- 付録 C: Definition + State のシナリオに拡張し、pop 後の再定義を拒否するケースを追加した。
- 付録 D: 型の健全性監査シナリオを追加した。

監査課題表(課題 -> 修正 -> 箇所 -> 残存リスク)

課題	修正	箇所	残存リスク
ゴースト型変数(定義本体から漏れ出す自由型変数)	`TVars(r) ⊆ TVars(tau)` の強制 + `INST_TYPE` のブリッジ注記 + `def_inst_coherent` の前提	`doc/attachments/qed_formal_spec.typ:701`, `doc/attachments/qed_formal_spec.typ:1052`	低(実装も、まったく同じ条件を強制しなければならない)
空の型による意味論上の逃げ道(空の型を通じた意味論上の逃げ道)	`TypeDefOK` + 非空性ウィットネスのゲート + 非空性保存定理を追加	`doc/attachments/qed_formal_spec.typ:257`, `doc/attachments/qed_formal_spec.typ:1190`	低〜中(typedef 構文の将来の拡張でもウィットネス規則を維持しなければならない)
スタックと理論の不整合(pop 後の再定義があいまい)	`(T,S)` を分離し、定義ヘッドの新規性を `DefHeads(T)` に結び付け、pop は履歴を巻き戻さない	`doc/attachments/qed_formal_spec.typ:208`, `doc/attachments/qed_formal_spec.typ:694`	低(記号の混同を避けるため、UI 層は引き続きカーネル上の同一性を示さなければならない)
`INST_TYPE` が査読で追跡できない(章をまたいで推測する必要がある)	規則内に明示的な許容性のアンカーと失敗の対応を追加	`doc/attachments/qed_formal_spec.typ:1052`	低
de Bruijn の型消去(カーネルレベルでの型消去)	de Bruijn コア構文を明示的な型ラベルを持つ形(`DAbs(tau, ...)`、`DBound(..., tau)`)に変更し、`TRANS`/`BETA` の照合条件を型付きコアのガードに変更	`doc/attachments/qed_formal_spec.typ:439`, `doc/attachments/qed_formal_spec.typ:886`, `doc/attachments/qed_formal_spec.typ:977`	低(実装は、境界のローワリング中に型ラベルを厳密に保持しなければならない)
多相のロックアウト(多相定数のインスタンス化が封じられる)	定数の主スキームとインスタンス関係 `tau ≼ tau_gen` を導入し、エラボレーション、コア型付け、`INST_TYPE` にインスタンスのガードを追加	`doc/attachments/qed_formal_spec.typ:125`, `doc/attachments/qed_formal_spec.typ:379`, `doc/attachments/qed_formal_spec.typ:1109`	低(実装も、同じインスタンス判定を用いなければならない)

増分改訂(de Bruijn の型消去の監査)

== De Bruijn Shifting (for BETA) (doc/attachments/qed_formal_spec.typ:439)
- 型なしのコンストラクタ(Abs(t)、BVar(k))を、型付きコアのコンストラクタ(DAbs(tau, t)、DBound(k, tau))に置き換えた。
- beta 簡約規則に、束縛子と引数の型の一致という副条件を追加した。
- 型付きコアの単射性の不変条件を追加し、異なる定義域の型に対する抽象が構造的に同一視されることを防ぐ。
== Boundary Conversion Properties (doc/attachments/qed_formal_spec.typ:510)
- 型に敏感なコア照合の補題を追加し、境界のローワリングが束縛子の定義域の型ラベルを消去しないことを述べた。
== Rule Schema: TRANS (doc/attachments/qed_formal_spec.typ:865)
- 型付き de Bruijn コアの照合の前提と対応する失敗項目を追加し、中間項がその「消去された構造」によって誤って照合されることを防ぐ。
== Rule Schema: BETA (doc/attachments/qed_formal_spec.typ:954)
- レデックスの形を型付き版に書き直した。
- 失敗の分類に束縛子の定義域ラベルの不一致を追加した。
- 前件の形に type_of(u) = tau が明示的に含まれるようになった。
付録の強化:
- 付録 A に TRANS/BETA の型付きコアの依存関係を追加した。
- 付録 B に型に敏感な de Bruijn 照合のチェック項目を追加した。
- 付録 E(型付き de Bruijn コア監査シナリオ)を追加した。

増分改訂(多相ロックアウトの監査)

== Constant Type Schemes and Instance Relation
- 定数の主スキーム kappa_c : tau_gen とインスタンス関係 tau ≼ tau_gen を追加した。
- 定数はコア内で「主スキーム + インスタンス化された型」として有効であることを述べた。リテラルな型の等しさはもはや要求されない。
== Named Elaboration Judgment および == Core Typing over Resolved Terms
- RConst のエラボレーションとコア型付けの前提は、いずれもインスタンス関係の判定に切り替わった。
- 「多相定数のインスタンス化の許容性」補題と「単相へのロックアウトなし」の注記を追加した。
== Rule Schema: INST_TYPE
- 定数インスタンスの整合性という副条件 tau_i ≼ tau_gen(kappa_c) を追加した。
- 失敗の分類に定数インスタンスの不一致を追加した。
- ブリッジ注記が、定数インスタンスのガードと表現力をカバーするようになった。
付録の強化:
- 付録 A に、INST_TYPE の定数インスタンス関係への依存を追加した。
- 付録 B に tau ≼ tau_gen のチェック項目を追加した。
- 付録 D に、多相定数のインスタンス化に関する監査シナリオ(id を bool/int のインスタンスで使用できること)を追加した。

受け入れチェックリスト(合否付き)

[PASS] INST_TYPE の節が DefOK、TypeDefOK、およびグローバルな許容性エンベロープを明示的に参照している。
[PASS] グローバルな履歴の意味論が DefHeads(T) に統一され、ローカルな pop の挙動から分離されている。
[PASS] 非空の型の意味論が、単なる仮定から TypeDefOK ゲート + 保存定理という記述に移行している。
[PASS] 原稿の付録に Ghost/Empty/Pop-Redefine の回帰シナリオが含まれている。
[PASS] de Bruijn コアが明示的な型注釈を持ち、TRANS/BETA 規則がそれらに対する検査を強制している。
[PASS] 多相定数の使用が tau preceq tau_gen インスタンス関係によって可能になり、単相へのロックアウトを避けている。
[PASS] コンパイル検査が通る。
- コマンド: typst compile doc/qed_formal_spec.typ doc/qed_formal_spec.pdf
- 結果: QED 形式仕様が正常に生成される。

未解決事項(なければ None と記す)

None。

増分改訂(構成的閉包)

SpecOK の節の Theorem Goal を正式な定理に格上げし、「単一ステップの仕様ヘッド除去」の構成的な証明方法を追加した。
- 再帰的な除去子 erase_spec を原稿内で定義する。
- 導出木のサイズに基づく整礎帰納法の不変条件を与える。
Constructive Closure: Derivation Objects and Erasure Operators の節を追加した。
- 有限の導出オブジェクト Derives(D, s) を導入する。
- 3 種類の除去子 erase_def / erase_spec / erase_typedef を定義する。
- 対応する 3 つの正しさの定理(旧言語の文の保存)を与える。
Meta-Theorem Target を、正式なグローバル保存性のメタ定理に格上げした。
- 有限の拡張列に対して、ステップごとに後ろ向きに除去していく合成的な証明を明示的に書き下す。
- 各ステップのゲート除去の正しさから、グローバルな T' ⊢ φ => T ⊢ φ を導く。
それに合わせて、文書の状況と P0 チェックリストを更新した。
- Current Status は「構成的閉包が原稿に与えられている」と記すようになった。
- チェックリストに「導出オブジェクト体系」と「ゲートごとの除去 + 合成定理」の 2 項目を追加した。

増分改訂(2 部構成への分割と権威の境界)

本原稿の冒頭に Part I: Logic Core (Normative) と Authority Contract を追加した。
- Part I が論理に関する唯一の規範的な情報源であると述べる。
- de Bruijn とスコープは論理的な正しさのための仕組みであり、任意の工学的詳細ではないと述べる。
工学編の入口を Part II: Engineering Realization (Informative + Conformance) に改名した。
- Part II は Part I の下流にあり、論理を逆向きに定義してはならないと明示的に宣言する。
Conformance Obligations (Part I -> Part II) の小節を追加した。
- 5 つの実装適合義務: 規則への忠実性、境界への忠実性、スコープの安定性、ゲートへの忠実性、および証明書の非権威性。
Documentation Maintenance Notes の最初の文を、2 部構成の保守方針を反映するように書き直した。
- Part I は論理に関する正本として保守される。
- Part II は Part I に対する適合性報告の層として保守される。

増分改訂(de Bruijn / スコープの証明の強化)

de Bruijn の節に 3 つのブリッジ定理を追加した。
- Lowering Preserves Typing;
- Lifting Preserves Typing up to Alpha;
- Boundary Commutation with Capture-Avoiding Substitution.
スコープ付きシャドーイングに関する 3 つの命題を、証明の概略から完全な証明に格上げした(定義からステップごとに導出)。
Resolution Freeze under Scope Mutation 定理を追加した。
- 解決済みの項の前提が、後続の push/add/pop 列に対して不変であることを形式的に述べる。
- スコープは将来の名前解決にのみ影響し、既存の解決済みオブジェクトへは書き戻されないと述べる。

増分改訂(自動フェーズ進行: Part I の脱工学化 + Part II の収束)

Part I の文言から工学上の結び付きを取り除いた(論理的内容は変えない)。
- Abstract を「implementation-aware specification」から「formal mathematical specification」に変更した。
- Type Grammar / Term Grammar の「In implementation terms」を「One canonical concrete representation」に書き直した。
- 境界/スコープの段落における API・実装に関する文言を、抽象的な意味論上の文言に書き直した(実装は可能なままだが、特定の実装には結び付かない)。
MK_COMB の節を Type Preservation Sketch から Type Preservation Theorem に格上げした。
- 元の導出構造を保ち、完全な「Proof.」で締める形式に仕上げた。
Part II を適合性の意味論に収束させた。
- エラー分類の整合に関する段落を「最終 API に対して規範的」から「工学的実現に対する適合目標」に変更した。
- 付録 B の結びの文を「論理の閉包 + 適合性/回帰ゲート」に変更した。

増分改訂(自動フェーズ進行: Part II の適合性の閉包)

Engineering Correspondence に「informative only」の境界宣言を追加した。
- モジュールの対応は監査のカバレッジのためだけにあり、Part I の定義や定理は一切変更しない。
Conformance Transfer Theorem の節を追加した。
- Faithful Realization(5 つの適合義務を満たすもの)を定義する。
- 実装から論理への転送定理を与える。実装がシーケント $s$ を受理するなら、 $s$ は Part I で導出可能である。
- 証明は受理のトレースを再構成する。規則の対応、境界補題による代入、スコープの安定性による消去、ゲートの対応、および証明書イベントの破棄である。
Primitive Rules の導入段落から実装への結合を取り除いた。
- 「実装の更新と並行して」を「Part I の副条件が権威を持つ」に変更した。

増分改訂(自動フェーズ進行: Primitive Rules に対する構成的閉包の強化)

Rule Schema の章の末尾に Rule-Level Constructive Preservation Capsules を追加した。
- 統一された構成的テンプレート Preserve_R : valid(Premises_R) => valid(Conclusion_R) を与える。
- 10 個の基本規則それぞれにカプセル化された保存の主張を与える(INST_TYPE の 3 つの制約、すなわちゲート、整合性、インスタンスを含む)。
- 要約定理 Rule Capsule Closure を追加し、「規則ごとの場合分け + カプセルの呼び出し」で P1 の義務を閉じるのに十分であると述べる。

増分改訂(自動フェーズ進行: 2 部構成の監査チェックリストの完結)

付録 B(P0 チェックリスト)を Part II の一貫性項目で拡張した。
- 項目 24-28 を追加した。Part II の下流宣言、5 つの適合義務、転送定理、非権威的な対応、およびエラー分類の適合性上の位置付けをカバーする。
付録 G Part II Conformance Audit Scenarios を追加した。
- 規則への忠実性のリプレイ
- 境界への忠実性
- スコープへの忠実性の安定性
- ゲートへの忠実性
- 証明書の非権威性
これにより、「Part I の論理の閉包 + Part II の適合性の閉包」という二段構えの監査構造が完成する。

増分改訂(自動フェーズ進行: 意味論的仮定のパッケージと無矛盾性の層)

Semantic Assumptions の下にモデルクラスのラッパーを追加した。
- Admissible Model Class の定義(型付け/表示 + Choice + Infinity のアンカー + ゲートが受理した定理)を追加する。
- Model-Class Non-Emptiness の仮定を追加し、「非自明なモデルが存在する」という前提を明示する。
無矛盾性の転送結果を追加した。
- Semantic Non-Triviality Transfer(反例モデルがあれば導出不可能である)
- Consistency Witness Form(同じモデルクラスの意味論の下では、ある文とその否定は同時には導出できない)

増分改訂(自動フェーズ進行: 主張から証明へのトレース表)

付録 H Claim-to-Proof Trace Matrix を追加した。
- 10 個の高水準の主張 C1..C10 から「定義のアンカー/証明のアンカー」への短い経路の対応を与える。
- 規則の健全性、3 種類のゲートの保存性、スコープ/境界の安定性、グローバルな保存性、適合性の転送、非自明性、および証明書の非権威性をカバーする。
付録の末尾に査読規則を追加した。
- 各主張は「主張 -> 定義 -> 定理」の 3 ステップで到達できることを目指し、査読と相互検証を容易にする。

Part I から工学用語をさらに取り除き、統一した。
- external modules は external contexts になる。
- implementation-level check は admission-procedure check になる。
- module boundaries and test responsibilities を証明ブロックの観点から書き直した。
- 無限性のアンカーと正準定理における implementation という語を、実現/提示の意味論に置き換えた。
それに合わせて、保守注記と監査シナリオの文言を統一した。
- APIs evolve は realization interfaces evolve になる。
- 付録 F のスキーマ拡張シナリオは、受理手続きの意味論を用いるようになった。
記法を統一した。
- 意味論的解釈の記法を "denote"(t, rho, M) に統一し、後の境界における表示補題と同じ引数規約を用いる。

増分改訂(自動フェーズ進行: 閉包アンカーの補完)

Part II の Audit Certificates and Replay Interface に、欠けていた定義アンカーを追加した。
- Admissible(T, t_h) の定義を追加する(Part I の Derives オブジェクトとゲートの適法性によりウィットネスされる)。
- SentenceInLanguage(T_0, t_h) の定義を追加する(閉じた文 + 基底言語の記号の制約)。
ConservativeReplayOK は、明示的に定義された述語を用いるようになり、暗黙の意味論的前提に依存しなくなった。

増分改訂(記法の一貫性の修正)

代入におけるスラッシュ記法を統一した。
- t[s/x] を t[s\/x] に統一する。
- 本文中の既存の s[u\/x] 記法に合わせ、査読や描画における [A/B] 形式のあいまいさを避ける。

論理的内容を変えずに、全文の文体を学術論文のスタイルに寄せた。
- Authority Contract を Normative Scope に改め、強い命令調の文を一部、学術的な説明文に書き直した。
- Part II の冒頭を、「implementation hooks」という枠組みから「concrete realization and conformance record」という枠組みに移した。
- Documentation Maintenance Notes を Concluding Remarks に、Near-term maintenance focus を Future refinement directions に改めた。
付録の文体を統一した。
- Audit Scenarios を一律に Validation Scenarios に改名した。
- 結びを「required before claiming」から「provide structured evidence for …」に変更した。
意味論上の細かな一貫性:
- 意味論的解釈の記法を "denote"(t, rho, M) に統一した(後の表示補題と整合)。
- ConservativeReplayOK に関連する述語は本文中で名前付きで定義されるようになり、暗黙の用語が減った。

形式仕様の変更履歴

今回の目標と範囲

節ごとの変更

監査課題表(課題 -> 修正 -> 箇所 -> 残存リスク)

増分改訂(de Bruijn の型消去の監査)

増分改訂(多相ロックアウトの監査)

受け入れチェックリスト(合否付き)

未解決事項(なければ None と記す)

増分改訂(構成的閉包)

増分改訂(2 部構成への分割と権威の境界)

増分改訂(de Bruijn / スコープの証明の強化)

増分改訂(自動フェーズ進行: Part I の脱工学化 + Part II の収束)

増分改訂(自動フェーズ進行: Part II の適合性の閉包)

増分改訂(自動フェーズ進行: Primitive Rules に対する構成的閉包の強化)

増分改訂(自動フェーズ進行: 2 部構成の監査チェックリストの完結)

増分改訂(自動フェーズ進行: 意味論的仮定のパッケージと無矛盾性の層)

増分改訂(自動フェーズ進行: 主張から証明へのトレース表)

増分改訂(自動フェーズ進行: 用語の一貫性の洗練)

増分改訂(自動フェーズ進行: 閉包アンカーの補完)

増分改訂(記法の一貫性の修正)

増分改訂(文体の洗練)