高階書換え系における引数切り落とし関数の下での実効規則について

摘要

高階書換え系（HRS）での強力な停止性証明手法として静的依存対法が知られている．この手法は静的な再帰構造解析を行い，静的再帰成分と呼ばれる解析結果の非循環性を示すことで証明を行う．この際に，非循環性を示すために考慮すべき規則を絞り込む実効規則と呼ばれる概念が提案されているが，高階変数を介した依存解析が困難であるため規則を絞り込めない場合がある．一方，一階の書換え系ではより考慮すべき規則を絞り込む，引数切り落とし関数の下での実効規則が提案されている．本研究ではこの成果をHRS上に拡張する．高階変数から始まる部分項を切り落とすことにより高階変数を介した依存解析を考慮せずにすむため，証明力を飛躍的に向上させることができる．