YONAPO RESEARCH
研究記録
MedDSL(仮称)

RESEARCH / RECORD

MedDSL(仮称)P2「意味能力の拡張契約」P2 設計

P2:意味能力の拡張契約の研究設計

原文 docs/research/19-p2-design.md

38 KB

GitHubで見る

版 be280c0

この文書の目次 11項目

作成日: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の手順 を再開する際の対象として保持する。