信憑性

▼

この記事を生成 AI が作成した情報を参照しています。調査・学習におけるメモとしての記事になります。本文における正確性や事実であるかどうについてはご自身でご確認ください。特に用語が実際に存在するのか、日本語訳として使われているのかについては判断できかねるので、LLM が生成した用語をそのまま使っています。

はじめに

大学生だったころ MSO Transducers について少しだけ触れたがその実態について直観を得ることができなかった。しかし、今日では LLM によって学習のハードルが下がっているので今であれば理解できるのではないかと思い、改めて調べながら自分の理解できている範囲でメモしつつ学習していく。

一階述語論理 (First-Order Logic, FOL)

一階述語論理では、集合の要素を変数として扱い、量化の対象することができる。ここでは、変数、量化は次の意味で使われる。

• 一階変数 (First-Order variables): $x, y, z, \dots$ のように小文字で表現され、集合の個々の要素を表す
• 量化 (Quantifiers): $\forall$ や $\exists$ を使って「全ての」、「ある」という意味の全称量化子、存在量化子を指す

例として、以下は「すべての $x$ について $y = x + 1$ となるような要素 $y$ が存在する」という述語になる。

$$\forall x \exists y (y = x + 1)$$

ここまでは簡単に理解できる。

単項二階述語論理 (Monadic Second-Order Logic, MSO)

二階述語論理 (Second-Order Logic, SOL) では、要素の「関係」や「関数」を量化の対象とすることができる。 MSO では、量化の対象を単項関係 (Monadic Relation)、すなわち「集合」に限定したものになる。さらに原子論理式 (Atomic formulas) と呼ばれる構造に固有の述語を扱える。

例えば、グラフが 2-彩色可能であることは次の述語で表現される。

$$\exists R \exists B (\forall v (v \in R \lor v \in B)) \land \forall u \forall v ((u, v) \in E \to \lnot ((u \in R \land v \in R) \lor (u \in B \land v \in B)))$$

$R$ (赤、Red)、$B$ (青、Blue) はそれぞれ頂点の集合、$E$ は辺の集合を表している。

いきなり複雑になった。分解して考えてみよう。

• $\exists R \exists B$:
  • ある頂点の集合 $R$、$B$ が存在する
• $\forall (v \in R \lor v \in B)$:
  • すべての頂点 $v$ について $R$ の要素または $B$ の要素
• $\forall u \forall v ((u, v) \in E \to \dots)$:
  • すべての頂点 $u$、$v$ について $(u, v)$ が辺の集合 $E$ の要素ならば…
• $\lnot ((u \in R \land v \in R) \lor (u \in B \land v \in B))$:
  • $u \in R \land v \in R$: 頂点 $u$、$v$ が $R$ に含まれている
  • $u \in B \land v \in B$: 頂点 $u$、$v$ が $B$ に含まれている

ここまで分解したらわかりやすい。確かにこの述語が真になるのはようなグラフは 2-彩色可能になる。

つまり、2-彩色可能なすべてのグラフの集合は MSO で表現できるということだ。

述語でグラフを表現する方法はグラフ理論の講義で学んだ気がするが完全に忘れてしまっていた。 MSO について調べているときもグラフ理論の講義と結びついていなかった。講義では単にグラフを述語を使って表現できるという文脈で紹介され、述語論理という側面でどのようなクラスになっているか考えてなかったように記憶している。

Büchi–Elgot–Trakhtenbrot theorem

文字列上の MSO と正規言語が等価な表現力を持つことを示す定理として Büchi–Elgot–Trakhtenbrot theorem があるらしい。 1960 年に書かれた論文で証明されているようなので古くから知られている定理のようだ。

論理学とオートマトン理論の橋渡しとなる理論のため重要な研究結果だったようだ。オートマトンの基礎について包括的に学習したことがないので知らなかった。やはり Elements of Automata Theory を読むべきか…。

大学生のときに [1706.01668] One-way definability of two-way word transducers を読んで MSO Transducers が出てきたが、そもそも正規言語が MSO で定義可能という事実が知らずに読んでいた。そのため、今読み直したら新しくわかることがあるかもしれないように思う。

Courcelle's Theorem

木幅 (treewidth) が有界なグラフのクラス上では、MSO で記述できる任意の性質は線形時間で判定できる定理は Courcelle's Theorem というらしい。

これは Tree Automaton と関係性がありそうな性質だ。 Gemini の Deep Research を使って調べたところ、文字列上と同様に正規木言語と MSO により表現できる木のクラスは一致するようだ。真偽については後日確かめてみたい。

こうした気になった点を 20 分ほど待てば Web 上を自動で調査して結果を確認できるのは凄い時代だ。自分が学生の頃に欲しかった。

正しい情報であるかは不明だが DeepResarch による調査結果を HTML に変換したものを置いておく。

$k = 4$ や $k = 5$ くらいから驚くほど計算量が増加するのは学部のときに書いた卒論の研究結果と似ていることが思い出される。

MSO Transducers

具体例: 文字列上の変換

アルファベット ${a, b, c}$ 上の文字列を入力として受け取り、$a$ を $b$ に、$b$ を $c$ に、$c$ を $a$ に置き換えるような変換は次の論理式で表せる。

• $L_b'(p') \iff L_a(p)$
• $L_c'(p') \iff L_b(p)$
• $L_a'(p') \iff L_c(p)$

ここで $L_a$、$L_b$、$L_c$ はそれぞれ入力文字列の位置 $p$ について文字が $a$、$b$、$c$ のときに真になる。 $L_a'$、$L_b'$、$L_c'$ は出力文字列の位置 $p'$ について同様の意味を持つ述語とする。 $p$ と $p'$ はそれぞれ入力文字列、出力文字列において同じ位置を指すものとする。

これはかなりカジュアルな定義だが MSO でできることを捉えるには十分だろう。後でより厳密な定義を試みる。

具体例: 補グラフの生成

グラフ $G = (V, E)$ から補グラフ $\overline{G} = (V, \overline{E})$ を出力する変換を考える。補グラフは元のグラフと同じ頂点集合を持ち、元のグラフで辺で結ばれていない頂点間に辺を持つグラフだ。

ここで MSO 変換の入力、出力は次のようになる。

• 入力: グラフ $G = (V, E)$
• 出力: 補グラフ $\overline{G} = (V, \overline{E})$

変換ルール

1. 出力頂点集合の定義:
   • $\forall (v \in V_{\mathrm out} \iff v \in V_{\mathit in})$
   • 出力グラフの頂点集合は入力グラフの頂点集合と同一であることを表現している
2. 出力辺集合の定義:
   • $\forall u \forall v ((u, v) \in E_{\mathit out} \iff u \neq v \land \lnot ((u, v) \in E_{\mathit in}))$
   • 「出力グラフにおいて 2 つの頂点 $u$, $v$ の間に辺が存在する $\iff$ $u$ と $v$ が異なる頂点かつ入力グラフにおいて $u$ と $v$ の間に辺が存在しない」ことを表現している

これらの定義は MSO で書かれているのでグラフから補グラフを生成する変換は MSO 変換として定義できることがわかる。

厳密な定義を見る

最初に MSO の感覚を掴むために見た例は厳密さがあまりにも欠けていた。もう少しばかり形式的な定義で MSO 変換を見てみる。

文字列構造の形式的定義

$\Sigma$-文字列構造 は、タプル $S = \langle D, <, (P_c)_{c \in \Sigma} \rangle$ として定義される。ここで、

• $D$: ドメイン (Domain) と呼ばれる位置 (position) の有限集合。
• $<$: ドメイン $D$ 上の全順序関係 (total order)。
• $(P_c)_{c \in \Sigma}$: ラベル (label) の集合。$c \in \Sigma$ について $P_c$ は $D$ の部分集合で「文字 $c$ が存在する位置の集合」を表す。
  • $P_a(p)$ は「位置 $p$ の文字は $a$ である」ことを意味する。

MSO 変換の形式的定義

MSO 変換 $T$ は、入力構造 $S_{\mathit in}$ から出力構造 $S_{\mathit out}$ への関係として定義される。関係は一つの MSO 論理式 $\varphi_T$ によって指定される。

論理式 $\varphi_T$ は、入力構造 $(D_{\mathit in}, <_{\mathit in}, P_c)$ と出力構造 $(D_{\mathit out}, <_{\mathit out}, P_c')$ によって記述される。

あるペア $(S_{\mathit in}, S_{\mathit out})$ が変換関係 $T$ に属するための必要十分条件は、そのペアが論理式 $\varphi_T$ を満たすこと。

$$(S_{\mathit in}, S_{\mathit out}) \in T \iff (S_{\mathit in}, S_{\mathit out}) \vDash \varphi_T$$

具体例

$a$ を $b$、$b$ を $c$、$c$ を $a$ に置き換える変換についてもう一度考えてみる。今度はより形式的な定義をしてみよう。

最初に入力構造、出力構造を次のように定義する。

• 入力構造: $S_{\mathit in} = \langle D_{\mathit in}, <_{\mathit in}, P_a, P_b, P_c \rangle$
• 出力構造: $S_{\mathit out} = \langle D_{\mathit out}, <_{\mathit out}, P_a', P_b', P_c' \rangle$

次に入力と出力の構造がラベルを無視したとき同型であることを表現する論理式を定義する。

$$\varphi_{\mathit iso} \equiv (D_{\mathit in} = D_{\mathit out}) \land (\forall x \forall y (x <_{\mathit in} y \leftrightarrow x <_{\mathit out} y))$$

これは $D_{\mathit in} = D_{\mathit out}$ で入力ドメインと出力ドメインが等しい (文字列長が同じ) ことと、$forall x \forall y (x <_{\mathit in} y \leftrightarrow x <_{\mathit out} y$ で位置の順序が同じであることを表現している。

ラベル変換規則 $\varphi_{\mathit relabel}$ は次のように定義される。

$$\varphi_{\mathit relabel} \equiv \forall x \in D_{\mathit in} \left( \begin{align*} (P_a(x) \leftrightarrow P_b'(x)) \land \\ (P_b(x) \leftrightarrow P_c'(x)) \land \\ (P_c(x) \leftrightarrow P_a'(x)) \end{align*} \right)$$

すべての入力ラベルの位置について同じ位置に存在するラベルに関して言及している。

最終的に $\varphi_T$ は $\varphi_{\mathrm iso}$ と $\varphi_{\mathrm replabel}$ の連言になる。

$$\varphi_T \equiv \varphi_{\mathit iso} \land \varphi_{\mathit relabel}$$

ここまでの定義によって目的の変換が MSO 論理によって表現できた。

実行例

入力として $abac$ を与えたときの動作を確認してみよう。

1. 入力構造 $S_{\mathit in}$
   • $D_{\mathit in} = \{1, 2, 3, 4\}$
   • $<_{\mathit in} = \{(1, 2), (1, 3), (1, 4), (2, 3), (2, 4), (3, 4)\}$
   • $P_a = \{1, 3\}$, $P_b = \{2\}$, $P_c = \{4\}$
2. 出力構造 $S_{\mathit out}$
   • $D_{\mathit out} = \{1, 2, 3, 4\}$
   • $<_{\mathit out} = <_{\mathit in}$
   • 出力ラベル $P_a'$, $P_b'$, $P_c'$ はラベル変換規則から次のようになる
     • $P_a \leftrightarrow P_b'$: $P_a = \{1, 3\}$ なので $P_b' = \{1, 3\}$
     • $P_b \leftrightarrow P_c'$: $P_b = \{2\}$ なので $P_c' = \{2\}$
     • $P_c \leftrightarrow P_a'$: $P_c = \{4\}$ なので $P_a' = \{4\}$

出力構造 $S_{\mathit out}$ を文字列として解釈すると $bcba$ が得られる。

個人的にはこれにより変換が定義できることは少しばかり奇妙な感覚があるが、Prolog でプログラムを書くのに似ているように感じた。

MSO も一枚岩ではない

一言に MSO をいってもどうやら複数のバリーションがあるようだ。 MSO の定義を見ると論理式を定義するときに使える述語を増やすことで定義できる変換が変わってくることがわかる。

グラフを対象とする場合、二つの頂点間が辺を持つか否か $\mathit{adj}(u, v)$ を扱える $\mathrm{MSO}_1$、頂点に対して辺が存在するか $\mathit{inc}(v, e)$ を扱える $\mathrm{MSO}_2$、集合 $X$ の要素数が法 $q$、$p$ に関して合同であるかを判定する $\mathit{card}_{p,q}(X)$ を扱える $\mathrm{CMSO}$、与えられた MSO の性質を満たす集合の最小または最大サイズを求める述語を追加した拡張 $\mathrm{MSO}$ ($\mathrm{EMSO}$) / $\mathrm{LinEMSOL}$ のような複数の拡張があるようだ。

おわりに

MSO Transducers について具体例を交えつつ確認した。何かしらの構造や変換を考えるとき、どうしても構成的な方法を想像してしまうので構造を定義し、その構造上の論理式によって変換や構造そのものを表現する方法はやはり手に馴染まない。恐らく証明の一部として示されているであると思うが、構成的な定義から論理式による定義への変換を一度なぞってみないと定義したい変換を思うように定義するのが難しいように感じる。 2-彩色可能や補グラフへの変換のような性質が明確なものであれば論理式による定義が自然に思い浮かばれるが、そうではない自由な変換をしたい場合は難しいだろう。

次は、この記事内で触れた定理の証明や関連する理論について調べていこうと思う。

記事履歴

作成: 2025年6月22日

更新履歴（直近1件）

feat: add post about MSO Transducers

SuzumiyaAoba2025/6/22 06:50f1970f1