作成日:2026-10-19。状態:設計用草案・独立確認前。P2-a(宣言の書式と既存 handler への後付け)のみ実装済みで、実行契約 20・結果 21 に記録しました。その後、拡張ホストの分離・防護例の追加・宣言の固定を行い、22 に記録しました。P2-b(パイロット「概念の分割」)も実装し、設計と義務の導出を 23、結果を 24 に記録しました。P2-c(併用の検査)も実装し、設計と義務の導出を 25、結果を 26 に記録しました。P2-d(評価の固定・版の手順・独立確認の準備)も実施し、設計を 27、結果を 28 に記録しました。P2-a で実装の都合から設計を変えた点は、本文に「P2-a での変更」として注記しています。それ以外(P2-b 以降)は研究設計で、実装済み・検証済みの範囲は §2 の「実現した条件」と §4 の導出の注記、および 20・21 に限ります。形式証明支援系による検証はなく、導出は手作業です。P0/P1 の固定(p0-draft-2)と、そのレビューで得た教訓(16-review-record-ai-001.md)を前提にします。
本書の P2 は実装・研究の段階名(P0・P1 に続く)で、R4 の評価 の証明課題 P1〜P4 とは別の名前空間です。受入条件の ID は X01〜X14、決定の ID は D14 とします。
D14:今回決めること
最終目標 の「新しい概念・属性・関係・表現形式の登場」に対し、P0/P1 は個別の handler(定義追加、有限予測、事象化、引き継ぎの認定)ごとに「既存の意味と共存する条件」を満たしてきました。P2 は、その条件を再利用できる拡張契約として取り出し、新しい意味能力を追加するとき何を宣言し、何を証明・検査すれば既存の意味と共存できるかを定めます。
| 研究対象 | 選定 | 確かめる原理 |
|---|---|---|
| 拡張契約 | 宣言(識別・所有・関係クラス・範囲・義務・停止・併用)と、クラス別の義務表 | 個別 handler の暗黙の条件が、欠落を検出できる形で書き下せるか |
| 共存の定義 | 所有の分離・観測の保存・不変条件の保存・停止・併用・識別の六つの合併 | 「新しい名前だから安全」「認定票があるから併用できる」を成功にしない |
| 併用 | 独立な拡張の併用、記号を共有する拡張の併用、基底の変更の波及 | 個別の認定から全体の保証を導けない境界を、反例と再検証範囲で示す |
| パイロット | 実装は契約の後付けの適合(P2-a)から。新しい能力の候補は §7 で比較し、最初の候補を「概念の分割」にする | 契約が既存の追加(後付け)だけでなく、未実装の新能力の設計を導けるか |
P2 は、個別の機能を増やす段階ではありません。拡張を足すための手順の側を、研究と評価の対象にします。
1. 問いと位置付け
最終目標は、将来の変化を原理的に受け止める体系です。P0/P1 で実証したのは、有限のいくつかの変化(定義追加、読み取り専用の意味モジュール、表現の改訂、射影、方針変更)に対する、個別に設計し、個別に固定した保存条件です。次の問いは未解決です。
新しい意味能力 X を追加するとき、X の作者は何を定義し何を示せば、既存のすべての意味(基底とすでに登録された拡張)と共存できると言えるか。逆に、何が欠けていれば共存を認めてはならないか。
実証済み・形式化・未解決の区別:
| 区分 | 内容 |
|---|---|
| 実証済み(有限の範囲) | P0 の S1/S2 認定、forecast(読み取り専用)、events(表現の改訂)、handover の認定・射影・可用性が、それぞれの条件を満たすこと。変異検査・独立オラクル・予算掃引で、記載の有限領域では矛盾が見つからなかった(17) |
| 本書で形式化(手作業) | 拡張の関係クラス、共存の定義、七つの補題(§4)、機械可読の宣言の案 |
| 未解決 | 任意の意味能力に対する判定、無限の更新列、拡張間の相互参照が循環する併用、動的な意味(時間発展)、独立の確認者による検証 |
2. 現在の handler が実現している条件(逆向きの整理)
契約の素材は、すでに動いている条件です。次の表は、各 handler がどの条件をどこで実現し、何で確かめているかの整理です(場所は draft-2 のコミット 2b501c1 時点)。
| 条件 | P0 の定義追加(S1/S2) | forecast | events(事象化) | handover(認定・射影・可用性) |
|---|---|---|---|---|
| 識別(版・仕様 hash) | 契約を P0_SPEC_SHA256 で固定。認定票に依存の hash |
forecast_spec.json の生バイトを SPEC_SHA256 で照合。artifact と consumer が仕様 hash を持つ |
events_spec.json を照合。snapshot が仕様 hash と原の hash を持つ |
handover_spec.json、P0 の契約と5ファイルを実行時に照合 |
| 実装の同一性 | certifier(identity.py) |
同左(認定票を出す場合) | 同左 | 同左。認定票に付与 |
| 所有・衝突 | predicate_owner_conflict、reference_redefined、定義は自モジュールの述語のみ |
固定の述語 URN、artifact の重複拒否 | native 述語 URN の衝突拒否、事象 ID の新鮮さ検査 | 資源・改名の捕獲・重複の拒否 |
| 旧との関係の宣言 | 旧語彙へのモデル保存的拡張(旧データのみ) | 読み取り専用:書き込み操作なし、基底の語彙へ導出しない | 翻訳:充足の対応・モデル被覆(手作業)、履歴と採用の可換 | 恒等・翻訳・射影・方針変更を別の認定票で区別 |
| 新しい回答型 | 認定票(certified/not_certified) |
forecast_probability(有理数)。基底の supported に変換しない |
役割表(evaluation_mode)。旧変数へ射影して返す |
認定票(証拠の強さ付き)。反例・喪失は別欄 |
| 未知・未対応 | 未知の required_capabilities を持つ文脈は unassessed |
known_capabilities で自分の能力だけを許す |
同左(基底の方針) | unsupported_profile、native registry にない runtime は不可 |
| 資源 | steps を課金、打切りで認定票を出さない | 仕様に課金点を固定、打切りで部分値を出さない | 同左 | 同左。合成は予算を共有 |
| 検査の根拠 | 構文の十分条件、DAG、所有 | 型付き有理数、採用の P0 方針 | 実体から再計算した票、反例 | 既知テンプレート、有限モデルの反例 |
| 評価 | P0 の22条件 | H01〜H06・H20 | H07〜H12 | H13〜H19 |
共通の核(kernel)
共存の多くは、拡張が個別に頑張った結果ではなく、共通の核が守る不変条件に依っています。これを明示しない限り、拡張の作者はその条件を再証明する羽目になるか、黙って破ります。
| 不変条件 | 内容 | 実現している場所 |
|---|---|---|
| I1 支持の根拠 | supported は、採用された(人の確認済み)主張からの導出だけ |
ledger.py の採用選択、query.py |
| I2 未決は偽でない | 導けないことを偽・否定にしない。否定は明示された主張だけ | query.py の状態、reference の unassessed |
| I3 AI の候補を採用しない | 人の確認がなければ保留 | ledger.py、forecast の報告 |
| I4 未知の能力は解釈しない | 可視の主張が未知の能力を要求すれば、その文脈は解釈しない(保留・訂正済みも含む) | ledger.py の unknown、各 handler |
| I5 打切りで部分回答を出さない | 資源停止では未完了の問いは値を持たず、認定票も出さない | Budget、各 handler の例外処理 |
| I6 原情報の保持 | 入力を変更せず、原主張・確認・訂正を残す | evaluate の入力保持、events の完全な読み戻し |
| I7 決定性 | 同じ入力・版・上限から同じ結果(正規化 hash が同じ) | canonical JSON、P22 |
この七つは文書に散在していた性質を、レビュー(16)で確認した範囲を基に整理したものです。形式的な完全性は主張しません。
3. 拡張契約(Extension Contract)
3.1 拡張の宣言
新しい意味能力 X を登録するには、次を宣言します。宣言に欠落があれば登録を拒否します(部分的に適用しない)。
| 項目 | 内容 |
|---|---|
| 識別 | 拡張 ID・版・仕様の生バイト hash・依存する基底/他拡張の ID・版・hash。実装の同一性(certifier)で実体を追跡する |
| 所有 | X が新しく所有する名前の一覧:述語・操作・回答型・能力・URN。基底や他の拡張の名前を再定義しない |
| 関係クラス | 基底との関係を R1〜R5(§3.3)のどれかで宣言する。複数あれば分けて宣言する |
| 範囲 | 保存を主張する基底の問い Q と、データの条件(例:旧データのみ、新所属データなし) |
| 対応 | 保存の一般形(§3.2)の E と ρ。恒等の場合はその旨 |
| 義務 | クラス別の義務(§3.3)それぞれについて、主張・前提・証拠の強さ・検査方法・防護例(P2-a での変更:設計時は「負例」。拒否だけでなく、変換しないこと・境界を守る例を含めるため「防護例」とし、ないときは理由を書く) |
| 停止 | 未知の能力・未対応の profile・資源上限・入力不正での振る舞い |
| 併用 | 他の拡張と共有する名前、読む他の拡張、順序への依存 |
| 状態 | 作成者草案か、独立確認済みか。AI 生成の宣言は、人の確認までは候補として登録しない(§9) |
3.2 保存の一般形
P0/P1 で現れた保存はすべて、「範囲 Q、要求の翻訳 E、回答の対応 ρ」の三つ組で書けます。X を加えた系 B⊕X について、
任意の基底の要求 r ∈ Q について、 O( eval_{B⊕X}( E(r) ) ) = ρ( O( eval_B(r) ) )
O は観測(何を比較するか)、eval は handler の評価、等式は完了した回答の間のものです(資源は §3.6)。
| 関係 | E | ρ | O の例 |
|---|---|---|---|
| 恒等(R1・R2) | 恒等 | 恒等 | 基底の要求の結果(認定票の certifier を除く)。R1 は旧語彙の含意 |
| 翻訳(R3) | 式の移し方(事象化) | 回答値の対応(旧変数への射影) | 旧 Q の回答集合、採用状態、根拠 |
| 射影(R4) | 恒等 | 射影を通して決まる部分 | 保持した区別だけに依る Q(U1 の因子化) |
| 方針変更(R5) | - | 保存を主張しない | 変わる点を記録する |
R3 ではさらに、充足の対応とモデル被覆(R5 の C1)と履歴・採用の可換が必要です。R1 では旧モデルの拡張可能性(S1/S2)です。三つ組は、これらの具体的な義務を束ねる枠です。
3.3 関係クラスと義務
| クラス | 例(現在の実現) | 宣言する範囲 | 義務 |
|---|---|---|---|
| R1 定義的拡張 | P0 の S1/S2 | 旧データ・旧語彙の問い | (1) 新記号は X が所有。(2) 右辺は旧語彙と前の新記号のみ、非循環。(3) 旧モデルは必ず拡張できる(N=ψ か N=∅)。(4) 追加の包含・新所属データ・存在の制約を持たない。(5) 認定は十分条件で、不認定は非保存の断定でない |
| R2 読み取り専用モジュール | forecast | 基底の全要求(非干渉) | (1) 基底の状態への書き込み操作を持たない。(2) 基底の語彙の述語へ導出しない。(3) 基底の状態は、核の採用選択を通してだけ読む。(4) 回答型は基底の状態と別で、変換規則を持たない(橋渡しは別の拡張、§4 L5)。(5) 未知の能力を自分の能力としてだけ許す |
| R3 翻訳(表現の改訂) | events | 宣言した Q の部分集合 | (1) E と ρ を明示。(2) 充足の対応。(3) 旧モデルの被覆。(4) 新理論は翻訳した旧理論と型構造のみ(一意名仮定も入れない)。(5) 原履歴の完全な読み戻しと、採用・保留・訂正の可換。(6) 新しい名前は原の記録に対して新鮮。(7) 新しい構造(件数・同一性)を問う Q は範囲外と明示 |
| R4 損失のある射影 | projection | 保持列に収まる Q | (1) 因子化できる Q を範囲にする。(2) 失われた区別の反例(同じ射影値で旧回答が異なる二記録)を提示できる。(3) 後段の無損失符号化・別添えで全体の復元を主張しない |
| R5 方針・意味の変更 | absence の診断 | 保存を主張しない | (1) 変わる点(追加される仮定、変わる状態)を記録する。(2) 認定を出さない。(3) 臨床の主張を追加しない |
| R6 公理つき読み取りモジュール(P2-b で追加) | 概念の分割 | 宣言した範囲の問い | R2 の (1)〜(5)((2) は「結論を基底の原子・状態として返さない」に読み替え)に加え、(6) 追加する公理が閉じていて要求が変えられない。(7) 旧データを矛盾させない(旧モデルの拡張)。(8) 結論が公理のモデルに対して健全かつ完全。(9) 公理から導いた結論は頼る公理を挙げ、採用された主張として示さない。(10) 範囲外を明示する。(11) 情報要求が実現可能で、臨床の否定を含意しない(23 の §4) |
| JOINT 併用(P2-c で追加) | 概念の分割の併用 | 宣言した範囲の問い | R2・R6 の義務に加え、(1) 併用の構造を宣言した実体から再計算する。(2) 互いに素な併用は個別の結果に分解できる。(3) 記号を共有する併用の保存性は併用全体で再判定し、個別の認定を根拠にしない。(4) 鎖では後段の状態が前段の定める個体に限り定まる。(5) 範囲を明示する。(6) 個別と併用の差を隠さない(25 の §5) |
| 合成 | 事象化+改名の鎖 | 範囲の交差 | 各段の実体・依存・方針・翻訳後 Q を実体から再計算して照合し、範囲を `Q02 = {q ∈ Q01 |
P2-a での変更:既存の handler に宣言を書くと、この表では所有者を決められない名前が出た。クラスを二つ加えた。BASE(基底。保存の主張を持たず、核の不変条件を実現する)と HOST(複数の操作が共有する前段。操作を持たない。引き継ぎの識別・仕様と P0 実体の固定)。R5 には、保存を主張しない診断(欠落を否定にする方針変更の診断、旧処理系の可用性の点検)を含める。義務は 20 の §2 に具体化した。
3.4 共存の定義
拡張 X が既存の意味と共存するとは、次の六つがすべて成り立つことです。一つでも欠ければ、他の五つが成り立っていても「共存」と呼びません。
| 記号 | 内容 | 検査の例 |
|---|---|---|
| C-own | 所有の分離:X の名前は基底・登録済みの拡張と重ならない | predicate_owner_conflict、native 述語 URN の衝突拒否 |
| C-pres | 宣言した関係クラスの義務が、宣言した範囲で成り立つ(§3.2・§3.3) | クラス別の義務表の検査、負例 |
| C-inv | X の新しい出力が、核の不変条件 I1〜I7 を破らない | 回答型の検査、AI 候補の保留、未知能力の停止 |
| C-stop | 未知・未対応・資源で止まる規則が宣言され、実装されている | 能力不一致、予算掃引 |
| C-comp | 登録済みの拡張との併用条件(§4 L3・L4)を満たす | 独立/共有の判定、併用の再検査 |
| C-id | 版・仕様・実装の同一性が追跡でき、変更時の再検証範囲が決まる | hash の固定、certifier、依存の波及(§4 L7) |
「同じ予算で完了する」ことは共存の条件に含めません。意味の保存から、同じ資源での完了は従いません(既存の方針)。
3.5 証拠の強さと認定
既存の区別をそのまま使い、宣言の各義務に証拠の強さを付けます:導出テンプレートによる検査(checked_native_template)、有限モデルの検査、個別の入出力の照合、自己申告。(P2-a での変更:手作業の導出 hand_derivation を finite_check と checked_native_template の間に加え、弱い順に五段階とした。事象化の被覆などを、有限照合と区別するため。)拡張全体の強さは最も弱い義務の強さとし、自己申告の義務が一つでもあれば、その拡張を認定済みと表示しません。変異検査・独立オラクル・予算掃引は、義務そのものの証拠ではなく、検査が実装の退行を検出できることの証拠として別に記録します(RV-01 の教訓:ゲートごとに負例が必要)。
3.6 停止規則
- 未対応の profile/操作:
unsupported_profile。同じ名前の別の操作で代用しない。 - 未知の能力:その文脈は解釈せず
unassessed。保留・訂正済みの修飾も落とさない(I4)。 - 資源上限:未完了の問いは値を持たず、認定票を出さない(I5)。拡張の処理は共通の予算を消費する。
- 入力不正:構造・参照・hash の検査は予算に依らず同じ結果(入力不正を予算不足に変えない)。
4. 共存についての手作業の導出
以下は、前提と結論を分けた手作業の導出です。機械検証はなく、実装との対応は §8 の受入条件で検査します。
L1(非干渉) 前提:(a) evaluate は schema_version と操作で唯一の handler に振り分ける。(b) 各 handler は要求の純粋な関数で、可変の共有状態を持たない(不変の識別の cache を除く)。(c) X の追加は新しいモジュールと振り分けの一行だけで、基底の核・handler のコードを変更しない。結論:基底の任意の要求 r に対し eval_{B⊕X}(r) と eval_B(r) は、certifier を除き一致する。導出:(a)(b)(c) より同じコード経路が同じ入力で実行される。限界:(c) はファイルの hash で検査できるが、核を変更する拡張は非干渉を主張できず、基底の改訂として全体を再検証する(draft-2 の確認の時刻順がその例)。
L2(能力の単調性) 理解する能力の集合を U ⊆ U' とする。文脈 c の可視の主張のどれも U'∖U の能力を要求しなければ、c に関する評価結果は U と U' で等しい。導出:文脈が解釈不能かどうかは、可視の主張の要求する能力と理解する能力の集合だけで決まる。結論:能力 X を理解する消費側を増やしても、X の修飾を含まない文脈の結果は変わらない。X の修飾を含む文脈は、未理解のとき unassessed、理解したとき X の意味で解釈され、前者について保存の主張はない。
L3(独立な読み取り専用モジュールの併用) X1、X2 が L1 を満たし、所有する操作・schema_version・回答型が互いに素で、互いのモジュールを読み込まず、互いの要求の欄を読まないとする。このとき B⊕X1⊕X2 で、基底・X1・X2 のどの要求の結果も B⊕X1、B⊕X2、B での結果と等しい。導出:純粋な handler の振り分け。限界:二つが同じ基底の状態を読むことは許す(読み取りのため)。共通の核を変更する場合は L7。
L4(保存的な拡張でも併用は保存的と限らない) 反例(R4 の K04):旧語彙 {A,B}、新記号 N。拡張 E1 {A⊑N} は N=A で、E2 {N⊑B} は N=∅ で、それぞれ旧モデルを拡張できる。併用すると A⊑N⊑B で旧側の A⊑B が強制され、旧モデル A={u}, B=∅ は拡張できない。導出の帰結:記号を共有する併用は、個別の認定票から導けず、併用全体で再判定する。十分条件:新しい記号の集合が互いに素で、それぞれの公理が自分の新記号と旧語彙だけを含み、非循環の S1/S2 の形なら、依存順に旧モデルを拡張できるので併用も保存的。
L5(回答型の橋渡しは別の意味変更) 基底の supported は I1(採用された主張からの導出)を意味する。X の回答型 K(例:確率)を基底の状態へ写す規則は、K の値を主張として扱うことになり I1 の意味を変える。したがってそのような規則は X の一部としては認められず、別の拡張(橋渡し)として R5 で宣言し、新しい採用方針・人の確認・明示の根拠を要求する。forecast の「確率1でも supported にしない」はこの帰結。
L6(合成) 範囲を Q02 = {q ∈ Q01 | E01(q) ∈ Q12}、E02 = E12∘E01、r02 = r01∘r12 とすれば、充足の対応とモデル被覆は二回の適用で合成される(R5 の合成)。履歴・採用の対応は別に合成する。途中の R4 が失った区別は後段で回復できない。有限段の帰納で足り、無限列の極限は未定義。
L7(基底変更の波及) 依存辺を「X が M を読み込む」または「X の仕様が M の契約・実体の hash を固定する」と定める。核または基底のモジュール M を変更したとき、M から到達できるすべての拡張の義務を再検証する。これは宣言(depends_on)と読み込みの関係から機械的に列挙できる。draft-2 で validation.py(確認の時刻順)を変えたとき、実際に再固定が要ったのは P0 の実体 hash・契約 hash・native 仕様とそれを埋め込む p1-c の例だった。列挙が実測と一致するかは X13 で検査する。
導出が示さないこと
任意の意味能力に対する共存の判定、拡張の無限列の極限、循環する相互参照を持つ併用、動的な意味(時間発展)、並行する更新、性能。これらは §10 の未解決に残します。
5. 拡張ホストの最小インターフェース(設計)
P2-a の後の追加作業での変更:引き継ぎの族について、ホストと操作を分離した(22)。handover.py はヘッダーの検査と登録表による振り分けだけを持ち、鎖・欠落の診断・再生の点検は別のモジュールに分け、最上位の振り分けは host.py の登録表(schema_version → 処理)にした。挙動は変えていない(分離の前後で、全例・改変入力・予算の全値掃引の22,052件の出力が一致)。3 つの族(予測・事象・引き継ぎ)のヘッダー検査の共通化は行わなかった:エラーの path・code が族ごとに違い(例:予算の不正に path が付くか)、1 つにまとめると結果が変わる、つまりリファクタリングではなく契約の変更になるため。以下は設計時の案のまま残す。
現在、forecast.py・events.py・handover.py はそれぞれほぼ同じ前段(consumer の profile・仕様 hash・操作の照合、native 仕様の実体確認、予算の検証)を実装しています。P2-a ではこれを共通化し、拡張が守るべき契約を実装の形にします。
| 部分 | 内容 |
|---|---|
| 登録 | 宣言(§3.1)を検証して拡張を登録。所有の衝突・依存の hash・クラス別の義務の欠落を拒否 |
| 振り分け | schema_version と操作から唯一の handler へ。未知は unsupported_profile |
| 前段 | consumer の profile・仕様 hash・操作、予算の検証、native 仕様の実体確認 |
| 核の API | 採用選択(select_view)、Budget、正規化 hash、入力の検査。拡張はこれらを経由して基底の状態を読む |
| 結果の包み | profile・schema・input_sha256・certifier の付与、入力の保持 |
| 検査の入口 | 非干渉(拡張あり/なしで基底の例を比較)、依存の波及、宣言の完全性の検査 |
実装の分離(ホストと handler)は、挙動を変えないリファクタリングとして行い、固定済みの例・テスト・変異検査で退行がないことを確認してから進めます。新しい意味は、ホストを変えた段階では追加しません。
6. 機械可読の拡張宣言(案)
宣言は JSON で、実装と同じ版管理に置きます。p2-extension-manifest-draft-1 の設計時の案です(実際の書式は 20 の §1:項目は18。negatives は guards、title・contract_doc・implementation・pins・embedded_in を追加し、depends_on は {id, version} に簡略化した):
{
"schema_version": "p2-extension-manifest-draft-1",
"id": "p1-finite-forecast", "version": "draft-1",
"status": {"review_state": "author_draft", "independent_review": false},
"spec": {"path": "src/med_dsl/forecast_spec.json", "sha256": "<生バイト>"},
"depends_on": [{"id": "p0-positive", "version": "draft-2", "contract_sha256": "<06 の生バイト>", "kernel_modules": ["ledger.py", "validation.py", "model.py"]}],
"owns": {"operations": ["query_forecast"], "answer_kinds": ["forecast_probability"],
"predicates": ["fiction:forecast_reported@1"], "capabilities": ["p1-finite-forecast-draft-1"]},
"class": "R2",
"scope": {"base_requests": "all", "data": "any"},
"obligations": [
{"id": "R2-5", "statement": "自己申告の read_only や未知の能力名を根拠に、未知の意味修飾を無視しない", "evidence": "checked_native_template",
"checks": ["tests/test_p1_forecast.py"], "negatives": ["examples/p1-a/read-only-self-claim.json", "examples/p1-a/unknown-capability.json"]}
],
"stops": {"unknown_capability": "unassessed", "unsupported": "unsupported_profile", "resource": "resource_limit"},
"composition": {"shares_names_with": [], "reads_extensions": [], "order_dependent": false},
"evaluation": {"denominators": "P1-a 7条件・31 JSON", "negative_per_gate": true, "budget_sweep": true, "oracle": "tests/review/..."}
}
宣言の検査(lint)が見るのは、書式、hash と実体の一致、所有の素性、クラス別の義務と負例の対応、依存の閉包です。意味の正しさを検査するものではありません。既存の handler 6件(S1/S2、forecast、events、事象化+改名の鎖、射影、参考意味の恒等テンプレート)に宣言を書くことが P2-a の最初の作業です。(P2-a での変更:全操作の所有者を決めるため、基底・host・欠落の診断・可用性の点検を加えて10件になった。)
7. パイロット候補の比較
契約を、既存の追加の後付けだけでなく、未実装の新能力の設計に使えるかを試します。候補を三つ比べ、選定の基準は「既存の意味と干渉し得る度合い」「最終目標(コード体系の変化)との関係」「実装規模」「反例の豊富さ」とします。
| 候補 | 内容 | 干渉の度合い | 最終目標との関係 | 規模 | 反例 |
|---|---|---|---|---|---|
| A 概念の分割(候補集合) | 旧 P を新 P1/P2 に分割。旧の記録は区別情報を持たない(R4 の K06)。被覆公理 P ⊑ P1 ⊔ P2 と排他 P1 ⊓ P2 ⊑ ⊥ |
中:旧の P の問いは変えず、新の P1/P2 の問いは「どちらか不明」を返す | 高:コード体系の細分化に直接対応 | 中 | 多い:未決と偽の混同、被覆の欠落、排他の破れ |
| B 有効期間つきの主張 | 記録時点とは別の、臨床的な有効期間 | 高:採用・訂正・可視性の規則に触れる | 中 | 大 | 中 |
| C 単位つきの数量 | 単位・換算を持つ数量の比較 | 低:読み取り専用の型になりやすい | 低 | 小 | 少ない |
最初の候補は A とする(P2-a の完了後に最終決定)。理由:(1) 変化に耐える体系という最終目標に最も近い。(2) 被覆公理は新記号が吸収できる(P1=P、P2=∅ で旧モデルが拡張できる)ため保存的であり、契約の R1 の延長で扱える。一方、基底の Horn 断片は選言を持たず、「P だが P1 か P2 かは不明」を表すために新しい回答型(候補集合)と情報要求が要る。これは新しい表現力の追加であり、契約が「保存的か」「型は基底と分離されているか」「未決を偽にしていないか」を実際に問う。(3) 旧の記録の再解釈を、旧の P の問いと新の P1/P2 の問いで分けて検査できる。B・C は A の結果を見て選ぶ。
A の設計の要点(概要):新しい回答型 candidate_set(候補の集合と、確定に必要な情報要求)。基底の undetermined を使い分け、「候補が複数ある」状態を「偽」にも「確定」にもしない。確定は新しい確認(人)か、別の根拠による。
8. 段階と受入条件
| 段階 | 作るもの | 条件 |
|---|---|---|
| P2-a(実装済み・独立確認前。結果 21、追加作業 22) | 拡張の宣言の書式、既存の handler 10件への後付けの宣言、宣言の検査(lint)、依存の波及の列挙、引き継ぎの族のホスト分離、防護例の追加、宣言の固定 | X01〜X03、X06、X13 は達成、X07 は一部達成(防護例のない義務が3件残る)。固定済みの例・テスト・変異検査で退行 0 |
| P2-b(実装済み・独立確認前。設計 23、結果 24) | パイロット A(概念の分割)を契約に沿って設計・実装。契約に R6 を追加 | X04、X05、X14 は達成。義務の手作業の導出、有限モデルの全数検査、防護例(欠落 0)、変異検査 |
| P2-c(実装済み・独立確認前。設計 25、結果 26) | 併用の検査:独立な拡張の機械的な判定、記号を共有する分割の併用(K04 型)の全数の判定、入れ子の鎖。契約に JOINT を追加 | X08、X09 は達成、X10 は一部達成(情報を失う段を含む鎖は範囲外)。義務の手作業の導出、全数・独立オラクル、防護例(欠落 0)、変異検査 |
| P2-d(実装済み・独立確認前。設計 27、結果 28) | 評価の固定、独立確認の準備(PO13〜PO18)、版の手順の実演 | X11、X12 は達成(範囲と限界は 28)。統合評価、検査器の変異検査、独立確認の資料と再開点。独立確認と評価の凍結は未実施 |
受入条件(設計。実行は未実施):
| ID | 条件 | 確かめること |
|---|---|---|
| X01 | 宣言の必須項目の欠落を持つ拡張は登録を拒否する | 部分適用をしない |
| X02 | 基底または他の拡張と名前が衝突する拡張は登録を拒否する | C-own |
| X03 | 固定した全例(P0 37+P1 80)を、登録した拡張あり/なしで実行し、観測が一致する(certifier を除く) |
L1・非干渉 |
| X04 | 拡張を理解しない消費側は、拡張の修飾を持つ文脈で停止し、保留・訂正済みの修飾も落とさない | L2・I4 |
| X05 | 拡張の回答型が基底の状態へ暗黙に変換される経路がない。橋渡しは別の拡張として宣言した場合だけ | L5・I1 |
| X06 | クラス別の義務の欠落(例:R3 で被覆の反例検査がない)を不認定にする | C-pres |
| X07 | 各クラスの各ゲートに、認定を拒否する負例が少なくとも一つある(P2-a では「防護例または理由つきの欠落」に置き換えて実現した。最初は欠落24件、追加作業の後は3件が残る。21、22) | RV-01 の教訓 |
| X08 | 所有が互いに素な二つの読み取り専用拡張を同時に載せ、順序を入れ替えても、基底・各拡張の観測が不変 | L3 |
| X09 | 記号を共有する二拡張の併用を、個別の認定票だけで認定しない(K04 型)。併用全体で再判定する | L4 |
| X10 | 鎖の範囲は交差に狭まり、途中の喪失(R4)は後段で回復しない | L6 |
| X11 | 版を上げた拡張の旧版の入力が、旧版の契約で再現できる(旧版の保持と再固定の手順) | C-id。draft-2 の手順の再現 |
| X12 | 拡張の処理が共通の予算を消費し、全予算で完了済みの行が汚れず、打切りで認定票・回答を出さない | C-stop・I5 |
| X13 | 基底の検証規則を変えたとき、宣言から列挙した再検証範囲が、実際に再固定が要った範囲と一致する(draft-2 の RV-05 を後付けで再現) | L7 |
| X14 | パイロット A:旧の P の問いは変わらず、新の P1/P2 の問いは候補集合と情報要求を返し、偽にも確定にもしない | 契約の新能力への適用 |
分母は P0・P1 と別に数えます。条件の達成を、拡張の普遍性や将来の全変化への耐性の証明とは扱いません。
証明義務の追加(PO13〜PO18)
12の証明義務 に、次を加えます(独立確認の対象):PO13 宣言の完全性と識別、PO14 所有と名前空間の分離、PO15 非干渉(基底の要求の観測不変)、PO16 不変条件 I1〜I7 の保存(新しい出力に対して)、PO17 併用(独立・共有・鎖)、PO18 基底変更の波及と再検証範囲。
9. 評価・独立確認・AI の位置付け
- 評価:ゲートごとの負例、予算の全値掃引、独立オラクルとの乱数照合、変異検査を、拡張の登録に必須の証拠とする(今回のレビューで、既存テストの通過だけでは主要ゲートの退行を検出できなかったため)。検出されない変異は、等価である理由を記録する。
- 独立確認:P2-a の宣言と P2-d の評価を、最初から外部レビューの対象に含める計画にする。内部の単独実施の記録と、外部で覆り得る内部判断(17 の §6)を区別して残す。
- AI と医療者:拡張の宣言は開発者の内部表現で、医療者には見せない。AI が提案した拡張の宣言は、人の確認までは候補であり、登録しない。採用の方針(人の確認、訂正は明示、旧版を消さない)を、拡張の登録にも同じ型で適用する。
- データ:すべて架空。外部資料・実データ・患者情報を追加しない。D03 の保留範囲を維持する。
10. 範囲外と未解決
- 任意の意味能力に対する共存の自動判定。契約は宣言と検査の枠であり、正しさの自動証明ではない。
- 拡張が拡張を読む併用、循環する依存、無限の更新列の極限。
- 動的な意味(時間発展)、並行する更新、性能・可用性。
- 契約の義務表が完全であること。クラス R1〜R5 は現在の実現を整理したもので、未知の意味能力がこれに収まる保証はない。収まらない場合は新しいクラスを定義する手順を、P2-b の結果から検討する。 P2-b で、R2 に収まらない公理つきの読み取りモジュールのために R6 を追加した(24 の §5)。
- 医学的な妥当性。契約は意味の共存を検査するもので、拡張の医学的な正しさを検査しない。
次の判断
P2-a・P2-b・P2-c・P2-d は着手・実装し、21・22・24・26・28 に記録した(利用者の了承済み)。2026-10-20の 利用者決定 により、現在のリポジトリは独立の確認者を置かずに進める。2026-10-20に 次のパイロットとして候補B「有効期間つきの主張」を選定 した(P2-e)。まず意味・保存条件・反例・受入条件の設計から進め、候補C「単位つきの数量」はその次の候補として保持する。PO13〜PO18と内部判断の独立確認は、将来、英語で記述する別リポジトリを立ち上げ、確認が必要な時点から G0の手順 を再開する際の対象として保持する。