💻 computer science

Non-Termination of Logic Programs Using Patterns

本論文は、有限な書き換え列の無限集合を表すパターンを生成する新しい展開手法を導入することにより、非ループ型の非停止を検出するための項書き換えアプローチを論理プログラミングへと適応させ、それをNTIツールを用いて実験的に評価するものである。

原著者： Etienne Payet

公開日 2026-08-10

📖 1 分で読めます☕ さくっと読める

原著者： Etienne Payet

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

ロボットがパズルを解こうとしている様子を観察していると想像してみてください。時として、ロボットはループに陥ることがあります。ステップAを行い、次にステップBを行い、またステップAを行う、という動作を永遠に繰り返すのです。それはまるで、ハムスターが回し車の中で走っているようなものです。動いてはいますが、どこにも辿り着いていません。コンピュータサイエンスの世界、特に「論理プログラミング」と呼ばれる分野において、これらのロボットは一連のルールに従って質問に答えようとするプログラムです。もしプログラムがループに陥ると、仕事がいつまでも終わりません。これは、プログラマーが検出したいバグなのです。

しかし、より厄介な種類の問題があります。プログラムが、きれいに繰り返される円状の動きに陥るのではなく、あるステップを踏み、次に少し異なるステップを踏み、またほとんど同じに見えるけれど実は少し違うステップを踏む、といった具合に、全く同じパターンを繰り返すことなく永遠に動き続けてしまうことがあります。それはまるで、同じ動きを二度と繰り返さないまま、踊り続けるダンサーのようです。これは「非ループ型非停止（non-looping non-termination）」と呼ばれます。明確な「ループ」を指し示すことができないため、これを見つけ出すのは非常に困難です。こうした無限で非反復的なシーケンスを検知することは、プログラムがいずれ停止することを証明したい、あるいは、永遠に走り続けてしまう特定の開始地点を見つけ出したいと考えているコンピュータ科学者にとって、大きな挑戦となっています。

この論文は、これら捉えどころのない非反復的な無限ループを捕まえるための、巧妙で新しい方法を紹介しています。著者であるエティエンヌ・パエット（Etienne Payet）は、論理プログラムのためのスーパーパワーを備えた探偵のようなツール、「NTI」を構築しました。プログラムをステップごとに観察する代わりに（それでは永遠に時間がかかってしまいます）、このツールは「アンフォールディング（展開）」と呼ばれる手法を使用します。アンフォールディングを、複雑な折り紙の鶴を平らに広げて、その下に隠れた折り目のパターンを見ることに例えてみましょう。プログラムのルールをアンフォールディングすることで、ツールは「パターン」――つまり、単一の特定の経路だけでなく、プログラムが取り得る無限の経路の家族（集合）を記述する抽象的な設計図――を作り出します。

この論文の主な発見は、「単純なパターン（simple patterns）」と呼ばれる簡略化されたバージョンの設計図を用いることで、プログラムが単純なループに陥ることなく永遠に走り続けることを数学的に証明できるということです。著者は、非常に厄介なことで知られる41種類の論理プログラムを用いてこのツールをテストしました。その結果、ツールは多くのプログラムにおいて、無限で非反復的な経路を特定することに成功しました。これには、既存のどのツールも、そのプログラムが非停止であることを証明できなかった4つのプログラムも含まれています。しかし、論文は自身の限界についても正直に述べています。このツールはすべてのケースを解決できたわけではなく、いくつかのプログラムについては、実行後に停止したり、10秒間でタイムアウトしたりしました。著者は、彼らの手法が探偵の道具箱に加わった強力な新しい道具ではあるものの、まだすべての謎を解く魔法の杖ではないと示唆しています。彼らは、より多くのトリッキーな非反復的無限ループを捕まえられるよう、将来的にツールをより賢くしていく計画です。

技術要約：パターンを用いた論理プログラムの非停止性

問題提起
本論文は、論理プログラム（LP）における非停止性の自動検出について扱う。既存の研究の多くは「ループ」（無限に繰り返すことができる有限の書き換え列）の検出に焦点を当てているが、本研究が対象とするのは「非ループ型の非停止（non-looping non-termination）」である。これらは、いかなるループも埋め込まない無限の書き換え列であり、本質的に非周期的であり、検出が困難である。著者によれば、このようなシーケンスは単純な論理プログラムからでも発生し得るが、標準的なループ検出手法ではそれらを特定できないことが多い。その動機は二重である。理論的な側面（驚くべき形式の無限シーケンスの研究）と、実用的な側面（プログラマーが永遠に実行され続けるクエリを特定するのを助けること）である。

手法
著者は、Emmesら（2012年）によって項書き換え系に対して導入されたアプローチを、論理プログラミングの領域に適応させている。核心となる手法は、有限の書き換えシーケンスの潜在的な無限集合を記述する「パターン」を生成する、新しい展開（unfolding）技術を定義することである。

パターンの定義:
- パターン置換（Pattern Substitutions）: 置換の集合 $\{\theta(n) = \sigma^n\mu \mid n \in \mathbb{N}\}$ を記述するペア $\theta = (\sigma, \mu)$ 、および $\sigma \star \mu$ として定義される。
- パターン項（Pattern Terms）: 集合 $\{s\theta(n) \mid n \in \mathbb{N}\}$ を記述するペア $(s, \theta)$ 。
- パターン規則（Pattern Rules）: パターン項のペア $(p, q)$ であり、バイナリ規則の集合 $\{(p(n), q(n)) \mid n \in \mathbb{N}\}$ を記述する。
正当性と展開:
- パターン規則がプログラム $P$ に対して**正しい（correct）**とは、それが記述する規則の集合が $P$ のバイナリ展開（$binunf(P)$）の部分集合であることを指す。
- 著者は、プログラム $P$ と正しいパターン規則の基底集合 $B$ からパターン規則を計算する、新しい展開演算子 $T^\pi_{P,B}$ を導入している。この演算子は、パターン項の単一化アルゴリズムを用いて規則を結合することで、無限の $binunf(P)$ の部分集合を有限の表現で捉え、従来のバイナリ展開よりも高速にプログラムを展開する。
単純なパターンと単一化:
- 自動化を可能にするため、著者はドメインを、単項コンテキストを含む特定の構造に従う「単純なパターン項（simple pattern terms）」に限定している。
- 単純なパターン項のための単一化アルゴリズムが提供されている。これは、単純なパターン項を特殊なシグネチャ $\Upsilon$ （繰り返される埋め込みを表す単項記号 $c_{a,b}$ を使用）上の項に写像し、古典的な単一化アルゴリズム（RobinsonやMartelli-Montanariなど）を適用するものである。
- このアルゴリズムは部分的に正しいことが証明されている。すなわち、成功裏に終了した場合、入力されたパターンシーケンスの最汎単一化子（mgu）を生成する。
非停止判定基準:
- 一般的基準（定理3）: Emmesらによる手法を適応したもので、もし展開されたパターンに $(u \star \sigma \star \mu, u\sigma^a \star \sigma^b\sigma' \star \mu\mu')$ という形式の規則が含まれ、 $\sigma'$ が $\sigma$ および $\mu$ と可換であるならば、無限の連鎖が存在すると述べている。
- 特別基準（定理5）: 「特殊なパターン規則（special pattern rules）」（単純な規則のサブセット）に対して、より容易にチェック可能な条件である。このような規則が展開内に存在する場合、その規則の左辺の特定のインスタンスから無限の連鎖が存在することが本論文で証明されている。

主な貢献
本論文の主な貢献は以下の4点である：

新しい展開技術: 論理プログラミングのための正しいパターン規則を生成する手法。これは、項書き換えにおける9つの推論規則よりもコンパクトな表現を提供し、複雑な適用戦略を必要としない。
単純なパターン項と単一化: 限定された形式のパターン項（「単純な」もの）の定義と、その正当性が証明された単一化アルゴリズム。
自動化可能な十分条件: 非ループ型の非停止を検出するための、容易にチェック可能な条件（定理5）。
実装（NTI）: このアプローチを NTI というツールとして実装したこと。

実験結果
著者は、Termination Problem Database (TPDB) にある非ループ型非停止の項書き換えシステム（TRS）に由来する41の論理プログラムを用いて、NTIを評価した。

成功: 本ツールは41プログラム中36プログラムに対して非停止性を証明することに成功した。特筆すべきは、2024年までのInternational Termination Competitionにおいて他のどのTRSアナライザによっても非停止性が証明されていなかった4つのプログラム（表中で † でマークされているもの）に対して成功した点である。
失敗: 本手法は5つのプログラムで失敗した。主な原因は、項の代表値の「自然な選択（natural choice）」（例12で議論）を用いる際の単一化アルゴリズムの不完全性、または単純なパターンへの制限（例9）によるものである。
パフォーマンス: 実行時間は概して低く、成功したケースでは300ミリ秒未満であったが、一部の複雑なケースではタイムアウトが発生した。

意義と主張
著者は、彼らのアプローチが、論理プログラムの停止性を否定できる、International Termination Competitionに参加している唯一のツールであると主張している。また、Payet (2024) による別の手法も非ループ型の非停止を証明できるが、それは異なる種類の非ループ性を扱っており、本論文でテストされた特定のプログラムの停止性を否定することはできないと述べている。逆に、Payet (2024) の手法は、本手法が失敗するプログラムの停止性を否定できる。したがって、これら2つのアプローチは補完的な関係にあると提示されている。

論文は、単一化アルゴリズムが現在は不完全であることや、単純なパターンへの制限が範囲を限定していること（例：変数を含む1-コンテキストを必要とするプログラムなど）を認め、控えめに結論づけている。今後の課題として、完全性の解決、初期のパターン生成（命題2）の拡張、およびEmmes et al. (2012) との直接比較のためのTRSへの適応が挙げられている。

関連論文