再帰プログラム部分計算のための停止性判定法

概要

論文の詳細を見る
本稿ではまず, 部分計算に関する新しい停止性判定法である再帰条件法を提案する.再帰条件法は, 既存の停止性判断法である実引数法と同じく, 同相埋め込み(homeomorphic embedding)関係を利用した整列擬順序(well-quasi ordering)に基づく判定法である.実引数法が, 実引数の文字列的な順序に関する逆順を調べるのに対して, 再帰条件法は, 再帰呼出しが起こる場合の条件(再帰条件)に関する指標の文字列的な逆順を調べる.したがって, 両者とも, 任意の部分計算を必ず止めることのできる停止性判定条件であるが, 止まるタイミングは同じとは限らない.どちらが先に止まるかは, 実行される部分計算によって異なる.しかし, 再帰条件法は意味論的な情報をより多く持つ再帰条件を用いるため, 多くの場合に, 実引数法よりある意味で都合良く止まることができる.本稿ではこの2つの停止条件の利害得失について詳細に議論する.さらに, 本稿では再帰条件法と実引数法の長所を取り入れた混合法を提案する.混合法は, この両者の停止条件をともに満たす場合にのみ停止するので, いかなる場合でも両者よりも早く止まる可能性がない判定法である.
一般社団法人情報処理学会の論文
2000-11-15