コンテンツにスキップ
Rigor

Matsumoto & Minamide 2010 (Ruby CFA) — Rigor 観点考察

Date: 2026-05-18.

Status: research note, no design commitments.

種別: 外部文献のRigor観点レビュー。

対象論文

Section titled “対象論文”

1. 論文要旨（一段落）

Section titled “1. 論文要旨（一段落）”

RubyのサブセットSemiRuby（class定義は事前所与・defはクラス名・ メソッド名・定義識別子の三つ組へ簡約・blockはラムダ式・return/break はthrow/catchペアに翻訳）に対して操作的意味論を与え、その上で メソッド定義について制御フロー依存な制御フロー解析（semi-flow-sensitive） を設計する。各プログラム点に「クラス×メソッド名 → メソッド定義」の写像 であるメソッド状況（method configuration）を関連付け、def式の 評価でこれを更新、if合流で集合的和をとる。値そのものは制御フロー 非依存、しかしどの定義が見えているかは制御フロー依存、という 非対称設計が新規性。 最後にPalsberg–Schwartzbach型の安全性解析（未定義メソッド呼び出し なし／yieldの対象はラムダ式）を定義し、保存 + Progressで 健全性を証明する。実装はOCaml + BDDBDDB（Datalog処理系）。

2. Rigorの今の設計との対応関係

Section titled “2. Rigorの今の設計との対応関係”
論文側の概念Rigor側の対応物一致度・所見
セミフローセンシティブという指針docs/type-specification/control-flow-analysis.mdのエッジ感度ナローイング、trinary certainty、fact stability一致。値のフルフローセンシティブ性を避けるという論文の現実主義は、Rigorのcertainty/effectモデルとも整合。
メソッド状況D = {(C,f) → d}Rigorのdispatcher階層（plugin → dependency-source → bundled）+ Plugin::FactStore（ADR-9）Rigorは静的に “どの定義が見えるか” をper-walkerでしか決めていない。論文のDはプログラム点ごとに動的に切り替わる点でRigorより強力。
例1：トップレベルclass A再オープンADR-17 pre_eval:論文ではセミフローセンシティブCFAが “x:Fixnum / y:String” をそのまま区別する。Rigorは同等の精度を「先に一度走らせてproject-wideなProjectPatchedMethodsを作る」二段階アプローチで近似する設計。論文側の方が解析機構としては美しく、ADR-17は工学的妥協であることが浮き彫りになる。
例2：defの中でdefを上書きRigorでは事実上ハンドルしていない論文の解析はこれも精度よく解析する。RigorはADR-5 robustness principle（Postel流の非対称規律）で「実務でそう頻繁には起きない」と切る側。代償として精度差は埋まらない。
例3：if分岐内のdefRigorのUnion narrowing双方とも保守的な和になる点で一致。論文もRigorも “本質的に静的解析不可能” と同じ判断。
SemiRubyのthrow/catchによるreturn/breakモデル化Rigorのnon-local-exit扱い（diagnostic familyの制御部分）設計判断としては同型。
インスタンス変数F[[l,@x]]Rigorのインスタンス変数推論（IVarのper-class shape）論文はロケーションごとに分割管理する点でRigorより細かい。Rigorはクラス単位＋初期化文脈で抑える。
安全性解析（未定義メソッド・yield健全性）Rigorのcall.method-not-found系（diagnostic-policy）検査対象はほぼ同じ。Rigorは加えてdef.return-type-mismatch系まで踏み込むが、論文側はそこまで型を持たない（値の集合のみ）。
健全性の形式証明（保存 + Progress）Rigorには存在しない仕様コーパスはRFC 2119規範だが、機械検証も操作的意味論もない。論文側がスコープをSemiRubyに絞ったからこそ証明できた事実は重要。Rigorが同等の証明を狙うなら、まず「証明可能な核（Rigor Core）」の切り出しが先になる。
実装：OCaml + BDDBDDB (Datalog)Rigor：手書きRuby推論エンジン + ファイルベース キャッシュ（ADR-4, ADR-6）論文のDatalog化はメンテ性で美しいが、（a）RBSとの結合、（b）pluginの任意Rubyロジック、（c）Ractor並列化（ADR-15）といったRigorの制約とは噛み合わない。設計トレードオフの差。

3. 論文がRigorに示唆する具体ポイント

Section titled “3. 論文がRigorに示唆する具体ポイント”

  1. 「メソッド定義の見え方だけはフローセンシティブ」というスライスは、 Rigorが次に精度を稼ぐ余地の一つを明確化している。現状Rigorは :leaf規律 + ADR-17の 事前評価でほぼ静的に決めてしまうが、部分的にプログラム点単位の “method configuration” を持つという中間案は理論的に正当化可能だと 本論文は示している。実装コストとキャッシュ整合性（ADR-6）次第。

  2. ADR-17のMVP（明示的ファイル列挙）で十分かの議論補強材料に なる。論文の例1のようなtop-level上書きはまさにADR-17のユース ケースで、論文は「メソッド定義に関して制御フローを区別する」 解析でこれを解いて見せている。 つまりADR-17の “explicit list” 路線は精度の下限を確実に押し上げる、 安価で正しい第一歩であると追認される。

  3. 健全性証明の不在はRigorの戦略的な空白として残っている。論文と 同じくコア + 外周の二層構造（SemiRuby ↔ Ruby全体）を取れば、 Rigorも “Rigor Kernel” だけは保存・Progressを狙えるはず。これは 現時点でROADMAPにも入っていないが、長期で価値の 高いトラックである。

  4. 本論文の第一著者 = Soutaro Matsumoto = Steepの作者という事実は、 RigorがSteep互換性（ADR-8） とRBS上位互換に置いている重みを再確認させる。Steepの現代的な実装の 系譜的前史をこの論文に見ることができる：method configurationが Steepの中ではsubtyping + global envのサニタイズで隠蔽されている、 という比較は単独でメモ価値がある。

  5. blockをlambda、return/breakをthrow/catchに翻訳するSemiRubyの スタイルは、ADR-16のマクロ展開 基盤Tier A（block-as-method）の意味論基礎としてそのまま流用できる。 SemiRubyの意味論をTier Aの「正しさ」の定義に採用する選択肢は 検討に値する。

4. まとめ

Section titled “4. まとめ”

論文はRigorの「メソッド定義の動的性vs静的解析」という最大級の 根本問題を、SemiRubyという最小核に絞ることで形式的に解いて見せた成果 である。Rigorは工学的にはより広いRuby表面をカバーしているが、 (a) pre_evalのような事前評価による近似に頼っており、（b）健全性の 機械的証明を持たない。論文のセミフローセンシティブCFAとその健全性証明は、Rigor の将来の “Rigor Kernel” 切り出しとmethod configurationを部分 採用するナローイング強化の両方向に、信頼できる出発点を提供している。

関連ADR / 仕様

Section titled “関連ADR / 仕様”

姉妹ノート

Section titled “姉妹ノート”

© 2026 TypedDuck. Licensed under CC BY-SA 4.0.