単純型項書換え系上の依存対法における実効規則と直積型項へのラベル付け

摘要

単純型項書換え系は高階の関数プログラムの計算モデルであり，その重要な性質に停止性がある．単純型項書換え系の停止性証明法として草刈と酒井は強計算依存対法を提案した．これは，静的な再帰の部分で無限ループが発生しないことを示すことにより停止性を証明する手法である．本論文では，強計算依存対法により停止性証明を行う際に解く必要のある制約を取り扱いやすいように削減・変換する二つの方法を提案する．一つは実効規則の概念の導入であり，制約を劇的に削減することができる．もう一つは直積塑項へのラベル付け法の導入であり，制約の解法の選択肢を増加させることができる．