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

単一化アルゴリズム(自由モノイド版)

単一化アルゴリズムをモノイドで表すことを考えます。

自由モノイド

集合 $A$ に対して $A^k$ を $k$ 個の $A$ の直積、 $+$ を集合の直和とすると $A^* = 1 + A + A^2 + A^3 + \cdots$ は $A$ で自由生成された(「文字列の連結」を演算とする)モノイドとなります( $1$ は「空文字列」)。 $A^*$ は簡約可能、すなわち(演算子を省略して書くと)

$xy = xz \implies y = z$
$xz = yz \implies x = y$

が成り立ちます。

生成要素の文字列

有限個の変数を表す文字の集合 $X$ と有限個の定数・関数を表す文字の集合 $C$ の集合の直和 $X + C$ で自由生成されたモノイドを $M$ とおきます( $M = (X + C)^*$ )。演算子を $\cdot$ と書きます(または省略します)。単位元を $1$ と書きます。すなわち

$M = \{r_1 \cdots r_l \mid r_1, \cdots, r_l \in X + C, l \in \mathbb{N}\}$

( $\mathbb{N} = \{0, 1, 2, \cdots\}$ )と定義します。 $C$ の元にある( $0$ 以上の)自然数(項数)が対応しているとします。項数 $n$ の $C$ の元全体を $C_n$ とおきます。 $C = C_0 + C_1 + C_2 + \cdots$ となります。 $C_+ = C_1 + C_2 + \cdots$ とおきます。

生成要素の文字列の長さ

$s = r_1 \cdots r_l \in M$ ( $r_1, \cdots, r_l \in X + C$ )に対して

$l$ を $\mathop{\mathrm{len}}(s)$
$r_i \in X + C$ を $s[i]$
$r_i \cdots r_j \in M$ を $s[i \cdots j]$
$r_i \cdots r_l \in M$ を $s[i \cdots]$
$r_1 \cdots r_j \in M$ を $s[\cdots j]$

と書くことにします。

項

$M$ の部分集合(または $M$ の元。この場合はその一つの元からなる集合を表すとします) $A_1, A_2$ に対して $\{a_1 \cdot a_2 \mid a_1, a_2 \in A\}$ を $A_1 \cdot A_2$ (または $A_1A_2$ )と書くことにします( $M$ の元の場合はその一つの元からなる集合を表すとします)。
$M$ の部分集合(または $M$ の元。この場合はその一つの元からなる集合を表すとします) $A_1, \cdots, A_n$ に対して $\{a_1 \cdots a_n \mid a_1 \in A_1, \cdots, a_n \in A_n\}$ を $A_1 \cdots A_n$ と書くことにします。
$M$ の部分集合 $A$ に対して $\{a_1 \cdots a_n \mid a_1, \cdots, a_n \in A\}$ を $A^n$ と書くことにします。

$T$ を

$X \subseteq T$
任意の $n \in \mathbb{N}$ に対して $C_n \cdot T^n \subseteq T$

を満たす最小の集合とします。 $T$ は

$T_0 = X$
$\displaystyle T_{k+1} = \bigcup_{n \in \mathbb{N}} C_n \cdot T_k^n$
$\displaystyle T = \bigcup_{k \in \mathbb{N}} T_k$

と帰納的に定義することができます。 $T$ の元を項と呼びます。

$s \in M$ に対して最初の項を求める「形式的写像」 $f(s)$ を

(1) $s \in x \cdot M, \ x \in X$ のとき $x$
(2) $s \in c \cdot M, \ c \in C_0$ のとき $c$
(3) のとき
- ここで $t_i$ は $s = c \cdot t_1 \cdots t_i \cdot w_i$ のとき $t_{i+1} = f(w_i)$ と帰納的に定義します。ある $t_i$ が $t_i = \bot$ となったときは、 $c \cdot t_1 \cdots t_n = \bot$ とします(この後の $t_{i+1}, t_{i+2}, \cdots$ は無視します)。
(4) $s = 1$ のとき $\bot$

と定義します。これは $f_k(s)$ を

(k1) $s \in x \cdot M, \ x \in X$ のとき $x$
(k2) $s \in c \cdot M, \ c \in C_0$ のとき $c$
(k3) のとき
- $t_i$ は $s = c \cdot t_1 \cdots t_i \cdot w_i$ のとき $t_{i+1} = f_{k+1}(w_i)$ と帰納的に定義します。ある $t_i$ が $t_i = \bot$ となったときは、 $c \cdot t_1 \cdots t_n = \bot$ とします(この後の $t_{i+1}, t_{i+2}, \cdots$ は無視します)。
(k4) $s = 1$ のとき $\bot$

と定義し、 $f=f_0, f_1, f_2, \cdots$ を合成したものを表すとします。

$s \in M$ に対して $f_k$ が(k3)にならない $k$ が存在すれば $f_k$ を(k3)で $f_{k+1}$ を呼び出さない $f'_k$ で置き換えて $f'=f_0, f_1, f_2, \cdots, f_{k-1}, f'_k$ を合成した「部分写像」を $f'$ としたとき $f(s) = f'(s)$ であるとします。 $f'_k(s)$ は以下のように定義します。

(k1') $s \in x \cdot M, \ x \in X$ のとき $x$
(k2') $s \in c \cdot M, \ c \in C_0$ のとき $c$
(k3') $s \in c \cdot M, \ c \in C_+$ のとき $\bot$
(k4') $s = 1$ のとき $\bot$

(T1) $f$ は $M$ から $M + \{\bot\}$ への写像

[証明] (k3)のとき $\mathop{\mathrm{len}}(s) > \mathop{\mathrm{len}}(t_i)$ となります。 $\mathop{\mathrm{len}}(s)$ は有限なので(k3)が無限に繰り返されることはありません。よってある $f_k$ で(k3)にはなりません。よって $s \in M$ を決めると $k$ が決まり、 $f(s)$ が決まります。よって $f$ は $M$ から $M + \{\bot\}$ への写像となります。[証明終わり]

(T2) $s \in M$ ならば $f(s) = \bot$ または $s \in f(s) \cdot M$

[証明] $f(s)$ の定義より
(1)のとき $s \in x \cdot M = f(s) \cdot M$ となります。
(2)のとき $s \in c \cdot M = f(s) \cdot M$ となります。
(3)のとき $t_i$ がどれも $\bot$ でなければ $s \in c \cdot t_1 \cdots t_n \cdot M = f(s) \cdot M$ となります。
(4)のとき $f(s) = \bot$ となります。
よって $f(s) = \bot$ または $s \in f(s) \cdot M$ となります。[証明終わり]

(T3) $s, u \in M$ ならば $f(s) = \bot$ または $f(s \cdot u) = f(s)$

[証明] $f(s)$ の定義より
(1)のとき $s = x \cdot w$ を満たす $w \in M$ が存在します。 $f(s) = x = f(s \cdot u)$ が成り立ちます。
(2)のとき $s = c \cdot w$ を満たす $w \in M$ が存在します。 $f(s) = c = f(s \cdot u)$ が成り立ちます。
(3)のとき $t_i$ がどれも $\bot$ でなければ $s = c \cdot t_1 \cdots t_n \cdot w_n$ となります。 $f(s) = c \cdot t_1 \cdots t_n = f(s \cdot u)$ が成り立ちます。
(4)のとき $f(s) = \bot$ となります。
よって $f(s) = \bot$ または $f(s \cdot u) = f(s)$ となります。[証明終わり]

(T4) $s \in M$ ならば $f(s) = \bot$ または $f(s) \in T$

[証明] $\mathop{\mathrm{len}}(t) = k$ で、 $\mathop{\mathrm{len}}(u) < k$ のとき $f(u)$ が $\bot$ でなければ $f(u) \in T$ と仮定します。
(1)のとき $f(t) = x \in T$ となります。
(2)のとき $f(t) = c \in T$ となります。
(3)のとき $t_i$ がどれも $\bot$ でなければ $f(t) = c \cdot t_1 \cdots t_n = c \cdot f(w_0) \cdots f(w_{n-1}) \in C_n \cdot T^n \subseteq T$ となります。
(4)のとき $f(s) = \bot$ となります。
よって $f(s) = \bot$ または $f(s) \in T$ となります。[証明終わり]

(T5) $t \in M$ のとき $t \in T \iff f(t) = t$

[証明] まず $t \in T$ のとき $f(t) = t$ であることを帰納的に示します。

$t \in T_0$ のときは $t \in X$ なので $f(t) = t$ は成り立ちます。

$t \in T_k$ のとき $f(t) = t$ と仮定します。 $t \in T_{k+1}$ をとります。ある $n$ に対して $t \in C_n \cdot T_k^n$ となります。 $t = c \cdot t_1 \cdots t_n$ ( $t_1, \cdots, t_n \in T_k$ )とおきます。帰納法の仮定から $f(t_i) = t_i$ ( $i = 1, 2, \cdots, n$ )が成り立ちます。

$t = c \cdot t_1 \cdots t_i \cdot w_i$ ( $w_i = t_{i+1} \cdots t_n$ )とおくと(T3)から $f(w_i) = f(t_{i+1} \cdots t_n) = f(t_{i+1}) = t_{i+1}$ となって、帰納的に $f(t) = c \cdot t_1 \cdots t_n = t$ が成り立ちます。

逆に $f(t) = t$ のとき(T4)より $t = f(t) \in T$ が成り立ちます。[証明終わり]

代入

$\sigma: X \to T$ に対して $\sigma^+: X + C \to T + C$ を
$\sigma^+(r) = \begin{cases} \sigma(r) & (r \in X \ のとき) \\ \overline{r} & (r \in C \ のとき) \\ \end{cases}$
とおきます。 $\overline{\sigma}: T \to T$ を

$\overline{\sigma}(r_1 \cdots r_n) = \sigma^+(r_1) \cdots \sigma^+(r_n)$ ( $r_1, \cdots, r_n \in X + C$ )

と定義します。

このような写像の有限個の合成(恒等写像を含む)を代入と呼びます。代入の全体を $\Sigma$ とおきます。

変数 $x$ に $x$ を含まない項 $t$ を対応させる写像を、 $T$ から $T$ への写像に拡張したものを $(x \mapsto 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$ は写像)。

「 $\varphi$ で写したもの」を $\psi$ で写す写像を $\varphi \to \psi$ と書くことにします。

(S1) $t \in T$ のとき $\overline{\sigma}(t) \in T$

[証明]
$t \in T_0$ のときは $t \in X$ なので代入の定義から $\overline{\sigma}(t) \in T$ となります。

$t \in T_k$ のとき $\overline{\sigma}(t) \in T$ と仮定します。 $t \in T_{k+1}$ をとります。ある $n$ に対して $t \in C_n \cdot T_k^n$ となります。 $t = c \cdot t_1 \cdots t_n$ ( $t_1, \cdots, t_n \in T_k$ )とおきます。帰納法の仮定から $\overline{\sigma}(t_i) \in T$ ( $i = 1, 2, \cdots, n$ )が成り立ちます。

$\overline{\sigma}(t) = \overline{\sigma}(c \cdot t_1 \cdots t_n) = c \cdot \overline{\sigma}(t_1) \cdots \overline{\sigma}(t_n) \in C_n \cdot T^n \subseteq T$

となります。[証明終わり]

(S2) $s \in M$ のとき $f(s) = \bot$ または $\overline{\sigma}(f(s)) = f(\overline{\sigma}(s))$

[証明] $f(s)$ の定義より
(1)のとき $s = x \cdot w$ を満たす $x \in X$ と $w \in M$ が存在し $f(s) = x$ となります。
$\overline{\sigma}(f(s)) = \overline{\sigma}(x) = \sigma(x)$
$f(\overline{\sigma}(s)) = f(\overline{\sigma}(x \cdot w)) = f(\sigma(x) \cdot \overline{\sigma}(w))$
よって $\sigma(x) \in T$ なので(T3)より $f(\sigma(x) \cdot \overline{\sigma}(w)) = \sigma(x)$ が成り立ちます。

(2)のとき $s = c \cdot w$ を満たす $c \in C_0$ と $w \in M$ が存在し $f(s) = c$ となります。
$\overline{\sigma}(f(s)) = \overline{\sigma}(c) = c$
$f(\overline{\sigma}(s)) = f(\overline{\sigma}(c \cdot w)) = f(c \cdot \overline{\sigma}(w))$
よって $c \in T$ なので(T3)より $f(c \cdot \overline{\sigma}(w)) = c$ が成り立ちます。

(3)のとき $t_i$ がどれも $\bot$ でなければ $s = c \cdot t_1 \cdots t_n \cdot w$ を満たす $c \in C_n$ と $w \in M$ と $t_1, \cdots, t_n \in T$ が存在し $f(s) = c \cdot t_1 \cdots t_n$ となります。
$\overline{\sigma}(f(s)) = \overline{\sigma}(c \cdot t_1 \cdots t_n)$
$f(\overline{\sigma}(s)) = f(\overline{\sigma}(c \cdot t_1 \cdots t_n \cdot w)) = f(\overline{\sigma}(c \cdot t_1 \cdots t_n) \cdot \overline{\sigma}(w))$
よって $c \cdot t_1 \cdots t_n \in T$ なので(S1)より $\overline{\sigma}(c \cdot t_1 \cdots t_n) \in T$ となり、(T3)より $f(\overline{\sigma}(c \cdot t_1 \cdots t_n) \cdot \overline{\sigma}(w)) = \overline{\sigma}(c \cdot t_1 \cdots t_n)$ が成り立ちます。

(4)のとき $f(s) = \bot$ となります。

よって $\overline{\sigma}(f(s)) = f(\overline{\sigma}(s))$ となります。[証明終わり]

(S3) $s, u \in M$ のとき $f(s) \ne \bot$ 、 $f(u) \ne \bot$ 、 $\overline{\sigma}(s) = \overline{\sigma}(u)$ ならば $\overline{\sigma}(f(s)) = \overline{\sigma}(f(u))$

[証明] (S2) より $\overline{\sigma}(f(s)) = f(\overline{\sigma}(s)) = f(\overline{\sigma}(u)) = \overline{\sigma}(f(u))$ となります。[証明終わり]

不一致集合

$S$ を $T$ の空ではない有限部分集合とします。

$i = 1, 2, \cdots$ に対して

$e(S, i) \iff$ 任意の $t \in S$ に対して $i \le \mathop{\mathrm{len}}(t)$ ( $i \le \min\{\mathop{\mathrm{len}}(t) \mid t \in S\}$ )
$n(S, i) \iff$ $e(S, i)$ かつすべての $t \in S$ の $t[i]$ が一致しない( $e(S, i) \land \#\{t[i] \mid t \in S\} > 1$ )

とおきます。最初の一致しない位置 $p(S)$ を

$n(S, i)$ が成り立つ $i$ が存在する( $\{i \mid n(S, i)\} \ne \varnothing$ )とき $n(S, i)$ が成り立つような $i$ の最小値( $p(S) = \min\{i \mid n(S, i)\}$ )
$n(S, i)$ が成り立つ $i$ が存在しない( $\{i \mid n(S, i)\} = \varnothing$ )とき $p(S) = \bot$

とおきます。

定義(不一致集合)

$S$ を $T$ の有限部分集合とします。不一致集合 $D(S)$ を

$n(S, i)$ が成り立つ $i$ が存在する( $\{i \mid n(S, i)\} \ne \varnothing$ )とき $D(S) = \{ f(t[p(S)\cdots]) \mid t \in S\}$
$n(S, i)$ が成り立つ $i$ が存在しない( $\{i \mid n(S, i)\} = \varnothing$ )とき $D(S) = \varnothing$ (空集合)

とおきます。

単一化アルゴリズム

単一化アルゴリズム(自由モノイド版) UAG

$S$ を $T$ の有限部分集合とします。まず $S$ が空集合ではないとき以下の「形式的写像」 $u(S, \theta)$ を定義します。
$u(S, \theta) =$

(1) $S\theta$ が一つの項からなるとき $\theta$
そうではないとき
- (2) がとを含むとき (以下を満たす任意のもの)
  - $x$ は変数
  - $t$ は $x$ が出現しない項
  - $\sigma = (x \mapsto t)$
  - $\theta'= \theta \to \sigma$
- (3) そうではないとき $\bot$

最初の項を求める「部分写像」 $f$ の場合と同様に、「形式的写像」 $u(S, \theta)$ を「部分写像」に変換します。この「部分写像」をここではアルゴリズムと呼びます。

$f$ の場合と同様に、無限個の写像の合成のような形に書き換えます。 $\theta$ も $\theta_k$ で置き換えて $u_k(S, \theta_k)$ とします。
$u_k(S, \theta_k) =$

(k1) $S\theta_k$ が一つの項からなるとき $\theta_k$
そうではないとき
- (k2) がとを含むとき (以下を満たす任意のもの)
  - $x_k$ は変数
  - $t_k$ は $x_k$ が出現しない項
  - $\sigma_k = (x_k \mapsto t_k)$
  - $\theta_{k+1}= \theta_k \to \sigma_k$
- (k3) そうではないとき $\bot$

(k2)を置き換えた $u'_k(S, \theta_k)$ も以下のように定義します。
$u'_k(S, \theta_k) =$

(k1') $S\theta_k$ が一つの項からなるとき $\theta_k$
(k2') そうではないとき $\bot$

$T$ の有限部分集合 $S$ に対して $u_k$ が(k3)にならない $k$ が存在すれば $u_k$ を $u'_k$ で置き換えて $u'=u_0, u_1, u_2, \cdots, u_{k-1}, u'_k$ を合成した「部分写像」 $u'$ として $u$ を定義することができます。

恒等写像を $1$ と書きます。 $u(S) = u_0(S, 1)$ とします。 $S$ が空集合のときは $u(S) = 1$ (恒等写像)とします。

定義 (単一化代入)

項の集合 $S$ に対して $S\theta$ の元の個数が $1$ となるような代入 $\theta$ を $S$ の単一化代入と呼びます。

$F(M)$ を $M$ の有限部分集合全体とします。

(UAGの停止性) $u$ は $F(M)$ から $\Sigma + \{\bot\}$ への写像

[証明] (k2)のとき $S\theta_{k+1}$ に現れる変数の個数は $S\theta_{k}$ に現れる変数の個数より少なくなります。 $S$ に現れる変数の個数は有限なので(k2)が無限に繰り返されることはありません。よって $T$ の有限部分集合 $S$ を決めると $k$ が決まり、 $u(S)$ が決まります。よって $u$ は $F(M)$ から $\Sigma + \{\bot\}$ への写像となります。[証明終わり]

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

[証明] (UAGの停止性)よりある $k$ が存在して(k1)で $u(S) = \theta_k$ となるか、または $u(S) = \bot$ となります。 $u(S) \in Σ$ から $u(S) = \bot$ にはならないので $u(S)$ は $S$ の単一化代入となります。[証明終わり]

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

(UAG2) $\tau$ が $S$ の単一化代入ならば $\tau$ は $D(S)$ の単一化代入

[証明] $D(S)$ が空集合ではないとします。 $\tau(u) = \tau(v), u[p(S)] \ne v[p(S)]$ を満たす $u, v \in S$ をとります。
$u_1 = u[\cdots p(S)-1], u_2 = u[p(S)\cdots]$
$v_1 = v[\cdots p(S)-1], v_2 = v[p(S)\cdots]$
とおくと $u = u_1 \cdot u_2$ 、 $v = v_1 \cdot v_2$ となります。
$\tau(u) = \tau(u_1 \cdot u_2) = \tau(u_1) \cdot \tau(u_2)$
$\tau(v) = \tau(v_1 \cdot v_2) = \tau(v_1) \cdot \tau(v_2)$
$\tau(u) = \tau(v)$ 、 $\tau(u_1) = \tau(v_1)$ より $\tau(u_2) = \tau(v_2)$ となり、(S3)より $\tau(f(u_2)) = \tau(f(v_2))$ が成り立ちます。[証明終わり]

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

[証明] (UAGの停止性)より $u$ は $F(M)$ から $\Sigma + \{\bot\}$ への写像となります。よって $u(S) \in Σ$ または $u(S) = \bot$ となります。

アルゴリズム UAG の $\theta_k$ について、 $\theta_k \in Σ$ かつ $\theta_k \le τ$ であることを帰納的に示します。

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

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

(k1)ではないとき $\theta_k \le \tau$ より $\theta_k \to \tau_k = \tau$ を満たす $\tau_k$ が存在します。 $\tau_k$ は $S\theta_k$ の単一化代入となります。(UAG2)より $\tau_k$ は $D(S\theta_k)$ の単一化代入となります。 $x, t \in D(S\theta_k)$ 、 $x \ne t$ をとることができ、 $\tau_k(x) = \tau_k(t)$ となるので $x, t$ のどちらかは変数となります。 $x$ を変数とすると、 $t$ は $x$ を含まない項となります。よって(k2)が成り立ちます。

$x, t$ をこのような任意のものとし、 $\sigma_{k} = (x \mapsto t)$ 、 $\theta_{k+1} = \theta_k \to \sigma_k$ とおくと、 $\tau_k(\sigma_k(x)) = \tau_k(t) = \tau_k(x)$ 、 $y$ が $x$ ではない変数のとき $\tau_k(\sigma_k(y)) = \tau_k(y)$ が成り立つので $\sigma_k \le \tau_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$ が成り立ちます。