Subtype inequalities
Subtype inequalities
复制标题
子类型不等式
DOI：
10.1109/lics.1992.185543
复制
发表时间：
1992
期刊：
影响因子：
--
通讯作者：
J. Tiuryn
中科院分区：
文献类型：
--
作者：
J. Tiuryn
研究了简单型子型不等式的可满足性问题。解决该问题的朴素算法对每个预定义的原子子类型的偏序集都在不确定的指数时间内运行，子类型不等式的可满足性问题是PSPACE-hard问题。另一方面，证明了如果原子子类型的偏置集是格的不相交并，则子类型不等式的可满足性问题在PTIME中是可解的。这一结果涵盖了原子子类型关系为相等时统一问题的重要特例
The satisfiability problem for subtype inequalities in simple types is studied. The naive algorithm that solves this problem runs in nondeterministic exponential time for every predefined poset of atomic subtypings the satisfiability problem for subtype inequalities is PSPACE-hard. On the other hand, it is proved that if the poset of atomic subtypings is a disjoint union of lattices, then the satisfiability problem for subtype inequalities is solvable in PTIME. This result covers the important special case of the unification problem that can be obtained when the atomic subtype relation is equality.<<ETX>>