単一化アルゴリズム(1) - 非専門的シンギュラリティー研究所

エレファントな群とリー代数(10) - エレファント・ビジュアライザー調査記録で説明した単一化アルゴリズムがわかりにくいので書き直します。

『数理論理学: 合理的エ-ジェントへの応用に向けて』の「定理 4.1 (単一化定理)」の証明について、(この本には書かれていないので)参照する本に『計算論理に基づく推論ソフトウェア論』があります。『計算論理に基づく推論ソフトウェア論』の「定理 3.3」に当たります。単一化アルゴリズムの定義も『数理論理学: 合理的エ-ジェントへの応用に向けて』と『計算論理に基づく推論ソフトウェア論』では少し違うようです。

この証明のわかりにくいところを構造に関する帰納法を使って書き直したものがエレファントな群とリー代数(11) - エレファント・ビジュアライザー調査記録に書いた証明です。

構造についてはエレファントな群とリー代数(10) - エレファント・ビジュアライザー調査記録で書いた構造を使って、それを一段階ずつ進めるように書き直したものがエレファントな群とリー代数(11) - エレファント・ビジュアライザー調査記録に書いた証明なのですが、見たところわかりにくいので今回書き直してみたいと思います。

ある決まった構造を持つ項を考えます。ここではこれを単に項と呼ぶことにします。このブログでは「一般マグマの多項式」と呼んでいたのですが、このブログだけの用語なのでここでは使いません。一般的な用語は「一階の項」のようです。

項全体を $T$ とおきます。変数 $x$ に $x$ を含まない項 $t$ を対応させる写像を、 $T$ から $T$ への写像に拡張したものを $(x \mapsto t)$ と書くことにします(これはこのブログだけの記法です)。このような写像の有限個の合成を代入と呼びます。 $0$ 個の合成(恒等写像)は $\epsilon$ と書くことにします。

『数理論理学: 合理的エ-ジェントへの応用に向けて』、『計算論理に基づく推論ソフトウェア論』では代入は集合のような記法 $\{t/x\}$ と表されています。このブログではこれは写像として扱います。多項式の代入が多項式全体から多項式全体への写像であるのと同様の考え方です。(演算の制約について議論するのではなく)代入について議論するときの一般的な用語がおそらくないので、このブロクではこのような構造を「一般マグマの多項式」と呼んでいます。『数理論理学: 合理的エ-ジェントへの応用に向けて』、『計算論理に基づく推論ソフトウェア論』では論理式について議論しているので写像や代数的構造などは扱わないのかもしれませんが、集合やアルゴリズムは使っているのでそのあたりはよくわかりません。

写像 $\varphi$ と $\psi$ の合成を $\varphi \circ \psi$ と書きます( $(\varphi \circ \psi)(t) = \varphi(\psi(t))$ )。逆方向の合成を $\varphi \to \psi$ と書きます( $(\varphi \to \psi)(t) = \psi(\varphi(t))$ 、これはこのブログだけの記法です)。

項 $t$ を写像 $\varphi$ で写した像を $t\varphi$ と書きます( $t\varphi = \varphi(t)$ )。項の集合 $S$ の各元を写像 $\varphi$ で写した像全体を $S\varphi$ と書きます( $S\varphi = \{\varphi(t) \mid t \in S\}$ )。 $(t\varphi)\psi$ を $t\varphi\psi$ 、 $(S\varphi)\psi$ を $S\varphi\psi$ と書きます( $\varphi, \psi$ は写像)。

アルゴリズム UAP

説明のため『計算論理に基づく推論ソフトウェア論』のアルゴリズム 3.1 に番号をつけます( $u = u_0$ とします)。

$u_k(S) \Leftarrow$	$\mathop{\mathbf{if}}$		$S$ が単一の項からなる
	$\mathop{\mathbf{then}}$		$\epsilon$	( $k$ -1)
	$\mathop{\mathbf{else}}$	$\mathop{\mathbf{if}}$	(*) $D(S)$ が $x_k$ と $t_k$ を含む
			$x_k$ は変数
			$t_k$ は $x_k$ が出現しない項
		$\mathop{\mathbf{then}}$	$u_{k+1}(S\sigma_k) \circ \sigma_k$	( $k$ -2)
			( $\sigma_k = (x_k \mapsto t_k)$ )
		$\mathop{\mathbf{else}}$	$\bot$	( $k$ -3)

(*) $D(S)$ は以下のようなものとします。

項は変数、定数、関数の形式で構成されるとします。項をポーランド記法で書きます。これは項を、項に現れる変数はその記号、定数はその記号、関数の形式は関数の記号の後に各引数を変換した文字列を並べた形式に変換した文字列です。この記法の各文字は、その文字を先頭とする部分項に対応しています。変数の記号、定数の記号、関数の記号をその部分項の指標と呼ぶことにします。ポーランド記法は各部分項の指標を並べた文字列となります。これを項の指標文字列と呼ぶことにします。これに対応する部分項の列を、項の部分項列と呼ぶことにします。

$S$ に属する各項の指標文字列を先頭から見ていって、最初に共通しない記号が見つかったとき、その位置を $p(S)$ とします。各項の対応する部分項列の $p(S)$ の位置の部分項全体の集合を $D(S)$ とおきます。

定義 (単一化代入)

項はこのような指標文字列で表されているとします。項の集合 $S$ に対して $S\theta$ の元の個数が $1$ となるような代入 $\theta$ を $S$ の単一化代入と呼びます。

(UAP1) $u(S) \in Σ$ ならば $u(S)$ は $S$ の単一化代入

[証明] $S$ に属する各項に含まれるすべての変数の集合の元の個数を $m(S)$ とおきます。

( $k$ -2)のとき $\theta_{k+1} = \theta_k \to \sigma_k$ と帰納的に定義すると、 $m(S)$ は有限で $m(S) > m(S\theta_1) > m(S\theta_2) > \cdots$ が成り立つので、ある $u_n$ では( $n$ -2)になることはありません。よって $u_n$ で終了します。

$n$ に関する帰納法により $u_n(S)$ が $S$ の単一化代入であることを示します。

$n = 0$ のとき $u(S) = u_0(S) = \epsilon$ は $S$ の単一化代入となっています。

$n > 0$ として $\theta_1 = u_1(S\sigma_0)$ が $S\sigma_0$ の単一化代入と仮定します。 $\theta = u(S) = u_0(S)$ とおくと $S\theta = S\sigma_0\theta_1$ の元の個数は $1$ となります。よって $\theta$ は $S$ の単一化代入となります。

帰納法により $u(S)$ が $S$ の単一化代入であることが示されました。[証明終わり]

$\sigma, \tau \in \Sigma$ に対して $\sigma \to \psi = \tau$ となる代入 $\psi$ が存在するとき $\sigma \le \tau$ と書くことにします。 $\le$ は前順序となります。

(UAP2) $\tau$ が $S$ の単一化代入ならば( $0$ -1)または( $0$ -2)の場合になり、( $0$ -2)の場合は $\sigma_0 \le τ$ が成り立つ

[証明] ( $0$ -2)または( $0$ -3)の場合、位置 $p(S)$ の指標が異なる $a, b \in S$ が存在します。その指標をそれぞれ $\alpha, \beta$ とおきます。代入 $\tau$ により、 $a$ の位置 $p(S)$ より前の指標文字列と $b$ の位置 $p(S)$ より前の指標文字列は $\tau$ によって同じものに変化します。よって変化後の文字列の長さは一致します。位置 $p(S)$ の変化後の位置も一致します。この位置を $p'$ とおきます。

$\alpha, \beta$ から始まる項は $\tau$ で変換されて位置 $p'$ から始まる項になります。 $\tau$ が $S$ の単一化代入であることから変換後の位置 $p'$ の指標は一致します。 $\alpha, \beta$ が変数でなければ $\tau$ による変換で保存されるので、どちらかは変数である必要があります。よって( $0$ -2)の場合となります。

( $0$ -2)の場合の $\sigma_0 = (x_0 \mapsto t_0)$ について $x_0\tau = t_0\tau$ でなければなりません。よって $x_0\sigma_0\tau = t_0\tau = x_0\tau$ が成り立ちます。また、 $y$ を $x_0$ 以外の変数とすると $y\sigma_0\tau = y\tau$ が成り立ちます。よって任意の変数に対して $\sigma_0 \to \tau$ と $\tau$ が写す先は同一のものとなるので $\sigma_0 \to \tau = \tau$ が成り立ちます。よって $\sigma_0 \le \tau$ が成り立ちます。[証明終わり]

(UAP3) $\tau$ が $S$ の単一化代入ならば $u(S) \in Σ$ かつ $u(S) \le τ$

[証明] アルゴリズム UAP が $u_n$ で停止したとします。 $\theta_k = \sigma_{0} \to \sigma_{1} \to \cdots \to \sigma_{k-1}$ とおくと $\theta_0 = \epsilon \le \theta_1 \le \cdots \le \theta_n$ となります。 $\theta_n \in Σ$ かつ $\theta_n \le τ$ であることを帰納的に示します。

$\theta_0 \in Σ$ かつ $\theta_0 \le τ$ は成り立っています。

$k < n$ とし、 $\theta_k \in Σ$ かつ $\theta_k \le τ$ であると仮定します。

$u_{k}(S\theta_k)$ が( $k$ -1)の場合は、 $k=n$ の場合なので、 $k < n$ のときは起こりません。

$u_{k}(S\theta_k)$ が( $k$ -2)または( $k$ -3)の場合を考えます。 $\theta_k \le \tau$ より $\theta_k \to \tau_k = \tau$ を満たす $\tau_k$ が存在します。 $\tau_k$ は $S\theta_k$ の単一化代入となります。

(UAP2)を $\tau_k$ と $S\theta_k$ に適用します。(UAP2)の $\sigma_0$ が存在するとき、その $\sigma_0$ を $d(\tau, S)$ と書くことにすると、 $\sigma_k = d(\tau_k, S\theta_k)$ が成り立ち、 $\theta_k \to \sigma_k \le \theta_k \to \tau_k$ となります。よって $\theta_{k+1} = \theta_k \to \sigma_k \le \theta_k \to \tau_k = \tau$ が成り立ちます。