確認日：2026-10-18。R5 の出典 と P0-d の実行記録 を引き継ぎます。P1 の確率の意味・認定票・有限例は本プロジェクトの設計であり、下記の論文が MedDSL の妥当性を証明したとはしません。
今回の一次資料
| ID | 資料・実際に確認した箇所 | 反映したこと・限界 |
|---|---|---|
| P1-S01 | Goguen・Burstall (1992), Institutions: Abstract Model Theory for Specification and Programming。§4.1、Definition32、Definition34、Proposition35、印刷pp.125–126（PDF31–32ページ） | 文とモデルの充足対応、および異なる体系へ推論を移す際のモデル側の全射性条件を再確認。P1 の E/r は向き・対象を独自に固定し、institution 全構造の実装・原著の命名との同一性は主張しない |
| P1-S02 | Fagin・Kolaitis・Miller・Popa (2005), Data Exchange: Semantics and Query Answering — IBM Research。著者・公表情報・抄録のみ | データ交換を満たす複数解と certain answers を区別する立場を確認。本文の定理・chase の停止性・計算量は今回未確認で、実装・universal solution の採用根拠にしない |
P1-S01 は Web の最初の抽出後、指定ページの再取得がタイムアウトしたため同じ配布URLから原著PDFを取得し、PDF31・32ページを画像化して数式と抽出文字を照合しました。Definition34 の語は画像で surjective on objects と確認し、文字抽出の誤りを仕様へ転記していません。全52ページを精読したわけではありません。
原PDFと二ページの画像は Git 管理外の data/research/p1-sources/ に置き、リポジトリへ同梱していません。原PDFの生バイト SHA-256 は f6715ca333dd03dc153a65907c1c974fa151690bb94eafffc065c363265b634d です。授業ページ上の配布を、ソースコードや派生物の公開許諾とは扱いません。
本プロジェクトで定めたこと
| 内容 | 根拠の種類 |
|---|---|
| データ・自由変数の割当を含む E/r と旧モデル被覆 | R5 C1 の研究用の導出を具体化した契約。原著の一般構造を実装したものではない |
| 四項関係から同一事象への役割付け | R5 C1-a のモデル構成を再利用。実行の支持・否定・履歴・由来の保存義務は別途加えた |
| 有限予測の有理数値・世界集合・交差 | 自分たちで定義する有限モデル。臨床確率や校正の外部基準を採用した主張ではない |
| 確率1と臨床事実の分離、未確認報告の保留 | プロジェクトの型と採用方針の設計要件 |
| 二つの旧記録が同じ値集合へ写る反例 | R5 U1 の独自の導出と P0 P08 の架空例 |
| 1/2要素の検査を通っても3要素モデルを失う反例 | H18 の手作業のモデル反例。未実装の有限モデル検査器の結果ではない |
RDF 1.1 の意味仕様も再度開きましたが、P1 の新しい符号化や推論器の採用根拠には追加していません。既存仕様の利用範囲は R5 の記録のままです。FHIR・OWL・外部語彙の新しい版への適合を今回確認したとはしません。
未確認の範囲
P1 のテンプレートに対する証明支援系での検算、有限予測・事象化の実装、合成の実行、独立した期待値の確認、医療者・AI の操作負担、臨床精度は未検証です。WHO・LOINC 等の取得・転用の保留は D03 のままです。今後外部資料を取り込む場合も、閲覧・取得・独自体系への利用・共有の条件を分けて確認します。