MysticIR Federation — 表面が違っても、地下パイプラインは同じ

概要

これは何か

MysticIR Federation v0.8.5 はプロトタイプ検証デモです — 完全な形式的証明ではなく、完成システムでもありません。3つの代表的な失敗ケースを対象に、1つの主張を確認することを目的としています。

💩 ScatLang と 🌊 SeaIR は全く異なる表面記号を使います。共有正規化パーサーによる正規化後、両者は同じ Core ASTを生成します。CEK マシンはその後、同じトレースを実行し、どちらの表面からスタートしても同じエラーシグネチャを同じステップで生成します。

現在の実装は、ScatLang 風および SeaIR 風の両方のトークンを受け付け、同じ Core AST ノードにマッピングする共有正規化パーサーを使用しています。v0.8.5 において「2つの独立したフロントエンドが収束する」と表現するのは過大評価です。これは v0.9 の課題です。

📋 査読メモ

地下パイプライン = Core AST + CEK machine + error signature と定義します。

安全な主張：「共有正規化パーサー上で、異なる表面記号を同じ Core AST に写し、frontend ラベルを除いた CEK trace / error signature が一致することを、代表的3ケースで確認した。」

💩 ではなく A ではないのか？
💩 と 🌊 は表面マーカーであり、意味論的なプリミティブではありません。MysticIR で重要なのはどの記号を使うかではなく、その記号が同一の Core AST ノードに射影されるかどうかです。A でも B でも同様に機能します。地下パイプラインは表面記法に無関心です。

アーキテクチャ

地下パイプライン構造

表面記号は2方向から入力されます。共有正規化パーサーがそれらを単一の Core AST に統合します。そこから先の実行は完全に同一です — 同じ継続、同じ環境、同じエラー。

💩 ScatLang

表面パーサー

🌊 SeaIR

表面パーサー

Core AST

両者が同一のツリー構造に正規化

CEK マシン / トレース

同一ステップ列、同一継続

Error Federation

同一シグネチャ（frontend ラベルを除く）

💩ScatLang / 🌊SeaIR のフロントエンドラベルはトレース記録に保持されるため、表面の違いは証拠として残りつつ、内部の実行は同一となります。

検証結果

3つの失敗ケース、全て確認済み

以下は Python スクリプト実行の実際の出力です。3つの代表的ケース全てで ast_equal、trace_equal、error_equal = true かつ surface_diff = true を確認しました。

ケース	エラー種別	ast_equal	trace_equal	error_equal	surface_diff	ステップ数
mod by zero 💩×3 ⊛ 💩₀ → ゼロ除算	ScatError	✓ true	✓ true	✓ true	✓ true	12 == 12
unbound variable 未定義変数 "missing" への参照	ScatError	✓ true	✓ true	✓ true	✓ true	2 == 2
step limit / infinite loop 0 ≠ succ(0) が常に true → ステップ40で停止	StepLimitError	✓ true	✓ true	✓ true	✓ true	40 == 40