項書換え系の単一化手法に関する研究

代入制約付き単一化問題(CS-UP)の判定手続きを拡張・一般化することを目的として研究を行ってきたが、手続きの対象となるクラスをわずかに広げただけでも同問題が決定不能となる場合が多く、CS-UPの計算複雑さが予想以上に大きいことが明らかになった。そこで問題の対象をCS-UPにおいて公理系が存在しない場合(代入制約付き構文的単一化問題、CS-SUP)に限定し、CS-SUPの計算量が入力クラスの大きさに対しどのように変化するかを考察した。具体的には、利用可能な項が(1)閉じている、(2)閉じているか線形である、(3)一般に非線形でも良い;ゴール項が(A)ともに線形である、(B)非線形でも良い;ゴール項に共通変数が(a)存在する、(b)存在しない;の3種の条件を考え、計12の入力クラスに対するCS-SUPの決定可能性、計算量について考察を行った。その結果、クラス3Aa(上記条件3、A、aの全てを満足する入力クラス)、3Ab、3Ba、3Bbに対するCS-SUPは決定不能であること、クラス1Aa、1Ab、1Ba、1Bb、2Aa、2Ab、2Ba、2Bbに対するCS-SUPは決定可能であることが明らかになった。またCS-SUPの計算量について、クラス2Ab、2Ba、2Bbに対してはNP-困難であること、クラス1Aa、1Ba、1Bbに対してはNP-完全であること、さらにクラス2Aa、1Aaに対しては決定性多項式時間で解けることを示した。これらの結果は理論的に興味深いだけでなく、CS-UPの判定手続きを拡張する上においても大きな示唆を与えるものであると考えられる。

代入制約付き単一化問題(CS-UP)の判定手続きを拡張・一般化することを目的として研究を行ってきたが、手続きの対象となるクラスをわずかに広げただけでも同問題が決定不能となる場合が多く、CS-UPの計算複雑さが予想以上に大きいことが明らかになった。そこで問題の対象をCS-UPにおいて公理系が存在しない場合(代入制約付き構文的単一化問題、CS-SUP)に限定し、CS-SUPの計算量が入力クラスの大きさに対しどのように変化するかを考察した。具体的には、利用可能な項が(1)閉じている、(2)閉じているか線形である、(3)一般に非線形でも良い;ゴール項が(A)ともに線形である、(B)非線形でも良い;ゴール項に共通変数が(a)存在する、(b)存在しない;の3種の条件を考え、計12の入力クラスに対するCS-SUPの決定可能性、計算量について考察を行った。その結果、クラス3Aa(上記条件3、A、aの全てを満足する入力クラス)、3Ab、3Ba、3Bbに対するCS-SUPは決定不能であること、クラス1Aa、1Ab、1Ba、1Bb、2Aa、2Ab、2Ba、2Bbに対するCS-SUPは決定可能であることが明らかになった。またCS-SUPの計算量について、クラス2Ab、2Ba、2Bbに対してはNP-困難であること、クラス1Aa、1Ba、1Bbに対してはNP-完全であること、さらにクラス2Aa、1Aaに対しては決定性多項式時間で解けることを示した。これらの結果は理論的に興味深いだけでなく、CS-UPの判定手続きを拡張する上においても大きな示唆を与えるものであると考えられる。