強計算性に基づいた単純型項書換え系の停止性証明法

摘要

停止性を持つ関数プログラムは評価を安全に実行できるだけでなく，様々な性質を検証する際に帰納法の土台として簡約関係自体を利用することもできる．それゆえに，関数プログラムの停止性証明法は非常に重要である．本論文では，依存対法と呼ばれる再帰構造解析法を用いた停止性証明法を与える．本手法の特長は，型付きλ計算の停止性証明で導入された強計算性の概念に基づいていることである．強計算性の概念を用いることにより，我々の再帰構造解析は取り扱いの困難な高階変数を事実上取り扱わなくてよい．そのため，非常に強力でかつ効率的な解析法になっている．