高階差分にもとづくループ停止性証明方法

摘要

本稿では，高階差分の概念を導入することで，ある式の値がループの繰り返しのなかで「将来的に常に正になる(あるいは負となる)」という時相的な情報を利用してループの停止性証明を行う方法を提案する．単なる差分だけではなく，2階以上の差分(高階差分)を考慮することで，標準的なランキング関数にもとづくアプローチでは取扱いの面倒な，連続する複数回の繰り返しにまたがる式の値の変化を直接的に扱うことが可能となる．本稿で示す定理にもとづく証明は従来と同じ1階述語論理の範囲内で行えるため，充足可能性判定問題に帰着させることでSMTソルバを用いた効率的な判定が可能である．