手続き型プログラムから書換え系への変換に基づく

摘要

項書換えの分野では帰納的定理の証明手法として潜在帰納法や書換え帰納法などが広く研究されている．2つの異なる関数が任意の入力に対して同様の出力を返すことは帰納的定職として捉えられるので，帰納的定理の証明法は関数型プログラムの等価性の検証に利用できる．本研究では，項書換えにおける帰納的定理の証明法を利用して手続き型プログラムの等価性の検証を試みる．具体的には，手続き型プログラムから書換え系への変換を与え，その変換により手続き型プログラムの等価性を項書換え系の関数の等価性に帰着できることを示す．