[ English | Japanese ]

停止性

（筆・齊藤 哲平、加筆・廣川）

1. 停止性とは

プログラムを実行した際、計算が止まらず応答しなくなってしまうことがありますが、 これはプログラムの「停止性」が欠如していることによって引き起こされる現象です。 この記事では停止性を証明する手法のうちの一つを紹介し、 その手法を実際にツールとして実装することを目標にします。

プログラムを項書換え系としてモデル化したとき、その停止性は以下のように数学的に定義できます。

定義（項書換え系の停止性）

項書換え系 $\RR$ が停止性を持つとは、無限の書き換え列 $t_0 \to_\RR t_1 \to_\RR t_2 \to_\RR \cdots$ が存在しないことである。

例（リストの連接）

シグネチャ $\{ \m{cons}^{(2)}, \m{append^{(2)}}, \m{nil^{(0)}} \}$ 上の項書換え系を考える。 \begin{align} \m{append}(\m{nil}, \mi{ys}) & \to \mi{ys} \\ \m{append}(\m{cons}(x, \mi{xs}), \mi{ys}) & \to \m{cons}(x, \m{append}(\mi{xs}, \mi{ys})) \end{align} この項書換えシステムは停止性を持つ。

例（足し算）

シグネチャ $\{ \m{add}^{(2)}, \m{s}^{(1)}, \m{0}^{(0)} \}$ 上の項書換え系を考える。 \begin{align} \m{add}(\m{0}, y) & \to y \\ \m{add}(\m{s}(x), y) & \to \m{s}(\m{add}(x, y)) \\ \m{add}(\m{add}(x, y), z) & \to \m{add}(x, \m{add}(y, z)) \end{align} この項書換えシステムは停止性を持つ。

停止性を持たないことは無限の書き換え列を見つけることで証明できます。

例（停止性を持たない項書換え系）

一つの規則からなる項書換え系 $\RR = \{\, \m{f}(x) \to \m{f}(\m{f}(x)) \,\}$ は 無限の書き換え列 \[ \m{f}(x) \to_\RR \m{f}(\m{f}(x)) \to_\RR \m{f}(\m{f}(\m{f}(x))) \to_\RR \cdots \] を持つ。したがって停止性を持たない。

2. 多項式解釈による停止性証明

リストの連接や足し算の項書換え系は停止性を持ちます。 無限列の書き換え列が存在しないことはどうすれば証明できるのでしょうか？ まずはそのための道具立てを用意します。

定義（自然数上の代数、付値、単調性）

シグネチャ $\FF$ 上の代数 $\AA$ は各関数記号 $f^{(n)} \in \FF$ に解釈関数 $f_\AA : \NN^n \to \NN$ を割り当てるものである。 また変数から自然数への関数を付値と呼ぶ。 代数 $\AA$ と付値 $\alpha$ における項 $t$ の解釈 $[\alpha]_\AA(\cdot)$ を次の再帰関数で定める。 \[ [\alpha]_\AA(t) = \begin{cases} \alpha(t) & \text{$t$ が変数のとき} \\ f_\AA([\alpha]_\AA(t_1),\ldots,[\alpha]_\AA(t_n)) & \text{$t = f(t_1,\ldots,t_n)$ のとき} \end{cases} \] また関数 $\phi : \NN^n \to \NN$ が（狭義）単調であるとは、任意の $x_1, \ldots, x_n, y \in \NN$ と $1 \leqslant i \leqslant n$ に対して、 \[ x_i > y \implies \phi(x_1, \ldots, x_i, \ldots, x_n) > \phi(x_1, \ldots, y, \ldots, x_n) \] を満たすことを言う。 単調な解釈関数からなる代数を単調代数と呼ぶ。

例（単調代数と付値）

シグネチャ $\{ \m{append}^{(2)}, \m{cons}^{(2)}, \m{nil}^{(0)} \}$ 上の代数 $\AA$ を \begin{align*} \m{append}_\AA(x, y) & = 2x + y + 1 & \m{cons}_\AA(x, y) & = x + y + 1 & \m{nil}_\AA & = 0 \end{align*} で定めれば $\AA$ は単調性を満たす。 例えば $\alpha(x) = 1$, $\alpha(y) = 2$ を満たす付値 $\alpha$ において 項 $\m{cons}(x, y)$ と $\m{append}(\m{cons}(x, y), \m{nil})$ の値は 次のように計算される。 \begin{align*} & [\alpha]_\AA(\m{cons}(x, y)) = \m{cons}_\AA(\alpha(x), \alpha(y)) = 1 + 2 + 1 = 4 \\ & [\alpha]_\AA(\m{append}(\m{cons}(x, y), \m{nil})) = \m{append}_\AA(\m{cons}_\AA(\alpha(x), \alpha(y)), \m{nil}_\AA) = 2 \cdot (1 + 2 + 1) + 0 + 1 = 9 \end{align*}

例（単調でない関数）

二引数の関数 $\phi(x,y) = y + 1$ を考える。 $2 > 1$ であるが $\phi(0,2) = 0 \ngtr 0 = \phi(0,1)$ であるから、この関数は単調ではない。

具体的な項書換え系の停止性を証明するには、以下の定理が利用できます。

定理（[L79, Z94]）

項書換え系 $\RR$ に対し、ある単調代数 $\AA$ が存在し 全ての書き換え規則 $\ell \to r \in \RR$ と付値 $\alpha$ に対して \[ [\alpha]_\AA(\ell) > [\alpha]_\AA(r) \] が成立するならば $\RR$ は停止性を持つ。

例（多項式解釈による停止性証明）

項書換え系 \begin{align*} \m{append}(\m{nil}, \mi{ys}) & \to \mi{ys} \\ \m{append}(\m{cons}(x, \mi{xs}), \mi{ys}) & \to \m{cons}(x, \m{append}(\mi{xs}, \mi{ys})) \end{align*} に対し、単調代数を \begin{align*} \m{append}_\AA(x, y) & = 2x + y + 1 & \m{cons}_\AA(x, y) & = x + y + 1 & \m{nil}_A & = 0 \end{align*} と定める。 このとき、任意の自然数$x, \mi{xs}, \mi{ys}$について、 \begin{alignat*}{3} \m{append}_\AA(\m{nil}_\AA, \mi{ys}) = {} && \mi{ys} + 1 & > \mi{ys} && = \mi{ys} \\ \m{append}_\AA(\m{cons}_\AA(x, \mi{xs}), \mi{ys}) = {} && 2x + 2\mi{xs} + \mi{ys} + 3 & > x + 2\mi{xs} + \mi{ys} + 2 && = \m{cons}_\AA(x, \m{append}_\AA(\mi{xs}, \mi{ys})) \end{alignat*} が成立する。定理よりこの項書換え系は停止性を持つ。

最後にこの手法の限界について少しみてみましょう。

例（多項式解釈による停止性証明の限界）

項書換え系 \( \RR = \{\, \m{f}(\m{g}(x)) \to \m{g}(\m{f}(\m{f}(x))) \,\} \) は停止性を持つが、自然数上の解釈では停止性を証明できない [FZ96]。

理解を確かめるための練習問題として、例で見た足し算のTRSの停止性を先の定理で証明してみると良いでしょう。

3. 自動化方法

ここからは項書換え系の停止性を先程の定理に基づいて自動証明する方法を説明します。 次の二つのステップに分けて自動化を実現します。

  1. 多項式に関する制約条件を、量化子の現れない形で記述する（量化記号消去）
  2. 制約条件を自動的に解くための外部のソルバーを呼ぶ方法を理解する（Z3の使い方）

3.1. 量化記号消去

議論を簡単にするため、代数の解釈関数 $f_\AA$ の形を線形多項式に限定して考えることにしましょう： \[ f_\AA(\seq{x}) = a_0 + a_1 x_1 + \cdots a_n x_n \qquad (a_0,\seq{a} \in \NN) \] 線形多項式の比較は次の定理を用いて係数の比較に帰着させることができます。

定理（量化記号消去）

$a_0, \cdots, a_n, b_0, \cdots, b_n \in \NN$ とする。以下は同値。
  • 任意の $x_1, \cdots, x_n \in \NN$ について $a_0 + a_1 x_1 + \cdots + a_n x_n > b_0 + b_1 x_1 + \cdots + b_n x_n$
  • $a_0 > b_0$ かつ 任意の $i \in \{ 1, \cdots, n \}$ について $a_i \geqslant b_i$

例（量化記号消去の適用例）

項書換え系 \begin{align} \m{append}(\m{nil}, \mi{ys}) & \to \mi{ys} \\ \m{append}(\m{cons}(x, \mi{xs}), \mi{ys}) & \to \m{cons}(x, \m{append}(\mi{xs}, \mi{ys})) \end{align} に対し、停止性を証明する単調代数を見つけたい。解釈は線形多項式に固定して考える。 \begin{align*} \m{append}_\AA(x, y) & = a_0 + a_1 x + a_2 y & \m{cons}_\AA(x, y) & = c_0 + c_1 x + c_2 y & \m{nil}_\AA & = n_0 \end{align*} とする（各係数は自然数）。単調性を満たすために \[ a_1, a_2, c_1, c_2 > 0 \] を課す。 各規則の両辺を解釈したとき左辺が右辺より大きいという条件を満たす必要があり、 これは任意の自然数 $x, \mi{xs}, \mi{ys} \in \NN$ に対して \begin{align*} \m{append}_\AA(\m{nil}_\AA, \mi{ys}) & > \mi{ys} \\ \m{append}_\AA(\m{cons}_\AA(x, \mi{xs}), \mi{ys}) & > \m{cons}_\AA(x, \m{append}_\AA(\mi{xs}, \mi{ys})) \end{align*} が成立することである。解釈の定義に沿って両辺を計算すれば、この条件は不等式 \begin{align*} (a_0 + a_1 n_0) + a_2 \cdot \mi{ys} & > \mi{ys} \\ (a_0 + a_1 c_0 + a_2) + a_1 c_1 \cdot x + a_1 c_2 \cdot \mi{xs} + a_2 \cdot \mi{ys} & > (c_0 + c_2 a_0) + c_1 \cdot x + c_2 a_1 \cdot \mi{xs} + c_2 a_2 \cdot \mi{ys} \end{align*} が任意の自然数 $x, \mi{xs}, \mi{ys} \in \NN$ に対して成立することと同値であり、さらに量化記号消去を用いれば \begin{align*} a_0 + a_1 n_0 & > 0 & a_2 & \geqslant 1 \\ a_0 + a_1 c_0 & > c_0 + c_2 a_0 & a_1 c_1 & \geqslant c_1 & a_1 c_2 & \geqslant c_2 a_1 & a_2 & \geqslant c_2 a_2 \end{align*} と同値であるとわかる。単調性の条件 $a_1, a_2, c_1, c_2 > 0$ の下でこの制約式を解けば、例えば解として \begin{align*} a_0 & = 1 & a_1 & = 2 & a_2 & = 1 & c_0 & = 1 & c_1 & = 1 & c_2 & = 1 & n_0 & = 0 \end{align*} が得られる。解釈関数の係数に割り当てれば \begin{align*} \m{append}_\AA(x, y) & = 2x + y + 1 & \m{cons}_\AA(x, y) & = x + y + 1 & \m{nil}_A & = 0 \end{align*} を得ることができる。これが先の停止性証明で用いた単調代数であることを確認せよ。

3.2. 制約ソルバーZ3の使い方

整数不等式を解くプログラムを書くことは容易ではありません。 現代では幸いなことに、そのような問題を解く SMT ソルバーと呼ばれるツールを利用することができます。 その一つである Z3 を用いて先の制約式を解くことにしましょう。 使用している OS 環境次第では、Z3 を apt や homebrew などのパッケージマネージャからインストールできるはずです。

Z3 への入力は SMT-LIB フォーマットで記述します。 その書式は具体例から見て取れると思います。

例（制約式の充足解を求める）

制約式 \begin{align*} a_0 + a_1 n_0 & > 0 & a_2 & \geqslant 1 \\ a_0 + a_1 c_0 & > c_0 + c_2 a_0 & a_1 c_1 & \geqslant c_1 & a_1 c_2 & \geqslant c_2 a_1 & a_2 & \geqslant c_2 a_2 \end{align*} を全て満たす係数を Z3 を用いて求める。 append.smt2 をダウンロードし、上記の数式との対応関係を観察されたい。 コマンドラインから z3 append.smt2 を実行すると下記のような出力が得られる。 
$ z3 append.smt2
sat
((a0 2)
 (a1 14)
 (a2 4)
 (c0 11)
 (c1 1)
 (c2 1)
 (n0 7))
同じ解が表示されるとは限らないが、このように表示されれば成功である。 より小さな値からなる解も存在するが停止性証明には上記の解で十分である。

例（制約問題の解なし）

次に制約を満たすことができない場合のSMTソルバーの振る舞いを確認する。 停止性を持たない項書換え系 $\RR = \{ \m{f}(x) \to \m{f}(\m{f}(x)) \}$ から得られる制約条件は fff.smt2 のようになる。ダウンロードしコマンドラインから z3 fff.smt2 を実行すると次の出力を得る。 
$ z3 fff.smt2
unsat
(error "line 10 column 18: model is not available")
停止性を持たないため解の非存在を表す unsat が出力される。

4. 停止性ツールの実装

必要な道具は揃いましたので、実際に項書換え系の停止性を判定するプログラムを実装してみましょう。 停止性を自動証明する国際競技会 termCOMP があり、 そこで用いられている入出力書式に沿って作成するとよいでしょう。 項書換え系を記述するARI フォーマットで記述されたファイルをコマンドラインから受け取り、 停止性を持つならば YES、判定不能な場合は MAYBE を出力するプログラムを実装します。 例えば、リストの連接 (append.ari) 

(format TRS)
(fun nil 0)
(fun cons 2)
(fun append 2)
(rule (append nil ys) ys)
(rule (append (cons x xs) ys) (cons x (append xs ys)))
が入力に与えられた場合は、 
YES
停止性を持たない TRS $\{ \m{f}(x) \to \m{f}(\m{f}(x)) \}$ (fff.ari) 
(format TRS)
(fun f 1)
(rule (f x) (f (f x)))
が入力に与えられた場合は、 
MAYBE
のように動作します。 多項式解釈で停止性を証明できなくとも停止性を持たないとは結論できません。 ここでは MAYBE と出力するにとどめておきます。

停止性証明ツールの実装は四つの部分に分けられます。

参考までに関数型言語 Haskell で実装する場合のヒントを記します。

また雛形となるコード termination.zip を用意しました。 実装の参考にしてください。

参考文献

[L79]
D. Lankford. On Proving Term Rewriting Systems Are Noetherian. Technical Report MTP-3, Louisiana Technical University, 1979.
[Z94]
H. Zantema. Termination of Term Rewriting: Interpretation and Type Elimination. Journal of Symbolic Computation, 17:23–50, 1994.
[FZ96]
M. C. F. Ferreira and H. Zantema. Total Termination of Term Rewriting. Applicable Algebra in Engineering, Communication and Computing, 7:133–162, 1996.