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

术语重写系统统一方法研究

基本信息

批准号：
07780267
负责人：
楫勇一
金额：
$ 0.58万
依托单位：
Nara Institute of Science and Technology
依托单位国家：
日本
项目类别：
Grant-in-Aid for Encouragement of Young Scientists (A)
财政年份：
1995
资助国家：
日本
起止时间：
1995 至无数据
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-07780267/
关键词：
単一化問題代入制約項書換え系計算複雑さ

项目摘要

代入制約付き単一化問題(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）非线性的。目标项中是否存在公共变量，以及 (b) 是否存在公共变量，并考虑了总共 12 个输入类的 CS-SUP 的可判定性和计算复杂性。因此，类 3Aa（满足上述所有条件 3、A 和 a 的输入类）、3Ab、3Ba 和 3Bb 的 CS-SUP 是不可判定的，类 1Aa、1Ab、1Ba、1Bb、2Aa、2Ab 、发现2Ba和2Bb是可测定的。关于CS-SUP的计算复杂度，对于类2Ab、2Ba和2Bb来说它是NP-hard的，对于类1Aa、1Ba和1Bb来说它是NP完全的，而且对于类2Aa和1Aa它是NP完全的。表明该问题可以在确定性多项式时间内解决。这些结果不仅在理论上很有趣，而且还为扩展 CS-UP 确定程序提供了重要意义。