Scoped MSO, Register Automata, and Expressions: Equivalence over Data Words

この論文「Scoped MSO, Register Automata, and Expressions: Equivalence over Data Words（スコープ付き MSO、レジスタオートマトン、および式：データ単語上の等価性）」は、無限アルファベット（データ値）を持つデータ単語に対する言語クラスを記述する新しい形式的体系を提案し、それらが非決定的レジスタオートマトン（NRA）と等価であることを示すものです。

以下に、論文の技術的な要約を問題設定、手法、主要な貢献、結果、意義の観点から詳細に記述します。

1. 問題設定と背景

• 背景: 有限アルファベットにおける「正則言語」は、有限オートマトン、正則式、モノadic 第二階論理（MSO）の 3 つの異なる記述体系によって特徴付けられるという「ロバスト性（頑健性）」が知られています（Kleene の定理、Büchi-Elgot-Trakhtenbrot の定理）。
• 課題: しかし、プロセス ID やデータベースキーなどをモデル化する**無限アルファベット（データ値）**を持つデータ単語（$\Sigma \times A$ 上の列）の文脈では、このロバスト性は失われています。既存の論理やオートマトンの多様性により、表現力が比較不可能であったり、決定可能性が異なるなど、統一的な「正則性」の概念が存在しませんでした。
• 対象モデル: 本論文は、**推測（guessing）**機能を持つ非決定的レジスタオートマトン（NRAg）を基準モデルとして扱います。NRAg は、有限個のレジスタにデータ値を格納・比較するだけでなく、入力に現れない新しいデータ値を「推測」してレジスタに格納できる能力を持っています。
• 既存の限界:
  • 単純に MSO にデータ比較を追加すると、判定問題が未決定（undecidable）になります。
  • 逆に、制約を厳しくしすぎると NRAg の表現力を捉えきれません。
  • 既存の式体系（Brunet & Silva など）は、名前の割り当て・解放を明示するバインダを含むため、構文が複雑になり、古典的な正則式の精神から離れていました。

2. 主要な貢献と新しい形式体系

著者は、NRAg の表現力を完全に捉える 2 つの新しい形式体系を提案し、これらが NRAg と等価であることを証明しました。

A. Scoped MSO (スコープ付き MSO)

NRAg の表現力に合わせた新しい論理体系です。

• セグメント・モダリティ ($\mathcal{X}\varphi$): 集合 $X$ で定義される「切断位置」に基づいて、論理式 $\varphi$ を部分区間（スコープ）ごとに評価する演算子です。これにより、レジスタの「ライブ区間（値が有効に保持されている区間）」に対応する構造を制御できます。
• 構文上の制限（Well-formedness）: データ原子論理式 $R(x)$ において、ネストされた変数（negation のスコープ内にある変数）は高々 1 つまでという制限を設けます。これにより、任意の位置間でのデータ比較を避け、レジスタの有限性を模倣します。
• 条件: この等価性は、原子（データ領域）が**「強力な推測（strong guessing）」の除去**が可能である場合に成立します。これは、推測された新しい値を、入力データ列に既に存在する値に置き換えても言語が変化しない性質を指します（等式原子 $A_=$ や稠密順序原子 $A_<$ はこの条件を満たします）。

B. データ正則式 (Data-Regular Expressions: DRE)

古典的な正則式の精神に則った、最小限の式体系です。

• 構成要素: 量子化なしの領域（quantifier-free regions）から構成されます。
• $k$-contracting 連結 ($E \cdot_k F$): 従来の連結ではなく、長さ $k$ の「オーバーラップ（インターフェース）」を介した連結を導入します。ここで $k$ はレジスタの数です。
  • 定義: $K \cdot_k L = \{ uw \mid \exists v \in (\Sigma \times A)^k, uv \in K, v^R w \in L \}$
  • 直観: 左側の式が $k$ 個のデータ値を「インターフェース」として渡され、右側の式がその値を逆順で受け取って処理を継続することを表現します。これは有限個のレジスタによるデータ値の移動を正確に反映しています。
• 反復: $E^{k,*}$ 演算子も同様に定義されます。

3. 主要な結果（定理）

論文の中心的な結果は、以下の「三位一体（Trinity）」の等価性の確立です。

$$\text{Automata (NRAg)} \equiv \text{Expressions (DRE)} \equiv \text{Logic (Scoped MSO)}$$

1. NRAg と DRE の等価性 (Theorem 5):

   • 任意の有限アルファベット $\Sigma$ と原子 $A$ に対して、NRAg が認識する言語のクラスは DRE で定義される言語と一致します。
   • 証明の要点:
     • $DRE \to NRAg$: $k$-contracting 連結の実現には、オートマトンが非決定的に $k$ 個のデータ値（インターフェース）を推測し、レジスタに格納して、右側の処理を開始する際にその値を逆順で再生成（replay）する機構を用います。
     • $NRAg \to DRE$: 制御フロー（状態遷移）とデータ整合性を分離します。制御フローは通常の正則式で記述し、データ整合性は各遷移を $2k+1$ 長のブロック（レジスタの前後の値と現在の入力値）としてエンコードし、量子化なしの条件でチェックします。

2. NRAg と Scoped MSO の等価性 (Theorem 9):

   • 「強力な推測の除去」が可能である原子 $A$ に対して、NRAg が認識する言語は Scoped MSO で定義可能です。
   • 証明の要点:
     • $MSO \to NRAg$: 論理式を、スコープモダリティを展開し、非局所的なデータ参照を「補助トラック（witness tracks）」を持つ多トラック形式に変換します。その後、局所的なデータテストのみになるように変換し、0 レジスタのオートマトン（有限アルファベット上の MSO）に帰着させます。
     • $NRAg \to MSO$: オートマトンの実行スケルトンを MSO で記述し、レジスタ制約を満たすことを保証するために、ライブ区間ごとに「証人（witness）」となる位置を $\mathcal{X}$ モダリティを用いて選択します。これにより、ネストされた変数を 1 つに抑えつつ、すべての制約を検証します。

3. 決定可能性 (Corollary 10):

   • 強力な推測の除去が可能であれば、Scoped MSO の充足可能性問題は、NRAg の空性判定問題と同値であり、決定可能です。

4. 拡張と特殊ケース

• 無限単語 ($\omega$-words): 結果は Büchi 受理条件を用いることで無限単語へ拡張可能です（Claim 12）。
• 強力な推測が必要な場合: 強力な推測を除去できない原子の場合、論理を拡張して「新しいデータトラック」に対する存在量化（$\exists t[\cdot]$）を追加することで、同様の等価性を維持できます（Section 5.2）。
• 推測なしの NRA: 推測を行わない決定性/非決定的 NRA については、スコープモダリティをより厳格な量化子に置き換えることで記述可能です。

5. 意義と展望

• 記述理論の完成: 無限アルファベットにおけるデータ言語に対して、有限アルファベットの場合と同様の「オートマトン・論理・式」の 3 元対称性を確立しました。
• ツールとしての価値: この論理体系（Scoped MSO）は、データ言語理論における未解決問題へのアプローチに有用です。例えば、Colcombet の「非曖昧レジスタオートマトンによる分離可能性」に関する予想の解決への示唆を与える可能性があります。
• 実用的な形式仕様: DRE は、複雑なバインダを使わずに、古典的な正則式に近い直感的な構文でデータ言語を指定できるため、実用的な仕様言語としての可能性を秘めています。

結論

Radosław Piórkowski によるこの論文は、データ値を扱う計算モデルの理論的基盤を大幅に強化しました。特に、Scoped MSOとData-Regular Expressionsという 2 つの新しい形式体系を提案し、これらが最も一般的な非決定的レジスタオートマトン（NRAg）と表現力において等価であることを示した点が画期的です。これにより、データ言語の解析、検証、合成に対して、論理的・代数的な強力なツールセットが提供されました。